%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KLE085+1 : TPTP v8.1.2. Released v4.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n008.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 : Thu Aug 31 05:34:30 EDT 2023 % Result : Theorem 8.50s 1.87s % Output : Proof 11.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : KLE085+1 : TPTP v8.1.2. Released v4.0.0. % 0.13/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.35 % Computer : n008.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Aug 29 12:32:02 EDT 2023 % 0.13/0.35 % CPUTime : % 0.20/0.62 ________ _____ % 0.20/0.62 ___ __ \_________(_)________________________________ % 0.20/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.20/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.20/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.20/0.62 % 0.20/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.20/0.62 (2023-06-19) % 0.20/0.62 % 0.20/0.62 (c) Philipp Rümmer, 2009-2023 % 0.20/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.20/0.62 Amanda Stjerna. % 0.20/0.62 Free software under BSD-3-Clause. % 0.20/0.62 % 0.20/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.20/0.62 % 0.20/0.62 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.20/0.63 Running up to 7 provers in parallel. % 0.20/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.20/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.20/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.20/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.20/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.20/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.20/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.49/1.03 Prover 1: Preprocessing ... % 2.49/1.03 Prover 4: Preprocessing ... % 2.94/1.08 Prover 5: Preprocessing ... % 2.94/1.08 Prover 6: Preprocessing ... % 2.94/1.08 Prover 2: Preprocessing ... % 2.94/1.08 Prover 3: Preprocessing ... % 2.94/1.08 Prover 0: Preprocessing ... % 3.87/1.34 Prover 3: Constructing countermodel ... % 3.87/1.38 Prover 6: Constructing countermodel ... % 4.68/1.40 Prover 1: Constructing countermodel ... % 4.68/1.44 Prover 5: Proving ... % 4.68/1.44 Prover 4: Constructing countermodel ... % 4.68/1.46 Prover 0: Proving ... % 5.57/1.53 Prover 3: gave up % 5.57/1.53 Prover 6: gave up % 5.57/1.53 Prover 1: gave up % 5.57/1.53 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 5.57/1.54 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 6.06/1.54 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 6.06/1.56 Prover 8: Preprocessing ... % 6.06/1.56 Prover 7: Preprocessing ... % 6.25/1.57 Prover 2: Proving ... % 6.25/1.58 Prover 9: Preprocessing ... % 6.67/1.65 Prover 8: Warning: ignoring some quantifiers % 6.94/1.66 Prover 8: Constructing countermodel ... % 6.94/1.69 Prover 7: Constructing countermodel ... % 6.94/1.71 Prover 9: Constructing countermodel ... % 7.81/1.79 Prover 8: gave up % 7.81/1.81 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 7.81/1.84 Prover 10: Preprocessing ... % 8.50/1.87 Prover 0: proved (1225ms) % 8.50/1.87 % 8.50/1.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 8.50/1.87 % 8.50/1.88 Prover 9: stopped % 8.50/1.88 Prover 2: stopped % 8.50/1.91 Prover 5: stopped % 8.86/1.93 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.86/1.93 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.86/1.93 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 8.86/1.93 Prover 13: Preprocessing ... % 8.86/1.93 Prover 11: Preprocessing ... % 8.86/1.93 Prover 10: Constructing countermodel ... % 8.86/1.93 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 8.86/1.95 Prover 16: Preprocessing ... % 8.86/1.95 Prover 10: gave up % 8.86/1.96 Prover 19: Preprocessing ... % 8.86/1.99 Prover 13: Warning: ignoring some quantifiers % 8.86/1.99 Prover 11: Constructing countermodel ... % 8.86/2.00 Prover 13: Constructing countermodel ... % 8.86/2.04 Prover 19: Warning: ignoring some quantifiers % 8.86/2.05 Prover 19: Constructing countermodel ... % 8.86/2.05 Prover 16: Warning: ignoring some quantifiers % 8.86/2.08 Prover 16: Constructing countermodel ... % 9.69/2.10 Prover 13: gave up % 9.69/2.16 Prover 19: gave up % 11.11/2.25 Prover 4: Found proof (size 83) % 11.11/2.25 Prover 4: proved (1599ms) % 11.11/2.25 Prover 11: stopped % 11.11/2.25 Prover 7: stopped % 11.11/2.25 Prover 16: stopped % 11.11/2.25 % 11.11/2.25 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 11.11/2.25 % 11.11/2.27 % SZS output start Proof for theBenchmark % 11.11/2.27 Assumptions after simplification: % 11.11/2.27 --------------------------------- % 11.11/2.27 % 11.11/2.27 (additive_associativity) % 11.11/2.30 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 11.11/2.30 (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ~ $i(v2) | ~ $i(v1) % 11.11/2.30 | ~ $i(v0) | ? [v5: $i] : (addition(v2, v5) = v4 & addition(v1, v0) = v5 & % 11.11/2.30 $i(v5) & $i(v4))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 11.11/2.30 : ! [v4: $i] : ( ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ~ % 11.11/2.30 $i(v2) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (addition(v5, v0) = v4 & % 11.11/2.30 addition(v2, v1) = v5 & $i(v5) & $i(v4))) % 11.11/2.30 % 11.11/2.30 (additive_commutativity) % 11.11/2.30 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v1, v0) = v2) | ~ % 11.11/2.30 $i(v1) | ~ $i(v0) | (addition(v0, v1) = v2 & $i(v2))) & ! [v0: $i] : ! % 11.11/2.30 [v1: $i] : ! [v2: $i] : ( ~ (addition(v0, v1) = v2) | ~ $i(v1) | ~ $i(v0) | % 11.11/2.30 (addition(v1, v0) = v2 & $i(v2))) % 11.11/2.30 % 11.11/2.30 (additive_idempotence) % 11.11/2.30 ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ (addition(v0, v0) = v1) | ~ $i(v0)) % 11.11/2.30 % 11.11/2.30 (domain1) % 11.11/2.30 $i(zero) & ! [v0: $i] : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | % 11.11/2.30 multiplication(v1, v0) = zero) % 11.11/2.30 % 11.11/2.30 (domain2) % 11.11/2.30 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ % 11.11/2.30 (antidomain(v2) = v3) | ~ (antidomain(v1) = v2) | ~ (multiplication(v0, % 11.11/2.30 v3) = v4) | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : ? [v6: $i] : ? [v7: % 11.11/2.30 $i] : (antidomain(v5) = v6 & antidomain(v4) = v7 & multiplication(v0, v1) % 11.11/2.30 = v5 & addition(v6, v7) = v7 & $i(v7) & $i(v6) & $i(v5))) & ! [v0: $i] : % 11.11/2.31 ! [v1: $i] : ! [v2: $i] : ( ~ (multiplication(v0, v1) = v2) | ~ $i(v1) | ~ % 11.11/2.31 $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : ? [v7: $i] % 11.11/2.31 : (antidomain(v6) = v7 & antidomain(v4) = v5 & antidomain(v2) = v3 & % 11.11/2.31 antidomain(v1) = v4 & multiplication(v0, v5) = v6 & addition(v3, v7) = v7 % 11.11/2.31 & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 11.11/2.31 % 11.11/2.31 (domain3) % 11.11/2.31 $i(one) & ! [v0: $i] : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | % 11.11/2.31 ? [v2: $i] : (antidomain(v1) = v2 & addition(v2, v1) = one & $i(v2))) % 11.11/2.31 % 11.11/2.31 (domain4) % 11.11/2.31 ! [v0: $i] : ! [v1: $i] : ( ~ (domain(v0) = v1) | ~ $i(v0) | ? [v2: $i] : % 11.11/2.31 (antidomain(v2) = v1 & antidomain(v0) = v2 & $i(v2) & $i(v1))) & ! [v0: $i] % 11.11/2.31 : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | ? [v2: $i] : % 11.11/2.31 (domain(v0) = v2 & antidomain(v1) = v2 & $i(v2))) % 11.11/2.31 % 11.11/2.31 (goals) % 11.11/2.31 $i(one) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = one) & % 11.11/2.31 domain(v0) = v1 & addition(v1, one) = v2 & $i(v2) & $i(v1) & $i(v0)) % 11.11/2.31 % 11.11/2.31 (function-axioms) % 11.11/2.31 ! [v0: MultipleValueBool] : ! [v1: MultipleValueBool] : ! [v2: $i] : ! % 11.11/2.31 [v3: $i] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) & ! [v0: % 11.11/2.31 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 11.11/2.31 (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) & ! [v0: % 11.11/2.31 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (addition(v3, % 11.11/2.31 v2) = v1) | ~ (addition(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 11.11/2.31 [v2: $i] : (v1 = v0 | ~ (codomain(v2) = v1) | ~ (codomain(v2) = v0)) & ! % 11.11/2.31 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (coantidomain(v2) = v1) | % 11.11/2.31 ~ (coantidomain(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 % 11.11/2.31 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) & ! [v0: $i] : ! [v1: % 11.11/2.31 $i] : ! [v2: $i] : (v1 = v0 | ~ (antidomain(v2) = v1) | ~ (antidomain(v2) % 11.11/2.31 = v0)) % 11.11/2.31 % 11.11/2.31 Further assumptions not needed in the proof: % 11.11/2.31 -------------------------------------------- % 11.11/2.31 additive_identity, codomain1, codomain2, codomain3, codomain4, % 11.11/2.31 left_annihilation, left_distributivity, multiplicative_associativity, % 11.11/2.31 multiplicative_left_identity, multiplicative_right_identity, order, % 11.11/2.31 right_annihilation, right_distributivity % 11.11/2.31 % 11.11/2.31 Those formulas are unsatisfiable: % 11.11/2.31 --------------------------------- % 11.11/2.31 % 11.11/2.31 Begin of proof % 11.11/2.31 | % 11.11/2.32 | ALPHA: (additive_commutativity) implies: % 11.11/2.32 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (addition(v1, v0) = v2) | % 11.11/2.32 | ~ $i(v1) | ~ $i(v0) | (addition(v0, v1) = v2 & $i(v2))) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (additive_associativity) implies: % 11.11/2.32 | (2) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 11.11/2.32 | ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ~ $i(v2) | % 11.11/2.32 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (addition(v5, v0) = v4 & % 11.11/2.32 | addition(v2, v1) = v5 & $i(v5) & $i(v4))) % 11.11/2.32 | (3) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( % 11.11/2.32 | ~ (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ~ $i(v2) | % 11.11/2.32 | ~ $i(v1) | ~ $i(v0) | ? [v5: $i] : (addition(v2, v5) = v4 & % 11.11/2.32 | addition(v1, v0) = v5 & $i(v5) & $i(v4))) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (domain1) implies: % 11.11/2.32 | (4) ! [v0: $i] : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | % 11.11/2.32 | multiplication(v1, v0) = zero) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (domain2) implies: % 11.11/2.32 | (5) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (multiplication(v0, v1) = % 11.11/2.32 | v2) | ~ $i(v1) | ~ $i(v0) | ? [v3: $i] : ? [v4: $i] : ? [v5: % 11.11/2.32 | $i] : ? [v6: $i] : ? [v7: $i] : (antidomain(v6) = v7 & % 11.11/2.32 | antidomain(v4) = v5 & antidomain(v2) = v3 & antidomain(v1) = v4 & % 11.11/2.32 | multiplication(v0, v5) = v6 & addition(v3, v7) = v7 & $i(v7) & % 11.11/2.32 | $i(v6) & $i(v5) & $i(v4) & $i(v3))) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (domain3) implies: % 11.11/2.32 | (6) ! [v0: $i] : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | ? % 11.11/2.32 | [v2: $i] : (antidomain(v1) = v2 & addition(v2, v1) = one & $i(v2))) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (domain4) implies: % 11.11/2.32 | (7) ! [v0: $i] : ! [v1: $i] : ( ~ (antidomain(v0) = v1) | ~ $i(v0) | ? % 11.11/2.32 | [v2: $i] : (domain(v0) = v2 & antidomain(v1) = v2 & $i(v2))) % 11.11/2.32 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ (domain(v0) = v1) | ~ $i(v0) | ? [v2: % 11.11/2.32 | $i] : (antidomain(v2) = v1 & antidomain(v0) = v2 & $i(v2) & % 11.11/2.32 | $i(v1))) % 11.11/2.32 | % 11.11/2.32 | ALPHA: (goals) implies: % 11.11/2.33 | (9) $i(one) % 11.57/2.33 | (10) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ( ~ (v2 = one) & domain(v0) % 11.57/2.33 | = v1 & addition(v1, one) = v2 & $i(v2) & $i(v1) & $i(v0)) % 11.57/2.33 | % 11.57/2.33 | ALPHA: (function-axioms) implies: % 11.57/2.33 | (11) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 11.57/2.33 | (antidomain(v2) = v1) | ~ (antidomain(v2) = v0)) % 11.57/2.33 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 11.57/2.33 | (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 11.57/2.33 | % 11.57/2.33 | DELTA: instantiating (10) with fresh symbols all_24_0, all_24_1, all_24_2 % 11.57/2.33 | gives: % 11.57/2.33 | (13) ~ (all_24_0 = one) & domain(all_24_2) = all_24_1 & addition(all_24_1, % 11.57/2.33 | one) = all_24_0 & $i(all_24_0) & $i(all_24_1) & $i(all_24_2) % 11.57/2.33 | % 11.57/2.33 | ALPHA: (13) implies: % 11.57/2.33 | (14) ~ (all_24_0 = one) % 11.57/2.33 | (15) $i(all_24_2) % 11.57/2.33 | (16) $i(all_24_1) % 11.57/2.33 | (17) addition(all_24_1, one) = all_24_0 % 11.57/2.33 | (18) domain(all_24_2) = all_24_1 % 11.57/2.33 | % 11.57/2.33 | GROUND_INST: instantiating (1) with one, all_24_1, all_24_0, simplifying with % 11.57/2.33 | (9), (16), (17) gives: % 11.57/2.33 | (19) addition(one, all_24_1) = all_24_0 & $i(all_24_0) % 11.57/2.33 | % 11.57/2.33 | ALPHA: (19) implies: % 11.57/2.33 | (20) addition(one, all_24_1) = all_24_0 % 11.57/2.33 | % 11.57/2.33 | GROUND_INST: instantiating (8) with all_24_2, all_24_1, simplifying with (15), % 11.57/2.33 | (18) gives: % 11.57/2.33 | (21) ? [v0: $i] : (antidomain(v0) = all_24_1 & antidomain(all_24_2) = v0 & % 11.57/2.33 | $i(v0) & $i(all_24_1)) % 11.57/2.33 | % 11.57/2.33 | DELTA: instantiating (21) with fresh symbol all_32_0 gives: % 11.57/2.33 | (22) antidomain(all_32_0) = all_24_1 & antidomain(all_24_2) = all_32_0 & % 11.57/2.33 | $i(all_32_0) & $i(all_24_1) % 11.57/2.33 | % 11.57/2.33 | ALPHA: (22) implies: % 11.57/2.33 | (23) $i(all_32_0) % 11.57/2.33 | (24) antidomain(all_24_2) = all_32_0 % 11.57/2.33 | (25) antidomain(all_32_0) = all_24_1 % 11.57/2.33 | % 11.57/2.33 | GROUND_INST: instantiating (4) with all_24_2, all_32_0, simplifying with (15), % 11.57/2.33 | (24) gives: % 11.57/2.33 | (26) multiplication(all_32_0, all_24_2) = zero % 11.57/2.33 | % 11.57/2.33 | GROUND_INST: instantiating (6) with all_24_2, all_32_0, simplifying with (15), % 11.57/2.33 | (24) gives: % 11.57/2.34 | (27) ? [v0: $i] : (antidomain(all_32_0) = v0 & addition(v0, all_32_0) = % 11.57/2.34 | one & $i(v0)) % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (4) with all_32_0, all_24_1, simplifying with (23), % 11.57/2.34 | (25) gives: % 11.57/2.34 | (28) multiplication(all_24_1, all_32_0) = zero % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (7) with all_32_0, all_24_1, simplifying with (23), % 11.57/2.34 | (25) gives: % 11.57/2.34 | (29) ? [v0: $i] : (domain(all_32_0) = v0 & antidomain(all_24_1) = v0 & % 11.57/2.34 | $i(v0)) % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (6) with all_32_0, all_24_1, simplifying with (23), % 11.57/2.34 | (25) gives: % 11.57/2.34 | (30) ? [v0: $i] : (antidomain(all_24_1) = v0 & addition(v0, all_24_1) = % 11.57/2.34 | one & $i(v0)) % 11.57/2.34 | % 11.57/2.34 | DELTA: instantiating (30) with fresh symbol all_46_0 gives: % 11.57/2.34 | (31) antidomain(all_24_1) = all_46_0 & addition(all_46_0, all_24_1) = one & % 11.57/2.34 | $i(all_46_0) % 11.57/2.34 | % 11.57/2.34 | ALPHA: (31) implies: % 11.57/2.34 | (32) addition(all_46_0, all_24_1) = one % 11.57/2.34 | (33) antidomain(all_24_1) = all_46_0 % 11.57/2.34 | % 11.57/2.34 | DELTA: instantiating (27) with fresh symbol all_48_0 gives: % 11.57/2.34 | (34) antidomain(all_32_0) = all_48_0 & addition(all_48_0, all_32_0) = one & % 11.57/2.34 | $i(all_48_0) % 11.57/2.34 | % 11.57/2.34 | ALPHA: (34) implies: % 11.57/2.34 | (35) $i(all_48_0) % 11.57/2.34 | (36) addition(all_48_0, all_32_0) = one % 11.57/2.34 | (37) antidomain(all_32_0) = all_48_0 % 11.57/2.34 | % 11.57/2.34 | DELTA: instantiating (29) with fresh symbol all_50_0 gives: % 11.57/2.34 | (38) domain(all_32_0) = all_50_0 & antidomain(all_24_1) = all_50_0 & % 11.57/2.34 | $i(all_50_0) % 11.57/2.34 | % 11.57/2.34 | ALPHA: (38) implies: % 11.57/2.34 | (39) $i(all_50_0) % 11.57/2.34 | (40) antidomain(all_24_1) = all_50_0 % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (11) with all_46_0, all_50_0, all_24_1, simplifying % 11.57/2.34 | with (33), (40) gives: % 11.57/2.34 | (41) all_50_0 = all_46_0 % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (11) with all_24_1, all_48_0, all_32_0, simplifying % 11.57/2.34 | with (25), (37) gives: % 11.57/2.34 | (42) all_48_0 = all_24_1 % 11.57/2.34 | % 11.57/2.34 | REDUCE: (36), (42) imply: % 11.57/2.34 | (43) addition(all_24_1, all_32_0) = one % 11.57/2.34 | % 11.57/2.34 | REDUCE: (39), (41) imply: % 11.57/2.34 | (44) $i(all_46_0) % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (2) with all_32_0, all_24_1, all_24_1, one, % 11.57/2.34 | all_24_0, simplifying with (16), (17), (23), (43) gives: % 11.57/2.34 | (45) ? [v0: $i] : (addition(v0, all_32_0) = all_24_0 & addition(all_24_1, % 11.57/2.34 | all_24_1) = v0 & $i(v0) & $i(all_24_0)) % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (2) with all_24_1, all_46_0, all_24_1, one, % 11.57/2.34 | all_24_0, simplifying with (16), (17), (32), (44) gives: % 11.57/2.34 | (46) ? [v0: $i] : (addition(v0, all_24_1) = all_24_0 & addition(all_24_1, % 11.57/2.34 | all_46_0) = v0 & $i(v0) & $i(all_24_0)) % 11.57/2.34 | % 11.57/2.34 | GROUND_INST: instantiating (3) with all_24_1, all_24_1, all_46_0, one, % 11.57/2.34 | all_24_0, simplifying with (16), (20), (32), (44) gives: % 11.57/2.35 | (47) ? [v0: $i] : (addition(all_46_0, v0) = all_24_0 & addition(all_24_1, % 11.57/2.35 | all_24_1) = v0 & $i(v0) & $i(all_24_0)) % 11.57/2.35 | % 11.57/2.35 | GROUND_INST: instantiating (1) with all_24_1, all_46_0, one, simplifying with % 11.57/2.35 | (16), (32), (44) gives: % 11.57/2.35 | (48) addition(all_24_1, all_46_0) = one & $i(one) % 11.57/2.35 | % 11.57/2.35 | ALPHA: (48) implies: % 11.57/2.35 | (49) addition(all_24_1, all_46_0) = one % 11.57/2.35 | % 11.57/2.35 | GROUND_INST: instantiating (5) with all_24_1, all_32_0, zero, simplifying with % 11.57/2.35 | (16), (23), (28) gives: % 11.57/2.35 | (50) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 11.57/2.35 | (antidomain(v3) = v4 & antidomain(v1) = v2 & antidomain(all_32_0) = v1 % 11.57/2.35 | & antidomain(zero) = v0 & multiplication(all_24_1, v2) = v3 & % 11.57/2.35 | addition(v0, v4) = v4 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 11.57/2.35 | % 11.57/2.35 | GROUND_INST: instantiating (5) with all_32_0, all_24_2, zero, simplifying with % 11.57/2.35 | (15), (23), (26) gives: % 11.57/2.35 | (51) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 11.57/2.35 | (antidomain(v3) = v4 & antidomain(v1) = v2 & antidomain(all_24_2) = v1 % 11.57/2.35 | & antidomain(zero) = v0 & multiplication(all_32_0, v2) = v3 & % 11.57/2.35 | addition(v0, v4) = v4 & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 11.57/2.35 | % 11.57/2.35 | GROUND_INST: instantiating (7) with all_24_1, all_46_0, simplifying with (16), % 11.57/2.35 | (33) gives: % 11.57/2.35 | (52) ? [v0: $i] : (domain(all_24_1) = v0 & antidomain(all_46_0) = v0 & % 11.57/2.35 | $i(v0)) % 11.57/2.35 | % 11.57/2.35 | GROUND_INST: instantiating (6) with all_24_1, all_46_0, simplifying with (16), % 11.57/2.35 | (33) gives: % 11.57/2.35 | (53) ? [v0: $i] : (antidomain(all_46_0) = v0 & addition(v0, all_46_0) = % 11.57/2.35 | one & $i(v0)) % 11.57/2.35 | % 11.57/2.35 | DELTA: instantiating (53) with fresh symbol all_62_0 gives: % 11.57/2.35 | (54) antidomain(all_46_0) = all_62_0 & addition(all_62_0, all_46_0) = one & % 11.57/2.35 | $i(all_62_0) % 11.57/2.35 | % 11.57/2.35 | ALPHA: (54) implies: % 11.57/2.35 | (55) addition(all_62_0, all_46_0) = one % 11.57/2.35 | (56) antidomain(all_46_0) = all_62_0 % 11.57/2.35 | % 11.57/2.35 | DELTA: instantiating (52) with fresh symbol all_64_0 gives: % 11.57/2.35 | (57) domain(all_24_1) = all_64_0 & antidomain(all_46_0) = all_64_0 & % 11.57/2.35 | $i(all_64_0) % 11.57/2.35 | % 11.57/2.35 | ALPHA: (57) implies: % 11.57/2.35 | (58) $i(all_64_0) % 11.57/2.35 | (59) antidomain(all_46_0) = all_64_0 % 11.57/2.35 | % 11.57/2.35 | DELTA: instantiating (47) with fresh symbol all_66_0 gives: % 11.57/2.35 | (60) addition(all_46_0, all_66_0) = all_24_0 & addition(all_24_1, all_24_1) % 11.57/2.35 | = all_66_0 & $i(all_66_0) & $i(all_24_0) % 11.57/2.35 | % 11.57/2.35 | ALPHA: (60) implies: % 11.57/2.35 | (61) addition(all_24_1, all_24_1) = all_66_0 % 11.57/2.35 | (62) addition(all_46_0, all_66_0) = all_24_0 % 11.57/2.35 | % 11.57/2.35 | DELTA: instantiating (46) with fresh symbol all_68_0 gives: % 11.57/2.35 | (63) addition(all_68_0, all_24_1) = all_24_0 & addition(all_24_1, all_46_0) % 11.57/2.35 | = all_68_0 & $i(all_68_0) & $i(all_24_0) % 11.57/2.35 | % 11.57/2.35 | ALPHA: (63) implies: % 11.57/2.35 | (64) addition(all_24_1, all_46_0) = all_68_0 % 11.57/2.35 | (65) addition(all_68_0, all_24_1) = all_24_0 % 11.57/2.35 | % 11.57/2.35 | DELTA: instantiating (45) with fresh symbol all_72_0 gives: % 11.57/2.36 | (66) addition(all_72_0, all_32_0) = all_24_0 & addition(all_24_1, all_24_1) % 11.57/2.36 | = all_72_0 & $i(all_72_0) & $i(all_24_0) % 11.57/2.36 | % 11.57/2.36 | ALPHA: (66) implies: % 11.57/2.36 | (67) addition(all_24_1, all_24_1) = all_72_0 % 11.57/2.36 | % 11.57/2.36 | DELTA: instantiating (51) with fresh symbols all_74_0, all_74_1, all_74_2, % 11.57/2.36 | all_74_3, all_74_4 gives: % 11.57/2.36 | (68) antidomain(all_74_1) = all_74_0 & antidomain(all_74_3) = all_74_2 & % 11.57/2.36 | antidomain(all_24_2) = all_74_3 & antidomain(zero) = all_74_4 & % 11.57/2.36 | multiplication(all_32_0, all_74_2) = all_74_1 & addition(all_74_4, % 11.57/2.36 | all_74_0) = all_74_0 & $i(all_74_0) & $i(all_74_1) & $i(all_74_2) & % 11.57/2.36 | $i(all_74_3) & $i(all_74_4) % 11.57/2.36 | % 11.57/2.36 | ALPHA: (68) implies: % 11.57/2.36 | (69) $i(all_74_2) % 11.57/2.36 | (70) antidomain(all_24_2) = all_74_3 % 11.57/2.36 | (71) antidomain(all_74_3) = all_74_2 % 11.57/2.36 | % 11.57/2.36 | DELTA: instantiating (50) with fresh symbols all_80_0, all_80_1, all_80_2, % 11.57/2.36 | all_80_3, all_80_4 gives: % 11.57/2.36 | (72) antidomain(all_80_1) = all_80_0 & antidomain(all_80_3) = all_80_2 & % 11.57/2.36 | antidomain(all_32_0) = all_80_3 & antidomain(zero) = all_80_4 & % 11.57/2.36 | multiplication(all_24_1, all_80_2) = all_80_1 & addition(all_80_4, % 11.57/2.36 | all_80_0) = all_80_0 & $i(all_80_0) & $i(all_80_1) & $i(all_80_2) & % 11.57/2.36 | $i(all_80_3) & $i(all_80_4) % 11.57/2.36 | % 11.57/2.36 | ALPHA: (72) implies: % 11.57/2.36 | (73) $i(all_80_2) % 11.57/2.36 | (74) antidomain(all_32_0) = all_80_3 % 11.57/2.36 | (75) antidomain(all_80_3) = all_80_2 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (12) with all_66_0, all_72_0, all_24_1, all_24_1, % 11.57/2.36 | simplifying with (61), (67) gives: % 11.57/2.36 | (76) all_72_0 = all_66_0 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (12) with one, all_68_0, all_46_0, all_24_1, % 11.57/2.36 | simplifying with (49), (64) gives: % 11.57/2.36 | (77) all_68_0 = one % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (11) with all_32_0, all_74_3, all_24_2, simplifying % 11.57/2.36 | with (24), (70) gives: % 11.57/2.36 | (78) all_74_3 = all_32_0 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (11) with all_24_1, all_80_3, all_32_0, simplifying % 11.57/2.36 | with (25), (74) gives: % 11.57/2.36 | (79) all_80_3 = all_24_1 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (11) with all_62_0, all_64_0, all_46_0, simplifying % 11.57/2.36 | with (56), (59) gives: % 11.57/2.36 | (80) all_64_0 = all_62_0 % 11.57/2.36 | % 11.57/2.36 | REDUCE: (75), (79) imply: % 11.57/2.36 | (81) antidomain(all_24_1) = all_80_2 % 11.57/2.36 | % 11.57/2.36 | REDUCE: (71), (78) imply: % 11.57/2.36 | (82) antidomain(all_32_0) = all_74_2 % 11.57/2.36 | % 11.57/2.36 | REDUCE: (58), (80) imply: % 11.57/2.36 | (83) $i(all_62_0) % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (11) with all_46_0, all_80_2, all_24_1, simplifying % 11.57/2.36 | with (33), (81) gives: % 11.57/2.36 | (84) all_80_2 = all_46_0 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (11) with all_24_1, all_74_2, all_32_0, simplifying % 11.57/2.36 | with (25), (82) gives: % 11.57/2.36 | (85) all_74_2 = all_24_1 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (additive_idempotence) with all_24_1, all_66_0, % 11.57/2.36 | simplifying with (16), (61) gives: % 11.57/2.36 | (86) all_66_0 = all_24_1 % 11.57/2.36 | % 11.57/2.36 | GROUND_INST: instantiating (3) with all_24_1, all_46_0, all_62_0, one, % 11.57/2.36 | all_24_0, simplifying with (16), (20), (44), (55), (83) gives: % 11.57/2.36 | (87) ? [v0: $i] : (addition(all_62_0, v0) = all_24_0 & addition(all_46_0, % 11.57/2.36 | all_24_1) = v0 & $i(v0) & $i(all_24_0)) % 11.57/2.36 | % 11.57/2.36 | DELTA: instantiating (87) with fresh symbol all_150_0 gives: % 11.57/2.37 | (88) addition(all_62_0, all_150_0) = all_24_0 & addition(all_46_0, % 11.57/2.37 | all_24_1) = all_150_0 & $i(all_150_0) & $i(all_24_0) % 11.57/2.37 | % 11.57/2.37 | ALPHA: (88) implies: % 11.57/2.37 | (89) addition(all_46_0, all_24_1) = all_150_0 % 11.57/2.37 | % 11.57/2.37 | REDUCE: (62), (86) imply: % 11.57/2.37 | (90) addition(all_46_0, all_24_1) = all_24_0 % 11.57/2.37 | % 11.57/2.37 | GROUND_INST: instantiating (12) with one, all_150_0, all_24_1, all_46_0, % 11.57/2.37 | simplifying with (32), (89) gives: % 11.57/2.37 | (91) all_150_0 = one % 11.57/2.37 | % 11.57/2.37 | GROUND_INST: instantiating (12) with all_24_0, all_150_0, all_24_1, all_46_0, % 11.57/2.37 | simplifying with (89), (90) gives: % 11.57/2.37 | (92) all_150_0 = all_24_0 % 11.57/2.37 | % 11.57/2.37 | COMBINE_EQS: (91), (92) imply: % 11.57/2.37 | (93) all_24_0 = one % 11.57/2.37 | % 11.57/2.37 | SIMP: (93) implies: % 11.57/2.37 | (94) all_24_0 = one % 11.57/2.37 | % 11.57/2.37 | REDUCE: (14), (94) imply: % 11.57/2.37 | (95) $false % 11.57/2.37 | % 11.57/2.37 | CLOSE: (95) is inconsistent. % 11.57/2.37 | % 11.57/2.37 End of proof % 11.57/2.37 % SZS output end Proof for theBenchmark % 11.57/2.37 % 11.57/2.37 1745ms %------------------------------------------------------------------------------