%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWC449_1 : TPTP v8.3.0. Released v8.3.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 : Tue May 14 09:00:30 EDT 2024 % Result : Theorem 13.52s 2.63s % Output : Proof 13.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC449_1 : TPTP v8.3.0. Released v8.3.0. % 0.11/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.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon May 13 14:45:53 EDT 2024 % 0.13/0.34 % CPUTime : % 0.63/0.61 ________ _____ % 0.63/0.61 ___ __ \_________(_)________________________________ % 0.63/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.63/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.63/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.63/0.61 % 0.63/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.63/0.61 (2023-06-19) % 0.63/0.61 % 0.63/0.61 (c) Philipp Rümmer, 2009-2023 % 0.63/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.63/0.61 Amanda Stjerna. % 0.63/0.61 Free software under BSD-3-Clause. % 0.63/0.61 % 0.63/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.63/0.61 % 0.63/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.63/0.62 Running up to 7 provers in parallel. % 0.63/0.63 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.63/0.63 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.63/0.63 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.63/0.63 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.63/0.63 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.63/0.63 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.63/0.63 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.55/1.06 Prover 6: Preprocessing ... % 2.55/1.06 Prover 3: Preprocessing ... % 2.55/1.06 Prover 5: Preprocessing ... % 2.55/1.06 Prover 0: Preprocessing ... % 2.55/1.06 Prover 2: Preprocessing ... % 2.55/1.06 Prover 1: Preprocessing ... % 2.55/1.06 Prover 4: Preprocessing ... % 4.23/1.28 Prover 6: Constructing countermodel ... % 4.23/1.29 Prover 1: Constructing countermodel ... % 4.23/1.29 Prover 4: Constructing countermodel ... % 4.23/1.30 Prover 3: Constructing countermodel ... % 4.53/1.32 Prover 0: Proving ... % 4.73/1.34 Prover 5: Proving ... % 4.73/1.35 Prover 2: Proving ... % 4.73/1.39 Prover 3: gave up % 4.73/1.39 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 4.73/1.39 Prover 1: gave up % 4.73/1.40 Prover 6: gave up % 4.73/1.41 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 4.73/1.41 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 4.73/1.42 Prover 7: Preprocessing ... % 5.40/1.45 Prover 9: Preprocessing ... % 5.40/1.45 Prover 8: Preprocessing ... % 5.87/1.51 Prover 7: Constructing countermodel ... % 5.87/1.52 Prover 8: Warning: ignoring some quantifiers % 5.87/1.53 Prover 8: Constructing countermodel ... % 5.87/1.55 Prover 9: Constructing countermodel ... % 12.23/2.32 Prover 4: Found proof (size 126) % 12.23/2.32 Prover 4: proved (1692ms) % 12.23/2.33 Prover 9: stopped % 12.23/2.33 Prover 0: stopped % 12.23/2.33 Prover 7: Found proof (size 126) % 12.23/2.33 Prover 7: proved (940ms) % 12.23/2.33 Prover 2: stopped % 12.23/2.34 Prover 8: stopped % 13.52/2.63 Prover 5: stopped % 13.52/2.63 % 13.52/2.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 13.52/2.63 % 13.52/2.65 % SZS output start Proof for theBenchmark % 13.52/2.66 Assumptions after simplification: % 13.52/2.66 --------------------------------- % 13.52/2.66 % 13.52/2.66 (conjecture_1) % 13.52/2.68 ? [v0: int] : ? [v1: int] : ? [v2: int] : ( ~ (v2 = v1) & $lesseq(0, v0) & % 13.52/2.68 fast(v0) = v2 & small(v0) = v1) % 13.52/2.68 % 13.52/2.68 (formula_1) % 13.52/2.69 ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ (f0(v0, v1) = v2) | % 13.52/2.69 $product($sum(v1, 2), v1) = v2) % 13.52/2.69 % 13.52/2.69 (formula_10) % 13.52/2.69 ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ ($lesseq(v0, 0) | % 13.52/2.69 ~ (u1(v0, v1) = v2)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 13.52/2.69 ($lesseq(1, v0)) | ~ (u1($sum(v0, -1), v1) = v2) | ? [v3: int] : (u1(v0, % 13.52/2.69 v1) = v3 & f1(v2) = v3)) & ! [v0: int] : ! [v1: int] : ! [v2: int] % 13.52/2.69 : ( ~ ($lesseq(1, v0)) | ~ (u1(v0, v1) = v2) | ? [v3: int] : (u1($sum(v0, % 13.52/2.69 -1), v1) = v3 & f1(v3) = v2)) % 13.52/2.69 % 13.52/2.69 (formula_11) % 13.52/2.70 ! [v0: int] : ! [v1: int] : ( ~ (v1(v0) = v1) | ? [v2: int] : (u1(g1, v2) = % 13.52/2.70 v1 & h1(v0) = v2)) & ! [v0: int] : ! [v1: int] : ( ~ (h1(v0) = v1) | ? % 13.52/2.70 [v2: int] : (v1(v0) = v2 & u1(g1, v1) = v2)) % 13.52/2.70 % 13.52/2.70 (formula_12) % 13.52/2.70 ! [v0: int] : ! [v1: int] : ( ~ (fast(v0) = v1) | v1(v0) = v1) & ! [v0: % 13.52/2.70 int] : ! [v1: int] : ( ~ (v1(v0) = v1) | fast(v0) = v1) % 13.52/2.70 % 13.52/2.70 (formula_2) % 13.52/2.70 ! [v0: int] : ! [v1: int] : (v1 = $product(4, v0) | ~ (g0(v0) = v1)) % 13.52/2.70 % 13.52/2.70 (formula_3) % 13.52/2.70 h0 = 2 % 13.52/2.70 % 13.52/2.70 (formula_4) % 13.52/2.70 ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ ($lesseq(v0, 0) | % 13.52/2.70 ~ (u0(v0, v1) = v2)) & ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 13.52/2.70 ($lesseq(1, v0)) | ~ (u0($sum(v0, -1), v1) = v2) | ? [v3: int] : (u0(v0, % 13.52/2.70 v1) = v3 & f0(v2, v0) = v3)) & ! [v0: int] : ! [v1: int] : ! [v2: % 13.52/2.70 int] : ( ~ ($lesseq(1, v0)) | ~ (u0(v0, v1) = v2) | ? [v3: int] : % 13.52/2.70 (u0($sum(v0, -1), v1) = v3 & f0(v3, v0) = v2)) % 13.52/2.70 % 13.52/2.70 (formula_5) % 13.52/2.71 ! [v0: int] : ! [v1: int] : ( ~ (v0(v0) = v1) | ? [v2: int] : (u0(v2, h0) = % 13.52/2.71 v1 & g0(v0) = v2)) & ! [v0: int] : ! [v1: int] : ( ~ (g0(v0) = v1) | ? % 13.52/2.71 [v2: int] : (v0(v0) = v2 & u0(v1, h0) = v2)) % 13.52/2.71 % 13.52/2.71 (formula_6) % 13.97/2.71 ! [v0: int] : ! [v1: int] : ( ~ (small(v0) = v1) | v0(v0) = v1) & ! [v0: % 13.97/2.71 int] : ! [v1: int] : ( ~ (v0(v0) = v1) | small(v0) = v1) % 13.97/2.71 % 13.97/2.71 (formula_7) % 13.97/2.71 ! [v0: int] : ! [v1: int] : ($difference(v1, v0) = 2 | ~ ($lesseq(v0, 0) | % 13.97/2.71 ~ (f1(v0) = v1)) & ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, v0)) | ~ % 13.97/2.71 (f1(v0) = v1) | $product($sum(v0, 2), v0) = v1) % 13.97/2.71 % 13.97/2.71 (formula_8) % 13.97/2.71 g1 = 1 % 13.97/2.71 % 13.97/2.71 (formula_9) % 13.97/2.71 ! [v0: int] : ! [v1: int] : (v1 = $product(4, v0) | ~ (h1(v0) = v1)) % 13.97/2.71 % 13.97/2.71 Those formulas are unsatisfiable: % 13.97/2.71 --------------------------------- % 13.97/2.71 % 13.97/2.71 Begin of proof % 13.97/2.71 | % 13.97/2.71 | ALPHA: (formula_4) implies: % 13.97/2.72 | (1) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ ($lesseq(1, v0)) | ~ % 13.97/2.72 | (u0(v0, v1) = v2) | ? [v3: int] : (u0($sum(v0, -1), v1) = v3 & % 13.97/2.72 | f0(v3, v0) = v2)) % 13.97/2.72 | (2) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ ($lesseq(1, v0)) | ~ % 13.97/2.72 | (u0($sum(v0, -1), v1) = v2) | ? [v3: int] : (u0(v0, v1) = v3 & % 13.97/2.72 | f0(v2, v0) = v3)) % 13.97/2.72 | (3) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ ($lesseq(v0, % 13.97/2.72 | 0) | ~ (u0(v0, v1) = v2)) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_5) implies: % 13.97/2.72 | (4) ! [v0: int] : ! [v1: int] : ( ~ (v0(v0) = v1) | ? [v2: int] : % 13.97/2.72 | (u0(v2, h0) = v1 & g0(v0) = v2)) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_6) implies: % 13.97/2.72 | (5) ! [v0: int] : ! [v1: int] : ( ~ (small(v0) = v1) | v0(v0) = v1) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_7) implies: % 13.97/2.72 | (6) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, v0)) | ~ (f1(v0) = v1) | % 13.97/2.72 | $product($sum(v0, 2), v0) = v1) % 13.97/2.72 | (7) ! [v0: int] : ! [v1: int] : ($difference(v1, v0) = 2 | ~ % 13.97/2.72 | ($lesseq(v0, 0) | ~ (f1(v0) = v1)) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_10) implies: % 13.97/2.72 | (8) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ ($lesseq(1, v0)) | ~ % 13.97/2.72 | (u1(v0, v1) = v2) | ? [v3: int] : (u1($sum(v0, -1), v1) = v3 & % 13.97/2.72 | f1(v3) = v2)) % 13.97/2.72 | (9) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ ($lesseq(v0, % 13.97/2.72 | 0) | ~ (u1(v0, v1) = v2)) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_11) implies: % 13.97/2.72 | (10) ! [v0: int] : ! [v1: int] : ( ~ (v1(v0) = v1) | ? [v2: int] : % 13.97/2.72 | (u1(g1, v2) = v1 & h1(v0) = v2)) % 13.97/2.72 | % 13.97/2.72 | ALPHA: (formula_12) implies: % 13.97/2.72 | (11) ! [v0: int] : ! [v1: int] : ( ~ (fast(v0) = v1) | v1(v0) = v1) % 13.97/2.72 | % 13.97/2.73 | DELTA: instantiating (conjecture_1) with fresh symbols all_14_0, all_14_1, % 13.97/2.73 | all_14_2 gives: % 13.97/2.73 | (12) ~ (all_14_0 = all_14_1) & $lesseq(0, all_14_2) & fast(all_14_2) = % 13.97/2.73 | all_14_0 & small(all_14_2) = all_14_1 % 13.97/2.73 | % 13.97/2.73 | ALPHA: (12) implies: % 13.97/2.73 | (13) ~ (all_14_0 = all_14_1) % 13.97/2.73 | (14) $lesseq(0, all_14_2) % 13.97/2.73 | (15) small(all_14_2) = all_14_1 % 13.97/2.73 | (16) fast(all_14_2) = all_14_0 % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (5) with all_14_2, all_14_1, simplifying with (15) % 13.97/2.73 | gives: % 13.97/2.73 | (17) v0(all_14_2) = all_14_1 % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (11) with all_14_2, all_14_0, simplifying with (16) % 13.97/2.73 | gives: % 13.97/2.73 | (18) v1(all_14_2) = all_14_0 % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (4) with all_14_2, all_14_1, simplifying with (17) % 13.97/2.73 | gives: % 13.97/2.73 | (19) ? [v0: int] : (u0(v0, h0) = all_14_1 & g0(all_14_2) = v0) % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (10) with all_14_2, all_14_0, simplifying with (18) % 13.97/2.73 | gives: % 13.97/2.73 | (20) ? [v0: int] : (u1(g1, v0) = all_14_0 & h1(all_14_2) = v0) % 13.97/2.73 | % 13.97/2.73 | DELTA: instantiating (20) with fresh symbol all_32_0 gives: % 13.97/2.73 | (21) u1(g1, all_32_0) = all_14_0 & h1(all_14_2) = all_32_0 % 13.97/2.73 | % 13.97/2.73 | ALPHA: (21) implies: % 13.97/2.73 | (22) h1(all_14_2) = all_32_0 % 13.97/2.73 | (23) u1(g1, all_32_0) = all_14_0 % 13.97/2.73 | % 13.97/2.73 | DELTA: instantiating (19) with fresh symbol all_34_0 gives: % 13.97/2.73 | (24) u0(all_34_0, h0) = all_14_1 & g0(all_14_2) = all_34_0 % 13.97/2.73 | % 13.97/2.73 | ALPHA: (24) implies: % 13.97/2.73 | (25) g0(all_14_2) = all_34_0 % 13.97/2.73 | (26) u0(all_34_0, h0) = all_14_1 % 13.97/2.73 | % 13.97/2.73 | REDUCE: (23), (formula_8) imply: % 13.97/2.73 | (27) u1(1, all_32_0) = all_14_0 % 13.97/2.73 | % 13.97/2.73 | REDUCE: (26), (formula_3) imply: % 13.97/2.73 | (28) u0(all_34_0, 2) = all_14_1 % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (formula_2) with all_14_2, all_34_0, simplifying % 13.97/2.73 | with (25) gives: % 13.97/2.73 | (29) all_34_0 = $product(4, all_14_2) % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (3) with all_34_0, 2, all_14_1, simplifying with % 13.97/2.73 | (28) gives: % 13.97/2.73 | (30) all_14_1 = 2 | ~ ($lesseq(all_34_0, 0) % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (formula_9) with all_14_2, all_32_0, simplifying % 13.97/2.73 | with (22) gives: % 13.97/2.73 | (31) all_32_0 = $product(4, all_14_2) % 13.97/2.73 | % 13.97/2.73 | REDUCE: (27), (31) imply: % 13.97/2.73 | (32) u1(1, $product(4, all_14_2)) = all_14_0 % 13.97/2.73 | % 13.97/2.73 | REDUCE: (28), (29) imply: % 13.97/2.73 | (33) u0($product(4, all_14_2), 2) = all_14_1 % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 1), 2, % 13.97/2.73 | all_14_1, simplifying with (33) gives: % 13.97/2.73 | (34) ~ ($lesseq(0, all_14_2)) | ? [v0: int] : (u0($sum($product(4, % 13.97/2.73 | all_14_2), 1), 2) = v0 & f0(all_14_1, $sum($product(4, % 13.97/2.73 | all_14_2), 1)) = v0) % 13.97/2.73 | % 13.97/2.73 | GROUND_INST: instantiating (1) with $product(4, all_14_2), 2, all_14_1, % 13.97/2.73 | simplifying with (33) gives: % 13.97/2.73 | (35) ~ ($lesseq(1, all_14_2)) | ? [v0: int] : (u0($sum($product(4, % 13.97/2.73 | all_14_2), -1), 2) = v0 & f0(v0, $product(4, all_14_2)) = % 13.97/2.73 | all_14_1) % 13.97/2.73 | % 13.97/2.74 | GROUND_INST: instantiating (8) with 1, $product(4, all_14_2), all_14_0, % 13.97/2.74 | simplifying with (32) gives: % 13.97/2.74 | (36) ? [v0: int] : (u1(0, $product(4, all_14_2)) = v0 & f1(v0) = all_14_0) % 13.97/2.74 | % 13.97/2.74 | DELTA: instantiating (36) with fresh symbol all_48_0 gives: % 13.97/2.74 | (37) u1(0, $product(4, all_14_2)) = all_48_0 & f1(all_48_0) = all_14_0 % 13.97/2.74 | % 13.97/2.74 | ALPHA: (37) implies: % 13.97/2.74 | (38) f1(all_48_0) = all_14_0 % 13.97/2.74 | (39) u1(0, $product(4, all_14_2)) = all_48_0 % 13.97/2.74 | % 13.97/2.74 | BETA: splitting (34) gives: % 13.97/2.74 | % 13.97/2.74 | Case 1: % 13.97/2.74 | | % 13.97/2.74 | | (40) $lesseq(all_14_2, -1) % 13.97/2.74 | | % 13.97/2.74 | | COMBINE_INEQS: (14), (40) imply: % 13.97/2.74 | | (41) $false % 13.97/2.74 | | % 13.97/2.74 | | CLOSE: (41) is inconsistent. % 13.97/2.74 | | % 13.97/2.74 | Case 2: % 13.97/2.74 | | % 13.97/2.74 | | (42) ? [v0: int] : (u0($sum($product(4, all_14_2), 1), 2) = v0 & % 13.97/2.74 | | f0(all_14_1, $sum($product(4, all_14_2), 1)) = v0) % 13.97/2.74 | | % 13.97/2.74 | | DELTA: instantiating (42) with fresh symbol all_57_0 gives: % 13.97/2.74 | | (43) u0($sum($product(4, all_14_2), 1), 2) = all_57_0 & f0(all_14_1, % 13.97/2.74 | | $sum($product(4, all_14_2), 1)) = all_57_0 % 13.97/2.74 | | % 13.97/2.74 | | ALPHA: (43) implies: % 13.97/2.74 | | (44) f0(all_14_1, $sum($product(4, all_14_2), 1)) = all_57_0 % 13.97/2.74 | | (45) u0($sum($product(4, all_14_2), 1), 2) = all_57_0 % 13.97/2.74 | | % 13.97/2.74 | | GROUND_INST: instantiating (7) with all_48_0, all_14_0, simplifying with % 13.97/2.74 | | (38) gives: % 13.97/2.74 | | (46) $difference(all_48_0, all_14_0) = -2 | ~ ($lesseq(all_48_0, 0) % 13.97/2.74 | | % 13.97/2.74 | | GROUND_INST: instantiating (9) with 0, $product(4, all_14_2), all_48_0, % 13.97/2.74 | | simplifying with (39) gives: % 13.97/2.74 | | (47) all_48_0 = $product(4, all_14_2) % 13.97/2.74 | | % 13.97/2.74 | | REDUCE: (38), (47) imply: % 13.97/2.74 | | (48) f1($product(4, all_14_2)) = all_14_0 % 13.97/2.74 | | % 13.97/2.74 | | GROUND_INST: instantiating (formula_1) with all_14_1, $sum($product(4, % 13.97/2.74 | | all_14_2), 1), all_57_0, simplifying with (44) gives: % 13.97/2.74 | | (49) $product($sum($product(4, all_14_2), 3), $sum($product(4, all_14_2), % 13.97/2.74 | | 1)) = all_57_0 % 13.97/2.74 | | % 13.97/2.74 | | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 2), 2, % 13.97/2.74 | | all_57_0, simplifying with (45) gives: % 13.97/2.74 | | (50) ~ ($lesseq(0, all_14_2)) | ? [v0: int] : (u0($sum($product(4, % 13.97/2.74 | | all_14_2), 2), 2) = v0 & f0(all_57_0, $sum($product(4, % 13.97/2.74 | | all_14_2), 2)) = v0) % 13.97/2.74 | | % 13.97/2.74 | | GROUND_INST: instantiating (6) with $product(4, all_14_2), all_14_0, % 13.97/2.74 | | simplifying with (48) gives: % 13.97/2.74 | | (51) ~ ($lesseq(1, all_14_2)) | $product($sum($product(4, all_14_2), 2), % 13.97/2.74 | | $product(4, all_14_2)) = all_14_0 % 13.97/2.74 | | % 13.97/2.74 | | BETA: splitting (50) gives: % 13.97/2.74 | | % 13.97/2.74 | | Case 1: % 13.97/2.74 | | | % 13.97/2.74 | | | (52) $lesseq(all_14_2, -1) % 13.97/2.74 | | | % 13.97/2.74 | | | COMBINE_INEQS: (14), (52) imply: % 13.97/2.74 | | | (53) $false % 13.97/2.74 | | | % 13.97/2.74 | | | CLOSE: (53) is inconsistent. % 13.97/2.74 | | | % 13.97/2.74 | | Case 2: % 13.97/2.74 | | | % 13.97/2.74 | | | (54) ? [v0: int] : (u0($sum($product(4, all_14_2), 2), 2) = v0 & % 13.97/2.74 | | | f0(all_57_0, $sum($product(4, all_14_2), 2)) = v0) % 13.97/2.74 | | | % 13.97/2.74 | | | DELTA: instantiating (54) with fresh symbol all_83_0 gives: % 13.97/2.74 | | | (55) u0($sum($product(4, all_14_2), 2), 2) = all_83_0 & f0(all_57_0, % 13.97/2.74 | | | $sum($product(4, all_14_2), 2)) = all_83_0 % 13.97/2.74 | | | % 13.97/2.74 | | | ALPHA: (55) implies: % 13.97/2.74 | | | (56) f0(all_57_0, $sum($product(4, all_14_2), 2)) = all_83_0 % 13.97/2.75 | | | (57) u0($sum($product(4, all_14_2), 2), 2) = all_83_0 % 13.97/2.75 | | | % 13.97/2.75 | | | GROUND_INST: instantiating (formula_1) with all_57_0, $sum($product(4, % 13.97/2.75 | | | all_14_2), 2), all_83_0, simplifying with (56) gives: % 13.97/2.75 | | | (58) $product($sum($product(4, all_14_2), 4), $sum($product(4, % 13.97/2.75 | | | all_14_2), 2)) = all_83_0 % 13.97/2.75 | | | % 13.97/2.75 | | | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 3), 2, % 13.97/2.75 | | | all_83_0, simplifying with (57) gives: % 13.97/2.75 | | | (59) ~ ($lesseq(0, all_14_2)) | ? [v0: int] : (u0($sum($product(4, % 13.97/2.75 | | | all_14_2), 3), 2) = v0 & f0(all_83_0, $sum($product(4, % 13.97/2.75 | | | all_14_2), 3)) = v0) % 13.97/2.75 | | | % 13.97/2.75 | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.75 | | | (60) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.75 | | | ($difference($difference(v2, v1), $product(8, v0)) = 5 | ~ % 13.97/2.75 | | | ($product($sum($product(4, v0), 4), $sum($product(4, v0), 2)) = % 13.97/2.75 | | | v2) | ~ ($product($sum($product(4, v0), 3), $sum($product(4, % 13.97/2.75 | | | v0), 1)) = v1)) % 13.97/2.75 | | | % 13.97/2.75 | | | GROUND_INST: instantiating (60) with all_14_2, all_57_0, all_83_0, % 13.97/2.75 | | | simplifying with (49), (58) gives: % 13.97/2.75 | | | (61) $difference($difference(all_83_0, all_57_0), $product(8, % 13.97/2.75 | | | all_14_2)) = 5 % 13.97/2.75 | | | % 13.97/2.75 | | | REDUCE: (58), (61) imply: % 13.97/2.75 | | | (62) $product($sum($product(4, all_14_2), 4), $sum($product(4, % 13.97/2.75 | | | all_14_2), 2)) = $sum($sum(all_57_0, $product(8, all_14_2)), % 13.97/2.75 | | | 5) % 13.97/2.75 | | | % 13.97/2.75 | | | BETA: splitting (59) gives: % 13.97/2.75 | | | % 13.97/2.75 | | | Case 1: % 13.97/2.75 | | | | % 13.97/2.75 | | | | (63) $lesseq(all_14_2, -1) % 13.97/2.75 | | | | % 13.97/2.75 | | | | COMBINE_INEQS: (14), (63) imply: % 13.97/2.75 | | | | (64) $false % 13.97/2.75 | | | | % 13.97/2.75 | | | | CLOSE: (64) is inconsistent. % 13.97/2.75 | | | | % 13.97/2.75 | | | Case 2: % 13.97/2.75 | | | | % 13.97/2.75 | | | | (65) ? [v0: int] : (u0($sum($product(4, all_14_2), 3), 2) = v0 & % 13.97/2.75 | | | | f0(all_83_0, $sum($product(4, all_14_2), 3)) = v0) % 13.97/2.75 | | | | % 13.97/2.75 | | | | DELTA: instantiating (65) with fresh symbol all_103_0 gives: % 13.97/2.75 | | | | (66) u0($sum($product(4, all_14_2), 3), 2) = all_103_0 & f0(all_83_0, % 13.97/2.75 | | | | $sum($product(4, all_14_2), 3)) = all_103_0 % 13.97/2.75 | | | | % 13.97/2.75 | | | | ALPHA: (66) implies: % 13.97/2.75 | | | | (67) f0(all_83_0, $sum($product(4, all_14_2), 3)) = all_103_0 % 13.97/2.75 | | | | (68) u0($sum($product(4, all_14_2), 3), 2) = all_103_0 % 13.97/2.75 | | | | % 13.97/2.75 | | | | REDUCE: (61), (67) imply: % 13.97/2.75 | | | | (69) f0($sum($sum(all_57_0, $product(8, all_14_2)), 5), % 13.97/2.75 | | | | $sum($product(4, all_14_2), 3)) = all_103_0 % 13.97/2.75 | | | | % 13.97/2.75 | | | | GROUND_INST: instantiating (formula_1) with $sum($sum(all_57_0, % 13.97/2.75 | | | | $product(8, all_14_2)), 5), $sum($product(4, all_14_2), % 13.97/2.75 | | | | 3), all_103_0, simplifying with (69) gives: % 13.97/2.75 | | | | (70) $product($sum($product(4, all_14_2), 5), $sum($product(4, % 13.97/2.75 | | | | all_14_2), 3)) = all_103_0 % 13.97/2.75 | | | | % 13.97/2.75 | | | | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 4), 2, % 13.97/2.75 | | | | all_103_0, simplifying with (68) gives: % 13.97/2.75 | | | | (71) ~ ($lesseq(0, all_14_2)) | ? [v0: int] : (u0($sum($product(4, % 13.97/2.75 | | | | all_14_2), 4), 2) = v0 & f0(all_103_0, $sum($product(4, % 13.97/2.75 | | | | all_14_2), 4)) = v0) % 13.97/2.75 | | | | % 13.97/2.75 | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.75 | | | | (72) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.75 | | | | ($difference($difference(v2, v1), $product(16, v0)) = 12 | ~ % 13.97/2.75 | | | | ($product($sum($product(4, v0), 5), $sum($product(4, v0), 3)) % 13.97/2.75 | | | | = v2) | ~ ($product($sum($product(4, v0), 4), % 13.97/2.75 | | | | $sum($product(4, v0), 2)) = $sum($sum(v1, $product(8, % 13.97/2.75 | | | | v0)), 5))) % 13.97/2.75 | | | | % 13.97/2.75 | | | | GROUND_INST: instantiating (72) with all_14_2, all_57_0, all_103_0, % 13.97/2.75 | | | | simplifying with (62), (70) gives: % 13.97/2.75 | | | | (73) $difference($difference(all_103_0, all_57_0), $product(16, % 13.97/2.75 | | | | all_14_2)) = 12 % 13.97/2.75 | | | | % 13.97/2.75 | | | | REDUCE: (70), (73) imply: % 13.97/2.76 | | | | (74) $product($sum($product(4, all_14_2), 5), $sum($product(4, % 13.97/2.76 | | | | all_14_2), 3)) = $sum($sum(all_57_0, $product(16, % 13.97/2.76 | | | | all_14_2)), 12) % 13.97/2.76 | | | | % 13.97/2.76 | | | | BETA: splitting (71) gives: % 13.97/2.76 | | | | % 13.97/2.76 | | | | Case 1: % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | (75) $lesseq(all_14_2, -1) % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | COMBINE_INEQS: (14), (75) imply: % 13.97/2.76 | | | | | (76) $false % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | CLOSE: (76) is inconsistent. % 13.97/2.76 | | | | | % 13.97/2.76 | | | | Case 2: % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | (77) ? [v0: int] : (u0($sum($product(4, all_14_2), 4), 2) = v0 & % 13.97/2.76 | | | | | f0(all_103_0, $sum($product(4, all_14_2), 4)) = v0) % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | DELTA: instantiating (77) with fresh symbol all_122_0 gives: % 13.97/2.76 | | | | | (78) u0($sum($product(4, all_14_2), 4), 2) = all_122_0 & % 13.97/2.76 | | | | | f0(all_103_0, $sum($product(4, all_14_2), 4)) = all_122_0 % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | ALPHA: (78) implies: % 13.97/2.76 | | | | | (79) f0(all_103_0, $sum($product(4, all_14_2), 4)) = all_122_0 % 13.97/2.76 | | | | | (80) u0($sum($product(4, all_14_2), 4), 2) = all_122_0 % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | REDUCE: (73), (79) imply: % 13.97/2.76 | | | | | (81) f0($sum($sum(all_57_0, $product(16, all_14_2)), 12), % 13.97/2.76 | | | | | $sum($product(4, all_14_2), 4)) = all_122_0 % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | GROUND_INST: instantiating (formula_1) with $sum($sum(all_57_0, % 13.97/2.76 | | | | | $product(16, all_14_2)), 12), $sum($product(4, % 13.97/2.76 | | | | | all_14_2), 4), all_122_0, simplifying with (81) % 13.97/2.76 | | | | | gives: % 13.97/2.76 | | | | | (82) $product($sum($product(4, all_14_2), 6), $sum($product(4, % 13.97/2.76 | | | | | all_14_2), 4)) = all_122_0 % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 5), 2, % 13.97/2.76 | | | | | all_122_0, simplifying with (80) gives: % 13.97/2.76 | | | | | (83) ~ ($lesseq(-1, all_14_2)) | ? [v0: int] : % 13.97/2.76 | | | | | (u0($sum($product(4, all_14_2), 5), 2) = v0 & f0(all_122_0, % 13.97/2.76 | | | | | $sum($product(4, all_14_2), 5)) = v0) % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.76 | | | | | (84) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.76 | | | | | ($difference($difference(v2, v1), $product(24, v0)) = 21 | ~ % 13.97/2.76 | | | | | ($product($sum($product(4, v0), 6), $sum($product(4, v0), % 13.97/2.76 | | | | | 4)) = v2) | ~ ($product($sum($product(4, v0), 5), % 13.97/2.76 | | | | | $sum($product(4, v0), 3)) = $sum($sum(v1, $product(16, % 13.97/2.76 | | | | | v0)), 12))) % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | GROUND_INST: instantiating (84) with all_14_2, all_57_0, all_122_0, % 13.97/2.76 | | | | | simplifying with (74), (82) gives: % 13.97/2.76 | | | | | (85) $difference($difference(all_122_0, all_57_0), $product(24, % 13.97/2.76 | | | | | all_14_2)) = 21 % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | REDUCE: (82), (85) imply: % 13.97/2.76 | | | | | (86) $product($sum($product(4, all_14_2), 6), $sum($product(4, % 13.97/2.76 | | | | | all_14_2), 4)) = $sum($sum(all_57_0, $product(24, % 13.97/2.76 | | | | | all_14_2)), 21) % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | BETA: splitting (83) gives: % 13.97/2.76 | | | | | % 13.97/2.76 | | | | | Case 1: % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | (87) $lesseq(all_14_2, -2) % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | COMBINE_INEQS: (14), (87) imply: % 13.97/2.76 | | | | | | (88) $false % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | CLOSE: (88) is inconsistent. % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | Case 2: % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | (89) ? [v0: int] : (u0($sum($product(4, all_14_2), 5), 2) = v0 & % 13.97/2.76 | | | | | | f0(all_122_0, $sum($product(4, all_14_2), 5)) = v0) % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | DELTA: instantiating (89) with fresh symbol all_142_0 gives: % 13.97/2.76 | | | | | | (90) u0($sum($product(4, all_14_2), 5), 2) = all_142_0 & % 13.97/2.76 | | | | | | f0(all_122_0, $sum($product(4, all_14_2), 5)) = all_142_0 % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | ALPHA: (90) implies: % 13.97/2.76 | | | | | | (91) f0(all_122_0, $sum($product(4, all_14_2), 5)) = all_142_0 % 13.97/2.76 | | | | | | (92) u0($sum($product(4, all_14_2), 5), 2) = all_142_0 % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | REDUCE: (85), (91) imply: % 13.97/2.76 | | | | | | (93) f0($sum($sum(all_57_0, $product(24, all_14_2)), 21), % 13.97/2.76 | | | | | | $sum($product(4, all_14_2), 5)) = all_142_0 % 13.97/2.76 | | | | | | % 13.97/2.76 | | | | | | GROUND_INST: instantiating (formula_1) with $sum($sum(all_57_0, % 13.97/2.76 | | | | | | $product(24, all_14_2)), 21), $sum($product(4, % 13.97/2.76 | | | | | | all_14_2), 5), all_142_0, simplifying with (93) % 13.97/2.76 | | | | | | gives: % 13.97/2.77 | | | | | | (94) $product($sum($product(4, all_14_2), 7), $sum($product(4, % 13.97/2.77 | | | | | | all_14_2), 5)) = all_142_0 % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | GROUND_INST: instantiating (2) with $sum($product(4, all_14_2), 6), % 13.97/2.77 | | | | | | 2, all_142_0, simplifying with (92) gives: % 13.97/2.77 | | | | | | (95) ~ ($lesseq(-1, all_14_2)) | ? [v0: int] : % 13.97/2.77 | | | | | | (u0($sum($product(4, all_14_2), 6), 2) = v0 & f0(all_142_0, % 13.97/2.77 | | | | | | $sum($product(4, all_14_2), 6)) = v0) % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.77 | | | | | | (96) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.77 | | | | | | ($difference($difference(v2, v1), $product(32, v0)) = 32 | % 13.97/2.77 | | | | | | ~ ($product($sum($product(4, v0), 7), $sum($product(4, % 13.97/2.77 | | | | | | v0), 5)) = v2) | ~ ($product($sum($product(4, % 13.97/2.77 | | | | | | v0), 6), $sum($product(4, v0), 4)) = $sum($sum(v1, % 13.97/2.77 | | | | | | $product(24, v0)), 21))) % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | GROUND_INST: instantiating (96) with all_14_2, all_57_0, all_142_0, % 13.97/2.77 | | | | | | simplifying with (86), (94) gives: % 13.97/2.77 | | | | | | (97) $difference($difference(all_142_0, all_57_0), $product(32, % 13.97/2.77 | | | | | | all_14_2)) = 32 % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | REDUCE: (94), (97) imply: % 13.97/2.77 | | | | | | (98) $product($sum($product(4, all_14_2), 7), $sum($product(4, % 13.97/2.77 | | | | | | all_14_2), 5)) = $sum($sum(all_57_0, $product(32, % 13.97/2.77 | | | | | | all_14_2)), 32) % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | BETA: splitting (95) gives: % 13.97/2.77 | | | | | | % 13.97/2.77 | | | | | | Case 1: % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | (99) $lesseq(all_14_2, -2) % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | COMBINE_INEQS: (14), (99) imply: % 13.97/2.77 | | | | | | | (100) $false % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | CLOSE: (100) is inconsistent. % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | Case 2: % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | (101) ? [v0: int] : (u0($sum($product(4, all_14_2), 6), 2) = % 13.97/2.77 | | | | | | | v0 & f0(all_142_0, $sum($product(4, all_14_2), 6)) = % 13.97/2.77 | | | | | | | v0) % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | DELTA: instantiating (101) with fresh symbol all_161_0 gives: % 13.97/2.77 | | | | | | | (102) u0($sum($product(4, all_14_2), 6), 2) = all_161_0 & % 13.97/2.77 | | | | | | | f0(all_142_0, $sum($product(4, all_14_2), 6)) = all_161_0 % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | ALPHA: (102) implies: % 13.97/2.77 | | | | | | | (103) f0(all_142_0, $sum($product(4, all_14_2), 6)) = all_161_0 % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | REDUCE: (97), (103) imply: % 13.97/2.77 | | | | | | | (104) f0($sum($sum(all_57_0, $product(32, all_14_2)), 32), % 13.97/2.77 | | | | | | | $sum($product(4, all_14_2), 6)) = all_161_0 % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | BETA: splitting (30) gives: % 13.97/2.77 | | | | | | | % 13.97/2.77 | | | | | | | Case 1: % 13.97/2.77 | | | | | | | | % 13.97/2.77 | | | | | | | | (105) $lesseq(1, all_34_0) % 13.97/2.77 | | | | | | | | % 13.97/2.77 | | | | | | | | REDUCE: (29), (105) imply: % 13.97/2.77 | | | | | | | | (106) $lesseq(1, all_14_2) % 13.97/2.77 | | | | | | | | % 13.97/2.77 | | | | | | | | SIMP: (106) implies: % 13.97/2.77 | | | | | | | | (107) $lesseq(1, all_14_2) % 13.97/2.77 | | | | | | | | % 13.97/2.77 | | | | | | | | BETA: splitting (51) gives: % 13.97/2.77 | | | | | | | | % 13.97/2.77 | | | | | | | | Case 1: % 13.97/2.77 | | | | | | | | | % 13.97/2.77 | | | | | | | | | (108) $product($sum($product(4, all_14_2), 2), $product(4, % 13.97/2.77 | | | | | | | | | all_14_2)) = all_14_0 % 13.97/2.77 | | | | | | | | | % 13.97/2.77 | | | | | | | | | BETA: splitting (35) gives: % 13.97/2.77 | | | | | | | | | % 13.97/2.77 | | | | | | | | | Case 1: % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | (109) $lesseq(all_14_2, 0) % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | COMBINE_INEQS: (107), (109) imply: % 13.97/2.77 | | | | | | | | | | (110) $false % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | CLOSE: (110) is inconsistent. % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | Case 2: % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | (111) ? [v0: int] : (u0($sum($product(4, all_14_2), -1), % 13.97/2.77 | | | | | | | | | | 2) = v0 & f0(v0, $product(4, all_14_2)) = % 13.97/2.77 | | | | | | | | | | all_14_1) % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | DELTA: instantiating (111) with fresh symbol all_182_0 % 13.97/2.77 | | | | | | | | | | gives: % 13.97/2.77 | | | | | | | | | | (112) u0($sum($product(4, all_14_2), -1), 2) = all_182_0 % 13.97/2.77 | | | | | | | | | | & f0(all_182_0, $product(4, all_14_2)) = all_14_1 % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | ALPHA: (112) implies: % 13.97/2.77 | | | | | | | | | | (113) f0(all_182_0, $product(4, all_14_2)) = all_14_1 % 13.97/2.77 | | | | | | | | | | % 13.97/2.77 | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.77 | | | | | | | | | | (114) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.77 | | | | | | | | | | ($difference($difference(v2, v1), $product(8, v0)) % 13.97/2.77 | | | | | | | | | | = 3 | ~ ($product($sum($product(4, v0), 7), % 13.97/2.77 | | | | | | | | | | $sum($product(4, v0), 5)) = $sum($sum(v2, % 13.97/2.77 | | | | | | | | | | $product(32, v0)), 32)) | ~ % 13.97/2.77 | | | | | | | | | | ($product($sum($product(4, v0), 2), $product(4, % 13.97/2.77 | | | | | | | | | | v0)) = v1)) % 13.97/2.77 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | GROUND_INST: instantiating (114) with all_14_2, all_14_0, % 13.97/2.78 | | | | | | | | | | all_57_0, simplifying with (98), (108) gives: % 13.97/2.78 | | | | | | | | | | (115) $difference($difference(all_57_0, all_14_0), % 13.97/2.78 | | | | | | | | | | $product(8, all_14_2)) = 3 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | REDUCE: (104), (115) imply: % 13.97/2.78 | | | | | | | | | | (116) f0($sum($sum(all_14_0, $product(40, all_14_2)), % 13.97/2.78 | | | | | | | | | | 35), $sum($product(4, all_14_2), 6)) = % 13.97/2.78 | | | | | | | | | | all_161_0 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | REDUCE: (98), (115) imply: % 13.97/2.78 | | | | | | | | | | (117) $product($sum($product(4, all_14_2), 7), % 13.97/2.78 | | | | | | | | | | $sum($product(4, all_14_2), 5)) = % 13.97/2.78 | | | | | | | | | | $sum($sum(all_14_0, $product(40, all_14_2)), 35) % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | GROUND_INST: instantiating (formula_1) with $sum($sum(all_14_0, % 13.97/2.78 | | | | | | | | | | $product(40, all_14_2)), 35), $sum($product(4, % 13.97/2.78 | | | | | | | | | | all_14_2), 6), all_161_0, simplifying with % 13.97/2.78 | | | | | | | | | | (116) gives: % 13.97/2.78 | | | | | | | | | | (118) $product($sum($product(4, all_14_2), 8), % 13.97/2.78 | | | | | | | | | | $sum($product(4, all_14_2), 6)) = all_161_0 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | GROUND_INST: instantiating (formula_1) with all_182_0, % 13.97/2.78 | | | | | | | | | | $product(4, all_14_2), all_14_1, simplifying with % 13.97/2.78 | | | | | | | | | | (113) gives: % 13.97/2.78 | | | | | | | | | | (119) $product($sum($product(4, all_14_2), 2), % 13.97/2.78 | | | | | | | | | | $product(4, all_14_2)) = all_14_1 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.78 | | | | | | | | | | (120) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 13.97/2.78 | | | | | | | | | | [v3: int] : ($difference($difference(v3, v2), % 13.97/2.78 | | | | | | | | | | $product(48, v0)) = 48 | ~ % 13.97/2.78 | | | | | | | | | | ($product($sum($product(4, v0), 8), % 13.97/2.78 | | | | | | | | | | $sum($product(4, v0), 6)) = v3) | ~ % 13.97/2.78 | | | | | | | | | | ($product($sum($product(4, v0), 7), % 13.97/2.78 | | | | | | | | | | $sum($product(4, v0), 5)) = $sum($sum(v2, % 13.97/2.78 | | | | | | | | | | $product(40, v0)), 35)) | ~ % 13.97/2.78 | | | | | | | | | | ($product($sum($product(4, v0), 2), $product(4, % 13.97/2.78 | | | | | | | | | | v0)) = v1)) % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | GROUND_INST: instantiating (120) with all_14_2, all_14_1, % 13.97/2.78 | | | | | | | | | | all_14_0, all_161_0, simplifying with (117), % 13.97/2.78 | | | | | | | | | | (118), (119) gives: % 13.97/2.78 | | | | | | | | | | (121) $difference($difference(all_161_0, all_14_0), % 13.97/2.78 | | | | | | | | | | $product(48, all_14_2)) = 48 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 13.97/2.78 | | | | | | | | | | (122) ! [v0: int] : ! [v1: int] : ! [v2: int] : % 13.97/2.78 | | | | | | | | | | ($difference($difference(v2, v1), $product(48, v0)) % 13.97/2.78 | | | | | | | | | | = 48 | ~ ($product($sum($product(4, v0), 8), % 13.97/2.78 | | | | | | | | | | $sum($product(4, v0), 6)) = v2) | ~ % 13.97/2.78 | | | | | | | | | | ($product($sum($product(4, v0), 2), $product(4, % 13.97/2.78 | | | | | | | | | | v0)) = v1)) % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | GROUND_INST: instantiating (122) with all_14_2, all_14_1, % 13.97/2.78 | | | | | | | | | | all_161_0, simplifying with (118), (119) gives: % 13.97/2.78 | | | | | | | | | | (123) $difference($difference(all_161_0, all_14_1), % 13.97/2.78 | | | | | | | | | | $product(48, all_14_2)) = 48 % 13.97/2.78 | | | | | | | | | | % 13.97/2.78 | | | | | | | | | | COMBINE_EQS: (121), (123) imply: % 13.97/2.79 | | | | | | | | | | (124) all_14_0 = all_14_1 % 13.97/2.79 | | | | | | | | | | % 13.97/2.79 | | | | | | | | | | REDUCE: (13), (124) imply: % 13.97/2.79 | | | | | | | | | | (125) $false % 13.97/2.79 | | | | | | | | | | % 13.97/2.79 | | | | | | | | | | CLOSE: (125) is inconsistent. % 13.97/2.79 | | | | | | | | | | % 13.97/2.79 | | | | | | | | | End of split % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | Case 2: % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | (126) $lesseq(all_14_2, 0) % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | COMBINE_INEQS: (107), (126) imply: % 13.97/2.79 | | | | | | | | | (127) $false % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | CLOSE: (127) is inconsistent. % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | End of split % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | Case 2: % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | (128) all_14_1 = 2 % 13.97/2.79 | | | | | | | | (129) $lesseq(all_34_0, 0) % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | REDUCE: (29), (129) imply: % 13.97/2.79 | | | | | | | | (130) $lesseq(all_14_2, 0) % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | SIMP: (130) implies: % 13.97/2.79 | | | | | | | | (131) $lesseq(all_14_2, 0) % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | ANTI_SYMM: (14), (131) imply: % 13.97/2.79 | | | | | | | | (132) all_14_2 = 0 % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | REDUCE: (13), (128) imply: % 13.97/2.79 | | | | | | | | (133) ~ (all_14_0 = 2) % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | COMBINE_EQS: (47), (132) imply: % 13.97/2.79 | | | | | | | | (134) all_48_0 = 0 % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | BETA: splitting (46) gives: % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | | Case 1: % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | (135) $lesseq(1, all_48_0) % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | REDUCE: (134), (135) imply: % 13.97/2.79 | | | | | | | | | (136) $false % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | CLOSE: (136) is inconsistent. % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | Case 2: % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | (137) $difference(all_48_0, all_14_0) = -2 % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | COMBINE_EQS: (134), (137) imply: % 13.97/2.79 | | | | | | | | | (138) all_14_0 = 2 % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | SIMP: (138) implies: % 13.97/2.79 | | | | | | | | | (139) all_14_0 = 2 % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | REDUCE: (133), (139) imply: % 13.97/2.79 | | | | | | | | | (140) $false % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | | CLOSE: (140) is inconsistent. % 13.97/2.79 | | | | | | | | | % 13.97/2.79 | | | | | | | | End of split % 13.97/2.79 | | | | | | | | % 13.97/2.79 | | | | | | | End of split % 13.97/2.79 | | | | | | | % 13.97/2.79 | | | | | | End of split % 13.97/2.79 | | | | | | % 13.97/2.79 | | | | | End of split % 13.97/2.79 | | | | | % 13.97/2.79 | | | | End of split % 13.97/2.79 | | | | % 13.97/2.79 | | | End of split % 13.97/2.79 | | | % 13.97/2.79 | | End of split % 13.97/2.79 | | % 13.97/2.79 | End of split % 13.97/2.79 | % 13.97/2.79 End of proof % 13.97/2.79 % SZS output end Proof for theBenchmark % 13.97/2.79 % 13.97/2.79 2182ms %------------------------------------------------------------------------------