%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR040+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 : n018.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 34.34s 5.29s % Output : Proof 45.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : CSR040+1 : TPTP v8.1.2. Released v3.4.0. % 0.10/0.12 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.12/0.32 % Computer : n018.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Mon Aug 28 13:42:47 EDT 2023 % 0.12/0.32 % CPUTime : % 0.18/0.58 ________ _____ % 0.18/0.58 ___ __ \_________(_)________________________________ % 0.18/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.18/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.18/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.18/0.58 % 0.18/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.18/0.58 (2023-06-19) % 0.18/0.58 % 0.18/0.58 (c) Philipp Rümmer, 2009-2023 % 0.18/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.18/0.58 Amanda Stjerna. % 0.18/0.58 Free software under BSD-3-Clause. % 0.18/0.58 % 0.18/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.18/0.58 % 0.18/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.18/0.59 Running up to 7 provers in parallel. % 0.18/0.61 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.18/0.61 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.18/0.61 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.18/0.61 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.18/0.61 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.18/0.61 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.18/0.61 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 3.57/1.24 Prover 4: Preprocessing ... % 3.57/1.24 Prover 1: Preprocessing ... % 4.22/1.28 Prover 6: Preprocessing ... % 4.22/1.28 Prover 0: Preprocessing ... % 4.22/1.28 Prover 5: Preprocessing ... % 4.22/1.28 Prover 3: Preprocessing ... % 4.22/1.28 Prover 2: Preprocessing ... % 8.11/1.86 Prover 2: Proving ... % 8.11/1.86 Prover 5: Proving ... % 9.72/2.05 Prover 6: Constructing countermodel ... % 9.72/2.05 Prover 3: Constructing countermodel ... % 10.16/2.10 Prover 1: Constructing countermodel ... % 11.40/2.25 Prover 0: Proving ... % 11.40/2.29 Prover 4: Constructing countermodel ... % 17.00/3.10 Prover 3: gave up % 17.00/3.10 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 18.52/3.21 Prover 7: Preprocessing ... % 18.52/3.23 Prover 1: gave up % 19.04/3.25 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 19.51/3.33 Prover 8: Preprocessing ... % 19.51/3.34 Prover 7: Constructing countermodel ... % 21.37/3.61 Prover 8: Warning: ignoring some quantifiers % 21.37/3.64 Prover 8: Constructing countermodel ... % 28.13/4.47 Prover 8: gave up % 28.13/4.49 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 28.68/4.54 Prover 9: Preprocessing ... % 30.47/4.73 Prover 9: Constructing countermodel ... % 34.34/5.29 Prover 0: proved (4688ms) % 34.34/5.29 % 34.34/5.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 34.34/5.29 % 34.34/5.30 Prover 6: stopped % 34.34/5.30 Prover 9: stopped % 34.34/5.30 Prover 2: stopped % 34.34/5.30 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 34.34/5.30 Prover 5: stopped % 34.34/5.30 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 34.34/5.30 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 34.34/5.30 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 34.34/5.30 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 35.11/5.38 Prover 10: Preprocessing ... % 35.11/5.39 Prover 16: Preprocessing ... % 35.11/5.39 Prover 13: Preprocessing ... % 35.11/5.39 Prover 11: Preprocessing ... % 35.68/5.43 Prover 19: Preprocessing ... % 35.68/5.44 Prover 10: Constructing countermodel ... % 36.25/5.48 Prover 16: Warning: ignoring some quantifiers % 36.25/5.50 Prover 16: Constructing countermodel ... % 36.25/5.51 Prover 13: Warning: ignoring some quantifiers % 36.25/5.52 Prover 13: Constructing countermodel ... % 37.38/5.64 Prover 11: Constructing countermodel ... % 37.38/5.65 Prover 19: Warning: ignoring some quantifiers % 37.38/5.66 Prover 19: Constructing countermodel ... % 45.09/6.64 Prover 10: Found proof (size 65) % 45.09/6.64 Prover 10: proved (1342ms) % 45.09/6.64 Prover 13: stopped % 45.09/6.64 Prover 11: stopped % 45.09/6.64 Prover 19: stopped % 45.09/6.64 Prover 7: stopped % 45.09/6.64 Prover 16: stopped % 45.09/6.64 Prover 4: stopped % 45.09/6.64 % 45.09/6.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 45.09/6.64 % 45.09/6.65 % SZS output start Proof for theBenchmark % 45.09/6.66 Assumptions after simplification: % 45.09/6.66 --------------------------------- % 45.09/6.66 % 45.09/6.66 (just10) % 45.38/6.66 $i(c_individual) & $i(c_collection) & disjointwith(c_collection, c_individual) % 45.38/6.66 % 45.38/6.66 (just102) % 45.38/6.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 45.38/6.66 ~ disjointwith(v0, v1) | ~ genls(v2, v1) | disjointwith(v0, v2)) % 45.38/6.66 % 45.38/6.66 (just103) % 45.38/6.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 45.38/6.66 ~ disjointwith(v0, v1) | ~ genls(v2, v0) | disjointwith(v2, v1)) % 45.38/6.66 % 45.38/6.66 (just111) % 45.38/6.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 45.38/6.66 ~ isa(v0, v1) | ~ genls(v1, v2) | isa(v0, v2)) % 45.38/6.66 % 45.38/6.66 (just114) % 45.38/6.66 $i(c_fixedordercollection) & ! [v0: $i] : ( ~ $i(v0) | ~ % 45.38/6.66 fixedordercollection(v0) | isa(v0, c_fixedordercollection)) % 45.38/6.66 % 45.38/6.66 (just116) % 45.38/6.66 $i(c_firstordercollection) & ! [v0: $i] : ( ~ $i(v0) | ~ % 45.38/6.66 firstordercollection(v0) | isa(v0, c_firstordercollection)) % 45.38/6.66 % 45.38/6.66 (just124) % 45.38/6.66 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 45.38/6.66 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 45.38/6.66 % 45.38/6.66 (just13) % 45.38/6.66 $i(c_collection) & $i(c_fixedordercollection) & genls(c_fixedordercollection, % 45.38/6.66 c_collection) % 45.38/6.66 % 45.38/6.66 (just15) % 45.38/6.67 $i(c_tptpcol_0_0) & $i(c_individual) & genls(c_tptpcol_0_0, c_individual) % 45.38/6.67 % 45.38/6.67 (just17) % 45.38/6.67 $i(c_tptpcol_16_62187) & firstordercollection(c_tptpcol_16_62187) % 45.38/6.67 % 45.38/6.67 (just18) % 45.38/6.67 $i(c_tptpcol_1_65536) & $i(c_tptpcol_0_0) & genls(c_tptpcol_1_65536, % 45.38/6.67 c_tptpcol_0_0) % 45.38/6.67 % 45.38/6.67 (just20) % 45.38/6.67 $i(c_tptpcol_2_98304) & $i(c_tptpcol_1_65536) & genls(c_tptpcol_2_98304, % 45.38/6.67 c_tptpcol_1_65536) % 45.38/6.67 % 45.38/6.67 (just22) % 45.38/6.67 $i(c_tptpcol_3_98305) & $i(c_tptpcol_2_98304) & genls(c_tptpcol_3_98305, % 45.38/6.67 c_tptpcol_2_98304) % 45.38/6.67 % 45.38/6.67 (just24) % 45.38/6.67 $i(c_tptpcol_4_106497) & $i(c_tptpcol_3_98305) & genls(c_tptpcol_4_106497, % 45.38/6.67 c_tptpcol_3_98305) % 45.38/6.67 % 45.38/6.67 (just26) % 45.38/6.67 $i(c_tptpcol_5_106498) & $i(c_tptpcol_4_106497) & genls(c_tptpcol_5_106498, % 45.38/6.67 c_tptpcol_4_106497) % 45.38/6.67 % 45.38/6.67 (just28) % 45.38/6.67 $i(c_tptpcol_6_108546) & $i(c_tptpcol_5_106498) & genls(c_tptpcol_6_108546, % 45.38/6.67 c_tptpcol_5_106498) % 45.38/6.67 % 45.38/6.67 (just3) % 45.38/6.67 $i(c_fixedordercollection) & $i(c_firstordercollection) & % 45.38/6.67 genls(c_firstordercollection, c_fixedordercollection) % 45.38/6.67 % 45.38/6.67 (just30) % 45.38/6.67 $i(c_tptpcol_7_108547) & $i(c_tptpcol_6_108546) & genls(c_tptpcol_7_108547, % 45.38/6.67 c_tptpcol_6_108546) % 45.38/6.67 % 45.38/6.67 (just32) % 45.38/6.67 $i(c_tptpcol_8_109059) & $i(c_tptpcol_7_108547) & genls(c_tptpcol_8_109059, % 45.38/6.67 c_tptpcol_7_108547) % 45.38/6.67 % 45.38/6.67 (just34) % 45.38/6.67 $i(c_tptpcol_9_109060) & $i(c_tptpcol_8_109059) & genls(c_tptpcol_9_109060, % 45.38/6.67 c_tptpcol_8_109059) % 45.38/6.67 % 45.38/6.67 (just36) % 45.38/6.67 $i(c_tptpcol_10_109061) & $i(c_tptpcol_9_109060) & genls(c_tptpcol_10_109061, % 45.38/6.67 c_tptpcol_9_109060) % 45.38/6.67 % 45.38/6.67 (just38) % 45.38/6.67 $i(c_tptpcol_11_109125) & $i(c_tptpcol_10_109061) & genls(c_tptpcol_11_109125, % 45.38/6.67 c_tptpcol_10_109061) % 45.38/6.67 % 45.38/6.67 (just40) % 45.38/6.67 $i(c_tptpcol_12_109157) & $i(c_tptpcol_11_109125) & genls(c_tptpcol_12_109157, % 45.38/6.67 c_tptpcol_11_109125) % 45.38/6.67 % 45.38/6.67 (just42) % 45.38/6.67 $i(c_tptpcol_13_109173) & $i(c_tptpcol_12_109157) & genls(c_tptpcol_13_109173, % 45.38/6.67 c_tptpcol_12_109157) % 45.38/6.67 % 45.38/6.67 (just44) % 45.38/6.67 $i(c_tptpcol_14_109181) & $i(c_tptpcol_13_109173) & genls(c_tptpcol_14_109181, % 45.38/6.67 c_tptpcol_13_109173) % 45.38/6.67 % 45.38/6.67 (just46) % 45.38/6.67 $i(c_tptpcol_15_109185) & $i(c_tptpcol_14_109181) & genls(c_tptpcol_15_109185, % 45.38/6.67 c_tptpcol_14_109181) % 45.38/6.67 % 45.38/6.67 (just48) % 45.38/6.67 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 45.38/6.67 ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 45.38/6.67 % 45.38/6.67 (just62) % 45.38/6.67 $i(c_tptpcol_15_109185) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_15_109185(v0) % 45.38/6.67 | isa(v0, c_tptpcol_15_109185)) % 45.38/6.67 % 45.38/6.67 (just64) % 45.38/6.67 $i(c_tptpcol_14_109181) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_14_109181(v0) % 45.38/6.67 | isa(v0, c_tptpcol_14_109181)) % 45.38/6.67 % 45.38/6.67 (just66) % 45.38/6.67 $i(c_tptpcol_13_109173) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_13_109173(v0) % 45.38/6.67 | isa(v0, c_tptpcol_13_109173)) % 45.38/6.67 % 45.38/6.67 (just68) % 45.38/6.67 $i(c_tptpcol_12_109157) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_12_109157(v0) % 45.38/6.67 | isa(v0, c_tptpcol_12_109157)) % 45.38/6.67 % 45.38/6.67 (just70) % 45.38/6.67 $i(c_tptpcol_11_109125) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_11_109125(v0) % 45.38/6.67 | isa(v0, c_tptpcol_11_109125)) % 45.38/6.67 % 45.38/6.67 (just72) % 45.38/6.67 $i(c_tptpcol_10_109061) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_10_109061(v0) % 45.38/6.67 | isa(v0, c_tptpcol_10_109061)) % 45.38/6.67 % 45.38/6.67 (just74) % 45.38/6.67 $i(c_tptpcol_9_109060) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_9_109060(v0) | % 45.38/6.67 isa(v0, c_tptpcol_9_109060)) % 45.38/6.67 % 45.38/6.67 (just76) % 45.38/6.67 $i(c_tptpcol_8_109059) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_8_109059(v0) | % 45.38/6.67 isa(v0, c_tptpcol_8_109059)) % 45.38/6.67 % 45.38/6.67 (just78) % 45.38/6.67 $i(c_tptpcol_7_108547) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_7_108547(v0) | % 45.38/6.67 isa(v0, c_tptpcol_7_108547)) % 45.38/6.67 % 45.38/6.67 (just80) % 45.38/6.67 $i(c_tptpcol_6_108546) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_6_108546(v0) | % 45.38/6.67 isa(v0, c_tptpcol_6_108546)) % 45.38/6.67 % 45.38/6.67 (just82) % 45.38/6.67 $i(c_tptpcol_5_106498) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_5_106498(v0) | % 45.38/6.67 isa(v0, c_tptpcol_5_106498)) % 45.38/6.67 % 45.38/6.67 (just84) % 45.38/6.67 $i(c_tptpcol_4_106497) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_4_106497(v0) | % 45.38/6.67 isa(v0, c_tptpcol_4_106497)) % 45.38/6.67 % 45.38/6.67 (just86) % 45.38/6.67 $i(c_tptpcol_3_98305) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_3_98305(v0) | % 45.38/6.68 isa(v0, c_tptpcol_3_98305)) % 45.38/6.68 % 45.38/6.68 (just88) % 45.38/6.68 $i(c_tptpcol_2_98304) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_2_98304(v0) | % 45.38/6.68 isa(v0, c_tptpcol_2_98304)) % 45.38/6.68 % 45.38/6.68 (just90) % 45.38/6.68 $i(c_tptpcol_1_65536) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_1_65536(v0) | % 45.38/6.68 isa(v0, c_tptpcol_1_65536)) % 45.38/6.68 % 45.38/6.68 (just94) % 45.38/6.68 $i(c_tptpcol_0_0) & ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_0_0(v0) | isa(v0, % 45.38/6.68 c_tptpcol_0_0)) % 45.38/6.68 % 45.38/6.68 (just96) % 45.38/6.68 $i(c_individual) & ! [v0: $i] : ( ~ $i(v0) | ~ individual(v0) | isa(v0, % 45.38/6.68 c_individual)) % 45.38/6.68 % 45.38/6.68 (just98) % 45.38/6.68 $i(c_collection) & ! [v0: $i] : ( ~ $i(v0) | ~ collection(v0) | isa(v0, % 45.38/6.68 c_collection)) % 45.38/6.68 % 45.38/6.68 (query40) % 45.38/6.69 $i(c_tptpcol_16_62187) & $i(c_translation_14) & % 45.38/6.69 $i(s_http_wwwthedailybulletincompostcardsmar9chtm) & ? [v0: $i] : ? [v1: $i] % 45.38/6.69 : ? [v2: $i] : (f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm) = v0 % 45.38/6.69 & f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 45.38/6.69 c_translation_14) = v2 & $i(v2) & $i(v1) & $i(v0) & mtvisible(v2) & % 45.38/6.69 tptpcol_15_109185(c_tptpcol_16_62187)) % 45.38/6.69 % 45.38/6.69 Further assumptions not needed in the proof: % 45.38/6.69 -------------------------------------------- % 45.38/6.69 just1, just100, just101, just104, just105, just106, just107, just108, just109, % 45.38/6.69 just11, just110, just112, just113, just115, just117, just118, just119, just12, % 45.38/6.69 just120, just121, just122, just123, just125, just126, just127, just128, just129, % 45.38/6.69 just130, just131, just132, just133, just134, just135, just136, just137, just138, % 45.38/6.69 just139, just14, just140, just141, just142, just143, just144, just145, just16, % 45.38/6.69 just19, just2, just21, just23, just25, just27, just29, just31, just33, just35, % 45.38/6.69 just37, just39, just4, just41, just43, just45, just47, just49, just5, just50, % 45.38/6.69 just51, just52, just53, just54, just55, just56, just57, just58, just59, just6, % 45.38/6.69 just60, just61, just63, just65, just67, just69, just7, just71, just73, just75, % 45.38/6.70 just77, just79, just8, just81, just83, just85, just87, just89, just9, just91, % 45.38/6.70 just92, just93, just95, just97, just99 % 45.38/6.70 % 45.38/6.70 Those formulas are unsatisfiable: % 45.38/6.70 --------------------------------- % 45.38/6.70 % 45.38/6.70 Begin of proof % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just3) implies: % 45.38/6.70 | (1) genls(c_firstordercollection, c_fixedordercollection) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just10) implies: % 45.38/6.70 | (2) disjointwith(c_collection, c_individual) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just13) implies: % 45.38/6.70 | (3) genls(c_fixedordercollection, c_collection) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just15) implies: % 45.38/6.70 | (4) genls(c_tptpcol_0_0, c_individual) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just17) implies: % 45.38/6.70 | (5) firstordercollection(c_tptpcol_16_62187) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just18) implies: % 45.38/6.70 | (6) genls(c_tptpcol_1_65536, c_tptpcol_0_0) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just20) implies: % 45.38/6.70 | (7) genls(c_tptpcol_2_98304, c_tptpcol_1_65536) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just22) implies: % 45.38/6.70 | (8) genls(c_tptpcol_3_98305, c_tptpcol_2_98304) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just24) implies: % 45.38/6.70 | (9) genls(c_tptpcol_4_106497, c_tptpcol_3_98305) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just26) implies: % 45.38/6.70 | (10) genls(c_tptpcol_5_106498, c_tptpcol_4_106497) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just28) implies: % 45.38/6.70 | (11) genls(c_tptpcol_6_108546, c_tptpcol_5_106498) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just30) implies: % 45.38/6.70 | (12) genls(c_tptpcol_7_108547, c_tptpcol_6_108546) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just32) implies: % 45.38/6.70 | (13) genls(c_tptpcol_8_109059, c_tptpcol_7_108547) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just34) implies: % 45.38/6.70 | (14) genls(c_tptpcol_9_109060, c_tptpcol_8_109059) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just36) implies: % 45.38/6.70 | (15) genls(c_tptpcol_10_109061, c_tptpcol_9_109060) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just38) implies: % 45.38/6.70 | (16) genls(c_tptpcol_11_109125, c_tptpcol_10_109061) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just40) implies: % 45.38/6.70 | (17) genls(c_tptpcol_12_109157, c_tptpcol_11_109125) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just42) implies: % 45.38/6.70 | (18) genls(c_tptpcol_13_109173, c_tptpcol_12_109157) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just44) implies: % 45.38/6.70 | (19) genls(c_tptpcol_14_109181, c_tptpcol_13_109173) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just46) implies: % 45.38/6.70 | (20) genls(c_tptpcol_15_109185, c_tptpcol_14_109181) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just62) implies: % 45.38/6.70 | (21) $i(c_tptpcol_15_109185) % 45.38/6.70 | (22) ! [v0: $i] : ( ~ $i(v0) | ~ tptpcol_15_109185(v0) | isa(v0, % 45.38/6.70 | c_tptpcol_15_109185)) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just64) implies: % 45.38/6.70 | (23) $i(c_tptpcol_14_109181) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just66) implies: % 45.38/6.70 | (24) $i(c_tptpcol_13_109173) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just68) implies: % 45.38/6.70 | (25) $i(c_tptpcol_12_109157) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just70) implies: % 45.38/6.70 | (26) $i(c_tptpcol_11_109125) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just72) implies: % 45.38/6.70 | (27) $i(c_tptpcol_10_109061) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just74) implies: % 45.38/6.70 | (28) $i(c_tptpcol_9_109060) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just76) implies: % 45.38/6.70 | (29) $i(c_tptpcol_8_109059) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just78) implies: % 45.38/6.70 | (30) $i(c_tptpcol_7_108547) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just80) implies: % 45.38/6.70 | (31) $i(c_tptpcol_6_108546) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just82) implies: % 45.38/6.70 | (32) $i(c_tptpcol_5_106498) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just84) implies: % 45.38/6.70 | (33) $i(c_tptpcol_4_106497) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just86) implies: % 45.38/6.70 | (34) $i(c_tptpcol_3_98305) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just88) implies: % 45.38/6.70 | (35) $i(c_tptpcol_2_98304) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just90) implies: % 45.38/6.70 | (36) $i(c_tptpcol_1_65536) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just94) implies: % 45.38/6.70 | (37) $i(c_tptpcol_0_0) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just96) implies: % 45.38/6.70 | (38) $i(c_individual) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just98) implies: % 45.38/6.70 | (39) $i(c_collection) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just114) implies: % 45.38/6.70 | (40) $i(c_fixedordercollection) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (just116) implies: % 45.38/6.70 | (41) $i(c_firstordercollection) % 45.38/6.70 | (42) ! [v0: $i] : ( ~ $i(v0) | ~ firstordercollection(v0) | isa(v0, % 45.38/6.70 | c_firstordercollection)) % 45.38/6.70 | % 45.38/6.70 | ALPHA: (query40) implies: % 45.38/6.70 | (43) $i(c_tptpcol_16_62187) % 45.38/6.70 | (44) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : % 45.38/6.70 | (f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm) = v0 & % 45.38/6.70 | f_urlreferentfn(v0) = v1 & f_contentmtofcdafromeventfn(v1, % 45.38/6.70 | c_translation_14) = v2 & $i(v2) & $i(v1) & $i(v0) & mtvisible(v2) % 45.38/6.70 | & tptpcol_15_109185(c_tptpcol_16_62187)) % 45.38/6.70 | % 45.38/6.71 | DELTA: instantiating (44) with fresh symbols all_119_0, all_119_1, all_119_2 % 45.38/6.71 | gives: % 45.38/6.71 | (45) f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm) = all_119_2 & % 45.38/6.71 | f_urlreferentfn(all_119_2) = all_119_1 & % 45.38/6.71 | f_contentmtofcdafromeventfn(all_119_1, c_translation_14) = all_119_0 & % 45.38/6.71 | $i(all_119_0) & $i(all_119_1) & $i(all_119_2) & mtvisible(all_119_0) & % 45.38/6.71 | tptpcol_15_109185(c_tptpcol_16_62187) % 45.38/6.71 | % 45.38/6.71 | ALPHA: (45) implies: % 45.38/6.71 | (46) tptpcol_15_109185(c_tptpcol_16_62187) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_fixedordercollection, % 45.38/6.71 | c_collection, c_firstordercollection, simplifying with (1), (3), % 45.38/6.71 | (39), (40), (41) gives: % 45.38/6.71 | (47) genls(c_firstordercollection, c_collection) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_1_65536, c_tptpcol_0_0, % 45.38/6.71 | c_tptpcol_2_98304, simplifying with (6), (7), (35), (36), (37) % 45.38/6.71 | gives: % 45.38/6.71 | (48) genls(c_tptpcol_2_98304, c_tptpcol_0_0) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_3_98305, % 45.38/6.71 | c_tptpcol_2_98304, c_tptpcol_4_106497, simplifying with (8), (9), % 45.38/6.71 | (33), (34), (35) gives: % 45.38/6.71 | (49) genls(c_tptpcol_4_106497, c_tptpcol_2_98304) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_5_106498, % 45.38/6.71 | c_tptpcol_4_106497, c_tptpcol_6_108546, simplifying with (10), % 45.38/6.71 | (11), (31), (32), (33) gives: % 45.38/6.71 | (50) genls(c_tptpcol_6_108546, c_tptpcol_4_106497) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_7_108547, % 45.38/6.71 | c_tptpcol_6_108546, c_tptpcol_8_109059, simplifying with (12), % 45.38/6.71 | (13), (29), (30), (31) gives: % 45.38/6.71 | (51) genls(c_tptpcol_8_109059, c_tptpcol_6_108546) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_9_109060, % 45.38/6.71 | c_tptpcol_8_109059, c_tptpcol_10_109061, simplifying with (14), % 45.38/6.71 | (15), (27), (28), (29) gives: % 45.38/6.71 | (52) genls(c_tptpcol_10_109061, c_tptpcol_8_109059) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_11_109125, % 45.38/6.71 | c_tptpcol_10_109061, c_tptpcol_12_109157, simplifying with (16), % 45.38/6.71 | (17), (25), (26), (27) gives: % 45.38/6.71 | (53) genls(c_tptpcol_12_109157, c_tptpcol_10_109061) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_13_109173, % 45.38/6.71 | c_tptpcol_12_109157, c_tptpcol_14_109181, simplifying with (18), % 45.38/6.71 | (19), (23), (24), (25) gives: % 45.38/6.71 | (54) genls(c_tptpcol_14_109181, c_tptpcol_12_109157) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (42) with c_tptpcol_16_62187, simplifying with (5), % 45.38/6.71 | (43) gives: % 45.38/6.71 | (55) isa(c_tptpcol_16_62187, c_firstordercollection) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just102) with c_collection, c_individual, % 45.38/6.71 | c_tptpcol_0_0, simplifying with (2), (4), (37), (38), (39) gives: % 45.38/6.71 | (56) disjointwith(c_collection, c_tptpcol_0_0) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (22) with c_tptpcol_16_62187, simplifying with % 45.38/6.71 | (43), (46) gives: % 45.38/6.71 | (57) isa(c_tptpcol_16_62187, c_tptpcol_15_109185) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_2_98304, c_tptpcol_0_0, % 45.38/6.71 | c_tptpcol_4_106497, simplifying with (33), (35), (37), (48), (49) % 45.38/6.71 | gives: % 45.38/6.71 | (58) genls(c_tptpcol_4_106497, c_tptpcol_0_0) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_6_108546, % 45.38/6.71 | c_tptpcol_4_106497, c_tptpcol_8_109059, simplifying with (29), % 45.38/6.71 | (31), (33), (50), (51) gives: % 45.38/6.71 | (59) genls(c_tptpcol_8_109059, c_tptpcol_4_106497) % 45.38/6.71 | % 45.38/6.71 | GROUND_INST: instantiating (just124) with c_tptpcol_10_109061, % 45.38/6.71 | c_tptpcol_8_109059, c_tptpcol_12_109157, simplifying with (25), % 45.38/6.71 | (27), (29), (52), (53) gives: % 45.38/6.72 | (60) genls(c_tptpcol_12_109157, c_tptpcol_8_109059) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just103) with c_collection, c_tptpcol_0_0, % 45.38/6.72 | c_firstordercollection, simplifying with (37), (39), (41), (47), % 45.38/6.72 | (56) gives: % 45.38/6.72 | (61) disjointwith(c_firstordercollection, c_tptpcol_0_0) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just111) with c_tptpcol_16_62187, % 45.38/6.72 | c_tptpcol_15_109185, c_tptpcol_14_109181, simplifying with (20), % 45.38/6.72 | (21), (23), (43), (57) gives: % 45.38/6.72 | (62) isa(c_tptpcol_16_62187, c_tptpcol_14_109181) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just102) with c_firstordercollection, % 45.38/6.72 | c_tptpcol_0_0, c_tptpcol_4_106497, simplifying with (33), (37), % 45.38/6.72 | (41), (58), (61) gives: % 45.38/6.72 | (63) disjointwith(c_firstordercollection, c_tptpcol_4_106497) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just111) with c_tptpcol_16_62187, % 45.38/6.72 | c_tptpcol_14_109181, c_tptpcol_12_109157, simplifying with (23), % 45.38/6.72 | (25), (43), (54), (62) gives: % 45.38/6.72 | (64) isa(c_tptpcol_16_62187, c_tptpcol_12_109157) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just102) with c_firstordercollection, % 45.38/6.72 | c_tptpcol_4_106497, c_tptpcol_8_109059, simplifying with (29), % 45.38/6.72 | (33), (41), (59), (63) gives: % 45.38/6.72 | (65) disjointwith(c_firstordercollection, c_tptpcol_8_109059) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just111) with c_tptpcol_16_62187, % 45.38/6.72 | c_tptpcol_12_109157, c_tptpcol_8_109059, simplifying with (25), % 45.38/6.72 | (29), (43), (60), (64) gives: % 45.38/6.72 | (66) isa(c_tptpcol_16_62187, c_tptpcol_8_109059) % 45.38/6.72 | % 45.38/6.72 | GROUND_INST: instantiating (just48) with c_tptpcol_16_62187, % 45.38/6.72 | c_firstordercollection, c_tptpcol_8_109059, simplifying with % 45.38/6.72 | (29), (41), (43), (55), (65), (66) gives: % 45.38/6.72 | (67) $false % 45.38/6.72 | % 45.38/6.72 | CLOSE: (67) is inconsistent. % 45.38/6.72 | % 45.38/6.72 End of proof % 45.38/6.72 % SZS output end Proof for theBenchmark % 45.38/6.72 % 45.38/6.72 6140ms %------------------------------------------------------------------------------