\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Thu Nov 07 16:36:35 CET 2019
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[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_SCOPE_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_COMPLETION
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[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\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\: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
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
"
}
\javaSource "..";
\proofObligation "#Proof Obligation Settings
#Thu Nov 07 16:36:35 CET 2019
name=MarbleRPS[MarbleRPS\\:\\:evaluate(int,int)].JML operation contract.0
contract=MarbleRPS[MarbleRPS\\:\\:evaluate(int,int)].JML operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
\proof {
(keyLog "0" (keyUser "jonas" ) (keyVersion "2d2a68348e607ba00900a9ecfaee13afec14c614"))
(autoModeTime "950")
(branch "dummy ID"
(builtin "One Step Simplification" (formula "1") (newnames "s1,s2,result,exc,heapAtPre,o,f"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "3"))
(rule "andLeft" (formula "4"))
(rule "andLeft" (formula "3"))
(rule "eqSymm" (formula "7") (term "0,0,1,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "5"))
(rule "inEqSimp_commuteLeq" (formula "3"))
(rule "assignment" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_evaluate,savedHeapBefore_evaluate"))
(builtin "One Step Simplification" (formula "7"))
(rule "returnUnfold" (formula "7") (term "1") (inst "#v0=x"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "x"))
(rule "compound_modulo_1" (formula "7") (term "1") (inst "#v=x_1"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "x_1"))
(rule "remove_parentheses_right" (formula "7") (term "1"))
(rule "compound_subtraction_1" (formula "7") (term "1") (inst "#v=x_2"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "x_2"))
(rule "assignmentAdditionInt" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaAddInt" (formula "7") (term "0,1,0"))
(rule "assignmentSubtractionInt" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaSubInt" (formula "7") (term "0,1,0"))
(rule "polySimp_elimSub" (formula "7") (term "0,1,0"))
(rule "assignmentModulo" (formula "7"))
(branch "Case 1"
(builtin "One Step Simplification" (formula "7"))
(rule "translateJavaMod" (formula "7") (term "0,1,0"))
(rule "methodCallReturn" (formula "7") (term "1"))
(rule "assignment" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "methodCallEmpty" (formula "7") (term "1"))
(rule "tryEmpty" (formula "7") (term "1"))
(rule "emptyModality" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "jmod_axiom" (formula "7") (term "0,1,1,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,1,1"))
(rule "polySimp_homoEq" (formula "7") (term "1,1,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,1,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,1,1,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,0,1,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,1,0,1,1,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0,1,1,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,0,1,0,1,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,0,1,0,1,1,1"))
(rule "mul_literals" (formula "7") (term "0,0,0,1,0,1,1,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1,1,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,1,1,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,0,1,1,1"))
(rule "add_literals" (formula "7") (term "0,0,0,0,1,1,1"))
(rule "jmod_axiom" (formula "7") (term "0,1,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0"))
(rule "jmod_axiom" (formula "7") (term "0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0,1"))
(rule "polySimp_homoEq" (formula "7") (term "1,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,0,1,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,0,1,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,1,0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,0,1,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,0,1,0,1,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,0,1,0,1,0,1"))
(rule "mul_literals" (formula "7") (term "0,0,0,1,0,1,0,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1,0,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,1,0,1"))
(rule "polySimp_addAssoc" (formula "7") (term "0,0,0,1,0,1"))
(rule "add_literals" (formula "7") (term "0,0,0,0,1,0,1"))
(rule "polySimp_sepPosMonomial" (formula "7") (term "1,1,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,1,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,1,1,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,1,1,1,1"))
(rule "mul_literals" (formula "7") (term "0,0,1,1,1,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,1,1,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,0,1,1,1,1"))
(rule "polySimp_sepNegMonomial" (formula "7") (term "1,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0"))
(rule "polySimp_sepPosMonomial" (formula "7") (term "1,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,1,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,1,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "0,1,1,0,1"))
(rule "mul_literals" (formula "7") (term "0,0,1,1,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0,1,1,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,0,1,1,0,1"))
(rule "commute_and" (formula "7") (term "1,0,1,1"))
(rule "commute_and" (formula "7") (term "0,0,0,1,1"))
(rule "commute_and" (formula "7") (term "1,0,0,1,1"))
(rule "cnf_rightDist" (formula "7") (term "0,0,0,1"))
(rule "commute_or" (formula "7") (term "0,0,0,0,1"))
(rule "andRight" (formula "7"))
(branch "Case 1"
(rule "impRight" (formula "7"))
(rule "applyEq" (formula "7") (term "0") (ifseqformula "1"))
(rule "applyEq" (formula "6") (term "0") (ifseqformula "1"))
(rule "applyEq" (formula "6") (term "0,1,0,0,0") (ifseqformula "1"))
(rule "polySimp_homoEq" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "1,0"))
(rule "polySimp_pullOutFactor1b" (formula "6") (term "0,0,1,0"))
(rule "add_literals" (formula "6") (term "1,1,0,0,1,0"))
(rule "times_zero_1" (formula "6") (term "1,0,0,1,0"))
(rule "add_zero_right" (formula "6") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "6") (term "0,1,0"))
(rule "qeq_literals" (formula "6") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "6"))
(rule "div_literals" (formula "6") (term "0,1,0"))
(rule "mul_literals" (formula "6") (term "1,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "polySimp_addComm1" (formula "6") (term "0,0"))
(rule "add_literals" (formula "6") (term "0,0,0"))
(rule "add_zero_left" (formula "6") (term "0,0"))
(rule "applyEq" (formula "6") (term "0,1,0") (ifseqformula "1"))
(rule "polySimp_pullOutFactor1" (formula "6") (term "0"))
(rule "add_literals" (formula "6") (term "1,0"))
(rule "times_zero_1" (formula "6") (term "0"))
(builtin "One Step Simplification" (formula "6"))
(rule "closeTrue" (formula "6"))
)
(branch "Case 2"
(rule "andRight" (formula "7"))
(branch "Case 1"
(rule "impRight" (formula "7"))
(rule "cnf_rightDist" (formula "1") (term "1,0"))
(rule "commute_or" (formula "1") (term "1,1,0"))
(rule "commute_or" (formula "1") (term "0,1,0"))
(rule "cnf_rightDist" (formula "1") (term "0,0"))
(rule "commute_or" (formula "1") (term "0,0,0"))
(rule "commute_or" (formula "1") (term "1,0,0"))
(rule "orLeft" (formula "1"))
(branch " (s1 = 0 | s1 = 2) & (s1 = 2 | s2 = 2) & ((s1 = 0 | s2 = 1) & (s2 = 1 | s2 = 2))"
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "2"))
(rule "andLeft" (formula "1"))
(rule "jdiv_axiom" (formula "11") (term "0,0"))
(rule "eqSymm" (formula "1"))
(rule "polySimp_mulComm0" (formula "1") (term "0,0,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "0,0,2,0"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,0"))
(rule "polySimp_elimOne" (formula "1") (term "1,0,0,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "0,0,0,2,0"))
(rule "mul_literals" (formula "1") (term "0,0,0,0,2,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "1") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "1") (term "0,0,0"))
(rule "polySimp_elimOne" (formula "1") (term "0,0,0"))
(rule "polyDiv_pullOut" (formula "1") (term "0,2,0") (inst "polyDivCoeff=Z(neglit(1(#)))"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,0,2,0"))
(rule "equal_literals" (formula "1") (term "0,0,2,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,0,0,0,2,0"))
(rule "polySimp_mulComm0" (formula "1") (term "2,0"))
(rule "polySimp_addComm0" (formula "1") (term "1,2,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,1,1,2,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,0,1,1,2,0"))
(rule "add_literals" (formula "1") (term "0,0,0,1,1,2,0"))
(rule "add_zero_left" (formula "1") (term "0,0,1,1,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "2,0"))
(rule "mul_literals" (formula "1") (term "0,2,0"))
(rule "polyDiv_pullOut" (formula "1") (term "1,0") (inst "polyDivCoeff=Z(1(#))"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,1,0"))
(rule "equal_literals" (formula "1") (term "0,1,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,0,0,1,0"))
(rule "polySimp_addComm0" (formula "1") (term "1,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,1,1,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,0,1,1,0"))
(rule "add_literals" (formula "1") (term "0,0,0,1,1,0"))
(rule "add_zero_left" (formula "1") (term "0,0,1,1,0"))
(rule "div_axiom" (formula "1") (term "0,1,2,0") (inst "quotient=quotient_0"))
(rule "qeq_literals" (formula "1") (term "0,1,1"))
(builtin "One Step Simplification" (formula "1"))
(rule "equal_literals" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,1,1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "polySimp_addAssoc" (formula "3") (term "0,1"))
(rule "polySimp_addComm1" (formula "3") (term "1"))
(rule "polySimp_addComm1" (formula "3") (term "0,1"))
(rule "add_literals" (formula "3") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "1,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "polySimp_addComm0" (formula "2") (term "0,0"))
(rule "inEqSimp_homoInEq1" (formula "3"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0"))
(rule "polySimp_addComm1" (formula "3") (term "0"))
(rule "polySimp_addComm1" (formula "3") (term "0,0"))
(rule "applyEq" (formula "4") (term "0,1,2,0") (ifseqformula "1"))
(rule "inEqSimp_sepPosMonomial1" (formula "2"))
(rule "polySimp_mulComm0" (formula "2") (term "1"))
(rule "polySimp_rightDist" (formula "2") (term "1"))
(rule "polySimp_mulLiterals" (formula "2") (term "1,1"))
(rule "polySimp_elimOne" (formula "2") (term "1,1"))
(rule "polySimp_mulComm0" (formula "2") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "2") (term "0,1"))
(rule "inEqSimp_sepPosMonomial0" (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 "polySimp_elimOne" (formula "3") (term "1,1"))
(rule "polySimp_rightDist" (formula "3") (term "0,1"))
(rule "mul_literals" (formula "3") (term "0,0,1"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,1"))
(rule "inEqSimp_exactShadow3" (formula "13") (ifseqformula "3"))
(rule "times_zero_1" (formula "13") (term "0,0"))
(rule "add_zero_left" (formula "13") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "13"))
(rule "polySimp_mulComm0" (formula "13") (term "1"))
(rule "polySimp_rightDist" (formula "13") (term "1"))
(rule "mul_literals" (formula "13") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "13") (term "1,1"))
(rule "inEqSimp_exactShadow3" (formula "2") (ifseqformula "15"))
(rule "polySimp_rightDist" (formula "2") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "2") (term "0,0,0"))
(rule "polySimp_mulComm0" (formula "2") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "2") (term "0,0,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "polySimp_addComm0" (formula "2") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "0"))
(rule "polySimp_elimOne" (formula "2") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "12") (ifseqformula "2"))
(rule "times_zero_1" (formula "12") (term "0,0"))
(rule "add_zero_left" (formula "12") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "12"))
(rule "polySimp_mulLiterals" (formula "12") (term "0"))
(rule "elimGcdLeq_antec" (formula "12") (inst "elimGcdRightDiv=Z(0(#))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "12") (term "0,0"))
(builtin "One Step Simplification" (formula "12"))
(rule "neg_literal" (formula "12") (term "0,0,0,0,0,0"))
(rule "times_zero_1" (formula "12") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "12") (term "1,0,0"))
(rule "polySimp_addLiterals" (formula "12") (term "0,0,0,0"))
(rule "add_literals" (formula "12") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "12") (term "0,0"))
(rule "add_literals" (formula "12") (term "1,1,0,0"))
(rule "times_zero_1" (formula "12") (term "1,0,0"))
(rule "add_zero_right" (formula "12") (term "0,0"))
(rule "qeq_literals" (formula "12") (term "0"))
(builtin "One Step Simplification" (formula "12"))
(rule "inEqSimp_exactShadow3" (formula "15") (ifseqformula "14"))
(rule "polySimp_rightDist" (formula "15") (term "0,0"))
(rule "mul_literals" (formula "15") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "15") (term "0"))
(rule "add_literals" (formula "15") (term "0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "15"))
(rule "mul_literals" (formula "15") (term "1"))
(rule "elimGcdGeq_antec" (formula "15") (inst "elimGcdRightDiv=Z(neglit(1(#)))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "15") (term "0,0"))
(builtin "One Step Simplification" (formula "15"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0"))
(rule "mul_literals" (formula "15") (term "1,0,0,0,0,0"))
(rule "polySimp_addLiterals" (formula "15") (term "0,0,0,0"))
(rule "add_literals" (formula "15") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "15") (term "0,0"))
(rule "add_literals" (formula "15") (term "1,1,0,0"))
(rule "times_zero_1" (formula "15") (term "1,0,0"))
(rule "add_zero_right" (formula "15") (term "0,0"))
(rule "leq_literals" (formula "15") (term "0"))
(builtin "One Step Simplification" (formula "15"))
(rule "div_axiom" (formula "5") (term "1,1,0") (inst "quotient=quotient_1"))
(rule "mul_literals" (formula "5") (term "1,1,1,1,1"))
(rule "equal_literals" (formula "5") (term "0"))
(builtin "One Step Simplification" (formula "5"))
(rule "qeq_literals" (formula "5") (term "0,1"))
(builtin "One Step Simplification" (formula "5"))
(rule "andLeft" (formula "5"))
(rule "andLeft" (formula "5"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1"))
(rule "polySimp_addComm1" (formula "7") (term "1"))
(rule "polySimp_addComm1" (formula "7") (term "0,1"))
(rule "add_literals" (formula "7") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "1,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "polySimp_addComm0" (formula "6") (term "0,0"))
(rule "inEqSimp_homoInEq1" (formula "7"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "polySimp_addComm1" (formula "7") (term "0,0"))
(rule "applyEq" (formula "8") (term "1,1,0") (ifseqformula "5"))
(rule "inEqSimp_sepNegMonomial1" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "0"))
(rule "polySimp_elimOne" (formula "6") (term "0"))
(rule "inEqSimp_sepNegMonomial0" (formula "7"))
(rule "polySimp_mulLiterals" (formula "7") (term "0"))
(rule "polySimp_elimOne" (formula "7") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "20") (ifseqformula "6"))
(rule "times_zero_1" (formula "20") (term "0,0"))
(rule "add_zero_left" (formula "20") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "20"))
(rule "polySimp_mulLiterals" (formula "20") (term "1"))
(rule "inEqSimp_exactShadow3" (formula "3") (ifseqformula "6"))
(rule "polySimp_rightDist" (formula "3") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "3") (term "0,0,0"))
(rule "polySimp_mulComm0" (formula "3") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "0,0,0"))
(rule "polySimp_addAssoc" (formula "3") (term "0"))
(rule "polySimp_addComm1" (formula "3") (term "0,0"))
(rule "polySimp_pullOutFactor2b" (formula "3") (term "0"))
(rule "add_literals" (formula "3") (term "1,1,0"))
(rule "times_zero_1" (formula "3") (term "1,0"))
(rule "add_zero_right" (formula "3") (term "0"))
(rule "polySimp_addComm0" (formula "3") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "3"))
(rule "polySimp_mulLiterals" (formula "3") (term "0"))
(rule "elimGcdLeq_antec" (formula "3") (inst "elimGcdRightDiv=mul(quotient_1, Z(neglit(1(#))))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "neg_literal" (formula "3") (term "0,0,0,0,0,1,0"))
(rule "mul_literals" (formula "3") (term "0,1,0,0,0,0,1,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,1,0"))
(rule "leq_literals" (formula "3") (term "0,0"))
(builtin "One Step Simplification" (formula "3"))
(rule "polySimp_pullOutFactor0b" (formula "3") (term "0,0"))
(rule "add_literals" (formula "3") (term "1,1,0,0"))
(rule "times_zero_1" (formula "3") (term "1,0,0"))
(rule "add_zero_right" (formula "3") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "3") (term "1,0,0,0"))
(rule "polySimp_mulComm0" (formula "3") (term "0,1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "3") (term "0,0"))
(rule "add_literals" (formula "3") (term "1,1,0,0"))
(rule "times_zero_1" (formula "3") (term "1,0,0"))
(rule "add_zero_right" (formula "3") (term "0,0"))
(rule "qeq_literals" (formula "3") (term "0"))
(builtin "One Step Simplification" (formula "3"))
(rule "inEqSimp_exactShadow3" (formula "8") (ifseqformula "5"))
(rule "polySimp_rightDist" (formula "8") (term "0,0"))
(rule "polySimp_rightDist" (formula "8") (term "0,0,0"))
(rule "mul_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0"))
(rule "polySimp_pullOutFactor2b" (formula "8") (term "0"))
(rule "add_literals" (formula "8") (term "1,1,0"))
(rule "times_zero_1" (formula "8") (term "1,0"))
(rule "add_zero_right" (formula "8") (term "0"))
(rule "polySimp_addAssoc" (formula "8") (term "0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "8"))
(rule "polySimp_mulComm0" (formula "8") (term "1"))
(rule "polySimp_rightDist" (formula "8") (term "1"))
(rule "mul_literals" (formula "8") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,1"))
(rule "elimGcdGeq_antec" (formula "8") (inst "elimGcdRightDiv=add(Z(neglit(1(#))), mul(quotient_1, Z(neglit(1(#)))))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "mul_literals" (formula "8") (term "0,1,0,0,0,0,1,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0,1,0"))
(rule "leq_literals" (formula "8") (term "0,0"))
(builtin "One Step Simplification" (formula "8"))
(rule "polySimp_pullOutFactor0b" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "1,1,0,0"))
(rule "times_zero_1" (formula "8") (term "1,0,0"))
(rule "add_zero_right" (formula "8") (term "0,0"))
(rule "polySimp_rightDist" (formula "8") (term "1,0,0,0"))
(rule "mul_literals" (formula "8") (term "0,1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,1,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0,0,0"))
(rule "add_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0,0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0,0"))
(rule "add_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "1,1,0,0"))
(rule "times_zero_1" (formula "8") (term "1,0,0"))
(rule "add_zero_right" (formula "8") (term "0,0"))
(rule "leq_literals" (formula "8") (term "0"))
(builtin "One Step Simplification" (formula "8"))
(rule "inEqSimp_exactShadow3" (formula "9") (ifseqformula "24"))
(rule "polySimp_rightDist" (formula "9") (term "0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0"))
(rule "polySimp_rightDist" (formula "9") (term "0,0,0"))
(rule "mul_literals" (formula "9") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "9") (term "1,0,0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0,0"))
(rule "add_literals" (formula "9") (term "0,0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "9"))
(rule "polySimp_mulLiterals" (formula "9") (term "0"))
(rule "polySimp_elimOne" (formula "9") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "8") (ifseqformula "18"))
(rule "add_zero_right" (formula "8") (term "0"))
(rule "polySimp_rightDist" (formula "8") (term "0"))
(rule "mul_literals" (formula "8") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0"))
(rule "polySimp_elimOne" (formula "8") (term "1,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "8"))
(rule "mul_literals" (formula "8") (term "1"))
(rule "inEqSimp_exactShadow3" (formula "20") (ifseqformula "10"))
(rule "times_zero_1" (formula "20") (term "0,0"))
(rule "add_zero_left" (formula "20") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "20"))
(rule "mul_literals" (formula "20") (term "1"))
(rule "inEqSimp_subsumption6" (formula "20") (ifseqformula "8"))
(rule "greater_literals" (formula "20") (term "0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "mul_literals" (formula "20") (term "1,0"))
(rule "leq_literals" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "inEqSimp_exactShadow3" (formula "22") (ifseqformula "3"))
(rule "mul_literals" (formula "22") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "22"))
(rule "polySimp_mulLiterals" (formula "22") (term "0"))
(rule "polySimp_elimOne" (formula "22") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "25") (ifseqformula "2"))
(rule "polySimp_mulAssoc" (formula "25") (term "0,0"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "polySimp_addAssoc" (formula "25") (term "0"))
(rule "polySimp_addComm0" (formula "25") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "25"))
(rule "polySimp_mulLiterals" (formula "25") (term "0"))
(rule "inEqSimp_subsumption4" (formula "25") (ifseqformula "3"))
(rule "greater_literals" (formula "25") (term "0,0"))
(builtin "One Step Simplification" (formula "25"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "inEqSimp_homoInEq0" (formula "25") (term "0"))
(rule "polySimp_mulLiterals" (formula "25") (term "1,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "25") (term "0,0"))
(rule "add_literals" (formula "25") (term "1,1,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0"))
(rule "add_zero_right" (formula "25") (term "0,0"))
(rule "qeq_literals" (formula "25") (term "0"))
(builtin "One Step Simplification" (formula "25"))
(rule "true_left" (formula "25"))
(rule "inEqSimp_exactShadow3" (formula "24") (ifseqformula "10"))
(rule "polySimp_rightDist" (formula "24") (term "0,0"))
(rule "mul_literals" (formula "24") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "24") (term "0"))
(rule "polySimp_addAssoc" (formula "24") (term "0,0"))
(rule "add_literals" (formula "24") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "24"))
(rule "polySimp_mulComm0" (formula "24") (term "1"))
(rule "polySimp_rightDist" (formula "24") (term "1"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1"))
(rule "mul_literals" (formula "24") (term "0,1"))
(rule "inEqSimp_subsumption6" (formula "24") (ifseqformula "9"))
(rule "greater_literals" (formula "24") (term "0,0"))
(builtin "One Step Simplification" (formula "24"))
(rule "polySimp_rightDist" (formula "24") (term "1,0"))
(rule "mul_literals" (formula "24") (term "0,1,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1,0"))
(rule "inEqSimp_homoInEq0" (formula "24") (term "0"))
(rule "polySimp_mulComm0" (formula "24") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "24") (term "1,0,0"))
(rule "mul_literals" (formula "24") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1,0,0"))
(rule "polySimp_addAssoc" (formula "24") (term "0,0"))
(rule "polySimp_addComm1" (formula "24") (term "0,0,0"))
(rule "add_literals" (formula "24") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "24") (term "0,0"))
(rule "add_literals" (formula "24") (term "1,1,0,0"))
(rule "times_zero_1" (formula "24") (term "1,0,0"))
(rule "add_zero_right" (formula "24") (term "0,0"))
(rule "qeq_literals" (formula "24") (term "0"))
(builtin "One Step Simplification" (formula "24"))
(rule "true_left" (formula "24"))
(rule "inEqSimp_exactShadow3" (formula "25") (ifseqformula "21"))
(rule "polySimp_mulAssoc" (formula "25") (term "0,0"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "polySimp_addComm0" (formula "25") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "25"))
(rule "polySimp_mulLiterals" (formula "25") (term "0"))
(rule "elimGcdLeq_antec" (formula "25") (inst "elimGcdRightDiv=Z(0(#))") (inst "elimGcdLeftDiv=quotient_1") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "25") (term "0,0"))
(builtin "One Step Simplification" (formula "25"))
(rule "neg_literal" (formula "25") (term "0,0,0,0,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "1,0,0"))
(rule "polySimp_addLiterals" (formula "25") (term "0,0,0,0"))
(rule "add_literals" (formula "25") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "25") (term "0,0"))
(rule "add_literals" (formula "25") (term "1,1,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0"))
(rule "add_zero_right" (formula "25") (term "0,0"))
(rule "qeq_literals" (formula "25") (term "0"))
(builtin "One Step Simplification" (formula "25"))
(rule "inEqSimp_subsumption0" (formula "22") (ifseqformula "25"))
(rule "leq_literals" (formula "22") (term "0"))
(builtin "One Step Simplification" (formula "22"))
(rule "true_left" (formula "22"))
(rule "cut_direct" (formula "16") (term "0"))
(branch "CUT: s2 = 1 TRUE"
(builtin "One Step Simplification" (formula "17"))
(rule "true_left" (formula "17"))
(rule "replace_known_left" (formula "15") (term "1") (ifseqformula "16"))
(builtin "One Step Simplification" (formula "15"))
(rule "true_left" (formula "15"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "15"))
(rule "inEqSimp_homoInEq0" (formula "5"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "polySimp_addComm1" (formula "5") (term "0,0"))
(rule "add_literals" (formula "5") (term "0,0,0"))
(rule "applyEq" (formula "25") (term "0") (ifseqformula "15"))
(rule "qeq_literals" (formula "25"))
(rule "true_left" (formula "25"))
(rule "applyEq" (formula "4") (term "0") (ifseqformula "15"))
(rule "inEqSimp_homoInEq1" (formula "4"))
(rule "mul_literals" (formula "4") (term "1,0"))
(rule "polySimp_addComm1" (formula "4") (term "0"))
(rule "polySimp_addComm0" (formula "4") (term "0,0"))
(rule "applyEq" (formula "11") (term "0") (ifseqformula "15"))
(rule "inEqSimp_homoInEq1" (formula "11"))
(rule "mul_literals" (formula "11") (term "1,0"))
(rule "polySimp_addComm1" (formula "11") (term "0"))
(rule "polySimp_addComm1" (formula "11") (term "0,0"))
(rule "add_literals" (formula "11") (term "0,0,0"))
(rule "applyEq" (formula "7") (term "0") (ifseqformula "15"))
(rule "inEqSimp_homoInEq0" (formula "7"))
(rule "mul_literals" (formula "7") (term "1,0"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "polySimp_addComm0" (formula "7") (term "0,0"))
(rule "applyEq" (formula "1") (term "1,0,0") (ifseqformula "15"))
(rule "polySimp_addComm0" (formula "1") (term "0,0"))
(rule "applyEq" (formula "12") (term "0,0,0") (ifseqformula "15"))
(rule "inEqSimp_homoInEq0" (formula "12") (term "0,0"))
(rule "mul_literals" (formula "12") (term "1,0,0,0"))
(rule "polySimp_addComm1" (formula "12") (term "0,0,0"))
(rule "add_literals" (formula "12") (term "0,0,0,0"))
(rule "applyEq" (formula "25") (term "0") (ifseqformula "15"))
(rule "leq_literals" (formula "25"))
(rule "true_left" (formula "25"))
(rule "applyEq" (formula "14") (term "0,1") (ifseqformula "15"))
(rule "equal_literals" (formula "14") (term "1"))
(builtin "One Step Simplification" (formula "14"))
(rule "replace_known_left" (formula "13") (term "1") (ifseqformula "14"))
(builtin "One Step Simplification" (formula "13"))
(rule "true_left" (formula "13"))
(rule "applyEq" (formula "6") (term "0,1,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "6") (term "1,0,0"))
(rule "polySimp_addComm0" (formula "6") (term "0,0"))
(rule "applyEq" (formula "24") (term "0,1,0,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "24") (term "1,0,0,0"))
(rule "polySimp_homoEq" (formula "24"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,0"))
(rule "polySimp_addComm1" (formula "24") (term "0"))
(rule "polySimp_addComm1" (formula "24") (term "0,0,1,0,0"))
(rule "add_literals" (formula "24") (term "0,0,0,1,0,0"))
(rule "applyEq" (formula "12") (term "0,1,0,1") (ifseqformula "14"))
(rule "mul_literals" (formula "12") (term "1,0,1"))
(rule "polySimp_addComm1" (formula "12") (term "0,1"))
(rule "add_literals" (formula "12") (term "0,0,1"))
(rule "applyEq" (formula "5") (term "1,0") (ifseqformula "13"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "applyEq" (formula "1") (term "0,1,0,0") (ifseqformula "13"))
(rule "mul_literals" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "div_literals" (formula "1") (term "0"))
(rule "eqSymm" (formula "1"))
(rule "applyEq" (formula "23") (term "0") (ifseqformula "13"))
(rule "inEqSimp_commuteGeq" (formula "23"))
(rule "applyEq" (formula "4") (term "1,0") (ifseqformula "13"))
(rule "polySimp_addComm1" (formula "4") (term "0"))
(rule "add_literals" (formula "4") (term "0,0"))
(rule "applyEq" (formula "10") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "10"))
(rule "mul_literals" (formula "10") (term "1,0"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "add_literals" (formula "10") (term "0,0"))
(rule "applyEq" (formula "19") (term "0") (ifseqformula "13"))
(rule "leq_literals" (formula "19"))
(rule "true_left" (formula "19"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "mul_literals" (formula "2") (term "1,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "add_literals" (formula "2") (term "0,0"))
(rule "add_zero_left" (formula "2") (term "0"))
(rule "applyEq" (formula "12") (term "1,0,0,0") (ifseqformula "13"))
(rule "add_literals" (formula "12") (term "0,0,0"))
(rule "qeq_literals" (formula "12") (term "0,0"))
(builtin "One Step Simplification" (formula "12"))
(rule "eqSymm" (formula "12"))
(rule "applyEq" (formula "6") (term "1,0,0") (ifseqformula "13"))
(rule "add_literals" (formula "6") (term "0,0"))
(rule "div_literals" (formula "6") (term "0"))
(rule "eqSymm" (formula "6"))
(rule "applyEq" (formula "23") (term "0,1,0") (ifseqformula "14"))
(rule "mul_literals" (formula "23") (term "1,0"))
(rule "polySimp_addComm1" (formula "23") (term "0"))
(rule "polySimp_addComm1" (formula "23") (term "0,0"))
(rule "add_literals" (formula "23") (term "0,0,0"))
(rule "applyEq" (formula "20") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "20"))
(rule "mul_literals" (formula "20") (term "1,0"))
(rule "polySimp_addComm1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "0,0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "13"))
(rule "qeq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "7") (term "1,0") (ifseqformula "13"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "0,0"))
(rule "applyEq" (formula "11") (term "1,0") (ifseqformula "13"))
(rule "polySimp_addComm1" (formula "11") (term "0"))
(rule "add_literals" (formula "11") (term "0,0"))
(rule "applyEq" (formula "7") (term "0,1,0") (ifseqformula "6"))
(rule "times_zero_2" (formula "7") (term "1,0"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "qeq_literals" (formula "7"))
(rule "true_left" (formula "7"))
(rule "applyEqRigid" (formula "18") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "18") (term "1,0"))
(rule "add_literals" (formula "18") (term "0"))
(rule "leq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "17") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "17"))
(rule "true_left" (formula "17"))
(rule "applyEq" (formula "3") (term "0") (ifseqformula "1"))
(rule "inEqSimp_commuteLeq" (formula "3"))
(rule "inEqSimp_homoInEq1" (formula "3"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0"))
(rule "polySimp_elimOne" (formula "3") (term "1,0"))
(rule "applyEq" (formula "16") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "16"))
(rule "true_left" (formula "16"))
(rule "applyEq" (formula "8") (term "0") (ifseqformula "1"))
(rule "inEqSimp_homoInEq1" (formula "8"))
(rule "mul_literals" (formula "8") (term "1,0"))
(rule "polySimp_addComm1" (formula "8") (term "0"))
(rule "add_literals" (formula "8") (term "0,0"))
(rule "add_zero_left" (formula "8") (term "0"))
(rule "applyEqRigid" (formula "7") (term "0") (ifseqformula "6"))
(rule "qeq_literals" (formula "7"))
(rule "true_left" (formula "7"))
(rule "applyEq" (formula "5") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "add_literals" (formula "5") (term "0"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEqRigid" (formula "8") (term "0,1,0") (ifseqformula "5"))
(rule "times_zero_2" (formula "8") (term "1,0"))
(rule "add_zero_right" (formula "8") (term "0"))
(rule "leq_literals" (formula "8"))
(rule "true_left" (formula "8"))
(rule "applyEq" (formula "15") (term "1,0,0,1,0") (ifseqformula "9"))
(rule "add_literals" (formula "15") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "15") (term "0,1,0"))
(rule "qeq_literals" (formula "15") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "15"))
(rule "div_literals" (formula "15") (term "0,1,0"))
(rule "mul_literals" (formula "15") (term "1,0"))
(rule "polySimp_addComm1" (formula "15") (term "0"))
(rule "add_literals" (formula "15") (term "0,0"))
(rule "applyEq" (formula "14") (term "0,0") (ifseqformula "5"))
(rule "times_zero_2" (formula "14") (term "0"))
(rule "leq_literals" (formula "14"))
(rule "true_left" (formula "14"))
(rule "applyEq" (formula "2") (term "0,0") (ifseqformula "1"))
(rule "mul_literals" (formula "2") (term "0"))
(rule "qeq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "3") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "3") (term "1,0"))
(rule "add_literals" (formula "3") (term "0"))
(rule "leq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEqRigid" (formula "11") (term "0") (ifseqformula "3"))
(rule "leq_literals" (formula "11"))
(rule "true_left" (formula "11"))
(rule "applyEq" (formula "5") (term "0,1,0") (ifseqformula "3"))
(rule "times_zero_2" (formula "5") (term "1,0"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "5") (term "1,0,0") (ifseqformula "6"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "jdiv_axiom_inline" (formula "5") (term "0"))
(rule "div_literals" (formula "5") (term "1,0"))
(rule "mul_literals" (formula "5") (term "0,0,2,0"))
(rule "qeq_literals" (formula "5") (term "0,0"))
(builtin "One Step Simplification" (formula "5"))
(rule "polySimp_homoEq" (formula "5"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "add_zero_left" (formula "5") (term "0"))
(rule "applyEq" (formula "4") (term "0,0") (ifseqformula "3"))
(rule "times_zero_2" (formula "4") (term "0"))
(rule "leq_literals" (formula "4"))
(rule "true_left" (formula "4"))
(rule "applyEq" (formula "8") (term "1,0") (ifseqformula "4"))
(rule "add_literals" (formula "8") (term "0"))
(builtin "One Step Simplification" (formula "8"))
(rule "closeTrue" (formula "8"))
)
(branch "CUT: s2 = 1 FALSE"
(builtin "One Step Simplification" (formula "16"))
(rule "replace_known_right" (formula "15") (term "1") (ifseqformula "28"))
(builtin "One Step Simplification" (formula "15"))
(rule "replace_known_left" (formula "14") (term "1") (ifseqformula "16"))
(builtin "One Step Simplification" (formula "14"))
(rule "true_left" (formula "14"))
(rule "replace_known_left" (formula "13") (term "0") (ifseqformula "14"))
(builtin "One Step Simplification" (formula "13"))
(rule "true_left" (formula "13"))
(rule "applyEq" (formula "10") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "10"))
(rule "times_zero_2" (formula "10") (term "1,0"))
(rule "add_zero_right" (formula "10") (term "0"))
(rule "applyEq" (formula "26") (term "0") (ifseqformula "14"))
(rule "equal_literals" (formula "26"))
(rule "false_right" (formula "26"))
(rule "applyEq" (formula "7") (term "0") (ifseqformula "14"))
(rule "inEqSimp_homoInEq0" (formula "7"))
(rule "mul_literals" (formula "7") (term "1,0"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "polySimp_addComm0" (formula "7") (term "0,0"))
(rule "applyEq" (formula "21") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "21"))
(rule "times_zero_2" (formula "21") (term "1,0"))
(rule "add_zero_right" (formula "21") (term "0"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "14"))
(rule "inEqSimp_homoInEq0" (formula "5"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "polySimp_addComm1" (formula "5") (term "0,0"))
(rule "add_literals" (formula "5") (term "0,0,0"))
(rule "add_zero_left" (formula "5") (term "0,0"))
(rule "applyEq" (formula "23") (term "0") (ifseqformula "13"))
(rule "inEqSimp_commuteGeq" (formula "23"))
(rule "applyEq" (formula "4") (term "0") (ifseqformula "14"))
(rule "inEqSimp_homoInEq1" (formula "4"))
(rule "mul_literals" (formula "4") (term "1,0"))
(rule "polySimp_addComm1" (formula "4") (term "0"))
(rule "polySimp_addComm0" (formula "4") (term "0,0"))
(rule "applyEq" (formula "25") (term "0") (ifseqformula "14"))
(rule "leq_literals" (formula "25"))
(rule "true_left" (formula "25"))
(rule "applyEq" (formula "12") (term "1,1,0,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "12") (term "1,0,0"))
(rule "applyEq" (formula "11") (term "0") (ifseqformula "14"))
(rule "inEqSimp_homoInEq1" (formula "11"))
(rule "mul_literals" (formula "11") (term "1,0"))
(rule "polySimp_addComm1" (formula "11") (term "0"))
(rule "polySimp_addComm1" (formula "11") (term "0,0"))
(rule "add_literals" (formula "11") (term "0,0,0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "13"))
(rule "qeq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "24") (term "0,1,0,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "24") (term "1,0,0,0"))
(rule "polySimp_homoEq" (formula "24"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,0"))
(rule "polySimp_addComm1" (formula "24") (term "0"))
(rule "polySimp_addComm1" (formula "24") (term "0,0,1,0,0"))
(rule "add_literals" (formula "24") (term "0,0,0,1,0,0"))
(rule "applyEq" (formula "12") (term "0,0,0") (ifseqformula "14"))
(rule "leq_literals" (formula "12") (term "0,0"))
(builtin "One Step Simplification" (formula "12"))
(rule "eqSymm" (formula "12"))
(rule "applyEq" (formula "1") (term "1,0,0") (ifseqformula "14"))
(rule "polySimp_addComm0" (formula "1") (term "0,0"))
(rule "applyEq" (formula "6") (term "0,1,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "6") (term "1,0,0"))
(rule "polySimp_addComm0" (formula "6") (term "0,0"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "times_zero_2" (formula "2") (term "1,0"))
(rule "add_zero_right" (formula "2") (term "0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "13"))
(rule "leq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "22") (term "0") (ifseqformula "14"))
(rule "qeq_literals" (formula "22"))
(rule "true_left" (formula "22"))
(rule "applyEq" (formula "6") (term "1,0,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "6") (term "0,0"))
(rule "div_literals" (formula "6") (term "0"))
(rule "eqSymm" (formula "6"))
(rule "applyEq" (formula "12") (term "0,1,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "12") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "12") (term "0,0"))
(rule "add_literals" (formula "12") (term "0,0,0"))
(rule "applyEq" (formula "4") (term "1,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "4") (term "0"))
(rule "applyEq" (formula "5") (term "1,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "applyEq" (formula "1") (term "0,1,0,0") (ifseqformula "13"))
(rule "times_zero_2" (formula "1") (term "1,0,0"))
(rule "add_zero_right" (formula "1") (term "0,0"))
(rule "div_literals" (formula "1") (term "0"))
(rule "eqSymm" (formula "1"))
(rule "applyEq" (formula "22") (term "0,1,0") (ifseqformula "14"))
(rule "mul_literals" (formula "22") (term "1,0"))
(rule "polySimp_addComm1" (formula "22") (term "0"))
(rule "polySimp_addComm1" (formula "22") (term "0,0"))
(rule "add_literals" (formula "22") (term "0,0,0"))
(rule "add_zero_left" (formula "22") (term "0,0"))
(rule "applyEq" (formula "11") (term "1,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "11") (term "0"))
(rule "applyEq" (formula "7") (term "1,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "applyEqRigid" (formula "9") (term "0,1,1") (ifseqformula "6"))
(rule "mul_literals" (formula "9") (term "1,1"))
(rule "add_literals" (formula "9") (term "1"))
(rule "applyEqRigid" (formula "20") (term "0") (ifseqformula "6"))
(rule "leq_literals" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "3") (term "0,1") (ifseqformula "6"))
(rule "mul_literals" (formula "3") (term "1"))
(rule "applyEq" (formula "8") (term "0") (ifseqformula "6"))
(rule "qeq_literals" (formula "8"))
(rule "true_left" (formula "8"))
(rule "applyEq" (formula "19") (term "0,0") (ifseqformula "6"))
(rule "mul_literals" (formula "19") (term "0"))
(rule "leq_literals" (formula "19"))
(rule "true_left" (formula "19"))
(rule "applyEq" (formula "9") (term "0,1,0") (ifseqformula "6"))
(rule "mul_literals" (formula "9") (term "1,0"))
(rule "add_literals" (formula "9") (term "0"))
(rule "qeq_literals" (formula "9"))
(rule "true_left" (formula "9"))
(rule "apply_eq_monomials" (formula "2") (term "1,0") (ifseqformula "1"))
(rule "add_zero_left" (formula "2") (term "1,0,1,0"))
(rule "polySimp_mulAssoc" (formula "2") (term "0,1,0"))
(rule "polySimp_mulComm0" (formula "2") (term "0,0,1,0"))
(rule "polySimp_mulLiterals" (formula "2") (term "0,1,0"))
(rule "polySimp_pullOutFactor0" (formula "2") (term "1,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 "qeq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEqRigid" (formula "16") (term "0,1,0") (ifseqformula "1"))
(rule "times_zero_2" (formula "16") (term "1,0"))
(rule "add_zero_right" (formula "16") (term "0"))
(rule "leq_literals" (formula "16"))
(rule "true_left" (formula "16"))
(rule "applyEqRigid" (formula "14") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "14"))
(rule "true_left" (formula "14"))
(rule "applyEqRigid" (formula "7") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "7"))
(rule "true_left" (formula "7"))
(rule "applyEqRigid" (formula "2") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEqRigid" (formula "12") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "12"))
(rule "true_left" (formula "12"))
(rule "applyEqRigid" (formula "7") (term "1,1") (ifseqformula "4"))
(rule "add_literals" (formula "7") (term "1"))
(rule "applyEq" (formula "12") (term "1,0,0,1,0") (ifseqformula "8"))
(rule "add_zero_right" (formula "12") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "12") (term "0,1,0"))
(rule "qeq_literals" (formula "12") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "12"))
(rule "div_literals" (formula "12") (term "0,1,0"))
(rule "times_zero_2" (formula "12") (term "1,0"))
(rule "add_zero_right" (formula "12") (term "0"))
(rule "close" (formula "12") (ifseqformula "8"))
)
)
(branch "(s1 = 1 & s2 = 0)<>"
(rule "andLeft" (formula "1"))
(rule "applyEq" (formula "6") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "6"))
(rule "true_left" (formula "6"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "2"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "6") (term "0,1,0,0,0") (ifseqformula "2"))
(rule "times_zero_2" (formula "6") (term "1,0,0,0"))
(rule "add_zero_right" (formula "6") (term "0,0,0"))
(rule "polySimp_homoEq" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "1,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "2"))
(rule "leq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "5") (term "0,1,0") (ifseqformula "2"))
(rule "times_zero_2" (formula "5") (term "1,0"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "applyEq" (formula "5") (term "1,0,0,1,0") (ifseqformula "1"))
(rule "add_literals" (formula "5") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "5") (term "0,1,0"))
(rule "qeq_literals" (formula "5") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "5"))
(rule "div_literals" (formula "5") (term "0,1,0"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "applyEq" (formula "5") (term "1,0") (ifseqformula "1"))
(rule "add_literals" (formula "5") (term "0"))
(builtin "One Step Simplification" (formula "5"))
(rule "closeTrue" (formula "5"))
)
)
(branch "Case 2"
(rule "impRight" (formula "7"))
(rule "cnf_rightDist" (formula "1") (term "0"))
(rule "commute_or" (formula "1") (term "0,0"))
(rule "cnf_rightDist" (formula "1") (term "1,0"))
(rule "commute_or" (formula "1") (term "0,1,0"))
(rule "cnf_rightDist" (formula "1") (term "0,0"))
(rule "commute_or" (formula "1") (term "1,0,0"))
(rule "orLeft" (formula "1"))
(branch " (s1 = 1 | s1 = 2) & (s1 = 1 | s2 = 0) & ((s1 = 2 | s2 = 2) & (s2 = 0 | s2 = 2))"
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "2"))
(rule "andLeft" (formula "1"))
(rule "jdiv_axiom" (formula "11") (term "0,0"))
(rule "eqSymm" (formula "1"))
(rule "polySimp_mulComm0" (formula "1") (term "0,0,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "0,0,2,0"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,0"))
(rule "polySimp_elimOne" (formula "1") (term "1,0,0,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "0,0,0,2,0"))
(rule "mul_literals" (formula "1") (term "0,0,0,0,2,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "1") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "1") (term "0,0,0"))
(rule "polySimp_elimOne" (formula "1") (term "0,0,0"))
(rule "polyDiv_pullOut" (formula "1") (term "0,2,0") (inst "polyDivCoeff=Z(neglit(1(#)))"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,0,2,0"))
(rule "equal_literals" (formula "1") (term "0,0,2,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,0,0,0,2,0"))
(rule "polySimp_mulComm0" (formula "1") (term "2,0"))
(rule "polySimp_addComm0" (formula "1") (term "1,2,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,1,1,2,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,0,1,1,2,0"))
(rule "add_literals" (formula "1") (term "0,0,0,1,1,2,0"))
(rule "add_zero_left" (formula "1") (term "0,0,1,1,2,0"))
(rule "polySimp_rightDist" (formula "1") (term "2,0"))
(rule "mul_literals" (formula "1") (term "0,2,0"))
(rule "polyDiv_pullOut" (formula "1") (term "1,0") (inst "polyDivCoeff=Z(1(#))"))
(rule "polySimp_mulLiterals" (formula "1") (term "1,0,0,2,1,0"))
(rule "equal_literals" (formula "1") (term "0,1,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,0,0,1,0"))
(rule "polySimp_addComm0" (formula "1") (term "1,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,1,1,0"))
(rule "polySimp_addComm1" (formula "1") (term "0,0,1,1,0"))
(rule "add_literals" (formula "1") (term "0,0,0,1,1,0"))
(rule "add_zero_left" (formula "1") (term "0,0,1,1,0"))
(rule "div_axiom" (formula "1") (term "0,1,2,0") (inst "quotient=quotient_0"))
(rule "qeq_literals" (formula "1") (term "0,1,1"))
(builtin "One Step Simplification" (formula "1"))
(rule "equal_literals" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "mul_literals" (formula "1") (term "1,1,1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "polySimp_addAssoc" (formula "3") (term "0,1"))
(rule "polySimp_addComm1" (formula "3") (term "1"))
(rule "polySimp_addComm1" (formula "3") (term "0,1"))
(rule "add_literals" (formula "3") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "1,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "polySimp_addComm0" (formula "2") (term "0,0"))
(rule "inEqSimp_homoInEq1" (formula "3"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0"))
(rule "polySimp_addComm1" (formula "3") (term "0"))
(rule "polySimp_addComm1" (formula "3") (term "0,0"))
(rule "applyEq" (formula "4") (term "0,1,2,0") (ifseqformula "1"))
(rule "inEqSimp_sepPosMonomial1" (formula "2"))
(rule "polySimp_mulComm0" (formula "2") (term "1"))
(rule "polySimp_rightDist" (formula "2") (term "1"))
(rule "polySimp_mulLiterals" (formula "2") (term "1,1"))
(rule "polySimp_elimOne" (formula "2") (term "1,1"))
(rule "polySimp_mulComm0" (formula "2") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "2") (term "0,1"))
(rule "inEqSimp_sepPosMonomial0" (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 "polySimp_elimOne" (formula "3") (term "1,1"))
(rule "polySimp_rightDist" (formula "3") (term "0,1"))
(rule "mul_literals" (formula "3") (term "0,0,1"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,1"))
(rule "inEqSimp_exactShadow3" (formula "13") (ifseqformula "3"))
(rule "times_zero_1" (formula "13") (term "0,0"))
(rule "add_zero_left" (formula "13") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "13"))
(rule "polySimp_mulComm0" (formula "13") (term "1"))
(rule "polySimp_rightDist" (formula "13") (term "1"))
(rule "mul_literals" (formula "13") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "13") (term "1,1"))
(rule "inEqSimp_exactShadow3" (formula "2") (ifseqformula "15"))
(rule "polySimp_rightDist" (formula "2") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "2") (term "0,0,0"))
(rule "polySimp_mulComm0" (formula "2") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "2") (term "0,0,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "polySimp_addComm0" (formula "2") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "0"))
(rule "polySimp_elimOne" (formula "2") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "12") (ifseqformula "2"))
(rule "times_zero_1" (formula "12") (term "0,0"))
(rule "add_zero_left" (formula "12") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "12"))
(rule "polySimp_mulLiterals" (formula "12") (term "0"))
(rule "elimGcdLeq_antec" (formula "12") (inst "elimGcdRightDiv=Z(0(#))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "12") (term "0,0"))
(builtin "One Step Simplification" (formula "12"))
(rule "neg_literal" (formula "12") (term "0,0,0,0,0,0"))
(rule "times_zero_1" (formula "12") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "12") (term "1,0,0"))
(rule "polySimp_addLiterals" (formula "12") (term "0,0,0,0"))
(rule "add_literals" (formula "12") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "12") (term "0,0"))
(rule "add_literals" (formula "12") (term "1,1,0,0"))
(rule "times_zero_1" (formula "12") (term "1,0,0"))
(rule "add_zero_right" (formula "12") (term "0,0"))
(rule "qeq_literals" (formula "12") (term "0"))
(builtin "One Step Simplification" (formula "12"))
(rule "inEqSimp_exactShadow3" (formula "15") (ifseqformula "14"))
(rule "polySimp_rightDist" (formula "15") (term "0,0"))
(rule "mul_literals" (formula "15") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "15") (term "0"))
(rule "add_literals" (formula "15") (term "0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "15"))
(rule "mul_literals" (formula "15") (term "1"))
(rule "elimGcdGeq_antec" (formula "15") (inst "elimGcdRightDiv=Z(neglit(1(#)))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "15") (term "0,0"))
(builtin "One Step Simplification" (formula "15"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "15") (term "1,0,0"))
(rule "mul_literals" (formula "15") (term "1,0,0,0,0,0"))
(rule "polySimp_addLiterals" (formula "15") (term "0,0,0,0"))
(rule "add_literals" (formula "15") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "15") (term "0,0"))
(rule "add_literals" (formula "15") (term "1,1,0,0"))
(rule "times_zero_1" (formula "15") (term "1,0,0"))
(rule "add_zero_right" (formula "15") (term "0,0"))
(rule "leq_literals" (formula "15") (term "0"))
(builtin "One Step Simplification" (formula "15"))
(rule "div_axiom" (formula "5") (term "1,1,0") (inst "quotient=quotient_1"))
(rule "mul_literals" (formula "5") (term "1,1,1,1,1"))
(rule "equal_literals" (formula "5") (term "0"))
(builtin "One Step Simplification" (formula "5"))
(rule "qeq_literals" (formula "5") (term "0,1"))
(builtin "One Step Simplification" (formula "5"))
(rule "andLeft" (formula "5"))
(rule "andLeft" (formula "5"))
(rule "polySimp_addAssoc" (formula "7") (term "0,1"))
(rule "polySimp_addComm1" (formula "7") (term "1"))
(rule "polySimp_addComm1" (formula "7") (term "0,1"))
(rule "add_literals" (formula "7") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "1,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "polySimp_addComm0" (formula "6") (term "0,0"))
(rule "inEqSimp_homoInEq1" (formula "7"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,0"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "polySimp_addComm1" (formula "7") (term "0,0"))
(rule "applyEq" (formula "8") (term "1,1,0") (ifseqformula "5"))
(rule "inEqSimp_sepNegMonomial1" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "0"))
(rule "polySimp_elimOne" (formula "6") (term "0"))
(rule "inEqSimp_sepNegMonomial0" (formula "7"))
(rule "polySimp_mulLiterals" (formula "7") (term "0"))
(rule "polySimp_elimOne" (formula "7") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "3") (ifseqformula "6"))
(rule "polySimp_rightDist" (formula "3") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "3") (term "0,0,0"))
(rule "polySimp_mulComm0" (formula "3") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "0,0,0"))
(rule "polySimp_addAssoc" (formula "3") (term "0"))
(rule "polySimp_addComm1" (formula "3") (term "0,0"))
(rule "polySimp_pullOutFactor2b" (formula "3") (term "0"))
(rule "add_literals" (formula "3") (term "1,1,0"))
(rule "times_zero_1" (formula "3") (term "1,0"))
(rule "add_zero_right" (formula "3") (term "0"))
(rule "polySimp_addComm0" (formula "3") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "3"))
(rule "polySimp_mulLiterals" (formula "3") (term "0"))
(rule "elimGcdLeq_antec" (formula "3") (inst "elimGcdRightDiv=mul(quotient_1, Z(neglit(1(#))))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "neg_literal" (formula "3") (term "0,0,0,0,0,1,0"))
(rule "mul_literals" (formula "3") (term "0,1,0,0,0,0,1,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,1,0"))
(rule "leq_literals" (formula "3") (term "0,0"))
(builtin "One Step Simplification" (formula "3"))
(rule "polySimp_pullOutFactor0b" (formula "3") (term "0,0"))
(rule "add_literals" (formula "3") (term "1,1,0,0"))
(rule "times_zero_1" (formula "3") (term "1,0,0"))
(rule "add_zero_right" (formula "3") (term "0,0"))
(rule "polySimp_mulAssoc" (formula "3") (term "1,0,0,0"))
(rule "polySimp_mulComm0" (formula "3") (term "0,1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "3") (term "1,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "3") (term "0,0"))
(rule "add_literals" (formula "3") (term "1,1,0,0"))
(rule "times_zero_1" (formula "3") (term "1,0,0"))
(rule "add_zero_right" (formula "3") (term "0,0"))
(rule "qeq_literals" (formula "3") (term "0"))
(builtin "One Step Simplification" (formula "3"))
(rule "inEqSimp_exactShadow3" (formula "8") (ifseqformula "5"))
(rule "polySimp_rightDist" (formula "8") (term "0,0"))
(rule "polySimp_rightDist" (formula "8") (term "0,0,0"))
(rule "mul_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0"))
(rule "polySimp_pullOutFactor2b" (formula "8") (term "0"))
(rule "add_literals" (formula "8") (term "1,1,0"))
(rule "times_zero_1" (formula "8") (term "1,0"))
(rule "add_zero_right" (formula "8") (term "0"))
(rule "polySimp_addAssoc" (formula "8") (term "0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "8"))
(rule "polySimp_mulComm0" (formula "8") (term "1"))
(rule "polySimp_rightDist" (formula "8") (term "1"))
(rule "mul_literals" (formula "8") (term "0,1"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,1"))
(rule "elimGcdGeq_antec" (formula "8") (inst "elimGcdRightDiv=add(Z(neglit(1(#))), mul(quotient_1, Z(neglit(1(#)))))") (inst "elimGcdLeftDiv=quotient_0") (inst "elimGcd=Z(3(#))"))
(rule "mul_literals" (formula "8") (term "0,1,0,0,0,0,1,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0,1,0"))
(rule "leq_literals" (formula "8") (term "0,0"))
(builtin "One Step Simplification" (formula "8"))
(rule "polySimp_pullOutFactor0b" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "1,1,0,0"))
(rule "times_zero_1" (formula "8") (term "1,0,0"))
(rule "add_zero_right" (formula "8") (term "0,0"))
(rule "polySimp_rightDist" (formula "8") (term "1,0,0,0"))
(rule "mul_literals" (formula "8") (term "0,1,0,0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,1,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0,0,0"))
(rule "add_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_addAssoc" (formula "8") (term "0,0"))
(rule "polySimp_addComm1" (formula "8") (term "0,0,0"))
(rule "add_literals" (formula "8") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "8") (term "0,0"))
(rule "add_literals" (formula "8") (term "1,1,0,0"))
(rule "times_zero_1" (formula "8") (term "1,0,0"))
(rule "add_zero_right" (formula "8") (term "0,0"))
(rule "leq_literals" (formula "8") (term "0"))
(builtin "One Step Simplification" (formula "8"))
(rule "inEqSimp_exactShadow3" (formula "9") (ifseqformula "23"))
(rule "polySimp_rightDist" (formula "9") (term "0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0"))
(rule "polySimp_rightDist" (formula "9") (term "0,0,0"))
(rule "mul_literals" (formula "9") (term "0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "9") (term "1,0,0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0,0"))
(rule "add_literals" (formula "9") (term "0,0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "9"))
(rule "polySimp_mulLiterals" (formula "9") (term "0"))
(rule "polySimp_elimOne" (formula "9") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "23") (ifseqformula "7"))
(rule "times_zero_1" (formula "23") (term "0,0"))
(rule "add_zero_left" (formula "23") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "23"))
(rule "polySimp_mulLiterals" (formula "23") (term "1"))
(rule "inEqSimp_exactShadow3" (formula "21") (ifseqformula "3"))
(rule "mul_literals" (formula "21") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "21"))
(rule "polySimp_mulLiterals" (formula "21") (term "0"))
(rule "polySimp_elimOne" (formula "21") (term "0"))
(rule "inEqSimp_exactShadow3" (formula "19") (ifseqformula "9"))
(rule "times_zero_1" (formula "19") (term "0,0"))
(rule "add_zero_left" (formula "19") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "19"))
(rule "mul_literals" (formula "19") (term "1"))
(rule "elimGcdGeq_antec" (formula "19") (inst "elimGcdRightDiv=Z(neglit(1(#)))") (inst "elimGcdLeftDiv=quotient_1") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "19") (term "0,0"))
(builtin "One Step Simplification" (formula "19"))
(rule "polySimp_mulLiterals" (formula "19") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "19") (term "1,0,0"))
(rule "mul_literals" (formula "19") (term "1,0,0,0,0,0"))
(rule "polySimp_addLiterals" (formula "19") (term "0,0,0,0"))
(rule "add_literals" (formula "19") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "19") (term "0,0"))
(rule "add_literals" (formula "19") (term "1,1,0,0"))
(rule "times_zero_1" (formula "19") (term "1,0,0"))
(rule "add_zero_right" (formula "19") (term "0,0"))
(rule "leq_literals" (formula "19") (term "0"))
(builtin "One Step Simplification" (formula "19"))
(rule "inEqSimp_exactShadow3" (formula "24") (ifseqformula "9"))
(rule "polySimp_rightDist" (formula "24") (term "0,0"))
(rule "mul_literals" (formula "24") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "24") (term "0"))
(rule "polySimp_addAssoc" (formula "24") (term "0,0"))
(rule "add_literals" (formula "24") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "24"))
(rule "polySimp_mulComm0" (formula "24") (term "1"))
(rule "polySimp_rightDist" (formula "24") (term "1"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1"))
(rule "mul_literals" (formula "24") (term "0,1"))
(rule "inEqSimp_subsumption6" (formula "24") (ifseqformula "8"))
(rule "greater_literals" (formula "24") (term "0,0"))
(builtin "One Step Simplification" (formula "24"))
(rule "polySimp_rightDist" (formula "24") (term "1,0"))
(rule "mul_literals" (formula "24") (term "0,1,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1,0"))
(rule "inEqSimp_homoInEq0" (formula "24") (term "0"))
(rule "polySimp_mulComm0" (formula "24") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "24") (term "1,0,0"))
(rule "mul_literals" (formula "24") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,1,0,0"))
(rule "polySimp_addAssoc" (formula "24") (term "0,0"))
(rule "polySimp_addComm1" (formula "24") (term "0,0,0"))
(rule "add_literals" (formula "24") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "24") (term "0,0"))
(rule "add_literals" (formula "24") (term "1,1,0,0"))
(rule "times_zero_1" (formula "24") (term "1,0,0"))
(rule "add_zero_right" (formula "24") (term "0,0"))
(rule "qeq_literals" (formula "24") (term "0"))
(builtin "One Step Simplification" (formula "24"))
(rule "true_left" (formula "24"))
(rule "inEqSimp_exactShadow3" (formula "25") (ifseqformula "2"))
(rule "polySimp_mulAssoc" (formula "25") (term "0,0"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "polySimp_addAssoc" (formula "25") (term "0"))
(rule "polySimp_addComm0" (formula "25") (term "0,0"))
(rule "inEqSimp_sepNegMonomial1" (formula "25"))
(rule "polySimp_mulLiterals" (formula "25") (term "0"))
(rule "inEqSimp_subsumption4" (formula "25") (ifseqformula "3"))
(rule "greater_literals" (formula "25") (term "0,0"))
(builtin "One Step Simplification" (formula "25"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "inEqSimp_homoInEq0" (formula "25") (term "0"))
(rule "polySimp_mulLiterals" (formula "25") (term "1,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "25") (term "0,0"))
(rule "add_literals" (formula "25") (term "1,1,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0"))
(rule "add_zero_right" (formula "25") (term "0,0"))
(rule "qeq_literals" (formula "25") (term "0"))
(builtin "One Step Simplification" (formula "25"))
(rule "true_left" (formula "25"))
(rule "inEqSimp_exactShadow3" (formula "8") (ifseqformula "18"))
(rule "add_zero_right" (formula "8") (term "0"))
(rule "polySimp_rightDist" (formula "8") (term "0"))
(rule "mul_literals" (formula "8") (term "0,0"))
(rule "polySimp_mulLiterals" (formula "8") (term "1,0"))
(rule "polySimp_elimOne" (formula "8") (term "1,0"))
(rule "inEqSimp_sepPosMonomial1" (formula "8"))
(rule "mul_literals" (formula "8") (term "1"))
(rule "inEqSimp_exactShadow3" (formula "25") (ifseqformula "21"))
(rule "polySimp_mulAssoc" (formula "25") (term "0,0"))
(rule "polySimp_mulComm0" (formula "25") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "0,0"))
(rule "polySimp_addComm0" (formula "25") (term "0"))
(rule "inEqSimp_sepNegMonomial1" (formula "25"))
(rule "polySimp_mulLiterals" (formula "25") (term "0"))
(rule "elimGcdLeq_antec" (formula "25") (inst "elimGcdRightDiv=Z(0(#))") (inst "elimGcdLeftDiv=quotient_1") (inst "elimGcd=Z(3(#))"))
(rule "leq_literals" (formula "25") (term "0,0"))
(builtin "One Step Simplification" (formula "25"))
(rule "neg_literal" (formula "25") (term "0,0,0,0,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0,0,0,0"))
(rule "polySimp_mulLiterals" (formula "25") (term "1,0,0"))
(rule "polySimp_addLiterals" (formula "25") (term "0,0,0,0"))
(rule "add_literals" (formula "25") (term "0,0,0,0"))
(rule "polySimp_pullOutFactor0b" (formula "25") (term "0,0"))
(rule "add_literals" (formula "25") (term "1,1,0,0"))
(rule "times_zero_1" (formula "25") (term "1,0,0"))
(rule "add_zero_right" (formula "25") (term "0,0"))
(rule "qeq_literals" (formula "25") (term "0"))
(builtin "One Step Simplification" (formula "25"))
(rule "inEqSimp_subsumption0" (formula "22") (ifseqformula "25"))
(rule "leq_literals" (formula "22") (term "0"))
(builtin "One Step Simplification" (formula "22"))
(rule "true_left" (formula "22"))
(rule "cut_direct" (formula "15") (term "1"))
(branch "CUT: s2 = 2 TRUE"
(builtin "One Step Simplification" (formula "16"))
(rule "true_left" (formula "16"))
(rule "replace_known_left" (formula "14") (term "1") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "14"))
(rule "true_left" (formula "14"))
(rule "applyEq" (formula "6") (term "0,1,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "6") (term "1,0,0"))
(rule "polySimp_addComm0" (formula "6") (term "0,0"))
(rule "applyEq" (formula "26") (term "0") (ifseqformula "14"))
(rule "leq_literals" (formula "26"))
(rule "true_left" (formula "26"))
(rule "applyEq" (formula "26") (term "0,1,0,0,0") (ifseqformula "14"))
(rule "mul_literals" (formula "26") (term "1,0,0,0"))
(rule "polySimp_homoEq" (formula "26"))
(rule "polySimp_mulLiterals" (formula "26") (term "1,0"))
(rule "polySimp_addComm1" (formula "26") (term "0"))
(rule "polySimp_addComm1" (formula "26") (term "0,0,1,0,0"))
(rule "add_literals" (formula "26") (term "0,0,0,1,0,0"))
(rule "applyEq" (formula "13") (term "0,1") (ifseqformula "14"))
(rule "equal_literals" (formula "13") (term "1"))
(builtin "One Step Simplification" (formula "13"))
(rule "replace_known_left" (formula "12") (term "0") (ifseqformula "13"))
(builtin "One Step Simplification" (formula "12"))
(rule "true_left" (formula "12"))
(rule "applyEq" (formula "11") (term "0,0,0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "11") (term "0,0"))
(rule "mul_literals" (formula "11") (term "1,0,0,0"))
(rule "polySimp_addComm1" (formula "11") (term "0,0,0"))
(rule "add_literals" (formula "11") (term "0,0,0,0"))
(rule "applyEq" (formula "10") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "10"))
(rule "mul_literals" (formula "10") (term "1,0"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "polySimp_addComm1" (formula "10") (term "0,0"))
(rule "add_literals" (formula "10") (term "0,0,0"))
(rule "applyEq" (formula "1") (term "1,0,0") (ifseqformula "13"))
(rule "polySimp_addComm0" (formula "1") (term "0,0"))
(rule "applyEq" (formula "4") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "4"))
(rule "mul_literals" (formula "4") (term "1,0"))
(rule "polySimp_addComm1" (formula "4") (term "0"))
(rule "polySimp_addComm0" (formula "4") (term "0,0"))
(rule "applyEq" (formula "24") (term "0") (ifseqformula "13"))
(rule "qeq_literals" (formula "24"))
(rule "true_left" (formula "24"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "5"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "polySimp_addComm1" (formula "5") (term "0,0"))
(rule "add_literals" (formula "5") (term "0,0,0"))
(rule "add_zero_left" (formula "5") (term "0,0"))
(rule "applyEq" (formula "7") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "7"))
(rule "mul_literals" (formula "7") (term "1,0"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "polySimp_addComm0" (formula "7") (term "0,0"))
(rule "applyEq" (formula "11") (term "0,1,0,1") (ifseqformula "13"))
(rule "mul_literals" (formula "11") (term "1,0,1"))
(rule "polySimp_addComm1" (formula "11") (term "0,1"))
(rule "add_literals" (formula "11") (term "0,0,1"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "12"))
(rule "qeq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "20") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq1" (formula "20"))
(rule "mul_literals" (formula "20") (term "1,0"))
(rule "polySimp_addComm1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "0,0"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "mul_literals" (formula "2") (term "1,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "add_literals" (formula "2") (term "0,0"))
(rule "applyEq" (formula "9") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq0" (formula "9"))
(rule "mul_literals" (formula "9") (term "1,0"))
(rule "polySimp_addComm1" (formula "9") (term "0"))
(rule "add_literals" (formula "9") (term "0,0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "12"))
(rule "leq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "6") (term "1,0,0") (ifseqformula "12"))
(rule "add_literals" (formula "6") (term "0,0"))
(rule "div_literals" (formula "6") (term "0"))
(rule "eqSymm" (formula "6"))
(rule "applyEq" (formula "21") (term "0") (ifseqformula "12"))
(rule "inEqSimp_commuteGeq" (formula "21"))
(rule "applyEq" (formula "1") (term "0,1,0,0") (ifseqformula "12"))
(rule "mul_literals" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "div_literals" (formula "1") (term "0"))
(rule "eqSymm" (formula "1"))
(rule "applyEq" (formula "5") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm0" (formula "5") (term "0"))
(rule "applyEq" (formula "11") (term "1,0,0,0") (ifseqformula "12"))
(rule "add_literals" (formula "11") (term "0,0,0"))
(rule "qeq_literals" (formula "11") (term "0,0"))
(builtin "One Step Simplification" (formula "11"))
(rule "eqSymm" (formula "11"))
(rule "applyEq" (formula "22") (term "0,1,0") (ifseqformula "13"))
(rule "mul_literals" (formula "22") (term "1,0"))
(rule "polySimp_addComm1" (formula "22") (term "0"))
(rule "polySimp_addComm1" (formula "22") (term "0,0"))
(rule "add_literals" (formula "22") (term "0,0,0"))
(rule "applyEq" (formula "7") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm1" (formula "7") (term "0"))
(rule "add_literals" (formula "7") (term "0,0"))
(rule "applyEq" (formula "4") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm1" (formula "4") (term "0"))
(rule "add_literals" (formula "4") (term "0,0"))
(rule "applyEq" (formula "10") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "add_literals" (formula "10") (term "0,0"))
(rule "applyEq" (formula "3") (term "0,1") (ifseqformula "6"))
(rule "mul_literals" (formula "3") (term "1"))
(rule "applyEq" (formula "20") (term "0") (ifseqformula "6"))
(rule "leq_literals" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "17") (term "0") (ifseqformula "6"))
(rule "qeq_literals" (formula "17"))
(rule "true_left" (formula "17"))
(rule "applyEqRigid" (formula "8") (term "0,1,1") (ifseqformula "6"))
(rule "mul_literals" (formula "8") (term "1,1"))
(rule "add_literals" (formula "8") (term "1"))
(rule "applyEq" (formula "16") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "16"))
(rule "true_left" (formula "16"))
(rule "applyEq" (formula "9") (term "0,1,0") (ifseqformula "6"))
(rule "mul_literals" (formula "9") (term "1,0"))
(rule "add_literals" (formula "9") (term "0"))
(rule "qeq_literals" (formula "9"))
(rule "true_left" (formula "9"))
(rule "applyEqRigid" (formula "15") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "15"))
(rule "true_left" (formula "15"))
(rule "applyEqRigid" (formula "16") (term "0,0") (ifseqformula "6"))
(rule "mul_literals" (formula "16") (term "0"))
(rule "leq_literals" (formula "16"))
(rule "true_left" (formula "16"))
(rule "applyEq" (formula "8") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "8"))
(rule "true_left" (formula "8"))
(rule "applyEqRigid" (formula "3") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEq" (formula "2") (term "0,1,0") (ifseqformula "1"))
(rule "times_zero_2" (formula "2") (term "1,0"))
(rule "add_zero_right" (formula "2") (term "0"))
(rule "qeq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "12") (term "0,1,0") (ifseqformula "1"))
(rule "times_zero_2" (formula "12") (term "1,0"))
(rule "add_zero_right" (formula "12") (term "0"))
(rule "leq_literals" (formula "12"))
(rule "true_left" (formula "12"))
(rule "applyEqRigid" (formula "3") (term "0,1,0") (ifseqformula "1"))
(rule "times_zero_2" (formula "3") (term "1,0"))
(rule "add_zero_right" (formula "3") (term "0"))
(rule "qeq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEqRigid" (formula "5") (term "0,1,0") (ifseqformula "3"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "add_literals" (formula "5") (term "0"))
(rule "leq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "10") (term "0,1,0") (ifseqformula "5"))
(rule "polySimp_mulComm0" (formula "10") (term "1,0"))
(rule "polySimp_rightDist" (formula "10") (term "1,0"))
(rule "mul_literals" (formula "10") (term "0,1,0"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "polySimp_addAssoc" (formula "10") (term "0,0"))
(rule "add_literals" (formula "10") (term "0,0,0"))
(rule "applyEqRigid" (formula "4") (term "0,1,0") (ifseqformula "3"))
(rule "mul_literals" (formula "4") (term "1,0"))
(rule "add_literals" (formula "4") (term "0"))
(rule "qeq_literals" (formula "4"))
(rule "true_left" (formula "4"))
(rule "applyEq" (formula "4") (term "1,0,0") (ifseqformula "5"))
(rule "add_literals" (formula "4") (term "0,0"))
(rule "jdiv_axiom_inline" (formula "4") (term "0"))
(rule "div_literals" (formula "4") (term "1,0"))
(rule "mul_literals" (formula "4") (term "0,0,2,0"))
(rule "qeq_literals" (formula "4") (term "0,0"))
(builtin "One Step Simplification" (formula "4"))
(rule "polySimp_homoEq" (formula "4"))
(rule "times_zero_2" (formula "4") (term "1,0"))
(rule "add_zero_right" (formula "4") (term "0"))
(rule "applyEqRigid" (formula "2") (term "0,1,0") (ifseqformula "1"))
(rule "times_zero_2" (formula "2") (term "1,0"))
(rule "add_zero_right" (formula "2") (term "0"))
(rule "leq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "8") (term "1,0") (ifseqformula "4"))
(rule "polySimp_addComm1" (formula "8") (term "0"))
(rule "add_literals" (formula "8") (term "0,0"))
(rule "applyEq" (formula "3") (term "1,0") (ifseqformula "2"))
(rule "add_literals" (formula "3") (term "0"))
(builtin "One Step Simplification" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEq" (formula "7") (term "0,1,0") (ifseqformula "2"))
(rule "mul_literals" (formula "7") (term "1,0"))
(rule "add_literals" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
(branch "CUT: s2 = 2 FALSE"
(builtin "One Step Simplification" (formula "15"))
(rule "replace_known_left" (formula "13") (term "1") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "13"))
(rule "true_left" (formula "13"))
(rule "replace_known_right" (formula "13") (term "1") (ifseqformula "27"))
(builtin "One Step Simplification" (formula "13"))
(rule "replace_known_left" (formula "12") (term "1") (ifseqformula "13"))
(builtin "One Step Simplification" (formula "12"))
(rule "true_left" (formula "12"))
(rule "applyEq" (formula "6") (term "0,1,0,0") (ifseqformula "13"))
(rule "times_zero_2" (formula "6") (term "1,0,0"))
(rule "add_zero_right" (formula "6") (term "0,0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "12"))
(rule "qeq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "12"))
(rule "leq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEq" (formula "19") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq1" (formula "19"))
(rule "mul_literals" (formula "19") (term "1,0"))
(rule "polySimp_addComm1" (formula "19") (term "0"))
(rule "add_literals" (formula "19") (term "0,0"))
(rule "applyEq" (formula "10") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "10"))
(rule "times_zero_2" (formula "10") (term "1,0"))
(rule "add_zero_right" (formula "10") (term "0"))
(rule "applyEq" (formula "9") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq0" (formula "9"))
(rule "mul_literals" (formula "9") (term "1,0"))
(rule "polySimp_addComm1" (formula "9") (term "0"))
(rule "add_literals" (formula "9") (term "0,0"))
(rule "applyEq" (formula "4") (term "1,1") (ifseqformula "12"))
(rule "polySimp_addComm0" (formula "4") (term "1"))
(rule "applyEq" (formula "11") (term "1,1,0,0") (ifseqformula "12"))
(rule "add_literals" (formula "11") (term "1,0,0"))
(rule "applyEq" (formula "22") (term "0") (ifseqformula "13"))
(rule "qeq_literals" (formula "22"))
(rule "true_left" (formula "22"))
(rule "applyEq" (formula "11") (term "0,0,0") (ifseqformula "13"))
(rule "leq_literals" (formula "11") (term "0,0"))
(builtin "One Step Simplification" (formula "11"))
(rule "eqSymm" (formula "11"))
(rule "applyEq" (formula "7") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "7"))
(rule "times_zero_2" (formula "7") (term "1,0"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "applyEq" (formula "4") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq1" (formula "4"))
(rule "times_zero_2" (formula "4") (term "1,0"))
(rule "add_zero_right" (formula "4") (term "0"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "13"))
(rule "inEqSimp_homoInEq0" (formula "5"))
(rule "times_zero_2" (formula "5") (term "1,0"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "12"))
(rule "inEqSimp_homoInEq0" (formula "2"))
(rule "mul_literals" (formula "2") (term "1,0"))
(rule "polySimp_addComm1" (formula "2") (term "0"))
(rule "add_literals" (formula "2") (term "0,0"))
(rule "add_zero_left" (formula "2") (term "0"))
(rule "applyEq" (formula "24") (term "0,1,0,0,0") (ifseqformula "13"))
(rule "times_zero_2" (formula "24") (term "1,0,0,0"))
(rule "add_zero_right" (formula "24") (term "0,0,0"))
(rule "polySimp_homoEq" (formula "24"))
(rule "polySimp_mulLiterals" (formula "24") (term "1,0"))
(rule "polySimp_addComm1" (formula "24") (term "0"))
(rule "applyEq" (formula "23") (term "0") (ifseqformula "13"))
(rule "equal_literals" (formula "23"))
(rule "false_right" (formula "23"))
(rule "applyEq" (formula "21") (term "0") (ifseqformula "12"))
(rule "inEqSimp_commuteGeq" (formula "21"))
(rule "applyEq" (formula "22") (term "0") (ifseqformula "13"))
(rule "leq_literals" (formula "22"))
(rule "true_left" (formula "22"))
(rule "applyEq" (formula "1") (term "1,0,0") (ifseqformula "13"))
(rule "add_zero_right" (formula "1") (term "0,0"))
(rule "applyEq" (formula "1") (term "0,0,0") (ifseqformula "12"))
(rule "mul_literals" (formula "1") (term "0,0"))
(rule "div_literals" (formula "1") (term "0"))
(rule "eqSymm" (formula "1"))
(rule "applyEq" (formula "7") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm0" (formula "7") (term "0"))
(rule "applyEq" (formula "6") (term "0,0") (ifseqformula "12"))
(rule "div_literals" (formula "6") (term "0"))
(rule "eqSymm" (formula "6"))
(rule "applyEq" (formula "10") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "add_literals" (formula "10") (term "0,0"))
(rule "add_zero_left" (formula "10") (term "0"))
(rule "applyEq" (formula "5") (term "1,0") (ifseqformula "12"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "applyEq" (formula "11") (term "0,1,0,0") (ifseqformula "13"))
(rule "times_zero_2" (formula "11") (term "1,0,0"))
(rule "add_zero_right" (formula "11") (term "0,0"))
(rule "applyEq" (formula "22") (term "0,1,0") (ifseqformula "13"))
(rule "times_zero_2" (formula "22") (term "1,0"))
(rule "add_zero_right" (formula "22") (term "0"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "18"))
(rule "true_left" (formula "18"))
(rule "applyEqRigid" (formula "8") (term "0") (ifseqformula "1"))
(rule "inEqSimp_homoInEq1" (formula "8"))
(rule "mul_literals" (formula "8") (term "1,0"))
(rule "polySimp_addComm1" (formula "8") (term "0"))
(rule "add_literals" (formula "8") (term "0,0"))
(rule "add_zero_left" (formula "8") (term "0"))
(rule "applyEqRigid" (formula "2") (term "0,0") (ifseqformula "1"))
(rule "mul_literals" (formula "2") (term "0"))
(rule "qeq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "15") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "15"))
(rule "true_left" (formula "15"))
(rule "applyEqRigid" (formula "2") (term "0") (ifseqformula "1"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "inEqSimp_homoInEq1" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "1,0"))
(rule "polySimp_elimOne" (formula "2") (term "1,0"))
(rule "applyEq" (formula "16") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "16") (term "1,0"))
(rule "add_literals" (formula "16") (term "0"))
(rule "leq_literals" (formula "16"))
(rule "true_left" (formula "16"))
(rule "applyEqRigid" (formula "3") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "3") (term "1,0"))
(rule "add_literals" (formula "3") (term "0"))
(rule "leq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "apply_eq_monomials" (formula "7") (term "1,0") (ifseqformula "4"))
(rule "add_zero_left" (formula "7") (term "1,0,1,0"))
(rule "polySimp_mulComm0" (formula "7") (term "0,1,0"))
(rule "polySimp_mulLiterals" (formula "7") (term "0,1,0"))
(rule "polySimp_pullOutFactor0" (formula "7") (term "1,0"))
(rule "add_literals" (formula "7") (term "1,1,0"))
(rule "times_zero_1" (formula "7") (term "1,0"))
(rule "add_zero_right" (formula "7") (term "0"))
(rule "qeq_literals" (formula "7"))
(rule "true_left" (formula "7"))
(rule "applyEq" (formula "14") (term "0") (ifseqformula "4"))
(rule "leq_literals" (formula "14"))
(rule "true_left" (formula "14"))
(rule "applyEq" (formula "13") (term "0") (ifseqformula "4"))
(rule "qeq_literals" (formula "13"))
(rule "true_left" (formula "13"))
(rule "applyEq" (formula "13") (term "0,0") (ifseqformula "4"))
(rule "times_zero_2" (formula "13") (term "0"))
(rule "leq_literals" (formula "13"))
(rule "true_left" (formula "13"))
(rule "applyEq" (formula "8") (term "1,1") (ifseqformula "4"))
(rule "add_zero_right" (formula "8") (term "1"))
(rule "applyEqRigid" (formula "5") (term "0,1,0") (ifseqformula "4"))
(rule "times_zero_2" (formula "5") (term "1,0"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEqRigid" (formula "6") (term "0,0") (ifseqformula "4"))
(rule "times_zero_2" (formula "6") (term "0"))
(rule "leq_literals" (formula "6"))
(rule "true_left" (formula "6"))
(rule "applyEq" (formula "3") (term "0,1,0") (ifseqformula "1"))
(rule "mul_literals" (formula "3") (term "1,0"))
(rule "add_literals" (formula "3") (term "0"))
(rule "qeq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEq" (formula "10") (term "1,0,0,1,0") (ifseqformula "6"))
(rule "add_literals" (formula "10") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "10") (term "0,1,0"))
(rule "qeq_literals" (formula "10") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "10"))
(rule "div_literals" (formula "10") (term "0,1,0"))
(rule "mul_literals" (formula "10") (term "1,0"))
(rule "polySimp_addComm1" (formula "10") (term "0"))
(rule "add_literals" (formula "10") (term "0,0"))
(rule "applyEq" (formula "5") (term "1,0,0") (ifseqformula "6"))
(rule "add_literals" (formula "5") (term "0,0"))
(rule "jdiv_axiom_inline" (formula "5") (term "0"))
(rule "div_literals" (formula "5") (term "1,0"))
(builtin "One Step Simplification" (formula "5"))
(rule "qeq_literals" (formula "5") (term "0"))
(builtin "One Step Simplification" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "2") (term "1,0") (ifseqformula "3"))
(rule "add_zero_right" (formula "2") (term "0"))
(rule "leq_literals" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "3") (term "0,0") (ifseqformula "2"))
(rule "times_zero_2" (formula "3") (term "0"))
(rule "leq_literals" (formula "3"))
(rule "true_left" (formula "3"))
(rule "applyEq" (formula "7") (term "1,0") (ifseqformula "3"))
(rule "add_literals" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
)
(branch "s1 = 0 & s2 = 1"
(rule "andLeft" (formula "1"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "1"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "1"))
(rule "leq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "6") (term "0") (ifseqformula "2"))
(rule "leq_literals" (formula "6"))
(rule "true_left" (formula "6"))
(rule "applyEq" (formula "6") (term "0,1,0,0,0") (ifseqformula "2"))
(rule "mul_literals" (formula "6") (term "1,0,0,0"))
(rule "polySimp_homoEq" (formula "6"))
(rule "polySimp_mulLiterals" (formula "6") (term "1,0"))
(rule "polySimp_addComm1" (formula "6") (term "0"))
(rule "polySimp_addComm1" (formula "6") (term "0,0,1,0,0"))
(rule "add_literals" (formula "6") (term "0,0,0,1,0,0"))
(rule "applyEq" (formula "5") (term "0") (ifseqformula "2"))
(rule "qeq_literals" (formula "5"))
(rule "true_left" (formula "5"))
(rule "applyEq" (formula "5") (term "0,1,0") (ifseqformula "2"))
(rule "mul_literals" (formula "5") (term "1,0"))
(rule "polySimp_addComm1" (formula "5") (term "0"))
(rule "polySimp_addComm1" (formula "5") (term "0,0"))
(rule "add_literals" (formula "5") (term "0,0,0"))
(rule "add_zero_left" (formula "5") (term "0,0"))
(rule "applyEq" (formula "5") (term "1,0,0,1,0") (ifseqformula "1"))
(rule "add_zero_right" (formula "5") (term "0,0,1,0"))
(rule "jdiv_axiom_inline" (formula "5") (term "0,1,0"))
(rule "qeq_literals" (formula "5") (term "0,0,1,0"))
(builtin "One Step Simplification" (formula "5"))
(rule "div_literals" (formula "5") (term "0,1,0"))
(rule "times_zero_2" (formula "5") (term "1,0"))
(rule "add_zero_right" (formula "5") (term "0"))
(rule "close" (formula "5") (ifseqformula "1"))
)
)
)
)
(branch "Case 2"
(builtin "One Step Simplification" (formula "7"))
(rule "equal_literals" (formula "7") (term "0"))
(builtin "One Step Simplification" (formula "7"))
(rule "closeTrue" (formula "7"))
)
)
}