%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : ARI678_1 : TPTP v8.1.2. Released v6.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n018.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 17:48:47 EDT 2023 % Result : Theorem 4.36s 1.38s % Output : Proof 6.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : ARI678_1 : TPTP v8.1.2. Released v6.3.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n018.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Tue Aug 29 18:18:33 EDT 2023 % 0.14/0.35 % CPUTime : % 0.22/0.62 ________ _____ % 0.22/0.62 ___ __ \_________(_)________________________________ % 0.22/0.62 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.22/0.62 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.22/0.62 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.22/0.62 % 0.22/0.62 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.22/0.62 (2023-06-19) % 0.22/0.62 % 0.22/0.62 (c) Philipp Rümmer, 2009-2023 % 0.22/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.22/0.62 Amanda Stjerna. % 0.22/0.62 Free software under BSD-3-Clause. % 0.22/0.62 % 0.22/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.22/0.62 % 0.22/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.22/0.64 Running up to 7 provers in parallel. % 0.22/0.65 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.22/0.65 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.22/0.65 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.22/0.65 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.22/0.65 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.22/0.65 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.22/0.65 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.16/1.00 Prover 5: Preprocessing ... % 2.16/1.00 Prover 1: Preprocessing ... % 2.16/1.00 Prover 0: Preprocessing ... % 2.16/1.00 Prover 3: Preprocessing ... % 2.16/1.00 Prover 4: Preprocessing ... % 2.16/1.00 Prover 6: Preprocessing ... % 2.16/1.00 Prover 2: Preprocessing ... % 2.16/1.06 Prover 0: Constructing countermodel ... % 2.16/1.06 Prover 1: Constructing countermodel ... % 2.16/1.06 Prover 4: Constructing countermodel ... % 2.16/1.06 Prover 5: Constructing countermodel ... % 2.16/1.06 Prover 2: Constructing countermodel ... % 2.16/1.06 Prover 6: Constructing countermodel ... % 2.16/1.06 Prover 3: Constructing countermodel ... % 4.36/1.38 Prover 3: proved (730ms) % 4.36/1.38 % 4.36/1.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.36/1.38 % 4.36/1.38 Prover 5: proved (729ms) % 4.36/1.38 % 4.36/1.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.36/1.38 % 4.36/1.39 Prover 2: stopped % 4.36/1.39 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 4.36/1.39 Prover 6: proved (736ms) % 4.36/1.39 % 4.36/1.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.36/1.39 % 4.36/1.39 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 4.36/1.39 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 4.36/1.39 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 4.36/1.40 Prover 0: proved (751ms) % 4.36/1.40 % 4.36/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.36/1.40 % 4.36/1.40 Prover 10: Preprocessing ... % 4.36/1.40 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 4.36/1.40 Prover 7: Preprocessing ... % 4.36/1.40 Prover 11: Preprocessing ... % 4.36/1.40 Prover 8: Preprocessing ... % 4.36/1.40 Prover 13: Preprocessing ... % 4.36/1.41 Prover 7: Constructing countermodel ... % 4.36/1.41 Prover 11: Constructing countermodel ... % 4.36/1.41 Prover 13: Constructing countermodel ... % 4.36/1.42 Prover 8: Constructing countermodel ... % 4.36/1.43 Prover 10: Constructing countermodel ... % 5.13/1.48 Prover 1: Found proof (size 178) % 5.13/1.48 Prover 1: proved (838ms) % 5.13/1.49 Prover 8: stopped % 5.52/1.50 Prover 4: Found proof (size 178) % 5.52/1.50 Prover 4: proved (858ms) % 5.52/1.54 Prover 7: Found proof (size 178) % 5.52/1.54 Prover 7: proved (160ms) % 5.52/1.55 Prover 11: Found proof (size 178) % 5.52/1.55 Prover 11: proved (156ms) % 5.52/1.55 Prover 13: Found proof (size 178) % 5.52/1.55 Prover 13: proved (148ms) % 5.52/1.55 Prover 10: Found proof (size 178) % 5.52/1.55 Prover 10: proved (159ms) % 5.52/1.55 % 5.52/1.55 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.52/1.55 % 5.91/1.56 % SZS output start Proof for theBenchmark % 5.91/1.57 Assumptions after simplification: % 5.91/1.57 --------------------------------- % 5.91/1.57 % 5.91/1.57 (conj) % 5.91/1.57 ? [v0: int] : ? [v1: int] : ($lesseq(v1, 7) & $product(v0, a) = v1 & % 5.91/1.57 $product(a, a) = v0) % 5.91/1.57 % 5.91/1.57 (conj_001) % 5.91/1.57 $lesseq(0, a) % 5.91/1.57 % 5.91/1.57 (conj_002) % 5.91/1.57 ? [v0: int] : ? [v1: int] : ? [v2: int] : ($lesseq(2, v2) & $product(v1, a) % 5.91/1.57 = v2 & $product(v0, a) = v1 & $product(a, a) = v0) % 5.91/1.57 % 5.91/1.57 Those formulas are unsatisfiable: % 5.91/1.57 --------------------------------- % 5.91/1.57 % 5.91/1.57 Begin of proof % 5.91/1.58 | % 5.91/1.58 | DELTA: instantiating (conj) with fresh symbols all_3_0, all_3_1 gives: % 5.91/1.58 | (1) $lesseq(all_3_0, 7) & $product(all_3_1, a) = all_3_0 & $product(a, a) = % 5.91/1.58 | all_3_1 % 5.91/1.58 | % 5.91/1.58 | ALPHA: (1) implies: % 5.91/1.58 | (2) $lesseq(all_3_0, 7) % 5.91/1.58 | (3) $product(a, a) = all_3_1 % 5.91/1.58 | (4) $product(all_3_1, a) = all_3_0 % 5.91/1.58 | % 5.91/1.58 | DELTA: instantiating (conj_002) with fresh symbols all_6_0, all_6_1, all_6_2 % 5.91/1.58 | gives: % 5.91/1.58 | (5) $lesseq(2, all_6_0) & $product(all_6_1, a) = all_6_0 & % 5.91/1.58 | $product(all_6_2, a) = all_6_1 & $product(a, a) = all_6_2 % 5.91/1.58 | % 5.91/1.58 | ALPHA: (5) implies: % 5.91/1.58 | (6) $lesseq(2, all_6_0) % 5.91/1.59 | (7) $product(a, a) = all_6_2 % 5.91/1.59 | (8) $product(all_6_2, a) = all_6_1 % 5.91/1.59 | (9) $product(all_6_1, a) = all_6_0 % 5.91/1.59 | % 5.91/1.59 | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.59 | (10) ! [v0: int] : ! [v1: int] : ! [v2: int] : (v2 = v1 | ~ % 5.91/1.59 | ($product(v0, v0) = v2) | ~ ($product(v0, v0) = v1)) % 5.91/1.59 | % 5.91/1.59 | GROUND_INST: instantiating (10) with a, all_3_1, all_6_2, simplifying with % 5.91/1.59 | (3), (7) gives: % 5.91/1.59 | (11) all_6_2 = all_3_1 % 5.91/1.59 | % 5.91/1.59 | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.59 | (12) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! [v3: int] : ! [v4: % 5.91/1.59 | int] : (v4 = v2 | ~ ($product(v3, v0) = v4) | ~ ($product(v1, v0) % 5.91/1.59 | = v2) | ~ ($product(v0, v0) = v3) | ~ ($product(v0, v0) = v1)) % 5.91/1.59 | % 5.91/1.59 | GROUND_INST: instantiating (12) with a, all_3_1, all_3_0, all_6_2, all_6_1, % 5.91/1.59 | simplifying with (3), (4), (7), (8) gives: % 5.91/1.59 | (13) all_6_1 = all_3_0 % 5.91/1.59 | % 5.91/1.59 | REDUCE: (9), (13) imply: % 5.91/1.59 | (14) $product(all_3_0, a) = all_6_0 % 5.91/1.59 | % 5.91/1.59 | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.59 | (15) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ ($lesseq(2, v2)) | ~ % 5.91/1.59 | ($lesseq(v1, -1)) | ~ ($lesseq(0, v0)) | ~ ($product(v1, v0) = % 5.91/1.59 | v2)) % 5.91/1.59 | % 5.91/1.59 | GROUND_INST: instantiating (15) with a, all_3_0, all_6_0, simplifying with % 5.91/1.59 | (14) gives: % 5.91/1.59 | (16) ~ ($lesseq(2, all_6_0)) | ~ ($lesseq(all_3_0, -1)) | ~ ($lesseq(0, % 5.91/1.59 | a)) % 5.91/1.59 | % 5.91/1.59 | BETA: splitting (16) gives: % 5.91/1.59 | % 5.91/1.59 | Case 1: % 5.91/1.59 | | % 5.91/1.59 | | (17) $lesseq(all_6_0, 1) % 5.91/1.59 | | % 5.91/1.59 | | COMBINE_INEQS: (6), (17) imply: % 5.91/1.59 | | (18) $false % 5.91/1.60 | | % 5.91/1.60 | | CLOSE: (18) is inconsistent. % 5.91/1.60 | | % 5.91/1.60 | Case 2: % 5.91/1.60 | | % 5.91/1.60 | | (19) ~ ($lesseq(all_3_0, -1)) | ~ ($lesseq(0, a)) % 5.91/1.60 | | % 5.91/1.60 | | BETA: splitting (19) gives: % 5.91/1.60 | | % 5.91/1.60 | | Case 1: % 5.91/1.60 | | | % 5.91/1.60 | | | (20) $lesseq(a, -1) % 5.91/1.60 | | | % 5.91/1.60 | | | COMBINE_INEQS: (20), (conj_001) imply: % 5.91/1.60 | | | (21) $false % 5.91/1.60 | | | % 5.91/1.60 | | | CLOSE: (21) is inconsistent. % 5.91/1.60 | | | % 5.91/1.60 | | Case 2: % 5.91/1.60 | | | % 5.91/1.60 | | | (22) $lesseq(0, all_3_0) % 5.91/1.60 | | | % 5.91/1.60 | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.60 | | | (23) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ ($lesseq(1, % 5.91/1.60 | | | $difference(v2, $product(7, v0)))) | ~ ($lesseq(v1, 7)) | % 5.91/1.60 | | | ~ ($lesseq(0, v0)) | ~ ($product(v1, v0) = v2)) % 5.91/1.60 | | | % 5.91/1.60 | | | GROUND_INST: instantiating (23) with a, all_3_0, all_6_0, simplifying with % 5.91/1.60 | | | (14) gives: % 5.91/1.60 | | | (24) ~ ($lesseq(1, $difference(all_6_0, $product(7, a)))) | ~ % 5.91/1.60 | | | ($lesseq(all_3_0, 7)) | ~ ($lesseq(0, a)) % 5.91/1.60 | | | % 5.91/1.60 | | | BETA: splitting (24) gives: % 5.91/1.60 | | | % 5.91/1.60 | | | Case 1: % 5.91/1.60 | | | | % 5.91/1.60 | | | | (25) $lesseq(8, all_3_0) % 5.91/1.60 | | | | % 5.91/1.60 | | | | COMBINE_INEQS: (2), (25) imply: % 5.91/1.60 | | | | (26) $false % 5.91/1.60 | | | | % 5.91/1.60 | | | | CLOSE: (26) is inconsistent. % 5.91/1.60 | | | | % 5.91/1.60 | | | Case 2: % 5.91/1.60 | | | | % 5.91/1.60 | | | | (27) ~ ($lesseq(1, $difference(all_6_0, $product(7, a)))) | ~ % 5.91/1.60 | | | | ($lesseq(0, a)) % 5.91/1.60 | | | | % 5.91/1.60 | | | | BETA: splitting (27) gives: % 5.91/1.60 | | | | % 5.91/1.60 | | | | Case 1: % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | (28) $lesseq(a, -1) % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | COMBINE_INEQS: (28), (conj_001) imply: % 5.91/1.60 | | | | | (29) $false % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | CLOSE: (29) is inconsistent. % 5.91/1.60 | | | | | % 5.91/1.60 | | | | Case 2: % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | (30) $lesseq(all_6_0, $product(7, a)) % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.60 | | | | | (31) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(v1, -1)) | ~ % 5.91/1.60 | | | | | ($lesseq(0, v0)) | ~ ($product(v0, v0) = v1)) % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | GROUND_INST: instantiating (31) with a, all_3_1, simplifying with (3) % 5.91/1.60 | | | | | gives: % 5.91/1.60 | | | | | (32) ~ ($lesseq(all_3_1, -1)) | ~ ($lesseq(0, a)) % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | BETA: splitting (32) gives: % 5.91/1.60 | | | | | % 5.91/1.60 | | | | | Case 1: % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | (33) $lesseq(a, -1) % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | COMBINE_INEQS: (33), (conj_001) imply: % 5.91/1.60 | | | | | | (34) $false % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | CLOSE: (34) is inconsistent. % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | Case 2: % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | (35) $lesseq(0, all_3_1) % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | COMBINE_INEQS: (6), (30) imply: % 5.91/1.60 | | | | | | (36) $lesseq(1, a) % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | SIMP: (36) implies: % 5.91/1.60 | | | | | | (37) $lesseq(1, a) % 5.91/1.60 | | | | | | % 5.91/1.60 | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.61 | | | | | | (38) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(v1, 0) | ~ % 5.91/1.61 | | | | | | ($lesseq(1, v0)) | ~ ($product(v0, v0) = v1)) % 5.91/1.61 | | | | | | % 5.91/1.61 | | | | | | GROUND_INST: instantiating (38) with a, all_3_1, simplifying with % 5.91/1.61 | | | | | | (3) gives: % 5.91/1.61 | | | | | | (39) ~ ($lesseq(all_3_1, 0) | ~ ($lesseq(1, a)) % 5.91/1.61 | | | | | | % 5.91/1.61 | | | | | | BETA: splitting (39) gives: % 5.91/1.61 | | | | | | % 5.91/1.61 | | | | | | Case 1: % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | (40) $lesseq(a, 0) % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | COMBINE_INEQS: (37), (40) imply: % 5.91/1.61 | | | | | | | (41) $false % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | CLOSE: (41) is inconsistent. % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | Case 2: % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | (42) $lesseq(1, all_3_1) % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.61 | | | | | | | (43) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.61 | | | | | | | ($lesseq(v2, 7)) | ~ ($lesseq(0, v2)) | ~ ($lesseq(5, % 5.91/1.61 | | | | | | | v1)) | ~ ($lesseq(1, v0)) | ~ ($product(v1, v0) = % 5.91/1.61 | | | | | | | v2) | ~ ($product(v0, v0) = v1)) % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | GROUND_INST: instantiating (43) with a, all_3_1, all_3_0, % 5.91/1.61 | | | | | | | simplifying with (3), (4) gives: % 5.91/1.61 | | | | | | | (44) ~ ($lesseq(all_3_0, 7)) | ~ ($lesseq(0, all_3_0)) | ~ % 5.91/1.61 | | | | | | | ($lesseq(5, all_3_1)) | ~ ($lesseq(1, a)) % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | BETA: splitting (44) gives: % 5.91/1.61 | | | | | | | % 5.91/1.61 | | | | | | | Case 1: % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | (45) ~ ($lesseq(all_3_0, 7)) | ~ ($lesseq(0, all_3_0)) % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | BETA: splitting (45) gives: % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | Case 1: % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | (46) $lesseq(8, all_3_0) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | COMBINE_INEQS: (2), (46) imply: % 5.91/1.61 | | | | | | | | | (47) $false % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | CLOSE: (47) is inconsistent. % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | Case 2: % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | (48) $lesseq(all_3_0, -1) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | COMBINE_INEQS: (22), (48) imply: % 5.91/1.61 | | | | | | | | | (49) $false % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | CLOSE: (49) is inconsistent. % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | End of split % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | Case 2: % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | (50) ~ ($lesseq(5, all_3_1)) | ~ ($lesseq(1, a)) % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | BETA: splitting (50) gives: % 5.91/1.61 | | | | | | | | % 5.91/1.61 | | | | | | | | Case 1: % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | (51) $lesseq(a, 0) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | COMBINE_INEQS: (37), (51) imply: % 5.91/1.61 | | | | | | | | | (52) $false % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | CLOSE: (52) is inconsistent. % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | Case 2: % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | (53) $lesseq(all_3_1, 4) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.61 | | | | | | | | | (54) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.61 | | | | | | | | | ($lesseq(1, $difference(v1, v2))) | ~ ($lesseq(0, % 5.91/1.61 | | | | | | | | | v1)) | ~ ($lesseq(1, v0)) | ~ ($product(v1, % 5.91/1.61 | | | | | | | | | v0) = v2)) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | GROUND_INST: instantiating (54) with a, all_3_0, all_6_0, % 5.91/1.61 | | | | | | | | | simplifying with (14) gives: % 5.91/1.61 | | | | | | | | | (55) ~ ($lesseq(1, $difference(all_3_0, all_6_0))) | ~ % 5.91/1.61 | | | | | | | | | ($lesseq(0, all_3_0)) | ~ ($lesseq(1, a)) % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | BETA: splitting (55) gives: % 5.91/1.61 | | | | | | | | | % 5.91/1.61 | | | | | | | | | Case 1: % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | (56) $lesseq(all_3_0, -1) % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | COMBINE_INEQS: (22), (56) imply: % 5.91/1.61 | | | | | | | | | | (57) $false % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | CLOSE: (57) is inconsistent. % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | Case 2: % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | (58) ~ ($lesseq(1, $difference(all_3_0, all_6_0))) | ~ % 5.91/1.61 | | | | | | | | | | ($lesseq(1, a)) % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | BETA: splitting (58) gives: % 5.91/1.61 | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | Case 1: % 5.91/1.61 | | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | | (59) $lesseq(a, 0) % 5.91/1.61 | | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | | COMBINE_INEQS: (37), (59) imply: % 5.91/1.61 | | | | | | | | | | | (60) $false % 5.91/1.61 | | | | | | | | | | | % 5.91/1.61 | | | | | | | | | | | CLOSE: (60) is inconsistent. % 5.91/1.61 | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | Case 2: % 5.91/1.62 | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | (61) $lesseq(all_3_0, all_6_0) % 5.91/1.62 | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | GROUND_INST: instantiating (54) with a, all_3_1, all_3_0, % 5.91/1.62 | | | | | | | | | | | simplifying with (4) gives: % 5.91/1.62 | | | | | | | | | | | (62) ~ ($lesseq(1, $difference(all_3_1, all_3_0))) | % 5.91/1.62 | | | | | | | | | | | ~ ($lesseq(0, all_3_1)) | ~ ($lesseq(1, a)) % 5.91/1.62 | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | BETA: splitting (62) gives: % 5.91/1.62 | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | Case 1: % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | (63) $lesseq(all_3_1, -1) % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | COMBINE_INEQS: (35), (63) imply: % 5.91/1.62 | | | | | | | | | | | | (64) $false % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | CLOSE: (64) is inconsistent. % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | Case 2: % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | (65) ~ ($lesseq(1, $difference(all_3_1, all_3_0))) | % 5.91/1.62 | | | | | | | | | | | | ~ ($lesseq(1, a)) % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | BETA: splitting (65) gives: % 5.91/1.62 | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | Case 1: % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | (66) $lesseq(a, 0) % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | COMBINE_INEQS: (37), (66) imply: % 5.91/1.62 | | | | | | | | | | | | | (67) $false % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | CLOSE: (67) is inconsistent. % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | Case 2: % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | (68) $lesseq(all_3_1, all_3_0) % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.62 | | | | | | | | | | | | | (69) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(2, % 5.91/1.62 | | | | | | | | | | | | | $difference($product(2, v0), v1))) | ~ % 5.91/1.62 | | | | | | | | | | | | | ($lesseq(1, v0)) | ~ ($product(v0, v0) = v1)) % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | GROUND_INST: instantiating (69) with a, all_3_1, simplifying % 5.91/1.62 | | | | | | | | | | | | | with (3) gives: % 5.91/1.62 | | | | | | | | | | | | | (70) ~ ($lesseq(2, $difference($product(2, a), % 5.91/1.62 | | | | | | | | | | | | | all_3_1))) | ~ ($lesseq(1, a)) % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | BETA: splitting (70) gives: % 5.91/1.62 | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | Case 1: % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | (71) $lesseq(a, 0) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (37), (71) imply: % 5.91/1.62 | | | | | | | | | | | | | | (72) $false % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | CLOSE: (72) is inconsistent. % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | Case 2: % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | (73) $lesseq(-1, $difference(all_3_1, $product(2, a))) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (30), (61) imply: % 5.91/1.62 | | | | | | | | | | | | | | (74) $lesseq(all_3_0, $product(7, a)) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (68), (74) imply: % 5.91/1.62 | | | | | | | | | | | | | | (75) $lesseq(all_3_1, $product(7, a)) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (42), (68) imply: % 5.91/1.62 | | | | | | | | | | | | | | (76) $lesseq(1, all_3_0) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (53), (73) imply: % 5.91/1.62 | | | | | | | | | | | | | | (77) $lesseq(a, 2) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | SIMP: (77) implies: % 5.91/1.62 | | | | | | | | | | | | | | (78) $lesseq(a, 2) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | COMBINE_INEQS: (42), (75) imply: % 5.91/1.62 | | | | | | | | | | | | | | (79) $lesseq(1, a) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.62 | | | | | | | | | | | | | | (80) ! [v0: int] : ! [v1: int] : ! [v2: int] : ! % 5.91/1.62 | | | | | | | | | | | | | | [v3: int] : ( ~ ($lesseq(1, $sum($difference(v3, % 5.91/1.62 | | | | | | | | | | | | | | $product(3, v2)), $product(2, v1)))) | % 5.91/1.62 | | | | | | | | | | | | | | ~ ($lesseq(v1, v2)) | ~ ($lesseq(v0, 2)) | ~ % 5.91/1.62 | | | | | | | | | | | | | | ($product(v2, v0) = v3) | ~ ($product(v1, v0) = % 5.91/1.62 | | | | | | | | | | | | | | v2)) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | GROUND_INST: instantiating (80) with a, all_3_1, all_3_0, % 5.91/1.62 | | | | | | | | | | | | | | all_6_0, simplifying with (4), (14) gives: % 5.91/1.62 | | | | | | | | | | | | | | (81) ~ ($lesseq(1, $sum($difference(all_6_0, % 5.91/1.62 | | | | | | | | | | | | | | $product(3, all_3_0)), $product(2, % 5.91/1.62 | | | | | | | | | | | | | | all_3_1)))) | ~ ($lesseq(all_3_1, % 5.91/1.62 | | | | | | | | | | | | | | all_3_0)) | ~ ($lesseq(a, 2)) % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | BETA: splitting (81) gives: % 5.91/1.62 | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | Case 1: % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | (82) $lesseq(1, $difference(all_3_1, all_3_0)) % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | COMBINE_INEQS: (68), (82) imply: % 5.91/1.62 | | | | | | | | | | | | | | | (83) $false % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | CLOSE: (83) is inconsistent. % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | Case 2: % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | (84) ~ ($lesseq(1, $sum($difference(all_6_0, % 5.91/1.62 | | | | | | | | | | | | | | | $product(3, all_3_0)), $product(2, % 5.91/1.62 | | | | | | | | | | | | | | | all_3_1)))) | ~ ($lesseq(a, 2)) % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | BETA: splitting (84) gives: % 5.91/1.62 | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | Case 1: % 5.91/1.62 | | | | | | | | | | | | | | | | % 5.91/1.62 | | | | | | | | | | | | | | | | (85) $lesseq(3, a) % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (85) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | (86) $false % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | CLOSE: (86) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | (87) $lesseq(0, $difference($difference($product(3, % 5.91/1.63 | | | | | | | | | | | | | | | | all_3_0), all_6_0), $product(2, all_3_1))) % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.63 | | | | | | | | | | | | | | | | (88) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.63 | | | | | | | | | | | | | | | | ($lesseq(-1, $difference($difference(v2, % 5.91/1.63 | | | | | | | | | | | | | | | | $product(2, v1)), v0))) | ~ ($lesseq(1, % 5.91/1.63 | | | | | | | | | | | | | | | | v1)) | ~ ($lesseq(v0, 2)) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | ($product(v1, v0) = v2)) % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | GROUND_INST: instantiating (88) with a, all_3_0, all_6_0, % 5.91/1.63 | | | | | | | | | | | | | | | | simplifying with (14) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | (89) ~ ($lesseq(-1, $difference($difference(all_6_0, % 5.91/1.63 | | | | | | | | | | | | | | | | $product(2, all_3_0)), a))) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | ($lesseq(1, all_3_0)) | ~ ($lesseq(a, 2)) % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | BETA: splitting (89) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | (90) $lesseq(all_3_0, 0) % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | COMBINE_INEQS: (76), (90) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | (91) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | CLOSE: (91) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | (92) ~ ($lesseq(-1, $difference($difference(all_6_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | $product(2, all_3_0)), a))) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | ($lesseq(a, 2)) % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | BETA: splitting (92) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | (93) $lesseq(3, a) % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (93) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | | (94) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | CLOSE: (94) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | (95) $lesseq(2, $sum($difference($product(2, all_3_0), % 5.91/1.63 | | | | | | | | | | | | | | | | | | all_6_0), a)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.63 | | | | | | | | | | | | | | | | | | (96) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | ($lesseq(9, $sum($difference($product(2, v1), % 5.91/1.63 | | | | | | | | | | | | | | | | | | v2), $product(4, v0)))) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | ($lesseq(v1, 4)) | ~ ($lesseq(v0, 2)) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | ($product(v1, v0) = v2)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (96) with a, all_3_1, all_3_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | | simplifying with (4) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | (97) ~ ($lesseq(9, $sum($difference($product(2, % 5.91/1.63 | | | | | | | | | | | | | | | | | | all_3_1), all_3_0), $product(4, a)))) | % 5.91/1.63 | | | | | | | | | | | | | | | | | | ~ ($lesseq(all_3_1, 4)) | ~ ($lesseq(a, 2)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | BETA: splitting (97) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | (98) $lesseq(5, all_3_1) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (53), (98) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | (99) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | CLOSE: (99) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | (100) ~ ($lesseq(9, $sum($difference($product(2, % 5.91/1.63 | | | | | | | | | | | | | | | | | | | all_3_1), all_3_0), $product(4, a)))) | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | ~ ($lesseq(a, 2)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | BETA: splitting (100) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | (101) $lesseq(3, a) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (101) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | (102) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | CLOSE: (102) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | (103) $lesseq(-8, $difference($difference(all_3_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | $product(2, all_3_1)), $product(4, a))) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | (104) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | ($lesseq(-3, $difference($difference(v2, v1), % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | $product(4, v0)))) | ~ ($lesseq(v1, 4)) | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(1, v0)) | ~ ($product(v1, v0) = % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | v2)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (104) with a, all_3_1, all_3_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | simplifying with (4) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | (105) ~ ($lesseq(-3, $difference($difference(all_3_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | all_3_1), $product(4, a)))) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | ($lesseq(all_3_1, 4)) | ~ ($lesseq(1, a)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | BETA: splitting (105) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | (106) $lesseq(5, all_3_1) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (53), (106) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | (107) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | CLOSE: (107) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | (108) ~ ($lesseq(-3, $difference($difference(all_3_0, % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | all_3_1), $product(4, a)))) | ~ % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | ($lesseq(1, a)) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | BETA: splitting (108) gives: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | (109) $lesseq(a, 0) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (37), (109) imply: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | (110) $false % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | CLOSE: (110) is inconsistent. % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | (111) $lesseq(4, $sum($difference(all_3_1, all_3_0), % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | $product(4, a))) % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.63 | | | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | (112) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | ($lesseq(3, $sum($difference(v2, $product(4, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | v1)), $product(5, v0)))) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | ($lesseq(-1, $difference(v1, $product(2, v0)))) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(v0, 2)) | ~ ($product(v1, v0) = % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | v2) | ~ ($product(v0, v0) = v1)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (112) with a, all_3_1, all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (4) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | (113) ~ ($lesseq(3, $sum($difference(all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | $product(4, all_3_1)), $product(5, a)))) | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(-1, $difference(all_3_1, $product(2, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | a)))) | ~ ($lesseq(a, 2)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (113) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | (114) $lesseq(2, $difference($product(2, a), all_3_1)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (73), (114) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | (115) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (115) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | (116) ~ ($lesseq(3, $sum($difference(all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | $product(4, all_3_1)), $product(5, a)))) | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(a, 2)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (116) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | (117) $lesseq(3, a) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (117) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | (118) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (118) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | (119) $lesseq(-2, $difference($difference($product(4, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | all_3_1), all_3_0), $product(5, a))) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | (120) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(0, $difference($difference($product(3, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | v1), v2), $product(3, v0)))) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(-1, $difference(v1, $product(2, v0)))) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(1, v0)) | ~ ($product(v1, v0) = % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | v2) | ~ ($product(v0, v0) = v1)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (120) with a, all_3_1, all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (3), (4) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | (121) ~ ($lesseq(0, $difference($difference($product(3, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | all_3_1), all_3_0), $product(3, a)))) | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(-1, $difference(all_3_1, $product(2, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | a)))) | ~ ($lesseq(1, a)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (121) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | (122) $lesseq(2, $difference($product(2, a), all_3_1)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (73), (122) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | (123) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (123) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | (124) ~ ($lesseq(0, $difference($difference($product(3, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | all_3_1), all_3_0), $product(3, a)))) | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | ~ ($lesseq(1, a)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (124) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | (125) $lesseq(a, 0) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (37), (125) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | (126) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (126) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | (127) $lesseq(1, $sum($difference(all_3_0, $product(3, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | all_3_1)), $product(3, a))) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (88) with a, all_3_1, all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (4) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | (128) ~ ($lesseq(-1, $difference($difference(all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | $product(2, all_3_1)), a))) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(1, all_3_1)) | ~ ($lesseq(a, 2)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (128) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | (129) $lesseq(all_3_1, 0) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (42), (129) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | (130) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (130) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | (131) ~ ($lesseq(-1, $difference($difference(all_3_0, % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | $product(2, all_3_1)), a))) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(a, 2)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (131) gives: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (132) $lesseq(3, a) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (132) imply: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (133) $false % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (133) is inconsistent. % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (134) $lesseq(2, $sum($difference($product(2, all_3_1), % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_3_0), a)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (135) ! [v0: int] : ! [v1: int] : ! [v2: int] : ( ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(2, $sum($difference(v1, v2), v0))) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(1, v1)) | ~ ($lesseq(1, v0)) | ~ % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($product(v1, v0) = v2)) % 5.91/1.64 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (135) with a, all_3_1, all_3_0, % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | simplifying with (4) gives: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | (136) ~ ($lesseq(2, $sum($difference(all_3_1, all_3_0), % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | a))) | ~ ($lesseq(1, all_3_1)) | ~ % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(1, a)) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (136) gives: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (137) $lesseq(all_3_1, 0) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (42), (137) imply: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (138) $false % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (138) is inconsistent. % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (139) ~ ($lesseq(2, $sum($difference(all_3_1, all_3_0), % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a))) | ~ ($lesseq(1, a)) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (139) gives: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (140) $lesseq(a, 0) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (37), (140) imply: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (141) $false % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (141) is inconsistent. % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (142) $lesseq(-1, $difference($difference(all_3_0, % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_3_1), a)) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (143) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(5, % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $difference($product(4, v0), v1))) | ~ % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(v0, 2)) | ~ ($product(v0, v0) = v1)) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (143) with a, all_3_1, simplifying % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with (3) gives: % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (144) ~ ($lesseq(5, $difference($product(4, a), % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_3_1))) | ~ ($lesseq(a, 2)) % 5.91/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (144) gives: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (145) $lesseq(3, a) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (145) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (146) $false % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (146) is inconsistent. % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (147) $lesseq(-4, $difference(all_3_1, $product(4, a))) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | THEORY_AXIOM GroebnerMultiplication: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (148) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(-1, % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $difference(v1, $product(3, v0)))) | ~ % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(v0, 2)) | ~ ($lesseq(1, v0)) | ~ % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($product(v0, v0) = v1)) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | GROUND_INST: instantiating (148) with a, all_3_1, simplifying % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | with (3) gives: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (149) ~ ($lesseq(-1, $difference(all_3_1, $product(3, % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a)))) | ~ ($lesseq(a, 2)) | ~ % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ($lesseq(1, a)) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (149) gives: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (150) $lesseq(3, a) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (78), (150) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (151) $false % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (151) is inconsistent. % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (152) ~ ($lesseq(-1, $difference(all_3_1, $product(3, % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a)))) | ~ ($lesseq(1, a)) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BETA: splitting (152) gives: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 1: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (153) $lesseq(a, 0) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (37), (153) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (154) $false % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (154) is inconsistent. % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Case 2: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (155) $lesseq(2, $difference($product(3, a), all_3_1)) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (6), (95) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (156) $lesseq(4, $sum($product(2, all_3_0), a)) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (134), (156) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (157) $lesseq(8, $sum($product(4, all_3_1), $product(3, % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | a))) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (111), (127) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (158) $lesseq(5, $difference($product(7, a), $product(2, % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | all_3_1))) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (157), (158) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (159) $lesseq(2, a) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (159) implies: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (160) $lesseq(2, a) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (6), (87) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (161) $lesseq(2, $difference($product(3, all_3_0), % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $product(2, all_3_1))) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (42), (161) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (162) $lesseq(2, all_3_0) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (162) implies: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (163) $lesseq(2, all_3_0) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (119), (163) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (164) $lesseq(0, $difference($product(4, all_3_1), % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $product(5, a))) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (160), (164) imply: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (165) $lesseq(3, all_3_1) % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (165) implies: % 6.39/1.65 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (166) $lesseq(3, all_3_1) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (2), (103) imply: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (167) $lesseq(-7, $difference($product(-1, all_3_1), % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | $product(2, a))) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (160), (167) imply: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (168) $lesseq(all_3_1, 3) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | SIMP: (168) implies: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (169) $lesseq(all_3_1, 3) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (155), (166) imply: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (170) $lesseq(2, a) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (147), (160) imply: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (171) $lesseq(4, all_3_1) % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | COMBINE_INEQS: (169), (171) imply: % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (172) $false % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | CLOSE: (172) is inconsistent. % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | | % 6.39/1.66 | | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | | % 6.39/1.66 | | | | | | | | | End of split % 6.39/1.66 | | | | | | | | | % 6.39/1.66 | | | | | | | | End of split % 6.39/1.66 | | | | | | | | % 6.39/1.66 | | | | | | | End of split % 6.39/1.66 | | | | | | | % 6.39/1.66 | | | | | | End of split % 6.39/1.66 | | | | | | % 6.39/1.66 | | | | | End of split % 6.39/1.66 | | | | | % 6.39/1.66 | | | | End of split % 6.39/1.66 | | | | % 6.39/1.66 | | | End of split % 6.39/1.66 | | | % 6.39/1.66 | | End of split % 6.39/1.66 | | % 6.39/1.66 | End of split % 6.39/1.66 | % 6.39/1.66 End of proof % 6.39/1.66 % SZS output end Proof for theBenchmark % 6.39/1.66 % 6.39/1.66 1032ms %------------------------------------------------------------------------------