%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : CSR063+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 : n011.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:37:03 EDT 2023 % Result : Theorem 18.95s 3.28s % Output : Proof 23.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR063+1 : TPTP v8.1.2. Released v3.4.0. % 0.07/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon Aug 28 10:52:55 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.61 ________ _____ % 0.19/0.61 ___ __ \_________(_)________________________________ % 0.19/0.61 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.61 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.61 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.61 % 0.19/0.61 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.61 (2023-06-19) % 0.19/0.61 % 0.19/0.61 (c) Philipp Rümmer, 2009-2023 % 0.19/0.61 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.61 Amanda Stjerna. % 0.19/0.61 Free software under BSD-3-Clause. % 0.19/0.61 % 0.19/0.61 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.61 % 0.19/0.61 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.63 Running up to 7 provers in parallel. % 0.19/0.64 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.64 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.64 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.64 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.64 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.64 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.19/0.64 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 3.68/1.21 Prover 1: Preprocessing ... % 3.68/1.21 Prover 4: Preprocessing ... % 3.68/1.24 Prover 6: Preprocessing ... % 3.68/1.24 Prover 3: Preprocessing ... % 3.68/1.24 Prover 5: Preprocessing ... % 3.68/1.24 Prover 2: Preprocessing ... % 3.68/1.24 Prover 0: Preprocessing ... % 8.06/1.84 Prover 2: Proving ... % 8.06/1.86 Prover 5: Proving ... % 8.06/1.98 Prover 6: Constructing countermodel ... % 9.19/2.07 Prover 3: Constructing countermodel ... % 9.19/2.09 Prover 1: Constructing countermodel ... % 10.91/2.25 Prover 0: Proving ... % 10.91/2.27 Prover 4: Constructing countermodel ... % 12.23/2.41 Prover 3: gave up % 12.23/2.41 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 13.03/2.52 Prover 1: gave up % 13.03/2.52 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 13.03/2.55 Prover 7: Preprocessing ... % 13.56/2.63 Prover 8: Preprocessing ... % 14.65/2.73 Prover 6: gave up % 14.65/2.73 Prover 9: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1423531889 % 14.65/2.77 Prover 7: Constructing countermodel ... % 15.29/2.82 Prover 9: Preprocessing ... % 15.89/2.89 Prover 8: Warning: ignoring some quantifiers % 15.89/2.91 Prover 8: Constructing countermodel ... % 18.18/3.22 Prover 9: Constructing countermodel ... % 18.95/3.28 Prover 0: proved (2645ms) % 18.95/3.28 % 18.95/3.28 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 18.95/3.28 % 18.95/3.28 Prover 8: gave up % 18.95/3.28 Prover 9: stopped % 18.95/3.29 Prover 2: stopped % 18.95/3.30 Prover 5: stopped % 18.95/3.31 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 18.95/3.31 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 18.95/3.31 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 18.95/3.31 Prover 16: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=completeFrugal -randomSeed=-2043353683 % 18.95/3.31 Prover 19: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=-1780594085 % 19.43/3.37 Prover 19: Preprocessing ... % 19.43/3.39 Prover 13: Preprocessing ... % 19.74/3.39 Prover 10: Preprocessing ... % 19.88/3.41 Prover 16: Preprocessing ... % 19.88/3.41 Prover 11: Preprocessing ... % 20.63/3.53 Prover 16: Warning: ignoring some quantifiers % 20.63/3.53 Prover 10: Constructing countermodel ... % 20.63/3.55 Prover 16: Constructing countermodel ... % 20.63/3.56 Prover 13: Warning: ignoring some quantifiers % 20.63/3.57 Prover 13: Constructing countermodel ... % 21.36/3.66 Prover 19: Warning: ignoring some quantifiers % 21.36/3.67 Prover 19: Constructing countermodel ... % 22.23/3.76 Prover 11: Constructing countermodel ... % 23.33/3.90 Prover 10: Found proof (size 42) % 23.33/3.90 Prover 10: proved (614ms) % 23.33/3.90 Prover 13: stopped % 23.33/3.90 Prover 7: stopped % 23.33/3.90 Prover 16: stopped % 23.33/3.90 Prover 4: stopped % 23.33/3.90 Prover 19: stopped % 23.33/3.90 Prover 11: stopped % 23.33/3.90 % 23.33/3.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 23.33/3.90 % 23.33/3.91 % SZS output start Proof for theBenchmark % 23.33/3.92 Assumptions after simplification: % 23.33/3.92 --------------------------------- % 23.33/3.92 % 23.33/3.92 (just1) % 23.33/3.92 $i(c_mathematicalthing) & $i(c_setorcollection) & genls(c_setorcollection, % 23.33/3.93 c_mathematicalthing) % 23.33/3.93 % 23.33/3.93 (just10) % 23.33/3.93 $i(c_mathematicalorcomputationalthing) & $i(c_mathematicalthing) & % 23.33/3.93 genls(c_mathematicalthing, c_mathematicalorcomputationalthing) % 23.33/3.93 % 23.33/3.93 (just100) % 23.33/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.93 ~ isa(v0, v1) | ~ genls(v1, v2) | isa(v0, v2)) % 23.33/3.93 % 23.33/3.93 (just103) % 23.33/3.93 $i(c_mathematicalthing) & ! [v0: $i] : ( ~ $i(v0) | ~ mathematicalthing(v0) % 23.33/3.93 | isa(v0, c_mathematicalthing)) % 23.33/3.93 % 23.33/3.93 (just105) % 23.33/3.93 $i(c_setorcollection) & ! [v0: $i] : ( ~ $i(v0) | ~ setorcollection(v0) | % 23.33/3.93 isa(v0, c_setorcollection)) % 23.33/3.93 % 23.33/3.93 (just113) % 23.33/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.93 ~ genls(v2, v0) | ~ genls(v0, v1) | genls(v2, v1)) % 23.33/3.93 % 23.33/3.93 (just13) % 23.33/3.93 $i(c_inanimateobject_nonnatural) & $i(c_artifact) & genls(c_artifact, % 23.33/3.93 c_inanimateobject_nonnatural) % 23.33/3.93 % 23.33/3.93 (just15) % 23.33/3.93 $i(c_inanimateobject) & $i(c_inanimateobject_nonnatural) & % 23.33/3.93 genls(c_inanimateobject_nonnatural, c_inanimateobject) % 23.33/3.93 % 23.33/3.93 (just17) % 23.33/3.93 $i(c_inanimateobject) & $i(c_partiallytangible) & genls(c_inanimateobject, % 23.33/3.93 c_partiallytangible) % 23.33/3.93 % 23.33/3.93 (just19) % 23.33/3.93 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.94 ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 23.33/3.94 % 23.33/3.94 (just22) % 23.33/3.94 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ disjointwith(v0, v1) | % 23.33/3.94 no(v0, v1)) % 23.33/3.94 % 23.33/3.94 (just26) % 23.33/3.94 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.94 ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 23.33/3.94 % 23.33/3.94 (just3) % 23.33/3.96 $i(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) & ? [v0: % 23.33/3.96 $i] : ? [v1: $i] : % 23.33/3.96 (f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) = v0 % 23.33/3.96 & f_urlreferentfn(v0) = v1 & $i(v1) & $i(v0) & computerdataartifact(v1)) % 23.33/3.96 % 23.33/3.96 (just30) % 23.33/3.96 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.96 ~ isa(v0, v2) | ~ isa(v0, v1) | ~ disjointwith(v1, v2)) % 23.33/3.96 % 23.33/3.96 (just4) % 23.33/3.96 $i(c_intangible) & $i(c_mathematicalorcomputationalthing) & % 23.33/3.96 genls(c_mathematicalorcomputationalthing, c_intangible) % 23.33/3.96 % 23.33/3.96 (just44) % 23.33/3.97 ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ no(v0, v1) | % 23.33/3.97 setorcollection(v0)) % 23.33/3.97 % 23.33/3.97 (just6) % 23.33/3.97 $i(c_partiallytangible) & $i(c_intangible) & disjointwith(c_intangible, % 23.33/3.97 c_partiallytangible) % 23.33/3.97 % 23.33/3.97 (just64) % 23.33/3.97 $i(c_inanimateobject) & ! [v0: $i] : ( ~ $i(v0) | ~ inanimateobject(v0) | % 23.33/3.97 isa(v0, c_inanimateobject)) % 23.33/3.97 % 23.33/3.97 (just66) % 23.33/3.97 $i(c_inanimateobject_nonnatural) & ! [v0: $i] : ( ~ $i(v0) | ~ % 23.33/3.97 inanimateobject_nonnatural(v0) | isa(v0, c_inanimateobject_nonnatural)) % 23.33/3.97 % 23.33/3.97 (just76) % 23.33/3.97 $i(c_artifact) & ! [v0: $i] : ( ~ $i(v0) | ~ artifact(v0) | isa(v0, % 23.33/3.97 c_artifact)) % 23.33/3.97 % 23.33/3.97 (just78) % 23.33/3.97 $i(c_partiallytangible) & ! [v0: $i] : ( ~ $i(v0) | ~ partiallytangible(v0) % 23.33/3.97 | isa(v0, c_partiallytangible)) % 23.33/3.97 % 23.33/3.97 (just8) % 23.33/3.97 $i(c_artifact) & $i(c_computerdataartifact) & genls(c_computerdataartifact, % 23.33/3.97 c_artifact) % 23.33/3.97 % 23.33/3.97 (just82) % 23.33/3.97 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.97 ~ disjointwith(v0, v1) | ~ genls(v2, v1) | disjointwith(v0, v2)) % 23.33/3.97 % 23.33/3.97 (just83) % 23.33/3.97 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 23.33/3.97 ~ disjointwith(v0, v1) | ~ genls(v2, v0) | disjointwith(v2, v1)) % 23.33/3.97 % 23.33/3.97 (just85) % 23.33/3.97 $i(c_intangible) & ! [v0: $i] : ( ~ $i(v0) | ~ intangible(v0) | isa(v0, % 23.33/3.97 c_intangible)) % 23.33/3.97 % 23.33/3.97 (just87) % 23.33/3.97 $i(c_mathematicalorcomputationalthing) & ! [v0: $i] : ( ~ $i(v0) | ~ % 23.33/3.97 mathematicalorcomputationalthing(v0) | isa(v0, % 23.33/3.97 c_mathematicalorcomputationalthing)) % 23.33/3.97 % 23.33/3.97 (just89) % 23.33/3.97 $i(c_computerdataartifact) & ! [v0: $i] : ( ~ $i(v0) | ~ % 23.33/3.97 computerdataartifact(v0) | isa(v0, c_computerdataartifact)) % 23.33/3.97 % 23.33/3.97 (query63) % 23.33/3.97 $i(c_tptpcol_16_118949) & % 23.33/3.97 $i(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) & ? [v0: % 23.33/3.97 $i] : ? [v1: $i] : % 23.33/3.97 (f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) = v0 % 23.33/3.97 & f_urlreferentfn(v0) = v1 & $i(v1) & $i(v0) & disjointwith(v1, % 23.33/3.97 c_tptpcol_16_118949)) % 23.33/3.97 % 23.33/3.97 (function-axioms) % 23.94/3.98 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_urlfn(v2) = v1) | % 23.94/3.98 ~ (f_urlfn(v2) = v0)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | % 23.94/3.98 ~ (f_urlreferentfn(v2) = v1) | ~ (f_urlreferentfn(v2) = v0)) % 23.94/3.98 % 23.94/3.98 Further assumptions not needed in the proof: % 23.94/3.98 -------------------------------------------- % 23.94/3.98 just101, just102, just104, just106, just107, just108, just109, just11, just110, % 23.94/3.98 just111, just112, just114, just115, just12, just14, just16, just18, just2, % 23.94/3.98 just20, just21, just23, just24, just25, just27, just28, just29, just31, just32, % 23.94/3.98 just33, just34, just35, just36, just37, just38, just39, just40, just41, just42, % 23.94/3.98 just43, just45, just46, just47, just48, just49, just5, just50, just51, just52, % 23.94/3.98 just53, just54, just55, just56, just57, just58, just59, just60, just61, just62, % 23.94/3.98 just63, just65, just67, just68, just69, just7, just70, just71, just72, just73, % 23.94/3.98 just74, just75, just77, just79, just80, just81, just84, just86, just88, just9, % 23.94/3.98 just90, just91, just92, just93, just94, just95, just96, just97, just98, just99 % 23.94/3.98 % 23.94/3.98 Those formulas are unsatisfiable: % 23.94/3.98 --------------------------------- % 23.94/3.98 % 23.94/3.98 Begin of proof % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just1) implies: % 23.94/3.98 | (1) genls(c_setorcollection, c_mathematicalthing) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just3) implies: % 23.94/3.98 | (2) ? [v0: $i] : ? [v1: $i] : % 23.94/3.98 | (f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/3.98 | = v0 & f_urlreferentfn(v0) = v1 & $i(v1) & $i(v0) & % 23.94/3.98 | computerdataartifact(v1)) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just4) implies: % 23.94/3.98 | (3) genls(c_mathematicalorcomputationalthing, c_intangible) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just6) implies: % 23.94/3.98 | (4) disjointwith(c_intangible, c_partiallytangible) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just8) implies: % 23.94/3.98 | (5) genls(c_computerdataartifact, c_artifact) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just10) implies: % 23.94/3.98 | (6) genls(c_mathematicalthing, c_mathematicalorcomputationalthing) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just13) implies: % 23.94/3.98 | (7) genls(c_artifact, c_inanimateobject_nonnatural) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just15) implies: % 23.94/3.98 | (8) genls(c_inanimateobject_nonnatural, c_inanimateobject) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just17) implies: % 23.94/3.98 | (9) genls(c_inanimateobject, c_partiallytangible) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just64) implies: % 23.94/3.98 | (10) $i(c_inanimateobject) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just66) implies: % 23.94/3.98 | (11) $i(c_inanimateobject_nonnatural) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just76) implies: % 23.94/3.98 | (12) $i(c_artifact) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just78) implies: % 23.94/3.98 | (13) $i(c_partiallytangible) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just85) implies: % 23.94/3.98 | (14) $i(c_intangible) % 23.94/3.98 | % 23.94/3.98 | ALPHA: (just87) implies: % 23.94/3.99 | (15) $i(c_mathematicalorcomputationalthing) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (just89) implies: % 23.94/3.99 | (16) $i(c_computerdataartifact) % 23.94/3.99 | (17) ! [v0: $i] : ( ~ $i(v0) | ~ computerdataartifact(v0) | isa(v0, % 23.94/3.99 | c_computerdataartifact)) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (just103) implies: % 23.94/3.99 | (18) $i(c_mathematicalthing) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (just105) implies: % 23.94/3.99 | (19) $i(c_setorcollection) % 23.94/3.99 | (20) ! [v0: $i] : ( ~ $i(v0) | ~ setorcollection(v0) | isa(v0, % 23.94/3.99 | c_setorcollection)) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (query63) implies: % 23.94/3.99 | (21) $i(c_tptpcol_16_118949) % 23.94/3.99 | (22) ? [v0: $i] : ? [v1: $i] : % 23.94/3.99 | (f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/3.99 | = v0 & f_urlreferentfn(v0) = v1 & $i(v1) & $i(v0) & disjointwith(v1, % 23.94/3.99 | c_tptpcol_16_118949)) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (function-axioms) implies: % 23.94/3.99 | (23) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ % 23.94/3.99 | (f_urlreferentfn(v2) = v1) | ~ (f_urlreferentfn(v2) = v0)) % 23.94/3.99 | (24) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : (v1 = v0 | ~ (f_urlfn(v2) = % 23.94/3.99 | v1) | ~ (f_urlfn(v2) = v0)) % 23.94/3.99 | % 23.94/3.99 | DELTA: instantiating (2) with fresh symbols all_103_0, all_103_1 gives: % 23.94/3.99 | (25) f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/3.99 | = all_103_1 & f_urlreferentfn(all_103_1) = all_103_0 & $i(all_103_0) & % 23.94/3.99 | $i(all_103_1) & computerdataartifact(all_103_0) % 23.94/3.99 | % 23.94/3.99 | ALPHA: (25) implies: % 23.94/3.99 | (26) computerdataartifact(all_103_0) % 23.94/3.99 | (27) f_urlreferentfn(all_103_1) = all_103_0 % 23.94/3.99 | (28) f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/3.99 | = all_103_1 % 23.94/3.99 | % 23.94/3.99 | DELTA: instantiating (22) with fresh symbols all_105_0, all_105_1 gives: % 23.94/3.99 | (29) f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/4.00 | = all_105_1 & f_urlreferentfn(all_105_1) = all_105_0 & $i(all_105_0) & % 23.94/4.00 | $i(all_105_1) & disjointwith(all_105_0, c_tptpcol_16_118949) % 23.94/4.00 | % 23.94/4.00 | ALPHA: (29) implies: % 23.94/4.00 | (30) disjointwith(all_105_0, c_tptpcol_16_118949) % 23.94/4.00 | (31) $i(all_105_0) % 23.94/4.00 | (32) f_urlreferentfn(all_105_1) = all_105_0 % 23.94/4.00 | (33) f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf) % 23.94/4.00 | = all_105_1 % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (24) with all_103_1, all_105_1, % 23.94/4.00 | s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf, % 23.94/4.00 | simplifying with (28), (33) gives: % 23.94/4.00 | (34) all_105_1 = all_103_1 % 23.94/4.00 | % 23.94/4.00 | REDUCE: (32), (34) imply: % 23.94/4.00 | (35) f_urlreferentfn(all_103_1) = all_105_0 % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (23) with all_103_0, all_105_0, all_103_1, % 23.94/4.00 | simplifying with (27), (35) gives: % 23.94/4.00 | (36) all_105_0 = all_103_0 % 23.94/4.00 | % 23.94/4.00 | REDUCE: (31), (36) imply: % 23.94/4.00 | (37) $i(all_103_0) % 23.94/4.00 | % 23.94/4.00 | REDUCE: (30), (36) imply: % 23.94/4.00 | (38) disjointwith(all_103_0, c_tptpcol_16_118949) % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (just113) with c_mathematicalthing, % 23.94/4.00 | c_mathematicalorcomputationalthing, c_setorcollection, % 23.94/4.00 | simplifying with (1), (6), (15), (18), (19) gives: % 23.94/4.00 | (39) genls(c_setorcollection, c_mathematicalorcomputationalthing) % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (just113) with c_artifact, % 23.94/4.00 | c_inanimateobject_nonnatural, c_computerdataartifact, simplifying % 23.94/4.00 | with (5), (7), (11), (12), (16) gives: % 23.94/4.00 | (40) genls(c_computerdataartifact, c_inanimateobject_nonnatural) % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (17) with all_103_0, simplifying with (26), (37) % 23.94/4.00 | gives: % 23.94/4.00 | (41) isa(all_103_0, c_computerdataartifact) % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (just82) with c_intangible, c_partiallytangible, % 23.94/4.00 | c_inanimateobject, simplifying with (4), (9), (10), (13), (14) % 23.94/4.00 | gives: % 23.94/4.00 | (42) disjointwith(c_intangible, c_inanimateobject) % 23.94/4.00 | % 23.94/4.00 | GROUND_INST: instantiating (just22) with all_103_0, c_tptpcol_16_118949, % 23.94/4.00 | simplifying with (21), (37), (38) gives: % 23.94/4.00 | (43) no(all_103_0, c_tptpcol_16_118949) % 23.94/4.00 | % 23.94/4.01 | GROUND_INST: instantiating (just83) with c_intangible, c_inanimateobject, % 23.94/4.01 | c_mathematicalorcomputationalthing, simplifying with (3), (10), % 23.94/4.01 | (14), (15), (42) gives: % 23.94/4.01 | (44) disjointwith(c_mathematicalorcomputationalthing, c_inanimateobject) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (just100) with all_103_0, c_computerdataartifact, % 23.94/4.01 | c_inanimateobject_nonnatural, simplifying with (11), (16), (37), % 23.94/4.01 | (40), (41) gives: % 23.94/4.01 | (45) isa(all_103_0, c_inanimateobject_nonnatural) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (just44) with all_103_0, c_tptpcol_16_118949, % 23.94/4.01 | simplifying with (21), (37), (43) gives: % 23.94/4.01 | (46) setorcollection(all_103_0) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (20) with all_103_0, simplifying with (37), (46) % 23.94/4.01 | gives: % 23.94/4.01 | (47) isa(all_103_0, c_setorcollection) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (just83) with c_mathematicalorcomputationalthing, % 23.94/4.01 | c_inanimateobject, c_setorcollection, simplifying with (10), % 23.94/4.01 | (15), (19), (39), (44) gives: % 23.94/4.01 | (48) disjointwith(c_setorcollection, c_inanimateobject) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (just100) with all_103_0, % 23.94/4.01 | c_inanimateobject_nonnatural, c_inanimateobject, simplifying with % 23.94/4.01 | (8), (10), (11), (37), (45) gives: % 23.94/4.01 | (49) isa(all_103_0, c_inanimateobject) % 23.94/4.01 | % 23.94/4.01 | GROUND_INST: instantiating (just30) with all_103_0, c_setorcollection, % 23.94/4.01 | c_inanimateobject, simplifying with (10), (19), (37), (47), (48), % 23.94/4.01 | (49) gives: % 23.94/4.01 | (50) $false % 23.94/4.01 | % 23.94/4.01 | CLOSE: (50) is inconsistent. % 23.94/4.01 | % 23.94/4.01 End of proof % 23.94/4.01 % SZS output end Proof for theBenchmark % 23.94/4.01 % 23.94/4.01 3397ms %------------------------------------------------------------------------------