%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV032+1 : TPTP v8.1.2. Bugfixed v3.3.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu Aug 31 22:54:39 EDT 2023 % Result : Theorem 24.54s 4.28s % Output : Proof 37.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.14 % Problem : SWV032+1 : TPTP v8.1.2. Bugfixed v3.3.0. % 0.00/0.15 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.16/0.37 % Computer : n012.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 300 % 0.16/0.37 % DateTime : Tue Aug 29 04:39:39 EDT 2023 % 0.16/0.37 % CPUTime : % 0.23/0.68 ________ _____ % 0.23/0.68 ___ __ \_________(_)________________________________ % 0.23/0.68 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.23/0.68 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.23/0.68 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.23/0.68 % 0.23/0.68 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.23/0.68 (2023-06-19) % 0.23/0.68 % 0.23/0.68 (c) Philipp Rümmer, 2009-2023 % 0.23/0.68 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.23/0.68 Amanda Stjerna. % 0.23/0.69 Free software under BSD-3-Clause. % 0.23/0.69 % 0.23/0.69 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.23/0.69 % 0.23/0.69 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.23/0.70 Running up to 7 provers in parallel. % 0.23/0.74 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.23/0.74 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.23/0.74 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.23/0.74 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.23/0.74 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.23/0.74 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.23/0.74 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 5.62/1.66 Prover 4: Preprocessing ... % 5.62/1.67 Prover 1: Preprocessing ... % 5.62/1.71 Prover 3: Preprocessing ... % 5.62/1.71 Prover 6: Preprocessing ... % 5.62/1.71 Prover 0: Preprocessing ... % 5.62/1.71 Prover 2: Preprocessing ... % 5.62/1.71 Prover 5: Preprocessing ... % 13.64/2.77 Prover 1: Warning: ignoring some quantifiers % 13.64/2.86 Prover 3: Warning: ignoring some quantifiers % 13.64/2.86 Prover 1: Constructing countermodel ... % 13.64/2.90 Prover 3: Constructing countermodel ... % 13.64/2.90 Prover 6: Proving ... % 13.64/2.94 Prover 4: Warning: ignoring some quantifiers % 15.65/3.09 Prover 4: Constructing countermodel ... % 15.65/3.11 Prover 5: Proving ... % 16.21/3.16 Prover 0: Proving ... % 16.95/3.27 Prover 2: Proving ... % 24.33/4.25 Prover 3: proved (3525ms) % 24.33/4.27 % 24.54/4.28 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 24.54/4.28 % 24.54/4.29 Prover 2: stopped % 24.54/4.31 Prover 5: stopped % 24.54/4.32 Prover 6: stopped % 24.54/4.35 Prover 0: stopped % 24.54/4.35 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 24.54/4.35 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 24.54/4.35 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 24.54/4.35 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 24.54/4.37 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 26.46/4.59 Prover 8: Preprocessing ... % 26.46/4.59 Prover 7: Preprocessing ... % 26.46/4.59 Prover 11: Preprocessing ... % 26.89/4.63 Prover 10: Preprocessing ... % 26.89/4.65 Prover 13: Preprocessing ... % 28.62/4.85 Prover 10: Warning: ignoring some quantifiers % 28.62/4.91 Prover 10: Constructing countermodel ... % 29.11/4.92 Prover 7: Warning: ignoring some quantifiers % 29.11/4.95 Prover 7: Constructing countermodel ... % 29.11/4.95 Prover 8: Warning: ignoring some quantifiers % 29.46/4.98 Prover 8: Constructing countermodel ... % 29.46/5.00 Prover 13: Warning: ignoring some quantifiers % 29.46/5.03 Prover 13: Constructing countermodel ... % 30.05/5.09 Prover 11: Warning: ignoring some quantifiers % 30.05/5.18 Prover 11: Constructing countermodel ... % 35.41/5.96 Prover 10: Found proof (size 97) % 35.41/5.96 Prover 10: proved (1632ms) % 35.41/5.96 Prover 7: stopped % 35.41/5.96 Prover 13: stopped % 35.41/5.96 Prover 11: stopped % 35.41/5.96 Prover 1: stopped % 35.41/5.96 Prover 8: stopped % 35.41/5.96 Prover 4: stopped % 35.41/5.96 % 35.41/5.96 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 35.41/5.96 % 35.41/5.98 % SZS output start Proof for theBenchmark % 35.41/5.99 Assumptions after simplification: % 35.41/5.99 --------------------------------- % 35.41/5.99 % 35.41/5.99 (const_array2_select) % 36.90/6.02 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 36.90/6.02 $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : ! [v10: $i] : % 36.90/6.02 (v10 = v6 | ~ (tptp_const_array2(v7, v8, v6) = v9) | ~ (a_select3(v9, v0, % 36.90/6.02 v3) = v10) | ~ (dim(v4, v5) = v8) | ~ (dim(v1, v2) = v7) | ~ $i(v6) | % 36.90/6.02 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 36.90/6.02 leq(v4, v3) | ~ leq(v3, v5) | ~ leq(v1, v0) | ~ leq(v0, v2)) % 36.90/6.02 % 36.90/6.02 (gauss_init_0041) % 36.90/6.03 $i(s_values7_init) & $i(simplex7_init) & $i(n330) & $i(n410) & $i(pv1376) & % 36.90/6.03 $i(pv20) & $i(pv19) & $i(init) & $i(n3) & $i(n2) & $i(n1) & $i(n0) & ? [v0: % 36.90/6.03 $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : % 36.90/6.03 ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: $i] : ? [v11: % 36.90/6.03 $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : (minus(n330, n1) = v1 & % 36.90/6.03 minus(n410, n1) = v0 & minus(pv1376, n1) = v2 & $i(v13) & $i(v12) & $i(v10) % 36.90/6.03 & $i(v2) & $i(v1) & $i(v0) & leq(pv1376, n3) & leq(pv20, v1) & leq(pv19, v0) % 36.90/6.03 & leq(n0, pv1376) & leq(n0, pv20) & leq(n0, pv19) & ! [v15: $i] : ! [v16: % 36.90/6.03 $i] : ! [v17: $i] : (v17 = init | ~ (a_select3(simplex7_init, v16, v15) % 36.90/6.03 = v17) | ~ $i(v16) | ~ $i(v15) | ~ leq(v16, n3) | ~ leq(v15, n2) | % 36.90/6.03 ~ leq(n0, v16) | ~ leq(n0, v15)) & ! [v15: $i] : ! [v16: $i] : (v16 = % 36.90/6.03 init | ~ (a_select2(s_values7_init, v15) = v16) | ~ $i(v15) | ~ % 36.90/6.03 leq(v15, v2) | ~ leq(n0, v15)) & (( ~ (v14 = init) & % 36.90/6.03 a_select3(simplex7_init, v13, v12) = v14 & $i(v14) & leq(v13, n3) & % 36.90/6.03 leq(v12, n2) & leq(n0, v13) & leq(n0, v12)) | ( ~ (v11 = init) & % 36.90/6.03 a_select2(s_values7_init, v10) = v11 & $i(v11) & leq(v10, v2) & leq(n0, % 36.90/6.03 v10)) | ( ~ (v9 = init) & tptp_const_array2(v6, v7, init) = v8 & % 36.90/6.03 a_select3(v8, pv19, pv20) = v9 & dim(n0, v1) = v7 & dim(n0, v0) = v6 & % 36.90/6.03 $i(v9) & $i(v8) & $i(v7) & $i(v6)) | ( ~ (v5 = init) & % 36.90/6.03 a_select3(simplex7_init, pv1376, n2) = v5 & $i(v5)) | ( ~ (v4 = init) & % 36.90/6.03 a_select3(simplex7_init, pv1376, n1) = v4 & $i(v4)) | ( ~ (v3 = init) & % 36.90/6.03 a_select3(simplex7_init, pv1376, n0) = v3 & $i(v3)))) % 36.90/6.03 % 36.90/6.03 (gt_1_0) % 36.90/6.03 $i(n1) & $i(n0) & gt(n1, n0) % 36.90/6.03 % 36.90/6.03 (gt_2_0) % 36.90/6.03 $i(n2) & $i(n0) & gt(n2, n0) % 36.90/6.03 % 36.90/6.03 (gt_3_0) % 36.90/6.03 $i(n3) & $i(n0) & gt(n3, n0) % 36.90/6.03 % 36.90/6.03 (gt_3_1) % 36.90/6.03 $i(n3) & $i(n1) & gt(n3, n1) % 36.90/6.03 % 36.90/6.03 (gt_3_2) % 36.90/6.03 $i(n3) & $i(n2) & gt(n3, n2) % 36.90/6.03 % 36.90/6.03 (leq_succ_gt_equiv) % 36.90/6.03 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (succ(v1) = v2) | ~ $i(v1) | ~ % 36.90/6.03 $i(v0) | ~ leq(v0, v1) | gt(v2, v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 36.90/6.03 $i] : ( ~ (succ(v1) = v2) | ~ $i(v1) | ~ $i(v0) | ~ gt(v2, v0) | leq(v0, % 36.90/6.03 v1)) % 36.90/6.03 % 36.90/6.03 (pred_minus_1) % 36.90/6.04 $i(n1) & ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 36.90/6.04 (pred(v0) = v1 & $i(v1))) % 36.90/6.04 % 36.90/6.04 (successor_1) % 36.90/6.04 succ(n0) = n1 & $i(n1) & $i(n0) % 36.90/6.04 % 36.90/6.04 (successor_2) % 36.90/6.04 $i(n2) & $i(n0) & ? [v0: $i] : (succ(v0) = n2 & succ(n0) = v0 & $i(v0)) % 36.90/6.04 % 36.90/6.04 (successor_3) % 36.90/6.04 $i(n3) & $i(n0) & ? [v0: $i] : ? [v1: $i] : (succ(v1) = n3 & succ(v0) = v1 & % 36.90/6.04 succ(n0) = v0 & $i(v1) & $i(v0)) % 36.90/6.04 % 36.90/6.04 (successor_4) % 36.90/6.04 $i(n4) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (succ(v2) = n4 & % 36.90/6.04 succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 & $i(v2) & $i(v1) & $i(v0)) % 36.90/6.04 % 36.90/6.04 (successor_5) % 36.90/6.04 $i(n5) & $i(n0) & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : % 36.90/6.04 (succ(v3) = n5 & succ(v2) = v3 & succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 % 36.90/6.04 & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 36.90/6.04 % 37.23/6.04 (function-axioms) % 37.23/6.05 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 37.23/6.05 $i] : (v1 = v0 | ~ (tptp_update3(v5, v4, v3, v2) = v1) | ~ % 37.23/6.05 (tptp_update3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 37.23/6.05 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_update2(v4, v3, v2) = % 37.23/6.05 v1) | ~ (tptp_update2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 37.23/6.05 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sum(v4, v3, v2) = v1) | % 37.23/6.05 ~ (sum(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 37.23/6.05 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_const_array2(v4, v3, v2) = v1) | % 37.23/6.05 ~ (tptp_const_array2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 37.23/6.05 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (a_select3(v4, v3, v2) = % 37.23/6.05 v1) | ~ (a_select3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 37.23/6.05 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (minus(v3, v2) = v1) | ~ (minus(v3, % 37.23/6.05 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 37.23/6.05 = v0 | ~ (plus(v3, v2) = v1) | ~ (plus(v3, v2) = v0)) & ! [v0: $i] : ! % 37.23/6.05 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_mmul(v3, v2) = v1) % 37.23/6.05 | ~ (tptp_mmul(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 37.23/6.05 ! [v3: $i] : (v1 = v0 | ~ (tptp_msub(v3, v2) = v1) | ~ (tptp_msub(v3, v2) = % 37.23/6.05 v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | % 37.23/6.05 ~ (tptp_madd(v3, v2) = v1) | ~ (tptp_madd(v3, v2) = v0)) & ! [v0: $i] : ! % 37.23/6.05 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (dim(v3, v2) = v1) | ~ % 37.23/6.05 (dim(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 37.23/6.05 : (v1 = v0 | ~ (tptp_const_array1(v3, v2) = v1) | ~ (tptp_const_array1(v3, % 37.23/6.05 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 37.23/6.05 = v0 | ~ (a_select2(v3, v2) = v1) | ~ (a_select2(v3, v2) = v0)) & ! [v0: % 37.23/6.05 $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 37.23/6.05 (uniform_int_rnd(v3, v2) = v1) | ~ (uniform_int_rnd(v3, v2) = v0)) & ! % 37.23/6.05 [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (inv(v2) = v1) | ~ % 37.23/6.05 (inv(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 37.23/6.05 (trans(v2) = v1) | ~ (trans(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 37.23/6.05 [v2: $i] : (v1 = v0 | ~ (succ(v2) = v1) | ~ (succ(v2) = v0)) & ! [v0: $i] : % 37.23/6.05 ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (pred(v2) = v1) | ~ (pred(v2) = % 37.23/6.05 v0)) % 37.23/6.05 % 37.23/6.05 Further assumptions not needed in the proof: % 37.23/6.05 -------------------------------------------- % 37.23/6.05 const_array1_select, defuse, finite_domain_0, finite_domain_1, finite_domain_2, % 37.23/6.05 finite_domain_3, finite_domain_4, finite_domain_5, gt_0_tptp_minus_1, % 37.23/6.05 gt_1_tptp_minus_1, gt_2_1, gt_2_tptp_minus_1, gt_330_0, gt_330_1, gt_330_2, % 37.23/6.05 gt_330_3, gt_330_4, gt_330_5, gt_330_tptp_minus_1, gt_3_tptp_minus_1, gt_410_0, % 37.23/6.05 gt_410_1, gt_410_2, gt_410_3, gt_410_330, gt_410_4, gt_410_5, % 37.23/6.05 gt_410_tptp_minus_1, gt_4_0, gt_4_1, gt_4_2, gt_4_3, gt_4_tptp_minus_1, gt_5_0, % 37.23/6.05 gt_5_1, gt_5_2, gt_5_3, gt_5_4, gt_5_tptp_minus_1, gt_succ, irreflexivity_gt, % 37.23/6.05 leq_geq, leq_gt1, leq_gt2, leq_gt_pred, leq_minus, leq_succ, leq_succ_gt, % 37.23/6.05 leq_succ_succ, lt_gt, matrix_symm_aba1, matrix_symm_aba2, matrix_symm_add, % 37.23/6.05 matrix_symm_inv, matrix_symm_joseph_update, matrix_symm_sub, matrix_symm_trans, % 37.23/6.05 matrix_symm_update_diagonal, pred_succ, reflexivity_leq, sel2_update_1, % 37.23/6.05 sel2_update_2, sel2_update_3, sel3_update_1, sel3_update_2, sel3_update_3, % 37.23/6.05 succ_plus_1_l, succ_plus_1_r, succ_plus_2_l, succ_plus_2_r, succ_plus_3_l, % 37.23/6.05 succ_plus_3_r, succ_plus_4_l, succ_plus_4_r, succ_plus_5_l, succ_plus_5_r, % 37.23/6.05 succ_pred, succ_tptp_minus_1, sum_plus_base, sum_plus_base_float, totality, % 37.23/6.05 transitivity_gt, transitivity_leq, ttrue, uniform_int_rand_ranges_hi, % 37.23/6.05 uniform_int_rand_ranges_lo % 37.23/6.05 % 37.23/6.05 Those formulas are unsatisfiable: % 37.23/6.05 --------------------------------- % 37.23/6.05 % 37.23/6.05 Begin of proof % 37.23/6.05 | % 37.23/6.05 | ALPHA: (leq_succ_gt_equiv) implies: % 37.23/6.05 | (1) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ (succ(v1) = v2) | ~ % 37.23/6.05 | $i(v1) | ~ $i(v0) | ~ gt(v2, v0) | leq(v0, v1)) % 37.23/6.05 | % 37.23/6.05 | ALPHA: (pred_minus_1) implies: % 37.23/6.06 | (2) ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 37.23/6.06 | (pred(v0) = v1 & $i(v1))) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gt_1_0) implies: % 37.23/6.06 | (3) gt(n1, n0) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gt_2_0) implies: % 37.23/6.06 | (4) gt(n2, n0) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gt_3_0) implies: % 37.23/6.06 | (5) gt(n3, n0) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gt_3_1) implies: % 37.23/6.06 | (6) gt(n3, n1) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gt_3_2) implies: % 37.23/6.06 | (7) gt(n3, n2) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (successor_4) implies: % 37.23/6.06 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : (succ(v2) = n4 & succ(v1) = % 37.23/6.06 | v2 & succ(v0) = v1 & succ(n0) = v0 & $i(v2) & $i(v1) & $i(v0)) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (successor_5) implies: % 37.23/6.06 | (9) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : (succ(v3) = n5 % 37.23/6.06 | & succ(v2) = v3 & succ(v1) = v2 & succ(v0) = v1 & succ(n0) = v0 & % 37.23/6.06 | $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (successor_1) implies: % 37.23/6.06 | (10) succ(n0) = n1 % 37.23/6.06 | % 37.23/6.06 | ALPHA: (successor_2) implies: % 37.23/6.06 | (11) ? [v0: $i] : (succ(v0) = n2 & succ(n0) = v0 & $i(v0)) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (successor_3) implies: % 37.23/6.06 | (12) ? [v0: $i] : ? [v1: $i] : (succ(v1) = n3 & succ(v0) = v1 & succ(n0) % 37.23/6.06 | = v0 & $i(v1) & $i(v0)) % 37.23/6.06 | % 37.23/6.06 | ALPHA: (gauss_init_0041) implies: % 37.23/6.06 | (13) $i(n0) % 37.23/6.06 | (14) $i(init) % 37.23/6.06 | (15) $i(pv19) % 37.23/6.06 | (16) $i(pv20) % 37.23/6.06 | (17) $i(pv1376) % 37.23/6.06 | (18) $i(n410) % 37.23/6.06 | (19) $i(n330) % 37.23/6.07 | (20) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 37.23/6.07 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : % 37.23/6.07 | ? [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: % 37.23/6.07 | $i] : (minus(n330, n1) = v1 & minus(n410, n1) = v0 & minus(pv1376, % 37.23/6.07 | n1) = v2 & $i(v13) & $i(v12) & $i(v10) & $i(v2) & $i(v1) & $i(v0) % 37.23/6.07 | & leq(pv1376, n3) & leq(pv20, v1) & leq(pv19, v0) & leq(n0, pv1376) % 37.23/6.07 | & leq(n0, pv20) & leq(n0, pv19) & ! [v15: $i] : ! [v16: $i] : ! % 37.23/6.07 | [v17: $i] : (v17 = init | ~ (a_select3(simplex7_init, v16, v15) = % 37.23/6.07 | v17) | ~ $i(v16) | ~ $i(v15) | ~ leq(v16, n3) | ~ leq(v15, % 37.23/6.07 | n2) | ~ leq(n0, v16) | ~ leq(n0, v15)) & ! [v15: $i] : ! % 37.23/6.07 | [v16: $i] : (v16 = init | ~ (a_select2(s_values7_init, v15) = v16) % 37.23/6.07 | | ~ $i(v15) | ~ leq(v15, v2) | ~ leq(n0, v15)) & (( ~ (v14 = % 37.23/6.07 | init) & a_select3(simplex7_init, v13, v12) = v14 & $i(v14) & % 37.23/6.07 | leq(v13, n3) & leq(v12, n2) & leq(n0, v13) & leq(n0, v12)) | ( ~ % 37.23/6.07 | (v11 = init) & a_select2(s_values7_init, v10) = v11 & $i(v11) & % 37.23/6.07 | leq(v10, v2) & leq(n0, v10)) | ( ~ (v9 = init) & % 37.23/6.07 | tptp_const_array2(v6, v7, init) = v8 & a_select3(v8, pv19, pv20) % 37.23/6.07 | = v9 & dim(n0, v1) = v7 & dim(n0, v0) = v6 & $i(v9) & $i(v8) & % 37.23/6.07 | $i(v7) & $i(v6)) | ( ~ (v5 = init) & a_select3(simplex7_init, % 37.23/6.07 | pv1376, n2) = v5 & $i(v5)) | ( ~ (v4 = init) & % 37.23/6.07 | a_select3(simplex7_init, pv1376, n1) = v4 & $i(v4)) | ( ~ (v3 = % 37.23/6.07 | init) & a_select3(simplex7_init, pv1376, n0) = v3 & $i(v3)))) % 37.23/6.07 | % 37.23/6.07 | ALPHA: (function-axioms) implies: % 37.23/6.07 | (21) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (succ(v2) = % 37.23/6.07 | v1) | ~ (succ(v2) = v0)) % 37.23/6.07 | % 37.23/6.07 | DELTA: instantiating (11) with fresh symbol all_54_0 gives: % 37.23/6.07 | (22) succ(all_54_0) = n2 & succ(n0) = all_54_0 & $i(all_54_0) % 37.23/6.07 | % 37.23/6.07 | ALPHA: (22) implies: % 37.23/6.07 | (23) $i(all_54_0) % 37.23/6.07 | (24) succ(n0) = all_54_0 % 37.23/6.07 | (25) succ(all_54_0) = n2 % 37.23/6.07 | % 37.23/6.07 | DELTA: instantiating (12) with fresh symbols all_57_0, all_57_1 gives: % 37.23/6.07 | (26) succ(all_57_0) = n3 & succ(all_57_1) = all_57_0 & succ(n0) = all_57_1 % 37.23/6.07 | & $i(all_57_0) & $i(all_57_1) % 37.23/6.07 | % 37.23/6.07 | ALPHA: (26) implies: % 37.23/6.07 | (27) $i(all_57_0) % 37.23/6.07 | (28) succ(n0) = all_57_1 % 37.23/6.07 | (29) succ(all_57_1) = all_57_0 % 37.23/6.07 | (30) succ(all_57_0) = n3 % 37.23/6.07 | % 37.23/6.07 | DELTA: instantiating (8) with fresh symbols all_59_0, all_59_1, all_59_2 % 37.23/6.07 | gives: % 37.23/6.07 | (31) succ(all_59_0) = n4 & succ(all_59_1) = all_59_0 & succ(all_59_2) = % 37.23/6.07 | all_59_1 & succ(n0) = all_59_2 & $i(all_59_0) & $i(all_59_1) & % 37.23/6.07 | $i(all_59_2) % 37.23/6.07 | % 37.23/6.07 | ALPHA: (31) implies: % 37.23/6.07 | (32) succ(n0) = all_59_2 % 37.23/6.07 | (33) succ(all_59_2) = all_59_1 % 37.23/6.07 | (34) succ(all_59_1) = all_59_0 % 37.23/6.07 | % 37.23/6.07 | DELTA: instantiating (9) with fresh symbols all_61_0, all_61_1, all_61_2, % 37.23/6.07 | all_61_3 gives: % 37.23/6.07 | (35) succ(all_61_0) = n5 & succ(all_61_1) = all_61_0 & succ(all_61_2) = % 37.23/6.07 | all_61_1 & succ(all_61_3) = all_61_2 & succ(n0) = all_61_3 & % 37.23/6.07 | $i(all_61_0) & $i(all_61_1) & $i(all_61_2) & $i(all_61_3) % 37.23/6.07 | % 37.23/6.07 | ALPHA: (35) implies: % 37.23/6.07 | (36) succ(n0) = all_61_3 % 37.23/6.07 | (37) succ(all_61_3) = all_61_2 % 37.23/6.07 | (38) succ(all_61_2) = all_61_1 % 37.23/6.07 | % 37.23/6.07 | DELTA: instantiating (20) with fresh symbols all_69_0, all_69_1, all_69_2, % 37.23/6.07 | all_69_3, all_69_4, all_69_5, all_69_6, all_69_7, all_69_8, all_69_9, % 37.23/6.07 | all_69_10, all_69_11, all_69_12, all_69_13, all_69_14 gives: % 37.23/6.08 | (39) minus(n330, n1) = all_69_13 & minus(n410, n1) = all_69_14 & % 37.23/6.08 | minus(pv1376, n1) = all_69_12 & $i(all_69_1) & $i(all_69_2) & % 37.23/6.08 | $i(all_69_4) & $i(all_69_12) & $i(all_69_13) & $i(all_69_14) & % 37.23/6.08 | leq(pv1376, n3) & leq(pv20, all_69_13) & leq(pv19, all_69_14) & % 37.23/6.08 | leq(n0, pv1376) & leq(n0, pv20) & leq(n0, pv19) & ! [v0: $i] : ! % 37.23/6.08 | [v1: $i] : ! [v2: $i] : (v2 = init | ~ (a_select3(simplex7_init, v1, % 37.23/6.08 | v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ leq(v1, n3) | ~ leq(v0, % 37.23/6.08 | n2) | ~ leq(n0, v1) | ~ leq(n0, v0)) & ! [v0: $i] : ! [v1: $i] % 37.23/6.08 | : (v1 = init | ~ (a_select2(s_values7_init, v0) = v1) | ~ $i(v0) | % 37.23/6.08 | ~ leq(v0, all_69_12) | ~ leq(n0, v0)) & (( ~ (all_69_0 = init) & % 37.23/6.08 | a_select3(simplex7_init, all_69_1, all_69_2) = all_69_0 & % 37.23/6.08 | $i(all_69_0) & leq(all_69_1, n3) & leq(all_69_2, n2) & leq(n0, % 37.23/6.08 | all_69_1) & leq(n0, all_69_2)) | ( ~ (all_69_3 = init) & % 37.23/6.08 | a_select2(s_values7_init, all_69_4) = all_69_3 & $i(all_69_3) & % 37.23/6.08 | leq(all_69_4, all_69_12) & leq(n0, all_69_4)) | ( ~ (all_69_5 = % 37.23/6.08 | init) & tptp_const_array2(all_69_8, all_69_7, init) = all_69_6 & % 37.23/6.08 | a_select3(all_69_6, pv19, pv20) = all_69_5 & dim(n0, all_69_13) = % 37.23/6.08 | all_69_7 & dim(n0, all_69_14) = all_69_8 & $i(all_69_5) & % 37.23/6.08 | $i(all_69_6) & $i(all_69_7) & $i(all_69_8)) | ( ~ (all_69_9 = % 37.23/6.08 | init) & a_select3(simplex7_init, pv1376, n2) = all_69_9 & % 37.23/6.08 | $i(all_69_9)) | ( ~ (all_69_10 = init) & a_select3(simplex7_init, % 37.23/6.08 | pv1376, n1) = all_69_10 & $i(all_69_10)) | ( ~ (all_69_11 = % 37.23/6.08 | init) & a_select3(simplex7_init, pv1376, n0) = all_69_11 & % 37.23/6.08 | $i(all_69_11))) % 37.23/6.08 | % 37.23/6.08 | ALPHA: (39) implies: % 37.23/6.08 | (40) leq(n0, pv19) % 37.23/6.08 | (41) leq(n0, pv20) % 37.23/6.08 | (42) leq(n0, pv1376) % 37.23/6.08 | (43) leq(pv19, all_69_14) % 37.23/6.08 | (44) leq(pv20, all_69_13) % 37.23/6.08 | (45) leq(pv1376, n3) % 37.23/6.08 | (46) $i(all_69_4) % 37.23/6.08 | (47) $i(all_69_2) % 37.23/6.08 | (48) $i(all_69_1) % 37.23/6.08 | (49) minus(n410, n1) = all_69_14 % 37.23/6.08 | (50) minus(n330, n1) = all_69_13 % 37.23/6.08 | (51) ( ~ (all_69_0 = init) & a_select3(simplex7_init, all_69_1, all_69_2) = % 37.23/6.08 | all_69_0 & $i(all_69_0) & leq(all_69_1, n3) & leq(all_69_2, n2) & % 37.23/6.08 | leq(n0, all_69_1) & leq(n0, all_69_2)) | ( ~ (all_69_3 = init) & % 37.23/6.08 | a_select2(s_values7_init, all_69_4) = all_69_3 & $i(all_69_3) & % 37.23/6.08 | leq(all_69_4, all_69_12) & leq(n0, all_69_4)) | ( ~ (all_69_5 = % 37.23/6.08 | init) & tptp_const_array2(all_69_8, all_69_7, init) = all_69_6 & % 37.23/6.08 | a_select3(all_69_6, pv19, pv20) = all_69_5 & dim(n0, all_69_13) = % 37.23/6.08 | all_69_7 & dim(n0, all_69_14) = all_69_8 & $i(all_69_5) & % 37.23/6.08 | $i(all_69_6) & $i(all_69_7) & $i(all_69_8)) | ( ~ (all_69_9 = init) % 37.23/6.08 | & a_select3(simplex7_init, pv1376, n2) = all_69_9 & $i(all_69_9)) | % 37.23/6.08 | ( ~ (all_69_10 = init) & a_select3(simplex7_init, pv1376, n1) = % 37.23/6.08 | all_69_10 & $i(all_69_10)) | ( ~ (all_69_11 = init) & % 37.23/6.08 | a_select3(simplex7_init, pv1376, n0) = all_69_11 & $i(all_69_11)) % 37.23/6.08 | (52) ! [v0: $i] : ! [v1: $i] : (v1 = init | ~ (a_select2(s_values7_init, % 37.23/6.08 | v0) = v1) | ~ $i(v0) | ~ leq(v0, all_69_12) | ~ leq(n0, v0)) % 37.23/6.08 | (53) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v2 = init | ~ % 37.23/6.08 | (a_select3(simplex7_init, v1, v0) = v2) | ~ $i(v1) | ~ $i(v0) | ~ % 37.23/6.08 | leq(v1, n3) | ~ leq(v0, n2) | ~ leq(n0, v1) | ~ leq(n0, v0)) % 37.23/6.08 | % 37.23/6.08 | GROUND_INST: instantiating (21) with all_57_1, all_59_2, n0, simplifying with % 37.23/6.09 | (28), (32) gives: % 37.23/6.09 | (54) all_59_2 = all_57_1 % 37.23/6.09 | % 37.23/6.09 | GROUND_INST: instantiating (21) with all_54_0, all_59_2, n0, simplifying with % 37.23/6.09 | (24), (32) gives: % 37.23/6.09 | (55) all_59_2 = all_54_0 % 37.23/6.09 | % 37.23/6.09 | GROUND_INST: instantiating (21) with all_57_1, all_61_3, n0, simplifying with % 37.23/6.09 | (28), (36) gives: % 37.23/6.09 | (56) all_61_3 = all_57_1 % 37.23/6.09 | % 37.23/6.09 | GROUND_INST: instantiating (21) with n1, all_61_3, n0, simplifying with (10), % 37.23/6.09 | (36) gives: % 37.23/6.09 | (57) all_61_3 = n1 % 37.23/6.09 | % 37.23/6.09 | COMBINE_EQS: (56), (57) imply: % 37.23/6.09 | (58) all_57_1 = n1 % 37.23/6.09 | % 37.23/6.09 | SIMP: (58) implies: % 37.23/6.09 | (59) all_57_1 = n1 % 37.23/6.09 | % 37.23/6.09 | COMBINE_EQS: (54), (55) imply: % 37.23/6.09 | (60) all_57_1 = all_54_0 % 37.23/6.09 | % 37.23/6.09 | SIMP: (60) implies: % 37.46/6.09 | (61) all_57_1 = all_54_0 % 37.46/6.09 | % 37.46/6.09 | COMBINE_EQS: (59), (61) imply: % 37.46/6.09 | (62) all_54_0 = n1 % 37.46/6.09 | % 37.46/6.09 | COMBINE_EQS: (55), (62) imply: % 37.46/6.09 | (63) all_59_2 = n1 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (37), (57) imply: % 37.46/6.09 | (64) succ(n1) = all_61_2 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (33), (63) imply: % 37.46/6.09 | (65) succ(n1) = all_59_1 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (29), (59) imply: % 37.46/6.09 | (66) succ(n1) = all_57_0 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (25), (62) imply: % 37.46/6.09 | (67) succ(n1) = n2 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (23), (62) imply: % 37.46/6.09 | (68) $i(n1) % 37.46/6.09 | % 37.46/6.09 | GROUND_INST: instantiating (21) with all_57_0, all_59_1, n1, simplifying with % 37.46/6.09 | (65), (66) gives: % 37.46/6.09 | (69) all_59_1 = all_57_0 % 37.46/6.09 | % 37.46/6.09 | GROUND_INST: instantiating (21) with all_59_1, all_61_2, n1, simplifying with % 37.46/6.09 | (64), (65) gives: % 37.46/6.09 | (70) all_61_2 = all_59_1 % 37.46/6.09 | % 37.46/6.09 | GROUND_INST: instantiating (21) with n2, all_61_2, n1, simplifying with (64), % 37.46/6.09 | (67) gives: % 37.46/6.09 | (71) all_61_2 = n2 % 37.46/6.09 | % 37.46/6.09 | COMBINE_EQS: (70), (71) imply: % 37.46/6.09 | (72) all_59_1 = n2 % 37.46/6.09 | % 37.46/6.09 | SIMP: (72) implies: % 37.46/6.09 | (73) all_59_1 = n2 % 37.46/6.09 | % 37.46/6.09 | COMBINE_EQS: (69), (73) imply: % 37.46/6.09 | (74) all_57_0 = n2 % 37.46/6.09 | % 37.46/6.09 | SIMP: (74) implies: % 37.46/6.09 | (75) all_57_0 = n2 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (38), (71) imply: % 37.46/6.09 | (76) succ(n2) = all_61_1 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (34), (73) imply: % 37.46/6.09 | (77) succ(n2) = all_59_0 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (30), (75) imply: % 37.46/6.09 | (78) succ(n2) = n3 % 37.46/6.09 | % 37.46/6.09 | REDUCE: (27), (75) imply: % 37.46/6.09 | (79) $i(n2) % 37.46/6.09 | % 37.46/6.09 | GROUND_INST: instantiating (21) with all_59_0, all_61_1, n2, simplifying with % 37.46/6.09 | (76), (77) gives: % 37.46/6.09 | (80) all_61_1 = all_59_0 % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (21) with n3, all_61_1, n2, simplifying with (76), % 37.46/6.10 | (78) gives: % 37.46/6.10 | (81) all_61_1 = n3 % 37.46/6.10 | % 37.46/6.10 | COMBINE_EQS: (80), (81) imply: % 37.46/6.10 | (82) all_59_0 = n3 % 37.46/6.10 | % 37.46/6.10 | SIMP: (82) implies: % 37.46/6.10 | (83) all_59_0 = n3 % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (1) with n0, n0, n1, simplifying with (3), (10), % 37.46/6.10 | (13) gives: % 37.46/6.10 | (84) leq(n0, n0) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (1) with n0, n1, n2, simplifying with (4), (13), % 37.46/6.10 | (67), (68) gives: % 37.46/6.10 | (85) leq(n0, n1) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (1) with n2, n2, n3, simplifying with (7), (78), % 37.46/6.10 | (79) gives: % 37.46/6.10 | (86) leq(n2, n2) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (1) with n1, n2, n3, simplifying with (6), (68), % 37.46/6.10 | (78), (79) gives: % 37.46/6.10 | (87) leq(n1, n2) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (1) with n0, n2, n3, simplifying with (5), (13), % 37.46/6.10 | (78), (79) gives: % 37.46/6.10 | (88) leq(n0, n2) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (2) with n410, all_69_14, simplifying with (18), % 37.46/6.10 | (49) gives: % 37.46/6.10 | (89) pred(n410) = all_69_14 & $i(all_69_14) % 37.46/6.10 | % 37.46/6.10 | ALPHA: (89) implies: % 37.46/6.10 | (90) $i(all_69_14) % 37.46/6.10 | % 37.46/6.10 | GROUND_INST: instantiating (2) with n330, all_69_13, simplifying with (19), % 37.46/6.10 | (50) gives: % 37.46/6.10 | (91) pred(n330) = all_69_13 & $i(all_69_13) % 37.46/6.10 | % 37.46/6.10 | ALPHA: (91) implies: % 37.46/6.10 | (92) $i(all_69_13) % 37.46/6.10 | % 37.46/6.10 | BETA: splitting (51) gives: % 37.46/6.10 | % 37.46/6.10 | Case 1: % 37.46/6.10 | | % 37.46/6.10 | | (93) ( ~ (all_69_0 = init) & a_select3(simplex7_init, all_69_1, all_69_2) % 37.46/6.10 | | = all_69_0 & $i(all_69_0) & leq(all_69_1, n3) & leq(all_69_2, n2) % 37.46/6.10 | | & leq(n0, all_69_1) & leq(n0, all_69_2)) | ( ~ (all_69_3 = init) & % 37.46/6.10 | | a_select2(s_values7_init, all_69_4) = all_69_3 & $i(all_69_3) & % 37.46/6.10 | | leq(all_69_4, all_69_12) & leq(n0, all_69_4)) | ( ~ (all_69_5 = % 37.46/6.10 | | init) & tptp_const_array2(all_69_8, all_69_7, init) = all_69_6 & % 37.46/6.10 | | a_select3(all_69_6, pv19, pv20) = all_69_5 & dim(n0, all_69_13) = % 37.46/6.10 | | all_69_7 & dim(n0, all_69_14) = all_69_8 & $i(all_69_5) & % 37.46/6.10 | | $i(all_69_6) & $i(all_69_7) & $i(all_69_8)) % 37.46/6.10 | | % 37.46/6.10 | | BETA: splitting (93) gives: % 37.46/6.10 | | % 37.46/6.10 | | Case 1: % 37.46/6.10 | | | % 37.46/6.10 | | | (94) ~ (all_69_0 = init) & a_select3(simplex7_init, all_69_1, % 37.46/6.10 | | | all_69_2) = all_69_0 & $i(all_69_0) & leq(all_69_1, n3) & % 37.46/6.10 | | | leq(all_69_2, n2) & leq(n0, all_69_1) & leq(n0, all_69_2) % 37.46/6.10 | | | % 37.46/6.10 | | | ALPHA: (94) implies: % 37.46/6.10 | | | (95) ~ (all_69_0 = init) % 37.46/6.10 | | | (96) leq(n0, all_69_2) % 37.46/6.10 | | | (97) leq(n0, all_69_1) % 37.46/6.11 | | | (98) leq(all_69_2, n2) % 37.46/6.11 | | | (99) leq(all_69_1, n3) % 37.46/6.11 | | | (100) a_select3(simplex7_init, all_69_1, all_69_2) = all_69_0 % 37.46/6.11 | | | % 37.46/6.11 | | | GROUND_INST: instantiating (53) with all_69_2, all_69_1, all_69_0, % 37.46/6.11 | | | simplifying with (47), (48), (96), (97), (98), (99), (100) % 37.46/6.11 | | | gives: % 37.46/6.11 | | | (101) all_69_0 = init % 37.46/6.11 | | | % 37.46/6.11 | | | REDUCE: (95), (101) imply: % 37.46/6.11 | | | (102) $false % 37.46/6.11 | | | % 37.46/6.11 | | | CLOSE: (102) is inconsistent. % 37.46/6.11 | | | % 37.46/6.11 | | Case 2: % 37.46/6.11 | | | % 37.46/6.11 | | | (103) ( ~ (all_69_3 = init) & a_select2(s_values7_init, all_69_4) = % 37.46/6.11 | | | all_69_3 & $i(all_69_3) & leq(all_69_4, all_69_12) & leq(n0, % 37.46/6.11 | | | all_69_4)) | ( ~ (all_69_5 = init) & % 37.46/6.11 | | | tptp_const_array2(all_69_8, all_69_7, init) = all_69_6 & % 37.46/6.11 | | | a_select3(all_69_6, pv19, pv20) = all_69_5 & dim(n0, all_69_13) % 37.46/6.11 | | | = all_69_7 & dim(n0, all_69_14) = all_69_8 & $i(all_69_5) & % 37.46/6.11 | | | $i(all_69_6) & $i(all_69_7) & $i(all_69_8)) % 37.46/6.11 | | | % 37.46/6.11 | | | BETA: splitting (103) gives: % 37.46/6.11 | | | % 37.46/6.11 | | | Case 1: % 37.46/6.11 | | | | % 37.46/6.11 | | | | (104) ~ (all_69_3 = init) & a_select2(s_values7_init, all_69_4) = % 37.46/6.11 | | | | all_69_3 & $i(all_69_3) & leq(all_69_4, all_69_12) & leq(n0, % 37.46/6.11 | | | | all_69_4) % 37.46/6.11 | | | | % 37.46/6.11 | | | | ALPHA: (104) implies: % 37.46/6.11 | | | | (105) ~ (all_69_3 = init) % 37.46/6.11 | | | | (106) leq(n0, all_69_4) % 37.46/6.11 | | | | (107) leq(all_69_4, all_69_12) % 37.46/6.11 | | | | (108) a_select2(s_values7_init, all_69_4) = all_69_3 % 37.46/6.11 | | | | % 37.46/6.11 | | | | GROUND_INST: instantiating (52) with all_69_4, all_69_3, simplifying % 37.46/6.11 | | | | with (46), (106), (107), (108) gives: % 37.46/6.11 | | | | (109) all_69_3 = init % 37.46/6.11 | | | | % 37.46/6.11 | | | | REDUCE: (105), (109) imply: % 37.46/6.11 | | | | (110) $false % 37.46/6.11 | | | | % 37.46/6.11 | | | | CLOSE: (110) is inconsistent. % 37.46/6.11 | | | | % 37.46/6.11 | | | Case 2: % 37.46/6.11 | | | | % 37.46/6.11 | | | | (111) ~ (all_69_5 = init) & tptp_const_array2(all_69_8, all_69_7, % 37.46/6.11 | | | | init) = all_69_6 & a_select3(all_69_6, pv19, pv20) = all_69_5 % 37.46/6.11 | | | | & dim(n0, all_69_13) = all_69_7 & dim(n0, all_69_14) = all_69_8 % 37.46/6.11 | | | | & $i(all_69_5) & $i(all_69_6) & $i(all_69_7) & $i(all_69_8) % 37.46/6.11 | | | | % 37.46/6.11 | | | | ALPHA: (111) implies: % 37.46/6.11 | | | | (112) ~ (all_69_5 = init) % 37.46/6.11 | | | | (113) dim(n0, all_69_14) = all_69_8 % 37.46/6.11 | | | | (114) dim(n0, all_69_13) = all_69_7 % 37.46/6.11 | | | | (115) a_select3(all_69_6, pv19, pv20) = all_69_5 % 37.46/6.11 | | | | (116) tptp_const_array2(all_69_8, all_69_7, init) = all_69_6 % 37.46/6.11 | | | | % 37.46/6.12 | | | | GROUND_INST: instantiating (const_array2_select) with pv19, n0, % 37.46/6.12 | | | | all_69_14, pv20, n0, all_69_13, init, all_69_8, all_69_7, % 37.46/6.12 | | | | all_69_6, all_69_5, simplifying with (13), (14), (15), % 37.46/6.12 | | | | (16), (40), (41), (43), (44), (90), (92), (113), (114), % 37.46/6.12 | | | | (115), (116) gives: % 37.46/6.12 | | | | (117) all_69_5 = init % 37.46/6.12 | | | | % 37.46/6.12 | | | | REDUCE: (112), (117) imply: % 37.46/6.12 | | | | (118) $false % 37.46/6.12 | | | | % 37.46/6.12 | | | | CLOSE: (118) is inconsistent. % 37.46/6.12 | | | | % 37.46/6.12 | | | End of split % 37.46/6.12 | | | % 37.46/6.12 | | End of split % 37.46/6.12 | | % 37.46/6.12 | Case 2: % 37.46/6.12 | | % 37.46/6.12 | | (119) ( ~ (all_69_9 = init) & a_select3(simplex7_init, pv1376, n2) = % 37.46/6.12 | | all_69_9 & $i(all_69_9)) | ( ~ (all_69_10 = init) & % 37.46/6.12 | | a_select3(simplex7_init, pv1376, n1) = all_69_10 & $i(all_69_10)) % 37.46/6.12 | | | ( ~ (all_69_11 = init) & a_select3(simplex7_init, pv1376, n0) = % 37.46/6.12 | | all_69_11 & $i(all_69_11)) % 37.46/6.12 | | % 37.46/6.12 | | BETA: splitting (119) gives: % 37.46/6.12 | | % 37.46/6.12 | | Case 1: % 37.46/6.12 | | | % 37.46/6.12 | | | (120) ~ (all_69_9 = init) & a_select3(simplex7_init, pv1376, n2) = % 37.46/6.12 | | | all_69_9 & $i(all_69_9) % 37.46/6.12 | | | % 37.46/6.12 | | | ALPHA: (120) implies: % 37.46/6.12 | | | (121) ~ (all_69_9 = init) % 37.46/6.12 | | | (122) a_select3(simplex7_init, pv1376, n2) = all_69_9 % 37.46/6.12 | | | % 37.46/6.12 | | | GROUND_INST: instantiating (53) with n2, pv1376, all_69_9, simplifying % 37.46/6.12 | | | with (17), (42), (45), (79), (86), (88), (122) gives: % 37.46/6.12 | | | (123) all_69_9 = init % 37.46/6.12 | | | % 37.46/6.12 | | | REDUCE: (121), (123) imply: % 37.46/6.12 | | | (124) $false % 37.46/6.12 | | | % 37.46/6.12 | | | CLOSE: (124) is inconsistent. % 37.46/6.12 | | | % 37.46/6.12 | | Case 2: % 37.46/6.12 | | | % 37.46/6.12 | | | (125) ( ~ (all_69_10 = init) & a_select3(simplex7_init, pv1376, n1) = % 37.46/6.12 | | | all_69_10 & $i(all_69_10)) | ( ~ (all_69_11 = init) & % 37.46/6.12 | | | a_select3(simplex7_init, pv1376, n0) = all_69_11 & % 37.46/6.12 | | | $i(all_69_11)) % 37.46/6.12 | | | % 37.46/6.12 | | | BETA: splitting (125) gives: % 37.46/6.12 | | | % 37.46/6.12 | | | Case 1: % 37.46/6.12 | | | | % 37.46/6.12 | | | | (126) ~ (all_69_10 = init) & a_select3(simplex7_init, pv1376, n1) = % 37.46/6.12 | | | | all_69_10 & $i(all_69_10) % 37.46/6.12 | | | | % 37.46/6.12 | | | | ALPHA: (126) implies: % 37.46/6.13 | | | | (127) ~ (all_69_10 = init) % 37.46/6.13 | | | | (128) a_select3(simplex7_init, pv1376, n1) = all_69_10 % 37.46/6.13 | | | | % 37.46/6.13 | | | | GROUND_INST: instantiating (53) with n1, pv1376, all_69_10, simplifying % 37.46/6.13 | | | | with (17), (42), (45), (68), (85), (87), (128) gives: % 37.46/6.13 | | | | (129) all_69_10 = init % 37.46/6.13 | | | | % 37.46/6.13 | | | | REDUCE: (127), (129) imply: % 37.46/6.13 | | | | (130) $false % 37.46/6.13 | | | | % 37.46/6.13 | | | | CLOSE: (130) is inconsistent. % 37.46/6.13 | | | | % 37.46/6.13 | | | Case 2: % 37.46/6.13 | | | | % 37.46/6.13 | | | | (131) ~ (all_69_11 = init) & a_select3(simplex7_init, pv1376, n0) = % 37.46/6.13 | | | | all_69_11 & $i(all_69_11) % 37.46/6.13 | | | | % 37.46/6.13 | | | | ALPHA: (131) implies: % 37.46/6.13 | | | | (132) ~ (all_69_11 = init) % 37.46/6.13 | | | | (133) a_select3(simplex7_init, pv1376, n0) = all_69_11 % 37.46/6.13 | | | | % 37.46/6.13 | | | | GROUND_INST: instantiating (53) with n0, pv1376, all_69_11, simplifying % 37.46/6.13 | | | | with (13), (17), (42), (45), (84), (88), (133) gives: % 37.46/6.13 | | | | (134) all_69_11 = init % 37.46/6.13 | | | | % 37.46/6.13 | | | | REDUCE: (132), (134) imply: % 37.46/6.13 | | | | (135) $false % 37.46/6.13 | | | | % 37.46/6.13 | | | | CLOSE: (135) is inconsistent. % 37.46/6.13 | | | | % 37.46/6.13 | | | End of split % 37.46/6.13 | | | % 37.46/6.13 | | End of split % 37.46/6.13 | | % 37.46/6.13 | End of split % 37.46/6.13 | % 37.46/6.13 End of proof % 37.46/6.13 % SZS output end Proof for theBenchmark % 37.46/6.13 % 37.46/6.13 5445ms %------------------------------------------------------------------------------