%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : DAT005_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 : n029.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Aug 30 22:18:51 EDT 2023 % Result : Theorem 4.32s 1.40s % Output : Proof 5.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : DAT005_1 : TPTP v8.1.2. Released v5.0.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Aug 24 14:33:08 EDT 2023 % 0.12/0.34 % CPUTime : % 0.19/0.66 ________ _____ % 0.19/0.66 ___ __ \_________(_)________________________________ % 0.19/0.66 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.66 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.66 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.66 % 0.19/0.66 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.66 (2023-06-19) % 0.19/0.66 % 0.19/0.66 (c) Philipp Rümmer, 2009-2023 % 0.19/0.66 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.66 Amanda Stjerna. % 0.19/0.66 Free software under BSD-3-Clause. % 0.19/0.66 % 0.19/0.66 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.66 % 0.19/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.19/0.68 Running up to 7 provers in parallel. % 0.19/0.70 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.70 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.70 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.70 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.70 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.70 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.70 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.28/1.06 Prover 4: Preprocessing ... % 2.28/1.06 Prover 1: Preprocessing ... % 2.81/1.10 Prover 2: Preprocessing ... % 2.81/1.10 Prover 6: Preprocessing ... % 2.81/1.10 Prover 3: Preprocessing ... % 2.81/1.10 Prover 5: Preprocessing ... % 2.81/1.10 Prover 0: Preprocessing ... % 3.41/1.18 Prover 6: Constructing countermodel ... % 3.41/1.19 Prover 4: Constructing countermodel ... % 3.41/1.20 Prover 0: Proving ... % 3.41/1.20 Prover 3: Constructing countermodel ... % 3.41/1.20 Prover 1: Constructing countermodel ... % 3.41/1.21 Prover 2: Proving ... % 3.41/1.21 Prover 5: Proving ... % 4.32/1.40 Prover 3: proved (701ms) % 4.32/1.40 % 4.32/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.32/1.40 % 4.32/1.40 Prover 6: stopped % 4.32/1.40 Prover 0: stopped % 4.32/1.40 Prover 5: stopped % 4.32/1.40 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 4.32/1.40 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 4.32/1.41 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 4.32/1.41 Prover 2: stopped % 4.32/1.41 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 4.32/1.41 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 5.04/1.42 Prover 7: Preprocessing ... % 5.04/1.43 Prover 13: Preprocessing ... % 5.04/1.43 Prover 8: Preprocessing ... % 5.04/1.44 Prover 10: Preprocessing ... % 5.04/1.44 Prover 11: Preprocessing ... % 5.04/1.46 Prover 8: Warning: ignoring some quantifiers % 5.04/1.46 Prover 8: Constructing countermodel ... % 5.04/1.46 Prover 10: Constructing countermodel ... % 5.04/1.47 Prover 11: Constructing countermodel ... % 5.04/1.48 Prover 7: Constructing countermodel ... % 5.04/1.48 Prover 13: Warning: ignoring some quantifiers % 5.04/1.48 Prover 13: Constructing countermodel ... % 5.04/1.50 Prover 4: Found proof (size 57) % 5.04/1.50 Prover 4: proved (808ms) % 5.04/1.51 Prover 7: stopped % 5.04/1.51 Prover 13: stopped % 5.04/1.51 Prover 8: stopped % 5.04/1.51 Prover 1: stopped % 5.04/1.51 Prover 11: stopped % 5.04/1.51 Prover 10: stopped % 5.04/1.51 % 5.04/1.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.04/1.51 % 5.04/1.52 % SZS output start Proof for theBenchmark % 5.04/1.52 Assumptions after simplification: % 5.04/1.52 --------------------------------- % 5.04/1.52 % 5.04/1.52 (ax1) % 5.04/1.55 ! [v0: array] : ! [v1: int] : ! [v2: int] : ! [v3: array] : ( ~ (write(v0, % 5.04/1.55 v1, v2) = v3) | ~ array(v0) | read(v3, v1) = v2) % 5.04/1.55 % 5.04/1.55 (ax2) % 5.04/1.55 ! [v0: array] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: array] : % 5.04/1.55 ! [v5: int] : (v2 = v1 | ~ (write(v0, v1, v3) = v4) | ~ (read(v4, v2) = v5) % 5.04/1.55 | ~ array(v0) | read(v0, v2) = v5) % 5.04/1.55 % 5.04/1.55 (co1) % 5.04/1.55 ? [v0: array] : ? [v1: array] : ? [v2: int] : ? [v3: array] : ? [v4: % 5.04/1.55 array] : ? [v5: array] : ? [v6: int] : ($lesseq(v2, 4) & $lesseq(3, v2) & % 5.04/1.55 write(v5, 4, 44) = v0 & write(v4, 5, 55) = v5 & write(v3, 4, 444) = v4 & % 5.04/1.55 write(v1, 3, 33) = v3 & read(v0, v2) = v6 & array(v5) & array(v4) & % 5.04/1.55 array(v3) & array(v1) & array(v0) & ( ~ ($lesseq(v6, 44)) | ~ ($lesseq(33, % 5.04/1.55 v6)))) % 5.04/1.55 % 5.04/1.55 (function-axioms) % 5.04/1.56 ! [v0: array] : ! [v1: array] : ! [v2: int] : ! [v3: int] : ! [v4: array] % 5.04/1.56 : (v1 = v0 | ~ (write(v4, v3, v2) = v1) | ~ (write(v4, v3, v2) = v0)) & ! % 5.04/1.56 [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: array] : (v1 = v0 | ~ % 5.04/1.56 (read(v3, v2) = v1) | ~ (read(v3, v2) = v0)) % 5.04/1.56 % 5.04/1.56 Those formulas are unsatisfiable: % 5.04/1.56 --------------------------------- % 5.04/1.56 % 5.04/1.56 Begin of proof % 5.04/1.56 | % 5.04/1.56 | ALPHA: (function-axioms) implies: % 5.04/1.56 | (1) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: array] : (v1 = v0 % 5.04/1.56 | | ~ (read(v3, v2) = v1) | ~ (read(v3, v2) = v0)) % 5.04/1.56 | % 5.04/1.56 | DELTA: instantiating (co1) with fresh symbols all_7_0, all_7_1, all_7_2, % 5.04/1.56 | all_7_3, all_7_4, all_7_5, all_7_6 gives: % 5.04/1.56 | (2) $lesseq(all_7_4, 4) & $lesseq(3, all_7_4) & write(all_7_1, 4, 44) = % 5.04/1.56 | all_7_6 & write(all_7_2, 5, 55) = all_7_1 & write(all_7_3, 4, 444) = % 5.04/1.56 | all_7_2 & write(all_7_5, 3, 33) = all_7_3 & read(all_7_6, all_7_4) = % 5.04/1.56 | all_7_0 & array(all_7_1) & array(all_7_2) & array(all_7_3) & % 5.04/1.56 | array(all_7_5) & array(all_7_6) & ( ~ ($lesseq(all_7_0, 44)) | ~ % 5.04/1.56 | ($lesseq(33, all_7_0))) % 5.04/1.56 | % 5.04/1.56 | ALPHA: (2) implies: % 5.04/1.57 | (3) $lesseq(3, all_7_4) % 5.04/1.57 | (4) $lesseq(all_7_4, 4) % 5.04/1.57 | (5) array(all_7_5) % 5.04/1.57 | (6) array(all_7_3) % 5.04/1.57 | (7) array(all_7_2) % 5.04/1.57 | (8) array(all_7_1) % 5.04/1.57 | (9) read(all_7_6, all_7_4) = all_7_0 % 5.04/1.57 | (10) write(all_7_5, 3, 33) = all_7_3 % 5.04/1.57 | (11) write(all_7_3, 4, 444) = all_7_2 % 5.04/1.57 | (12) write(all_7_2, 5, 55) = all_7_1 % 5.04/1.57 | (13) write(all_7_1, 4, 44) = all_7_6 % 5.04/1.57 | (14) ~ ($lesseq(all_7_0, 44)) | ~ ($lesseq(33, all_7_0)) % 5.04/1.57 | % 5.04/1.57 | GROUND_INST: instantiating (ax1) with all_7_5, 3, 33, all_7_3, simplifying % 5.04/1.57 | with (5), (10) gives: % 5.04/1.57 | (15) read(all_7_3, 3) = 33 % 5.04/1.57 | % 5.04/1.57 | GROUND_INST: instantiating (ax2) with all_7_1, 4, all_7_4, 44, all_7_6, % 5.04/1.57 | all_7_0, simplifying with (8), (9), (13) gives: % 5.04/1.57 | (16) all_7_4 = 4 | read(all_7_1, all_7_4) = all_7_0 % 5.04/1.57 | % 5.04/1.57 | GROUND_INST: instantiating (ax1) with all_7_1, 4, 44, all_7_6, simplifying % 5.04/1.57 | with (8), (13) gives: % 5.04/1.57 | (17) read(all_7_6, 4) = 44 % 5.04/1.57 | % 5.04/1.57 | GROUND_INST: instantiating (1) with all_7_0, 44, 4, all_7_6, simplifying with % 5.04/1.57 | (17) gives: % 5.04/1.57 | (18) all_7_0 = 44 | ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.57 | % 5.04/1.57 | BETA: splitting (14) gives: % 5.04/1.57 | % 5.04/1.57 | Case 1: % 5.04/1.57 | | % 5.04/1.57 | | (19) $lesseq(45, all_7_0) % 5.04/1.57 | | % 5.04/1.57 | | BETA: splitting (16) gives: % 5.04/1.57 | | % 5.04/1.57 | | Case 1: % 5.04/1.57 | | | % 5.04/1.57 | | | (20) read(all_7_1, all_7_4) = all_7_0 % 5.04/1.57 | | | % 5.04/1.58 | | | GROUND_INST: instantiating (ax2) with all_7_2, 5, all_7_4, 55, all_7_1, % 5.04/1.58 | | | all_7_0, simplifying with (7), (12), (20) gives: % 5.04/1.58 | | | (21) all_7_4 = 5 | read(all_7_2, all_7_4) = all_7_0 % 5.04/1.58 | | | % 5.04/1.58 | | | BETA: splitting (18) gives: % 5.04/1.58 | | | % 5.04/1.58 | | | Case 1: % 5.04/1.58 | | | | % 5.04/1.58 | | | | (22) ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.58 | | | | % 5.04/1.58 | | | | BETA: splitting (21) gives: % 5.04/1.58 | | | | % 5.04/1.58 | | | | Case 1: % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | (23) read(all_7_2, all_7_4) = all_7_0 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | PRED_UNIFY: (9), (22) imply: % 5.04/1.58 | | | | | (24) ~ (all_7_4 = 4) % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | STRENGTHEN: (4), (24) imply: % 5.04/1.58 | | | | | (25) $lesseq(all_7_4, 3) % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | ANTI_SYMM: (3), (25) imply: % 5.04/1.58 | | | | | (26) all_7_4 = 3 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | REDUCE: (23), (26) imply: % 5.04/1.58 | | | | | (27) read(all_7_2, 3) = all_7_0 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | GROUND_INST: instantiating (ax2) with all_7_3, 4, 3, 444, all_7_2, % 5.04/1.58 | | | | | all_7_0, simplifying with (6), (11), (27) gives: % 5.04/1.58 | | | | | (28) read(all_7_3, 3) = all_7_0 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | GROUND_INST: instantiating (1) with 33, all_7_0, 3, all_7_3, % 5.04/1.58 | | | | | simplifying with (15), (28) gives: % 5.04/1.58 | | | | | (29) all_7_0 = 33 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | REDUCE: (19), (29) imply: % 5.04/1.58 | | | | | (30) $false % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | CLOSE: (30) is inconsistent. % 5.04/1.58 | | | | | % 5.04/1.58 | | | | Case 2: % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | (31) all_7_4 = 5 % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | REDUCE: (4), (31) imply: % 5.04/1.58 | | | | | (32) $false % 5.04/1.58 | | | | | % 5.04/1.58 | | | | | CLOSE: (32) is inconsistent. % 5.04/1.58 | | | | | % 5.04/1.58 | | | | End of split % 5.04/1.58 | | | | % 5.04/1.58 | | | Case 2: % 5.04/1.58 | | | | % 5.04/1.58 | | | | (33) all_7_0 = 44 % 5.04/1.58 | | | | % 5.04/1.58 | | | | REDUCE: (19), (33) imply: % 5.04/1.58 | | | | (34) $false % 5.04/1.58 | | | | % 5.04/1.58 | | | | CLOSE: (34) is inconsistent. % 5.04/1.58 | | | | % 5.04/1.58 | | | End of split % 5.04/1.58 | | | % 5.04/1.58 | | Case 2: % 5.04/1.58 | | | % 5.04/1.58 | | | (35) all_7_4 = 4 % 5.04/1.58 | | | % 5.04/1.58 | | | REDUCE: (9), (35) imply: % 5.04/1.58 | | | (36) read(all_7_6, 4) = all_7_0 % 5.04/1.58 | | | % 5.04/1.58 | | | BETA: splitting (18) gives: % 5.04/1.58 | | | % 5.04/1.58 | | | Case 1: % 5.04/1.58 | | | | % 5.04/1.58 | | | | (37) ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.58 | | | | % 5.04/1.58 | | | | PRED_UNIFY: (36), (37) imply: % 5.04/1.58 | | | | (38) $false % 5.04/1.58 | | | | % 5.04/1.58 | | | | CLOSE: (38) is inconsistent. % 5.04/1.58 | | | | % 5.04/1.58 | | | Case 2: % 5.04/1.58 | | | | % 5.04/1.58 | | | | (39) all_7_0 = 44 % 5.04/1.58 | | | | % 5.04/1.58 | | | | REDUCE: (19), (39) imply: % 5.04/1.58 | | | | (40) $false % 5.04/1.58 | | | | % 5.04/1.58 | | | | CLOSE: (40) is inconsistent. % 5.04/1.58 | | | | % 5.04/1.58 | | | End of split % 5.04/1.58 | | | % 5.04/1.58 | | End of split % 5.04/1.58 | | % 5.04/1.58 | Case 2: % 5.04/1.58 | | % 5.04/1.58 | | (41) $lesseq(all_7_0, 32) % 5.04/1.58 | | % 5.04/1.58 | | BETA: splitting (16) gives: % 5.04/1.58 | | % 5.04/1.58 | | Case 1: % 5.04/1.58 | | | % 5.04/1.59 | | | (42) read(all_7_1, all_7_4) = all_7_0 % 5.04/1.59 | | | % 5.04/1.59 | | | GROUND_INST: instantiating (ax2) with all_7_2, 5, all_7_4, 55, all_7_1, % 5.04/1.59 | | | all_7_0, simplifying with (7), (12), (42) gives: % 5.04/1.59 | | | (43) all_7_4 = 5 | read(all_7_2, all_7_4) = all_7_0 % 5.04/1.59 | | | % 5.04/1.59 | | | BETA: splitting (18) gives: % 5.04/1.59 | | | % 5.04/1.59 | | | Case 1: % 5.04/1.59 | | | | % 5.04/1.59 | | | | (44) ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.59 | | | | % 5.04/1.59 | | | | BETA: splitting (43) gives: % 5.04/1.59 | | | | % 5.04/1.59 | | | | Case 1: % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | (45) read(all_7_2, all_7_4) = all_7_0 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | PRED_UNIFY: (9), (44) imply: % 5.04/1.59 | | | | | (46) ~ (all_7_4 = 4) % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | STRENGTHEN: (4), (46) imply: % 5.04/1.59 | | | | | (47) $lesseq(all_7_4, 3) % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | ANTI_SYMM: (3), (47) imply: % 5.04/1.59 | | | | | (48) all_7_4 = 3 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | REDUCE: (45), (48) imply: % 5.04/1.59 | | | | | (49) read(all_7_2, 3) = all_7_0 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | GROUND_INST: instantiating (ax2) with all_7_3, 4, 3, 444, all_7_2, % 5.04/1.59 | | | | | all_7_0, simplifying with (6), (11), (49) gives: % 5.04/1.59 | | | | | (50) read(all_7_3, 3) = all_7_0 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | GROUND_INST: instantiating (1) with 33, all_7_0, 3, all_7_3, % 5.04/1.59 | | | | | simplifying with (15), (50) gives: % 5.04/1.59 | | | | | (51) all_7_0 = 33 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | REDUCE: (41), (51) imply: % 5.04/1.59 | | | | | (52) $false % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | CLOSE: (52) is inconsistent. % 5.04/1.59 | | | | | % 5.04/1.59 | | | | Case 2: % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | (53) all_7_4 = 5 % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | REDUCE: (4), (53) imply: % 5.04/1.59 | | | | | (54) $false % 5.04/1.59 | | | | | % 5.04/1.59 | | | | | CLOSE: (54) is inconsistent. % 5.04/1.59 | | | | | % 5.04/1.59 | | | | End of split % 5.04/1.59 | | | | % 5.04/1.59 | | | Case 2: % 5.04/1.59 | | | | % 5.04/1.59 | | | | (55) read(all_7_6, 4) = all_7_0 % 5.04/1.59 | | | | % 5.04/1.59 | | | | REF_CLOSE: (18), (41), (55) are inconsistent by sub-proof #1. % 5.04/1.59 | | | | % 5.04/1.59 | | | End of split % 5.04/1.59 | | | % 5.04/1.59 | | Case 2: % 5.04/1.59 | | | % 5.04/1.59 | | | (56) all_7_4 = 4 % 5.04/1.59 | | | % 5.04/1.59 | | | REDUCE: (9), (56) imply: % 5.04/1.59 | | | (57) read(all_7_6, 4) = all_7_0 % 5.04/1.59 | | | % 5.04/1.59 | | | REF_CLOSE: (18), (41), (57) are inconsistent by sub-proof #1. % 5.04/1.59 | | | % 5.04/1.59 | | End of split % 5.04/1.59 | | % 5.04/1.59 | End of split % 5.04/1.59 | % 5.04/1.59 End of proof % 5.04/1.59 % 5.04/1.59 Sub-proof #1 shows that the following formulas are inconsistent: % 5.04/1.59 ---------------------------------------------------------------- % 5.04/1.59 (1) all_7_0 = 44 | ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.59 (2) read(all_7_6, 4) = all_7_0 % 5.04/1.60 (3) $lesseq(all_7_0, 32) % 5.04/1.60 % 5.04/1.60 Begin of proof % 5.04/1.60 | % 5.04/1.60 | BETA: splitting (1) gives: % 5.04/1.60 | % 5.04/1.60 | Case 1: % 5.04/1.60 | | % 5.04/1.60 | | (4) ~ (read(all_7_6, 4) = all_7_0) % 5.04/1.60 | | % 5.04/1.60 | | PRED_UNIFY: (2), (4) imply: % 5.04/1.60 | | (5) $false % 5.04/1.60 | | % 5.04/1.60 | | CLOSE: (5) is inconsistent. % 5.04/1.60 | | % 5.04/1.60 | Case 2: % 5.04/1.60 | | % 5.04/1.60 | | (6) all_7_0 = 44 % 5.04/1.60 | | % 5.04/1.60 | | REDUCE: (3), (6) imply: % 5.04/1.60 | | (7) $false % 5.04/1.60 | | % 5.04/1.60 | | CLOSE: (7) is inconsistent. % 5.04/1.60 | | % 5.04/1.60 | End of split % 5.04/1.60 | % 5.04/1.60 End of proof % 5.04/1.60 % SZS output end Proof for theBenchmark % 5.04/1.60 % 5.04/1.60 932ms %------------------------------------------------------------------------------