%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR039+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 : n014.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:40 EDT 2023 % Result : Theorem 36.04s 5.50s % Output : Proof 58.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : CSR039+1 : TPTP v8.1.2. Released v3.4.0. % 0.00/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.14/0.33 % Computer : n014.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Mon Aug 28 09:57:15 EDT 2023 % 0.14/0.33 % CPUTime : % 0.18/0.56 ________ _____ % 0.18/0.56 ___ __ \_________(_)________________________________ % 0.18/0.56 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.18/0.56 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.18/0.56 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.18/0.56 % 0.18/0.56 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.18/0.56 (2023-06-19) % 0.18/0.56 % 0.18/0.56 (c) Philipp Rümmer, 2009-2023 % 0.18/0.56 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.18/0.56 Amanda Stjerna. % 0.18/0.56 Free software under BSD-3-Clause. % 0.18/0.56 % 0.18/0.56 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.18/0.56 % 0.18/0.56 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.18/0.57 Running up to 7 provers in parallel. % 0.18/0.58 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.18/0.58 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.18/0.58 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.18/0.58 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.18/0.58 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.18/0.58 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.18/0.58 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.86/1.20 Prover 4: Preprocessing ... % 3.86/1.20 Prover 1: Preprocessing ... % 4.25/1.23 Prover 6: Preprocessing ... % 4.25/1.23 Prover 2: Preprocessing ... % 4.25/1.23 Prover 0: Preprocessing ... % 4.25/1.23 Prover 3: Preprocessing ... % 4.25/1.25 Prover 5: Preprocessing ... % 8.69/1.87 Prover 5: Proving ... % 8.69/1.88 Prover 2: Proving ... % 10.47/2.13 Prover 6: Constructing countermodel ... % 10.47/2.13 Prover 3: Constructing countermodel ... % 10.47/2.16 Prover 1: Constructing countermodel ... % 11.35/2.24 Prover 0: Proving ... % 12.32/2.37 Prover 4: Constructing countermodel ... % 21.91/3.71 Prover 3: gave up % 21.91/3.71 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 23.27/3.80 Prover 7: Preprocessing ... % 24.92/4.03 Prover 7: Constructing countermodel ... % 24.92/4.06 Prover 1: gave up % 24.92/4.06 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 25.58/4.15 Prover 8: Preprocessing ... % 28.50/4.51 Prover 8: Warning: ignoring some quantifiers % 28.50/4.54 Prover 8: Constructing countermodel ... % 36.04/5.49 Prover 0: proved (4897ms) % 36.04/5.49 % 36.04/5.50 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 36.04/5.50 % 36.04/5.50 Prover 6: stopped % 36.04/5.50 Prover 2: stopped % 36.04/5.52 Prover 5: stopped % 36.04/5.52 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 36.04/5.52 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 36.04/5.52 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 36.04/5.52 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 36.04/5.65 Prover 10: Preprocessing ... % 36.04/5.65 Prover 11: Preprocessing ... % 36.04/5.69 Prover 13: Preprocessing ... % 36.04/5.69 Prover 16: Preprocessing ... % 38.02/5.78 Prover 10: Constructing countermodel ... % 38.42/5.82 Prover 16: Warning: ignoring some quantifiers % 38.42/5.82 Prover 13: Warning: ignoring some quantifiers % 38.42/5.82 Prover 16: Constructing countermodel ... % 38.42/5.82 Prover 13: Constructing countermodel ... % 39.95/6.01 Prover 8: gave up % 39.95/6.02 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 39.95/6.04 Prover 11: Constructing countermodel ... % 41.06/6.15 Prover 19: Preprocessing ... % 42.99/6.44 Prover 19: Warning: ignoring some quantifiers % 42.99/6.47 Prover 19: Constructing countermodel ... % 57.40/8.40 Prover 13: Found proof (size 84) % 57.40/8.40 Prover 13: proved (2885ms) % 57.40/8.40 Prover 10: stopped % 57.40/8.40 Prover 16: stopped % 57.40/8.40 Prover 7: stopped % 57.40/8.40 Prover 19: stopped % 57.40/8.40 Prover 11: stopped % 57.40/8.41 Prover 4: stopped % 57.40/8.41 % 57.40/8.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 57.40/8.41 % 57.40/8.42 % SZS output start Proof for theBenchmark % 57.40/8.42 Assumptions after simplification: % 57.40/8.42 --------------------------------- % 57.40/8.42 % 57.40/8.42 (just100) % 57.40/8.43 $i(c_tptpcol_5_90114) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_5_90114(v0) | % 57.40/8.43 isa(v0, c_tptpcol_5_90114)) % 57.40/8.43 % 57.40/8.43 (just102) % 57.40/8.43 $i(c_tptpcol_4_90113) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_4_90113(v0) | % 57.40/8.43 isa(v0, c_tptpcol_4_90113)) % 57.40/8.43 % 57.40/8.43 (just104) % 57.40/8.43 $i(c_tptpcol_3_81921) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_3_81921(v0) | % 57.40/8.43 isa(v0, c_tptpcol_3_81921)) % 57.40/8.43 % 57.40/8.43 (just106) % 57.40/8.43 $i(c_tptpcol_1_65536) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_1_65536(v0) | % 57.40/8.43 isa(v0, c_tptpcol_1_65536)) % 57.40/8.43 % 57.40/8.43 (just108) % 57.40/8.43 $i(c_tptpcol_2_65537) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_2_65537(v0) | % 57.40/8.43 isa(v0, c_tptpcol_2_65537)) % 57.40/8.43 % 57.40/8.43 (just11) % 57.40/8.43 $i(c_tptpcol_4_16387) & $i(c_tptpcol_3_16386) & genls(c_tptpcol_4_16387, % 57.40/8.43 c_tptpcol_3_16386) % 57.40/8.43 % 57.40/8.43 (just112) % 57.40/8.43 $i(c_tptpcol_12_18663) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_12_18663(v0) | % 57.40/8.43 isa(v0, c_tptpcol_12_18663)) % 57.40/8.43 % 57.40/8.43 (just114) % 57.40/8.43 $i(c_tptpcol_11_18631) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_11_18631(v0) | % 57.40/8.43 isa(v0, c_tptpcol_11_18631)) % 57.40/8.43 % 57.40/8.43 (just116) % 57.40/8.43 $i(c_tptpcol_10_18567) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_10_18567(v0) | % 57.40/8.43 isa(v0, c_tptpcol_10_18567)) % 57.40/8.43 % 57.40/8.43 (just118) % 57.40/8.43 $i(c_tptpcol_9_18439) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_9_18439(v0) | % 57.40/8.43 isa(v0, c_tptpcol_9_18439)) % 57.40/8.43 % 57.40/8.43 (just120) % 57.40/8.43 $i(c_tptpcol_8_18438) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_8_18438(v0) | % 57.40/8.43 isa(v0, c_tptpcol_8_18438)) % 57.40/8.43 % 57.40/8.43 (just122) % 57.40/8.43 $i(c_tptpcol_7_18437) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_7_18437(v0) | % 57.40/8.43 isa(v0, c_tptpcol_7_18437)) % 57.40/8.43 % 57.40/8.43 (just124) % 57.40/8.43 $i(c_tptpcol_6_18436) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_6_18436(v0) | % 57.40/8.43 isa(v0, c_tptpcol_6_18436)) % 57.40/8.43 % 57.40/8.43 (just126) % 57.40/8.44 $i(c_tptpcol_5_16388) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_5_16388(v0) | % 57.40/8.44 isa(v0, c_tptpcol_5_16388)) % 57.40/8.44 % 57.40/8.44 (just128) % 57.40/8.44 $i(c_tptpcol_4_16387) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_4_16387(v0) | % 57.40/8.44 isa(v0, c_tptpcol_4_16387)) % 57.40/8.44 % 57.40/8.44 (just13) % 57.40/8.44 $i(c_tptpcol_5_16388) & $i(c_tptpcol_4_16387) & genls(c_tptpcol_5_16388, % 57.40/8.44 c_tptpcol_4_16387) % 57.40/8.44 % 57.40/8.44 (just130) % 57.40/8.44 $i(c_tptpcol_3_16386) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_3_16386(v0) | % 57.40/8.44 isa(v0, c_tptpcol_3_16386)) % 57.40/8.44 % 57.40/8.44 (just132) % 57.40/8.44 $i(c_tptpcol_1_1) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_1_1(v0) | isa(v0, % 57.40/8.44 c_tptpcol_1_1)) % 57.40/8.44 % 57.40/8.44 (just134) % 57.40/8.44 $i(c_tptpcol_2_2) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_2_2(v0) | isa(v0, % 57.40/8.44 c_tptpcol_2_2)) % 57.40/8.44 % 57.40/8.44 (just142) % 57.40/8.44 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 57.40/8.44 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 57.40/8.44 % 57.40/8.44 (just15) % 57.40/8.44 $i(c_tptpcol_6_18436) & $i(c_tptpcol_5_16388) & genls(c_tptpcol_6_18436, % 57.40/8.44 c_tptpcol_5_16388) % 57.40/8.44 % 57.40/8.44 (just17) % 57.40/8.44 $i(c_tptpcol_7_18437) & $i(c_tptpcol_6_18436) & genls(c_tptpcol_7_18437, % 57.40/8.44 c_tptpcol_6_18436) % 57.40/8.44 % 57.40/8.44 (just19) % 57.40/8.44 $i(c_tptpcol_8_18438) & $i(c_tptpcol_7_18437) & genls(c_tptpcol_8_18438, % 57.40/8.44 c_tptpcol_7_18437) % 57.40/8.44 % 57.40/8.44 (just21) % 57.40/8.44 $i(c_tptpcol_9_18439) & $i(c_tptpcol_8_18438) & genls(c_tptpcol_9_18439, % 57.40/8.44 c_tptpcol_8_18438) % 57.40/8.44 % 57.40/8.44 (just23) % 57.40/8.44 $i(c_tptpcol_10_18567) & $i(c_tptpcol_9_18439) & genls(c_tptpcol_10_18567, % 57.40/8.44 c_tptpcol_9_18439) % 57.40/8.44 % 57.40/8.44 (just25) % 57.40/8.44 $i(c_tptpcol_11_18631) & $i(c_tptpcol_10_18567) & genls(c_tptpcol_11_18631, % 57.40/8.44 c_tptpcol_10_18567) % 57.40/8.44 % 57.40/8.44 (just27) % 57.40/8.44 $i(c_tptpcol_12_18663) & $i(c_tptpcol_11_18631) & genls(c_tptpcol_12_18663, % 57.40/8.44 c_tptpcol_11_18631) % 57.40/8.44 % 57.40/8.44 (just29) % 57.40/8.44 $i(c_tptpcol_13_18664) & $i(c_tptpcol_12_18663) & genls(c_tptpcol_13_18664, % 57.40/8.44 c_tptpcol_12_18663) % 57.40/8.44 % 57.40/8.44 (just31) % 57.40/8.44 $i(c_tptpcol_1_65536) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_2_65537, % 57.40/8.44 c_tptpcol_1_65536) % 57.40/8.44 % 57.40/8.44 (just33) % 57.40/8.44 $i(c_tptpcol_3_81921) & $i(c_tptpcol_2_65537) & genls(c_tptpcol_3_81921, % 57.40/8.44 c_tptpcol_2_65537) % 57.40/8.44 % 57.40/8.44 (just35) % 57.40/8.44 $i(c_tptpcol_4_90113) & $i(c_tptpcol_3_81921) & genls(c_tptpcol_4_90113, % 57.40/8.44 c_tptpcol_3_81921) % 57.40/8.44 % 57.40/8.44 (just37) % 57.40/8.44 $i(c_tptpcol_5_90114) & $i(c_tptpcol_4_90113) & genls(c_tptpcol_5_90114, % 57.40/8.44 c_tptpcol_4_90113) % 57.40/8.44 % 57.40/8.44 (just39) % 57.40/8.44 $i(c_tptpcol_6_92162) & $i(c_tptpcol_5_90114) & genls(c_tptpcol_6_92162, % 57.40/8.44 c_tptpcol_5_90114) % 57.40/8.44 % 57.40/8.44 (just41) % 57.40/8.44 $i(c_tptpcol_7_93186) & $i(c_tptpcol_6_92162) & genls(c_tptpcol_7_93186, % 57.40/8.44 c_tptpcol_6_92162) % 57.40/8.44 % 57.40/8.44 (just43) % 57.40/8.44 $i(c_tptpcol_8_93698) & $i(c_tptpcol_7_93186) & genls(c_tptpcol_8_93698, % 57.40/8.44 c_tptpcol_7_93186) % 57.40/8.44 % 57.40/8.44 (just45) % 57.40/8.44 $i(c_tptpcol_9_93699) & $i(c_tptpcol_8_93698) & genls(c_tptpcol_9_93699, % 57.40/8.44 c_tptpcol_8_93698) % 57.40/8.44 % 57.40/8.44 (just47) % 57.40/8.44 $i(c_tptpcol_10_93700) & $i(c_tptpcol_9_93699) & genls(c_tptpcol_10_93700, % 57.40/8.44 c_tptpcol_9_93699) % 57.40/8.44 % 57.40/8.44 (just49) % 57.40/8.44 $i(c_tptpcol_11_93764) & $i(c_tptpcol_10_93700) & genls(c_tptpcol_11_93764, % 57.40/8.44 c_tptpcol_10_93700) % 57.40/8.44 % 57.40/8.44 (just51) % 57.40/8.44 $i(c_tptpcol_12_93765) & $i(c_tptpcol_11_93764) & genls(c_tptpcol_12_93765, % 57.40/8.44 c_tptpcol_11_93764) % 57.40/8.44 % 57.40/8.44 (just53) % 57.40/8.44 $i(c_tptpcol_13_93766) & $i(c_tptpcol_12_93765) & genls(c_tptpcol_13_93766, % 57.40/8.44 c_tptpcol_12_93765) % 57.40/8.44 % 57.40/8.44 (just55) % 57.40/8.45 $i(c_tptpcol_14_93774) & $i(c_tptpcol_13_93766) & genls(c_tptpcol_14_93774, % 57.40/8.45 c_tptpcol_13_93766) % 57.40/8.45 % 57.40/8.45 (just57) % 57.40/8.45 $i(c_tptpcol_15_93775) & $i(c_tptpcol_14_93774) & genls(c_tptpcol_15_93775, % 57.40/8.45 c_tptpcol_14_93774) % 57.40/8.45 % 57.40/8.45 (just59) % 57.40/8.45 $i(c_tptpcol_1_65536) & $i(c_tptpcol_1_1) & disjointwith(c_tptpcol_1_1, % 57.40/8.45 c_tptpcol_1_65536) % 57.40/8.45 % 57.40/8.45 (just7) % 57.40/8.45 $i(c_tptpcol_1_1) & $i(c_tptpcol_2_2) & genls(c_tptpcol_2_2, c_tptpcol_1_1) % 57.40/8.45 % 57.40/8.45 (just76) % 57.40/8.45 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ disjointwith(v0, v1) | % 57.40/8.45 disjointwith(v1, v0)) % 57.40/8.45 % 57.40/8.45 (just77) % 57.40/8.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 57.40/8.45 ~ disjointwith(v0, v1) | ~ genls(v2, v1) | disjointwith(v0, v2)) % 57.40/8.45 % 57.40/8.45 (just78) % 57.40/8.45 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 57.40/8.45 ~ disjointwith(v0, v1) | ~ genls(v2, v0) | disjointwith(v2, v1)) % 57.40/8.45 % 57.40/8.45 (just82) % 57.40/8.45 $i(c_tptpcol_14_93774) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_14_93774(v0) | % 57.40/8.45 isa(v0, c_tptpcol_14_93774)) % 57.40/8.45 % 57.40/8.45 (just84) % 57.40/8.45 $i(c_tptpcol_13_93766) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_13_93766(v0) | % 57.40/8.45 isa(v0, c_tptpcol_13_93766)) % 57.40/8.45 % 57.40/8.45 (just86) % 57.40/8.45 $i(c_tptpcol_12_93765) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_12_93765(v0) | % 57.40/8.45 isa(v0, c_tptpcol_12_93765)) % 57.40/8.45 % 57.40/8.45 (just88) % 57.40/8.45 $i(c_tptpcol_11_93764) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_11_93764(v0) | % 57.40/8.45 isa(v0, c_tptpcol_11_93764)) % 57.40/8.45 % 57.40/8.45 (just9) % 57.40/8.45 $i(c_tptpcol_3_16386) & $i(c_tptpcol_2_2) & genls(c_tptpcol_3_16386, % 57.40/8.45 c_tptpcol_2_2) % 57.40/8.45 % 57.40/8.45 (just90) % 57.40/8.45 $i(c_tptpcol_10_93700) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_10_93700(v0) | % 57.40/8.45 isa(v0, c_tptpcol_10_93700)) % 57.40/8.45 % 57.40/8.45 (just92) % 57.40/8.45 $i(c_tptpcol_9_93699) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_9_93699(v0) | % 57.40/8.45 isa(v0, c_tptpcol_9_93699)) % 57.40/8.45 % 57.40/8.45 (just94) % 57.40/8.45 $i(c_tptpcol_8_93698) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_8_93698(v0) | % 57.40/8.45 isa(v0, c_tptpcol_8_93698)) % 57.40/8.45 % 57.40/8.45 (just96) % 57.40/8.45 $i(c_tptpcol_7_93186) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_7_93186(v0) | % 57.40/8.45 isa(v0, c_tptpcol_7_93186)) % 57.40/8.45 % 57.40/8.45 (just98) % 57.40/8.45 $i(c_tptpcol_6_92162) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_6_92162(v0) | % 57.40/8.45 isa(v0, c_tptpcol_6_92162)) % 57.40/8.45 % 57.40/8.45 (query39) % 58.61/8.47 $i(c_tptpcol_15_93775) & $i(c_tptpcol_13_18664) & $i(c_translation_7) & % 58.61/8.47 $i(s_http_wwwpoweripodsearchinfobrown_ipodhtml) & ? [v0: $i] : ? [v1: $i] : % 58.61/8.47 ? [v2: $i] : (f_contentmtofcdafromeventfn(v1, c_translation_7) = v2 & % 58.61/8.47 f_urlreferentfn(v0) = v1 & % 58.61/8.47 f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml) = v0 & $i(v2) & $i(v1) % 58.61/8.47 & $i(v0) & mtvisible(v2) & ~ disjointwith(c_tptpcol_15_93775, % 58.61/8.47 c_tptpcol_13_18664)) % 58.61/8.47 % 58.61/8.47 Further assumptions not needed in the proof: % 58.61/8.47 -------------------------------------------- % 58.61/8.47 just1, just10, just101, just103, just105, just107, just109, just110, just111, % 58.61/8.47 just113, just115, just117, just119, just12, just121, just123, just125, just127, % 58.61/8.47 just129, just131, just133, just135, just136, just137, just138, just139, just14, % 58.61/8.47 just140, just141, just143, just144, just145, just146, just147, just148, just149, % 58.61/8.47 just150, just151, just152, just153, just154, just155, just156, just157, just158, % 58.61/8.47 just159, just16, just160, just161, just162, just163, just164, just165, just166, % 58.61/8.47 just167, just168, just169, just170, just18, just2, just20, just22, just24, % 58.61/8.47 just26, just28, just3, just30, just32, just34, just36, just38, just4, just40, % 58.61/8.47 just42, just44, just46, just48, just5, just50, just52, just54, just56, just58, % 58.61/8.47 just6, just60, just61, just62, just63, just64, just65, just66, just67, just68, % 58.61/8.47 just69, just70, just71, just72, just73, just74, just75, just79, just8, just80, % 58.61/8.47 just81, just83, just85, just87, just89, just91, just93, just95, just97, just99 % 58.61/8.47 % 58.61/8.47 Those formulas are unsatisfiable: % 58.61/8.47 --------------------------------- % 58.61/8.47 % 58.61/8.47 Begin of proof % 58.61/8.47 | % 58.61/8.47 | ALPHA: (just7) implies: % 58.61/8.47 | (1) genls(c_tptpcol_2_2, c_tptpcol_1_1) % 58.61/8.47 | % 58.61/8.47 | ALPHA: (just9) implies: % 58.61/8.47 | (2) genls(c_tptpcol_3_16386, c_tptpcol_2_2) % 58.61/8.47 | % 58.61/8.47 | ALPHA: (just11) implies: % 58.61/8.47 | (3) genls(c_tptpcol_4_16387, c_tptpcol_3_16386) % 58.61/8.47 | % 58.61/8.47 | ALPHA: (just13) implies: % 58.61/8.47 | (4) genls(c_tptpcol_5_16388, c_tptpcol_4_16387) % 58.61/8.47 | % 58.61/8.47 | ALPHA: (just15) implies: % 58.61/8.47 | (5) genls(c_tptpcol_6_18436, c_tptpcol_5_16388) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just17) implies: % 58.61/8.48 | (6) genls(c_tptpcol_7_18437, c_tptpcol_6_18436) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just19) implies: % 58.61/8.48 | (7) genls(c_tptpcol_8_18438, c_tptpcol_7_18437) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just21) implies: % 58.61/8.48 | (8) genls(c_tptpcol_9_18439, c_tptpcol_8_18438) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just23) implies: % 58.61/8.48 | (9) genls(c_tptpcol_10_18567, c_tptpcol_9_18439) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just25) implies: % 58.61/8.48 | (10) genls(c_tptpcol_11_18631, c_tptpcol_10_18567) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just27) implies: % 58.61/8.48 | (11) genls(c_tptpcol_12_18663, c_tptpcol_11_18631) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just29) implies: % 58.61/8.48 | (12) genls(c_tptpcol_13_18664, c_tptpcol_12_18663) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just31) implies: % 58.61/8.48 | (13) genls(c_tptpcol_2_65537, c_tptpcol_1_65536) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just33) implies: % 58.61/8.48 | (14) genls(c_tptpcol_3_81921, c_tptpcol_2_65537) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just35) implies: % 58.61/8.48 | (15) genls(c_tptpcol_4_90113, c_tptpcol_3_81921) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just37) implies: % 58.61/8.48 | (16) genls(c_tptpcol_5_90114, c_tptpcol_4_90113) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just39) implies: % 58.61/8.48 | (17) genls(c_tptpcol_6_92162, c_tptpcol_5_90114) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just41) implies: % 58.61/8.48 | (18) genls(c_tptpcol_7_93186, c_tptpcol_6_92162) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just43) implies: % 58.61/8.48 | (19) genls(c_tptpcol_8_93698, c_tptpcol_7_93186) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just45) implies: % 58.61/8.48 | (20) genls(c_tptpcol_9_93699, c_tptpcol_8_93698) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just47) implies: % 58.61/8.48 | (21) genls(c_tptpcol_10_93700, c_tptpcol_9_93699) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just49) implies: % 58.61/8.48 | (22) genls(c_tptpcol_11_93764, c_tptpcol_10_93700) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just51) implies: % 58.61/8.48 | (23) genls(c_tptpcol_12_93765, c_tptpcol_11_93764) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just53) implies: % 58.61/8.48 | (24) genls(c_tptpcol_13_93766, c_tptpcol_12_93765) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just55) implies: % 58.61/8.48 | (25) genls(c_tptpcol_14_93774, c_tptpcol_13_93766) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just57) implies: % 58.61/8.48 | (26) genls(c_tptpcol_15_93775, c_tptpcol_14_93774) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just59) implies: % 58.61/8.48 | (27) disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just82) implies: % 58.61/8.48 | (28) $i(c_tptpcol_14_93774) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just84) implies: % 58.61/8.48 | (29) $i(c_tptpcol_13_93766) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just86) implies: % 58.61/8.48 | (30) $i(c_tptpcol_12_93765) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just88) implies: % 58.61/8.48 | (31) $i(c_tptpcol_11_93764) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just90) implies: % 58.61/8.48 | (32) $i(c_tptpcol_10_93700) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just92) implies: % 58.61/8.48 | (33) $i(c_tptpcol_9_93699) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just94) implies: % 58.61/8.48 | (34) $i(c_tptpcol_8_93698) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just96) implies: % 58.61/8.48 | (35) $i(c_tptpcol_7_93186) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just98) implies: % 58.61/8.48 | (36) $i(c_tptpcol_6_92162) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just100) implies: % 58.61/8.48 | (37) $i(c_tptpcol_5_90114) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just102) implies: % 58.61/8.48 | (38) $i(c_tptpcol_4_90113) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just104) implies: % 58.61/8.48 | (39) $i(c_tptpcol_3_81921) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just106) implies: % 58.61/8.48 | (40) $i(c_tptpcol_1_65536) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just108) implies: % 58.61/8.48 | (41) $i(c_tptpcol_2_65537) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just112) implies: % 58.61/8.48 | (42) $i(c_tptpcol_12_18663) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just114) implies: % 58.61/8.48 | (43) $i(c_tptpcol_11_18631) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just116) implies: % 58.61/8.48 | (44) $i(c_tptpcol_10_18567) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just118) implies: % 58.61/8.48 | (45) $i(c_tptpcol_9_18439) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just120) implies: % 58.61/8.48 | (46) $i(c_tptpcol_8_18438) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just122) implies: % 58.61/8.48 | (47) $i(c_tptpcol_7_18437) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just124) implies: % 58.61/8.48 | (48) $i(c_tptpcol_6_18436) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just126) implies: % 58.61/8.48 | (49) $i(c_tptpcol_5_16388) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just128) implies: % 58.61/8.48 | (50) $i(c_tptpcol_4_16387) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just130) implies: % 58.61/8.48 | (51) $i(c_tptpcol_3_16386) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just132) implies: % 58.61/8.48 | (52) $i(c_tptpcol_1_1) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (just134) implies: % 58.61/8.48 | (53) $i(c_tptpcol_2_2) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (query39) implies: % 58.61/8.48 | (54) $i(c_tptpcol_13_18664) % 58.61/8.48 | (55) $i(c_tptpcol_15_93775) % 58.61/8.48 | (56) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 58.61/8.48 | (f_contentmtofcdafromeventfn(v1, c_translation_7) = v2 & % 58.61/8.48 | f_urlreferentfn(v0) = v1 & % 58.61/8.48 | f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml) = v0 & $i(v2) & % 58.61/8.48 | $i(v1) & $i(v0) & mtvisible(v2) & ~ % 58.61/8.48 | disjointwith(c_tptpcol_15_93775, c_tptpcol_13_18664)) % 58.61/8.48 | % 58.61/8.48 | DELTA: instantiating (56) with fresh symbols all_144_0, all_144_1, all_144_2 % 58.61/8.48 | gives: % 58.61/8.48 | (57) f_contentmtofcdafromeventfn(all_144_1, c_translation_7) = all_144_0 & % 58.61/8.48 | f_urlreferentfn(all_144_2) = all_144_1 & % 58.61/8.48 | f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml) = all_144_2 & % 58.61/8.48 | $i(all_144_0) & $i(all_144_1) & $i(all_144_2) & mtvisible(all_144_0) & % 58.61/8.48 | ~ disjointwith(c_tptpcol_15_93775, c_tptpcol_13_18664) % 58.61/8.48 | % 58.61/8.48 | ALPHA: (57) implies: % 58.61/8.49 | (58) ~ disjointwith(c_tptpcol_15_93775, c_tptpcol_13_18664) % 58.61/8.49 | % 58.61/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_2_2, c_tptpcol_1_1, % 58.61/8.49 | c_tptpcol_3_16386, simplifying with (1), (2), (51), (52), (53) % 58.61/8.49 | gives: % 58.61/8.49 | (59) genls(c_tptpcol_3_16386, c_tptpcol_1_1) % 58.61/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_4_16387, % 58.82/8.49 | c_tptpcol_3_16386, c_tptpcol_5_16388, simplifying with (3), (4), % 58.82/8.49 | (49), (50), (51) gives: % 58.82/8.49 | (60) genls(c_tptpcol_5_16388, c_tptpcol_3_16386) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_7_18437, % 58.82/8.49 | c_tptpcol_6_18436, c_tptpcol_8_18438, simplifying with (6), (7), % 58.82/8.49 | (46), (47), (48) gives: % 58.82/8.49 | (61) genls(c_tptpcol_8_18438, c_tptpcol_6_18436) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_9_18439, % 58.82/8.49 | c_tptpcol_8_18438, c_tptpcol_10_18567, simplifying with (8), (9), % 58.82/8.49 | (44), (45), (46) gives: % 58.82/8.49 | (62) genls(c_tptpcol_10_18567, c_tptpcol_8_18438) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_12_18663, % 58.82/8.49 | c_tptpcol_11_18631, c_tptpcol_13_18664, simplifying with (11), % 58.82/8.49 | (12), (42), (43), (54) gives: % 58.82/8.49 | (63) genls(c_tptpcol_13_18664, c_tptpcol_11_18631) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_2_65537, % 58.82/8.49 | c_tptpcol_1_65536, c_tptpcol_3_81921, simplifying with (13), % 58.82/8.49 | (14), (39), (40), (41) gives: % 58.82/8.49 | (64) genls(c_tptpcol_3_81921, c_tptpcol_1_65536) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_4_90113, % 58.82/8.49 | c_tptpcol_3_81921, c_tptpcol_5_90114, simplifying with (15), % 58.82/8.49 | (16), (37), (38), (39) gives: % 58.82/8.49 | (65) genls(c_tptpcol_5_90114, c_tptpcol_3_81921) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_6_92162, % 58.82/8.49 | c_tptpcol_5_90114, c_tptpcol_7_93186, simplifying with (17), % 58.82/8.49 | (18), (35), (36), (37) gives: % 58.82/8.49 | (66) genls(c_tptpcol_7_93186, c_tptpcol_5_90114) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_8_93698, % 58.82/8.49 | c_tptpcol_7_93186, c_tptpcol_9_93699, simplifying with (19), % 58.82/8.49 | (20), (33), (34), (35) gives: % 58.82/8.49 | (67) genls(c_tptpcol_9_93699, c_tptpcol_7_93186) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_10_93700, % 58.82/8.49 | c_tptpcol_9_93699, c_tptpcol_11_93764, simplifying with (21), % 58.82/8.49 | (22), (31), (32), (33) gives: % 58.82/8.49 | (68) genls(c_tptpcol_11_93764, c_tptpcol_9_93699) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_12_93765, % 58.82/8.49 | c_tptpcol_11_93764, c_tptpcol_13_93766, simplifying with (23), % 58.82/8.49 | (24), (29), (30), (31) gives: % 58.82/8.49 | (69) genls(c_tptpcol_13_93766, c_tptpcol_11_93764) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just142) with c_tptpcol_14_93774, % 58.82/8.49 | c_tptpcol_13_93766, c_tptpcol_15_93775, simplifying with (25), % 58.82/8.49 | (26), (28), (29), (55) gives: % 58.82/8.49 | (70) genls(c_tptpcol_15_93775, c_tptpcol_13_93766) % 58.82/8.49 | % 58.82/8.49 | GROUND_INST: instantiating (just76) with c_tptpcol_1_1, c_tptpcol_1_65536, % 58.82/8.49 | simplifying with (27), (40), (52) gives: % 58.82/8.49 | (71) disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1) % 58.82/8.49 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_3_16386, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_5_16388, simplifying with (49), (51), (52), (59), (60) % 58.82/8.50 | gives: % 58.82/8.50 | (72) genls(c_tptpcol_5_16388, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_6_18436, % 58.82/8.50 | c_tptpcol_5_16388, c_tptpcol_8_18438, simplifying with (5), (46), % 58.82/8.50 | (48), (49), (61) gives: % 58.82/8.50 | (73) genls(c_tptpcol_8_18438, c_tptpcol_5_16388) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_11_18631, % 58.82/8.50 | c_tptpcol_10_18567, c_tptpcol_13_18664, simplifying with (10), % 58.82/8.50 | (43), (44), (54), (63) gives: % 58.82/8.50 | (74) genls(c_tptpcol_13_18664, c_tptpcol_10_18567) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_5_90114, % 58.82/8.50 | c_tptpcol_3_81921, c_tptpcol_7_93186, simplifying with (35), % 58.82/8.50 | (37), (39), (65), (66) gives: % 58.82/8.50 | (75) genls(c_tptpcol_7_93186, c_tptpcol_3_81921) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_9_93699, % 58.82/8.50 | c_tptpcol_7_93186, c_tptpcol_11_93764, simplifying with (31), % 58.82/8.50 | (33), (35), (67), (68) gives: % 58.82/8.50 | (76) genls(c_tptpcol_11_93764, c_tptpcol_7_93186) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_13_93766, % 58.82/8.50 | c_tptpcol_11_93764, c_tptpcol_15_93775, simplifying with (29), % 58.82/8.50 | (31), (55), (69), (70) gives: % 58.82/8.50 | (77) genls(c_tptpcol_15_93775, c_tptpcol_11_93764) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just78) with c_tptpcol_1_65536, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_3_81921, simplifying with (39), (40), (52), (64), (71) % 58.82/8.50 | gives: % 58.82/8.50 | (78) disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_5_16388, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_8_18438, simplifying with (46), (49), (52), (72), (73) % 58.82/8.50 | gives: % 58.82/8.50 | (79) genls(c_tptpcol_8_18438, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_10_18567, % 58.82/8.50 | c_tptpcol_8_18438, c_tptpcol_13_18664, simplifying with (44), % 58.82/8.50 | (46), (54), (62), (74) gives: % 58.82/8.50 | (80) genls(c_tptpcol_13_18664, c_tptpcol_8_18438) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_11_93764, % 58.82/8.50 | c_tptpcol_7_93186, c_tptpcol_15_93775, simplifying with (31), % 58.82/8.50 | (35), (55), (76), (77) gives: % 58.82/8.50 | (81) genls(c_tptpcol_15_93775, c_tptpcol_7_93186) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just78) with c_tptpcol_3_81921, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_7_93186, simplifying with (35), (39), (52), (75), (78) % 58.82/8.50 | gives: % 58.82/8.50 | (82) disjointwith(c_tptpcol_7_93186, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just142) with c_tptpcol_8_18438, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_13_18664, simplifying with (46), (52), (54), (79), (80) % 58.82/8.50 | gives: % 58.82/8.50 | (83) genls(c_tptpcol_13_18664, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just78) with c_tptpcol_7_93186, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_15_93775, simplifying with (35), (52), (55), (81), (82) % 58.82/8.50 | gives: % 58.82/8.50 | (84) disjointwith(c_tptpcol_15_93775, c_tptpcol_1_1) % 58.82/8.50 | % 58.82/8.50 | GROUND_INST: instantiating (just77) with c_tptpcol_15_93775, c_tptpcol_1_1, % 58.82/8.50 | c_tptpcol_13_18664, simplifying with (52), (54), (55), (58), % 58.82/8.50 | (83), (84) gives: % 58.82/8.50 | (85) $false % 58.82/8.50 | % 58.82/8.50 | CLOSE: (85) is inconsistent. % 58.82/8.50 | % 58.82/8.50 End of proof % 58.82/8.50 % SZS output end Proof for theBenchmark % 58.82/8.50 % 58.82/8.50 7947ms %------------------------------------------------------------------------------