%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR036+1 : TPTP v8.1.2. Released v3.4.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n007.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 21:36:37 EDT 2023 % Result : Theorem 33.41s 5.04s % Output : Proof 55.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : CSR036+1 : TPTP v8.1.2. Released v3.4.0. % 0.06/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.11/0.33 % Computer : n007.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Mon Aug 28 13:04:57 EDT 2023 % 0.11/0.33 % CPUTime : % 0.18/0.59 ________ _____ % 0.18/0.59 ___ __ \_________(_)________________________________ % 0.18/0.59 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.18/0.59 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.18/0.59 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.18/0.59 % 0.18/0.59 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.18/0.59 (2023-06-19) % 0.18/0.59 % 0.18/0.59 (c) Philipp Rümmer, 2009-2023 % 0.18/0.59 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.18/0.59 Amanda Stjerna. % 0.18/0.59 Free software under BSD-3-Clause. % 0.18/0.59 % 0.18/0.59 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.18/0.59 % 0.18/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.18/0.61 Running up to 7 provers in parallel. % 0.18/0.62 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.18/0.62 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.18/0.62 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.18/0.62 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.18/0.62 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.18/0.62 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.18/0.62 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.75/1.23 Prover 1: Preprocessing ... % 3.75/1.23 Prover 4: Preprocessing ... % 3.75/1.27 Prover 2: Preprocessing ... % 3.75/1.27 Prover 5: Preprocessing ... % 3.75/1.27 Prover 0: Preprocessing ... % 3.75/1.27 Prover 3: Preprocessing ... % 3.75/1.28 Prover 6: Preprocessing ... % 7.91/1.78 Prover 5: Constructing countermodel ... % 7.91/1.78 Prover 2: Constructing countermodel ... % 10.13/2.02 Prover 6: Constructing countermodel ... % 10.62/2.12 Prover 1: Constructing countermodel ... % 10.62/2.13 Prover 3: Constructing countermodel ... % 12.45/2.33 Prover 4: Constructing countermodel ... % 12.45/2.36 Prover 0: Proving ... % 21.06/3.43 Prover 3: gave up % 21.06/3.43 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 21.06/3.50 Prover 7: Preprocessing ... % 21.06/3.51 Prover 1: gave up % 21.80/3.52 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 22.47/3.60 Prover 8: Preprocessing ... % 22.47/3.63 Prover 7: Constructing countermodel ... % 24.14/3.88 Prover 8: Warning: ignoring some quantifiers % 24.14/3.90 Prover 8: Constructing countermodel ... % 33.41/5.04 Prover 0: proved (4410ms) % 33.41/5.04 % 33.41/5.04 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.41/5.04 % 33.41/5.04 Prover 2: stopped % 33.41/5.04 Prover 5: stopped % 33.41/5.06 Prover 6: stopped % 33.41/5.06 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 33.41/5.06 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 33.41/5.06 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 33.41/5.06 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 34.25/5.11 Prover 8: gave up % 34.46/5.13 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 34.46/5.16 Prover 10: Preprocessing ... % 34.46/5.16 Prover 11: Preprocessing ... % 34.46/5.17 Prover 13: Preprocessing ... % 34.46/5.19 Prover 16: Preprocessing ... % 34.46/5.22 Prover 19: Preprocessing ... % 35.21/5.26 Prover 10: Constructing countermodel ... % 35.21/5.28 Prover 16: Constructing countermodel ... % 35.21/5.28 Prover 13: Constructing countermodel ... % 36.80/5.44 Prover 19: Warning: ignoring some quantifiers % 36.80/5.45 Prover 19: Constructing countermodel ... % 36.80/5.47 Prover 11: Constructing countermodel ... % 53.11/7.49 Prover 19: gave up % 55.40/7.82 Prover 10: Found proof (size 61) % 55.40/7.82 Prover 10: proved (2774ms) % 55.40/7.82 Prover 13: stopped % 55.40/7.82 Prover 11: stopped % 55.40/7.82 Prover 16: stopped % 55.40/7.82 Prover 7: stopped % 55.40/7.82 Prover 4: stopped % 55.40/7.82 % 55.40/7.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 55.40/7.82 % 55.40/7.83 % SZS output start Proof for theBenchmark % 55.40/7.84 Assumptions after simplification: % 55.40/7.84 --------------------------------- % 55.40/7.84 % 55.40/7.84 (just10) % 55.40/7.84 $i(c_tptpcol_4_16387) & $i(c_tptpcol_3_16386) & genls(c_tptpcol_4_16387, % 55.40/7.84 c_tptpcol_3_16386) % 55.40/7.84 % 55.40/7.84 (just12) % 55.40/7.84 $i(c_tptpcol_5_20483) & $i(c_tptpcol_4_16387) & genls(c_tptpcol_5_20483, % 55.40/7.84 c_tptpcol_4_16387) % 55.40/7.84 % 55.40/7.84 (just14) % 55.40/7.84 $i(c_tptpcol_6_20484) & $i(c_tptpcol_5_20483) & genls(c_tptpcol_6_20484, % 55.40/7.84 c_tptpcol_5_20483) % 55.40/7.84 % 55.40/7.84 (just155) % 55.40/7.84 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 55.40/7.84 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 55.40/7.84 % 55.40/7.84 (just16) % 55.40/7.84 $i(c_tptpcol_7_21508) & $i(c_tptpcol_6_20484) & genls(c_tptpcol_7_21508, % 55.40/7.84 c_tptpcol_6_20484) % 55.40/7.84 % 55.40/7.84 (just18) % 55.40/7.84 $i(c_tptpcol_8_22020) & $i(c_tptpcol_7_21508) & genls(c_tptpcol_8_22020, % 55.40/7.84 c_tptpcol_7_21508) % 55.40/7.84 % 55.40/7.84 (just20) % 55.40/7.84 $i(c_tptpcol_9_22021) & $i(c_tptpcol_8_22020) & genls(c_tptpcol_9_22021, % 55.40/7.84 c_tptpcol_8_22020) % 55.40/7.84 % 55.40/7.84 (just22) % 55.40/7.84 $i(c_tptpcol_10_22022) & $i(c_tptpcol_9_22021) & genls(c_tptpcol_10_22022, % 55.40/7.84 c_tptpcol_9_22021) % 55.40/7.84 % 55.40/7.84 (just24) % 55.40/7.85 $i(c_tptpcol_11_22023) & $i(c_tptpcol_10_22022) & genls(c_tptpcol_11_22023, % 55.40/7.85 c_tptpcol_10_22022) % 55.40/7.85 % 55.40/7.85 (just26) % 55.40/7.85 $i(c_tptpcol_12_22055) & $i(c_tptpcol_11_22023) & genls(c_tptpcol_12_22055, % 55.40/7.85 c_tptpcol_11_22023) % 55.40/7.85 % 55.40/7.85 (just28) % 55.40/7.85 $i(c_tptpcol_13_22071) & $i(c_tptpcol_12_22055) & genls(c_tptpcol_13_22071, % 55.40/7.85 c_tptpcol_12_22055) % 55.40/7.85 % 55.40/7.85 (just30) % 55.40/7.85 $i(c_tptpcol_14_22072) & $i(c_tptpcol_13_22071) & genls(c_tptpcol_14_22072, % 55.40/7.85 c_tptpcol_13_22071) % 55.40/7.85 % 55.40/7.85 (just32) % 55.40/7.85 $i(c_tptpcol_15_22076) & $i(c_tptpcol_14_22072) & genls(c_tptpcol_15_22076, % 55.40/7.85 c_tptpcol_14_22072) % 55.40/7.85 % 55.40/7.85 (just34) % 55.40/7.85 $i(c_tptpcol_1_65536) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_2_65537, % 55.40/7.85 c_tptpcol_1_65536) % 55.40/7.85 % 55.40/7.85 (just36) % 55.40/7.85 $i(c_tptpcol_3_65538) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_3_65538, % 55.40/7.85 c_tptpcol_2_65537) % 55.40/7.85 % 55.40/7.85 (just38) % 55.40/7.85 $i(c_tptpcol_4_65539) & $i(c_tptpcol_3_65538) & genls(c_tptpcol_4_65539, % 55.40/7.85 c_tptpcol_3_65538) % 55.40/7.85 % 55.40/7.85 (just40) % 55.40/7.85 $i(c_tptpcol_5_69635) & $i(c_tptpcol_4_65539) & genls(c_tptpcol_5_69635, % 55.40/7.85 c_tptpcol_4_65539) % 55.40/7.85 % 55.40/7.85 (just42) % 55.40/7.85 $i(c_tptpcol_6_71683) & $i(c_tptpcol_5_69635) & genls(c_tptpcol_6_71683, % 55.40/7.85 c_tptpcol_5_69635) % 55.40/7.85 % 55.40/7.85 (just44) % 55.40/7.85 $i(c_tptpcol_7_72707) & $i(c_tptpcol_6_71683) & genls(c_tptpcol_7_72707, % 55.40/7.85 c_tptpcol_6_71683) % 55.40/7.85 % 55.40/7.85 (just46) % 55.40/7.85 $i(c_tptpcol_8_72708) & $i(c_tptpcol_7_72707) & genls(c_tptpcol_8_72708, % 55.40/7.85 c_tptpcol_7_72707) % 55.40/7.85 % 55.40/7.85 (just48) % 55.40/7.85 $i(c_tptpcol_9_72709) & $i(c_tptpcol_8_72708) & genls(c_tptpcol_9_72709, % 55.40/7.85 c_tptpcol_8_72708) % 55.40/7.85 % 55.40/7.85 (just50) % 55.40/7.85 $i(c_tptpcol_10_72710) & $i(c_tptpcol_9_72709) & genls(c_tptpcol_10_72710, % 55.40/7.85 c_tptpcol_9_72709) % 55.40/7.85 % 55.40/7.85 (just52) % 55.40/7.85 $i(c_tptpcol_11_72774) & $i(c_tptpcol_10_72710) & genls(c_tptpcol_11_72774, % 55.40/7.85 c_tptpcol_10_72710) % 55.40/7.85 % 55.40/7.85 (just54) % 55.40/7.85 $i(c_tptpcol_12_72775) & $i(c_tptpcol_11_72774) & genls(c_tptpcol_12_72775, % 55.40/7.85 c_tptpcol_11_72774) % 55.40/7.85 % 55.40/7.85 (just56) % 55.40/7.85 $i(c_tptpcol_13_72791) & $i(c_tptpcol_12_72775) & genls(c_tptpcol_13_72791, % 55.40/7.85 c_tptpcol_12_72775) % 55.40/7.85 % 55.40/7.85 (just58) % 55.40/7.85 $i(c_tptpcol_14_72792) & $i(c_tptpcol_13_72791) & genls(c_tptpcol_14_72792, % 55.40/7.85 c_tptpcol_13_72791) % 55.40/7.85 % 55.40/7.85 (just6) % 55.40/7.85 $i(c_tptpcol_1_1) & $i(c_tptpcol_2_2) & genls(c_tptpcol_2_2, c_tptpcol_1_1) % 55.40/7.85 % 55.40/7.85 (just60) % 55.40/7.85 $i(c_tptpcol_15_72793) & $i(c_tptpcol_14_72792) & genls(c_tptpcol_15_72793, % 55.40/7.85 c_tptpcol_14_72792) % 55.40/7.85 % 55.40/7.85 (just62) % 55.40/7.85 $i(c_tptpcol_16_72795) & $i(c_tptpcol_15_72793) & genls(c_tptpcol_16_72795, % 55.40/7.85 c_tptpcol_15_72793) % 55.40/7.85 % 55.40/7.85 (just64) % 55.40/7.85 $i(c_tptpcol_1_65536) & $i(c_tptpcol_1_1) & disjointwith(c_tptpcol_1_1, % 55.40/7.85 c_tptpcol_1_65536) % 55.40/7.85 % 55.40/7.85 (just8) % 55.40/7.85 $i(c_tptpcol_3_16386) & $i(c_tptpcol_2_2) & genls(c_tptpcol_3_16386, % 55.40/7.85 c_tptpcol_2_2) % 55.40/7.85 % 55.40/7.85 (just84) % 55.40/7.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 55.40/7.85 ~ disjointwith(v0, v1) | ~ genls(v2, v1) | disjointwith(v0, v2)) % 55.40/7.85 % 55.40/7.85 (just85) % 55.40/7.85 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 55.40/7.85 ~ disjointwith(v0, v1) | ~ genls(v2, v0) | disjointwith(v2, v1)) % 55.40/7.85 % 55.40/7.85 (query36) % 55.40/7.86 $i(c_tptp_member974_mt) & $i(c_tptpcol_16_72795) & $i(c_tptpcol_15_22076) & % 55.40/7.86 mtvisible(c_tptp_member974_mt) & ~ disjointwith(c_tptpcol_15_22076, % 55.40/7.86 c_tptpcol_16_72795) % 55.40/7.86 % 55.40/7.86 Further assumptions not needed in the proof: % 55.40/7.86 -------------------------------------------- % 55.40/7.86 just1, just100, just101, just102, just103, just104, just105, just106, just107, % 55.40/7.86 just108, just109, just11, just110, just111, just112, just113, just114, just115, % 55.40/7.86 just116, just117, just118, just119, just120, just121, just122, just123, just124, % 55.40/7.86 just125, just126, just127, just128, just129, just13, just130, just131, just132, % 55.40/7.86 just133, just134, just135, just136, just137, just138, just139, just140, just141, % 55.40/7.86 just142, just143, just144, just145, just146, just147, just148, just149, just15, % 55.40/7.86 just150, just151, just152, just153, just154, just156, just157, just158, just159, % 55.40/7.86 just160, just161, just162, just163, just164, just165, just166, just167, just168, % 55.40/7.86 just169, just17, just170, just171, just172, just173, just19, just2, just21, % 55.40/7.86 just23, just25, just27, just29, just3, just31, just33, just35, just37, just39, % 55.40/7.86 just4, just41, just43, just45, just47, just49, just5, just51, just53, just55, % 55.40/7.86 just57, just59, just61, just63, just65, just66, just67, just68, just69, just7, % 55.40/7.86 just70, just71, just72, just73, just74, just75, just76, just77, just78, just79, % 55.40/7.86 just80, just81, just82, just83, just86, just87, just88, just89, just9, just90, % 55.40/7.86 just91, just92, just93, just94, just95, just96, just97, just98, just99 % 55.40/7.86 % 55.40/7.86 Those formulas are unsatisfiable: % 55.40/7.86 --------------------------------- % 55.40/7.86 % 55.40/7.86 Begin of proof % 55.40/7.86 | % 55.40/7.86 | ALPHA: (query36) implies: % 55.40/7.86 | (1) ~ disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just64) implies: % 55.40/7.86 | (2) disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just62) implies: % 55.40/7.86 | (3) genls(c_tptpcol_16_72795, c_tptpcol_15_72793) % 55.40/7.86 | (4) $i(c_tptpcol_16_72795) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just60) implies: % 55.40/7.86 | (5) genls(c_tptpcol_15_72793, c_tptpcol_14_72792) % 55.40/7.86 | (6) $i(c_tptpcol_15_72793) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just58) implies: % 55.40/7.86 | (7) genls(c_tptpcol_14_72792, c_tptpcol_13_72791) % 55.40/7.86 | (8) $i(c_tptpcol_14_72792) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just56) implies: % 55.40/7.86 | (9) genls(c_tptpcol_13_72791, c_tptpcol_12_72775) % 55.40/7.86 | (10) $i(c_tptpcol_13_72791) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just54) implies: % 55.40/7.86 | (11) genls(c_tptpcol_12_72775, c_tptpcol_11_72774) % 55.40/7.86 | (12) $i(c_tptpcol_12_72775) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just52) implies: % 55.40/7.86 | (13) genls(c_tptpcol_11_72774, c_tptpcol_10_72710) % 55.40/7.86 | (14) $i(c_tptpcol_11_72774) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just50) implies: % 55.40/7.86 | (15) genls(c_tptpcol_10_72710, c_tptpcol_9_72709) % 55.40/7.86 | (16) $i(c_tptpcol_10_72710) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just48) implies: % 55.40/7.86 | (17) genls(c_tptpcol_9_72709, c_tptpcol_8_72708) % 55.40/7.86 | (18) $i(c_tptpcol_9_72709) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just46) implies: % 55.40/7.86 | (19) genls(c_tptpcol_8_72708, c_tptpcol_7_72707) % 55.40/7.86 | (20) $i(c_tptpcol_8_72708) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just44) implies: % 55.40/7.86 | (21) genls(c_tptpcol_7_72707, c_tptpcol_6_71683) % 55.40/7.86 | (22) $i(c_tptpcol_7_72707) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just42) implies: % 55.40/7.86 | (23) genls(c_tptpcol_6_71683, c_tptpcol_5_69635) % 55.40/7.86 | (24) $i(c_tptpcol_6_71683) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just40) implies: % 55.40/7.86 | (25) genls(c_tptpcol_5_69635, c_tptpcol_4_65539) % 55.40/7.86 | (26) $i(c_tptpcol_5_69635) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just38) implies: % 55.40/7.86 | (27) genls(c_tptpcol_4_65539, c_tptpcol_3_65538) % 55.40/7.86 | (28) $i(c_tptpcol_4_65539) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just36) implies: % 55.40/7.86 | (29) genls(c_tptpcol_3_65538, c_tptpcol_2_65537) % 55.40/7.86 | (30) $i(c_tptpcol_3_65538) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just34) implies: % 55.40/7.86 | (31) genls(c_tptpcol_2_65537, c_tptpcol_1_65536) % 55.40/7.86 | (32) $i(c_tptpcol_2_65537) % 55.40/7.86 | (33) $i(c_tptpcol_1_65536) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just32) implies: % 55.40/7.86 | (34) genls(c_tptpcol_15_22076, c_tptpcol_14_22072) % 55.40/7.86 | (35) $i(c_tptpcol_15_22076) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just30) implies: % 55.40/7.86 | (36) genls(c_tptpcol_14_22072, c_tptpcol_13_22071) % 55.40/7.86 | (37) $i(c_tptpcol_14_22072) % 55.40/7.86 | % 55.40/7.86 | ALPHA: (just28) implies: % 55.40/7.86 | (38) genls(c_tptpcol_13_22071, c_tptpcol_12_22055) % 55.40/7.87 | (39) $i(c_tptpcol_13_22071) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just26) implies: % 55.40/7.87 | (40) genls(c_tptpcol_12_22055, c_tptpcol_11_22023) % 55.40/7.87 | (41) $i(c_tptpcol_12_22055) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just24) implies: % 55.40/7.87 | (42) genls(c_tptpcol_11_22023, c_tptpcol_10_22022) % 55.40/7.87 | (43) $i(c_tptpcol_11_22023) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just22) implies: % 55.40/7.87 | (44) genls(c_tptpcol_10_22022, c_tptpcol_9_22021) % 55.40/7.87 | (45) $i(c_tptpcol_10_22022) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just20) implies: % 55.40/7.87 | (46) genls(c_tptpcol_9_22021, c_tptpcol_8_22020) % 55.40/7.87 | (47) $i(c_tptpcol_9_22021) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just18) implies: % 55.40/7.87 | (48) genls(c_tptpcol_8_22020, c_tptpcol_7_21508) % 55.40/7.87 | (49) $i(c_tptpcol_8_22020) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just16) implies: % 55.40/7.87 | (50) genls(c_tptpcol_7_21508, c_tptpcol_6_20484) % 55.40/7.87 | (51) $i(c_tptpcol_7_21508) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just14) implies: % 55.40/7.87 | (52) genls(c_tptpcol_6_20484, c_tptpcol_5_20483) % 55.40/7.87 | (53) $i(c_tptpcol_6_20484) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just12) implies: % 55.40/7.87 | (54) genls(c_tptpcol_5_20483, c_tptpcol_4_16387) % 55.40/7.87 | (55) $i(c_tptpcol_5_20483) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just10) implies: % 55.40/7.87 | (56) genls(c_tptpcol_4_16387, c_tptpcol_3_16386) % 55.40/7.87 | (57) $i(c_tptpcol_4_16387) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just8) implies: % 55.40/7.87 | (58) genls(c_tptpcol_3_16386, c_tptpcol_2_2) % 55.40/7.87 | (59) $i(c_tptpcol_3_16386) % 55.40/7.87 | % 55.40/7.87 | ALPHA: (just6) implies: % 55.40/7.87 | (60) genls(c_tptpcol_2_2, c_tptpcol_1_1) % 55.40/7.87 | (61) $i(c_tptpcol_2_2) % 55.40/7.87 | (62) $i(c_tptpcol_1_1) % 55.40/7.87 | % 55.40/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_3_16386, c_tptpcol_2_2, % 55.40/7.87 | c_tptpcol_4_16387, simplifying with (56), (57), (58), (59), (61) % 55.40/7.87 | gives: % 55.40/7.87 | (63) genls(c_tptpcol_4_16387, c_tptpcol_2_2) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_5_20483, % 55.99/7.87 | c_tptpcol_4_16387, c_tptpcol_6_20484, simplifying with (52), % 55.99/7.87 | (53), (54), (55), (57) gives: % 55.99/7.87 | (64) genls(c_tptpcol_6_20484, c_tptpcol_4_16387) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_7_21508, % 55.99/7.87 | c_tptpcol_6_20484, c_tptpcol_8_22020, simplifying with (48), % 55.99/7.87 | (49), (50), (51), (53) gives: % 55.99/7.87 | (65) genls(c_tptpcol_8_22020, c_tptpcol_6_20484) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_9_22021, % 55.99/7.87 | c_tptpcol_8_22020, c_tptpcol_10_22022, simplifying with (44), % 55.99/7.87 | (45), (46), (47), (49) gives: % 55.99/7.87 | (66) genls(c_tptpcol_10_22022, c_tptpcol_8_22020) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_11_22023, % 55.99/7.87 | c_tptpcol_10_22022, c_tptpcol_12_22055, simplifying with (40), % 55.99/7.87 | (41), (42), (43), (45) gives: % 55.99/7.87 | (67) genls(c_tptpcol_12_22055, c_tptpcol_10_22022) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_14_22072, % 55.99/7.87 | c_tptpcol_13_22071, c_tptpcol_15_22076, simplifying with (34), % 55.99/7.87 | (35), (36), (37), (39) gives: % 55.99/7.87 | (68) genls(c_tptpcol_15_22076, c_tptpcol_13_22071) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_2_65537, % 55.99/7.87 | c_tptpcol_1_65536, c_tptpcol_3_65538, simplifying with (29), % 55.99/7.87 | (30), (31), (32), (33) gives: % 55.99/7.87 | (69) genls(c_tptpcol_3_65538, c_tptpcol_1_65536) % 55.99/7.87 | % 55.99/7.87 | GROUND_INST: instantiating (just155) with c_tptpcol_4_65539, % 55.99/7.87 | c_tptpcol_3_65538, c_tptpcol_5_69635, simplifying with (25), % 55.99/7.87 | (26), (27), (28), (30) gives: % 55.99/7.88 | (70) genls(c_tptpcol_5_69635, c_tptpcol_3_65538) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_6_71683, % 55.99/7.88 | c_tptpcol_5_69635, c_tptpcol_7_72707, simplifying with (21), % 55.99/7.88 | (22), (23), (24), (26) gives: % 55.99/7.88 | (71) genls(c_tptpcol_7_72707, c_tptpcol_5_69635) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_8_72708, % 55.99/7.88 | c_tptpcol_7_72707, c_tptpcol_9_72709, simplifying with (17), % 55.99/7.88 | (18), (19), (20), (22) gives: % 55.99/7.88 | (72) genls(c_tptpcol_9_72709, c_tptpcol_7_72707) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_10_72710, % 55.99/7.88 | c_tptpcol_9_72709, c_tptpcol_11_72774, simplifying with (13), % 55.99/7.88 | (14), (15), (16), (18) gives: % 55.99/7.88 | (73) genls(c_tptpcol_11_72774, c_tptpcol_9_72709) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_12_72775, % 55.99/7.88 | c_tptpcol_11_72774, c_tptpcol_13_72791, simplifying with (9), % 55.99/7.88 | (10), (11), (12), (14) gives: % 55.99/7.88 | (74) genls(c_tptpcol_13_72791, c_tptpcol_11_72774) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_15_72793, % 55.99/7.88 | c_tptpcol_14_72792, c_tptpcol_16_72795, simplifying with (3), % 55.99/7.88 | (4), (5), (6), (8) gives: % 55.99/7.88 | (75) genls(c_tptpcol_16_72795, c_tptpcol_14_72792) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just85) with c_tptpcol_1_1, c_tptpcol_1_65536, % 55.99/7.88 | c_tptpcol_2_2, simplifying with (2), (33), (60), (61), (62) % 55.99/7.88 | gives: % 55.99/7.88 | (76) disjointwith(c_tptpcol_2_2, c_tptpcol_1_65536) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_6_20484, % 55.99/7.88 | c_tptpcol_4_16387, c_tptpcol_8_22020, simplifying with (49), % 55.99/7.88 | (53), (57), (64), (65) gives: % 55.99/7.88 | (77) genls(c_tptpcol_8_22020, c_tptpcol_4_16387) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_10_22022, % 55.99/7.88 | c_tptpcol_8_22020, c_tptpcol_12_22055, simplifying with (41), % 55.99/7.88 | (45), (49), (66), (67) gives: % 55.99/7.88 | (78) genls(c_tptpcol_12_22055, c_tptpcol_8_22020) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_13_22071, % 55.99/7.88 | c_tptpcol_12_22055, c_tptpcol_15_22076, simplifying with (35), % 55.99/7.88 | (38), (39), (41), (68) gives: % 55.99/7.88 | (79) genls(c_tptpcol_15_22076, c_tptpcol_12_22055) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_3_65538, % 55.99/7.88 | c_tptpcol_1_65536, c_tptpcol_5_69635, simplifying with (26), % 55.99/7.88 | (30), (33), (69), (70) gives: % 55.99/7.88 | (80) genls(c_tptpcol_5_69635, c_tptpcol_1_65536) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_7_72707, % 55.99/7.88 | c_tptpcol_5_69635, c_tptpcol_9_72709, simplifying with (18), % 55.99/7.88 | (22), (26), (71), (72) gives: % 55.99/7.88 | (81) genls(c_tptpcol_9_72709, c_tptpcol_5_69635) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_11_72774, % 55.99/7.88 | c_tptpcol_9_72709, c_tptpcol_13_72791, simplifying with (10), % 55.99/7.88 | (14), (18), (73), (74) gives: % 55.99/7.88 | (82) genls(c_tptpcol_13_72791, c_tptpcol_9_72709) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_14_72792, % 55.99/7.88 | c_tptpcol_13_72791, c_tptpcol_16_72795, simplifying with (4), % 55.99/7.88 | (7), (8), (10), (75) gives: % 55.99/7.88 | (83) genls(c_tptpcol_16_72795, c_tptpcol_13_72791) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just85) with c_tptpcol_2_2, c_tptpcol_1_65536, % 55.99/7.88 | c_tptpcol_4_16387, simplifying with (33), (57), (61), (63), (76) % 55.99/7.88 | gives: % 55.99/7.88 | (84) disjointwith(c_tptpcol_4_16387, c_tptpcol_1_65536) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_12_22055, % 55.99/7.88 | c_tptpcol_8_22020, c_tptpcol_15_22076, simplifying with (35), % 55.99/7.88 | (41), (49), (78), (79) gives: % 55.99/7.88 | (85) genls(c_tptpcol_15_22076, c_tptpcol_8_22020) % 55.99/7.88 | % 55.99/7.88 | GROUND_INST: instantiating (just155) with c_tptpcol_5_69635, % 55.99/7.88 | c_tptpcol_1_65536, c_tptpcol_9_72709, simplifying with (18), % 55.99/7.88 | (26), (33), (80), (81) gives: % 55.99/7.88 | (86) genls(c_tptpcol_9_72709, c_tptpcol_1_65536) % 55.99/7.88 | % 55.99/7.89 | GROUND_INST: instantiating (just155) with c_tptpcol_13_72791, % 55.99/7.89 | c_tptpcol_9_72709, c_tptpcol_16_72795, simplifying with (4), % 55.99/7.89 | (10), (18), (82), (83) gives: % 55.99/7.89 | (87) genls(c_tptpcol_16_72795, c_tptpcol_9_72709) % 55.99/7.89 | % 55.99/7.89 | GROUND_INST: instantiating (just85) with c_tptpcol_4_16387, c_tptpcol_1_65536, % 55.99/7.89 | c_tptpcol_8_22020, simplifying with (33), (49), (57), (77), (84) % 55.99/7.89 | gives: % 55.99/7.89 | (88) disjointwith(c_tptpcol_8_22020, c_tptpcol_1_65536) % 55.99/7.89 | % 55.99/7.89 | GROUND_INST: instantiating (just155) with c_tptpcol_9_72709, % 55.99/7.89 | c_tptpcol_1_65536, c_tptpcol_16_72795, simplifying with (4), % 55.99/7.89 | (18), (33), (86), (87) gives: % 55.99/7.89 | (89) genls(c_tptpcol_16_72795, c_tptpcol_1_65536) % 55.99/7.89 | % 55.99/7.89 | GROUND_INST: instantiating (just85) with c_tptpcol_8_22020, c_tptpcol_1_65536, % 55.99/7.89 | c_tptpcol_15_22076, simplifying with (33), (35), (49), (85), (88) % 55.99/7.89 | gives: % 55.99/7.89 | (90) disjointwith(c_tptpcol_15_22076, c_tptpcol_1_65536) % 55.99/7.89 | % 55.99/7.89 | GROUND_INST: instantiating (just84) with c_tptpcol_15_22076, % 55.99/7.89 | c_tptpcol_1_65536, c_tptpcol_16_72795, simplifying with (1), (4), % 55.99/7.89 | (33), (35), (89), (90) gives: % 55.99/7.89 | (91) $false % 55.99/7.89 | % 55.99/7.89 | CLOSE: (91) is inconsistent. % 55.99/7.89 | % 55.99/7.89 End of proof % 55.99/7.89 % SZS output end Proof for theBenchmark % 55.99/7.89 % 55.99/7.89 7295ms %------------------------------------------------------------------------------