%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : KRS103+1 : TPTP v8.1.2. Released v3.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n009.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:51:15 EDT 2023 % Result : Unsatisfiable 14.01s 2.64s % Output : Proof 15.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS103+1 : TPTP v8.1.2. Released v3.1.0. % 0.06/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n009.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Mon Aug 28 02:03:05 EDT 2023 % 0.13/0.33 % CPUTime : % 0.66/0.65 ________ _____ % 0.66/0.65 ___ __ \_________(_)________________________________ % 0.66/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.66/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.66/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.66/0.65 % 0.66/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.66/0.65 (2023-06-19) % 0.66/0.65 % 0.66/0.65 (c) Philipp Rümmer, 2009-2023 % 0.66/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.66/0.65 Amanda Stjerna. % 0.66/0.65 Free software under BSD-3-Clause. % 0.66/0.65 % 0.66/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.66/0.65 % 0.66/0.65 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.66/0.67 Running up to 7 provers in parallel. % 0.82/0.69 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.82/0.69 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.82/0.69 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.82/0.69 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.82/0.69 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.82/0.69 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.82/0.69 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.96/1.22 Prover 1: Preprocessing ... % 2.96/1.22 Prover 4: Preprocessing ... % 3.53/1.26 Prover 5: Preprocessing ... % 3.53/1.26 Prover 2: Preprocessing ... % 3.53/1.26 Prover 0: Preprocessing ... % 3.53/1.26 Prover 3: Preprocessing ... % 3.53/1.26 Prover 6: Preprocessing ... % 6.08/1.64 Prover 5: Proving ... % 6.08/1.65 Prover 2: Proving ... % 7.33/1.78 Prover 1: Constructing countermodel ... % 7.81/1.82 Prover 3: Constructing countermodel ... % 8.13/1.89 Prover 6: Constructing countermodel ... % 8.13/1.90 Prover 3: gave up % 8.13/1.90 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.13/1.90 Prover 1: gave up % 8.13/1.91 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.13/1.91 Prover 6: gave up % 8.13/1.93 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 9.01/1.98 Prover 7: Preprocessing ... % 9.01/1.99 Prover 8: Preprocessing ... % 9.01/2.00 Prover 9: Preprocessing ... % 9.01/2.02 Prover 7: Warning: ignoring some quantifiers % 9.41/2.04 Prover 7: Constructing countermodel ... % 10.06/2.14 Prover 4: Constructing countermodel ... % 10.06/2.15 Prover 8: Warning: ignoring some quantifiers % 10.06/2.16 Prover 8: Constructing countermodel ... % 11.13/2.27 Prover 8: gave up % 11.13/2.28 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 11.80/2.35 Prover 10: Preprocessing ... % 11.80/2.39 Prover 10: Warning: ignoring some quantifiers % 11.80/2.40 Prover 10: Constructing countermodel ... % 11.80/2.41 Prover 0: Proving ... % 13.40/2.58 Prover 9: Constructing countermodel ... % 14.01/2.64 Prover 2: proved (1954ms) % 14.01/2.64 % 14.01/2.64 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 14.01/2.64 % 14.01/2.64 Prover 9: stopped % 14.01/2.64 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 14.01/2.64 Prover 5: stopped % 14.10/2.65 Prover 0: stopped % 14.10/2.66 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 14.10/2.66 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 14.10/2.66 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 14.10/2.68 Prover 11: Preprocessing ... % 14.10/2.69 Prover 16: Preprocessing ... % 14.10/2.70 Prover 13: Preprocessing ... % 14.10/2.72 Prover 7: Found proof (size 527) % 14.10/2.72 Prover 7: proved (818ms) % 14.10/2.72 Prover 10: stopped % 14.10/2.72 Prover 16: stopped % 14.10/2.72 Prover 4: stopped % 14.67/2.73 Prover 13: Warning: ignoring some quantifiers % 14.67/2.73 Prover 19: Preprocessing ... % 14.67/2.73 Prover 13: Constructing countermodel ... % 14.67/2.73 Prover 13: stopped % 14.67/2.77 Prover 11: stopped % 15.01/2.82 Prover 19: Warning: ignoring some quantifiers % 15.01/2.83 Prover 19: Constructing countermodel ... % 15.01/2.84 Prover 19: stopped % 15.01/2.84 % 15.01/2.84 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 15.01/2.84 % 15.01/2.86 % SZS output start Proof for theBenchmark % 15.43/2.86 Assumptions after simplification: % 15.43/2.86 --------------------------------- % 15.43/2.86 % 15.43/2.86 (axiom_11) % 15.43/2.86 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus4(v0) | cplus6(v0) | % 15.43/2.87 cminus8(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_12) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus1(v0) | cplus6(v0) | % 15.43/2.87 cminus4(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_19) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus2(v0) | cminus6(v0) | % 15.43/2.87 cplus1(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_2) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus6(v0) | cplus9(v0) | % 15.43/2.87 cplus1(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_20) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus2(v0) | cplus8(v0) | % 15.43/2.87 cminus3(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_21) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus2(v0) | cplus4(v0) | % 15.43/2.87 cminus6(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_22) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus2(v0) | cminus7(v0) | % 15.43/2.87 cplus6(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_25) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus4(v0) | cplus3(v0) | % 15.43/2.87 cplus9(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_26) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus2(v0) | cminus7(v0) | % 15.43/2.87 cminus5(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_27) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus4(v0) | cplus6(v0) | % 15.43/2.87 cminus5(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_28) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus4(v0) | cminus9(v0) | % 15.43/2.87 cplus3(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_29) % 15.43/2.87 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus7(v0) | cminus4(v0) | % 15.43/2.87 cminus3(v0)) % 15.43/2.87 % 15.43/2.87 (axiom_3) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus8(v0) | cminus5(v0) | % 15.43/2.88 cminus3(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_30) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus4(v0) | cplus9(v0) | % 15.43/2.88 cplus1(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_31) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus4(v0) | cminus8(v0) | % 15.43/2.88 cplus9(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_33) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus2(v0) | cminus9(v0) | % 15.43/2.88 cplus7(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_34) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus4(v0) | cplus7(v0) | % 15.43/2.88 cplus9(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_35) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus2(v0) | cminus9(v0) | % 15.43/2.88 cplus3(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_36) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus2(v0) | cminus1(v0) | % 15.43/2.88 cplus4(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_39) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus2(v0) | cplus3(v0) | % 15.43/2.88 cminus8(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_4) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus8(v0) | cplus7(v0) | % 15.43/2.88 cminus3(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_40) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus9(v0) | cplus3(v0) | % 15.43/2.88 cminus5(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_43) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus9(v0) | cminus6(v0) | % 15.43/2.88 cplus1(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_45) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus2(v0) | cminus4(v0) | % 15.43/2.88 cplus8(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_46) % 15.43/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cplus8(v0) | cplus7(v0) | % 15.43/2.88 cminus5(v0)) % 15.43/2.88 % 15.43/2.88 (axiom_47) % 15.43/2.88 $i(i2003_11_14_17_20_46476) & cTest(i2003_11_14_17_20_46476) % 15.43/2.88 % 15.43/2.88 (axiom_48) % 15.54/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cplus8(v0) | ~ cminus8(v0)) % 15.54/2.88 % 15.54/2.88 (axiom_49) % 15.54/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.54/2.88 % 15.54/2.88 (axiom_50) % 15.54/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cplus4(v0) | ~ cminus4(v0)) % 15.54/2.88 % 15.54/2.88 (axiom_51) % 15.54/2.88 ! [v0: $i] : ( ~ $i(v0) | ~ cminus7(v0) | ~ cplus7(v0)) % 15.54/2.88 % 15.54/2.88 (axiom_52) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cplus3(v0) | ~ cminus3(v0)) % 15.54/2.89 % 15.54/2.89 (axiom_54) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cminus2(v0) | ~ cplus2(v0)) % 15.54/2.89 % 15.54/2.89 (axiom_55) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cminus1(v0) | ~ cplus1(v0)) % 15.54/2.89 % 15.54/2.89 (axiom_56) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cplus6(v0) | ~ cminus6(v0)) % 15.54/2.89 % 15.54/2.89 (axiom_6) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus7(v0) | cplus3(v0) | % 15.54/2.89 cplus8(v0)) % 15.54/2.89 % 15.54/2.89 (axiom_9) % 15.54/2.89 ! [v0: $i] : ( ~ $i(v0) | ~ cTest(v0) | cminus9(v0) | cminus4(v0) | % 15.54/2.89 cminus8(v0)) % 15.54/2.89 % 15.54/2.89 Further assumptions not needed in the proof: % 15.54/2.89 -------------------------------------------- % 15.54/2.89 axiom_0, axiom_1, axiom_10, axiom_13, axiom_14, axiom_15, axiom_16, axiom_17, % 15.54/2.89 axiom_18, axiom_23, axiom_24, axiom_32, axiom_37, axiom_38, axiom_41, axiom_42, % 15.54/2.89 axiom_44, axiom_5, axiom_53, axiom_7, axiom_8 % 15.54/2.89 % 15.54/2.89 Those formulas are unsatisfiable: % 15.54/2.89 --------------------------------- % 15.54/2.89 % 15.54/2.89 Begin of proof % 15.54/2.89 | % 15.54/2.89 | ALPHA: (axiom_47) implies: % 15.54/2.89 | (1) cTest(i2003_11_14_17_20_46476) % 15.54/2.89 | (2) $i(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_21) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (3) cminus2(i2003_11_14_17_20_46476) | cplus4(i2003_11_14_17_20_46476) | % 15.54/2.89 | cminus6(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_35) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (4) cminus2(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.54/2.89 | cplus3(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_33) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (5) cminus2(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.54/2.89 | cplus7(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_22) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (6) cminus2(i2003_11_14_17_20_46476) | cminus7(i2003_11_14_17_20_46476) | % 15.54/2.89 | cplus6(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_39) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (7) cminus2(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.54/2.89 | cminus8(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_36) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.89 | (8) cplus2(i2003_11_14_17_20_46476) | cminus1(i2003_11_14_17_20_46476) | % 15.54/2.89 | cplus4(i2003_11_14_17_20_46476) % 15.54/2.89 | % 15.54/2.89 | GROUND_INST: instantiating (axiom_26) with i2003_11_14_17_20_46476, % 15.54/2.89 | simplifying with (1), (2) gives: % 15.54/2.90 | (9) cplus2(i2003_11_14_17_20_46476) | cminus7(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus5(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_45) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (10) cplus2(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus8(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_20) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (11) cplus2(i2003_11_14_17_20_46476) | cplus8(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus3(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_19) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (12) cplus2(i2003_11_14_17_20_46476) | cminus6(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus1(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_12) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (13) cminus1(i2003_11_14_17_20_46476) | cplus6(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus4(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_28) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (14) cplus4(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus3(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_25) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (15) cplus4(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus9(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_11) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (16) cplus4(i2003_11_14_17_20_46476) | cplus6(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus8(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_27) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (17) cplus4(i2003_11_14_17_20_46476) | cplus6(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus5(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_40) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (18) cminus9(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus5(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_9) with i2003_11_14_17_20_46476, simplifying % 15.54/2.90 | with (1), (2) gives: % 15.54/2.90 | (19) cminus9(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus8(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_43) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (20) cminus9(i2003_11_14_17_20_46476) | cminus6(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus1(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_6) with i2003_11_14_17_20_46476, simplifying % 15.54/2.90 | with (1), (2) gives: % 15.54/2.90 | (21) cminus7(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus8(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_29) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (22) cminus7(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus3(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_34) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (23) cminus4(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus9(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_31) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (24) cminus4(i2003_11_14_17_20_46476) | cminus8(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus9(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_30) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (25) cminus4(i2003_11_14_17_20_46476) | cplus9(i2003_11_14_17_20_46476) | % 15.54/2.90 | cplus1(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_46) with i2003_11_14_17_20_46476, % 15.54/2.90 | simplifying with (1), (2) gives: % 15.54/2.90 | (26) cplus8(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus5(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_4) with i2003_11_14_17_20_46476, simplifying % 15.54/2.90 | with (1), (2) gives: % 15.54/2.90 | (27) cplus8(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus3(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.90 | GROUND_INST: instantiating (axiom_3) with i2003_11_14_17_20_46476, simplifying % 15.54/2.90 | with (1), (2) gives: % 15.54/2.90 | (28) cminus8(i2003_11_14_17_20_46476) | cminus5(i2003_11_14_17_20_46476) | % 15.54/2.90 | cminus3(i2003_11_14_17_20_46476) % 15.54/2.90 | % 15.54/2.91 | GROUND_INST: instantiating (axiom_2) with i2003_11_14_17_20_46476, simplifying % 15.54/2.91 | with (1), (2) gives: % 15.54/2.91 | (29) cminus6(i2003_11_14_17_20_46476) | cplus9(i2003_11_14_17_20_46476) | % 15.54/2.91 | cplus1(i2003_11_14_17_20_46476) % 15.54/2.91 | % 15.54/2.91 | BETA: splitting (29) gives: % 15.54/2.91 | % 15.54/2.91 | Case 1: % 15.54/2.91 | | % 15.54/2.91 | | (30) cminus6(i2003_11_14_17_20_46476) % 15.54/2.91 | | % 15.54/2.91 | | BETA: splitting (26) gives: % 15.54/2.91 | | % 15.54/2.91 | | Case 1: % 15.54/2.91 | | | % 15.54/2.91 | | | (31) cplus8(i2003_11_14_17_20_46476) % 15.54/2.91 | | | % 15.54/2.91 | | | BETA: splitting (25) gives: % 15.54/2.91 | | | % 15.54/2.91 | | | Case 1: % 15.54/2.91 | | | | % 15.54/2.91 | | | | (32) cminus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | % 15.54/2.91 | | | | BETA: splitting (17) gives: % 15.54/2.91 | | | | % 15.54/2.91 | | | | Case 1: % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | (33) cplus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | GROUND_INST: instantiating (axiom_50) with i2003_11_14_17_20_46476, % 15.54/2.91 | | | | | simplifying with (2), (32), (33) gives: % 15.54/2.91 | | | | | (34) $false % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | CLOSE: (34) is inconsistent. % 15.54/2.91 | | | | | % 15.54/2.91 | | | | Case 2: % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | (35) ~ cplus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | BETA: splitting (16) gives: % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | Case 1: % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | (36) cplus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | PRED_UNIFY: (35), (36) imply: % 15.54/2.91 | | | | | | (37) $false % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | CLOSE: (37) is inconsistent. % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | Case 2: % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | (38) cplus6(i2003_11_14_17_20_46476) | % 15.54/2.91 | | | | | | cminus8(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | BETA: splitting (38) gives: % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | Case 1: % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | (39) cplus6(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | GROUND_INST: instantiating (axiom_56) with % 15.54/2.91 | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), (30), % 15.54/2.91 | | | | | | | (39) gives: % 15.54/2.91 | | | | | | | (40) $false % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | CLOSE: (40) is inconsistent. % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | Case 2: % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | (41) cminus8(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | GROUND_INST: instantiating (axiom_48) with % 15.54/2.91 | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), (31), % 15.54/2.91 | | | | | | | (41) gives: % 15.54/2.91 | | | | | | | (42) $false % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | CLOSE: (42) is inconsistent. % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | End of split % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | End of split % 15.54/2.91 | | | | | % 15.54/2.91 | | | | End of split % 15.54/2.91 | | | | % 15.54/2.91 | | | Case 2: % 15.54/2.91 | | | | % 15.54/2.91 | | | | (43) ~ cminus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | % 15.54/2.91 | | | | REF_CLOSE: (2), (18), (19), (24), (28), (31), (43), (axiom_48), % 15.54/2.91 | | | | (axiom_49) are inconsistent by sub-proof #9. % 15.54/2.91 | | | | % 15.54/2.91 | | | End of split % 15.54/2.91 | | | % 15.54/2.91 | | Case 2: % 15.54/2.91 | | | % 15.54/2.91 | | | (44) ~ cplus8(i2003_11_14_17_20_46476) % 15.54/2.91 | | | % 15.54/2.91 | | | BETA: splitting (25) gives: % 15.54/2.91 | | | % 15.54/2.91 | | | Case 1: % 15.54/2.91 | | | | % 15.54/2.91 | | | | (45) cminus4(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | % 15.54/2.91 | | | | BETA: splitting (21) gives: % 15.54/2.91 | | | | % 15.54/2.91 | | | | Case 1: % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | (46) cminus7(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | BETA: splitting (11) gives: % 15.54/2.91 | | | | | % 15.54/2.91 | | | | | Case 1: % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | (47) cplus2(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | BETA: splitting (27) gives: % 15.54/2.91 | | | | | | % 15.54/2.91 | | | | | | Case 1: % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | (48) cplus8(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | PRED_UNIFY: (44), (48) imply: % 15.54/2.91 | | | | | | | (49) $false % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | CLOSE: (49) is inconsistent. % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | Case 2: % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | (50) cplus7(i2003_11_14_17_20_46476) | % 15.54/2.91 | | | | | | | cminus3(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | BETA: splitting (5) gives: % 15.54/2.91 | | | | | | | % 15.54/2.91 | | | | | | | Case 1: % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | (51) cminus2(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | GROUND_INST: instantiating (axiom_54) with % 15.54/2.91 | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.54/2.91 | | | | | | | | (47), (51) gives: % 15.54/2.91 | | | | | | | | (52) $false % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | CLOSE: (52) is inconsistent. % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | Case 2: % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | (53) cminus9(i2003_11_14_17_20_46476) | % 15.54/2.91 | | | | | | | | cplus7(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | BETA: splitting (18) gives: % 15.54/2.91 | | | | | | | | % 15.54/2.91 | | | | | | | | Case 1: % 15.54/2.91 | | | | | | | | | % 15.54/2.91 | | | | | | | | | (54) cminus9(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | | | % 15.54/2.91 | | | | | | | | | BETA: splitting (50) gives: % 15.54/2.91 | | | | | | | | | % 15.54/2.91 | | | | | | | | | Case 1: % 15.54/2.91 | | | | | | | | | | % 15.54/2.91 | | | | | | | | | | (55) cplus7(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | | | | % 15.54/2.91 | | | | | | | | | | GROUND_INST: instantiating (axiom_51) with % 15.54/2.91 | | | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.54/2.91 | | | | | | | | | | (46), (55) gives: % 15.54/2.91 | | | | | | | | | | (56) $false % 15.54/2.91 | | | | | | | | | | % 15.54/2.91 | | | | | | | | | | CLOSE: (56) is inconsistent. % 15.54/2.91 | | | | | | | | | | % 15.54/2.91 | | | | | | | | | Case 2: % 15.54/2.91 | | | | | | | | | | % 15.54/2.91 | | | | | | | | | | (57) cminus3(i2003_11_14_17_20_46476) % 15.54/2.91 | | | | | | | | | | % 15.54/2.92 | | | | | | | | | | REF_CLOSE: (2), (15), (45), (54), (57), (axiom_49), % 15.54/2.92 | | | | | | | | | | (axiom_50), (axiom_52) are inconsistent by % 15.54/2.92 | | | | | | | | | | sub-proof #8. % 15.54/2.92 | | | | | | | | | | % 15.54/2.92 | | | | | | | | | End of split % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | Case 2: % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | (58) ~ cminus9(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | REF_CLOSE: (2), (46), (53), (58), (axiom_51) are inconsistent % 15.54/2.92 | | | | | | | | | by sub-proof #7. % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | End of split % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | End of split % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | End of split % 15.54/2.92 | | | | | | % 15.54/2.92 | | | | | Case 2: % 15.54/2.92 | | | | | | % 15.54/2.92 | | | | | | (59) cplus8(i2003_11_14_17_20_46476) | % 15.54/2.92 | | | | | | cminus3(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | % 15.54/2.92 | | | | | | BETA: splitting (59) gives: % 15.54/2.92 | | | | | | % 15.54/2.92 | | | | | | Case 1: % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | (60) cplus8(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | PRED_UNIFY: (44), (60) imply: % 15.54/2.92 | | | | | | | (61) $false % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | CLOSE: (61) is inconsistent. % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | Case 2: % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | (62) cminus3(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | BETA: splitting (4) gives: % 15.54/2.92 | | | | | | | % 15.54/2.92 | | | | | | | Case 1: % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | | (63) cminus2(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | | REF_CLOSE: (2), (11), (14), (15), (20), (44), (45), (63), % 15.54/2.92 | | | | | | | | (axiom_49), (axiom_50), (axiom_52), (axiom_54) are % 15.54/2.92 | | | | | | | | inconsistent by sub-proof #5. % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | Case 2: % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | | (64) ~ cminus2(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | | BETA: splitting (18) gives: % 15.54/2.92 | | | | | | | | % 15.54/2.92 | | | | | | | | Case 1: % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | (65) cminus9(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | REF_CLOSE: (2), (15), (45), (62), (65), (axiom_49), % 15.54/2.92 | | | | | | | | | (axiom_50), (axiom_52) are inconsistent by % 15.54/2.92 | | | | | | | | | sub-proof #8. % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | Case 2: % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | (66) ~ cminus9(i2003_11_14_17_20_46476) % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | | REF_CLOSE: (2), (5), (46), (64), (66), (axiom_51) are % 15.54/2.92 | | | | | | | | | inconsistent by sub-proof #4. % 15.54/2.92 | | | | | | | | | % 15.54/2.92 | | | | | | | | End of split % 15.54/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | End of split % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | End of split % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | End of split % 15.73/2.92 | | | | | % 15.73/2.92 | | | | Case 2: % 15.73/2.92 | | | | | % 15.73/2.92 | | | | | (67) ~ cminus7(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | (68) cplus3(i2003_11_14_17_20_46476) | % 15.73/2.92 | | | | | cplus8(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | % 15.73/2.92 | | | | | BETA: splitting (68) gives: % 15.73/2.92 | | | | | % 15.73/2.92 | | | | | Case 1: % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | (69) cplus3(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | BETA: splitting (9) gives: % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | Case 1: % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | (70) cplus2(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | BETA: splitting (6) gives: % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | Case 1: % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | (71) cminus2(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | GROUND_INST: instantiating (axiom_54) with % 15.73/2.92 | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.73/2.92 | | | | | | | | (70), (71) gives: % 15.73/2.92 | | | | | | | | (72) $false % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | CLOSE: (72) is inconsistent. % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | Case 2: % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | (73) cminus7(i2003_11_14_17_20_46476) | % 15.73/2.92 | | | | | | | | cplus6(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | BETA: splitting (73) gives: % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | Case 1: % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | (74) cminus7(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | PRED_UNIFY: (67), (74) imply: % 15.73/2.92 | | | | | | | | | (75) $false % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | CLOSE: (75) is inconsistent. % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | Case 2: % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | (76) cplus6(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | GROUND_INST: instantiating (axiom_56) with % 15.73/2.92 | | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.73/2.92 | | | | | | | | | (30), (76) gives: % 15.73/2.92 | | | | | | | | | (77) $false % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | | CLOSE: (77) is inconsistent. % 15.73/2.92 | | | | | | | | | % 15.73/2.92 | | | | | | | | End of split % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | End of split % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | Case 2: % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | (78) ~ cplus2(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | BETA: splitting (11) gives: % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | | Case 1: % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | (79) cplus2(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | PRED_UNIFY: (78), (79) imply: % 15.73/2.92 | | | | | | | | (80) $false % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | CLOSE: (80) is inconsistent. % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | Case 2: % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | (81) cplus8(i2003_11_14_17_20_46476) | % 15.73/2.92 | | | | | | | | cminus3(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | | REF_CLOSE: (2), (44), (69), (81), (axiom_52) are inconsistent by % 15.73/2.92 | | | | | | | | sub-proof #6. % 15.73/2.92 | | | | | | | | % 15.73/2.92 | | | | | | | End of split % 15.73/2.92 | | | | | | | % 15.73/2.92 | | | | | | End of split % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | Case 2: % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | (82) cplus8(i2003_11_14_17_20_46476) % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | PRED_UNIFY: (44), (82) imply: % 15.73/2.92 | | | | | | (83) $false % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | | CLOSE: (83) is inconsistent. % 15.73/2.92 | | | | | | % 15.73/2.92 | | | | | End of split % 15.73/2.92 | | | | | % 15.73/2.92 | | | | End of split % 15.73/2.92 | | | | % 15.73/2.92 | | | Case 2: % 15.73/2.92 | | | | % 15.73/2.93 | | | | (84) ~ cminus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | % 15.73/2.93 | | | | REF_CLOSE: (2), (5), (7), (10), (18), (21), (22), (23), (44), (84), % 15.73/2.93 | | | | (axiom_49), (axiom_51), (axiom_52), (axiom_54) are % 15.73/2.93 | | | | inconsistent by sub-proof #2. % 15.73/2.93 | | | | % 15.73/2.93 | | | End of split % 15.73/2.93 | | | % 15.73/2.93 | | End of split % 15.73/2.93 | | % 15.73/2.93 | Case 2: % 15.73/2.93 | | % 15.73/2.93 | | (85) ~ cminus6(i2003_11_14_17_20_46476) % 15.73/2.93 | | % 15.73/2.93 | | BETA: splitting (26) gives: % 15.73/2.93 | | % 15.73/2.93 | | Case 1: % 15.73/2.93 | | | % 15.73/2.93 | | | (86) cplus8(i2003_11_14_17_20_46476) % 15.73/2.93 | | | % 15.73/2.93 | | | BETA: splitting (25) gives: % 15.73/2.93 | | | % 15.73/2.93 | | | Case 1: % 15.73/2.93 | | | | % 15.73/2.93 | | | | (87) cminus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | % 15.73/2.93 | | | | BETA: splitting (4) gives: % 15.73/2.93 | | | | % 15.73/2.93 | | | | Case 1: % 15.73/2.93 | | | | | % 15.73/2.93 | | | | | (88) cminus2(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | % 15.73/2.93 | | | | | BETA: splitting (12) gives: % 15.73/2.93 | | | | | % 15.73/2.93 | | | | | Case 1: % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | (89) cplus2(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | GROUND_INST: instantiating (axiom_54) with i2003_11_14_17_20_46476, % 15.73/2.93 | | | | | | simplifying with (2), (88), (89) gives: % 15.73/2.93 | | | | | | (90) $false % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | CLOSE: (90) is inconsistent. % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | Case 2: % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | (91) cminus6(i2003_11_14_17_20_46476) | % 15.73/2.93 | | | | | | cplus1(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | BETA: splitting (91) gives: % 15.73/2.93 | | | | | | % 15.73/2.93 | | | | | | Case 1: % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | (92) cminus6(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | PRED_UNIFY: (85), (92) imply: % 15.73/2.93 | | | | | | | (93) $false % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | CLOSE: (93) is inconsistent. % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | Case 2: % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | (94) cplus1(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | BETA: splitting (17) gives: % 15.73/2.93 | | | | | | | % 15.73/2.93 | | | | | | | Case 1: % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | (95) cplus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | GROUND_INST: instantiating (axiom_50) with % 15.73/2.93 | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.73/2.93 | | | | | | | | (87), (95) gives: % 15.73/2.93 | | | | | | | | (96) $false % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | CLOSE: (96) is inconsistent. % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | Case 2: % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | (97) ~ cplus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | BETA: splitting (13) gives: % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | | Case 1: % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | (98) cminus1(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | GROUND_INST: instantiating (axiom_55) with % 15.73/2.93 | | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.73/2.93 | | | | | | | | | (94), (98) gives: % 15.73/2.93 | | | | | | | | | (99) $false % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | CLOSE: (99) is inconsistent. % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | Case 2: % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | (100) ~ cminus1(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | BETA: splitting (8) gives: % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | | Case 1: % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | (101) cplus2(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | GROUND_INST: instantiating (axiom_54) with % 15.73/2.93 | | | | | | | | | | i2003_11_14_17_20_46476, simplifying with (2), % 15.73/2.93 | | | | | | | | | | (88), (101) gives: % 15.73/2.93 | | | | | | | | | | (102) $false % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | CLOSE: (102) is inconsistent. % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | Case 2: % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | (103) cminus1(i2003_11_14_17_20_46476) | % 15.73/2.93 | | | | | | | | | | cplus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | BETA: splitting (103) gives: % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | Case 1: % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | (104) cminus1(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | PRED_UNIFY: (100), (104) imply: % 15.73/2.93 | | | | | | | | | | | (105) $false % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | CLOSE: (105) is inconsistent. % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | Case 2: % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | (106) cplus4(i2003_11_14_17_20_46476) % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | PRED_UNIFY: (97), (106) imply: % 15.73/2.93 | | | | | | | | | | | (107) $false % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | | CLOSE: (107) is inconsistent. % 15.73/2.93 | | | | | | | | | | | % 15.73/2.93 | | | | | | | | | | End of split % 15.73/2.93 | | | | | | | | | | % 15.73/2.93 | | | | | | | | | End of split % 15.73/2.93 | | | | | | | | | % 15.73/2.93 | | | | | | | | End of split % 15.73/2.93 | | | | | | | | % 15.73/2.93 | | | | | | | End of split % 15.73/2.93 | | | | | | | % 15.78/2.93 | | | | | | End of split % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | End of split % 15.78/2.93 | | | | | % 15.78/2.93 | | | | Case 2: % 15.78/2.93 | | | | | % 15.78/2.93 | | | | | (108) ~ cminus2(i2003_11_14_17_20_46476) % 15.78/2.93 | | | | | % 15.78/2.93 | | | | | BETA: splitting (3) gives: % 15.78/2.93 | | | | | % 15.78/2.93 | | | | | Case 1: % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | | (109) cminus2(i2003_11_14_17_20_46476) % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | | PRED_UNIFY: (108), (109) imply: % 15.78/2.93 | | | | | | (110) $false % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | | CLOSE: (110) is inconsistent. % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | Case 2: % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | | (111) cplus4(i2003_11_14_17_20_46476) | % 15.78/2.93 | | | | | | cminus6(i2003_11_14_17_20_46476) % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | | REF_CLOSE: (2), (85), (87), (111), (axiom_50) are inconsistent by % 15.78/2.93 | | | | | | sub-proof #1. % 15.78/2.93 | | | | | | % 15.78/2.93 | | | | | End of split % 15.78/2.93 | | | | | % 15.78/2.93 | | | | End of split % 15.78/2.93 | | | | % 15.78/2.93 | | | Case 2: % 15.78/2.93 | | | | % 15.78/2.93 | | | | (112) ~ cminus4(i2003_11_14_17_20_46476) % 15.78/2.93 | | | | % 15.78/2.93 | | | | REF_CLOSE: (2), (18), (19), (24), (28), (86), (112), (axiom_48), % 15.78/2.93 | | | | (axiom_49) are inconsistent by sub-proof #9. % 15.78/2.94 | | | | % 15.78/2.94 | | | End of split % 15.78/2.94 | | | % 15.78/2.94 | | Case 2: % 15.78/2.94 | | | % 15.78/2.94 | | | (113) ~ cplus8(i2003_11_14_17_20_46476) % 15.78/2.94 | | | % 15.78/2.94 | | | BETA: splitting (25) gives: % 15.78/2.94 | | | % 15.78/2.94 | | | Case 1: % 15.78/2.94 | | | | % 15.78/2.94 | | | | (114) cminus4(i2003_11_14_17_20_46476) % 15.78/2.94 | | | | % 15.78/2.94 | | | | BETA: splitting (3) gives: % 15.78/2.94 | | | | % 15.78/2.94 | | | | Case 1: % 15.78/2.94 | | | | | % 15.78/2.94 | | | | | (115) cminus2(i2003_11_14_17_20_46476) % 15.78/2.94 | | | | | % 15.78/2.94 | | | | | REF_CLOSE: (2), (11), (14), (15), (20), (113), (114), (115), % 15.78/2.94 | | | | | (axiom_49), (axiom_50), (axiom_52), (axiom_54) are % 15.78/2.94 | | | | | inconsistent by sub-proof #5. % 15.78/2.94 | | | | | % 15.78/2.94 | | | | Case 2: % 15.78/2.94 | | | | | % 15.78/2.94 | | | | | (116) cplus4(i2003_11_14_17_20_46476) | % 15.78/2.94 | | | | | cminus6(i2003_11_14_17_20_46476) % 15.78/2.94 | | | | | % 15.78/2.94 | | | | | REF_CLOSE: (2), (85), (114), (116), (axiom_50) are inconsistent by % 15.78/2.94 | | | | | sub-proof #1. % 15.78/2.94 | | | | | % 15.78/2.94 | | | | End of split % 15.78/2.94 | | | | % 15.78/2.94 | | | Case 2: % 15.78/2.94 | | | | % 15.78/2.94 | | | | (117) ~ cminus4(i2003_11_14_17_20_46476) % 15.78/2.94 | | | | % 15.78/2.94 | | | | REF_CLOSE: (2), (5), (7), (10), (18), (21), (22), (23), (113), (117), % 15.78/2.94 | | | | (axiom_49), (axiom_51), (axiom_52), (axiom_54) are % 15.78/2.94 | | | | inconsistent by sub-proof #2. % 15.78/2.94 | | | | % 15.78/2.94 | | | End of split % 15.78/2.94 | | | % 15.78/2.94 | | End of split % 15.78/2.94 | | % 15.78/2.94 | End of split % 15.78/2.94 | % 15.78/2.94 End of proof % 15.78/2.94 % 15.78/2.94 Sub-proof #1 shows that the following formulas are inconsistent: % 15.78/2.94 ---------------------------------------------------------------- % 15.78/2.94 (1) ~ cminus6(i2003_11_14_17_20_46476) % 15.78/2.94 (2) cminus4(i2003_11_14_17_20_46476) % 15.78/2.94 (3) ! [v0: $i] : ( ~ $i(v0) | ~ cplus4(v0) | ~ cminus4(v0)) % 15.78/2.94 (4) cplus4(i2003_11_14_17_20_46476) | cminus6(i2003_11_14_17_20_46476) % 15.78/2.94 (5) $i(i2003_11_14_17_20_46476) % 15.78/2.94 % 15.78/2.94 Begin of proof % 15.78/2.94 | % 15.78/2.94 | BETA: splitting (4) gives: % 15.78/2.94 | % 15.78/2.94 | Case 1: % 15.78/2.94 | | % 15.78/2.94 | | (6) cplus4(i2003_11_14_17_20_46476) % 15.78/2.94 | | % 15.78/2.94 | | GROUND_INST: instantiating (3) with i2003_11_14_17_20_46476, simplifying % 15.78/2.94 | | with (2), (5), (6) gives: % 15.78/2.94 | | (7) $false % 15.78/2.94 | | % 15.78/2.94 | | CLOSE: (7) is inconsistent. % 15.78/2.94 | | % 15.78/2.94 | Case 2: % 15.78/2.94 | | % 15.78/2.94 | | (8) cminus6(i2003_11_14_17_20_46476) % 15.78/2.94 | | % 15.78/2.94 | | PRED_UNIFY: (1), (8) imply: % 15.78/2.94 | | (9) $false % 15.78/2.94 | | % 15.78/2.94 | | CLOSE: (9) is inconsistent. % 15.78/2.94 | | % 15.78/2.94 | End of split % 15.78/2.94 | % 15.78/2.94 End of proof % 15.78/2.94 % 15.78/2.94 Sub-proof #2 shows that the following formulas are inconsistent: % 15.78/2.94 ---------------------------------------------------------------- % 15.78/2.94 (1) cminus2(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.94 cminus8(i2003_11_14_17_20_46476) % 15.78/2.94 (2) ! [v0: $i] : ( ~ $i(v0) | ~ cminus2(v0) | ~ cplus2(v0)) % 15.78/2.94 (3) ~ cplus8(i2003_11_14_17_20_46476) % 15.78/2.94 (4) cminus7(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.94 cplus8(i2003_11_14_17_20_46476) % 15.78/2.94 (5) ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.78/2.94 (6) cplus2(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.78/2.94 cplus8(i2003_11_14_17_20_46476) % 15.78/2.94 (7) cminus7(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.78/2.94 cminus3(i2003_11_14_17_20_46476) % 15.78/2.94 (8) cminus4(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) | % 15.78/2.94 cplus9(i2003_11_14_17_20_46476) % 15.78/2.94 (9) cminus2(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.78/2.94 cplus7(i2003_11_14_17_20_46476) % 15.78/2.94 (10) cminus9(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.94 cminus5(i2003_11_14_17_20_46476) % 15.78/2.94 (11) ! [v0: $i] : ( ~ $i(v0) | ~ cplus3(v0) | ~ cminus3(v0)) % 15.78/2.94 (12) ~ cminus4(i2003_11_14_17_20_46476) % 15.78/2.94 (13) $i(i2003_11_14_17_20_46476) % 15.78/2.94 (14) ! [v0: $i] : ( ~ $i(v0) | ~ cminus7(v0) | ~ cplus7(v0)) % 15.78/2.94 % 15.78/2.94 Begin of proof % 15.78/2.94 | % 15.78/2.94 | BETA: splitting (6) gives: % 15.78/2.94 | % 15.78/2.94 | Case 1: % 15.78/2.94 | | % 15.78/2.94 | | (15) cplus2(i2003_11_14_17_20_46476) % 15.78/2.94 | | % 15.78/2.94 | | BETA: splitting (4) gives: % 15.78/2.94 | | % 15.78/2.94 | | Case 1: % 15.78/2.94 | | | % 15.78/2.94 | | | (16) cminus7(i2003_11_14_17_20_46476) % 15.78/2.94 | | | % 15.78/2.95 | | | REF_CLOSE: (1), (2), (5), (8), (9), (10), (12), (13), (14), (15), (16) are % 15.78/2.95 | | | inconsistent by sub-proof #3. % 15.78/2.95 | | | % 15.78/2.95 | | Case 2: % 15.78/2.95 | | | % 15.78/2.95 | | | (17) cplus3(i2003_11_14_17_20_46476) | cplus8(i2003_11_14_17_20_46476) % 15.78/2.95 | | | % 15.78/2.95 | | | BETA: splitting (7) gives: % 15.78/2.95 | | | % 15.78/2.95 | | | Case 1: % 15.78/2.95 | | | | % 15.78/2.95 | | | | (18) cminus7(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | % 15.78/2.95 | | | | REF_CLOSE: (1), (2), (5), (8), (9), (10), (12), (13), (14), (15), (18) % 15.78/2.95 | | | | are inconsistent by sub-proof #3. % 15.78/2.95 | | | | % 15.78/2.95 | | | Case 2: % 15.78/2.95 | | | | % 15.78/2.95 | | | | (19) cminus4(i2003_11_14_17_20_46476) | % 15.78/2.95 | | | | cminus3(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | % 15.78/2.95 | | | | BETA: splitting (19) gives: % 15.78/2.95 | | | | % 15.78/2.95 | | | | Case 1: % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | (20) cminus4(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | PRED_UNIFY: (12), (20) imply: % 15.78/2.95 | | | | | (21) $false % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | CLOSE: (21) is inconsistent. % 15.78/2.95 | | | | | % 15.78/2.95 | | | | Case 2: % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | (22) cminus3(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | BETA: splitting (17) gives: % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | Case 1: % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | (23) cplus3(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | GROUND_INST: instantiating (11) with i2003_11_14_17_20_46476, % 15.78/2.95 | | | | | | simplifying with (13), (22), (23) gives: % 15.78/2.95 | | | | | | (24) $false % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | CLOSE: (24) is inconsistent. % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | Case 2: % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | (25) cplus8(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | PRED_UNIFY: (3), (25) imply: % 15.78/2.95 | | | | | | (26) $false % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | | CLOSE: (26) is inconsistent. % 15.78/2.95 | | | | | | % 15.78/2.95 | | | | | End of split % 15.78/2.95 | | | | | % 15.78/2.95 | | | | End of split % 15.78/2.95 | | | | % 15.78/2.95 | | | End of split % 15.78/2.95 | | | % 15.78/2.95 | | End of split % 15.78/2.95 | | % 15.78/2.95 | Case 2: % 15.78/2.95 | | % 15.78/2.95 | | (27) cminus4(i2003_11_14_17_20_46476) | cplus8(i2003_11_14_17_20_46476) % 15.78/2.95 | | % 15.78/2.95 | | BETA: splitting (27) gives: % 15.78/2.95 | | % 15.78/2.95 | | Case 1: % 15.78/2.95 | | | % 15.78/2.95 | | | (28) cminus4(i2003_11_14_17_20_46476) % 15.78/2.95 | | | % 15.78/2.95 | | | PRED_UNIFY: (12), (28) imply: % 15.78/2.95 | | | (29) $false % 15.78/2.95 | | | % 15.78/2.95 | | | CLOSE: (29) is inconsistent. % 15.78/2.95 | | | % 15.78/2.95 | | Case 2: % 15.78/2.95 | | | % 15.78/2.95 | | | (30) cplus8(i2003_11_14_17_20_46476) % 15.78/2.95 | | | % 15.78/2.95 | | | PRED_UNIFY: (3), (30) imply: % 15.78/2.95 | | | (31) $false % 15.78/2.95 | | | % 15.78/2.95 | | | CLOSE: (31) is inconsistent. % 15.78/2.95 | | | % 15.78/2.95 | | End of split % 15.78/2.95 | | % 15.78/2.95 | End of split % 15.78/2.95 | % 15.78/2.95 End of proof % 15.78/2.95 % 15.78/2.95 Sub-proof #3 shows that the following formulas are inconsistent: % 15.78/2.95 ---------------------------------------------------------------- % 15.78/2.95 (1) cminus2(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.95 cminus8(i2003_11_14_17_20_46476) % 15.78/2.95 (2) ! [v0: $i] : ( ~ $i(v0) | ~ cminus2(v0) | ~ cplus2(v0)) % 15.78/2.95 (3) cplus2(i2003_11_14_17_20_46476) % 15.78/2.95 (4) ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.78/2.95 (5) cminus4(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) | % 15.78/2.95 cplus9(i2003_11_14_17_20_46476) % 15.78/2.95 (6) cminus2(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.78/2.95 cplus7(i2003_11_14_17_20_46476) % 15.78/2.95 (7) cminus9(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.95 cminus5(i2003_11_14_17_20_46476) % 15.78/2.95 (8) cminus7(i2003_11_14_17_20_46476) % 15.78/2.95 (9) ~ cminus4(i2003_11_14_17_20_46476) % 15.78/2.95 (10) $i(i2003_11_14_17_20_46476) % 15.78/2.95 (11) ! [v0: $i] : ( ~ $i(v0) | ~ cminus7(v0) | ~ cplus7(v0)) % 15.78/2.95 % 15.78/2.95 Begin of proof % 15.78/2.95 | % 15.78/2.95 | BETA: splitting (1) gives: % 15.78/2.95 | % 15.78/2.95 | Case 1: % 15.78/2.95 | | % 15.78/2.95 | | (12) cminus2(i2003_11_14_17_20_46476) % 15.78/2.95 | | % 15.78/2.95 | | GROUND_INST: instantiating (2) with i2003_11_14_17_20_46476, simplifying % 15.78/2.95 | | with (3), (10), (12) gives: % 15.78/2.95 | | (13) $false % 15.78/2.95 | | % 15.78/2.95 | | CLOSE: (13) is inconsistent. % 15.78/2.95 | | % 15.78/2.95 | Case 2: % 15.78/2.95 | | % 15.78/2.95 | | (14) ~ cminus2(i2003_11_14_17_20_46476) % 15.78/2.95 | | % 15.78/2.95 | | BETA: splitting (5) gives: % 15.78/2.95 | | % 15.78/2.95 | | Case 1: % 15.78/2.95 | | | % 15.78/2.95 | | | (15) cminus4(i2003_11_14_17_20_46476) % 15.78/2.95 | | | % 15.78/2.95 | | | PRED_UNIFY: (9), (15) imply: % 15.78/2.95 | | | (16) $false % 15.78/2.95 | | | % 15.78/2.95 | | | CLOSE: (16) is inconsistent. % 15.78/2.95 | | | % 15.78/2.95 | | Case 2: % 15.78/2.95 | | | % 15.78/2.95 | | | (17) cplus7(i2003_11_14_17_20_46476) | cplus9(i2003_11_14_17_20_46476) % 15.78/2.95 | | | % 15.78/2.95 | | | BETA: splitting (7) gives: % 15.78/2.95 | | | % 15.78/2.95 | | | Case 1: % 15.78/2.95 | | | | % 15.78/2.95 | | | | (18) cminus9(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | % 15.78/2.95 | | | | BETA: splitting (17) gives: % 15.78/2.95 | | | | % 15.78/2.95 | | | | Case 1: % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | (19) cplus7(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | GROUND_INST: instantiating (11) with i2003_11_14_17_20_46476, % 15.78/2.95 | | | | | simplifying with (8), (10), (19) gives: % 15.78/2.95 | | | | | (20) $false % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | CLOSE: (20) is inconsistent. % 15.78/2.95 | | | | | % 15.78/2.95 | | | | Case 2: % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | (21) cplus9(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | GROUND_INST: instantiating (4) with i2003_11_14_17_20_46476, % 15.78/2.95 | | | | | simplifying with (10), (18), (21) gives: % 15.78/2.95 | | | | | (22) $false % 15.78/2.95 | | | | | % 15.78/2.95 | | | | | CLOSE: (22) is inconsistent. % 15.78/2.95 | | | | | % 15.78/2.95 | | | | End of split % 15.78/2.95 | | | | % 15.78/2.95 | | | Case 2: % 15.78/2.95 | | | | % 15.78/2.95 | | | | (23) ~ cminus9(i2003_11_14_17_20_46476) % 15.78/2.95 | | | | % 15.78/2.95 | | | | REF_CLOSE: (6), (8), (10), (11), (14), (23) are inconsistent by % 15.78/2.95 | | | | sub-proof #4. % 15.78/2.95 | | | | % 15.78/2.95 | | | End of split % 15.78/2.95 | | | % 15.78/2.95 | | End of split % 15.78/2.95 | | % 15.78/2.95 | End of split % 15.78/2.95 | % 15.78/2.95 End of proof % 15.78/2.95 % 15.78/2.95 Sub-proof #4 shows that the following formulas are inconsistent: % 15.78/2.95 ---------------------------------------------------------------- % 15.78/2.95 (1) ~ cminus9(i2003_11_14_17_20_46476) % 15.78/2.95 (2) ~ cminus2(i2003_11_14_17_20_46476) % 15.78/2.95 (3) cminus2(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.78/2.95 cplus7(i2003_11_14_17_20_46476) % 15.78/2.96 (4) cminus7(i2003_11_14_17_20_46476) % 15.78/2.96 (5) $i(i2003_11_14_17_20_46476) % 15.78/2.96 (6) ! [v0: $i] : ( ~ $i(v0) | ~ cminus7(v0) | ~ cplus7(v0)) % 15.78/2.96 % 15.78/2.96 Begin of proof % 15.78/2.96 | % 15.78/2.96 | BETA: splitting (3) gives: % 15.78/2.96 | % 15.78/2.96 | Case 1: % 15.78/2.96 | | % 15.78/2.96 | | (7) cminus2(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | PRED_UNIFY: (2), (7) imply: % 15.78/2.96 | | (8) $false % 15.78/2.96 | | % 15.78/2.96 | | CLOSE: (8) is inconsistent. % 15.78/2.96 | | % 15.78/2.96 | Case 2: % 15.78/2.96 | | % 15.78/2.96 | | (9) cminus9(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | REF_CLOSE: (1), (4), (5), (6), (9) are inconsistent by sub-proof #7. % 15.78/2.96 | | % 15.78/2.96 | End of split % 15.78/2.96 | % 15.78/2.96 End of proof % 15.78/2.96 % 15.78/2.96 Sub-proof #5 shows that the following formulas are inconsistent: % 15.78/2.96 ---------------------------------------------------------------- % 15.78/2.96 (1) cplus4(i2003_11_14_17_20_46476) | cminus9(i2003_11_14_17_20_46476) | % 15.78/2.96 cplus3(i2003_11_14_17_20_46476) % 15.78/2.96 (2) ! [v0: $i] : ( ~ $i(v0) | ~ cminus2(v0) | ~ cplus2(v0)) % 15.78/2.96 (3) cplus2(i2003_11_14_17_20_46476) | cplus8(i2003_11_14_17_20_46476) | % 15.78/2.96 cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 (4) cplus4(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.96 cplus9(i2003_11_14_17_20_46476) % 15.78/2.96 (5) cminus4(i2003_11_14_17_20_46476) % 15.78/2.96 (6) ! [v0: $i] : ( ~ $i(v0) | ~ cplus4(v0) | ~ cminus4(v0)) % 15.78/2.96 (7) ~ cplus8(i2003_11_14_17_20_46476) % 15.78/2.96 (8) ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.78/2.96 (9) cminus9(i2003_11_14_17_20_46476) | cminus6(i2003_11_14_17_20_46476) | % 15.78/2.96 cplus1(i2003_11_14_17_20_46476) % 15.78/2.96 (10) ! [v0: $i] : ( ~ $i(v0) | ~ cplus3(v0) | ~ cminus3(v0)) % 15.78/2.96 (11) $i(i2003_11_14_17_20_46476) % 15.78/2.96 (12) cminus2(i2003_11_14_17_20_46476) % 15.78/2.96 % 15.78/2.96 Begin of proof % 15.78/2.96 | % 15.78/2.96 | BETA: splitting (9) gives: % 15.78/2.96 | % 15.78/2.96 | Case 1: % 15.78/2.96 | | % 15.78/2.96 | | (13) cminus9(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | BETA: splitting (3) gives: % 15.78/2.96 | | % 15.78/2.96 | | Case 1: % 15.78/2.96 | | | % 15.78/2.96 | | | (14) cplus2(i2003_11_14_17_20_46476) % 15.78/2.96 | | | % 15.78/2.96 | | | GROUND_INST: instantiating (2) with i2003_11_14_17_20_46476, simplifying % 15.78/2.96 | | | with (11), (12), (14) gives: % 15.78/2.96 | | | (15) $false % 15.78/2.96 | | | % 15.78/2.96 | | | CLOSE: (15) is inconsistent. % 15.78/2.96 | | | % 15.78/2.96 | | Case 2: % 15.78/2.96 | | | % 15.78/2.96 | | | (16) cplus8(i2003_11_14_17_20_46476) | cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | | % 15.78/2.96 | | | BETA: splitting (16) gives: % 15.78/2.96 | | | % 15.78/2.96 | | | Case 1: % 15.78/2.96 | | | | % 15.78/2.96 | | | | (17) cplus8(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | % 15.78/2.96 | | | | PRED_UNIFY: (7), (17) imply: % 15.78/2.96 | | | | (18) $false % 15.78/2.96 | | | | % 15.78/2.96 | | | | CLOSE: (18) is inconsistent. % 15.78/2.96 | | | | % 15.78/2.96 | | | Case 2: % 15.78/2.96 | | | | % 15.78/2.96 | | | | (19) cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | % 15.78/2.96 | | | | REF_CLOSE: (4), (5), (6), (8), (10), (11), (13), (19) are inconsistent % 15.78/2.96 | | | | by sub-proof #8. % 15.78/2.96 | | | | % 15.78/2.96 | | | End of split % 15.78/2.96 | | | % 15.78/2.96 | | End of split % 15.78/2.96 | | % 15.78/2.96 | Case 2: % 15.78/2.96 | | % 15.78/2.96 | | (20) ~ cminus9(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | BETA: splitting (1) gives: % 15.78/2.96 | | % 15.78/2.96 | | Case 1: % 15.78/2.96 | | | % 15.78/2.96 | | | (21) cplus4(i2003_11_14_17_20_46476) % 15.78/2.96 | | | % 15.78/2.96 | | | GROUND_INST: instantiating (6) with i2003_11_14_17_20_46476, simplifying % 15.78/2.96 | | | with (5), (11), (21) gives: % 15.78/2.96 | | | (22) $false % 15.78/2.96 | | | % 15.78/2.96 | | | CLOSE: (22) is inconsistent. % 15.78/2.96 | | | % 15.78/2.96 | | Case 2: % 15.78/2.96 | | | % 15.78/2.96 | | | (23) cminus9(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | | % 15.78/2.96 | | | BETA: splitting (23) gives: % 15.78/2.96 | | | % 15.78/2.96 | | | Case 1: % 15.78/2.96 | | | | % 15.78/2.96 | | | | (24) cminus9(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | % 15.78/2.96 | | | | PRED_UNIFY: (20), (24) imply: % 15.78/2.96 | | | | (25) $false % 15.78/2.96 | | | | % 15.78/2.96 | | | | CLOSE: (25) is inconsistent. % 15.78/2.96 | | | | % 15.78/2.96 | | | Case 2: % 15.78/2.96 | | | | % 15.78/2.96 | | | | (26) cplus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | % 15.78/2.96 | | | | BETA: splitting (3) gives: % 15.78/2.96 | | | | % 15.78/2.96 | | | | Case 1: % 15.78/2.96 | | | | | % 15.78/2.96 | | | | | (27) cplus2(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | | % 15.78/2.96 | | | | | GROUND_INST: instantiating (2) with i2003_11_14_17_20_46476, % 15.78/2.96 | | | | | simplifying with (11), (12), (27) gives: % 15.78/2.96 | | | | | (28) $false % 15.78/2.96 | | | | | % 15.78/2.96 | | | | | CLOSE: (28) is inconsistent. % 15.78/2.96 | | | | | % 15.78/2.96 | | | | Case 2: % 15.78/2.96 | | | | | % 15.78/2.96 | | | | | (29) cplus8(i2003_11_14_17_20_46476) | % 15.78/2.96 | | | | | cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | | | | % 15.78/2.96 | | | | | REF_CLOSE: (7), (10), (11), (26), (29) are inconsistent by sub-proof % 15.78/2.96 | | | | | #6. % 15.78/2.96 | | | | | % 15.78/2.96 | | | | End of split % 15.78/2.96 | | | | % 15.78/2.96 | | | End of split % 15.78/2.96 | | | % 15.78/2.96 | | End of split % 15.78/2.96 | | % 15.78/2.96 | End of split % 15.78/2.96 | % 15.78/2.96 End of proof % 15.78/2.96 % 15.78/2.96 Sub-proof #6 shows that the following formulas are inconsistent: % 15.78/2.96 ---------------------------------------------------------------- % 15.78/2.96 (1) ~ cplus8(i2003_11_14_17_20_46476) % 15.78/2.96 (2) cplus3(i2003_11_14_17_20_46476) % 15.78/2.96 (3) cplus8(i2003_11_14_17_20_46476) | cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 (4) ! [v0: $i] : ( ~ $i(v0) | ~ cplus3(v0) | ~ cminus3(v0)) % 15.78/2.96 (5) $i(i2003_11_14_17_20_46476) % 15.78/2.96 % 15.78/2.96 Begin of proof % 15.78/2.96 | % 15.78/2.96 | BETA: splitting (3) gives: % 15.78/2.96 | % 15.78/2.96 | Case 1: % 15.78/2.96 | | % 15.78/2.96 | | (6) cplus8(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | PRED_UNIFY: (1), (6) imply: % 15.78/2.96 | | (7) $false % 15.78/2.96 | | % 15.78/2.96 | | CLOSE: (7) is inconsistent. % 15.78/2.96 | | % 15.78/2.96 | Case 2: % 15.78/2.96 | | % 15.78/2.96 | | (8) cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | GROUND_INST: instantiating (4) with i2003_11_14_17_20_46476, simplifying % 15.78/2.96 | | with (2), (5), (8) gives: % 15.78/2.96 | | (9) $false % 15.78/2.96 | | % 15.78/2.96 | | CLOSE: (9) is inconsistent. % 15.78/2.96 | | % 15.78/2.96 | End of split % 15.78/2.96 | % 15.78/2.96 End of proof % 15.78/2.96 % 15.78/2.96 Sub-proof #7 shows that the following formulas are inconsistent: % 15.78/2.96 ---------------------------------------------------------------- % 15.78/2.96 (1) cminus9(i2003_11_14_17_20_46476) | cplus7(i2003_11_14_17_20_46476) % 15.78/2.96 (2) ~ cminus9(i2003_11_14_17_20_46476) % 15.78/2.96 (3) cminus7(i2003_11_14_17_20_46476) % 15.78/2.96 (4) $i(i2003_11_14_17_20_46476) % 15.78/2.96 (5) ! [v0: $i] : ( ~ $i(v0) | ~ cminus7(v0) | ~ cplus7(v0)) % 15.78/2.96 % 15.78/2.96 Begin of proof % 15.78/2.96 | % 15.78/2.96 | BETA: splitting (1) gives: % 15.78/2.96 | % 15.78/2.96 | Case 1: % 15.78/2.96 | | % 15.78/2.96 | | (6) cminus9(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | PRED_UNIFY: (2), (6) imply: % 15.78/2.96 | | (7) $false % 15.78/2.96 | | % 15.78/2.96 | | CLOSE: (7) is inconsistent. % 15.78/2.96 | | % 15.78/2.96 | Case 2: % 15.78/2.96 | | % 15.78/2.96 | | (8) cplus7(i2003_11_14_17_20_46476) % 15.78/2.96 | | % 15.78/2.96 | | GROUND_INST: instantiating (5) with i2003_11_14_17_20_46476, simplifying % 15.78/2.96 | | with (3), (4), (8) gives: % 15.78/2.96 | | (9) $false % 15.78/2.96 | | % 15.78/2.96 | | CLOSE: (9) is inconsistent. % 15.78/2.96 | | % 15.78/2.96 | End of split % 15.78/2.96 | % 15.78/2.96 End of proof % 15.78/2.96 % 15.78/2.96 Sub-proof #8 shows that the following formulas are inconsistent: % 15.78/2.96 ---------------------------------------------------------------- % 15.78/2.96 (1) cplus4(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.96 cplus9(i2003_11_14_17_20_46476) % 15.78/2.96 (2) cminus3(i2003_11_14_17_20_46476) % 15.78/2.96 (3) cminus4(i2003_11_14_17_20_46476) % 15.78/2.96 (4) ! [v0: $i] : ( ~ $i(v0) | ~ cplus4(v0) | ~ cminus4(v0)) % 15.78/2.97 (5) ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.78/2.97 (6) cminus9(i2003_11_14_17_20_46476) % 15.78/2.97 (7) ! [v0: $i] : ( ~ $i(v0) | ~ cplus3(v0) | ~ cminus3(v0)) % 15.78/2.97 (8) $i(i2003_11_14_17_20_46476) % 15.78/2.97 % 15.78/2.97 Begin of proof % 15.78/2.97 | % 15.78/2.97 | BETA: splitting (1) gives: % 15.78/2.97 | % 15.78/2.97 | Case 1: % 15.78/2.97 | | % 15.78/2.97 | | (9) cplus4(i2003_11_14_17_20_46476) % 15.78/2.97 | | % 15.78/2.97 | | GROUND_INST: instantiating (4) with i2003_11_14_17_20_46476, simplifying % 15.78/2.97 | | with (3), (8), (9) gives: % 15.78/2.97 | | (10) $false % 15.78/2.97 | | % 15.78/2.97 | | CLOSE: (10) is inconsistent. % 15.78/2.97 | | % 15.78/2.97 | Case 2: % 15.78/2.97 | | % 15.78/2.97 | | (11) cplus3(i2003_11_14_17_20_46476) | cplus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | % 15.78/2.97 | | BETA: splitting (11) gives: % 15.78/2.97 | | % 15.78/2.97 | | Case 1: % 15.78/2.97 | | | % 15.78/2.97 | | | (12) cplus3(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | GROUND_INST: instantiating (7) with i2003_11_14_17_20_46476, simplifying % 15.78/2.97 | | | with (2), (8), (12) gives: % 15.78/2.97 | | | (13) $false % 15.78/2.97 | | | % 15.78/2.97 | | | CLOSE: (13) is inconsistent. % 15.78/2.97 | | | % 15.78/2.97 | | Case 2: % 15.78/2.97 | | | % 15.78/2.97 | | | (14) cplus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | GROUND_INST: instantiating (5) with i2003_11_14_17_20_46476, simplifying % 15.78/2.97 | | | with (6), (8), (14) gives: % 15.78/2.97 | | | (15) $false % 15.78/2.97 | | | % 15.78/2.97 | | | CLOSE: (15) is inconsistent. % 15.78/2.97 | | | % 15.78/2.97 | | End of split % 15.78/2.97 | | % 15.78/2.97 | End of split % 15.78/2.97 | % 15.78/2.97 End of proof % 15.78/2.97 % 15.78/2.97 Sub-proof #9 shows that the following formulas are inconsistent: % 15.78/2.97 ---------------------------------------------------------------- % 15.78/2.97 (1) ! [v0: $i] : ( ~ $i(v0) | ~ cplus8(v0) | ~ cminus8(v0)) % 15.78/2.97 (2) cminus4(i2003_11_14_17_20_46476) | cminus8(i2003_11_14_17_20_46476) | % 15.78/2.97 cplus9(i2003_11_14_17_20_46476) % 15.78/2.97 (3) ! [v0: $i] : ( ~ $i(v0) | ~ cminus9(v0) | ~ cplus9(v0)) % 15.78/2.97 (4) cminus8(i2003_11_14_17_20_46476) | cminus5(i2003_11_14_17_20_46476) | % 15.78/2.97 cminus3(i2003_11_14_17_20_46476) % 15.78/2.97 (5) cplus8(i2003_11_14_17_20_46476) % 15.78/2.97 (6) cminus9(i2003_11_14_17_20_46476) | cminus4(i2003_11_14_17_20_46476) | % 15.78/2.97 cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 (7) cminus9(i2003_11_14_17_20_46476) | cplus3(i2003_11_14_17_20_46476) | % 15.78/2.97 cminus5(i2003_11_14_17_20_46476) % 15.78/2.97 (8) ~ cminus4(i2003_11_14_17_20_46476) % 15.78/2.97 (9) $i(i2003_11_14_17_20_46476) % 15.78/2.97 % 15.78/2.97 Begin of proof % 15.78/2.97 | % 15.78/2.97 | BETA: splitting (7) gives: % 15.78/2.97 | % 15.78/2.97 | Case 1: % 15.78/2.97 | | % 15.78/2.97 | | (10) cminus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | % 15.78/2.97 | | BETA: splitting (4) gives: % 15.78/2.97 | | % 15.78/2.97 | | Case 1: % 15.78/2.97 | | | % 15.78/2.97 | | | (11) cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | GROUND_INST: instantiating (1) with i2003_11_14_17_20_46476, simplifying % 15.78/2.97 | | | with (5), (9), (11) gives: % 15.78/2.97 | | | (12) $false % 15.78/2.97 | | | % 15.78/2.97 | | | CLOSE: (12) is inconsistent. % 15.78/2.97 | | | % 15.78/2.97 | | Case 2: % 15.78/2.97 | | | % 15.78/2.97 | | | (13) ~ cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | BETA: splitting (2) gives: % 15.78/2.97 | | | % 15.78/2.97 | | | Case 1: % 15.78/2.97 | | | | % 15.78/2.97 | | | | (14) cminus4(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | % 15.78/2.97 | | | | PRED_UNIFY: (8), (14) imply: % 15.78/2.97 | | | | (15) $false % 15.78/2.97 | | | | % 15.78/2.97 | | | | CLOSE: (15) is inconsistent. % 15.78/2.97 | | | | % 15.78/2.97 | | | Case 2: % 15.78/2.97 | | | | % 15.78/2.97 | | | | (16) cminus8(i2003_11_14_17_20_46476) | % 15.78/2.97 | | | | cplus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | % 15.78/2.97 | | | | BETA: splitting (16) gives: % 15.78/2.97 | | | | % 15.78/2.97 | | | | Case 1: % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | (17) cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | PRED_UNIFY: (13), (17) imply: % 15.78/2.97 | | | | | (18) $false % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | CLOSE: (18) is inconsistent. % 15.78/2.97 | | | | | % 15.78/2.97 | | | | Case 2: % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | (19) cplus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | GROUND_INST: instantiating (3) with i2003_11_14_17_20_46476, % 15.78/2.97 | | | | | simplifying with (9), (10), (19) gives: % 15.78/2.97 | | | | | (20) $false % 15.78/2.97 | | | | | % 15.78/2.97 | | | | | CLOSE: (20) is inconsistent. % 15.78/2.97 | | | | | % 15.78/2.97 | | | | End of split % 15.78/2.97 | | | | % 15.78/2.97 | | | End of split % 15.78/2.97 | | | % 15.78/2.97 | | End of split % 15.78/2.97 | | % 15.78/2.97 | Case 2: % 15.78/2.97 | | % 15.78/2.97 | | (21) ~ cminus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | % 15.78/2.97 | | BETA: splitting (6) gives: % 15.78/2.97 | | % 15.78/2.97 | | Case 1: % 15.78/2.97 | | | % 15.78/2.97 | | | (22) cminus9(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | PRED_UNIFY: (21), (22) imply: % 15.78/2.97 | | | (23) $false % 15.78/2.97 | | | % 15.78/2.97 | | | CLOSE: (23) is inconsistent. % 15.78/2.97 | | | % 15.78/2.97 | | Case 2: % 15.78/2.97 | | | % 15.78/2.97 | | | (24) cminus4(i2003_11_14_17_20_46476) | % 15.78/2.97 | | | cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 | | | % 15.78/2.97 | | | BETA: splitting (24) gives: % 15.78/2.97 | | | % 15.78/2.97 | | | Case 1: % 15.78/2.97 | | | | % 15.78/2.97 | | | | (25) cminus4(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | % 15.78/2.97 | | | | PRED_UNIFY: (8), (25) imply: % 15.78/2.97 | | | | (26) $false % 15.78/2.97 | | | | % 15.78/2.97 | | | | CLOSE: (26) is inconsistent. % 15.78/2.97 | | | | % 15.78/2.97 | | | Case 2: % 15.78/2.97 | | | | % 15.78/2.97 | | | | (27) cminus8(i2003_11_14_17_20_46476) % 15.78/2.97 | | | | % 15.78/2.97 | | | | GROUND_INST: instantiating (1) with i2003_11_14_17_20_46476, simplifying % 15.78/2.97 | | | | with (5), (9), (27) gives: % 15.78/2.97 | | | | (28) $false % 15.78/2.97 | | | | % 15.78/2.97 | | | | CLOSE: (28) is inconsistent. % 15.78/2.97 | | | | % 15.78/2.97 | | | End of split % 15.78/2.97 | | | % 15.78/2.97 | | End of split % 15.78/2.97 | | % 15.78/2.97 | End of split % 15.78/2.97 | % 15.78/2.97 End of proof % 15.78/2.97 % SZS output end Proof for theBenchmark % 15.78/2.97 % 15.78/2.97 2319ms %------------------------------------------------------------------------------