%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : DAT052_1 : TPTP v8.1.2. Released v5.0.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n022.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 : Wed Aug 30 22:19:02 EDT 2023 % Result : Theorem 7.89s 1.87s % Output : Proof 11.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : DAT052_1 : TPTP v8.1.2. Released v5.0.0. % 0.00/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % 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 : Thu Aug 24 14:13:25 EDT 2023 % 0.13/0.35 % CPUTime : % 0.21/0.58 ________ _____ % 0.21/0.58 ___ __ \_________(_)________________________________ % 0.21/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.58 % 0.21/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.58 (2023-06-19) % 0.21/0.58 % 0.21/0.59 (c) Philipp Rümmer, 2009-2023 % 0.21/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.59 Amanda Stjerna. % 0.21/0.59 Free software under BSD-3-Clause. % 0.21/0.59 % 0.21/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.59 % 0.21/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.21/0.60 Running up to 7 provers in parallel. % 0.21/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.21/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 2.45/1.08 Prover 4: Preprocessing ... % 2.45/1.08 Prover 1: Preprocessing ... % 2.93/1.12 Prover 2: Preprocessing ... % 2.93/1.12 Prover 5: Preprocessing ... % 2.93/1.12 Prover 3: Preprocessing ... % 2.93/1.12 Prover 0: Preprocessing ... % 2.93/1.12 Prover 6: Preprocessing ... % 4.57/1.43 Prover 1: Constructing countermodel ... % 4.57/1.45 Prover 3: Constructing countermodel ... % 4.57/1.45 Prover 6: Constructing countermodel ... % 4.57/1.52 Prover 5: Proving ... % 5.33/1.53 Prover 2: Proving ... % 5.33/1.57 Prover 4: Constructing countermodel ... % 5.33/1.58 Prover 0: Proving ... % 7.89/1.87 Prover 3: proved (1263ms) % 7.89/1.87 % 7.89/1.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.89/1.87 % 7.89/1.87 Prover 6: stopped % 8.60/1.88 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 8.60/1.89 Prover 2: stopped % 8.66/1.90 Prover 0: stopped % 8.66/1.90 Prover 5: stopped % 8.80/1.91 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 8.80/1.91 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 8.80/1.91 Prover 7: Preprocessing ... % 8.80/1.91 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 8.80/1.92 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 8.80/1.95 Prover 8: Preprocessing ... % 8.80/1.95 Prover 10: Preprocessing ... % 8.80/1.96 Prover 11: Preprocessing ... % 8.80/1.98 Prover 13: Preprocessing ... % 9.51/2.01 Prover 7: Constructing countermodel ... % 9.51/2.02 Prover 10: Constructing countermodel ... % 9.51/2.03 Prover 8: Warning: ignoring some quantifiers % 9.51/2.03 Prover 8: Constructing countermodel ... % 9.51/2.06 Prover 13: Warning: ignoring some quantifiers % 9.51/2.07 Prover 13: Constructing countermodel ... % 10.14/2.12 Prover 11: Constructing countermodel ... % 10.14/2.27 Prover 10: Found proof (size 85) % 10.14/2.27 Prover 10: proved (366ms) % 10.14/2.27 Prover 11: stopped % 10.14/2.27 Prover 13: stopped % 10.14/2.27 Prover 8: stopped % 10.14/2.27 Prover 7: stopped % 10.14/2.27 Prover 1: stopped % 10.14/2.27 Prover 4: stopped % 10.14/2.27 % 10.14/2.27 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 10.14/2.27 % 10.14/2.29 % SZS output start Proof for theBenchmark % 10.14/2.29 Assumptions after simplification: % 10.14/2.29 --------------------------------- % 10.14/2.29 % 10.14/2.29 (ax11) % 10.14/2.30 ! [v0: record] : ! [v1: record] : ( ~ (split2(v0) = v1) | ~ record(v0) | ~ % 10.14/2.30 isrecord(v0) | isrecord(v1) | ? [v2: record] : (next(v0) = v2 & record(v2) % 10.14/2.30 & ~ isrecord(v2))) % 10.14/2.30 % 10.14/2.30 (ax12) % 10.14/2.31 ! [v0: record] : ! [v1: record] : ( ~ (split2(v0) = v1) | ~ record(v0) | ~ % 10.14/2.31 isrecord(v0) | ? [v2: record] : ? [v3: int] : ? [v4: int] : (next(v0) = % 10.14/2.31 v2 & record(v2) & ( ~ isrecord(v2) | (v4 = v3 & data(v2) = v3 & data(v1) = % 10.14/2.31 v3)))) % 10.14/2.31 % 10.14/2.31 (ax13) % 10.14/2.31 ! [v0: record] : ! [v1: record] : ( ~ (split2(v0) = v1) | ~ record(v0) | ~ % 10.14/2.31 isrecord(v0) | ? [v2: record] : ? [v3: record] : ? [v4: record] : ? [v5: % 10.14/2.31 record] : (next(v0) = v2 & record(v2) & ( ~ isrecord(v2) | (v5 = v3 & % 10.14/2.31 split2(v4) = v3 & next(v2) = v4 & next(v1) = v3 & record(v4) & % 10.14/2.31 record(v3))))) % 10.14/2.31 % 10.14/2.31 (ax3) % 10.14/2.31 ! [v0: record] : ! [v1: int] : ( ~ (length(v0) = v1) | ~ record(v0) | ~ % 10.14/2.31 isrecord(v0) | ? [v2: record] : (next(v0) = v2 & length(v2) = $sum(v1, -1) % 10.14/2.31 & record(v2))) % 10.14/2.31 % 10.14/2.31 (ax5) % 10.14/2.31 ! [v0: record] : ! [v1: record] : ( ~ (split1(v0) = v1) | ~ record(v0) | ~ % 10.14/2.31 isrecord(v0) | isrecord(v1)) % 10.14/2.31 % 10.14/2.31 (ax8) % 10.14/2.31 ! [v0: record] : ! [v1: record] : ( ~ (split1(v0) = v1) | ~ record(v0) | ~ % 10.14/2.31 isrecord(v0) | ? [v2: record] : ? [v3: record] : ? [v4: record] : ? [v5: % 10.14/2.31 record] : (next(v0) = v2 & record(v2) & ( ~ isrecord(v2) | (v5 = v3 & % 10.14/2.31 split1(v4) = v3 & next(v2) = v4 & next(v1) = v3 & record(v4) & % 10.14/2.31 record(v3))))) % 10.14/2.31 % 10.14/2.31 (co1) % 11.12/2.32 ? [v0: record] : ? [v1: record] : ? [v2: record] : ? [v3: record] : ? % 11.12/2.32 [v4: int] : ? [v5: record] : ? [v6: int] : ? [v7: record] : ? [v8: int] : % 11.12/2.32 ? [v9: record] : ? [v10: int] : ? [v11: int] : ( ~ ($difference(v11, v10) = % 11.12/2.32 v8) & split2(v1) = v5 & split2(v0) = v9 & split1(v1) = v3 & split1(v0) = % 11.12/2.32 v7 & next(v2) = v1 & next(v0) = v2 & length(v9) = v10 & length(v7) = v8 & % 11.12/2.32 length(v5) = v6 & length(v3) = v4 & length(v1) = $sum(v6, v4) & length(v0) = % 11.12/2.32 v11 & record(v9) & record(v7) & record(v5) & record(v3) & record(v2) & % 11.12/2.32 record(v1) & record(v0) & isrecord(v2) & isrecord(v0)) % 11.12/2.32 % 11.12/2.32 (function-axioms) % 11.12/2.32 ! [v0: record] : ! [v1: record] : ! [v2: record] : (v1 = v0 | ~ % 11.12/2.32 (split2(v2) = v1) | ~ (split2(v2) = v0)) & ! [v0: int] : ! [v1: int] : ! % 11.12/2.32 [v2: record] : (v1 = v0 | ~ (data(v2) = v1) | ~ (data(v2) = v0)) & ! [v0: % 11.12/2.32 record] : ! [v1: record] : ! [v2: record] : (v1 = v0 | ~ (split1(v2) = % 11.12/2.32 v1) | ~ (split1(v2) = v0)) & ! [v0: record] : ! [v1: record] : ! [v2: % 11.12/2.32 record] : (v1 = v0 | ~ (next(v2) = v1) | ~ (next(v2) = v0)) & ! [v0: int] % 11.12/2.32 : ! [v1: int] : ! [v2: record] : (v1 = v0 | ~ (length(v2) = v1) | ~ % 11.12/2.32 (length(v2) = v0)) % 11.12/2.32 % 11.12/2.32 Further assumptions not needed in the proof: % 11.12/2.32 -------------------------------------------- % 11.12/2.32 ax1, ax10, ax2, ax4, ax6, ax7, ax9 % 11.12/2.32 % 11.12/2.32 Those formulas are unsatisfiable: % 11.12/2.32 --------------------------------- % 11.12/2.32 % 11.12/2.32 Begin of proof % 11.12/2.32 | % 11.12/2.32 | ALPHA: (function-axioms) implies: % 11.12/2.33 | (1) ! [v0: int] : ! [v1: int] : ! [v2: record] : (v1 = v0 | ~ % 11.12/2.33 | (length(v2) = v1) | ~ (length(v2) = v0)) % 11.71/2.33 | (2) ! [v0: record] : ! [v1: record] : ! [v2: record] : (v1 = v0 | ~ % 11.71/2.33 | (next(v2) = v1) | ~ (next(v2) = v0)) % 11.71/2.33 | (3) ! [v0: record] : ! [v1: record] : ! [v2: record] : (v1 = v0 | ~ % 11.71/2.33 | (split1(v2) = v1) | ~ (split1(v2) = v0)) % 11.71/2.33 | (4) ! [v0: record] : ! [v1: record] : ! [v2: record] : (v1 = v0 | ~ % 11.71/2.33 | (split2(v2) = v1) | ~ (split2(v2) = v0)) % 11.71/2.33 | % 11.71/2.33 | DELTA: instantiating (co1) with fresh symbols all_18_0, all_18_1, all_18_2, % 11.71/2.33 | all_18_3, all_18_4, all_18_5, all_18_6, all_18_7, all_18_8, all_18_9, % 11.71/2.33 | all_18_10, all_18_11 gives: % 11.71/2.33 | (5) ~ ($difference(all_18_0, all_18_1) = all_18_3) & split2(all_18_10) = % 11.71/2.33 | all_18_6 & split2(all_18_11) = all_18_2 & split1(all_18_10) = all_18_8 % 11.71/2.33 | & split1(all_18_11) = all_18_4 & next(all_18_9) = all_18_10 & % 11.71/2.33 | next(all_18_11) = all_18_9 & length(all_18_2) = all_18_1 & % 11.71/2.33 | length(all_18_4) = all_18_3 & length(all_18_6) = all_18_5 & % 11.71/2.33 | length(all_18_8) = all_18_7 & length(all_18_10) = $sum(all_18_5, % 11.71/2.33 | all_18_7) & length(all_18_11) = all_18_0 & record(all_18_2) & % 11.71/2.33 | record(all_18_4) & record(all_18_6) & record(all_18_8) & % 11.71/2.33 | record(all_18_9) & record(all_18_10) & record(all_18_11) & % 11.71/2.33 | isrecord(all_18_9) & isrecord(all_18_11) % 11.71/2.33 | % 11.71/2.33 | ALPHA: (5) implies: % 11.71/2.33 | (6) ~ ($difference(all_18_0, all_18_1) = all_18_3) % 11.71/2.33 | (7) isrecord(all_18_11) % 11.71/2.33 | (8) isrecord(all_18_9) % 11.71/2.33 | (9) record(all_18_11) % 11.71/2.33 | (10) record(all_18_4) % 11.71/2.33 | (11) record(all_18_2) % 11.71/2.33 | (12) length(all_18_11) = all_18_0 % 11.71/2.33 | (13) length(all_18_10) = $sum(all_18_5, all_18_7) % 11.71/2.33 | (14) length(all_18_8) = all_18_7 % 11.71/2.33 | (15) length(all_18_6) = all_18_5 % 11.71/2.33 | (16) length(all_18_4) = all_18_3 % 11.71/2.33 | (17) length(all_18_2) = all_18_1 % 11.71/2.33 | (18) next(all_18_11) = all_18_9 % 11.71/2.34 | (19) next(all_18_9) = all_18_10 % 11.71/2.34 | (20) split1(all_18_11) = all_18_4 % 11.71/2.34 | (21) split1(all_18_10) = all_18_8 % 11.71/2.34 | (22) split2(all_18_11) = all_18_2 % 11.71/2.34 | (23) split2(all_18_10) = all_18_6 % 11.71/2.34 | % 11.71/2.34 | GROUND_INST: instantiating (ax3) with all_18_11, all_18_0, simplifying with % 11.71/2.34 | (7), (9), (12) gives: % 11.71/2.34 | (24) ? [v0: record] : (next(all_18_11) = v0 & length(v0) = $sum(all_18_0, % 11.71/2.34 | -1) & record(v0)) % 11.71/2.34 | % 11.71/2.34 | GROUND_INST: instantiating (ax5) with all_18_11, all_18_4, simplifying with % 11.71/2.34 | (7), (9), (20) gives: % 11.71/2.34 | (25) isrecord(all_18_4) % 11.71/2.34 | % 11.71/2.34 | GROUND_INST: instantiating (ax8) with all_18_11, all_18_4, simplifying with % 11.71/2.34 | (7), (9), (20) gives: % 11.71/2.34 | (26) ? [v0: record] : ? [v1: record] : ? [v2: record] : ? [v3: record] % 11.71/2.34 | : (next(all_18_11) = v0 & record(v0) & ( ~ isrecord(v0) | (v3 = v1 & % 11.71/2.34 | split1(v2) = v1 & next(v0) = v2 & next(all_18_4) = v1 & % 11.71/2.34 | record(v2) & record(v1)))) % 11.71/2.34 | % 11.71/2.34 | GROUND_INST: instantiating (ax11) with all_18_11, all_18_2, simplifying with % 11.71/2.34 | (7), (9), (22) gives: % 11.78/2.34 | (27) isrecord(all_18_2) | ? [v0: record] : (next(all_18_11) = v0 & % 11.78/2.34 | record(v0) & ~ isrecord(v0)) % 11.78/2.34 | % 11.78/2.34 | GROUND_INST: instantiating (ax13) with all_18_11, all_18_2, simplifying with % 11.78/2.34 | (7), (9), (22) gives: % 11.78/2.34 | (28) ? [v0: record] : ? [v1: record] : ? [v2: record] : ? [v3: record] % 11.78/2.34 | : (next(all_18_11) = v0 & record(v0) & ( ~ isrecord(v0) | (v3 = v1 & % 11.78/2.34 | split2(v2) = v1 & next(v0) = v2 & next(all_18_2) = v1 & % 11.78/2.34 | record(v2) & record(v1)))) % 11.78/2.34 | % 11.78/2.34 | GROUND_INST: instantiating (ax12) with all_18_11, all_18_2, simplifying with % 11.78/2.34 | (7), (9), (22) gives: % 11.78/2.34 | (29) ? [v0: record] : ? [v1: int] : ? [v2: int] : (next(all_18_11) = v0 % 11.78/2.34 | & record(v0) & ( ~ isrecord(v0) | (v2 = v1 & data(v0) = v1 & % 11.78/2.34 | data(all_18_2) = v1))) % 11.78/2.34 | % 11.78/2.34 | DELTA: instantiating (24) with fresh symbol all_27_0 gives: % 11.78/2.34 | (30) next(all_18_11) = all_27_0 & length(all_27_0) = $sum(all_18_0, -1) & % 11.78/2.34 | record(all_27_0) % 11.78/2.34 | % 11.78/2.34 | ALPHA: (30) implies: % 11.78/2.34 | (31) record(all_27_0) % 11.78/2.34 | (32) length(all_27_0) = $sum(all_18_0, -1) % 11.78/2.34 | (33) next(all_18_11) = all_27_0 % 11.78/2.34 | % 11.78/2.34 | DELTA: instantiating (29) with fresh symbols all_29_0, all_29_1, all_29_2 % 11.78/2.34 | gives: % 11.78/2.35 | (34) next(all_18_11) = all_29_2 & record(all_29_2) & ( ~ isrecord(all_29_2) % 11.78/2.35 | | (all_29_0 = all_29_1 & data(all_29_2) = all_29_1 & data(all_18_2) % 11.78/2.35 | = all_29_1)) % 11.78/2.35 | % 11.78/2.35 | ALPHA: (34) implies: % 11.78/2.35 | (35) next(all_18_11) = all_29_2 % 11.78/2.35 | % 11.78/2.35 | DELTA: instantiating (26) with fresh symbols all_32_0, all_32_1, all_32_2, % 11.78/2.35 | all_32_3 gives: % 11.78/2.35 | (36) next(all_18_11) = all_32_3 & record(all_32_3) & ( ~ isrecord(all_32_3) % 11.78/2.35 | | (all_32_0 = all_32_2 & split1(all_32_1) = all_32_2 & % 11.78/2.35 | next(all_32_3) = all_32_1 & next(all_18_4) = all_32_2 & % 11.78/2.35 | record(all_32_1) & record(all_32_2))) % 11.78/2.35 | % 11.78/2.35 | ALPHA: (36) implies: % 11.78/2.35 | (37) next(all_18_11) = all_32_3 % 11.78/2.35 | (38) ~ isrecord(all_32_3) | (all_32_0 = all_32_2 & split1(all_32_1) = % 11.78/2.35 | all_32_2 & next(all_32_3) = all_32_1 & next(all_18_4) = all_32_2 & % 11.78/2.35 | record(all_32_1) & record(all_32_2)) % 11.78/2.35 | % 11.78/2.35 | DELTA: instantiating (28) with fresh symbols all_34_0, all_34_1, all_34_2, % 11.78/2.35 | all_34_3 gives: % 11.78/2.35 | (39) next(all_18_11) = all_34_3 & record(all_34_3) & ( ~ isrecord(all_34_3) % 11.78/2.35 | | (all_34_0 = all_34_2 & split2(all_34_1) = all_34_2 & % 11.78/2.35 | next(all_34_3) = all_34_1 & next(all_18_2) = all_34_2 & % 11.78/2.35 | record(all_34_1) & record(all_34_2))) % 11.78/2.35 | % 11.78/2.35 | ALPHA: (39) implies: % 11.78/2.35 | (40) next(all_18_11) = all_34_3 % 11.78/2.35 | (41) ~ isrecord(all_34_3) | (all_34_0 = all_34_2 & split2(all_34_1) = % 11.78/2.35 | all_34_2 & next(all_34_3) = all_34_1 & next(all_18_2) = all_34_2 & % 11.78/2.35 | record(all_34_1) & record(all_34_2)) % 11.78/2.35 | % 11.78/2.35 | GROUND_INST: instantiating (2) with all_18_9, all_32_3, all_18_11, simplifying % 11.78/2.35 | with (18), (37) gives: % 11.78/2.35 | (42) all_32_3 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | GROUND_INST: instantiating (2) with all_29_2, all_32_3, all_18_11, simplifying % 11.78/2.35 | with (35), (37) gives: % 11.78/2.35 | (43) all_32_3 = all_29_2 % 11.78/2.35 | % 11.78/2.35 | GROUND_INST: instantiating (2) with all_29_2, all_34_3, all_18_11, simplifying % 11.78/2.35 | with (35), (40) gives: % 11.78/2.35 | (44) all_34_3 = all_29_2 % 11.78/2.35 | % 11.78/2.35 | GROUND_INST: instantiating (2) with all_27_0, all_34_3, all_18_11, simplifying % 11.78/2.35 | with (33), (40) gives: % 11.78/2.35 | (45) all_34_3 = all_27_0 % 11.78/2.35 | % 11.78/2.35 | COMBINE_EQS: (44), (45) imply: % 11.78/2.35 | (46) all_29_2 = all_27_0 % 11.78/2.35 | % 11.78/2.35 | SIMP: (46) implies: % 11.78/2.35 | (47) all_29_2 = all_27_0 % 11.78/2.35 | % 11.78/2.35 | COMBINE_EQS: (42), (43) imply: % 11.78/2.35 | (48) all_29_2 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | SIMP: (48) implies: % 11.78/2.35 | (49) all_29_2 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | COMBINE_EQS: (47), (49) imply: % 11.78/2.35 | (50) all_27_0 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | SIMP: (50) implies: % 11.78/2.35 | (51) all_27_0 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | COMBINE_EQS: (45), (51) imply: % 11.78/2.35 | (52) all_34_3 = all_18_9 % 11.78/2.35 | % 11.78/2.35 | REDUCE: (32), (51) imply: % 11.78/2.35 | (53) length(all_18_9) = $sum(all_18_0, -1) % 11.78/2.35 | % 11.78/2.35 | REDUCE: (31), (51) imply: % 11.78/2.35 | (54) record(all_18_9) % 11.78/2.35 | % 11.78/2.35 | BETA: splitting (27) gives: % 11.78/2.35 | % 11.78/2.35 | Case 1: % 11.78/2.35 | | % 11.78/2.35 | | (55) isrecord(all_18_2) % 11.78/2.35 | | % 11.78/2.35 | | BETA: splitting (41) gives: % 11.78/2.35 | | % 11.78/2.35 | | Case 1: % 11.78/2.35 | | | % 11.78/2.35 | | | (56) ~ isrecord(all_34_3) % 11.78/2.35 | | | % 11.78/2.35 | | | REDUCE: (52), (56) imply: % 11.78/2.35 | | | (57) ~ isrecord(all_18_9) % 11.78/2.35 | | | % 11.78/2.35 | | | PRED_UNIFY: (8), (57) imply: % 11.78/2.35 | | | (58) $false % 11.78/2.36 | | | % 11.78/2.36 | | | CLOSE: (58) is inconsistent. % 11.78/2.36 | | | % 11.78/2.36 | | Case 2: % 11.78/2.36 | | | % 11.78/2.36 | | | (59) isrecord(all_34_3) % 11.78/2.36 | | | (60) all_34_0 = all_34_2 & split2(all_34_1) = all_34_2 & next(all_34_3) % 11.78/2.36 | | | = all_34_1 & next(all_18_2) = all_34_2 & record(all_34_1) & % 11.78/2.36 | | | record(all_34_2) % 11.78/2.36 | | | % 11.78/2.36 | | | ALPHA: (60) implies: % 11.78/2.36 | | | (61) next(all_18_2) = all_34_2 % 11.78/2.36 | | | (62) next(all_34_3) = all_34_1 % 11.78/2.36 | | | (63) split2(all_34_1) = all_34_2 % 11.78/2.36 | | | % 11.78/2.36 | | | REDUCE: (52), (62) imply: % 11.78/2.36 | | | (64) next(all_18_9) = all_34_1 % 11.78/2.36 | | | % 11.78/2.36 | | | BETA: splitting (38) gives: % 11.78/2.36 | | | % 11.78/2.36 | | | Case 1: % 11.78/2.36 | | | | % 11.78/2.36 | | | | (65) ~ isrecord(all_32_3) % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (42), (65) imply: % 11.78/2.36 | | | | (66) ~ isrecord(all_18_9) % 11.78/2.36 | | | | % 11.78/2.36 | | | | PRED_UNIFY: (8), (66) imply: % 11.78/2.36 | | | | (67) $false % 11.78/2.36 | | | | % 11.78/2.36 | | | | CLOSE: (67) is inconsistent. % 11.78/2.36 | | | | % 11.78/2.36 | | | Case 2: % 11.78/2.36 | | | | % 11.78/2.36 | | | | (68) isrecord(all_32_3) % 11.78/2.36 | | | | (69) all_32_0 = all_32_2 & split1(all_32_1) = all_32_2 & % 11.78/2.36 | | | | next(all_32_3) = all_32_1 & next(all_18_4) = all_32_2 & % 11.78/2.36 | | | | record(all_32_1) & record(all_32_2) % 11.78/2.36 | | | | % 11.78/2.36 | | | | ALPHA: (69) implies: % 11.78/2.36 | | | | (70) next(all_18_4) = all_32_2 % 11.78/2.36 | | | | (71) next(all_32_3) = all_32_1 % 11.78/2.36 | | | | (72) split1(all_32_1) = all_32_2 % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (42), (71) imply: % 11.78/2.36 | | | | (73) next(all_18_9) = all_32_1 % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (2) with all_18_10, all_34_1, all_18_9, % 11.78/2.36 | | | | simplifying with (19), (64) gives: % 11.78/2.36 | | | | (74) all_34_1 = all_18_10 % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (2) with all_32_1, all_34_1, all_18_9, % 11.78/2.36 | | | | simplifying with (64), (73) gives: % 11.78/2.36 | | | | (75) all_34_1 = all_32_1 % 11.78/2.36 | | | | % 11.78/2.36 | | | | COMBINE_EQS: (74), (75) imply: % 11.78/2.36 | | | | (76) all_32_1 = all_18_10 % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (63), (74) imply: % 11.78/2.36 | | | | (77) split2(all_18_10) = all_34_2 % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (72), (76) imply: % 11.78/2.36 | | | | (78) split1(all_18_10) = all_32_2 % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (3) with all_18_8, all_32_2, all_18_10, % 11.78/2.36 | | | | simplifying with (21), (78) gives: % 11.78/2.36 | | | | (79) all_32_2 = all_18_8 % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (4) with all_18_6, all_34_2, all_18_10, % 11.78/2.36 | | | | simplifying with (23), (77) gives: % 11.78/2.36 | | | | (80) all_34_2 = all_18_6 % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (61), (80) imply: % 11.78/2.36 | | | | (81) next(all_18_2) = all_18_6 % 11.78/2.36 | | | | % 11.78/2.36 | | | | REDUCE: (70), (79) imply: % 11.78/2.36 | | | | (82) next(all_18_4) = all_18_8 % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (ax3) with all_18_4, all_18_3, simplifying % 11.78/2.36 | | | | with (10), (16), (25) gives: % 11.78/2.36 | | | | (83) ? [v0: record] : (next(all_18_4) = v0 & length(v0) = % 11.78/2.36 | | | | $sum(all_18_3, -1) & record(v0)) % 11.78/2.36 | | | | % 11.78/2.36 | | | | GROUND_INST: instantiating (ax3) with all_18_2, all_18_1, simplifying % 11.78/2.36 | | | | with (11), (17), (55) gives: % 11.78/2.37 | | | | (84) ? [v0: record] : (next(all_18_2) = v0 & length(v0) = % 11.78/2.37 | | | | $sum(all_18_1, -1) & record(v0)) % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (ax3) with all_18_9, $sum(all_18_0, -1), % 11.78/2.37 | | | | simplifying with (8), (53), (54) gives: % 11.78/2.37 | | | | (85) ? [v0: record] : (next(all_18_9) = v0 & length(v0) = % 11.78/2.37 | | | | $sum(all_18_0, -2) & record(v0)) % 11.78/2.37 | | | | % 11.78/2.37 | | | | DELTA: instantiating (84) with fresh symbol all_71_0 gives: % 11.78/2.37 | | | | (86) next(all_18_2) = all_71_0 & length(all_71_0) = $sum(all_18_1, % 11.78/2.37 | | | | -1) & record(all_71_0) % 11.78/2.37 | | | | % 11.78/2.37 | | | | ALPHA: (86) implies: % 11.78/2.37 | | | | (87) length(all_71_0) = $sum(all_18_1, -1) % 11.78/2.37 | | | | (88) next(all_18_2) = all_71_0 % 11.78/2.37 | | | | % 11.78/2.37 | | | | DELTA: instantiating (83) with fresh symbol all_73_0 gives: % 11.78/2.37 | | | | (89) next(all_18_4) = all_73_0 & length(all_73_0) = $sum(all_18_3, % 11.78/2.37 | | | | -1) & record(all_73_0) % 11.78/2.37 | | | | % 11.78/2.37 | | | | ALPHA: (89) implies: % 11.78/2.37 | | | | (90) length(all_73_0) = $sum(all_18_3, -1) % 11.78/2.37 | | | | (91) next(all_18_4) = all_73_0 % 11.78/2.37 | | | | % 11.78/2.37 | | | | DELTA: instantiating (85) with fresh symbol all_77_0 gives: % 11.78/2.37 | | | | (92) next(all_18_9) = all_77_0 & length(all_77_0) = $sum(all_18_0, % 11.78/2.37 | | | | -2) & record(all_77_0) % 11.78/2.37 | | | | % 11.78/2.37 | | | | ALPHA: (92) implies: % 11.78/2.37 | | | | (93) length(all_77_0) = $sum(all_18_0, -2) % 11.78/2.37 | | | | (94) next(all_18_9) = all_77_0 % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (2) with all_18_10, all_77_0, all_18_9, % 11.78/2.37 | | | | simplifying with (19), (94) gives: % 11.78/2.37 | | | | (95) all_77_0 = all_18_10 % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (2) with all_18_8, all_73_0, all_18_4, % 11.78/2.37 | | | | simplifying with (82), (91) gives: % 11.78/2.37 | | | | (96) all_73_0 = all_18_8 % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (2) with all_18_6, all_71_0, all_18_2, % 11.78/2.37 | | | | simplifying with (81), (88) gives: % 11.78/2.37 | | | | (97) all_71_0 = all_18_6 % 11.78/2.37 | | | | % 11.78/2.37 | | | | REDUCE: (93), (95) imply: % 11.78/2.37 | | | | (98) length(all_18_10) = $sum(all_18_0, -2) % 11.78/2.37 | | | | % 11.78/2.37 | | | | REDUCE: (90), (96) imply: % 11.78/2.37 | | | | (99) length(all_18_8) = $sum(all_18_3, -1) % 11.78/2.37 | | | | % 11.78/2.37 | | | | REDUCE: (87), (97) imply: % 11.78/2.37 | | | | (100) length(all_18_6) = $sum(all_18_1, -1) % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (1) with $sum(all_18_5, all_18_7), % 11.78/2.37 | | | | $sum(all_18_0, -2), all_18_10, simplifying with (13), (98) % 11.78/2.37 | | | | gives: % 11.78/2.37 | | | | (101) $difference($difference(all_18_0, all_18_5), all_18_7) = 2 % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (1) with all_18_7, $sum(all_18_3, -1), % 11.78/2.37 | | | | all_18_8, simplifying with (14), (99) gives: % 11.78/2.37 | | | | (102) $difference(all_18_3, all_18_7) = 1 % 11.78/2.37 | | | | % 11.78/2.37 | | | | GROUND_INST: instantiating (1) with all_18_5, $sum(all_18_1, -1), % 11.78/2.37 | | | | all_18_6, simplifying with (15), (100) gives: % 11.78/2.37 | | | | (103) $difference(all_18_1, all_18_5) = 1 % 11.78/2.37 | | | | % 11.78/2.37 | | | | REDUCE: (6), (101), (102), (103) imply: % 11.78/2.37 | | | | (104) $false % 11.78/2.37 | | | | % 11.78/2.37 | | | | CLOSE: (104) is inconsistent. % 11.78/2.37 | | | | % 11.78/2.37 | | | End of split % 11.78/2.37 | | | % 11.78/2.37 | | End of split % 11.78/2.37 | | % 11.78/2.37 | Case 2: % 11.78/2.37 | | % 11.78/2.38 | | (105) ? [v0: record] : (next(all_18_11) = v0 & record(v0) & ~ % 11.78/2.38 | | isrecord(v0)) % 11.78/2.38 | | % 11.78/2.38 | | DELTA: instantiating (105) with fresh symbol all_44_0 gives: % 11.78/2.38 | | (106) next(all_18_11) = all_44_0 & record(all_44_0) & ~ % 11.78/2.38 | | isrecord(all_44_0) % 11.78/2.38 | | % 11.78/2.38 | | ALPHA: (106) implies: % 11.78/2.38 | | (107) ~ isrecord(all_44_0) % 11.78/2.38 | | (108) next(all_18_11) = all_44_0 % 11.78/2.38 | | % 11.78/2.38 | | GROUND_INST: instantiating (2) with all_18_9, all_44_0, all_18_11, % 11.78/2.38 | | simplifying with (18), (108) gives: % 11.78/2.38 | | (109) all_44_0 = all_18_9 % 11.78/2.38 | | % 11.78/2.38 | | REDUCE: (107), (109) imply: % 11.78/2.38 | | (110) ~ isrecord(all_18_9) % 11.78/2.38 | | % 11.78/2.38 | | PRED_UNIFY: (8), (110) imply: % 11.78/2.38 | | (111) $false % 11.78/2.38 | | % 11.78/2.38 | | CLOSE: (111) is inconsistent. % 11.78/2.38 | | % 11.78/2.38 | End of split % 11.78/2.38 | % 11.78/2.38 End of proof % 11.78/2.38 % SZS output end Proof for theBenchmark % 11.78/2.38 % 11.78/2.38 1791ms %------------------------------------------------------------------------------