%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWX207+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 : n029.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 07:05:45 PM UTC 2026 % Result : Theorem 14.96s 2.72s % Output : Proof 21.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX207+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.15/0.33 % Computer : n029.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 11:35:29 EDT 2026 % 0.15/0.34 % CPUTime : % 0.51/0.61 ________ _____ % 0.51/0.61 ___ __ \_________(_)________________________________ % 0.51/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.51/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.51/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.51/0.61 % 0.51/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.51/0.61 (2023-06-19) % 0.51/0.61 % 0.51/0.61 (c) Philipp Rümmer, 2009-2023 % 0.51/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.51/0.61 Amanda Stjerna. % 0.51/0.61 Free software under BSD-3-Clause. % 0.51/0.61 % 0.51/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.51/0.61 % 0.51/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.51/0.62 Running up to 7 provers in parallel. % 0.71/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.71/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.71/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.71/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.71/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.71/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.71/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 1.71/0.99 Prover 4: Preprocessing ... % 1.71/1.00 Prover 1: Preprocessing ... % 2.53/1.04 Prover 3: Preprocessing ... % 2.53/1.04 Prover 6: Preprocessing ... % 2.53/1.04 Prover 5: Preprocessing ... % 2.53/1.04 Prover 0: Preprocessing ... % 2.53/1.04 Prover 2: Preprocessing ... % 4.50/1.33 Prover 1: Constructing countermodel ... % 4.50/1.34 Prover 3: Constructing countermodel ... % 4.50/1.34 Prover 6: Proving ... % 4.50/1.37 Prover 4: Constructing countermodel ... % 4.50/1.39 Prover 0: Proving ... % 5.25/1.41 Prover 5: Proving ... % 5.25/1.47 Prover 3: gave up % 5.25/1.47 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 5.25/1.48 Prover 2: Proving ... % 5.94/1.50 Prover 7: Preprocessing ... % 5.94/1.55 Prover 1: gave up % 5.94/1.55 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 5.94/1.58 Prover 8: Preprocessing ... % 6.64/1.60 Prover 7: Constructing countermodel ... % 7.39/1.70 Prover 8: Warning: ignoring some quantifiers % 7.39/1.71 Prover 8: Constructing countermodel ... % 8.86/1.97 Prover 8: gave up % 9.69/2.03 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 9.69/2.04 Prover 9: Preprocessing ... % 10.49/2.14 Prover 9: Constructing countermodel ... % 14.96/2.71 Prover 0: proved (2088ms) % 14.96/2.72 % 14.96/2.72 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.96/2.72 % 14.96/2.72 Prover 9: stopped % 14.96/2.72 Prover 6: stopped % 14.96/2.72 Prover 2: stopped % 14.96/2.72 Prover 5: stopped % 14.96/2.72 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 14.96/2.72 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.96/2.72 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.96/2.72 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.96/2.72 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 14.96/2.74 Prover 11: Preprocessing ... % 14.96/2.74 Prover 13: Preprocessing ... % 14.96/2.74 Prover 10: Preprocessing ... % 14.96/2.76 Prover 19: Preprocessing ... % 14.96/2.76 Prover 16: Preprocessing ... % 15.74/2.80 Prover 11: Constructing countermodel ... % 15.74/2.81 Prover 16: Warning: ignoring some quantifiers % 15.74/2.81 Prover 16: Constructing countermodel ... % 15.74/2.83 Prover 19: Warning: ignoring some quantifiers % 15.74/2.84 Prover 19: Constructing countermodel ... % 15.74/2.85 Prover 10: Constructing countermodel ... % 15.74/2.87 Prover 13: Warning: ignoring some quantifiers % 15.74/2.87 Prover 13: Constructing countermodel ... % 16.52/2.93 Prover 10: gave up % 17.32/3.04 Prover 19: gave up % 17.32/3.11 Prover 13: gave up % 18.66/3.20 Prover 16: gave up % 21.09/3.63 Prover 4: Found proof (size 96) % 21.09/3.63 Prover 4: proved (2993ms) % 21.09/3.63 Prover 7: stopped % 21.09/3.63 Prover 11: stopped % 21.09/3.63 % 21.09/3.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 21.09/3.63 % 21.09/3.65 % SZS output start Proof for theBenchmark % 21.09/3.65 Assumptions after simplification: % 21.09/3.65 --------------------------------- % 21.09/3.65 % 21.09/3.65 (axiom_014) % 21.09/3.66 ~ (pB = pA) & $i(pB) & $i(pA) % 21.09/3.66 % 21.09/3.66 (axiom_017) % 21.09/3.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (c2(v0, v1) = v2) | ~ $i(v1) | % 21.09/3.68 ~ $i(v0) | proj1C(v2) = v0) % 21.09/3.68 % 21.09/3.68 (axiom_019) % 21.09/3.68 $i(nil) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (append(nil, v0) = v1) | % 21.09/3.68 ~ $i(v0)) % 21.09/3.68 % 21.09/3.68 (axiom_020) % 21.09/3.68 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 21.09/3.68 (append(v3, v0) = v4) | ~ (cons(v1, v2) = v3) | ~ $i(v2) | ~ $i(v1) | ~ % 21.09/3.68 $i(v0) | ? [v5: $i] : (append(v2, v0) = v5 & cons(v1, v5) = v4 & $i(v5) & % 21.09/3.68 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: % 21.09/3.68 $i] : ( ~ (append(v2, v0) = v3) | ~ (cons(v1, v3) = v4) | ~ $i(v2) | ~ % 21.09/3.68 $i(v1) | ~ $i(v0) | ? [v5: $i] : (append(v5, v0) = v4 & cons(v1, v2) = v5 % 21.09/3.68 & $i(v5) & $i(v4))) % 21.09/3.68 % 21.09/3.68 (axiom_021) % 21.09/3.69 $i(a) & $i(nil) & ? [v0: $i] : (cons(a, nil) = v0 & $i(v0) & ! [v1: $i] : ! % 21.09/3.69 [v2: $i] : ( ~ (linP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? % 21.09/3.69 [v5: $i] : (linP(v3) = v4 & append(v2, v0) = v5 & append(v0, v5) = v4 & % 21.09/3.69 aP(v1) = v3 & $i(v5) & $i(v4) & $i(v3))) & ! [v1: $i] : ! [v2: $i] : ( % 21.09/3.69 ~ (aP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 21.09/3.69 (linP(v2) = v3 & linP(v1) = v4 & append(v4, v0) = v5 & append(v0, v5) = v3 % 21.09/3.69 & $i(v5) & $i(v4) & $i(v3)))) % 21.09/3.69 % 21.09/3.69 (axiom_022) % 21.09/3.69 $i(b) & $i(nil) & ? [v0: $i] : (cons(b, nil) = v0 & $i(v0) & ! [v1: $i] : ! % 21.09/3.69 [v2: $i] : ( ~ (linP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? % 21.09/3.69 [v5: $i] : (linP(v3) = v4 & append(v2, v0) = v5 & append(v0, v5) = v4 & % 21.09/3.69 bP(v1) = v3 & $i(v5) & $i(v4) & $i(v3))) & ! [v1: $i] : ! [v2: $i] : ( % 21.09/3.69 ~ (bP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 21.09/3.69 (linP(v2) = v3 & linP(v1) = v4 & append(v4, v0) = v5 & append(v0, v5) = v3 % 21.09/3.69 & $i(v5) & $i(v4) & $i(v3)))) % 21.09/3.69 % 21.09/3.69 (axiom_023) % 21.09/3.69 $i(pA) & $i(a) & $i(nil) & ? [v0: $i] : (linP(pA) = v0 & cons(a, nil) = v0 & % 21.09/3.69 $i(v0)) % 21.09/3.69 % 21.09/3.69 (axiom_024) % 21.09/3.69 $i(pB) & $i(b) & $i(nil) & ? [v0: $i] : (linP(pB) = v0 & cons(b, nil) = v0 & % 21.09/3.69 $i(v0)) % 21.09/3.69 % 21.09/3.69 (axiom_025) % 21.09/3.69 linP(pE) = nil & $i(pE) & $i(nil) % 21.09/3.70 % 21.09/3.70 (axiom_026) % 21.62/3.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 21.62/3.70 (linP(v1) = v3) | ~ (linP(v0) = v2) | ~ (append(v2, v3) = v4) | ~ $i(v1) % 21.62/3.70 | ~ $i(v0) | ? [v5: $i] : (linC(v5) = v4 & c2(v0, v1) = v5 & $i(v5) & % 21.62/3.70 $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (c2(v0, v1) = v2) % 21.62/3.70 | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 21.62/3.70 (linC(v2) = v3 & linP(v1) = v5 & linP(v0) = v4 & append(v4, v5) = v3 & % 21.62/3.70 $i(v5) & $i(v4) & $i(v3))) % 21.62/3.70 % 21.62/3.70 (goal_027) % 21.62/3.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (linC(v1) = v2) | ~ % 21.62/3.70 (linC(v0) = v2) | ~ $i(v1) | ~ $i(v0)) % 21.62/3.70 % 21.62/3.70 (function-axioms) % 21.62/3.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.62/3.70 (append(v3, v2) = v1) | ~ (append(v3, v2) = v0)) & ! [v0: $i] : ! [v1: % 21.62/3.70 $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (c2(v3, v2) = v1) | ~ % 21.62/3.70 (c2(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : % 21.62/3.70 (v1 = v0 | ~ (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) & ! [v0: $i] : ! % 21.62/3.70 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (linC(v2) = v1) | ~ (linC(v2) = v0)) & % 21.62/3.70 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (linP(v2) = v1) | ~ % 21.62/3.70 (linP(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 21.62/3.70 (proj2C(v2) = v1) | ~ (proj2C(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 21.62/3.70 [v2: $i] : (v1 = v0 | ~ (proj1C(v2) = v1) | ~ (proj1C(v2) = v0)) & ! [v0: % 21.62/3.70 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (bP(v2) = v1) | ~ (bP(v2) = % 21.62/3.70 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 21.62/3.71 (proj1BP(v2) = v1) | ~ (proj1BP(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 21.62/3.71 [v2: $i] : (v1 = v0 | ~ (aP(v2) = v1) | ~ (aP(v2) = v0)) & ! [v0: $i] : ! % 21.62/3.71 [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (proj1AP(v2) = v1) | ~ (proj1AP(v2) = % 21.62/3.71 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (tail(v2) = % 21.62/3.71 v1) | ~ (tail(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 21.62/3.71 = v0 | ~ (head(v2) = v1) | ~ (head(v2) = v0)) % 21.62/3.71 % 21.62/3.71 Further assumptions not needed in the proof: % 21.62/3.71 -------------------------------------------- % 21.62/3.71 axiom_001, axiom_002, axiom_003, axiom_004, axiom_005, axiom_006, axiom_007, % 21.62/3.71 axiom_008, axiom_009, axiom_010, axiom_011, axiom_012, axiom_013, axiom_015, % 21.62/3.71 axiom_016, axiom_018 % 21.62/3.71 % 21.62/3.71 Those formulas are unsatisfiable: % 21.62/3.71 --------------------------------- % 21.62/3.71 % 21.62/3.71 Begin of proof % 21.62/3.71 | % 21.62/3.71 | ALPHA: (axiom_014) implies: % 21.62/3.71 | (1) ~ (pB = pA) % 21.62/3.71 | % 21.62/3.71 | ALPHA: (axiom_019) implies: % 21.62/3.71 | (2) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (append(nil, v0) = v1) | ~ % 21.62/3.71 | $i(v0)) % 21.62/3.71 | % 21.62/3.71 | ALPHA: (axiom_020) implies: % 21.62/3.71 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 21.62/3.71 | ~ (append(v3, v0) = v4) | ~ (cons(v1, v2) = v3) | ~ $i(v2) | ~ % 21.62/3.71 | $i(v1) | ~ $i(v0) | ? [v5: $i] : (append(v2, v0) = v5 & cons(v1, % 21.62/3.71 | v5) = v4 & $i(v5) & $i(v4))) % 21.62/3.71 | % 21.62/3.71 | ALPHA: (axiom_021) implies: % 21.62/3.71 | (4) ? [v0: $i] : (cons(a, nil) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : % 21.62/3.71 | ( ~ (linP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 21.62/3.71 | $i] : (linP(v3) = v4 & append(v2, v0) = v5 & append(v0, v5) = v4 % 21.62/3.71 | & aP(v1) = v3 & $i(v5) & $i(v4) & $i(v3))) & ! [v1: $i] : ! % 21.62/3.71 | [v2: $i] : ( ~ (aP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] % 21.62/3.71 | : ? [v5: $i] : (linP(v2) = v3 & linP(v1) = v4 & append(v4, v0) = % 21.62/3.71 | v5 & append(v0, v5) = v3 & $i(v5) & $i(v4) & $i(v3)))) % 21.62/3.71 | % 21.62/3.71 | ALPHA: (axiom_022) implies: % 21.62/3.71 | (5) ? [v0: $i] : (cons(b, nil) = v0 & $i(v0) & ! [v1: $i] : ! [v2: $i] : % 21.62/3.71 | ( ~ (linP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 21.62/3.71 | $i] : (linP(v3) = v4 & append(v2, v0) = v5 & append(v0, v5) = v4 % 21.62/3.71 | & bP(v1) = v3 & $i(v5) & $i(v4) & $i(v3))) & ! [v1: $i] : ! % 21.62/3.72 | [v2: $i] : ( ~ (bP(v1) = v2) | ~ $i(v1) | ? [v3: $i] : ? [v4: $i] % 21.62/3.72 | : ? [v5: $i] : (linP(v2) = v3 & linP(v1) = v4 & append(v4, v0) = % 21.62/3.72 | v5 & append(v0, v5) = v3 & $i(v5) & $i(v4) & $i(v3)))) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (axiom_023) implies: % 21.62/3.72 | (6) $i(a) % 21.62/3.72 | (7) $i(pA) % 21.62/3.72 | (8) ? [v0: $i] : (linP(pA) = v0 & cons(a, nil) = v0 & $i(v0)) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (axiom_024) implies: % 21.62/3.72 | (9) $i(b) % 21.62/3.72 | (10) $i(pB) % 21.62/3.72 | (11) ? [v0: $i] : (linP(pB) = v0 & cons(b, nil) = v0 & $i(v0)) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (axiom_025) implies: % 21.62/3.72 | (12) $i(nil) % 21.62/3.72 | (13) $i(pE) % 21.62/3.72 | (14) linP(pE) = nil % 21.62/3.72 | % 21.62/3.72 | ALPHA: (axiom_026) implies: % 21.62/3.72 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 21.62/3.72 | ( ~ (linP(v1) = v3) | ~ (linP(v0) = v2) | ~ (append(v2, v3) = v4) | % 21.62/3.72 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (linC(v5) = v4 & c2(v0, v1) = % 21.62/3.72 | v5 & $i(v5) & $i(v4))) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (function-axioms) implies: % 21.62/3.72 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (proj1C(v2) = % 21.62/3.72 | v1) | ~ (proj1C(v2) = v0)) % 21.62/3.72 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.62/3.72 | (cons(v3, v2) = v1) | ~ (cons(v3, v2) = v0)) % 21.62/3.72 | (18) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 21.62/3.72 | (append(v3, v2) = v1) | ~ (append(v3, v2) = v0)) % 21.62/3.72 | % 21.62/3.72 | DELTA: instantiating (11) with fresh symbol all_22_0 gives: % 21.62/3.72 | (19) linP(pB) = all_22_0 & cons(b, nil) = all_22_0 & $i(all_22_0) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (19) implies: % 21.62/3.72 | (20) cons(b, nil) = all_22_0 % 21.62/3.72 | (21) linP(pB) = all_22_0 % 21.62/3.72 | % 21.62/3.72 | DELTA: instantiating (8) with fresh symbol all_24_0 gives: % 21.62/3.72 | (22) linP(pA) = all_24_0 & cons(a, nil) = all_24_0 & $i(all_24_0) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (22) implies: % 21.62/3.72 | (23) cons(a, nil) = all_24_0 % 21.62/3.72 | (24) linP(pA) = all_24_0 % 21.62/3.72 | % 21.62/3.72 | DELTA: instantiating (5) with fresh symbol all_26_0 gives: % 21.62/3.72 | (25) cons(b, nil) = all_26_0 & $i(all_26_0) & ! [v0: $i] : ! [v1: $i] : ( % 21.62/3.72 | ~ (linP(v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: % 21.62/3.72 | $i] : (linP(v2) = v3 & append(v1, all_26_0) = v4 & % 21.62/3.72 | append(all_26_0, v4) = v3 & bP(v0) = v2 & $i(v4) & $i(v3) & % 21.62/3.72 | $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ (bP(v0) = v1) | ~ % 21.62/3.72 | $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (linP(v1) = v2 & % 21.62/3.72 | linP(v0) = v3 & append(v3, all_26_0) = v4 & append(all_26_0, v4) = % 21.62/3.72 | v2 & $i(v4) & $i(v3) & $i(v2))) % 21.62/3.72 | % 21.62/3.72 | ALPHA: (25) implies: % 21.62/3.72 | (26) $i(all_26_0) % 21.62/3.73 | (27) cons(b, nil) = all_26_0 % 21.62/3.73 | (28) ! [v0: $i] : ! [v1: $i] : ( ~ (linP(v0) = v1) | ~ $i(v0) | ? [v2: % 21.62/3.73 | $i] : ? [v3: $i] : ? [v4: $i] : (linP(v2) = v3 & append(v1, % 21.62/3.73 | all_26_0) = v4 & append(all_26_0, v4) = v3 & bP(v0) = v2 & % 21.62/3.73 | $i(v4) & $i(v3) & $i(v2))) % 21.62/3.73 | % 21.62/3.73 | DELTA: instantiating (4) with fresh symbol all_29_0 gives: % 21.62/3.73 | (29) cons(a, nil) = all_29_0 & $i(all_29_0) & ! [v0: $i] : ! [v1: $i] : ( % 21.62/3.73 | ~ (linP(v0) = v1) | ~ $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: % 21.62/3.73 | $i] : (linP(v2) = v3 & append(v1, all_29_0) = v4 & % 21.62/3.73 | append(all_29_0, v4) = v3 & aP(v0) = v2 & $i(v4) & $i(v3) & % 21.62/3.73 | $i(v2))) & ! [v0: $i] : ! [v1: $i] : ( ~ (aP(v0) = v1) | ~ % 21.62/3.73 | $i(v0) | ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : (linP(v1) = v2 & % 21.62/3.73 | linP(v0) = v3 & append(v3, all_29_0) = v4 & append(all_29_0, v4) = % 21.62/3.73 | v2 & $i(v4) & $i(v3) & $i(v2))) % 21.62/3.73 | % 21.62/3.73 | ALPHA: (29) implies: % 21.62/3.73 | (30) $i(all_29_0) % 21.62/3.73 | (31) cons(a, nil) = all_29_0 % 21.62/3.73 | (32) ! [v0: $i] : ! [v1: $i] : ( ~ (linP(v0) = v1) | ~ $i(v0) | ? [v2: % 21.62/3.73 | $i] : ? [v3: $i] : ? [v4: $i] : (linP(v2) = v3 & append(v1, % 21.62/3.73 | all_29_0) = v4 & append(all_29_0, v4) = v3 & aP(v0) = v2 & % 21.62/3.73 | $i(v4) & $i(v3) & $i(v2))) % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (17) with all_22_0, all_26_0, nil, b, simplifying % 21.62/3.73 | with (20), (27) gives: % 21.62/3.73 | (33) all_26_0 = all_22_0 % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (17) with all_24_0, all_29_0, nil, a, simplifying % 21.62/3.73 | with (23), (31) gives: % 21.62/3.73 | (34) all_29_0 = all_24_0 % 21.62/3.73 | % 21.62/3.73 | REDUCE: (30), (34) imply: % 21.62/3.73 | (35) $i(all_24_0) % 21.62/3.73 | % 21.62/3.73 | REDUCE: (26), (33) imply: % 21.62/3.73 | (36) $i(all_22_0) % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (32) with pA, all_24_0, simplifying with (7), (24) % 21.62/3.73 | gives: % 21.62/3.73 | (37) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (linP(v0) = v1 & % 21.62/3.73 | append(all_29_0, v2) = v1 & append(all_24_0, all_29_0) = v2 & aP(pA) % 21.62/3.73 | = v0 & $i(v2) & $i(v1) & $i(v0)) % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (28) with pB, all_22_0, simplifying with (10), (21) % 21.62/3.73 | gives: % 21.62/3.73 | (38) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (linP(v0) = v1 & % 21.62/3.73 | append(all_26_0, v2) = v1 & append(all_22_0, all_26_0) = v2 & bP(pB) % 21.62/3.73 | = v0 & $i(v2) & $i(v1) & $i(v0)) % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (32) with pE, nil, simplifying with (13), (14) % 21.62/3.73 | gives: % 21.62/3.73 | (39) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (linP(v0) = v1 & % 21.62/3.73 | append(all_29_0, v2) = v1 & append(nil, all_29_0) = v2 & aP(pE) = v0 % 21.62/3.73 | & $i(v2) & $i(v1) & $i(v0)) % 21.62/3.73 | % 21.62/3.73 | GROUND_INST: instantiating (28) with pE, nil, simplifying with (13), (14) % 21.62/3.73 | gives: % 21.62/3.73 | (40) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (linP(v0) = v1 & % 21.62/3.73 | append(all_26_0, v2) = v1 & append(nil, all_26_0) = v2 & bP(pE) = v0 % 21.62/3.73 | & $i(v2) & $i(v1) & $i(v0)) % 21.62/3.73 | % 21.62/3.73 | DELTA: instantiating (38) with fresh symbols all_42_0, all_42_1, all_42_2 % 21.62/3.73 | gives: % 21.62/3.73 | (41) linP(all_42_2) = all_42_1 & append(all_26_0, all_42_0) = all_42_1 & % 21.62/3.74 | append(all_22_0, all_26_0) = all_42_0 & bP(pB) = all_42_2 & % 21.62/3.74 | $i(all_42_0) & $i(all_42_1) & $i(all_42_2) % 21.62/3.74 | % 21.62/3.74 | ALPHA: (41) implies: % 21.62/3.74 | (42) $i(all_42_0) % 21.62/3.74 | (43) append(all_22_0, all_26_0) = all_42_0 % 21.62/3.74 | (44) append(all_26_0, all_42_0) = all_42_1 % 21.62/3.74 | % 21.62/3.74 | DELTA: instantiating (37) with fresh symbols all_46_0, all_46_1, all_46_2 % 21.62/3.74 | gives: % 21.62/3.74 | (45) linP(all_46_2) = all_46_1 & append(all_29_0, all_46_0) = all_46_1 & % 21.62/3.74 | append(all_24_0, all_29_0) = all_46_0 & aP(pA) = all_46_2 & % 21.62/3.74 | $i(all_46_0) & $i(all_46_1) & $i(all_46_2) % 21.62/3.74 | % 21.62/3.74 | ALPHA: (45) implies: % 21.62/3.74 | (46) $i(all_46_0) % 21.62/3.74 | (47) append(all_24_0, all_29_0) = all_46_0 % 21.62/3.74 | (48) append(all_29_0, all_46_0) = all_46_1 % 21.62/3.74 | % 21.62/3.74 | DELTA: instantiating (40) with fresh symbols all_50_0, all_50_1, all_50_2 % 21.62/3.74 | gives: % 21.62/3.74 | (49) linP(all_50_2) = all_50_1 & append(all_26_0, all_50_0) = all_50_1 & % 21.62/3.74 | append(nil, all_26_0) = all_50_0 & bP(pE) = all_50_2 & $i(all_50_0) & % 21.62/3.74 | $i(all_50_1) & $i(all_50_2) % 21.62/3.74 | % 21.62/3.74 | ALPHA: (49) implies: % 21.62/3.74 | (50) $i(all_50_2) % 21.62/3.74 | (51) $i(all_50_0) % 21.62/3.74 | (52) append(nil, all_26_0) = all_50_0 % 21.62/3.74 | (53) append(all_26_0, all_50_0) = all_50_1 % 21.62/3.74 | (54) linP(all_50_2) = all_50_1 % 21.62/3.74 | % 21.62/3.74 | DELTA: instantiating (39) with fresh symbols all_52_0, all_52_1, all_52_2 % 21.62/3.74 | gives: % 21.62/3.74 | (55) linP(all_52_2) = all_52_1 & append(all_29_0, all_52_0) = all_52_1 & % 21.62/3.74 | append(nil, all_29_0) = all_52_0 & aP(pE) = all_52_2 & $i(all_52_0) & % 21.62/3.74 | $i(all_52_1) & $i(all_52_2) % 21.62/3.74 | % 21.62/3.74 | ALPHA: (55) implies: % 21.62/3.74 | (56) $i(all_52_2) % 21.62/3.74 | (57) $i(all_52_0) % 21.62/3.74 | (58) append(nil, all_29_0) = all_52_0 % 21.62/3.74 | (59) append(all_29_0, all_52_0) = all_52_1 % 21.62/3.74 | (60) linP(all_52_2) = all_52_1 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (34), (59) imply: % 21.62/3.74 | (61) append(all_24_0, all_52_0) = all_52_1 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (34), (48) imply: % 21.62/3.74 | (62) append(all_24_0, all_46_0) = all_46_1 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (33), (53) imply: % 21.62/3.74 | (63) append(all_22_0, all_50_0) = all_50_1 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (33), (44) imply: % 21.62/3.74 | (64) append(all_22_0, all_42_0) = all_42_1 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (34), (47) imply: % 21.62/3.74 | (65) append(all_24_0, all_24_0) = all_46_0 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (33), (43) imply: % 21.62/3.74 | (66) append(all_22_0, all_22_0) = all_42_0 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (34), (58) imply: % 21.62/3.74 | (67) append(nil, all_24_0) = all_52_0 % 21.62/3.74 | % 21.62/3.74 | REDUCE: (33), (52) imply: % 21.62/3.74 | (68) append(nil, all_22_0) = all_50_0 % 21.62/3.74 | % 21.62/3.74 | GROUND_INST: instantiating (2) with all_22_0, all_50_0, simplifying with (36), % 21.62/3.74 | (68) gives: % 21.62/3.74 | (69) all_50_0 = all_22_0 % 21.62/3.74 | % 21.62/3.74 | GROUND_INST: instantiating (2) with all_24_0, all_52_0, simplifying with (35), % 21.62/3.74 | (67) gives: % 21.62/3.74 | (70) all_52_0 = all_24_0 % 21.62/3.74 | % 21.62/3.74 | GROUND_INST: instantiating (15) with pB, pB, all_22_0, all_22_0, all_42_0, % 21.62/3.74 | simplifying with (10), (21), (66) gives: % 21.62/3.74 | (71) ? [v0: $i] : (linC(v0) = all_42_0 & c2(pB, pB) = v0 & $i(v0) & % 21.62/3.74 | $i(all_42_0)) % 21.62/3.74 | % 21.62/3.74 | GROUND_INST: instantiating (3) with all_42_0, b, nil, all_22_0, all_42_1, % 21.62/3.74 | simplifying with (9), (12), (20), (42), (64) gives: % 21.62/3.74 | (72) ? [v0: $i] : (append(nil, all_42_0) = v0 & cons(b, v0) = all_42_1 & % 21.62/3.74 | $i(v0) & $i(all_42_1)) % 21.62/3.74 | % 21.62/3.74 | GROUND_INST: instantiating (3) with all_50_0, b, nil, all_22_0, all_50_1, % 21.62/3.75 | simplifying with (9), (12), (20), (51), (63) gives: % 21.62/3.75 | (73) ? [v0: $i] : (append(nil, all_50_0) = v0 & cons(b, v0) = all_50_1 & % 21.62/3.75 | $i(v0) & $i(all_50_1)) % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (15) with pA, pA, all_24_0, all_24_0, all_46_0, % 21.62/3.75 | simplifying with (7), (24), (65) gives: % 21.62/3.75 | (74) ? [v0: $i] : (linC(v0) = all_46_0 & c2(pA, pA) = v0 & $i(v0) & % 21.62/3.75 | $i(all_46_0)) % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (3) with all_46_0, a, nil, all_24_0, all_46_1, % 21.62/3.75 | simplifying with (6), (12), (23), (46), (62) gives: % 21.62/3.75 | (75) ? [v0: $i] : (append(nil, all_46_0) = v0 & cons(a, v0) = all_46_1 & % 21.62/3.75 | $i(v0) & $i(all_46_1)) % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (3) with all_52_0, a, nil, all_24_0, all_52_1, % 21.62/3.75 | simplifying with (6), (12), (23), (57), (61) gives: % 21.62/3.75 | (76) ? [v0: $i] : (append(nil, all_52_0) = v0 & cons(a, v0) = all_52_1 & % 21.62/3.75 | $i(v0) & $i(all_52_1)) % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (76) with fresh symbol all_60_0 gives: % 21.62/3.75 | (77) append(nil, all_52_0) = all_60_0 & cons(a, all_60_0) = all_52_1 & % 21.62/3.75 | $i(all_60_0) & $i(all_52_1) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (77) implies: % 21.62/3.75 | (78) $i(all_52_1) % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (72) with fresh symbol all_66_0 gives: % 21.62/3.75 | (79) append(nil, all_42_0) = all_66_0 & cons(b, all_66_0) = all_42_1 & % 21.62/3.75 | $i(all_66_0) & $i(all_42_1) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (79) implies: % 21.62/3.75 | (80) append(nil, all_42_0) = all_66_0 % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (74) with fresh symbol all_68_0 gives: % 21.62/3.75 | (81) linC(all_68_0) = all_46_0 & c2(pA, pA) = all_68_0 & $i(all_68_0) & % 21.62/3.75 | $i(all_46_0) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (81) implies: % 21.62/3.75 | (82) $i(all_68_0) % 21.62/3.75 | (83) c2(pA, pA) = all_68_0 % 21.62/3.75 | (84) linC(all_68_0) = all_46_0 % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (73) with fresh symbol all_72_0 gives: % 21.62/3.75 | (85) append(nil, all_50_0) = all_72_0 & cons(b, all_72_0) = all_50_1 & % 21.62/3.75 | $i(all_72_0) & $i(all_50_1) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (85) implies: % 21.62/3.75 | (86) $i(all_50_1) % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (75) with fresh symbol all_78_0 gives: % 21.62/3.75 | (87) append(nil, all_46_0) = all_78_0 & cons(a, all_78_0) = all_46_1 & % 21.62/3.75 | $i(all_78_0) & $i(all_46_1) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (87) implies: % 21.62/3.75 | (88) append(nil, all_46_0) = all_78_0 % 21.62/3.75 | % 21.62/3.75 | DELTA: instantiating (71) with fresh symbol all_88_0 gives: % 21.62/3.75 | (89) linC(all_88_0) = all_42_0 & c2(pB, pB) = all_88_0 & $i(all_88_0) & % 21.62/3.75 | $i(all_42_0) % 21.62/3.75 | % 21.62/3.75 | ALPHA: (89) implies: % 21.62/3.75 | (90) $i(all_88_0) % 21.62/3.75 | (91) c2(pB, pB) = all_88_0 % 21.62/3.75 | (92) linC(all_88_0) = all_42_0 % 21.62/3.75 | % 21.62/3.75 | REDUCE: (61), (70) imply: % 21.62/3.75 | (93) append(all_24_0, all_24_0) = all_52_1 % 21.62/3.75 | % 21.62/3.75 | REDUCE: (63), (69) imply: % 21.62/3.75 | (94) append(all_22_0, all_22_0) = all_50_1 % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (18) with all_42_0, all_50_1, all_22_0, all_22_0, % 21.62/3.75 | simplifying with (66), (94) gives: % 21.62/3.75 | (95) all_50_1 = all_42_0 % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (18) with all_46_0, all_52_1, all_24_0, all_24_0, % 21.62/3.75 | simplifying with (65), (93) gives: % 21.62/3.75 | (96) all_52_1 = all_46_0 % 21.62/3.75 | % 21.62/3.75 | REDUCE: (60), (96) imply: % 21.62/3.75 | (97) linP(all_52_2) = all_46_0 % 21.62/3.75 | % 21.62/3.75 | REDUCE: (54), (95) imply: % 21.62/3.75 | (98) linP(all_50_2) = all_42_0 % 21.62/3.75 | % 21.62/3.75 | GROUND_INST: instantiating (axiom_017) with pA, pA, all_68_0, simplifying with % 21.62/3.75 | (7), (83) gives: % 21.62/3.76 | (99) proj1C(all_68_0) = pA % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (axiom_017) with pB, pB, all_88_0, simplifying with % 21.62/3.76 | (10), (91) gives: % 21.62/3.76 | (100) proj1C(all_88_0) = pB % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (2) with all_42_0, all_66_0, simplifying with (42), % 21.62/3.76 | (80) gives: % 21.62/3.76 | (101) all_66_0 = all_42_0 % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (2) with all_46_0, all_78_0, simplifying with (46), % 21.62/3.76 | (88) gives: % 21.62/3.76 | (102) all_78_0 = all_46_0 % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (15) with pE, all_50_2, nil, all_42_0, all_66_0, % 21.62/3.76 | simplifying with (13), (14), (50), (80), (98) gives: % 21.62/3.76 | (103) ? [v0: $i] : (linC(v0) = all_66_0 & c2(pE, all_50_2) = v0 & $i(v0) & % 21.62/3.76 | $i(all_66_0)) % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (15) with pE, all_52_2, nil, all_46_0, all_78_0, % 21.62/3.76 | simplifying with (13), (14), (56), (88), (97) gives: % 21.62/3.76 | (104) ? [v0: $i] : (linC(v0) = all_78_0 & c2(pE, all_52_2) = v0 & $i(v0) & % 21.62/3.76 | $i(all_78_0)) % 21.62/3.76 | % 21.62/3.76 | DELTA: instantiating (104) with fresh symbol all_136_0 gives: % 21.62/3.76 | (105) linC(all_136_0) = all_78_0 & c2(pE, all_52_2) = all_136_0 & % 21.62/3.76 | $i(all_136_0) & $i(all_78_0) % 21.62/3.76 | % 21.62/3.76 | ALPHA: (105) implies: % 21.62/3.76 | (106) $i(all_136_0) % 21.62/3.76 | (107) c2(pE, all_52_2) = all_136_0 % 21.62/3.76 | (108) linC(all_136_0) = all_78_0 % 21.62/3.76 | % 21.62/3.76 | DELTA: instantiating (103) with fresh symbol all_144_0 gives: % 21.62/3.76 | (109) linC(all_144_0) = all_66_0 & c2(pE, all_50_2) = all_144_0 & % 21.62/3.76 | $i(all_144_0) & $i(all_66_0) % 21.62/3.76 | % 21.62/3.76 | ALPHA: (109) implies: % 21.62/3.76 | (110) $i(all_144_0) % 21.62/3.76 | (111) c2(pE, all_50_2) = all_144_0 % 21.62/3.76 | (112) linC(all_144_0) = all_66_0 % 21.62/3.76 | % 21.62/3.76 | REDUCE: (101), (112) imply: % 21.62/3.76 | (113) linC(all_144_0) = all_42_0 % 21.62/3.76 | % 21.62/3.76 | REDUCE: (102), (108) imply: % 21.62/3.76 | (114) linC(all_136_0) = all_46_0 % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (axiom_017) with pE, all_50_2, all_144_0, % 21.62/3.76 | simplifying with (13), (50), (111) gives: % 21.62/3.76 | (115) proj1C(all_144_0) = pE % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (axiom_017) with pE, all_52_2, all_136_0, % 21.62/3.76 | simplifying with (13), (56), (107) gives: % 21.62/3.76 | (116) proj1C(all_136_0) = pE % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (goal_027) with all_68_0, all_136_0, all_46_0, % 21.62/3.76 | simplifying with (82), (84), (106), (114) gives: % 21.62/3.76 | (117) all_136_0 = all_68_0 % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (goal_027) with all_88_0, all_144_0, all_42_0, % 21.62/3.76 | simplifying with (90), (92), (110), (113) gives: % 21.62/3.76 | (118) all_144_0 = all_88_0 % 21.62/3.76 | % 21.62/3.76 | REDUCE: (115), (118) imply: % 21.62/3.76 | (119) proj1C(all_88_0) = pE % 21.62/3.76 | % 21.62/3.76 | REDUCE: (116), (117) imply: % 21.62/3.76 | (120) proj1C(all_68_0) = pE % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (16) with pA, pE, all_68_0, simplifying with (99), % 21.62/3.76 | (120) gives: % 21.62/3.76 | (121) pE = pA % 21.62/3.76 | % 21.62/3.76 | GROUND_INST: instantiating (16) with pB, pE, all_88_0, simplifying with (100), % 21.62/3.76 | (119) gives: % 21.62/3.76 | (122) pE = pB % 21.62/3.76 | % 21.62/3.76 | COMBINE_EQS: (121), (122) imply: % 21.62/3.76 | (123) pB = pA % 21.62/3.76 | % 21.62/3.76 | SIMP: (123) implies: % 21.62/3.76 | (124) pB = pA % 21.62/3.76 | % 21.62/3.76 | REDUCE: (1), (124) imply: % 21.62/3.76 | (125) $false % 21.62/3.77 | % 21.62/3.77 | CLOSE: (125) is inconsistent. % 21.62/3.77 | % 21.62/3.77 End of proof % 21.62/3.77 % SZS output end Proof for theBenchmark % 21.62/3.77 % 21.62/3.77 3157ms %------------------------------------------------------------------------------