%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : COM220_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 06:21:35 PM UTC 2026 % Result : Theorem 74.09s 10.37s % Output : Proof 105.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : COM220_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.33 % Computer : n006.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Mon May 4 19:02:30 EDT 2026 % 0.12/0.33 % CPUTime : % 0.49/0.61 ________ _____ % 0.49/0.61 ___ __ \_________(_)________________________________ % 0.49/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.49/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.49/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.49/0.61 % 0.49/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.49/0.61 (2023-06-19) % 0.49/0.61 % 0.49/0.61 (c) Philipp Rümmer, 2009-2023 % 0.49/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.49/0.61 Amanda Stjerna. % 0.49/0.61 Free software under BSD-3-Clause. % 0.49/0.61 % 0.49/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.49/0.61 % 0.49/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.62/0.63 Running up to 7 provers in parallel. % 0.62/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.62/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.62/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.62/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.62/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.62/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.62/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 6.11/1.63 Prover 1: Preprocessing ... % 6.11/1.66 Prover 4: Preprocessing ... % 6.11/1.67 Prover 5: Preprocessing ... % 6.11/1.67 Prover 6: Preprocessing ... % 6.11/1.67 Prover 3: Preprocessing ... % 6.11/1.67 Prover 2: Preprocessing ... % 6.11/1.68 Prover 0: Preprocessing ... % 16.06/2.92 Prover 1: Warning: ignoring some quantifiers % 16.06/2.96 Prover 3: Warning: ignoring some quantifiers % 16.96/3.05 Prover 3: Constructing countermodel ... % 16.96/3.06 Prover 1: Constructing countermodel ... % 16.96/3.11 Prover 6: Proving ... % 18.39/3.26 Prover 4: Warning: ignoring some quantifiers % 18.39/3.30 Prover 5: Proving ... % 19.13/3.34 Prover 4: Constructing countermodel ... % 19.96/3.42 Prover 0: Proving ... % 20.69/3.56 Prover 2: Proving ... % 73.31/10.29 Prover 2: stopped % 74.09/10.30 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 74.09/10.37 Prover 5: proved (9727ms) % 74.09/10.37 % 74.09/10.37 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 74.09/10.37 % 74.09/10.37 Prover 6: stopped % 74.09/10.37 Prover 0: stopped % 74.09/10.38 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 74.09/10.39 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 74.09/10.39 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 74.87/10.40 Prover 3: stopped % 74.87/10.41 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 75.63/10.51 Prover 7: Preprocessing ... % 76.42/10.63 Prover 13: Preprocessing ... % 76.42/10.64 Prover 10: Preprocessing ... % 76.42/10.64 Prover 11: Preprocessing ... % 76.42/10.68 Prover 8: Preprocessing ... % 78.71/10.94 Prover 8: Warning: ignoring some quantifiers % 78.71/10.96 Prover 8: Constructing countermodel ... % 78.71/10.96 Prover 7: Warning: ignoring some quantifiers % 78.71/10.97 Prover 7: Constructing countermodel ... % 78.71/10.98 Prover 10: Warning: ignoring some quantifiers % 78.71/10.99 Prover 13: Warning: ignoring some quantifiers % 78.71/10.99 Prover 10: Constructing countermodel ... % 78.71/11.01 Prover 13: Constructing countermodel ... % 79.61/11.02 Prover 11: Warning: ignoring some quantifiers % 79.61/11.03 Prover 11: Constructing countermodel ... % 104.63/14.27 Prover 10: Found proof (size 64) % 104.63/14.27 Prover 10: proved (3900ms) % 104.63/14.27 Prover 4: stopped % 104.63/14.27 Prover 8: stopped % 104.63/14.27 Prover 7: stopped % 104.63/14.28 Prover 1: stopped % 104.63/14.28 Prover 11: stopped % 104.63/14.28 Prover 13: stopped % 104.63/14.28 % 104.63/14.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 104.63/14.28 % 104.63/14.29 % SZS output start Proof for theBenchmark % 104.63/14.29 Assumptions after simplification: % 104.63/14.29 --------------------------------- % 104.63/14.29 % 104.63/14.29 (EQ-someTerm) % 105.31/14.32 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 105.31/14.32 (vsomeTerm(v1) = v2) | ~ (vsomeTerm(v0) = v2) | ~ vTerm(v1) | ~ % 105.31/14.32 vTerm(v0)) % 105.31/14.32 % 105.31/14.32 (Preservation-Iszero-IH0) % 105.31/14.32 vTerm(vt1) & ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: % 105.31/14.32 vTy] : ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ % 105.31/14.32 vTerm(v2) | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 105.31/14.32 % 105.31/14.32 (Preservation-Iszero-t1-isSomeTerm-True) % 105.31/14.32 vTerm(vt1) & vTerm(vZero) & ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: % 105.31/14.32 vOptTerm] : ? [v3: vTy] : ? [v4: vTerm] : ( ~ (vt1 = vZero) & vreduce(v1) % 105.31/14.32 = v2 & vreduce(vt1) = v0 & vsomeTerm(v4) = v2 & vIszero(vt1) = v1 & vTy(v3) % 105.31/14.32 & vOptTerm(v2) & vOptTerm(v0) & vTerm(v4) & vTerm(v1) & vptchecksimple(v1, % 105.31/14.32 v3) & visSomeTerm(v0) & ~ vptchecksimple(v4, v3) & ! [v5: vTerm] : ( ~ % 105.31/14.32 (vSucc(v5) = vt1) | ~ vTerm(v5))) % 105.31/14.32 % 105.31/14.32 (TPlus_inv2) % 105.31/14.32 vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ( ~ (vPlus(v0, % 105.31/14.32 v1) = v2) | ~ vTerm(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, vNat) | % 105.31/14.32 vptchecksimple(v1, vNat)) % 105.31/14.32 % 105.31/14.32 (Tiszero) % 105.31/14.32 vTy(vB) & vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) % 105.31/14.32 | ~ vTerm(v0) | ~ vptchecksimple(v0, vNat) | vptchecksimple(v1, vB)) % 105.31/14.32 % 105.31/14.32 (Tiszero_inv1) % 105.31/14.33 vTy(vB) & vTy(vNat) & ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) % 105.31/14.33 | ~ vTerm(v0) | ~ vptchecksimple(v1, vB) | vptchecksimple(v0, vNat)) % 105.31/14.33 % 105.31/14.33 (Tiszero_inv2) % 105.31/14.33 vTy(vB) & ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 105.31/14.33 (vIszero(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ vptchecksimple(v2, v1)) % 105.31/14.33 % 105.31/14.33 (getTerm-0) % 105.31/14.33 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 105.31/14.33 vgetTerm(v1) = v0) % 105.31/14.33 % 105.31/14.33 (isSomeTerm-1) % 105.31/14.33 ! [v0: vTerm] : ! [v1: vOptTerm] : ( ~ (vsomeTerm(v0) = v1) | ~ vTerm(v0) | % 105.31/14.33 visSomeTerm(v1)) % 105.31/14.33 % 105.31/14.33 (isSomeTerm-true-INV) % 105.31/14.33 ! [v0: vOptTerm] : ( ~ vOptTerm(v0) | ~ visSomeTerm(v0) | ? [v1: vTerm] : % 105.31/14.33 (vsomeTerm(v1) = v0 & vTerm(v1))) % 105.31/14.33 % 105.31/14.33 (reduce-16) % 105.31/14.33 vTerm(vZero) & ! [v0: vTerm] : ! [v1: vTerm] : (v0 = vZero | ~ (vIszero(v0) % 105.31/14.33 = v1) | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: vOptTerm] : ? [v4: % 105.31/14.33 vTerm] : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 105.31/14.33 vTerm] : (vTerm(v7) & ((v8 = v0 & vSucc(v7) = v0) | (vreduce(v0) = v2 & % 105.31/14.33 vOptTerm(v2) & ( ~ visSomeTerm(v2) | (v6 = v3 & vreduce(v1) = v3 & % 105.31/14.33 vgetTerm(v2) = v4 & vsomeTerm(v5) = v3 & vIszero(v4) = v5 & % 105.31/14.33 vOptTerm(v3) & vTerm(v5) & vTerm(v4))))))) % 105.31/14.33 % 105.31/14.33 (function-axioms) % 105.31/14.34 ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : ! [v4: % 105.31/14.34 vTerm] : (v1 = v0 | ~ (vIfelse(v4, v3, v2) = v1) | ~ (vIfelse(v4, v3, v2) % 105.31/14.34 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] % 105.31/14.34 : (v1 = v0 | ~ (vplusop(v3, v2) = v1) | ~ (vplusop(v3, v2) = v0)) & ! [v0: % 105.31/14.34 vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : ! [v3: vTerm] : (v1 = v0 | ~ % 105.31/14.34 (vPlus(v3, v2) = v1) | ~ (vPlus(v3, v2) = v0)) & ! [v0: vOptTerm] : ! % 105.31/14.34 [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vreduce(v2) = v1) | ~ % 105.31/14.34 (vreduce(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : % 105.31/14.34 (v1 = v0 | ~ (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) & ! [v0: % 105.31/14.34 vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 105.31/14.34 (vsomeTerm(v2) = v1) | ~ (vsomeTerm(v2) = v0)) & ! [v0: vTerm] : ! [v1: % 105.31/14.34 vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ (vIszero(v2) = v1) | ~ (vIszero(v2) % 105.31/14.34 = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 105.31/14.34 (vPred(v2) = v1) | ~ (vPred(v2) = v0)) & ! [v0: vTerm] : ! [v1: vTerm] : % 105.31/14.34 ! [v2: vTerm] : (v1 = v0 | ~ (vSucc(v2) = v1) | ~ (vSucc(v2) = v0)) % 105.31/14.34 % 105.31/14.34 Further assumptions not needed in the proof: % 105.31/14.34 -------------------------------------------- % 105.31/14.34 DIFF-B-Nat, DIFF-False-Ifelse, DIFF-False-Iszero, DIFF-False-Plus, % 105.31/14.34 DIFF-False-Pred, DIFF-False-Succ, DIFF-False-Zero, DIFF-Ifelse-Iszero, % 105.31/14.34 DIFF-Ifelse-Plus, DIFF-Ifelse-Pred, DIFF-Ifelse-Succ, DIFF-Ifelse-Zero, % 105.31/14.34 DIFF-Iszero-Plus, DIFF-Pred-Iszero, DIFF-Pred-Plus, DIFF-Succ-Iszero, % 105.31/14.34 DIFF-Succ-Plus, DIFF-Succ-Pred, DIFF-True-False, DIFF-True-Ifelse, % 105.31/14.34 DIFF-True-Iszero, DIFF-True-Plus, DIFF-True-Pred, DIFF-True-Succ, % 105.31/14.34 DIFF-True-Zero, DIFF-Zero-Iszero, DIFF-Zero-Plus, DIFF-Zero-Pred, % 105.31/14.34 DIFF-Zero-Succ, DIFF-noTerm-someTerm, EQ-Ifelse, EQ-Iszero, EQ-Plus, EQ-Pred, % 105.31/14.34 EQ-Succ, TPlus, TPlus_inv0, TPlus_inv1, TPred, TPred_inv1, TPred_inv2, TSucc, % 105.31/14.34 TSucc_inv1, TSucc_inv2, TZero, TZero_inv, Tfalse, Tif, Tif_inv1, Tif_inv2, % 105.31/14.34 Tif_inv3, Ttrue, dom-OptTerm, dom-Term, dom-Ty, isNV-0, isNV-1, isNV-2, % 105.31/14.34 isNV-false-INV, isNV-true-INV, isSomeTerm-0, isSomeTerm-false-INV, isValue-0, % 105.31/14.34 isValue-1, isValue-2, isValue-false-INV, isValue-true-INV, plusop-0, plusop-1, % 105.31/14.34 plusop-2, plusop-INV, reduce-0, reduce-1, reduce-10, reduce-11, reduce-12, % 105.31/14.34 reduce-13, reduce-14, reduce-15, reduce-17, reduce-18, reduce-19, reduce-2, % 105.31/14.34 reduce-20, reduce-21, reduce-22, reduce-23, reduce-3, reduce-4, reduce-5, % 105.31/14.34 reduce-6, reduce-7, reduce-8, reduce-9, reduce-INV % 105.31/14.34 % 105.31/14.34 Those formulas are unsatisfiable: % 105.31/14.34 --------------------------------- % 105.31/14.34 % 105.31/14.34 Begin of proof % 105.31/14.34 | % 105.31/14.34 | ALPHA: (reduce-16) implies: % 105.31/14.34 | (1) ! [v0: vTerm] : ! [v1: vTerm] : (v0 = vZero | ~ (vIszero(v0) = v1) | % 105.31/14.34 | ~ vTerm(v0) | ? [v2: vOptTerm] : ? [v3: vOptTerm] : ? [v4: vTerm] % 105.31/14.34 | : ? [v5: vTerm] : ? [v6: vOptTerm] : ? [v7: vTerm] : ? [v8: % 105.31/14.34 | vTerm] : (vTerm(v7) & ((v8 = v0 & vSucc(v7) = v0) | (vreduce(v0) = % 105.31/14.34 | v2 & vOptTerm(v2) & ( ~ visSomeTerm(v2) | (v6 = v3 & % 105.31/14.34 | vreduce(v1) = v3 & vgetTerm(v2) = v4 & vsomeTerm(v5) = v3 & % 105.31/14.34 | vIszero(v4) = v5 & vOptTerm(v3) & vTerm(v5) & % 105.31/14.34 | vTerm(v4))))))) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (Tiszero) implies: % 105.31/14.34 | (2) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | ~ vTerm(v0) % 105.31/14.34 | | ~ vptchecksimple(v0, vNat) | vptchecksimple(v1, vB)) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (Tiszero_inv1) implies: % 105.31/14.34 | (3) ! [v0: vTerm] : ! [v1: vTerm] : ( ~ (vIszero(v0) = v1) | ~ vTerm(v0) % 105.31/14.34 | | ~ vptchecksimple(v1, vB) | vptchecksimple(v0, vNat)) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (Tiszero_inv2) implies: % 105.31/14.34 | (4) ! [v0: vTerm] : ! [v1: vTy] : ! [v2: vTerm] : (v1 = vB | ~ % 105.31/14.34 | (vIszero(v0) = v2) | ~ vTy(v1) | ~ vTerm(v0) | ~ % 105.31/14.34 | vptchecksimple(v2, v1)) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (TPlus_inv2) implies: % 105.31/14.34 | (5) vTy(vNat) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (Preservation-Iszero-IH0) implies: % 105.31/14.34 | (6) ? [v0: vOptTerm] : (vreduce(vt1) = v0 & vOptTerm(v0) & ! [v1: vTy] : % 105.31/14.34 | ! [v2: vTerm] : ( ~ (vsomeTerm(v2) = v0) | ~ vTy(v1) | ~ vTerm(v2) % 105.31/14.34 | | ~ vptchecksimple(vt1, v1) | vptchecksimple(v2, v1))) % 105.31/14.34 | % 105.31/14.34 | ALPHA: (Preservation-Iszero-t1-isSomeTerm-True) implies: % 105.31/14.35 | (7) vTerm(vt1) % 105.31/14.35 | (8) ? [v0: vOptTerm] : ? [v1: vTerm] : ? [v2: vOptTerm] : ? [v3: vTy] : % 105.31/14.35 | ? [v4: vTerm] : ( ~ (vt1 = vZero) & vreduce(v1) = v2 & vreduce(vt1) = % 105.31/14.35 | v0 & vsomeTerm(v4) = v2 & vIszero(vt1) = v1 & vTy(v3) & vOptTerm(v2) % 105.31/14.35 | & vOptTerm(v0) & vTerm(v4) & vTerm(v1) & vptchecksimple(v1, v3) & % 105.31/14.35 | visSomeTerm(v0) & ~ vptchecksimple(v4, v3) & ! [v5: vTerm] : ( ~ % 105.31/14.35 | (vSucc(v5) = vt1) | ~ vTerm(v5))) % 105.31/14.35 | % 105.31/14.35 | ALPHA: (function-axioms) implies: % 105.31/14.35 | (9) ! [v0: vTerm] : ! [v1: vTerm] : ! [v2: vOptTerm] : (v1 = v0 | ~ % 105.31/14.35 | (vgetTerm(v2) = v1) | ~ (vgetTerm(v2) = v0)) % 105.31/14.35 | (10) ! [v0: vOptTerm] : ! [v1: vOptTerm] : ! [v2: vTerm] : (v1 = v0 | ~ % 105.31/14.35 | (vreduce(v2) = v1) | ~ (vreduce(v2) = v0)) % 105.31/14.35 | % 105.31/14.35 | DELTA: instantiating (6) with fresh symbol all_100_0 gives: % 105.31/14.35 | (11) vreduce(vt1) = all_100_0 & vOptTerm(all_100_0) & ! [v0: vTy] : ! % 105.31/14.35 | [v1: vTerm] : ( ~ (vsomeTerm(v1) = all_100_0) | ~ vTy(v0) | ~ % 105.31/14.35 | vTerm(v1) | ~ vptchecksimple(vt1, v0) | vptchecksimple(v1, v0)) % 105.31/14.35 | % 105.31/14.35 | ALPHA: (11) implies: % 105.31/14.35 | (12) vreduce(vt1) = all_100_0 % 105.31/14.35 | (13) ! [v0: vTy] : ! [v1: vTerm] : ( ~ (vsomeTerm(v1) = all_100_0) | ~ % 105.31/14.35 | vTy(v0) | ~ vTerm(v1) | ~ vptchecksimple(vt1, v0) | % 105.31/14.35 | vptchecksimple(v1, v0)) % 105.31/14.35 | % 105.31/14.35 | DELTA: instantiating (8) with fresh symbols all_107_0, all_107_1, all_107_2, % 105.31/14.35 | all_107_3, all_107_4 gives: % 105.31/14.35 | (14) ~ (vt1 = vZero) & vreduce(all_107_3) = all_107_2 & vreduce(vt1) = % 105.31/14.35 | all_107_4 & vsomeTerm(all_107_0) = all_107_2 & vIszero(vt1) = % 105.31/14.35 | all_107_3 & vTy(all_107_1) & vOptTerm(all_107_2) & vOptTerm(all_107_4) % 105.31/14.35 | & vTerm(all_107_0) & vTerm(all_107_3) & vptchecksimple(all_107_3, % 105.31/14.35 | all_107_1) & visSomeTerm(all_107_4) & ~ vptchecksimple(all_107_0, % 105.31/14.35 | all_107_1) & ! [v0: vTerm] : ( ~ (vSucc(v0) = vt1) | ~ vTerm(v0)) % 105.31/14.35 | % 105.31/14.35 | ALPHA: (14) implies: % 105.31/14.35 | (15) ~ (vt1 = vZero) % 105.31/14.35 | (16) ~ vptchecksimple(all_107_0, all_107_1) % 105.31/14.35 | (17) visSomeTerm(all_107_4) % 105.31/14.35 | (18) vptchecksimple(all_107_3, all_107_1) % 105.31/14.35 | (19) vTerm(all_107_0) % 105.31/14.35 | (20) vOptTerm(all_107_4) % 105.31/14.35 | (21) vOptTerm(all_107_2) % 105.31/14.35 | (22) vTy(all_107_1) % 105.31/14.35 | (23) vIszero(vt1) = all_107_3 % 105.31/14.35 | (24) vsomeTerm(all_107_0) = all_107_2 % 105.31/14.35 | (25) vreduce(vt1) = all_107_4 % 105.31/14.35 | (26) vreduce(all_107_3) = all_107_2 % 105.31/14.35 | (27) ! [v0: vTerm] : ( ~ (vSucc(v0) = vt1) | ~ vTerm(v0)) % 105.31/14.35 | % 105.31/14.35 | GROUND_INST: instantiating (10) with all_100_0, all_107_4, vt1, simplifying % 105.31/14.35 | with (12), (25) gives: % 105.31/14.35 | (28) all_107_4 = all_100_0 % 105.31/14.36 | % 105.31/14.36 | REDUCE: (20), (28) imply: % 105.31/14.36 | (29) vOptTerm(all_100_0) % 105.31/14.36 | % 105.31/14.36 | REDUCE: (17), (28) imply: % 105.31/14.36 | (30) visSomeTerm(all_100_0) % 105.31/14.36 | % 105.31/14.36 | GROUND_INST: instantiating (isSomeTerm-true-INV) with all_100_0, simplifying % 105.31/14.36 | with (29), (30) gives: % 105.31/14.36 | (31) ? [v0: vTerm] : (vsomeTerm(v0) = all_100_0 & vTerm(v0)) % 105.31/14.36 | % 105.31/14.36 | GROUND_INST: instantiating (4) with vt1, all_107_1, all_107_3, simplifying % 105.31/14.36 | with (7), (18), (22), (23) gives: % 105.31/14.36 | (32) all_107_1 = vB % 105.31/14.36 | % 105.31/14.36 | GROUND_INST: instantiating (1) with vt1, all_107_3, simplifying with (7), (23) % 105.31/14.36 | gives: % 105.31/14.36 | (33) vt1 = vZero | ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : % 105.31/14.36 | ? [v3: vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : % 105.31/14.36 | (vTerm(v5) & ((v6 = vt1 & vSucc(v5) = vt1) | (vreduce(vt1) = v0 & % 105.31/14.36 | vOptTerm(v0) & ( ~ visSomeTerm(v0) | (v4 = v1 & % 105.31/14.36 | vreduce(all_107_3) = v1 & vgetTerm(v0) = v2 & vsomeTerm(v3) % 105.31/14.36 | = v1 & vIszero(v2) = v3 & vOptTerm(v1) & vTerm(v3) & % 105.31/14.36 | vTerm(v2)))))) % 105.31/14.36 | % 105.31/14.36 | GROUND_INST: instantiating (isSomeTerm-1) with all_107_0, all_107_2, % 105.31/14.36 | simplifying with (19), (24) gives: % 105.31/14.36 | (34) visSomeTerm(all_107_2) % 105.31/14.36 | % 105.31/14.36 | DELTA: instantiating (31) with fresh symbol all_127_0 gives: % 105.31/14.36 | (35) vsomeTerm(all_127_0) = all_100_0 & vTerm(all_127_0) % 105.31/14.36 | % 105.31/14.36 | ALPHA: (35) implies: % 105.31/14.36 | (36) vTerm(all_127_0) % 105.31/14.36 | (37) vsomeTerm(all_127_0) = all_100_0 % 105.31/14.36 | % 105.31/14.36 | REDUCE: (18), (32) imply: % 105.31/14.36 | (38) vptchecksimple(all_107_3, vB) % 105.31/14.36 | % 105.31/14.36 | REDUCE: (16), (32) imply: % 105.31/14.36 | (39) ~ vptchecksimple(all_107_0, vB) % 105.31/14.36 | % 105.31/14.36 | BETA: splitting (33) gives: % 105.31/14.36 | % 105.31/14.36 | Case 1: % 105.31/14.36 | | % 105.31/14.36 | | (40) vt1 = vZero % 105.31/14.36 | | % 105.31/14.36 | | REDUCE: (15), (40) imply: % 105.31/14.36 | | (41) $false % 105.31/14.36 | | % 105.31/14.36 | | CLOSE: (41) is inconsistent. % 105.31/14.36 | | % 105.31/14.36 | Case 2: % 105.31/14.36 | | % 105.31/14.36 | | (42) ? [v0: vOptTerm] : ? [v1: vOptTerm] : ? [v2: vTerm] : ? [v3: % 105.31/14.36 | | vTerm] : ? [v4: vOptTerm] : ? [v5: vTerm] : ? [v6: vTerm] : % 105.31/14.36 | | (vTerm(v5) & ((v6 = vt1 & vSucc(v5) = vt1) | (vreduce(vt1) = v0 & % 105.31/14.36 | | vOptTerm(v0) & ( ~ visSomeTerm(v0) | (v4 = v1 & % 105.31/14.36 | | vreduce(all_107_3) = v1 & vgetTerm(v0) = v2 & % 105.31/14.36 | | vsomeTerm(v3) = v1 & vIszero(v2) = v3 & vOptTerm(v1) & % 105.31/14.36 | | vTerm(v3) & vTerm(v2)))))) % 105.31/14.36 | | % 105.31/14.36 | | DELTA: instantiating (42) with fresh symbols all_143_0, all_143_1, % 105.31/14.36 | | all_143_2, all_143_3, all_143_4, all_143_5, all_143_6 gives: % 105.31/14.36 | | (43) vTerm(all_143_1) & ((all_143_0 = vt1 & vSucc(all_143_1) = vt1) | % 105.31/14.36 | | (vreduce(vt1) = all_143_6 & vOptTerm(all_143_6) & ( ~ % 105.31/14.36 | | visSomeTerm(all_143_6) | (all_143_2 = all_143_5 & % 105.31/14.36 | | vreduce(all_107_3) = all_143_5 & vgetTerm(all_143_6) = % 105.31/14.36 | | all_143_4 & vsomeTerm(all_143_3) = all_143_5 & % 105.31/14.36 | | vIszero(all_143_4) = all_143_3 & vOptTerm(all_143_5) & % 105.31/14.36 | | vTerm(all_143_3) & vTerm(all_143_4))))) % 105.31/14.36 | | % 105.31/14.36 | | ALPHA: (43) implies: % 105.31/14.37 | | (44) vTerm(all_143_1) % 105.31/14.37 | | (45) (all_143_0 = vt1 & vSucc(all_143_1) = vt1) | (vreduce(vt1) = % 105.31/14.37 | | all_143_6 & vOptTerm(all_143_6) & ( ~ visSomeTerm(all_143_6) | % 105.31/14.37 | | (all_143_2 = all_143_5 & vreduce(all_107_3) = all_143_5 & % 105.31/14.37 | | vgetTerm(all_143_6) = all_143_4 & vsomeTerm(all_143_3) = % 105.31/14.37 | | all_143_5 & vIszero(all_143_4) = all_143_3 & % 105.31/14.37 | | vOptTerm(all_143_5) & vTerm(all_143_3) & vTerm(all_143_4)))) % 105.31/14.37 | | % 105.31/14.37 | | GROUND_INST: instantiating (isSomeTerm-true-INV) with all_107_2, simplifying % 105.31/14.37 | | with (21), (34) gives: % 105.31/14.37 | | (46) ? [v0: vTerm] : (vsomeTerm(v0) = all_107_2 & vTerm(v0)) % 105.31/14.37 | | % 105.31/14.37 | | GROUND_INST: instantiating (3) with vt1, all_107_3, simplifying with (7), % 105.31/14.37 | | (23), (38) gives: % 105.31/14.37 | | (47) vptchecksimple(vt1, vNat) % 105.31/14.37 | | % 105.31/14.37 | | GROUND_INST: instantiating (getTerm-0) with all_127_0, all_100_0, % 105.31/14.37 | | simplifying with (36), (37) gives: % 105.31/14.37 | | (48) vgetTerm(all_100_0) = all_127_0 % 105.31/14.37 | | % 105.31/14.37 | | DELTA: instantiating (46) with fresh symbol all_151_0 gives: % 105.31/14.37 | | (49) vsomeTerm(all_151_0) = all_107_2 & vTerm(all_151_0) % 105.31/14.37 | | % 105.31/14.37 | | ALPHA: (49) implies: % 105.31/14.37 | | (50) vTerm(all_151_0) % 105.31/14.37 | | (51) vsomeTerm(all_151_0) = all_107_2 % 105.31/14.37 | | % 105.31/14.37 | | GROUND_INST: instantiating (13) with vNat, all_127_0, simplifying with (5), % 105.31/14.37 | | (36), (37), (47) gives: % 105.31/14.37 | | (52) vptchecksimple(all_127_0, vNat) % 105.31/14.37 | | % 105.31/14.37 | | GROUND_INST: instantiating (EQ-someTerm) with all_107_0, all_151_0, % 105.31/14.37 | | all_107_2, simplifying with (19), (24), (50), (51) gives: % 105.31/14.37 | | (53) all_151_0 = all_107_0 % 105.31/14.37 | | % 105.31/14.37 | | BETA: splitting (45) gives: % 105.31/14.37 | | % 105.31/14.37 | | Case 1: % 105.31/14.37 | | | % 105.31/14.37 | | | (54) all_143_0 = vt1 & vSucc(all_143_1) = vt1 % 105.31/14.37 | | | % 105.31/14.37 | | | ALPHA: (54) implies: % 105.31/14.37 | | | (55) vSucc(all_143_1) = vt1 % 105.31/14.37 | | | % 105.31/14.37 | | | GROUND_INST: instantiating (27) with all_143_1, simplifying with (44), % 105.31/14.37 | | | (55) gives: % 105.31/14.37 | | | (56) $false % 105.31/14.37 | | | % 105.31/14.37 | | | CLOSE: (56) is inconsistent. % 105.31/14.37 | | | % 105.31/14.37 | | Case 2: % 105.31/14.37 | | | % 105.31/14.37 | | | (57) vreduce(vt1) = all_143_6 & vOptTerm(all_143_6) & ( ~ % 105.31/14.37 | | | visSomeTerm(all_143_6) | (all_143_2 = all_143_5 & % 105.31/14.37 | | | vreduce(all_107_3) = all_143_5 & vgetTerm(all_143_6) = % 105.31/14.37 | | | all_143_4 & vsomeTerm(all_143_3) = all_143_5 & % 105.31/14.37 | | | vIszero(all_143_4) = all_143_3 & vOptTerm(all_143_5) & % 105.31/14.37 | | | vTerm(all_143_3) & vTerm(all_143_4))) % 105.31/14.37 | | | % 105.31/14.37 | | | ALPHA: (57) implies: % 105.31/14.37 | | | (58) vreduce(vt1) = all_143_6 % 105.31/14.37 | | | (59) ~ visSomeTerm(all_143_6) | (all_143_2 = all_143_5 & % 105.31/14.37 | | | vreduce(all_107_3) = all_143_5 & vgetTerm(all_143_6) = all_143_4 % 105.31/14.37 | | | & vsomeTerm(all_143_3) = all_143_5 & vIszero(all_143_4) = % 105.31/14.37 | | | all_143_3 & vOptTerm(all_143_5) & vTerm(all_143_3) & % 105.31/14.37 | | | vTerm(all_143_4)) % 105.31/14.37 | | | % 105.31/14.37 | | | GROUND_INST: instantiating (10) with all_100_0, all_143_6, vt1, % 105.31/14.37 | | | simplifying with (12), (58) gives: % 105.31/14.37 | | | (60) all_143_6 = all_100_0 % 105.31/14.37 | | | % 105.31/14.37 | | | BETA: splitting (59) gives: % 105.31/14.37 | | | % 105.31/14.37 | | | Case 1: % 105.31/14.37 | | | | % 105.31/14.37 | | | | (61) ~ visSomeTerm(all_143_6) % 105.31/14.37 | | | | % 105.31/14.37 | | | | REDUCE: (60), (61) imply: % 105.31/14.37 | | | | (62) ~ visSomeTerm(all_100_0) % 105.31/14.37 | | | | % 105.31/14.37 | | | | PRED_UNIFY: (30), (62) imply: % 105.31/14.37 | | | | (63) $false % 105.31/14.37 | | | | % 105.31/14.37 | | | | CLOSE: (63) is inconsistent. % 105.31/14.37 | | | | % 105.31/14.37 | | | Case 2: % 105.31/14.37 | | | | % 105.31/14.37 | | | | (64) all_143_2 = all_143_5 & vreduce(all_107_3) = all_143_5 & % 105.31/14.37 | | | | vgetTerm(all_143_6) = all_143_4 & vsomeTerm(all_143_3) = % 105.31/14.37 | | | | all_143_5 & vIszero(all_143_4) = all_143_3 & vOptTerm(all_143_5) % 105.31/14.37 | | | | & vTerm(all_143_3) & vTerm(all_143_4) % 105.31/14.37 | | | | % 105.31/14.37 | | | | ALPHA: (64) implies: % 105.31/14.37 | | | | (65) vTerm(all_143_4) % 105.31/14.37 | | | | (66) vTerm(all_143_3) % 105.31/14.37 | | | | (67) vIszero(all_143_4) = all_143_3 % 105.31/14.37 | | | | (68) vsomeTerm(all_143_3) = all_143_5 % 105.31/14.38 | | | | (69) vgetTerm(all_143_6) = all_143_4 % 105.31/14.38 | | | | (70) vreduce(all_107_3) = all_143_5 % 105.31/14.38 | | | | % 105.31/14.38 | | | | REDUCE: (60), (69) imply: % 105.31/14.38 | | | | (71) vgetTerm(all_100_0) = all_143_4 % 105.31/14.38 | | | | % 105.31/14.38 | | | | GROUND_INST: instantiating (9) with all_127_0, all_143_4, all_100_0, % 105.31/14.38 | | | | simplifying with (48), (71) gives: % 105.31/14.38 | | | | (72) all_143_4 = all_127_0 % 105.31/14.38 | | | | % 105.31/14.38 | | | | GROUND_INST: instantiating (10) with all_107_2, all_143_5, all_107_3, % 105.31/14.38 | | | | simplifying with (26), (70) gives: % 105.31/14.38 | | | | (73) all_143_5 = all_107_2 % 105.31/14.38 | | | | % 105.31/14.38 | | | | REDUCE: (68), (73) imply: % 105.31/14.38 | | | | (74) vsomeTerm(all_143_3) = all_107_2 % 105.31/14.38 | | | | % 105.31/14.38 | | | | REDUCE: (67), (72) imply: % 105.31/14.38 | | | | (75) vIszero(all_127_0) = all_143_3 % 105.31/14.38 | | | | % 105.31/14.38 | | | | GROUND_INST: instantiating (2) with all_127_0, all_143_3, simplifying % 105.31/14.38 | | | | with (36), (52), (75) gives: % 105.31/14.38 | | | | (76) vptchecksimple(all_143_3, vB) % 105.31/14.38 | | | | % 105.31/14.38 | | | | GROUND_INST: instantiating (EQ-someTerm) with all_107_0, all_143_3, % 105.31/14.38 | | | | all_107_2, simplifying with (19), (24), (66), (74) gives: % 105.31/14.38 | | | | (77) all_143_3 = all_107_0 % 105.31/14.38 | | | | % 105.31/14.38 | | | | REDUCE: (76), (77) imply: % 105.31/14.38 | | | | (78) vptchecksimple(all_107_0, vB) % 105.31/14.38 | | | | % 105.31/14.38 | | | | PRED_UNIFY: (39), (78) imply: % 105.31/14.38 | | | | (79) $false % 105.31/14.38 | | | | % 105.31/14.38 | | | | CLOSE: (79) is inconsistent. % 105.31/14.38 | | | | % 105.31/14.38 | | | End of split % 105.31/14.38 | | | % 105.31/14.38 | | End of split % 105.31/14.38 | | % 105.31/14.38 | End of split % 105.31/14.38 | % 105.31/14.38 End of proof % 105.31/14.38 % SZS output end Proof for theBenchmark % 105.31/14.38 % 105.31/14.38 13768ms %------------------------------------------------------------------------------