%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWV050+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 : n025.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:42 EDT 2023 % Result : Theorem 16.15s 2.99s % Output : Proof 19.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV050+1 : TPTP v8.1.2. Bugfixed v3.3.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Aug 29 03:37:55 EDT 2023 % 0.13/0.33 % CPUTime : % 0.18/0.61 ________ _____ % 0.18/0.61 ___ __ \_________(_)________________________________ % 0.18/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.18/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.18/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.18/0.61 % 0.18/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.18/0.61 (2023-06-19) % 0.18/0.61 % 0.18/0.61 (c) Philipp Rümmer, 2009-2023 % 0.18/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.18/0.61 Amanda Stjerna. % 0.18/0.61 Free software under BSD-3-Clause. % 0.18/0.61 % 0.18/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.18/0.61 % 0.18/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.18/0.62 Running up to 7 provers in parallel. % 0.18/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.18/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.18/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.18/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.18/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.18/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.18/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.72/1.42 Prover 4: Preprocessing ... % 4.72/1.42 Prover 1: Preprocessing ... % 4.72/1.45 Prover 3: Preprocessing ... % 4.72/1.45 Prover 5: Preprocessing ... % 4.72/1.45 Prover 0: Preprocessing ... % 4.72/1.45 Prover 6: Preprocessing ... % 4.72/1.46 Prover 2: Preprocessing ... % 10.53/2.27 Prover 1: Warning: ignoring some quantifiers % 11.09/2.35 Prover 3: Warning: ignoring some quantifiers % 12.04/2.43 Prover 1: Constructing countermodel ... % 12.04/2.43 Prover 4: Warning: ignoring some quantifiers % 12.04/2.43 Prover 3: Constructing countermodel ... % 12.25/2.44 Prover 6: Proving ... % 12.25/2.49 Prover 5: Proving ... % 12.25/2.51 Prover 4: Constructing countermodel ... % 12.98/2.58 Prover 0: Proving ... % 13.45/2.65 Prover 2: Proving ... % 16.15/2.99 Prover 3: proved (2352ms) % 16.15/2.99 % 16.15/2.99 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 16.15/2.99 % 16.15/3.01 Prover 6: stopped % 16.15/3.01 Prover 2: stopped % 16.15/3.01 Prover 5: stopped % 16.15/3.02 Prover 0: stopped % 16.15/3.03 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 16.15/3.03 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 16.15/3.03 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 16.15/3.03 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 16.15/3.03 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 16.87/3.07 Prover 1: Found proof (size 16) % 16.87/3.07 Prover 1: proved (2439ms) % 16.87/3.07 Prover 4: stopped % 17.33/3.16 Prover 7: Preprocessing ... % 17.33/3.17 Prover 13: Preprocessing ... % 17.33/3.17 Prover 10: Preprocessing ... % 17.33/3.17 Prover 11: Preprocessing ... % 17.33/3.20 Prover 8: Preprocessing ... % 18.13/3.23 Prover 7: stopped % 18.13/3.26 Prover 10: stopped % 18.13/3.27 Prover 11: stopped % 18.13/3.28 Prover 13: stopped % 18.88/3.43 Prover 8: Warning: ignoring some quantifiers % 18.88/3.45 Prover 8: Constructing countermodel ... % 19.34/3.47 Prover 8: stopped % 19.34/3.47 % 19.34/3.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.34/3.47 % 19.34/3.47 % SZS output start Proof for theBenchmark % 19.34/3.48 Assumptions after simplification: % 19.34/3.48 --------------------------------- % 19.34/3.48 % 19.34/3.48 (cl5_nebula_norm_0022) % 19.61/3.53 $i(sigmaold) & $i(pv91) & $i(sigma) & $i(pv88) & $i(rhoold) & $i(pv89) & % 19.61/3.53 $i(rho) & $i(pv86) & $i(muold) & $i(pv87) & $i(mu) & $i(n5) & $i(n1) & $i(n0) % 19.61/3.53 & ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? % 19.61/3.53 [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? [v10: % 19.61/3.53 $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : ? [v15: % 19.61/3.53 $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: $i] : ? [v20: % 19.61/3.53 $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? [v24: $i] : ? [v25: % 19.61/3.53 $i] : ? [v26: $i] : ( ~ (v26 = n0) & abs(v20) = v21 & abs(v19) = v23 & % 19.61/3.53 abs(v18) = v22 & abs(v11) = v12 & abs(v10) = v14 & abs(v9) = v13 & abs(v3) = % 19.61/3.53 v4 & abs(v2) = v6 & abs(v1) = v5 & divide(v21, v24) = v25 & divide(v12, v15) % 19.61/3.53 = v16 & divide(v4, v7) = v8 & minus(v18, v19) = v20 & minus(v9, v10) = v11 & % 19.61/3.53 minus(v1, v2) = v3 & minus(n5, n1) = v0 & minus(n0, n1) = v17 & plus(v22, % 19.61/3.53 v23) = v24 & plus(v13, v14) = v15 & plus(v5, v6) = v7 & sum(n0, v17, v25) % 19.61/3.53 = v26 & sum(n0, v0, v16) = pv88 & sum(n0, v0, v8) = pv86 & % 19.61/3.53 a_select2(sigmaold, pv91) = v19 & a_select2(sigma, pv91) = v18 & % 19.61/3.53 a_select2(rhoold, pv89) = v10 & a_select2(rho, pv89) = v9 & a_select2(muold, % 19.61/3.53 pv87) = v2 & a_select2(mu, pv87) = v1 & $i(v26) & $i(v25) & $i(v24) & % 19.61/3.53 $i(v23) & $i(v22) & $i(v21) & $i(v20) & $i(v19) & $i(v18) & $i(v17) & % 19.61/3.54 $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & $i(v11) & $i(v10) & $i(v9) % 19.61/3.54 & $i(v8) & $i(v7) & $i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & % 19.61/3.54 $i(v0)) % 19.61/3.54 % 19.61/3.54 (gt_3_tptp_minus_1) % 19.61/3.54 gt(n3, tptp_minus_1) = 0 & $i(n3) & $i(tptp_minus_1) % 19.61/3.54 % 19.61/3.54 (pred_minus_1) % 19.61/3.54 $i(n1) & ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 19.61/3.54 (pred(v0) = v1 & $i(v1))) % 19.61/3.54 % 19.61/3.54 (pred_succ) % 19.61/3.54 ! [v0: $i] : ! [v1: $i] : ( ~ (succ(v0) = v1) | ~ $i(v0) | pred(v1) = v0) % 19.61/3.54 % 19.61/3.54 (succ_tptp_minus_1) % 19.61/3.54 succ(tptp_minus_1) = n0 & $i(tptp_minus_1) & $i(n0) % 19.61/3.54 % 19.61/3.54 (sum_plus_base) % 19.61/3.54 $i(tptp_minus_1) & $i(n0) & ! [v0: $i] : ! [v1: $i] : (v1 = n0 | ~ (sum(n0, % 19.61/3.54 tptp_minus_1, v0) = v1) | ~ $i(v0)) % 19.61/3.54 % 19.61/3.54 (function-axioms) % 19.61/3.56 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 19.61/3.56 $i] : (v1 = v0 | ~ (tptp_update3(v5, v4, v3, v2) = v1) | ~ % 19.61/3.56 (tptp_update3(v5, v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 19.61/3.56 $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_update2(v4, v3, v2) = % 19.61/3.56 v1) | ~ (tptp_update2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 19.61/3.56 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (sum(v4, v3, v2) = v1) | % 19.61/3.56 ~ (sum(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! % 19.61/3.56 [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (tptp_const_array2(v4, v3, v2) = v1) | % 19.61/3.56 ~ (tptp_const_array2(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 19.61/3.56 [v2: $i] : ! [v3: $i] : ! [v4: $i] : (v1 = v0 | ~ (a_select3(v4, v3, v2) = % 19.61/3.56 v1) | ~ (a_select3(v4, v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! % 19.61/3.56 [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (divide(v3, v2) = v1) | ~ (divide(v3, % 19.61/3.56 v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 % 19.61/3.56 = v0 | ~ (minus(v3, v2) = v1) | ~ (minus(v3, v2) = v0)) & ! [v0: $i] : ! % 19.61/3.56 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (plus(v3, v2) = v1) | ~ % 19.61/3.56 (plus(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 19.61/3.56 : (v1 = v0 | ~ (tptp_mmul(v3, v2) = v1) | ~ (tptp_mmul(v3, v2) = v0)) & ! % 19.61/3.56 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.61/3.56 (tptp_msub(v3, v2) = v1) | ~ (tptp_msub(v3, v2) = v0)) & ! [v0: $i] : ! % 19.61/3.56 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (tptp_madd(v3, v2) = v1) % 19.61/3.56 | ~ (tptp_madd(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 19.61/3.56 ! [v3: $i] : (v1 = v0 | ~ (dim(v3, v2) = v1) | ~ (dim(v3, v2) = v0)) & ! % 19.61/3.56 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.61/3.56 (tptp_const_array1(v3, v2) = v1) | ~ (tptp_const_array1(v3, v2) = v0)) & ! % 19.61/3.56 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ % 19.61/3.56 (a_select2(v3, v2) = v1) | ~ (a_select2(v3, v2) = v0)) & ! [v0: $i] : ! % 19.61/3.56 [v1: $i] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (uniform_int_rnd(v3, v2) % 19.61/3.56 = v1) | ~ (uniform_int_rnd(v3, v2) = v0)) & ! [v0: MultipleValueBool] : % 19.61/3.56 ! [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (geq(v3, % 19.61/3.56 v2) = v1) | ~ (geq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! % 19.61/3.56 [v1: MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (lt(v3, % 19.61/3.56 v2) = v1) | ~ (lt(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.61/3.56 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (leq(v3, v2) % 19.61/3.56 = v1) | ~ (leq(v3, v2) = v0)) & ! [v0: MultipleValueBool] : ! [v1: % 19.61/3.56 MultipleValueBool] : ! [v2: $i] : ! [v3: $i] : (v1 = v0 | ~ (gt(v3, v2) = % 19.61/3.56 v1) | ~ (gt(v3, v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 19.61/3.56 (v1 = v0 | ~ (abs(v2) = v1) | ~ (abs(v2) = v0)) & ! [v0: $i] : ! [v1: $i] % 19.61/3.56 : ! [v2: $i] : (v1 = v0 | ~ (inv(v2) = v1) | ~ (inv(v2) = v0)) & ! [v0: % 19.61/3.56 $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (trans(v2) = v1) | ~ % 19.61/3.56 (trans(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 19.61/3.56 (succ(v2) = v1) | ~ (succ(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 19.61/3.56 $i] : (v1 = v0 | ~ (pred(v2) = v1) | ~ (pred(v2) = v0)) % 19.61/3.56 % 19.61/3.56 Further assumptions not needed in the proof: % 19.61/3.56 -------------------------------------------- % 19.61/3.56 const_array1_select, const_array2_select, defuse, finite_domain_0, % 19.61/3.56 finite_domain_1, finite_domain_2, finite_domain_3, finite_domain_4, % 19.61/3.56 finite_domain_5, gt_0_tptp_minus_1, gt_1_0, gt_1_tptp_minus_1, gt_2_0, gt_2_1, % 19.61/3.56 gt_2_tptp_minus_1, gt_3_0, gt_3_1, gt_3_2, gt_4_0, gt_4_1, gt_4_2, gt_4_3, % 19.61/3.56 gt_4_tptp_minus_1, gt_5_0, gt_5_1, gt_5_2, gt_5_3, gt_5_4, gt_5_tptp_minus_1, % 19.61/3.56 gt_succ, irreflexivity_gt, leq_geq, leq_gt1, leq_gt2, leq_gt_pred, leq_minus, % 19.61/3.56 leq_succ, leq_succ_gt, leq_succ_gt_equiv, leq_succ_succ, lt_gt, % 19.61/3.56 matrix_symm_aba1, matrix_symm_aba2, matrix_symm_add, matrix_symm_inv, % 19.61/3.56 matrix_symm_joseph_update, matrix_symm_sub, matrix_symm_trans, % 19.61/3.56 matrix_symm_update_diagonal, reflexivity_leq, sel2_update_1, sel2_update_2, % 19.61/3.56 sel2_update_3, sel3_update_1, sel3_update_2, sel3_update_3, succ_plus_1_l, % 19.61/3.56 succ_plus_1_r, succ_plus_2_l, succ_plus_2_r, succ_plus_3_l, succ_plus_3_r, % 19.61/3.56 succ_plus_4_l, succ_plus_4_r, succ_plus_5_l, succ_plus_5_r, succ_pred, % 19.61/3.56 successor_1, successor_2, successor_3, successor_4, successor_5, % 19.61/3.56 sum_plus_base_float, totality, transitivity_gt, transitivity_leq, ttrue, % 19.61/3.56 uniform_int_rand_ranges_hi, uniform_int_rand_ranges_lo % 19.61/3.56 % 19.61/3.56 Those formulas are unsatisfiable: % 19.61/3.56 --------------------------------- % 19.61/3.56 % 19.61/3.56 Begin of proof % 19.61/3.56 | % 19.61/3.56 | ALPHA: (sum_plus_base) implies: % 19.61/3.56 | (1) ! [v0: $i] : ! [v1: $i] : (v1 = n0 | ~ (sum(n0, tptp_minus_1, v0) = % 19.61/3.56 | v1) | ~ $i(v0)) % 19.61/3.56 | % 19.61/3.56 | ALPHA: (succ_tptp_minus_1) implies: % 19.61/3.56 | (2) succ(tptp_minus_1) = n0 % 19.61/3.56 | % 19.61/3.56 | ALPHA: (pred_minus_1) implies: % 19.61/3.56 | (3) ! [v0: $i] : ! [v1: $i] : ( ~ (minus(v0, n1) = v1) | ~ $i(v0) | % 19.61/3.56 | (pred(v0) = v1 & $i(v1))) % 19.61/3.56 | % 19.61/3.56 | ALPHA: (gt_3_tptp_minus_1) implies: % 19.61/3.56 | (4) $i(tptp_minus_1) % 19.61/3.56 | % 19.61/3.56 | ALPHA: (cl5_nebula_norm_0022) implies: % 19.61/3.56 | (5) $i(n0) % 19.61/3.57 | (6) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 19.61/3.57 | ? [v5: $i] : ? [v6: $i] : ? [v7: $i] : ? [v8: $i] : ? [v9: $i] : ? % 19.61/3.57 | [v10: $i] : ? [v11: $i] : ? [v12: $i] : ? [v13: $i] : ? [v14: $i] : % 19.61/3.57 | ? [v15: $i] : ? [v16: $i] : ? [v17: $i] : ? [v18: $i] : ? [v19: % 19.61/3.57 | $i] : ? [v20: $i] : ? [v21: $i] : ? [v22: $i] : ? [v23: $i] : ? % 19.61/3.57 | [v24: $i] : ? [v25: $i] : ? [v26: $i] : ( ~ (v26 = n0) & abs(v20) = % 19.61/3.57 | v21 & abs(v19) = v23 & abs(v18) = v22 & abs(v11) = v12 & abs(v10) = % 19.61/3.57 | v14 & abs(v9) = v13 & abs(v3) = v4 & abs(v2) = v6 & abs(v1) = v5 & % 19.61/3.57 | divide(v21, v24) = v25 & divide(v12, v15) = v16 & divide(v4, v7) = v8 % 19.61/3.57 | & minus(v18, v19) = v20 & minus(v9, v10) = v11 & minus(v1, v2) = v3 & % 19.61/3.57 | minus(n5, n1) = v0 & minus(n0, n1) = v17 & plus(v22, v23) = v24 & % 19.61/3.57 | plus(v13, v14) = v15 & plus(v5, v6) = v7 & sum(n0, v17, v25) = v26 & % 19.61/3.57 | sum(n0, v0, v16) = pv88 & sum(n0, v0, v8) = pv86 & % 19.61/3.57 | a_select2(sigmaold, pv91) = v19 & a_select2(sigma, pv91) = v18 & % 19.61/3.57 | a_select2(rhoold, pv89) = v10 & a_select2(rho, pv89) = v9 & % 19.61/3.57 | a_select2(muold, pv87) = v2 & a_select2(mu, pv87) = v1 & $i(v26) & % 19.61/3.57 | $i(v25) & $i(v24) & $i(v23) & $i(v22) & $i(v21) & $i(v20) & $i(v19) & % 19.61/3.57 | $i(v18) & $i(v17) & $i(v16) & $i(v15) & $i(v14) & $i(v13) & $i(v12) & % 19.61/3.57 | $i(v11) & $i(v10) & $i(v9) & $i(v8) & $i(v7) & $i(v6) & $i(v5) & % 19.61/3.57 | $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0)) % 19.61/3.57 | % 19.61/3.57 | ALPHA: (function-axioms) implies: % 19.61/3.57 | (7) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (pred(v2) = v1) % 19.61/3.57 | | ~ (pred(v2) = v0)) % 19.61/3.57 | % 19.61/3.57 | DELTA: instantiating (6) with fresh symbols all_74_0, all_74_1, all_74_2, % 19.61/3.57 | all_74_3, all_74_4, all_74_5, all_74_6, all_74_7, all_74_8, all_74_9, % 19.61/3.57 | all_74_10, all_74_11, all_74_12, all_74_13, all_74_14, all_74_15, % 19.61/3.57 | all_74_16, all_74_17, all_74_18, all_74_19, all_74_20, all_74_21, % 19.61/3.57 | all_74_22, all_74_23, all_74_24, all_74_25, all_74_26 gives: % 19.61/3.57 | (8) ~ (all_74_0 = n0) & abs(all_74_6) = all_74_5 & abs(all_74_7) = % 19.61/3.57 | all_74_3 & abs(all_74_8) = all_74_4 & abs(all_74_15) = all_74_14 & % 19.61/3.57 | abs(all_74_16) = all_74_12 & abs(all_74_17) = all_74_13 & % 19.61/3.57 | abs(all_74_23) = all_74_22 & abs(all_74_24) = all_74_20 & % 19.61/3.57 | abs(all_74_25) = all_74_21 & divide(all_74_5, all_74_2) = all_74_1 & % 19.61/3.57 | divide(all_74_14, all_74_11) = all_74_10 & divide(all_74_22, all_74_19) % 19.61/3.57 | = all_74_18 & minus(all_74_8, all_74_7) = all_74_6 & minus(all_74_17, % 19.61/3.57 | all_74_16) = all_74_15 & minus(all_74_25, all_74_24) = all_74_23 & % 19.61/3.57 | minus(n5, n1) = all_74_26 & minus(n0, n1) = all_74_9 & plus(all_74_4, % 19.61/3.57 | all_74_3) = all_74_2 & plus(all_74_13, all_74_12) = all_74_11 & % 19.61/3.57 | plus(all_74_21, all_74_20) = all_74_19 & sum(n0, all_74_9, all_74_1) = % 19.61/3.57 | all_74_0 & sum(n0, all_74_26, all_74_10) = pv88 & sum(n0, all_74_26, % 19.61/3.57 | all_74_18) = pv86 & a_select2(sigmaold, pv91) = all_74_7 & % 19.61/3.57 | a_select2(sigma, pv91) = all_74_8 & a_select2(rhoold, pv89) = all_74_16 % 19.61/3.57 | & a_select2(rho, pv89) = all_74_17 & a_select2(muold, pv87) = all_74_24 % 19.61/3.57 | & a_select2(mu, pv87) = all_74_25 & $i(all_74_0) & $i(all_74_1) & % 19.61/3.57 | $i(all_74_2) & $i(all_74_3) & $i(all_74_4) & $i(all_74_5) & % 19.61/3.57 | $i(all_74_6) & $i(all_74_7) & $i(all_74_8) & $i(all_74_9) & % 19.61/3.57 | $i(all_74_10) & $i(all_74_11) & $i(all_74_12) & $i(all_74_13) & % 19.61/3.57 | $i(all_74_14) & $i(all_74_15) & $i(all_74_16) & $i(all_74_17) & % 19.61/3.57 | $i(all_74_18) & $i(all_74_19) & $i(all_74_20) & $i(all_74_21) & % 19.61/3.57 | $i(all_74_22) & $i(all_74_23) & $i(all_74_24) & $i(all_74_25) & % 19.61/3.57 | $i(all_74_26) % 19.61/3.58 | % 19.61/3.58 | ALPHA: (8) implies: % 19.61/3.58 | (9) ~ (all_74_0 = n0) % 19.61/3.58 | (10) $i(all_74_1) % 19.61/3.58 | (11) sum(n0, all_74_9, all_74_1) = all_74_0 % 19.61/3.58 | (12) minus(n0, n1) = all_74_9 % 19.61/3.58 | % 19.61/3.58 | GROUND_INST: instantiating (pred_succ) with tptp_minus_1, n0, simplifying with % 19.61/3.58 | (2), (4) gives: % 19.61/3.58 | (13) pred(n0) = tptp_minus_1 % 19.61/3.58 | % 19.61/3.58 | GROUND_INST: instantiating (3) with n0, all_74_9, simplifying with (5), (12) % 19.61/3.58 | gives: % 19.61/3.58 | (14) pred(n0) = all_74_9 & $i(all_74_9) % 19.61/3.58 | % 19.61/3.58 | ALPHA: (14) implies: % 19.61/3.58 | (15) pred(n0) = all_74_9 % 19.61/3.58 | % 19.61/3.58 | GROUND_INST: instantiating (7) with tptp_minus_1, all_74_9, n0, simplifying % 19.61/3.58 | with (13), (15) gives: % 19.61/3.58 | (16) all_74_9 = tptp_minus_1 % 19.61/3.58 | % 19.61/3.58 | REDUCE: (11), (16) imply: % 19.61/3.58 | (17) sum(n0, tptp_minus_1, all_74_1) = all_74_0 % 19.61/3.58 | % 19.61/3.58 | GROUND_INST: instantiating (1) with all_74_1, all_74_0, simplifying with (10), % 19.61/3.58 | (17) gives: % 19.61/3.58 | (18) all_74_0 = n0 % 19.61/3.58 | % 19.61/3.58 | REDUCE: (9), (18) imply: % 19.61/3.58 | (19) $false % 19.61/3.58 | % 19.61/3.58 | CLOSE: (19) is inconsistent. % 19.61/3.58 | % 19.61/3.58 End of proof % 19.61/3.58 % SZS output end Proof for theBenchmark % 19.61/3.58 % 19.61/3.58 2972ms %------------------------------------------------------------------------------