%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWW616_2 : TPTP v8.1.2. Released v6.1.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.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 : Fri Sep 1 00:50:55 EDT 2023 % Result : Theorem 15.94s 3.04s % Output : Proof 20.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : SWW616_2 : TPTP v8.1.2. Released v6.1.0. % 0.00/0.11 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.31 % Computer : n006.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Aug 27 17:46:22 EDT 2023 % 0.11/0.32 % CPUTime : % 0.16/0.61 ________ _____ % 0.16/0.61 ___ __ \_________(_)________________________________ % 0.16/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.16/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.16/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.16/0.61 % 0.16/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.16/0.61 (2023-06-19) % 0.16/0.62 % 0.16/0.62 (c) Philipp Rümmer, 2009-2023 % 0.16/0.62 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.16/0.62 Amanda Stjerna. % 0.16/0.62 Free software under BSD-3-Clause. % 0.16/0.62 % 0.16/0.62 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.16/0.62 % 0.16/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.16/0.64 Running up to 7 provers in parallel. % 0.16/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.16/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.16/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.16/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.16/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.16/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.16/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.64/1.50 Prover 1: Preprocessing ... % 4.64/1.50 Prover 0: Preprocessing ... % 4.64/1.50 Prover 5: Preprocessing ... % 4.64/1.50 Prover 2: Preprocessing ... % 4.64/1.51 Prover 4: Preprocessing ... % 4.64/1.51 Prover 3: Preprocessing ... % 4.64/1.53 Prover 6: Preprocessing ... % 12.58/2.56 Prover 1: Warning: ignoring some quantifiers % 13.25/2.66 Prover 4: Warning: ignoring some quantifiers % 13.25/2.73 Prover 3: Warning: ignoring some quantifiers % 13.25/2.74 Prover 1: Constructing countermodel ... % 13.25/2.78 Prover 3: Constructing countermodel ... % 13.25/2.79 Prover 4: Constructing countermodel ... % 13.25/2.80 Prover 6: Proving ... % 13.85/2.82 Prover 0: Proving ... % 15.25/2.94 Prover 5: Proving ... % 15.94/3.04 Prover 3: proved (2383ms) % 15.94/3.04 % 15.94/3.04 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.94/3.04 % 15.94/3.04 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 15.94/3.04 Prover 2: Proving ... % 15.94/3.05 Prover 2: stopped % 15.94/3.05 Prover 0: stopped % 15.94/3.05 Prover 5: stopped % 15.94/3.06 Prover 6: stopped % 15.94/3.06 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 15.94/3.06 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 15.94/3.06 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 15.94/3.08 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 16.48/3.15 Prover 1: Found proof (size 16) % 16.48/3.15 Prover 1: proved (2503ms) % 16.48/3.15 Prover 4: stopped % 17.51/3.34 Prover 13: Preprocessing ... % 17.51/3.35 Prover 8: Preprocessing ... % 17.51/3.35 Prover 11: Preprocessing ... % 17.51/3.37 Prover 10: Preprocessing ... % 17.51/3.43 Prover 7: Preprocessing ... % 18.46/3.47 Prover 10: stopped % 18.46/3.49 Prover 11: stopped % 18.46/3.52 Prover 13: stopped % 19.67/3.55 Prover 7: stopped % 19.67/3.61 Prover 8: Warning: ignoring some quantifiers % 20.12/3.64 Prover 8: Constructing countermodel ... % 20.12/3.66 Prover 8: stopped % 20.12/3.66 % 20.12/3.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.12/3.66 % 20.12/3.66 % SZS output start Proof for theBenchmark % 20.12/3.67 Assumptions after simplification: % 20.12/3.67 --------------------------------- % 20.12/3.67 % 20.12/3.67 (wP_parameter_maximum_subarray_rec) % 20.43/3.69 ? [v0: map_int_int] : ? [v1: int] : ? [v2: int] : ? [v3: int] : ? [v4: % 20.43/3.69 int] : ($lesseq(1, v3) & $lesseq(1, $difference(v2, v1)) & $lesseq(0, v1) & % 20.43/3.69 sum(v0, v1, $sum(v3, v1)) = v4 & div($difference(v2, v1), 2) = v3 & % 20.43/3.69 map_int_int(v0) & ? [v5: int] : ? [v6: int] : ? [v7: int] : ($lesseq(0, % 20.43/3.69 $sum($difference(v3, v6), v1)) & $lesseq(v1, v6) & $lesseq(1, % 20.43/3.69 $difference($difference(v2, v3), v1)) & sum(v0, v6, $sum(v3, v1)) = v7 & % 20.43/3.69 sum(v0, v6, $sum(v3, v1)) = v5 & ! [v8: int] : ! [v9: int] : ( ~ % 20.43/3.69 ($lesseq(1, $difference(v9, v7))) | ~ ($lesseq(0, $sum($difference(v3, % 20.43/3.69 v8), v1))) | ~ ($lesseq(v1, v8)) | ~ (sum(v0, v8, $sum(v3, % 20.43/3.69 v1)) = v9)) & ! [v8: int] : ! [v9: int] : ( ~ ($lesseq(1, % 20.43/3.69 $difference(v9, v5))) | ~ ($lesseq(0, $sum($difference(v3, v8), % 20.43/3.69 v1))) | ~ ($lesseq(v1, v8)) | ~ (sum(v0, v8, $sum(v3, v1)) = % 20.43/3.69 v9)) & ? [v8: int] : ? [v9: int] : ($lesseq(1, $difference(v9, v5)) % 20.43/3.69 & $lesseq(0, $sum($difference(v3, v8), v1)) & $lesseq(v1, v8) & sum(v0, % 20.43/3.69 v8, $sum(v3, v1)) = v9))) % 20.43/3.69 % 20.43/3.69 Further assumptions not needed in the proof: % 20.43/3.69 -------------------------------------------- % 20.43/3.69 abs_def, abs_le, abs_pos, array_inversion, bool_inversion, bridgeL, bridgeL1, % 20.43/3.69 bridgeL2, bridgeR, bridgeR1, bridgeR2, compatOrderMult, const1, const_sort, % 20.43/3.69 contents_def, contents_sort, div_1, div_bound, div_inf, div_mod, div_mult, % 20.43/3.69 div_sign_neg, div_sign_pos, elts_def, elts_sort, get_def, get_sort, get_sort1, % 20.43/3.69 length_def, make_def, make_sort, match_bool_False, match_bool_True, % 20.43/3.69 match_bool_sort, maxsub_def, maxsublo_def, mk_array_sort, mk_ref_sort, mod_1, % 20.43/3.69 mod_bound, mod_inf, mod_mult, mod_sign_neg, mod_sign_pos, ref_inversion, % 20.43/3.69 rounds_toward_zero, select_eq, select_neq, set_def, set_sort, set_sort1, % 20.43/3.69 sum_def, sum_def_empty, sum_def_non_empty, sum_eq, sum_right_extension, % 20.43/3.69 sum_transitivity, t2tb_sort, t2tb_sort1, t2tb_sort2, true_False, % 20.43/3.69 tuple0_inversion, witness_sort % 20.43/3.69 % 20.43/3.69 Those formulas are unsatisfiable: % 20.43/3.69 --------------------------------- % 20.43/3.69 % 20.43/3.69 Begin of proof % 20.43/3.69 | % 20.43/3.69 | DELTA: instantiating (wP_parameter_maximum_subarray_rec) with fresh symbols % 20.43/3.69 | all_86_0, all_86_1, all_86_2, all_86_3, all_86_4 gives: % 20.43/3.70 | (1) $lesseq(1, all_86_1) & $lesseq(1, $difference(all_86_2, all_86_3)) & % 20.43/3.70 | $lesseq(0, all_86_3) & sum(all_86_4, all_86_3, $sum(all_86_1, % 20.43/3.70 | all_86_3)) = all_86_0 & div($difference(all_86_2, all_86_3), 2) = % 20.43/3.70 | all_86_1 & map_int_int(all_86_4) & ? [v0: int] : ? [v1: int] : ? % 20.43/3.70 | [v2: int] : ($lesseq(0, $sum($difference(all_86_1, v1), all_86_3)) & % 20.43/3.70 | $lesseq(all_86_3, v1) & $lesseq(1, $difference($difference(all_86_2, % 20.43/3.70 | all_86_1), all_86_3)) & sum(all_86_4, v1, $sum(all_86_1, % 20.43/3.70 | all_86_3)) = v2 & sum(all_86_4, v1, $sum(all_86_1, all_86_3)) = % 20.43/3.70 | v0 & ! [v3: int] : ! [v4: int] : ( ~ ($lesseq(1, $difference(v4, % 20.43/3.70 | v2))) | ~ ($lesseq(0, $sum($difference(all_86_1, v3), % 20.43/3.70 | all_86_3))) | ~ ($lesseq(all_86_3, v3)) | ~ (sum(all_86_4, % 20.43/3.70 | v3, $sum(all_86_1, all_86_3)) = v4)) & ! [v3: int] : ! [v4: % 20.43/3.70 | int] : ( ~ ($lesseq(1, $difference(v4, v0))) | ~ ($lesseq(0, % 20.43/3.70 | $sum($difference(all_86_1, v3), all_86_3))) | ~ % 20.43/3.70 | ($lesseq(all_86_3, v3)) | ~ (sum(all_86_4, v3, $sum(all_86_1, % 20.43/3.70 | all_86_3)) = v4)) & ? [v3: int] : ? [v4: int] : ($lesseq(1, % 20.43/3.70 | $difference(v4, v0)) & $lesseq(0, $sum($difference(all_86_1, v3), % 20.43/3.70 | all_86_3)) & $lesseq(all_86_3, v3) & sum(all_86_4, v3, % 20.43/3.70 | $sum(all_86_1, all_86_3)) = v4)) % 20.43/3.70 | % 20.43/3.70 | ALPHA: (1) implies: % 20.43/3.70 | (2) ? [v0: int] : ? [v1: int] : ? [v2: int] : ($lesseq(0, % 20.43/3.70 | $sum($difference(all_86_1, v1), all_86_3)) & $lesseq(all_86_3, v1) % 20.43/3.70 | & $lesseq(1, $difference($difference(all_86_2, all_86_1), all_86_3)) % 20.43/3.70 | & sum(all_86_4, v1, $sum(all_86_1, all_86_3)) = v2 & sum(all_86_4, % 20.43/3.70 | v1, $sum(all_86_1, all_86_3)) = v0 & ! [v3: int] : ! [v4: int] : % 20.43/3.70 | ( ~ ($lesseq(1, $difference(v4, v2))) | ~ ($lesseq(0, % 20.43/3.70 | $sum($difference(all_86_1, v3), all_86_3))) | ~ % 20.43/3.70 | ($lesseq(all_86_3, v3)) | ~ (sum(all_86_4, v3, $sum(all_86_1, % 20.43/3.70 | all_86_3)) = v4)) & ! [v3: int] : ! [v4: int] : ( ~ % 20.43/3.70 | ($lesseq(1, $difference(v4, v0))) | ~ ($lesseq(0, % 20.43/3.71 | $sum($difference(all_86_1, v3), all_86_3))) | ~ % 20.43/3.71 | ($lesseq(all_86_3, v3)) | ~ (sum(all_86_4, v3, $sum(all_86_1, % 20.43/3.71 | all_86_3)) = v4)) & ? [v3: int] : ? [v4: int] : ($lesseq(1, % 20.43/3.71 | $difference(v4, v0)) & $lesseq(0, $sum($difference(all_86_1, v3), % 20.43/3.71 | all_86_3)) & $lesseq(all_86_3, v3) & sum(all_86_4, v3, % 20.43/3.71 | $sum(all_86_1, all_86_3)) = v4)) % 20.43/3.71 | % 20.43/3.71 | DELTA: instantiating (2) with fresh symbols all_89_0, all_89_1, all_89_2 % 20.43/3.71 | gives: % 20.43/3.71 | (3) $lesseq(0, $sum($difference(all_86_1, all_89_1), all_86_3)) & % 20.43/3.71 | $lesseq(all_86_3, all_89_1) & $lesseq(1, % 20.43/3.71 | $difference($difference(all_86_2, all_86_1), all_86_3)) & % 20.43/3.71 | sum(all_86_4, all_89_1, $sum(all_86_1, all_86_3)) = all_89_0 & % 20.43/3.71 | sum(all_86_4, all_89_1, $sum(all_86_1, all_86_3)) = all_89_2 & ! [v0: % 20.43/3.71 | int] : ! [v1: int] : ( ~ ($lesseq(1, $difference(v1, all_89_0))) | % 20.43/3.71 | ~ ($lesseq(0, $sum($difference(all_86_1, v0), all_86_3))) | ~ % 20.43/3.71 | ($lesseq(all_86_3, v0)) | ~ (sum(all_86_4, v0, $sum(all_86_1, % 20.43/3.71 | all_86_3)) = v1)) & ! [v0: int] : ! [v1: int] : ( ~ % 20.43/3.71 | ($lesseq(1, $difference(v1, all_89_2))) | ~ ($lesseq(0, % 20.43/3.71 | $sum($difference(all_86_1, v0), all_86_3))) | ~ % 20.43/3.71 | ($lesseq(all_86_3, v0)) | ~ (sum(all_86_4, v0, $sum(all_86_1, % 20.43/3.71 | all_86_3)) = v1)) & ? [v0: int] : ? [v1: int] : ($lesseq(1, % 20.43/3.71 | $difference(v1, all_89_2)) & $lesseq(0, $sum($difference(all_86_1, % 20.43/3.71 | v0), all_86_3)) & $lesseq(all_86_3, v0) & sum(all_86_4, v0, % 20.43/3.71 | $sum(all_86_1, all_86_3)) = v1) % 20.43/3.71 | % 20.43/3.71 | ALPHA: (3) implies: % 20.43/3.71 | (4) ! [v0: int] : ! [v1: int] : ( ~ ($lesseq(1, $difference(v1, % 20.43/3.71 | all_89_2))) | ~ ($lesseq(0, $sum($difference(all_86_1, v0), % 20.43/3.71 | all_86_3))) | ~ ($lesseq(all_86_3, v0)) | ~ (sum(all_86_4, % 20.43/3.71 | v0, $sum(all_86_1, all_86_3)) = v1)) % 20.43/3.71 | (5) ? [v0: int] : ? [v1: int] : ($lesseq(1, $difference(v1, all_89_2)) & % 20.43/3.71 | $lesseq(0, $sum($difference(all_86_1, v0), all_86_3)) & % 20.43/3.71 | $lesseq(all_86_3, v0) & sum(all_86_4, v0, $sum(all_86_1, all_86_3)) = % 20.43/3.71 | v1) % 20.43/3.71 | % 20.43/3.71 | DELTA: instantiating (5) with fresh symbols all_93_0, all_93_1 gives: % 20.43/3.71 | (6) $lesseq(1, $difference(all_93_0, all_89_2)) & $lesseq(0, % 20.43/3.71 | $sum($difference(all_86_1, all_93_1), all_86_3)) & $lesseq(all_86_3, % 20.43/3.71 | all_93_1) & sum(all_86_4, all_93_1, $sum(all_86_1, all_86_3)) = % 20.43/3.71 | all_93_0 % 20.43/3.71 | % 20.43/3.71 | ALPHA: (6) implies: % 20.43/3.71 | (7) $lesseq(all_86_3, all_93_1) % 20.43/3.71 | (8) $lesseq(0, $sum($difference(all_86_1, all_93_1), all_86_3)) % 20.43/3.71 | (9) $lesseq(1, $difference(all_93_0, all_89_2)) % 20.43/3.71 | (10) sum(all_86_4, all_93_1, $sum(all_86_1, all_86_3)) = all_93_0 % 20.43/3.71 | % 20.43/3.72 | GROUND_INST: instantiating (4) with all_93_1, all_93_0, simplifying with (10) % 20.43/3.72 | gives: % 20.43/3.72 | (11) ~ ($lesseq(1, $difference(all_93_0, all_89_2))) | ~ ($lesseq(0, % 20.43/3.72 | $sum($difference(all_86_1, all_93_1), all_86_3))) | ~ % 20.43/3.72 | ($lesseq(all_86_3, all_93_1)) % 20.43/3.72 | % 20.43/3.72 | BETA: splitting (11) gives: % 20.43/3.72 | % 20.43/3.72 | Case 1: % 20.43/3.72 | | % 20.43/3.72 | | (12) $lesseq(1, $difference(all_86_3, all_93_1)) % 20.43/3.72 | | % 20.43/3.72 | | COMBINE_INEQS: (7), (12) imply: % 20.43/3.72 | | (13) $false % 20.43/3.72 | | % 20.43/3.72 | | CLOSE: (13) is inconsistent. % 20.43/3.72 | | % 20.43/3.72 | Case 2: % 20.43/3.72 | | % 20.43/3.72 | | (14) ~ ($lesseq(1, $difference(all_93_0, all_89_2))) | ~ ($lesseq(0, % 20.43/3.72 | | $sum($difference(all_86_1, all_93_1), all_86_3))) % 20.43/3.72 | | % 20.43/3.72 | | BETA: splitting (14) gives: % 20.43/3.72 | | % 20.43/3.72 | | Case 1: % 20.43/3.72 | | | % 20.43/3.72 | | | (15) $lesseq(all_93_0, all_89_2) % 20.43/3.72 | | | % 20.43/3.72 | | | COMBINE_INEQS: (9), (15) imply: % 20.43/3.72 | | | (16) $false % 20.43/3.72 | | | % 20.43/3.72 | | | CLOSE: (16) is inconsistent. % 20.43/3.72 | | | % 20.43/3.72 | | Case 2: % 20.43/3.72 | | | % 20.43/3.72 | | | (17) $lesseq(1, $difference($difference(all_93_1, all_86_1), all_86_3)) % 20.43/3.72 | | | % 20.43/3.72 | | | COMBINE_INEQS: (8), (17) imply: % 20.43/3.72 | | | (18) $false % 20.43/3.72 | | | % 20.43/3.72 | | | CLOSE: (18) is inconsistent. % 20.43/3.72 | | | % 20.43/3.72 | | End of split % 20.43/3.72 | | % 20.43/3.72 | End of split % 20.43/3.72 | % 20.43/3.72 End of proof % 20.43/3.72 % SZS output end Proof for theBenchmark % 20.43/3.72 % 20.43/3.72 3104ms %------------------------------------------------------------------------------