%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR049+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 : n001.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:49 EDT 2023 % Result : Theorem 38.10s 5.96s % Output : Proof 62.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : CSR049+1 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.35 % Computer : n001.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Mon Aug 28 09:59:35 EDT 2023 % 0.21/0.36 % CPUTime : % 0.21/0.63 ________ _____ % 0.21/0.63 ___ __ \_________(_)________________________________ % 0.21/0.63 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.63 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.63 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.63 % 0.21/0.63 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.63 (2023-06-19) % 0.21/0.63 % 0.21/0.63 (c) Philipp Rümmer, 2009-2023 % 0.21/0.63 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.63 Amanda Stjerna. % 0.21/0.63 Free software under BSD-3-Clause. % 0.21/0.63 % 0.21/0.63 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.63 % 0.21/0.63 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.64 Running up to 7 provers in parallel. % 0.21/0.66 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.66 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.66 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.66 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.66 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.21/0.66 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.66 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 4.03/1.30 Prover 4: Preprocessing ... % 4.03/1.30 Prover 1: Preprocessing ... % 4.46/1.34 Prover 0: Preprocessing ... % 4.46/1.34 Prover 2: Preprocessing ... % 4.46/1.34 Prover 6: Preprocessing ... % 4.46/1.34 Prover 3: Preprocessing ... % 4.46/1.34 Prover 5: Preprocessing ... % 7.86/1.86 Prover 5: Constructing countermodel ... % 7.86/1.89 Prover 2: Constructing countermodel ... % 11.17/2.35 Prover 6: Constructing countermodel ... % 11.88/2.38 Prover 3: Constructing countermodel ... % 12.06/2.40 Prover 1: Constructing countermodel ... % 13.39/2.64 Prover 0: Proving ... % 13.39/2.65 Prover 4: Constructing countermodel ... % 22.59/3.83 Prover 3: gave up % 22.59/3.85 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 23.36/3.94 Prover 7: Preprocessing ... % 24.85/4.14 Prover 7: Constructing countermodel ... % 25.68/4.27 Prover 1: gave up % 25.68/4.27 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 26.44/4.37 Prover 8: Preprocessing ... % 28.88/4.70 Prover 8: Warning: ignoring some quantifiers % 29.36/4.71 Prover 8: Constructing countermodel ... % 38.10/5.94 Prover 8: gave up % 38.10/5.95 Prover 0: proved (5299ms) % 38.10/5.95 % 38.10/5.96 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.10/5.96 % 38.10/5.96 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 38.10/5.96 Prover 5: stopped % 38.10/5.96 Prover 2: stopped % 38.10/5.96 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 38.10/5.97 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 38.10/5.97 Prover 6: stopped % 38.10/5.98 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 38.10/5.99 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 38.10/6.07 Prover 9: Preprocessing ... % 39.34/6.09 Prover 11: Preprocessing ... % 39.34/6.10 Prover 13: Preprocessing ... % 39.34/6.12 Prover 10: Preprocessing ... % 39.34/6.13 Prover 16: Preprocessing ... % 40.29/6.23 Prover 13: Constructing countermodel ... % 40.29/6.23 Prover 10: Constructing countermodel ... % 41.12/6.28 Prover 16: Constructing countermodel ... % 41.96/6.42 Prover 11: Constructing countermodel ... % 42.98/6.52 Prover 9: Constructing countermodel ... % 43.41/6.55 Prover 9: stopped % 43.50/6.58 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 43.88/6.64 Prover 19: Preprocessing ... % 44.26/6.87 Prover 19: Warning: ignoring some quantifiers % 45.53/6.90 Prover 19: Constructing countermodel ... % 60.04/8.84 Prover 19: gave up % 60.92/8.97 Prover 10: Found proof (size 63) % 60.92/8.97 Prover 10: proved (3017ms) % 60.92/8.97 Prover 13: stopped % 60.92/8.98 Prover 16: stopped % 60.92/8.98 Prover 7: stopped % 60.92/8.98 Prover 11: stopped % 60.92/8.98 Prover 4: stopped % 60.92/8.98 % 60.92/8.98 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 60.92/8.98 % 60.92/8.99 % SZS output start Proof for theBenchmark % 60.92/8.99 Assumptions after simplification: % 60.92/8.99 --------------------------------- % 60.92/8.99 % 60.92/8.99 (just11) % 60.92/9.00 $i(c_tptpcol_4_24578) & $i(c_tptpcol_3_16386) & genls(c_tptpcol_4_24578, % 60.92/9.00 c_tptpcol_3_16386) % 60.92/9.00 % 60.92/9.00 (just13) % 60.92/9.00 $i(c_tptpcol_5_24579) & $i(c_tptpcol_4_24578) & genls(c_tptpcol_5_24579, % 60.92/9.00 c_tptpcol_4_24578) % 60.92/9.00 % 60.92/9.00 (just15) % 60.92/9.00 $i(c_tptpcol_6_26627) & $i(c_tptpcol_5_24579) & genls(c_tptpcol_6_26627, % 60.92/9.00 c_tptpcol_5_24579) % 60.92/9.00 % 60.92/9.00 (just158) % 60.92/9.00 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 60.92/9.00 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 60.92/9.00 % 60.92/9.00 (just17) % 60.92/9.00 $i(c_tptpcol_7_26628) & $i(c_tptpcol_6_26627) & genls(c_tptpcol_7_26628, % 60.92/9.00 c_tptpcol_6_26627) % 60.92/9.00 % 60.92/9.00 (just19) % 60.92/9.00 $i(c_tptpcol_8_26629) & $i(c_tptpcol_7_26628) & genls(c_tptpcol_8_26629, % 60.92/9.00 c_tptpcol_7_26628) % 60.92/9.00 % 60.92/9.00 (just21) % 61.90/9.00 $i(c_tptpcol_9_26885) & $i(c_tptpcol_8_26629) & genls(c_tptpcol_9_26885, % 61.90/9.00 c_tptpcol_8_26629) % 61.90/9.00 % 61.90/9.00 (just23) % 61.90/9.00 $i(c_tptpcol_10_26886) & $i(c_tptpcol_9_26885) & genls(c_tptpcol_10_26886, % 61.90/9.00 c_tptpcol_9_26885) % 61.90/9.00 % 61.90/9.00 (just25) % 61.90/9.00 $i(c_tptpcol_11_26887) & $i(c_tptpcol_10_26886) & genls(c_tptpcol_11_26887, % 61.90/9.00 c_tptpcol_10_26886) % 61.90/9.00 % 61.90/9.00 (just27) % 61.90/9.00 $i(c_tptpcol_12_26919) & $i(c_tptpcol_11_26887) & genls(c_tptpcol_12_26919, % 61.90/9.00 c_tptpcol_11_26887) % 61.90/9.00 % 61.90/9.00 (just29) % 61.90/9.00 $i(c_tptpcol_13_26920) & $i(c_tptpcol_12_26919) & genls(c_tptpcol_13_26920, % 61.90/9.00 c_tptpcol_12_26919) % 61.90/9.00 % 61.90/9.00 (just31) % 61.90/9.00 $i(c_tptpcol_14_26921) & $i(c_tptpcol_13_26920) & genls(c_tptpcol_14_26921, % 61.90/9.00 c_tptpcol_13_26920) % 61.90/9.00 % 61.90/9.00 (just33) % 61.90/9.00 $i(c_tptpcol_15_26925) & $i(c_tptpcol_14_26921) & genls(c_tptpcol_15_26925, % 61.90/9.00 c_tptpcol_14_26921) % 61.90/9.00 % 61.90/9.00 (just35) % 61.90/9.00 $i(c_tptpcol_16_26926) & $i(c_tptpcol_15_26925) & genls(c_tptpcol_16_26926, % 61.90/9.00 c_tptpcol_15_26925) % 61.90/9.00 % 61.90/9.00 (just37) % 61.90/9.00 $i(c_tptpcol_1_65536) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_2_65537, % 61.90/9.00 c_tptpcol_1_65536) % 61.90/9.00 % 61.90/9.00 (just39) % 61.90/9.00 $i(c_tptpcol_3_81921) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_3_81921, % 61.90/9.00 c_tptpcol_2_65537) % 61.90/9.00 % 61.90/9.00 (just41) % 61.90/9.00 $i(c_tptpcol_4_90113) & $i(c_tptpcol_3_81921) & genls(c_tptpcol_4_90113, % 61.90/9.00 c_tptpcol_3_81921) % 61.90/9.00 % 61.90/9.00 (just43) % 61.90/9.00 $i(c_tptpcol_5_90114) & $i(c_tptpcol_4_90113) & genls(c_tptpcol_5_90114, % 61.90/9.00 c_tptpcol_4_90113) % 61.90/9.00 % 61.90/9.00 (just45) % 61.90/9.00 $i(c_tptpcol_6_92162) & $i(c_tptpcol_5_90114) & genls(c_tptpcol_6_92162, % 61.90/9.00 c_tptpcol_5_90114) % 61.90/9.01 % 61.90/9.01 (just47) % 61.90/9.01 $i(c_tptpcol_7_92163) & $i(c_tptpcol_6_92162) & genls(c_tptpcol_7_92163, % 61.90/9.01 c_tptpcol_6_92162) % 61.90/9.01 % 61.90/9.01 (just49) % 61.90/9.01 $i(c_tptpcol_8_92164) & $i(c_tptpcol_7_92163) & genls(c_tptpcol_8_92164, % 61.90/9.01 c_tptpcol_7_92163) % 61.90/9.01 % 61.90/9.01 (just51) % 61.90/9.01 $i(c_tptpcol_9_92165) & $i(c_tptpcol_8_92164) & genls(c_tptpcol_9_92165, % 61.90/9.01 c_tptpcol_8_92164) % 61.90/9.01 % 61.90/9.01 (just53) % 61.90/9.01 $i(c_tptpcol_10_92166) & $i(c_tptpcol_9_92165) & genls(c_tptpcol_10_92166, % 61.90/9.01 c_tptpcol_9_92165) % 61.90/9.01 % 61.90/9.01 (just55) % 61.90/9.01 $i(c_tptpcol_11_92230) & $i(c_tptpcol_10_92166) & genls(c_tptpcol_11_92230, % 61.90/9.01 c_tptpcol_10_92166) % 61.90/9.01 % 61.90/9.01 (just57) % 61.90/9.01 $i(c_tptpcol_12_92262) & $i(c_tptpcol_11_92230) & genls(c_tptpcol_12_92262, % 61.90/9.01 c_tptpcol_11_92230) % 61.90/9.01 % 61.90/9.01 (just59) % 61.90/9.01 $i(c_tptpcol_13_92263) & $i(c_tptpcol_12_92262) & genls(c_tptpcol_13_92263, % 61.90/9.01 c_tptpcol_12_92262) % 61.90/9.01 % 61.90/9.01 (just61) % 61.90/9.01 $i(c_tptpcol_14_92264) & $i(c_tptpcol_13_92263) & genls(c_tptpcol_14_92264, % 61.90/9.01 c_tptpcol_13_92263) % 61.90/9.01 % 61.90/9.01 (just63) % 61.90/9.01 $i(c_tptpcol_15_92268) & $i(c_tptpcol_14_92264) & genls(c_tptpcol_15_92268, % 61.90/9.01 c_tptpcol_14_92264) % 61.90/9.01 % 61.90/9.01 (just65) % 61.90/9.01 $i(c_tptpcol_16_92269) & $i(c_tptpcol_15_92268) & genls(c_tptpcol_16_92269, % 61.90/9.01 c_tptpcol_15_92268) % 61.90/9.01 % 61.90/9.01 (just67) % 61.90/9.01 $i(c_tptpcol_1_65536) & $i(c_tptpcol_1_1) & disjointwith(c_tptpcol_1_1, % 61.90/9.01 c_tptpcol_1_65536) % 61.90/9.01 % 61.90/9.01 (just7) % 61.90/9.01 $i(c_tptpcol_1_1) & $i(c_tptpcol_2_2) & genls(c_tptpcol_2_2, c_tptpcol_1_1) % 61.90/9.01 % 61.90/9.01 (just85) % 61.90/9.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 61.90/9.01 ~ disjointwith(v0, v1) | ~ genls(v2, v1) | disjointwith(v0, v2)) % 61.90/9.01 % 61.90/9.01 (just86) % 61.90/9.01 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 61.90/9.01 ~ disjointwith(v0, v1) | ~ genls(v2, v0) | disjointwith(v2, v1)) % 61.90/9.01 % 61.90/9.01 (just9) % 61.90/9.01 $i(c_tptpcol_3_16386) & $i(c_tptpcol_2_2) & genls(c_tptpcol_3_16386, % 61.90/9.01 c_tptpcol_2_2) % 61.90/9.01 % 61.90/9.01 (query49) % 61.90/9.01 $i(c_tptpcol_16_92269) & $i(c_tptpcol_16_26926) & % 61.90/9.01 $i(c_unitedstatesgeographypeoplemt) & % 61.90/9.01 mtvisible(c_unitedstatesgeographypeoplemt) & ~ % 61.90/9.01 disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269) % 61.90/9.01 % 61.90/9.01 Further assumptions not needed in the proof: % 61.90/9.01 -------------------------------------------- % 61.90/9.01 just1, just10, just100, just101, just102, just103, just104, just105, just106, % 61.90/9.01 just107, just108, just109, just110, just111, just112, just113, just114, just115, % 61.90/9.01 just116, just117, just118, just119, just12, just120, just121, just122, just123, % 61.90/9.01 just124, just125, just126, just127, just128, just129, just130, just131, just132, % 61.90/9.01 just133, just134, just135, just136, just137, just138, just139, just14, just140, % 61.90/9.01 just141, just142, just143, just144, just145, just146, just147, just148, just149, % 61.90/9.01 just150, just151, just152, just153, just154, just155, just156, just157, just159, % 61.90/9.01 just16, just160, just161, just162, just163, just164, just165, just166, just167, % 61.90/9.01 just168, just169, just170, just171, just172, just173, just174, just175, just176, % 61.90/9.01 just18, just2, just20, just22, just24, just26, just28, just3, just30, just32, % 61.90/9.01 just34, just36, just38, just4, just40, just42, just44, just46, just48, just5, % 61.90/9.01 just50, just52, just54, just56, just58, just6, just60, just62, just64, just66, % 61.90/9.01 just68, just69, just70, just71, just72, just73, just74, just75, just76, just77, % 61.90/9.01 just78, just79, just8, just80, just81, just82, just83, just84, just87, just88, % 61.90/9.01 just89, just90, just91, just92, just93, just94, just95, just96, just97, just98, % 61.90/9.01 just99 % 61.90/9.01 % 61.90/9.01 Those formulas are unsatisfiable: % 61.90/9.01 --------------------------------- % 61.90/9.01 % 61.90/9.01 Begin of proof % 61.90/9.01 | % 61.90/9.01 | ALPHA: (query49) implies: % 61.90/9.01 | (1) ~ disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269) % 61.90/9.01 | % 61.90/9.01 | ALPHA: (just67) implies: % 61.90/9.01 | (2) disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536) % 61.90/9.01 | % 61.90/9.01 | ALPHA: (just65) implies: % 61.90/9.01 | (3) genls(c_tptpcol_16_92269, c_tptpcol_15_92268) % 61.90/9.01 | (4) $i(c_tptpcol_16_92269) % 61.90/9.01 | % 61.90/9.01 | ALPHA: (just63) implies: % 61.90/9.01 | (5) genls(c_tptpcol_15_92268, c_tptpcol_14_92264) % 61.90/9.01 | (6) $i(c_tptpcol_15_92268) % 61.90/9.01 | % 61.90/9.01 | ALPHA: (just61) implies: % 61.90/9.02 | (7) genls(c_tptpcol_14_92264, c_tptpcol_13_92263) % 61.90/9.02 | (8) $i(c_tptpcol_14_92264) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just59) implies: % 61.90/9.02 | (9) genls(c_tptpcol_13_92263, c_tptpcol_12_92262) % 61.90/9.02 | (10) $i(c_tptpcol_13_92263) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just57) implies: % 61.90/9.02 | (11) genls(c_tptpcol_12_92262, c_tptpcol_11_92230) % 61.90/9.02 | (12) $i(c_tptpcol_12_92262) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just55) implies: % 61.90/9.02 | (13) genls(c_tptpcol_11_92230, c_tptpcol_10_92166) % 61.90/9.02 | (14) $i(c_tptpcol_11_92230) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just53) implies: % 61.90/9.02 | (15) genls(c_tptpcol_10_92166, c_tptpcol_9_92165) % 61.90/9.02 | (16) $i(c_tptpcol_10_92166) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just51) implies: % 61.90/9.02 | (17) genls(c_tptpcol_9_92165, c_tptpcol_8_92164) % 61.90/9.02 | (18) $i(c_tptpcol_9_92165) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just49) implies: % 61.90/9.02 | (19) genls(c_tptpcol_8_92164, c_tptpcol_7_92163) % 61.90/9.02 | (20) $i(c_tptpcol_8_92164) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just47) implies: % 61.90/9.02 | (21) genls(c_tptpcol_7_92163, c_tptpcol_6_92162) % 61.90/9.02 | (22) $i(c_tptpcol_7_92163) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just45) implies: % 61.90/9.02 | (23) genls(c_tptpcol_6_92162, c_tptpcol_5_90114) % 61.90/9.02 | (24) $i(c_tptpcol_6_92162) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just43) implies: % 61.90/9.02 | (25) genls(c_tptpcol_5_90114, c_tptpcol_4_90113) % 61.90/9.02 | (26) $i(c_tptpcol_5_90114) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just41) implies: % 61.90/9.02 | (27) genls(c_tptpcol_4_90113, c_tptpcol_3_81921) % 61.90/9.02 | (28) $i(c_tptpcol_4_90113) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just39) implies: % 61.90/9.02 | (29) genls(c_tptpcol_3_81921, c_tptpcol_2_65537) % 61.90/9.02 | (30) $i(c_tptpcol_3_81921) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just37) implies: % 61.90/9.02 | (31) genls(c_tptpcol_2_65537, c_tptpcol_1_65536) % 61.90/9.02 | (32) $i(c_tptpcol_2_65537) % 61.90/9.02 | (33) $i(c_tptpcol_1_65536) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just35) implies: % 61.90/9.02 | (34) genls(c_tptpcol_16_26926, c_tptpcol_15_26925) % 61.90/9.02 | (35) $i(c_tptpcol_16_26926) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just33) implies: % 61.90/9.02 | (36) genls(c_tptpcol_15_26925, c_tptpcol_14_26921) % 61.90/9.02 | (37) $i(c_tptpcol_15_26925) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just31) implies: % 61.90/9.02 | (38) genls(c_tptpcol_14_26921, c_tptpcol_13_26920) % 61.90/9.02 | (39) $i(c_tptpcol_14_26921) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just29) implies: % 61.90/9.02 | (40) genls(c_tptpcol_13_26920, c_tptpcol_12_26919) % 61.90/9.02 | (41) $i(c_tptpcol_13_26920) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just27) implies: % 61.90/9.02 | (42) genls(c_tptpcol_12_26919, c_tptpcol_11_26887) % 61.90/9.02 | (43) $i(c_tptpcol_12_26919) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just25) implies: % 61.90/9.02 | (44) genls(c_tptpcol_11_26887, c_tptpcol_10_26886) % 61.90/9.02 | (45) $i(c_tptpcol_11_26887) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just23) implies: % 61.90/9.02 | (46) genls(c_tptpcol_10_26886, c_tptpcol_9_26885) % 61.90/9.02 | (47) $i(c_tptpcol_10_26886) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just21) implies: % 61.90/9.02 | (48) genls(c_tptpcol_9_26885, c_tptpcol_8_26629) % 61.90/9.02 | (49) $i(c_tptpcol_9_26885) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just19) implies: % 61.90/9.02 | (50) genls(c_tptpcol_8_26629, c_tptpcol_7_26628) % 61.90/9.02 | (51) $i(c_tptpcol_8_26629) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just17) implies: % 61.90/9.02 | (52) genls(c_tptpcol_7_26628, c_tptpcol_6_26627) % 61.90/9.02 | (53) $i(c_tptpcol_7_26628) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just15) implies: % 61.90/9.02 | (54) genls(c_tptpcol_6_26627, c_tptpcol_5_24579) % 61.90/9.02 | (55) $i(c_tptpcol_6_26627) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just13) implies: % 61.90/9.02 | (56) genls(c_tptpcol_5_24579, c_tptpcol_4_24578) % 61.90/9.02 | (57) $i(c_tptpcol_5_24579) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just11) implies: % 61.90/9.02 | (58) genls(c_tptpcol_4_24578, c_tptpcol_3_16386) % 61.90/9.02 | (59) $i(c_tptpcol_4_24578) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just9) implies: % 61.90/9.02 | (60) genls(c_tptpcol_3_16386, c_tptpcol_2_2) % 61.90/9.02 | (61) $i(c_tptpcol_3_16386) % 61.90/9.02 | % 61.90/9.02 | ALPHA: (just7) implies: % 61.90/9.02 | (62) genls(c_tptpcol_2_2, c_tptpcol_1_1) % 61.90/9.02 | (63) $i(c_tptpcol_2_2) % 61.90/9.02 | (64) $i(c_tptpcol_1_1) % 61.90/9.02 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_3_16386, c_tptpcol_2_2, % 61.90/9.03 | c_tptpcol_4_24578, simplifying with (58), (59), (60), (61), (63) % 61.90/9.03 | gives: % 61.90/9.03 | (65) genls(c_tptpcol_4_24578, c_tptpcol_2_2) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_5_24579, % 61.90/9.03 | c_tptpcol_4_24578, c_tptpcol_6_26627, simplifying with (54), % 61.90/9.03 | (55), (56), (57), (59) gives: % 61.90/9.03 | (66) genls(c_tptpcol_6_26627, c_tptpcol_4_24578) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_7_26628, % 61.90/9.03 | c_tptpcol_6_26627, c_tptpcol_8_26629, simplifying with (50), % 61.90/9.03 | (51), (52), (53), (55) gives: % 61.90/9.03 | (67) genls(c_tptpcol_8_26629, c_tptpcol_6_26627) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_9_26885, % 61.90/9.03 | c_tptpcol_8_26629, c_tptpcol_10_26886, simplifying with (46), % 61.90/9.03 | (47), (48), (49), (51) gives: % 61.90/9.03 | (68) genls(c_tptpcol_10_26886, c_tptpcol_8_26629) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_11_26887, % 61.90/9.03 | c_tptpcol_10_26886, c_tptpcol_12_26919, simplifying with (42), % 61.90/9.03 | (43), (44), (45), (47) gives: % 61.90/9.03 | (69) genls(c_tptpcol_12_26919, c_tptpcol_10_26886) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_13_26920, % 61.90/9.03 | c_tptpcol_12_26919, c_tptpcol_14_26921, simplifying with (38), % 61.90/9.03 | (39), (40), (41), (43) gives: % 61.90/9.03 | (70) genls(c_tptpcol_14_26921, c_tptpcol_12_26919) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_15_26925, % 61.90/9.03 | c_tptpcol_14_26921, c_tptpcol_16_26926, simplifying with (34), % 61.90/9.03 | (35), (36), (37), (39) gives: % 61.90/9.03 | (71) genls(c_tptpcol_16_26926, c_tptpcol_14_26921) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_2_65537, % 61.90/9.03 | c_tptpcol_1_65536, c_tptpcol_3_81921, simplifying with (29), % 61.90/9.03 | (30), (31), (32), (33) gives: % 61.90/9.03 | (72) genls(c_tptpcol_3_81921, c_tptpcol_1_65536) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_4_90113, % 61.90/9.03 | c_tptpcol_3_81921, c_tptpcol_5_90114, simplifying with (25), % 61.90/9.03 | (26), (27), (28), (30) gives: % 61.90/9.03 | (73) genls(c_tptpcol_5_90114, c_tptpcol_3_81921) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_6_92162, % 61.90/9.03 | c_tptpcol_5_90114, c_tptpcol_7_92163, simplifying with (21), % 61.90/9.03 | (22), (23), (24), (26) gives: % 61.90/9.03 | (74) genls(c_tptpcol_7_92163, c_tptpcol_5_90114) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_8_92164, % 61.90/9.03 | c_tptpcol_7_92163, c_tptpcol_9_92165, simplifying with (17), % 61.90/9.03 | (18), (19), (20), (22) gives: % 61.90/9.03 | (75) genls(c_tptpcol_9_92165, c_tptpcol_7_92163) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_10_92166, % 61.90/9.03 | c_tptpcol_9_92165, c_tptpcol_11_92230, simplifying with (13), % 61.90/9.03 | (14), (15), (16), (18) gives: % 61.90/9.03 | (76) genls(c_tptpcol_11_92230, c_tptpcol_9_92165) % 61.90/9.03 | % 61.90/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_12_92262, % 61.90/9.03 | c_tptpcol_11_92230, c_tptpcol_13_92263, simplifying with (9), % 61.90/9.03 | (10), (11), (12), (14) gives: % 61.90/9.03 | (77) genls(c_tptpcol_13_92263, c_tptpcol_11_92230) % 61.90/9.03 | % 62.07/9.03 | GROUND_INST: instantiating (just158) with c_tptpcol_15_92268, % 62.07/9.03 | c_tptpcol_14_92264, c_tptpcol_16_92269, simplifying with (3), % 62.07/9.03 | (4), (5), (6), (8) gives: % 62.07/9.03 | (78) genls(c_tptpcol_16_92269, c_tptpcol_14_92264) % 62.07/9.03 | % 62.07/9.03 | GROUND_INST: instantiating (just86) with c_tptpcol_1_1, c_tptpcol_1_65536, % 62.07/9.03 | c_tptpcol_2_2, simplifying with (2), (33), (62), (63), (64) % 62.07/9.03 | gives: % 62.07/9.03 | (79) disjointwith(c_tptpcol_2_2, c_tptpcol_1_65536) % 62.07/9.03 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_6_26627, % 62.07/9.04 | c_tptpcol_4_24578, c_tptpcol_8_26629, simplifying with (51), % 62.07/9.04 | (55), (59), (66), (67) gives: % 62.07/9.04 | (80) genls(c_tptpcol_8_26629, c_tptpcol_4_24578) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_10_26886, % 62.07/9.04 | c_tptpcol_8_26629, c_tptpcol_12_26919, simplifying with (43), % 62.07/9.04 | (47), (51), (68), (69) gives: % 62.07/9.04 | (81) genls(c_tptpcol_12_26919, c_tptpcol_8_26629) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_14_26921, % 62.07/9.04 | c_tptpcol_12_26919, c_tptpcol_16_26926, simplifying with (35), % 62.07/9.04 | (39), (43), (70), (71) gives: % 62.07/9.04 | (82) genls(c_tptpcol_16_26926, c_tptpcol_12_26919) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_3_81921, % 62.07/9.04 | c_tptpcol_1_65536, c_tptpcol_5_90114, simplifying with (26), % 62.07/9.04 | (30), (33), (72), (73) gives: % 62.07/9.04 | (83) genls(c_tptpcol_5_90114, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_7_92163, % 62.07/9.04 | c_tptpcol_5_90114, c_tptpcol_9_92165, simplifying with (18), % 62.07/9.04 | (22), (26), (74), (75) gives: % 62.07/9.04 | (84) genls(c_tptpcol_9_92165, c_tptpcol_5_90114) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_11_92230, % 62.07/9.04 | c_tptpcol_9_92165, c_tptpcol_13_92263, simplifying with (10), % 62.07/9.04 | (14), (18), (76), (77) gives: % 62.07/9.04 | (85) genls(c_tptpcol_13_92263, c_tptpcol_9_92165) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_14_92264, % 62.07/9.04 | c_tptpcol_13_92263, c_tptpcol_16_92269, simplifying with (4), % 62.07/9.04 | (7), (8), (10), (78) gives: % 62.07/9.04 | (86) genls(c_tptpcol_16_92269, c_tptpcol_13_92263) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just86) with c_tptpcol_2_2, c_tptpcol_1_65536, % 62.07/9.04 | c_tptpcol_4_24578, simplifying with (33), (59), (63), (65), (79) % 62.07/9.04 | gives: % 62.07/9.04 | (87) disjointwith(c_tptpcol_4_24578, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_12_26919, % 62.07/9.04 | c_tptpcol_8_26629, c_tptpcol_16_26926, simplifying with (35), % 62.07/9.04 | (43), (51), (81), (82) gives: % 62.07/9.04 | (88) genls(c_tptpcol_16_26926, c_tptpcol_8_26629) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_5_90114, % 62.07/9.04 | c_tptpcol_1_65536, c_tptpcol_9_92165, simplifying with (18), % 62.07/9.04 | (26), (33), (83), (84) gives: % 62.07/9.04 | (89) genls(c_tptpcol_9_92165, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_13_92263, % 62.07/9.04 | c_tptpcol_9_92165, c_tptpcol_16_92269, simplifying with (4), % 62.07/9.04 | (10), (18), (85), (86) gives: % 62.07/9.04 | (90) genls(c_tptpcol_16_92269, c_tptpcol_9_92165) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just86) with c_tptpcol_4_24578, c_tptpcol_1_65536, % 62.07/9.04 | c_tptpcol_8_26629, simplifying with (33), (51), (59), (80), (87) % 62.07/9.04 | gives: % 62.07/9.04 | (91) disjointwith(c_tptpcol_8_26629, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just158) with c_tptpcol_9_92165, % 62.07/9.04 | c_tptpcol_1_65536, c_tptpcol_16_92269, simplifying with (4), % 62.07/9.04 | (18), (33), (89), (90) gives: % 62.07/9.04 | (92) genls(c_tptpcol_16_92269, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just86) with c_tptpcol_8_26629, c_tptpcol_1_65536, % 62.07/9.04 | c_tptpcol_16_26926, simplifying with (33), (35), (51), (88), (91) % 62.07/9.04 | gives: % 62.07/9.04 | (93) disjointwith(c_tptpcol_16_26926, c_tptpcol_1_65536) % 62.07/9.04 | % 62.07/9.04 | GROUND_INST: instantiating (just85) with c_tptpcol_16_26926, % 62.07/9.04 | c_tptpcol_1_65536, c_tptpcol_16_92269, simplifying with (1), (4), % 62.07/9.04 | (33), (35), (92), (93) gives: % 62.07/9.04 | (94) $false % 62.07/9.05 | % 62.07/9.05 | CLOSE: (94) is inconsistent. % 62.07/9.05 | % 62.07/9.05 End of proof % 62.07/9.05 % SZS output end Proof for theBenchmark % 62.07/9.05 % 62.07/9.05 8417ms %------------------------------------------------------------------------------