\profile "Java Profile"; \settings { "#Proof-Settings-Config-File #Tue Jan 31 15:49:36 CET 2017 [StrategyProperty]VBT_PHASE=VBT_SYM_EX [SMTSettings]useUninterpretedMultiplication=true [SMTSettings]SelectedTaclets= [StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT [StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF [StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER [StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF [StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF [StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS [StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE [SMTSettings]instantiateHierarchyAssumptions=true [StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF [StrategyProperty]DEP_OPTIONS_KEY=DEP_ON [StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT [StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE [StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF [StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF [Strategy]Timeout=-1 [Strategy]MaximumNumberOfAutomaticApplications=10000 [SMTSettings]integersMaximum=2147483645 [Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , moreSeqRules-moreSeqRules\\:on , permissions-permissions\\:off , joinGenerateIsWeakeningGoal-joinGenerateIsWeakeningGoal\\:off [SMTSettings]useConstantsForBigOrSmallIntegers=true [StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT [StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON [StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE [SMTSettings]maxGenericSorts=2 [SMTSettings]integersMinimum=-2147483645 [SMTSettings]invariantForall=false [SMTSettings]UseBuiltUniqueness=false [SMTSettings]explicitTypeHierarchy=false [Strategy]ActiveStrategy=JavaCardDLStrategy [StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED " } \javaSource ""; \proofObligation "#Proof Obligation Settings #Tue Jan 31 15:49:36 CET 2017 name=Sort[Sort\\:\\:max(int)].JML normal_behavior operation contract.0 contract=Sort[Sort\\:\\:max(int)].JML normal_behavior operation contract.0 class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO "; \proof { (keyLog "0" (keyUser "pschmitt" ) (keyVersion "3b928241d3c6497f2bf3626bad48a3118b304db1")) (autoModeTime "2414") (branch "dummy ID" (builtin "One Step Simplification" (formula "1") (newnames "start,self,result,exc,heapAtPre,o,f")) (rule "impRight" (formula "1")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "2")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "3")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "4")) (rule "andLeft" (formula "1")) (rule "andLeft" (formula "1")) (rule "notLeft" (formula "2")) (rule "eqSymm" (formula "10") (term "0,0,1,0,1")) (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,1,0,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,1,0,0,0,1")) (rule "polySimp_addComm1" (formula "10") (term "0,1,0,1,0,0,0,1")) (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,0,0,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) (rule "inEqSimp_ltToLeq" (formula "7")) (rule "polySimp_mulComm0" (formula "7") (term "1,0,0")) (rule "polySimp_addComm1" (formula "7") (term "0")) (rule "inEqSimp_gtToGeq" (formula "5")) (rule "times_zero_1" (formula "5") (term "1,0,0")) (rule "add_zero_right" (formula "5") (term "0,0")) (rule "inEqSimp_commuteGeq" (formula "10") (term "1,0,0,0,0,0,1")) (rule "inEqSimp_commuteLeq" (formula "10") (term "0,0,0,0,0,0,0,1")) (rule "inEqSimp_commuteLeq" (formula "6")) (rule "assignment" (formula "10") (term "1")) (builtin "One Step Simplification" (formula "10")) (rule "inEqSimp_sepNegMonomial0" (formula "7")) (rule "polySimp_mulLiterals" (formula "7") (term "0")) (rule "polySimp_elimOne" (formula "7") (term "0")) (rule "inEqSimp_sepPosMonomial1" (formula "5")) (rule "mul_literals" (formula "5") (term "1")) (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,0,0,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,0,0,0,0,1")) (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,0,0,0,0,1")) (rule "mul_literals" (formula "10") (term "0,1,1,0,0,0,0,0,0,1")) (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,0,0,0,0,1")) (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,0,0,0,0,1")) (rule "inEqSimp_sepNegMonomial0" (formula "10") (term "1,0,1,0,0,0,1")) (rule "polySimp_mulLiterals" (formula "10") (term "0,1,0,1,0,0,0,1")) (rule "polySimp_elimOne" (formula "10") (term "0,1,0,1,0,0,0,1")) (rule "nnf_imp2or" (formula "10") (term "0,0,0,0,0,1")) (rule "nnf_notAnd" (formula "10") (term "0,0,0,0,0,0,1")) (rule "inEqSimp_notGeq" (formula "10") (term "0,0,0,0,0,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,0,0,0,0,0,0,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "0,0,0,0,0,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,0,0,0,0,0,1")) (rule "polySimp_rightDist" (formula "10") (term "1,0,0,0,0,0,0,0,1")) (rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0,0,0,0,0,0,1")) (rule "mul_literals" (formula "10") (term "0,1,0,0,0,0,0,0,0,1")) (rule "polySimp_elimOne" (formula "10") (term "1,1,0,0,0,0,0,0,0,1")) (rule "inEqSimp_notLeq" (formula "10") (term "1,0,0,0,0,0,0,1")) (rule "polySimp_rightDist" (formula "10") (term "1,0,0,1,0,0,0,0,0,0,1")) (rule "mul_literals" (formula "10") (term "0,1,0,0,1,0,0,0,0,0,0,1")) (rule "polySimp_addAssoc" (formula "10") (term "0,0,1,0,0,0,0,0,0,1")) (rule "add_literals" (formula "10") (term "0,0,0,1,0,0,0,0,0,0,1")) (rule "add_zero_left" (formula "10") (term "0,0,1,0,0,0,0,0,0,1")) (rule "inEqSimp_sepPosMonomial1" (formula "10") (term "1,0,0,0,0,0,0,1")) (rule "polySimp_mulLiterals" (formula "10") (term "1,1,0,0,0,0,0,0,1")) (rule "polySimp_elimOne" (formula "10") (term "1,1,0,0,0,0,0,0,1")) (rule "Class_invariant_axiom_for_Sort" (formula "8") (inst "sk=sk_0") (ifseqformula "3")) (branch "Use Axiom" (rule "notLeft" (formula "8")) (rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore_max,savedHeapBefore_max,_startBefore_max")) (builtin "One Step Simplification" (formula "10")) (rule "variableDeclarationAssign" (formula "10") (term "1")) (rule "variableDeclaration" (formula "10") (term "1") (newnames "counter")) (rule "assignment" (formula "10") (term "1")) (builtin "One Step Simplification" (formula "10")) (rule "variableDeclarationAssign" (formula "10") (term "1")) (rule "variableDeclaration" (formula "10") (term "1") (newnames "idx")) (rule "assignment" (formula "10") (term "1")) (builtin "One Step Simplification" (formula "10")) (builtin "Loop Invariant" (formula "10") (newnames "variant,b,heapBefore_LOOP,counterBefore_LOOP,idxBefore_LOOP,counter_0,idx_0,heap_After_LOOP,anon_heap_LOOP,o,f")) (branch "Invariant Initially Valid" (builtin "One Step Simplification" (formula "10") (ifInst "" (formula "1"))) (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0,0,1")) (rule "inEqSimp_ltToLeq" (formula "10") (term "1,0")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0,1,0")) (rule "polySimp_addComm1" (formula "10") (term "0,1,0")) (rule "inEqSimp_commuteLeq" (formula "10") (term "1,0,0,0")) (rule "inEqSimp_commuteGeq" (formula "10") (term "1,0,1")) (rule "inEqSimp_homoInEq0" (formula "10") (term "1,0,0")) (rule "polySimp_pullOutFactor1" (formula "10") (term "0,1,0,0")) (rule "add_literals" (formula "10") (term "1,0,1,0,0")) (rule "times_zero_1" (formula "10") (term "0,1,0,0")) (rule "qeq_literals" (formula "10") (term "1,0,0")) (builtin "One Step Simplification" (formula "10")) (rule "inEqSimp_homoInEq0" (formula "10") (term "0,0,0")) (rule "polySimp_pullOutFactor1" (formula "10") (term "0,0,0,0")) (rule "add_literals" (formula "10") (term "1,0,0,0,0")) (rule "times_zero_1" (formula "10") (term "0,0,0,0")) (rule "qeq_literals" (formula "10") (term "0,0,0")) (builtin "One Step Simplification" (formula "10")) (rule "inEqSimp_sepPosMonomial0" (formula "10") (term "1,0,0,1")) (rule "polySimp_mulComm0" (formula "10") (term "1,1,0,0,1")) (rule "polySimp_rightDist" (formula "10") (term "1,1,0,0,1")) (rule "mul_literals" (formula "10") (term "0,1,1,0,0,1")) (rule "polySimp_mulLiterals" (formula "10") (term "1,1,1,0,0,1")) (rule "polySimp_elimOne" (formula "10") (term "1,1,1,0,0,1")) (rule "inEqSimp_sepNegMonomial0" (formula "10") (term "1,0")) (rule "polySimp_mulLiterals" (formula "10") (term "0,1,0")) (rule "polySimp_elimOne" (formula "10") (term "0,1,0")) (rule "replace_known_left" (formula "10") (term "1,0") (ifseqformula "7")) (builtin "One Step Simplification" (formula "10")) (rule "inEqSimp_subsumption1" (formula "10") (term "0") (ifseqformula "7")) (rule "inEqSimp_homoInEq0" (formula "10") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "10") (term "0,0,0")) (rule "add_literals" (formula "10") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "10") (term "1,0,0,0")) (rule "add_zero_right" (formula "10") (term "0,0,0")) (rule "qeq_literals" (formula "10") (term "0,0")) (builtin "One Step Simplification" (formula "10")) (rule "allRight" (formula "10") (inst "sk=x_11")) (rule "impRight" (formula "10")) (rule "andLeft" (formula "1")) (rule "inEqSimp_leqRight" (formula "12")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "1")) (rule "polySimp_mulComm0" (formula "1") (term "1")) (rule "polySimp_rightDist" (formula "1") (term "1")) (rule "mul_literals" (formula "1") (term "0,1")) (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) (rule "polySimp_elimOne" (formula "1") (term "1,1")) (rule "inEqSimp_contradInEq0" (formula "2") (ifseqformula "3")) (rule "andLeft" (formula "2")) (rule "inEqSimp_homoInEq1" (formula "2")) (rule "polySimp_mulComm0" (formula "2") (term "1,0")) (rule "polySimp_rightDist" (formula "2") (term "1,0")) (rule "mul_literals" (formula "2") (term "0,1,0")) (rule "polySimp_addAssoc" (formula "2") (term "0")) (rule "polySimp_addComm0" (formula "2") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "2") (term "0")) (rule "add_literals" (formula "2") (term "1,1,0")) (rule "times_zero_1" (formula "2") (term "1,0")) (rule "add_zero_right" (formula "2") (term "0")) (rule "leq_literals" (formula "2")) (rule "closeFalse" (formula "2")) ) (branch "Body Preserves Invariant" (builtin "One Step Simplification" (formula "9")) (builtin "One Step Simplification" (formula "12")) (rule "translateJavaSubInt" (formula "12") (term "0,1,1,1,0,1")) (rule "translateJavaSubInt" (formula "12") (term "0,1,1,1,0,1,1")) (rule "andLeft" (formula "9")) (rule "impRight" (formula "13")) (rule "andLeft" (formula "10")) (rule "andLeft" (formula "10")) (rule "andLeft" (formula "10")) (rule "andLeft" (formula "10")) (rule "eqSymm" (formula "18") (term "0,0,1,0,1,1,0,1")) (rule "polySimp_elimSub" (formula "18") (term "0,1,1,1,0")) (rule "polySimp_elimSub" (formula "18") (term "0,1,1,1,0,1")) (rule "polySimp_addComm0" (formula "18") (term "0,1,1,1,0")) (rule "polySimp_addComm0" (formula "18") (term "0,1,1,1,0,1")) (rule "inEqSimp_ltToLeq" (formula "15") (term "1,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,0,0,1,0,0")) (rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,0,1,1,0,1")) (rule "polySimp_addComm1" (formula "18") (term "0,1,0,0,0,1,1,0,1")) (rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,0,0,1,1,0,1")) (rule "polySimp_addComm1" (formula "18") (term "0,1,0,0,0,0,1,1,0,1")) (rule "inEqSimp_ltToLeq" (formula "14")) (rule "polySimp_mulComm0" (formula "14") (term "1,0,0")) (rule "polySimp_addComm1" (formula "14") (term "0")) (rule "inEqSimp_ltToLeq" (formula "13")) (rule "polySimp_mulComm0" (formula "13") (term "1,0,0")) (rule "polySimp_addComm1" (formula "13") (term "0")) (rule "inEqSimp_commuteGeq" (formula "15") (term "1,0")) (rule "inEqSimp_commuteLeq" (formula "18") (term "1,0,0,0,0,0,0,1,1,0,1")) (rule "inEqSimp_commuteGeq" (formula "18") (term "1,0,1,0,0,1,1,0,1")) (rule "inEqSimp_commuteLeq" (formula "18") (term "0,0,0,0,0,0,0,1,1,0,1")) (rule "inEqSimp_commuteLeq" (formula "18") (term "1,0,0,0,0,0,1,1,0,1")) (rule "inEqSimp_commuteLeq" (formula "11")) (rule "variableDeclarationAssign" (formula "1") (term "1")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "1") (term "1") (newnames "b_2")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "exc_1")) (rule "assignment" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "thrownExc")) (rule "blockThrow" (formula "18") (term "1,0,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "15") (term "1,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,1,0,0")) (rule "polySimp_rightDist" (formula "15") (term "1,1,0,0")) (rule "mul_literals" (formula "15") (term "0,1,1,0,0")) (rule "polySimp_mulLiterals" (formula "15") (term "1,1,1,0,0")) (rule "polySimp_elimOne" (formula "15") (term "1,1,1,0,0")) (rule "inEqSimp_sepNegMonomial0" (formula "14")) (rule "polySimp_mulLiterals" (formula "14") (term "0")) (rule "polySimp_elimOne" (formula "14") (term "0")) (rule "inEqSimp_sepNegMonomial0" (formula "13")) (rule "polySimp_mulLiterals" (formula "13") (term "0")) (rule "polySimp_elimOne" (formula "13") (term "0")) (rule "inEqSimp_sepNegMonomial0" (formula "17") (term "1,0,0,0,0,1,1,0,1")) (rule "polySimp_mulLiterals" (formula "17") (term "0,1,0,0,0,0,1,1,0,1")) (rule "polySimp_elimOne" (formula "17") (term "0,1,0,0,0,0,1,1,0,1")) (rule "inEqSimp_sepNegMonomial0" (formula "17") (term "1,0,0,0,1,1,0,1")) (rule "polySimp_mulLiterals" (formula "17") (term "0,1,0,0,0,1,1,0,1")) (rule "polySimp_elimOne" (formula "17") (term "0,1,0,0,0,1,1,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "17") (term "1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "17") (term "1,1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_rightDist" (formula "17") (term "1,1,0,0,1,0,0,1,1,0,1")) (rule "mul_literals" (formula "17") (term "0,1,1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulLiterals" (formula "17") (term "1,1,1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_elimOne" (formula "17") (term "1,1,1,0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_exactShadow3" (formula "7") (ifseqformula "12")) (rule "times_zero_1" (formula "7") (term "0,0")) (rule "add_zero_left" (formula "7") (term "0")) (rule "inEqSimp_exactShadow3" (formula "8") (ifseqformula "11")) (rule "mul_literals" (formula "8") (term "0,0")) (rule "add_zero_left" (formula "8") (term "0")) (rule "boxToDiamond" (formula "1") (term "1")) (builtin "One Step Simplification" (formula "1")) (rule "notLeft" (formula "1")) (rule "nnf_imp2or" (formula "15") (term "0")) (rule "nnf_notAnd" (formula "15") (term "0,0")) (rule "inEqSimp_notLeq" (formula "15") (term "1,0,0")) (rule "polySimp_rightDist" (formula "15") (term "1,0,0,1,0,0")) (rule "mul_literals" (formula "15") (term "0,1,0,0,1,0,0")) (rule "polySimp_addAssoc" (formula "15") (term "0,0,1,0,0")) (rule "add_literals" (formula "15") (term "0,0,0,1,0,0")) (rule "add_zero_left" (formula "15") (term "0,0,1,0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "15") (term "1,0,0")) (rule "polySimp_mulLiterals" (formula "15") (term "1,1,0,0")) (rule "polySimp_elimOne" (formula "15") (term "1,1,0,0")) (rule "inEqSimp_notGeq" (formula "15") (term "0,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,0,0,0,0,0")) (rule "inEqSimp_sepPosMonomial0" (formula "15") (term "0,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,0,0,0")) (rule "polySimp_rightDist" (formula "15") (term "1,0,0,0")) (rule "mul_literals" (formula "15") (term "0,1,0,0,0")) (rule "polySimp_mulLiterals" (formula "15") (term "1,1,0,0,0")) (rule "polySimp_elimOne" (formula "15") (term "1,1,0,0,0")) (rule "nnf_imp2or" (formula "19") (term "0,1,0,0,1,1,0,1")) (rule "nnf_notAnd" (formula "19") (term "0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_notLeq" (formula "19") (term "1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_rightDist" (formula "19") (term "1,0,0,1,0,0,1,0,0,1,1,0,1")) (rule "mul_literals" (formula "19") (term "0,1,0,0,1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_addAssoc" (formula "19") (term "0,0,1,0,0,1,0,0,1,1,0,1")) (rule "add_literals" (formula "19") (term "0,0,0,1,0,0,1,0,0,1,1,0,1")) (rule "add_zero_left" (formula "19") (term "0,0,1,0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_sepPosMonomial1" (formula "19") (term "1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulLiterals" (formula "19") (term "1,1,0,0,1,0,0,1,1,0,1")) (rule "polySimp_elimOne" (formula "19") (term "1,1,0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_notGeq" (formula "19") (term "0,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "19") (term "1,0,0,0,0,0,1,0,0,1,1,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "19") (term "0,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulComm0" (formula "19") (term "1,0,0,0,1,0,0,1,1,0,1")) (rule "polySimp_rightDist" (formula "19") (term "1,0,0,0,1,0,0,1,1,0,1")) (rule "mul_literals" (formula "19") (term "0,1,0,0,0,1,0,0,1,1,0,1")) (rule "polySimp_mulLiterals" (formula "19") (term "1,1,0,0,0,1,0,0,1,1,0,1")) (rule "polySimp_elimOne" (formula "19") (term "1,1,0,0,0,1,0,0,1,1,0,1")) (rule "commute_or" (formula "15") (term "0,0")) (rule "compound_less_than_comparison_2" (formula "16") (term "1") (inst "#v1=x_1") (inst "#v0=x")) (rule "variableDeclarationAssign" (formula "16") (term "1")) (rule "variableDeclaration" (formula "16") (term "1") (newnames "x_2")) (rule "assignment" (formula "16") (term "1")) (builtin "One Step Simplification" (formula "16")) (rule "variableDeclarationAssign" (formula "16") (term "1")) (rule "variableDeclaration" (formula "16") (term "1") (newnames "x_3")) (rule "eval_order_access2" (formula "16") (term "1") (inst "#v0=x_arr")) (rule "variableDeclarationAssign" (formula "16") (term "1")) (rule "variableDeclaration" (formula "16") (term "1") (newnames "x_arr_1")) (rule "assignment_read_attribute_this" (formula "16")) (builtin "One Step Simplification" (formula "16")) (rule "assignment_read_length" (formula "16")) (branch "Normal Execution (x_arr_1 != null)" (builtin "One Step Simplification" (formula "16")) (rule "less_than_comparison_simple" (formula "16") (term "1")) (builtin "One Step Simplification" (formula "16")) (rule "inEqSimp_ltToLeq" (formula "16") (term "0,0,0")) (rule "polySimp_mulComm0" (formula "16") (term "1,0,0,0,0,0")) (rule "polySimp_addComm1" (formula "16") (term "0,0,0,0")) (rule "inEqSimp_sepNegMonomial0" (formula "16") (term "0,0,0")) (rule "polySimp_mulLiterals" (formula "16") (term "0,0,0,0")) (rule "polySimp_elimOne" (formula "16") (term "0,0,0,0")) (rule "methodCallEmpty" (formula "16") (term "1")) (rule "emptyModality" (formula "16") (term "1")) (builtin "One Step Simplification" (formula "16")) (rule "notRight" (formula "16")) (rule "inEqSimp_subsumption1" (formula "13") (ifseqformula "1")) (rule "inEqSimp_homoInEq0" (formula "13") (term "0")) (rule "polySimp_pullOutFactor1b" (formula "13") (term "0,0")) (rule "add_literals" (formula "13") (term "1,1,0,0")) (rule "times_zero_1" (formula "13") (term "1,0,0")) (rule "add_literals" (formula "13") (term "0,0")) (rule "qeq_literals" (formula "13") (term "0")) (builtin "One Step Simplification" (formula "13")) (rule "true_left" (formula "13")) (rule "arrayLengthIsAShort" (formula "10") (term "0")) (builtin "One Step Simplification" (formula "10")) (rule "true_left" (formula "10")) (rule "arrayLengthNotNegative" (formula "10") (term "0")) (rule "inEqSimp_subsumption1" (formula "10") (ifseqformula "6")) (rule "leq_literals" (formula "10") (term "0")) (builtin "One Step Simplification" (formula "10")) (rule "true_left" (formula "10")) (rule "ifUnfold" (formula "18") (term "1") (inst "#boolv=x")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_4")) (rule "compound_less_than_comparison_2" (formula "18") (term "1") (inst "#v1=x_6") (inst "#v0=x_5")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_5")) (rule "assignment" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_6")) (rule "eval_order_array_access6" (formula "18") (term "1") (inst "#v0=x_arr")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_arr_2")) (rule "assignment_read_attribute_this" (formula "18")) (builtin "One Step Simplification" (formula "18")) (rule "assignment_read_length" (formula "18")) (branch "Normal Execution (x_arr_2 != null)" (builtin "One Step Simplification" (formula "18")) (rule "less_than_comparison_simple" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "inEqSimp_ltToLeq" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0,1,0")) (rule "polySimp_addComm1" (formula "18") (term "0,0,0,1,0")) (rule "inEqSimp_sepNegMonomial0" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulLiterals" (formula "18") (term "0,0,0,1,0")) (rule "polySimp_elimOne" (formula "18") (term "0,0,0,1,0")) (rule "replace_known_left" (formula "18") (term "0,0,1,0") (ifseqformula "1")) (builtin "One Step Simplification" (formula "18")) (rule "ifSplit" (formula "18")) (branch "if x_4 true" (builtin "One Step Simplification" (formula "19")) (builtin "One Step Simplification" (formula "1")) (rule "true_left" (formula "1")) (rule "ifUnfold" (formula "18") (term "1") (inst "#boolv=x")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_7")) (rule "compound_greater_than_comparison_2" (formula "18") (term "1") (inst "#v1=x_9") (inst "#v0=x_8")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_8")) (rule "eval_order_array_access4" (formula "18") (term "1") (inst "#v0=x_arr")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_arr_3")) (rule "assignment_read_attribute_this" (formula "18")) (builtin "One Step Simplification" (formula "18")) (rule "assignment_array2" (formula "18")) (branch "Normal Execution (x_arr_3 != null)" (builtin "One Step Simplification" (formula "18")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_9")) (rule "eval_order_array_access4" (formula "18") (term "1") (inst "#v0=x_arr")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_arr_4")) (rule "assignment_read_attribute_this" (formula "18")) (builtin "One Step Simplification" (formula "18")) (rule "assignment_array2" (formula "18")) (branch "Normal Execution (x_arr_4 != null)" (builtin "One Step Simplification" (formula "18")) (rule "greater_than_comparison_simple" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "inEqSimp_gtToGeq" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0,1,0")) (rule "polySimp_addComm1" (formula "18") (term "0,0,0,1,0")) (rule "inEqSimp_sepNegMonomial1" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulLiterals" (formula "18") (term "0,0,0,1,0")) (rule "polySimp_elimOne" (formula "18") (term "0,0,0,1,0")) (rule "onlyCreatedObjectsAreReferenced" (formula "6") (term "0,0") (ifseqformula "2")) (rule "replace_known_right" (formula "6") (term "0") (ifseqformula "17")) (builtin "One Step Simplification" (formula "6")) (rule "ifSplit" (formula "19")) (branch "if x_7 true" (builtin "One Step Simplification" (formula "20")) (builtin "One Step Simplification" (formula "1")) (rule "assignment" (formula "20") (term "1")) (builtin "One Step Simplification" (formula "20")) (rule "assignmentAdditionInt" (formula "20") (term "1")) (builtin "One Step Simplification" (formula "20")) (rule "translateJavaAddInt" (formula "20") (term "0,1,0")) (rule "polySimp_addComm0" (formula "20") (term "0,1,0")) (rule "tryEmpty" (formula "20") (term "1")) (rule "methodCallEmpty" (formula "20") (term "1")) (rule "emptyModality" (formula "20") (term "1")) (builtin "One Step Simplification" (formula "20") (ifInst "" (formula "2")) (ifInst "" (formula "2")) (ifInst "" (formula "12"))) (rule "polySimp_mulComm0" (formula "20") (term "0,0,1")) (rule "polySimp_rightDist" (formula "20") (term "0,0,1")) (rule "mul_literals" (formula "20") (term "0,0,0,1")) (rule "precOfInt" (formula "20") (term "1")) (rule "inEqSimp_ltToLeq" (formula "20") (term "1,1")) (rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,1")) (rule "polySimp_mulAssoc" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_mulComm0" (formula "20") (term "0,0,1,0,0,1,1")) (rule "polySimp_mulLiterals" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_elimOne" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,1,1")) (rule "polySimp_addComm1" (formula "20") (term "0,0,1,1")) (rule "polySimp_pullOutFactor2b" (formula "20") (term "0,1,1")) (rule "add_literals" (formula "20") (term "1,1,0,1,1")) (rule "times_zero_1" (formula "20") (term "1,0,1,1")) (rule "add_zero_right" (formula "20") (term "0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,1,1")) (rule "polySimp_addComm1" (formula "20") (term "0,0,1,1")) (rule "add_literals" (formula "20") (term "0,0,0,1,1")) (rule "add_zero_left" (formula "20") (term "0,0,1,1")) (rule "polySimp_pullOutFactor1" (formula "20") (term "0,1,1")) (rule "add_literals" (formula "20") (term "1,0,1,1")) (rule "times_zero_1" (formula "20") (term "0,1,1")) (rule "leq_literals" (formula "20") (term "1,1")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_commuteGeq" (formula "20") (term "1,0,0")) (rule "replace_known_left" (formula "20") (term "1,0,0") (ifseqformula "14")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_commuteGeq" (formula "20") (term "0,0")) (rule "inEqSimp_homoInEq0" (formula "20") (term "1")) (rule "mul_literals" (formula "20") (term "1,0,1")) (rule "add_zero_right" (formula "20") (term "0,1")) (rule "inEqSimp_sepPosMonomial1" (formula "20") (term "1")) (rule "polySimp_mulComm0" (formula "20") (term "1,1")) (rule "polySimp_rightDist" (formula "20") (term "1,1")) (rule "mul_literals" (formula "20") (term "0,1,1")) (rule "polySimp_mulLiterals" (formula "20") (term "1,1,1")) (rule "polySimp_elimOne" (formula "20") (term "1,1,1")) (rule "replace_known_left" (formula "20") (term "1") (ifseqformula "2")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_subsumption0" (formula "20") (term "0") (ifseqformula "14")) (rule "inEqSimp_homoInEq0" (formula "20") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "20") (term "0,0,0")) (rule "add_literals" (formula "20") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "20") (term "1,0,0,0")) (rule "add_literals" (formula "20") (term "0,0,0")) (rule "qeq_literals" (formula "20") (term "0,0")) (builtin "One Step Simplification" (formula "20")) (rule "allRight" (formula "20") (inst "sk=x_10")) (rule "orRight" (formula "20")) (rule "orRight" (formula "20")) (rule "inEqSimp_leqRight" (formula "22")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "inEqSimp_leqRight" (formula "21")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_geqRight" (formula "22")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "3")) (rule "polySimp_mulComm0" (formula "3") (term "1")) (rule "polySimp_rightDist" (formula "3") (term "1")) (rule "polySimp_mulLiterals" (formula "3") (term "1,1")) (rule "mul_literals" (formula "3") (term "0,1")) (rule "polySimp_elimOne" (formula "3") (term "1,1")) (rule "inEqSimp_sepPosMonomial1" (formula "2")) (rule "polySimp_mulLiterals" (formula "2") (term "1")) (rule "polySimp_elimOne" (formula "2") (term "1")) (rule "inEqSimp_sepPosMonomial0" (formula "1")) (rule "polySimp_mulLiterals" (formula "1") (term "1")) (rule "polySimp_elimOne" (formula "1") (term "1")) (rule "inEqSimp_exactShadow3" (formula "2") (ifseqformula "1")) (rule "polySimp_mulComm0" (formula "2") (term "0,0")) (rule "polySimp_addComm0" (formula "2") (term "0")) (rule "inEqSimp_sepNegMonomial1" (formula "2")) (rule "polySimp_mulLiterals" (formula "2") (term "0")) (rule "polySimp_elimOne" (formula "2") (term "0")) (rule "allLeft" (formula "20") (inst "t=x_10")) (rule "inEqSimp_contradInEq1" (formula "20") (term "1,0") (ifseqformula "2")) (rule "inEqSimp_homoInEq1" (formula "20") (term "0,1,0")) (rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0")) (rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,0")) (rule "mul_literals" (formula "20") (term "0,1,0,0,1,0")) (rule "polySimp_addAssoc" (formula "20") (term "0,0,1,0")) (rule "polySimp_addComm0" (formula "20") (term "0,0,0,1,0")) (rule "polySimp_pullOutFactor1b" (formula "20") (term "0,0,1,0")) (rule "add_literals" (formula "20") (term "1,1,0,0,1,0")) (rule "times_zero_1" (formula "20") (term "1,0,0,1,0")) (rule "add_zero_right" (formula "20") (term "0,0,1,0")) (rule "leq_literals" (formula "20") (term "0,1,0")) (builtin "One Step Simplification" (formula "20")) (rule "cut_direct" (formula "20") (term "0")) (branch "CUT: x_10 >= counter_0 TRUE" (builtin "One Step Simplification" (formula "21")) (rule "true_left" (formula "21")) (rule "inEqSimp_antiSymm" (formula "20") (ifseqformula "1")) (rule "applyEqRigid" (formula "21") (term "0") (ifseqformula "20")) (rule "inEqSimp_homoInEq1" (formula "21")) (rule "polySimp_pullOutFactor1" (formula "21") (term "0")) (rule "add_literals" (formula "21") (term "1,0")) (rule "times_zero_1" (formula "21") (term "0")) (rule "leq_literals" (formula "21")) (rule "true_left" (formula "21")) (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "20")) (rule "inEqSimp_homoInEq0" (formula "1")) (rule "polySimp_pullOutFactor1" (formula "1") (term "0")) (rule "add_literals" (formula "1") (term "1,0")) (rule "times_zero_1" (formula "1") (term "0")) (rule "qeq_literals" (formula "1")) (rule "true_left" (formula "1")) (rule "applyEq" (formula "1") (term "0") (ifseqformula "19")) (rule "inEqSimp_commuteGeq" (formula "1")) (rule "applyEqRigid" (formula "1") (term "0,2,0") (ifseqformula "18")) (rule "inEqSimp_homoInEq1" (formula "1")) (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) (rule "add_literals" (formula "1") (term "1,1,0")) (rule "times_zero_1" (formula "1") (term "1,0")) (rule "add_zero_right" (formula "1") (term "0")) (rule "leq_literals" (formula "1")) (rule "closeFalse" (formula "1")) ) (branch "CUT: x_10 >= counter_0 FALSE" (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_geqRight" (formula "22")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "inEqSimp_sepPosMonomial0" (formula "1")) (rule "polySimp_mulComm0" (formula "1") (term "1")) (rule "polySimp_rightDist" (formula "1") (term "1")) (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) (rule "mul_literals" (formula "1") (term "0,1")) (rule "polySimp_elimOne" (formula "1") (term "1,1")) (rule "inEqSimp_subsumption0" (formula "2") (ifseqformula "1")) (rule "inEqSimp_homoInEq0" (formula "2") (term "0")) (rule "polySimp_mulComm0" (formula "2") (term "1,0,0")) (rule "polySimp_rightDist" (formula "2") (term "1,0,0")) (rule "mul_literals" (formula "2") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "2") (term "0,0")) (rule "polySimp_addComm0" (formula "2") (term "0,0,0")) (rule "polySimp_pullOutFactor1b" (formula "2") (term "0,0")) (rule "add_literals" (formula "2") (term "1,1,0,0")) (rule "times_zero_1" (formula "2") (term "1,0,0")) (rule "add_zero_right" (formula "2") (term "0,0")) (rule "qeq_literals" (formula "2") (term "0")) (builtin "One Step Simplification" (formula "2")) (rule "true_left" (formula "2")) (rule "inEqSimp_exactShadow3" (formula "2") (ifseqformula "1")) (rule "polySimp_mulComm0" (formula "2") (term "0,0")) (rule "polySimp_addComm0" (formula "2") (term "0")) (rule "inEqSimp_sepNegMonomial1" (formula "2")) (rule "polySimp_mulLiterals" (formula "2") (term "0")) (rule "polySimp_elimOne" (formula "2") (term "0")) (rule "inEqSimp_subsumption0" (formula "18") (ifseqformula "2")) (rule "inEqSimp_homoInEq0" (formula "18") (term "0")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0")) (rule "polySimp_rightDist" (formula "18") (term "1,0,0")) (rule "mul_literals" (formula "18") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "18") (term "0,0")) (rule "polySimp_addComm0" (formula "18") (term "0,0,0")) (rule "polySimp_pullOutFactor1b" (formula "18") (term "0,0")) (rule "add_literals" (formula "18") (term "1,1,0,0")) (rule "times_zero_1" (formula "18") (term "1,0,0")) (rule "add_zero_right" (formula "18") (term "0,0")) (rule "qeq_literals" (formula "18") (term "0")) (builtin "One Step Simplification" (formula "18")) (rule "true_left" (formula "18")) (rule "inEqSimp_exactShadow3" (formula "4") (ifseqformula "20")) (rule "polySimp_rightDist" (formula "4") (term "0,0")) (rule "mul_literals" (formula "4") (term "0,0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "4")) (rule "polySimp_mulComm0" (formula "4") (term "1")) (rule "polySimp_rightDist" (formula "4") (term "1")) (rule "mul_literals" (formula "4") (term "0,1")) (rule "polySimp_mulLiterals" (formula "4") (term "1,1")) (rule "polySimp_elimOne" (formula "4") (term "1,1")) (rule "inEqSimp_contradInEq1" (formula "6") (ifseqformula "4")) (rule "andLeft" (formula "6")) (rule "inEqSimp_homoInEq1" (formula "6")) (rule "polySimp_mulComm0" (formula "6") (term "1,0")) (rule "polySimp_rightDist" (formula "6") (term "1,0")) (rule "mul_literals" (formula "6") (term "0,1,0")) (rule "polySimp_addAssoc" (formula "6") (term "0")) (rule "polySimp_addComm1" (formula "6") (term "0,0")) (rule "add_literals" (formula "6") (term "0,0,0")) (rule "polySimp_pullOutFactor1b" (formula "6") (term "0")) (rule "add_literals" (formula "6") (term "1,1,0")) (rule "times_zero_1" (formula "6") (term "1,0")) (rule "add_zero_right" (formula "6") (term "0")) (rule "leq_literals" (formula "6")) (rule "closeFalse" (formula "6")) ) ) (branch "if x_7 false" (builtin "One Step Simplification" (formula "20")) (builtin "One Step Simplification" (formula "1")) (rule "notLeft" (formula "1")) (rule "inEqSimp_leqRight" (formula "17")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "1")) (rule "polySimp_mulLiterals" (formula "1") (term "1")) (rule "polySimp_elimOne" (formula "1") (term "1")) (rule "assignmentAdditionInt" (formula "20") (term "1")) (builtin "One Step Simplification" (formula "20")) (rule "translateJavaAddInt" (formula "20") (term "0,1,0")) (rule "polySimp_addComm0" (formula "20") (term "0,1,0")) (rule "tryEmpty" (formula "20") (term "1")) (rule "methodCallEmpty" (formula "20") (term "1")) (rule "emptyModality" (formula "20") (term "1")) (builtin "One Step Simplification" (formula "20") (ifInst "" (formula "2")) (ifInst "" (formula "16")) (ifInst "" (formula "12"))) (rule "polySimp_mulComm0" (formula "20") (term "0,0,1")) (rule "polySimp_rightDist" (formula "20") (term "0,0,1")) (rule "mul_literals" (formula "20") (term "0,0,0,1")) (rule "precOfInt" (formula "20") (term "1")) (rule "inEqSimp_ltToLeq" (formula "20") (term "1,1")) (rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,1")) (rule "polySimp_mulAssoc" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_mulComm0" (formula "20") (term "0,0,1,0,0,1,1")) (rule "polySimp_mulLiterals" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_elimOne" (formula "20") (term "0,1,0,0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,1,1")) (rule "polySimp_addComm1" (formula "20") (term "0,0,1,1")) (rule "polySimp_pullOutFactor2b" (formula "20") (term "0,1,1")) (rule "add_literals" (formula "20") (term "1,1,0,1,1")) (rule "times_zero_1" (formula "20") (term "1,0,1,1")) (rule "add_zero_right" (formula "20") (term "0,1,1")) (rule "polySimp_addAssoc" (formula "20") (term "0,1,1")) (rule "polySimp_addComm1" (formula "20") (term "0,0,1,1")) (rule "add_literals" (formula "20") (term "0,0,0,1,1")) (rule "add_zero_left" (formula "20") (term "0,0,1,1")) (rule "polySimp_pullOutFactor1" (formula "20") (term "0,1,1")) (rule "add_literals" (formula "20") (term "1,0,1,1")) (rule "times_zero_1" (formula "20") (term "0,1,1")) (rule "leq_literals" (formula "20") (term "1,1")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_commuteGeq" (formula "20") (term "0,0,0")) (rule "inEqSimp_commuteGeq" (formula "20") (term "1,0,0")) (rule "replace_known_left" (formula "20") (term "1,0,0") (ifseqformula "15")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_homoInEq0" (formula "20") (term "1")) (rule "mul_literals" (formula "20") (term "1,0,1")) (rule "add_zero_right" (formula "20") (term "0,1")) (rule "inEqSimp_sepPosMonomial1" (formula "20") (term "1")) (rule "polySimp_mulComm0" (formula "20") (term "1,1")) (rule "polySimp_rightDist" (formula "20") (term "1,1")) (rule "mul_literals" (formula "20") (term "0,1,1")) (rule "polySimp_mulLiterals" (formula "20") (term "1,1,1")) (rule "polySimp_elimOne" (formula "20") (term "1,1,1")) (rule "replace_known_left" (formula "20") (term "1") (ifseqformula "2")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_subsumption0" (formula "20") (term "0") (ifseqformula "14")) (rule "inEqSimp_homoInEq0" (formula "20") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "20") (term "0,0,0")) (rule "add_literals" (formula "20") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "20") (term "1,0,0,0")) (rule "add_literals" (formula "20") (term "0,0,0")) (rule "qeq_literals" (formula "20") (term "0,0")) (builtin "One Step Simplification" (formula "20")) (rule "allRight" (formula "20") (inst "sk=x_0")) (rule "orRight" (formula "20")) (rule "orRight" (formula "20")) (rule "inEqSimp_leqRight" (formula "22")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "inEqSimp_leqRight" (formula "21")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_geqRight" (formula "22")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "3")) (rule "polySimp_mulComm0" (formula "3") (term "1")) (rule "polySimp_rightDist" (formula "3") (term "1")) (rule "polySimp_mulLiterals" (formula "3") (term "1,1")) (rule "mul_literals" (formula "3") (term "0,1")) (rule "polySimp_elimOne" (formula "3") (term "1,1")) (rule "inEqSimp_sepPosMonomial1" (formula "2")) (rule "polySimp_mulLiterals" (formula "2") (term "1")) (rule "polySimp_elimOne" (formula "2") (term "1")) (rule "inEqSimp_sepPosMonomial0" (formula "1")) (rule "polySimp_mulLiterals" (formula "1") (term "1")) (rule "polySimp_elimOne" (formula "1") (term "1")) (rule "inEqSimp_exactShadow3" (formula "2") (ifseqformula "1")) (rule "polySimp_mulComm0" (formula "2") (term "0,0")) (rule "polySimp_addComm0" (formula "2") (term "0")) (rule "inEqSimp_sepNegMonomial1" (formula "2")) (rule "polySimp_mulLiterals" (formula "2") (term "0")) (rule "polySimp_elimOne" (formula "2") (term "0")) (rule "allLeft" (formula "20") (inst "t=x_0")) (rule "inEqSimp_contradInEq1" (formula "20") (term "1,0") (ifseqformula "2")) (rule "inEqSimp_homoInEq1" (formula "20") (term "0,1,0")) (rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0")) (rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,0")) (rule "mul_literals" (formula "20") (term "0,1,0,0,1,0")) (rule "polySimp_addAssoc" (formula "20") (term "0,0,1,0")) (rule "polySimp_addComm0" (formula "20") (term "0,0,0,1,0")) (rule "polySimp_pullOutFactor1b" (formula "20") (term "0,0,1,0")) (rule "add_literals" (formula "20") (term "1,1,0,0,1,0")) (rule "times_zero_1" (formula "20") (term "1,0,0,1,0")) (rule "add_zero_right" (formula "20") (term "0,0,1,0")) (rule "leq_literals" (formula "20") (term "0,1,0")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_contradInEq1" (formula "20") (term "1") (ifseqformula "3")) (rule "inEqSimp_homoInEq1" (formula "20") (term "0,1")) (rule "polySimp_pullOutFactor1b" (formula "20") (term "0,0,1")) (rule "add_literals" (formula "20") (term "1,1,0,0,1")) (rule "times_zero_1" (formula "20") (term "1,0,0,1")) (rule "add_zero_right" (formula "20") (term "0,0,1")) (rule "leq_literals" (formula "20") (term "0,1")) (builtin "One Step Simplification" (formula "20")) (rule "inEqSimp_antiSymm" (formula "20") (ifseqformula "1")) (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "20")) (rule "inEqSimp_homoInEq0" (formula "1")) (rule "polySimp_pullOutFactor1" (formula "1") (term "0")) (rule "add_literals" (formula "1") (term "1,0")) (rule "times_zero_1" (formula "1") (term "0")) (rule "qeq_literals" (formula "1")) (rule "true_left" (formula "1")) (rule "applyEq" (formula "20") (term "0") (ifseqformula "19")) (rule "inEqSimp_homoInEq1" (formula "20")) (rule "polySimp_pullOutFactor1" (formula "20") (term "0")) (rule "add_literals" (formula "20") (term "1,0")) (rule "times_zero_1" (formula "20") (term "0")) (rule "leq_literals" (formula "20")) (rule "true_left" (formula "20")) (rule "applyEq" (formula "2") (term "0,2,0") (ifseqformula "19")) (rule "inEqSimp_homoInEq1" (formula "2")) (rule "polySimp_addComm1" (formula "2") (term "0")) (rule "applyEqRigid" (formula "1") (term "0") (ifseqformula "19")) (rule "inEqSimp_commuteGeq" (formula "1")) (rule "inEqSimp_sepPosMonomial0" (formula "1")) (rule "polySimp_mulComm0" (formula "1") (term "1")) (rule "polySimp_rightDist" (formula "1") (term "1")) (rule "mul_literals" (formula "1") (term "0,1")) (rule "polySimp_mulLiterals" (formula "1") (term "1,1")) (rule "polySimp_elimOne" (formula "1") (term "1,1")) (rule "inEqSimp_contradInEq0" (formula "2") (ifseqformula "1")) (rule "andLeft" (formula "2")) (rule "inEqSimp_homoInEq1" (formula "2")) (rule "polySimp_mulComm0" (formula "2") (term "1,0")) (rule "polySimp_rightDist" (formula "2") (term "1,0")) (rule "mul_literals" (formula "2") (term "0,1,0")) (rule "polySimp_addAssoc" (formula "2") (term "0")) (rule "polySimp_addComm0" (formula "2") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "2") (term "0")) (rule "add_literals" (formula "2") (term "1,1,0")) (rule "times_zero_1" (formula "2") (term "1,0")) (rule "add_zero_right" (formula "2") (term "0")) (rule "leq_literals" (formula "2")) (rule "closeFalse" (formula "2")) ) ) (branch "Null Reference (x_arr_4 = null)" (rule "false_right" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "closeFalse" (formula "1")) ) (branch "Index Out of Bounds (x_arr_4 != null, but idx Out of Bounds!)" (rule "false_right" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) (rule "times_zero_1" (formula "1") (term "1,0,0,1")) (rule "add_zero_right" (formula "1") (term "0,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) (rule "mul_literals" (formula "1") (term "1,1")) (rule "inEqSimp_contradInEq1" (formula "1") (term "0") (ifseqformula "15")) (rule "inEqSimp_homoInEq1" (formula "1") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,0")) (rule "add_literals" (formula "1") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "1") (term "1,0,0,0")) (rule "add_zero_right" (formula "1") (term "0,0,0")) (rule "leq_literals" (formula "1") (term "0,0")) (builtin "One Step Simplification" (formula "1")) (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "8")) (rule "qeq_literals" (formula "1") (term "0")) (builtin "One Step Simplification" (formula "1")) (rule "closeFalse" (formula "1")) ) ) (branch "Null Reference (x_arr_3 = null)" (builtin "One Step Simplification" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "closeFalse" (formula "1")) ) (branch "Index Out of Bounds (x_arr_3 != null, but counter Out of Bounds!)" (rule "false_right" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "inEqSimp_ltToLeq" (formula "1") (term "1")) (rule "times_zero_1" (formula "1") (term "1,0,0,1")) (rule "add_zero_right" (formula "1") (term "0,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "1") (term "1")) (rule "mul_literals" (formula "1") (term "1,1")) (rule "inEqSimp_contradInEq1" (formula "1") (term "0") (ifseqformula "2")) (rule "inEqSimp_homoInEq1" (formula "1") (term "0,0")) (rule "polySimp_pullOutFactor1b" (formula "1") (term "0,0,0")) (rule "add_literals" (formula "1") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "1") (term "1,0,0,0")) (rule "add_zero_right" (formula "1") (term "0,0,0")) (rule "leq_literals" (formula "1") (term "0,0")) (builtin "One Step Simplification" (formula "1")) (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "9")) (rule "qeq_literals" (formula "1") (term "0")) (builtin "One Step Simplification" (formula "1")) (rule "closeFalse" (formula "1")) ) ) (branch "if x_4 false" (builtin "One Step Simplification" (formula "19")) (builtin "One Step Simplification" (formula "1")) (rule "closeFalse" (formula "1")) ) ) (branch "Null Reference (x_arr_2 = null)" (builtin "One Step Simplification" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "closeFalse" (formula "1")) ) ) (branch "Null Reference (x_arr_1 = null)" (rule "false_right" (formula "17")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "closeFalse" (formula "1")) ) ) (branch "Use Case" (builtin "One Step Simplification" (formula "9")) (builtin "One Step Simplification" (formula "12")) (rule "andLeft" (formula "9")) (rule "andLeft" (formula "9")) (rule "andLeft" (formula "9")) (rule "andLeft" (formula "9")) (rule "andLeft" (formula "9")) (rule "inEqSimp_ltToLeq" (formula "14") (term "1,0,0")) (rule "polySimp_mulComm0" (formula "14") (term "1,0,0,1,0,0")) (rule "inEqSimp_ltToLeq" (formula "13")) (rule "polySimp_mulComm0" (formula "13") (term "1,0,0")) (rule "polySimp_addComm1" (formula "13") (term "0")) (rule "inEqSimp_ltToLeq" (formula "12")) (rule "polySimp_mulComm0" (formula "12") (term "1,0,0")) (rule "polySimp_addComm1" (formula "12") (term "0")) (rule "inEqSimp_commuteGeq" (formula "14") (term "1,0")) (rule "inEqSimp_commuteLeq" (formula "10")) (rule "variableDeclarationAssign" (formula "17") (term "1")) (rule "variableDeclaration" (formula "17") (term "1") (newnames "b_1")) (rule "inEqSimp_sepPosMonomial0" (formula "14") (term "1,0,0")) (rule "polySimp_mulComm0" (formula "14") (term "1,1,0,0")) (rule "polySimp_rightDist" (formula "14") (term "1,1,0,0")) (rule "polySimp_mulLiterals" (formula "14") (term "1,1,1,0,0")) (rule "mul_literals" (formula "14") (term "0,1,1,0,0")) (rule "polySimp_elimOne" (formula "14") (term "1,1,1,0,0")) (rule "inEqSimp_sepNegMonomial0" (formula "13")) (rule "polySimp_mulLiterals" (formula "13") (term "0")) (rule "polySimp_elimOne" (formula "13") (term "0")) (rule "inEqSimp_sepNegMonomial0" (formula "12")) (rule "polySimp_mulLiterals" (formula "12") (term "0")) (rule "polySimp_elimOne" (formula "12") (term "0")) (rule "inEqSimp_exactShadow3" (formula "6") (ifseqformula "9")) (rule "times_zero_1" (formula "6") (term "0,0")) (rule "add_zero_left" (formula "6") (term "0")) (rule "inEqSimp_exactShadow3" (formula "7") (ifseqformula "12")) (rule "times_zero_1" (formula "7") (term "0,0")) (rule "add_zero_left" (formula "7") (term "0")) (rule "nnf_imp2or" (formula "15") (term "0")) (rule "nnf_notAnd" (formula "15") (term "0,0")) (rule "inEqSimp_notLeq" (formula "15") (term "1,0,0")) (rule "polySimp_rightDist" (formula "15") (term "1,0,0,1,0,0")) (rule "mul_literals" (formula "15") (term "0,1,0,0,1,0,0")) (rule "polySimp_addAssoc" (formula "15") (term "0,0,1,0,0")) (rule "add_literals" (formula "15") (term "0,0,0,1,0,0")) (rule "add_zero_left" (formula "15") (term "0,0,1,0,0")) (rule "inEqSimp_sepPosMonomial1" (formula "15") (term "1,0,0")) (rule "polySimp_mulLiterals" (formula "15") (term "1,1,0,0")) (rule "polySimp_elimOne" (formula "15") (term "1,1,0,0")) (rule "inEqSimp_notGeq" (formula "15") (term "0,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,0,0,0,0,0")) (rule "inEqSimp_sepPosMonomial0" (formula "15") (term "0,0,0")) (rule "polySimp_mulComm0" (formula "15") (term "1,0,0,0")) (rule "polySimp_rightDist" (formula "15") (term "1,0,0,0")) (rule "polySimp_mulLiterals" (formula "15") (term "1,1,0,0,0")) (rule "mul_literals" (formula "15") (term "0,1,0,0,0")) (rule "polySimp_elimOne" (formula "15") (term "1,1,0,0,0")) (rule "commute_or" (formula "15") (term "0,0")) (rule "compound_less_than_comparison_2" (formula "18") (term "1") (inst "#v1=x_1") (inst "#v0=x")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x")) (rule "assignment" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_1")) (rule "eval_order_array_access6" (formula "18") (term "1") (inst "#v0=x_arr")) (rule "variableDeclarationAssign" (formula "18") (term "1")) (rule "variableDeclaration" (formula "18") (term "1") (newnames "x_arr")) (rule "assignment_read_attribute_this" (formula "18")) (builtin "One Step Simplification" (formula "18")) (rule "assignment_read_length" (formula "18")) (branch "Normal Execution (x_arr != null)" (builtin "One Step Simplification" (formula "18")) (rule "less_than_comparison_simple" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "inEqSimp_ltToLeq" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0,1,0")) (rule "polySimp_addComm1" (formula "18") (term "0,0,0,1,0")) (rule "inEqSimp_sepNegMonomial0" (formula "18") (term "0,0,1,0")) (rule "polySimp_mulLiterals" (formula "18") (term "0,0,0,1,0")) (rule "polySimp_elimOne" (formula "18") (term "0,0,0,1,0")) (rule "methodCallEmpty" (formula "18") (term "1")) (rule "emptyModality" (formula "18") (term "1")) (builtin "One Step Simplification" (formula "18")) (rule "impRight" (formula "18")) (rule "notLeft" (formula "1")) (rule "inEqSimp_geqRight" (formula "16")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "inEqSimp_sepPosMonomial0" (formula "1")) (rule "polySimp_mulLiterals" (formula "1") (term "1")) (rule "polySimp_elimOne" (formula "1") (term "1")) (rule "inEqSimp_antiSymm" (formula "13") (ifseqformula "1")) (rule "applyEq" (formula "1") (term "0") (ifseqformula "13")) (rule "inEqSimp_homoInEq0" (formula "1")) (rule "polySimp_pullOutFactor1" (formula "1") (term "0")) (rule "add_literals" (formula "1") (term "1,0")) (rule "times_zero_1" (formula "1") (term "0")) (rule "qeq_literals" (formula "1")) (rule "true_left" (formula "1")) (rule "applyEq" (formula "13") (term "0") (ifseqformula "12")) (rule "inEqSimp_homoInEq1" (formula "13")) (rule "polySimp_pullOutFactor1" (formula "13") (term "0")) (rule "add_literals" (formula "13") (term "1,0")) (rule "times_zero_1" (formula "13") (term "0")) (rule "leq_literals" (formula "13")) (rule "true_left" (formula "13")) (rule "applyEq" (formula "5") (term "0") (ifseqformula "12")) (rule "applyEq" (formula "14") (term "0") (ifseqformula "12")) (rule "inEqSimp_homoInEq1" (formula "14")) (rule "polySimp_addComm1" (formula "14") (term "0")) (rule "applyEq" (formula "9") (term "0") (ifseqformula "12")) (rule "inEqSimp_homoInEq1" (formula "9")) (rule "polySimp_addComm1" (formula "9") (term "0")) (rule "inEqSimp_sepPosMonomial0" (formula "14")) (rule "polySimp_mulComm0" (formula "14") (term "1")) (rule "polySimp_rightDist" (formula "14") (term "1")) (rule "mul_literals" (formula "14") (term "0,1")) (rule "polySimp_mulLiterals" (formula "14") (term "1,1")) (rule "polySimp_elimOne" (formula "14") (term "1,1")) (rule "inEqSimp_sepPosMonomial0" (formula "9")) (rule "polySimp_mulComm0" (formula "9") (term "1")) (rule "polySimp_rightDist" (formula "9") (term "1")) (rule "mul_literals" (formula "9") (term "0,1")) (rule "polySimp_mulLiterals" (formula "9") (term "1,1")) (rule "polySimp_elimOne" (formula "9") (term "1,1")) (rule "inEqSimp_subsumption1" (formula "6") (ifseqformula "5")) (rule "leq_literals" (formula "6") (term "0")) (builtin "One Step Simplification" (formula "6")) (rule "true_left" (formula "6")) (rule "inEqSimp_subsumption0" (formula "10") (ifseqformula "8")) (rule "inEqSimp_homoInEq0" (formula "10") (term "0")) (rule "polySimp_mulComm0" (formula "10") (term "1,0,0")) (rule "polySimp_rightDist" (formula "10") (term "1,0,0")) (rule "mul_literals" (formula "10") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "10") (term "0,0")) (rule "polySimp_addComm0" (formula "10") (term "0,0,0")) (rule "polySimp_pullOutFactor1b" (formula "10") (term "0,0")) (rule "add_literals" (formula "10") (term "1,1,0,0")) (rule "times_zero_1" (formula "10") (term "1,0,0")) (rule "add_literals" (formula "10") (term "0,0")) (rule "qeq_literals" (formula "10") (term "0")) (builtin "One Step Simplification" (formula "10")) (rule "true_left" (formula "10")) (rule "inEqSimp_exactShadow3" (formula "6") (ifseqformula "12")) (rule "times_zero_1" (formula "6") (term "0,0")) (rule "add_zero_left" (formula "6") (term "0")) (rule "inEqSimp_sepPosMonomial1" (formula "6")) (rule "mul_literals" (formula "6") (term "1")) (rule "inEqSimp_exactShadow3" (formula "7") (ifseqformula "8")) (rule "times_zero_1" (formula "7") (term "0,0")) (rule "add_zero_left" (formula "7") (term "0")) (rule "inEqSimp_sepPosMonomial1" (formula "7")) (rule "mul_literals" (formula "7") (term "1")) (rule "methodCallReturn" (formula "16") (term "1")) (rule "assignment" (formula "16") (term "1")) (builtin "One Step Simplification" (formula "16")) (rule "methodCallEmpty" (formula "16") (term "1")) (rule "tryEmpty" (formula "16") (term "1")) (rule "emptyModality" (formula "16") (term "1")) (builtin "One Step Simplification" (formula "16") (ifInst "" (formula "11"))) (rule "applyEq" (formula "16") (term "1,1,0,0,0") (ifseqformula "10")) (rule "applyEq" (formula "16") (term "0,0,1") (ifseqformula "10")) (rule "inEqSimp_homoInEq1" (formula "16") (term "0,1")) (rule "polySimp_addComm1" (formula "16") (term "0,0,1")) (rule "inEqSimp_sepPosMonomial0" (formula "16") (term "0,1")) (rule "polySimp_mulComm0" (formula "16") (term "1,0,1")) (rule "polySimp_rightDist" (formula "16") (term "1,0,1")) (rule "polySimp_mulLiterals" (formula "16") (term "1,1,0,1")) (rule "mul_literals" (formula "16") (term "0,1,0,1")) (rule "polySimp_elimOne" (formula "16") (term "1,1,0,1")) (rule "replace_known_left" (formula "16") (term "0,1") (ifseqformula "12")) (builtin "One Step Simplification" (formula "16")) (rule "Class_invariant_axiom_for_Sort" (formula "16") (term "1") (inst "sk=sk_1") (ifseqformula "3")) (branch "Use Axiom" (rule "replace_known_right" (formula "16") (term "0,1") (ifseqformula "14")) (builtin "One Step Simplification" (formula "16")) (rule "allRight" (formula "16") (inst "sk=i_0")) (rule "orRight" (formula "16")) (rule "orRight" (formula "16")) (rule "inEqSimp_leqRight" (formula "18")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "polySimp_addComm1" (formula "1") (term "0")) (rule "inEqSimp_geqRight" (formula "18")) (rule "polySimp_mulComm0" (formula "1") (term "1,0,0")) (rule "inEqSimp_leqRight" (formula "18")) (rule "polySimp_rightDist" (formula "1") (term "1,0,0")) (rule "mul_literals" (formula "1") (term "0,1,0,0")) (rule "polySimp_addAssoc" (formula "1") (term "0,0")) (rule "add_literals" (formula "1") (term "0,0,0")) (rule "add_zero_left" (formula "1") (term "0,0")) (rule "polySimp_addComm0" (formula "1") (term "0")) (rule "inEqSimp_sepNegMonomial1" (formula "3")) (rule "polySimp_mulLiterals" (formula "3") (term "0")) (rule "polySimp_elimOne" (formula "3") (term "0")) (rule "inEqSimp_sepPosMonomial0" (formula "2")) (rule "polySimp_mulComm0" (formula "2") (term "1")) (rule "polySimp_rightDist" (formula "2") (term "1")) (rule "mul_literals" (formula "2") (term "0,1")) (rule "polySimp_mulLiterals" (formula "2") (term "1,1")) (rule "polySimp_elimOne" (formula "2") (term "1,1")) (rule "inEqSimp_sepNegMonomial1" (formula "1")) (rule "polySimp_mulLiterals" (formula "1") (term "0")) (rule "polySimp_elimOne" (formula "1") (term "0")) (rule "inEqSimp_exactShadow3" (formula "10") (ifseqformula "1")) (rule "times_zero_1" (formula "10") (term "0,0")) (rule "add_zero_left" (formula "10") (term "0")) (rule "inEqSimp_exactShadow3" (formula "10") (ifseqformula "2")) (rule "times_zero_1" (formula "10") (term "0,0")) (rule "add_zero_left" (formula "10") (term "0")) (rule "inEqSimp_sepPosMonomial1" (formula "10")) (rule "mul_literals" (formula "10") (term "1")) (rule "allLeft" (formula "17") (inst "t=i_0")) (rule "inEqSimp_commuteLeq" (formula "17") (term "1")) (rule "inEqSimp_homoInEq0" (formula "17") (term "1,0")) (rule "polySimp_addComm1" (formula "17") (term "0,1,0")) (rule "inEqSimp_sepPosMonomial1" (formula "17") (term "1,0")) (rule "polySimp_mulComm0" (formula "17") (term "1,1,0")) (rule "polySimp_rightDist" (formula "17") (term "1,1,0")) (rule "mul_literals" (formula "17") (term "0,1,1,0")) (rule "polySimp_mulLiterals" (formula "17") (term "1,1,1,0")) (rule "polySimp_elimOne" (formula "17") (term "1,1,1,0")) (rule "inEqSimp_contradInEq0" (formula "17") (term "1") (ifseqformula "3")) (rule "inEqSimp_homoInEq1" (formula "17") (term "0,1")) (rule "polySimp_mulComm0" (formula "17") (term "1,0,0,1")) (rule "polySimp_rightDist" (formula "17") (term "1,0,0,1")) (rule "mul_literals" (formula "17") (term "0,1,0,0,1")) (rule "polySimp_addAssoc" (formula "17") (term "0,0,1")) (rule "polySimp_addComm0" (formula "17") (term "0,0,0,1")) (rule "polySimp_pullOutFactor1b" (formula "17") (term "0,0,1")) (rule "add_literals" (formula "17") (term "1,1,0,0,1")) (rule "times_zero_1" (formula "17") (term "1,0,0,1")) (rule "add_zero_right" (formula "17") (term "0,0,1")) (rule "leq_literals" (formula "17") (term "0,1")) (builtin "One Step Simplification" (formula "17")) (rule "inEqSimp_contradInEq0" (formula "17") (term "0") (ifseqformula "2")) (rule "inEqSimp_homoInEq1" (formula "17") (term "0,0")) (rule "polySimp_mulComm0" (formula "17") (term "1,0,0,0")) (rule "polySimp_rightDist" (formula "17") (term "1,0,0,0")) (rule "mul_literals" (formula "17") (term "0,1,0,0,0")) (rule "polySimp_addAssoc" (formula "17") (term "0,0,0")) (rule "polySimp_addComm0" (formula "17") (term "0,0,0,0")) (rule "polySimp_pullOutFactor1b" (formula "17") (term "0,0,0")) (rule "add_literals" (formula "17") (term "1,1,0,0,0")) (rule "times_zero_1" (formula "17") (term "1,0,0,0")) (rule "add_zero_right" (formula "17") (term "0,0,0")) (rule "leq_literals" (formula "17") (term "0,0")) (builtin "One Step Simplification" (formula "17")) (rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "17")) (rule "andLeft" (formula "1")) (rule "inEqSimp_homoInEq1" (formula "1")) (rule "polySimp_pullOutFactor1b" (formula "1") (term "0")) (rule "add_literals" (formula "1") (term "1,1,0")) (rule "times_zero_1" (formula "1") (term "1,0")) (rule "add_zero_right" (formula "1") (term "0")) (rule "leq_literals" (formula "1")) (rule "closeFalse" (formula "1")) ) (branch "Show Axiom Satisfiability" (builtin "One Step Simplification" (formula "16") (ifInst "" (formula "14")) (ifInst "" (formula "14"))) (rule "closeTrue" (formula "16")) ) ) (branch "Null Reference (x_arr = null)" (builtin "One Step Simplification" (formula "19")) (builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17"))) (rule "closeFalse" (formula "1")) ) ) ) (branch "Show Axiom Satisfiability" (builtin "One Step Simplification" (formula "9")) (rule "closeTrue" (formula "9")) ) ) }