%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWB013+2 : TPTP v8.1.2. Released v5.2.0. % Transfm : none % Format : tptp % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % Computer : n006.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 : Thu Aug 31 20:11:41 EDT 2023 % Result : Theorem 10.48s 2.11s % Output : Proof 16.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB013+2 : TPTP v8.1.2. Released v5.2.0. % 0.12/0.13 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.13/0.34 % Computer : n006.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 : Sun Aug 27 07:17:22 EDT 2023 % 0.13/0.34 % CPUTime : % 0.19/0.58 ________ _____ % 0.19/0.58 ___ __ \_________(_)________________________________ % 0.19/0.58 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.19/0.58 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.19/0.58 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.19/0.58 (2023-06-19) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2023 % 0.19/0.58 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.19/0.58 Amanda Stjerna. % 0.19/0.58 Free software under BSD-3-Clause. % 0.19/0.58 % 0.19/0.58 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.19/0.59 Running up to 7 provers in parallel. % 0.19/0.60 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.19/0.60 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 0.19/0.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.19/0.60 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.19/0.60 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.19/0.60 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.19/0.60 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 2.60/0.99 Prover 1: Preprocessing ... % 2.60/0.99 Prover 4: Preprocessing ... % 2.60/1.03 Prover 6: Preprocessing ... % 2.60/1.03 Prover 0: Preprocessing ... % 2.60/1.03 Prover 5: Preprocessing ... % 2.60/1.03 Prover 2: Preprocessing ... % 2.60/1.03 Prover 3: Preprocessing ... % 4.21/1.31 Prover 5: Proving ... % 4.21/1.34 Prover 2: Proving ... % 5.44/1.46 Prover 3: Constructing countermodel ... % 5.44/1.46 Prover 6: Proving ... % 5.44/1.48 Prover 1: Constructing countermodel ... % 9.16/2.09 Prover 4: Constructing countermodel ... % 9.16/2.11 Prover 3: proved (1510ms) % 9.16/2.11 % 10.48/2.11 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.48/2.11 % 10.48/2.11 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 10.48/2.12 Prover 5: stopped % 10.48/2.13 Prover 6: stopped % 10.48/2.14 Prover 7: Preprocessing ... % 10.48/2.14 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 10.48/2.14 Prover 10: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=919308125 % 10.48/2.17 Prover 2: stopped % 10.48/2.18 Prover 8: Preprocessing ... % 10.48/2.18 Prover 10: Preprocessing ... % 10.48/2.18 Prover 11: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1509710984 % 11.27/2.20 Prover 7: Warning: ignoring some quantifiers % 11.31/2.21 Prover 7: Constructing countermodel ... % 11.31/2.23 Prover 0: Proving ... % 11.31/2.23 Prover 11: Preprocessing ... % 11.31/2.23 Prover 10: Warning: ignoring some quantifiers % 11.31/2.24 Prover 0: stopped % 11.31/2.24 Prover 13: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=complete -randomSeed=1138197443 % 11.31/2.25 Prover 10: Constructing countermodel ... % 11.31/2.26 Prover 13: Preprocessing ... % 12.06/2.33 Prover 13: Warning: ignoring some quantifiers % 12.06/2.33 Prover 13: Constructing countermodel ... % 12.06/2.36 Prover 8: Warning: ignoring some quantifiers % 12.06/2.37 Prover 8: Constructing countermodel ... % 15.04/2.87 Prover 10: Found proof (size 23) % 15.04/2.87 Prover 10: proved (726ms) % 15.04/2.87 Prover 7: stopped % 15.04/2.87 Prover 13: stopped % 15.04/2.87 Prover 4: stopped % 15.04/2.87 Prover 8: stopped % 15.04/2.89 Prover 11: Constructing countermodel ... % 15.04/2.89 Prover 1: stopped % 15.04/2.90 Prover 11: stopped % 15.04/2.90 % 15.04/2.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.04/2.90 % 15.04/2.90 % SZS output start Proof for theBenchmark % 15.04/2.90 Assumptions after simplification: % 15.04/2.90 --------------------------------- % 15.04/2.90 % 15.04/2.90 (owl_chain_003) % 16.63/2.92 $i(uri_owl_propertyChainAxiom) & $i(uri_rdf_nil) & $i(uri_rdf_rest) & % 16.63/2.92 $i(uri_rdf_first) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 16.63/2.92 [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] % 16.63/2.92 : ! [v10: $i] : ( ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ $i(v6) | % 16.63/2.92 ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.92 iext(v6, v9, v10) | ~ iext(v4, v8, v9) | ~ iext(v2, v7, v8) | ~ % 16.63/2.92 iext(uri_owl_propertyChainAxiom, v0, v1) | ~ iext(uri_rdf_rest, v5, % 16.63/2.92 uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ iext(uri_rdf_rest, v1, % 16.63/2.92 v3) | ~ iext(uri_rdf_first, v5, v6) | ~ iext(uri_rdf_first, v3, v4) | ~ % 16.63/2.92 iext(uri_rdf_first, v1, v2) | iext(v0, v7, v10)) & ! [v0: $i] : ! [v1: $i] % 16.63/2.92 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ % 16.63/2.92 $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 16.63/2.92 $i(v0) | ~ ip(v6) | ~ ip(v4) | ~ ip(v2) | ~ ip(v0) | ~ % 16.63/2.92 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 16.63/2.92 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 16.63/2.93 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 16.63/2.93 iext(uri_owl_propertyChainAxiom, v0, v1) | ? [v7: $i] : ? [v8: $i] : ? % 16.63/2.93 [v9: $i] : ? [v10: $i] : ($i(v10) & $i(v9) & $i(v8) & $i(v7) & iext(v6, v9, % 16.63/2.93 v10) & iext(v4, v8, v9) & iext(v2, v7, v8) & ~ iext(v0, v7, v10))) & ! % 16.63/2.93 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 16.63/2.93 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 16.63/2.93 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_propertyChainAxiom, v0, v1) | ~ % 16.63/2.93 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 16.63/2.93 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 16.63/2.93 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ip(v6)) & ! % 16.63/2.93 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 16.63/2.93 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 16.63/2.93 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_propertyChainAxiom, v0, v1) | ~ % 16.63/2.93 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 16.63/2.93 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 16.63/2.93 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ip(v4)) & ! % 16.63/2.93 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 16.63/2.93 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 16.63/2.93 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_propertyChainAxiom, v0, v1) | ~ % 16.63/2.93 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 16.63/2.93 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 16.63/2.93 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ip(v2)) & ! % 16.63/2.93 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 16.63/2.93 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 16.63/2.93 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_propertyChainAxiom, v0, v1) | ~ % 16.63/2.93 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 16.63/2.93 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 16.63/2.93 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ip(v0)) % 16.63/2.93 % 16.63/2.93 (owl_eqdis_sameas) % 16.63/2.93 $i(uri_owl_sameAs) & ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ % 16.63/2.93 $i(v0) | ~ iext(uri_owl_sameAs, v0, v1)) & ? [v0: $i] : ( ~ $i(v0) | % 16.63/2.93 iext(uri_owl_sameAs, v0, v0)) % 16.63/2.93 % 16.63/2.93 (owl_inv) % 16.63/2.93 $i(uri_owl_inverseOf) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 16.63/2.93 : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(v1, v3, v2) | ~ % 16.63/2.93 iext(uri_owl_inverseOf, v0, v1) | iext(v0, v2, v3)) & ! [v0: $i] : ! [v1: % 16.63/2.93 $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ % 16.63/2.93 $i(v0) | ~ iext(v0, v2, v3) | ~ iext(uri_owl_inverseOf, v0, v1) | iext(v1, % 16.63/2.93 v3, v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ ip(v1) % 16.63/2.93 | ~ ip(v0) | iext(uri_owl_inverseOf, v0, v1) | ? [v2: $i] : ? [v3: $i] : % 16.63/2.93 ($i(v3) & $i(v2) & ( ~ iext(v1, v3, v2) | ~ iext(v0, v2, v3)) & (iext(v1, % 16.63/2.93 v3, v2) | iext(v0, v2, v3)))) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) % 16.63/2.93 | ~ $i(v0) | ~ iext(uri_owl_inverseOf, v0, v1) | ip(v1)) & ! [v0: $i] : % 16.63/2.93 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_inverseOf, v0, v1) | % 16.63/2.93 ip(v0)) % 16.63/2.93 % 16.63/2.93 (owl_rdfsext_subclassof) % 16.63/2.93 $i(uri_rdfs_subClassOf) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) % 16.63/2.93 | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, v2) | ~ iext(uri_rdfs_subClassOf, % 16.63/2.93 v0, v1) | icext(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 16.63/2.93 $i(v0) | ~ ic(v1) | ~ ic(v0) | iext(uri_rdfs_subClassOf, v0, v1) | ? [v2: % 16.63/2.93 $i] : ($i(v2) & icext(v0, v2) & ~ icext(v1, v2))) & ! [v0: $i] : ! [v1: % 16.63/2.93 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ iext(uri_rdfs_subClassOf, v0, v1) | % 16.63/2.93 ic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.93 iext(uri_rdfs_subClassOf, v0, v1) | ic(v0)) % 16.63/2.93 % 16.63/2.93 (owl_rdfsext_subpropertyof) % 16.63/2.94 $i(uri_rdfs_subPropertyOf) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: % 16.63/2.94 $i] : ( ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(v0, v2, v3) | % 16.63/2.94 ~ iext(uri_rdfs_subPropertyOf, v0, v1) | iext(v1, v2, v3)) & ! [v0: $i] : % 16.63/2.94 ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ ip(v1) | ~ ip(v0) | % 16.63/2.94 iext(uri_rdfs_subPropertyOf, v0, v1) | ? [v2: $i] : ? [v3: $i] : ($i(v3) & % 16.63/2.94 $i(v2) & iext(v0, v2, v3) & ~ iext(v1, v2, v3))) & ! [v0: $i] : ! [v1: % 16.63/2.94 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ iext(uri_rdfs_subPropertyOf, v0, v1) | % 16.63/2.94 ip(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.94 iext(uri_rdfs_subPropertyOf, v0, v1) | ip(v0)) % 16.63/2.94 % 16.63/2.94 (owl_restrict_somevaluesfrom) % 16.63/2.94 $i(uri_owl_onProperty) & $i(uri_owl_someValuesFrom) & ! [v0: $i] : ! [v1: % 16.63/2.94 $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ % 16.63/2.94 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v2, v4) | ~ iext(v1, v3, v4) | ~ % 16.63/2.94 iext(uri_owl_onProperty, v0, v1) | ~ iext(uri_owl_someValuesFrom, v0, v2) | % 16.63/2.94 icext(v0, v3)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ % 16.63/2.94 $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, v3) | ~ % 16.63/2.94 iext(uri_owl_onProperty, v0, v1) | ~ iext(uri_owl_someValuesFrom, v0, v2) | % 16.63/2.94 ? [v4: $i] : ($i(v4) & icext(v2, v4) & iext(v1, v3, v4))) % 16.63/2.94 % 16.63/2.94 (rdfs_cext_def) % 16.63/2.94 $i(uri_rdf_type) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.94 icext(v1, v0) | iext(uri_rdf_type, v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( % 16.63/2.94 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_rdf_type, v0, v1) | icext(v1, v0)) % 16.63/2.94 % 16.63/2.94 (testcase_conclusion_fullish_013_Cliques) % 16.63/2.94 $i(uri_ex_bob) & $i(uri_ex_alice) & $i(uri_foaf_knows) & ~ % 16.63/2.94 iext(uri_foaf_knows, uri_ex_alice, uri_ex_bob) % 16.63/2.94 % 16.63/2.94 (testcase_premise_fullish_013_Cliques) % 16.63/2.94 $i(uri_ex_JoesGang) & $i(uri_owl_ObjectProperty) & $i(uri_owl_Restriction) & % 16.63/2.94 $i(uri_rdfs_range) & $i(uri_ex_sameCliqueAs) & $i(uri_owl_Class) & % 16.63/2.94 $i(uri_ex_Clique) & $i(uri_ex_bob) & $i(uri_ex_alice) & $i(uri_foaf_knows) & % 16.63/2.94 $i(uri_owl_inverseOf) & $i(uri_owl_propertyChainAxiom) & $i(uri_rdf_nil) & % 16.63/2.94 $i(uri_rdf_rest) & $i(uri_rdf_first) & $i(uri_owl_sameAs) & % 16.63/2.94 $i(uri_rdfs_subPropertyOf) & $i(uri_rdfs_subClassOf) & $i(uri_owl_onProperty) % 16.63/2.94 & $i(uri_owl_someValuesFrom) & $i(uri_rdf_type) & ? [v0: $i] : ? [v1: $i] : % 16.63/2.94 ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ($i(v4) & $i(v3) & $i(v2) & $i(v1) & % 16.63/2.94 $i(v0) & iext(uri_rdfs_range, uri_ex_sameCliqueAs, uri_ex_Clique) & % 16.63/2.94 iext(uri_owl_inverseOf, v1, uri_rdf_type) & iext(uri_owl_propertyChainAxiom, % 16.63/2.94 uri_foaf_knows, v2) & iext(uri_rdf_rest, v4, uri_rdf_nil) & % 16.63/2.94 iext(uri_rdf_rest, v3, v4) & iext(uri_rdf_rest, v2, v3) & % 16.63/2.94 iext(uri_rdf_first, v4, v1) & iext(uri_rdf_first, v3, uri_ex_sameCliqueAs) & % 16.63/2.94 iext(uri_rdf_first, v2, uri_rdf_type) & iext(uri_rdfs_subPropertyOf, % 16.63/2.94 uri_ex_sameCliqueAs, uri_owl_sameAs) & iext(uri_rdfs_subClassOf, % 16.63/2.94 uri_ex_Clique, v0) & iext(uri_owl_onProperty, v0, uri_ex_sameCliqueAs) & % 16.63/2.94 iext(uri_owl_someValuesFrom, v0, uri_ex_Clique) & iext(uri_rdf_type, v0, % 16.63/2.94 uri_owl_Restriction) & iext(uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique) % 16.63/2.94 & iext(uri_rdf_type, uri_ex_Clique, uri_owl_Class) & iext(uri_rdf_type, % 16.63/2.94 uri_ex_bob, uri_ex_JoesGang) & iext(uri_rdf_type, uri_ex_alice, % 16.63/2.94 uri_ex_JoesGang) & iext(uri_rdf_type, uri_foaf_knows, % 16.63/2.94 uri_owl_ObjectProperty)) % 16.63/2.94 % 16.63/2.94 Those formulas are unsatisfiable: % 16.63/2.94 --------------------------------- % 16.63/2.94 % 16.63/2.94 Begin of proof % 16.63/2.94 | % 16.63/2.94 | ALPHA: (testcase_conclusion_fullish_013_Cliques) implies: % 16.63/2.94 | (1) ~ iext(uri_foaf_knows, uri_ex_alice, uri_ex_bob) % 16.63/2.94 | % 16.63/2.94 | ALPHA: (testcase_premise_fullish_013_Cliques) implies: % 16.63/2.95 | (2) $i(uri_foaf_knows) % 16.63/2.95 | (3) $i(uri_ex_alice) % 16.63/2.95 | (4) $i(uri_ex_bob) % 16.63/2.95 | (5) $i(uri_ex_Clique) % 16.63/2.95 | (6) $i(uri_ex_sameCliqueAs) % 16.63/2.95 | (7) $i(uri_ex_JoesGang) % 16.63/2.95 | (8) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 16.63/2.95 | ($i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & iext(uri_rdfs_range, % 16.63/2.95 | uri_ex_sameCliqueAs, uri_ex_Clique) & iext(uri_owl_inverseOf, v1, % 16.63/2.95 | uri_rdf_type) & iext(uri_owl_propertyChainAxiom, uri_foaf_knows, % 16.63/2.95 | v2) & iext(uri_rdf_rest, v4, uri_rdf_nil) & iext(uri_rdf_rest, v3, % 16.63/2.95 | v4) & iext(uri_rdf_rest, v2, v3) & iext(uri_rdf_first, v4, v1) & % 16.63/2.95 | iext(uri_rdf_first, v3, uri_ex_sameCliqueAs) & iext(uri_rdf_first, % 16.63/2.95 | v2, uri_rdf_type) & iext(uri_rdfs_subPropertyOf, % 16.63/2.95 | uri_ex_sameCliqueAs, uri_owl_sameAs) & iext(uri_rdfs_subClassOf, % 16.63/2.95 | uri_ex_Clique, v0) & iext(uri_owl_onProperty, v0, % 16.63/2.95 | uri_ex_sameCliqueAs) & iext(uri_owl_someValuesFrom, v0, % 16.63/2.95 | uri_ex_Clique) & iext(uri_rdf_type, v0, uri_owl_Restriction) & % 16.63/2.95 | iext(uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique) & % 16.63/2.95 | iext(uri_rdf_type, uri_ex_Clique, uri_owl_Class) & iext(uri_rdf_type, % 16.63/2.95 | uri_ex_bob, uri_ex_JoesGang) & iext(uri_rdf_type, uri_ex_alice, % 16.63/2.95 | uri_ex_JoesGang) & iext(uri_rdf_type, uri_foaf_knows, % 16.63/2.95 | uri_owl_ObjectProperty)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_inv) implies: % 16.63/2.95 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | ~ % 16.63/2.95 | $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(v1, v3, v2) | ~ % 16.63/2.95 | iext(uri_owl_inverseOf, v0, v1) | iext(v0, v2, v3)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_chain_003) implies: % 16.63/2.95 | (10) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 16.63/2.95 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ! [v8: $i] : ! [v9: $i] : % 16.63/2.95 | ! [v10: $i] : ( ~ $i(v10) | ~ $i(v9) | ~ $i(v8) | ~ $i(v7) | ~ % 16.63/2.95 | $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | % 16.63/2.95 | ~ $i(v0) | ~ iext(v6, v9, v10) | ~ iext(v4, v8, v9) | ~ iext(v2, % 16.63/2.95 | v7, v8) | ~ iext(uri_owl_propertyChainAxiom, v0, v1) | ~ % 16.63/2.95 | iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) % 16.63/2.95 | | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | % 16.63/2.95 | ~ iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 16.63/2.95 | iext(v0, v7, v10)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_eqdis_sameas) implies: % 16.63/2.95 | (11) $i(uri_owl_sameAs) % 16.63/2.95 | (12) ! [v0: $i] : ! [v1: $i] : (v1 = v0 | ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.95 | iext(uri_owl_sameAs, v0, v1)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_rdfsext_subpropertyof) implies: % 16.63/2.95 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 16.63/2.95 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(v0, v2, v3) | ~ % 16.63/2.95 | iext(uri_rdfs_subPropertyOf, v0, v1) | iext(v1, v2, v3)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_rdfsext_subclassof) implies: % 16.63/2.95 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 16.63/2.95 | $i(v0) | ~ icext(v0, v2) | ~ iext(uri_rdfs_subClassOf, v0, v1) | % 16.63/2.95 | icext(v1, v2)) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (owl_restrict_somevaluesfrom) implies: % 16.63/2.95 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ( ~ $i(v3) | % 16.63/2.95 | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, v3) | ~ % 16.63/2.95 | iext(uri_owl_onProperty, v0, v1) | ~ iext(uri_owl_someValuesFrom, % 16.63/2.95 | v0, v2) | ? [v4: $i] : ($i(v4) & icext(v2, v4) & iext(v1, v3, % 16.63/2.95 | v4))) % 16.63/2.95 | % 16.63/2.95 | ALPHA: (rdfs_cext_def) implies: % 16.63/2.95 | (16) $i(uri_rdf_type) % 16.63/2.95 | (17) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 16.63/2.95 | iext(uri_rdf_type, v0, v1) | icext(v1, v0)) % 16.63/2.95 | % 16.63/2.95 | DELTA: instantiating (8) with fresh symbols all_11_0, all_11_1, all_11_2, % 16.63/2.95 | all_11_3, all_11_4 gives: % 16.63/2.96 | (18) $i(all_11_0) & $i(all_11_1) & $i(all_11_2) & $i(all_11_3) & % 16.63/2.96 | $i(all_11_4) & iext(uri_rdfs_range, uri_ex_sameCliqueAs, % 16.63/2.96 | uri_ex_Clique) & iext(uri_owl_inverseOf, all_11_3, uri_rdf_type) & % 16.63/2.96 | iext(uri_owl_propertyChainAxiom, uri_foaf_knows, all_11_2) & % 16.63/2.96 | iext(uri_rdf_rest, all_11_0, uri_rdf_nil) & iext(uri_rdf_rest, % 16.63/2.96 | all_11_1, all_11_0) & iext(uri_rdf_rest, all_11_2, all_11_1) & % 16.63/2.96 | iext(uri_rdf_first, all_11_0, all_11_3) & iext(uri_rdf_first, % 16.63/2.96 | all_11_1, uri_ex_sameCliqueAs) & iext(uri_rdf_first, all_11_2, % 16.63/2.96 | uri_rdf_type) & iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, % 16.63/2.96 | uri_owl_sameAs) & iext(uri_rdfs_subClassOf, uri_ex_Clique, all_11_4) % 16.63/2.96 | & iext(uri_owl_onProperty, all_11_4, uri_ex_sameCliqueAs) & % 16.63/2.96 | iext(uri_owl_someValuesFrom, all_11_4, uri_ex_Clique) & % 16.63/2.96 | iext(uri_rdf_type, all_11_4, uri_owl_Restriction) & iext(uri_rdf_type, % 16.63/2.96 | uri_ex_JoesGang, uri_ex_Clique) & iext(uri_rdf_type, uri_ex_Clique, % 16.63/2.96 | uri_owl_Class) & iext(uri_rdf_type, uri_ex_bob, uri_ex_JoesGang) & % 16.63/2.96 | iext(uri_rdf_type, uri_ex_alice, uri_ex_JoesGang) & iext(uri_rdf_type, % 16.63/2.96 | uri_foaf_knows, uri_owl_ObjectProperty) % 16.63/2.96 | % 16.63/2.96 | ALPHA: (18) implies: % 16.63/2.96 | (19) iext(uri_rdf_type, uri_ex_alice, uri_ex_JoesGang) % 16.63/2.96 | (20) iext(uri_rdf_type, uri_ex_bob, uri_ex_JoesGang) % 16.63/2.96 | (21) iext(uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique) % 16.63/2.96 | (22) iext(uri_owl_someValuesFrom, all_11_4, uri_ex_Clique) % 16.63/2.96 | (23) iext(uri_owl_onProperty, all_11_4, uri_ex_sameCliqueAs) % 16.63/2.96 | (24) iext(uri_rdfs_subClassOf, uri_ex_Clique, all_11_4) % 16.63/2.96 | (25) iext(uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, uri_owl_sameAs) % 16.63/2.96 | (26) iext(uri_rdf_first, all_11_2, uri_rdf_type) % 16.63/2.96 | (27) iext(uri_rdf_first, all_11_1, uri_ex_sameCliqueAs) % 16.63/2.96 | (28) iext(uri_rdf_first, all_11_0, all_11_3) % 16.63/2.96 | (29) iext(uri_rdf_rest, all_11_2, all_11_1) % 16.63/2.96 | (30) iext(uri_rdf_rest, all_11_1, all_11_0) % 16.63/2.96 | (31) iext(uri_rdf_rest, all_11_0, uri_rdf_nil) % 16.63/2.96 | (32) iext(uri_owl_propertyChainAxiom, uri_foaf_knows, all_11_2) % 16.63/2.96 | (33) iext(uri_owl_inverseOf, all_11_3, uri_rdf_type) % 16.63/2.96 | (34) $i(all_11_4) % 16.63/2.96 | (35) $i(all_11_3) % 16.63/2.96 | (36) $i(all_11_2) % 16.63/2.96 | (37) $i(all_11_1) % 16.63/2.96 | (38) $i(all_11_0) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (17) with uri_ex_JoesGang, uri_ex_Clique, % 16.63/2.96 | simplifying with (5), (7), (21) gives: % 16.63/2.96 | (39) icext(uri_ex_Clique, uri_ex_JoesGang) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (9) with all_11_3, uri_rdf_type, uri_ex_JoesGang, % 16.63/2.96 | uri_ex_bob, simplifying with (4), (7), (16), (20), (33), (35) % 16.63/2.96 | gives: % 16.63/2.96 | (40) iext(all_11_3, uri_ex_JoesGang, uri_ex_bob) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (14) with uri_ex_Clique, all_11_4, uri_ex_JoesGang, % 16.63/2.96 | simplifying with (5), (7), (24), (34), (39) gives: % 16.63/2.96 | (41) icext(all_11_4, uri_ex_JoesGang) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (15) with all_11_4, uri_ex_sameCliqueAs, % 16.63/2.96 | uri_ex_Clique, uri_ex_JoesGang, simplifying with (5), (6), (7), % 16.63/2.96 | (22), (23), (34), (41) gives: % 16.63/2.96 | (42) ? [v0: $i] : ($i(v0) & icext(uri_ex_Clique, v0) & % 16.63/2.96 | iext(uri_ex_sameCliqueAs, uri_ex_JoesGang, v0)) % 16.63/2.96 | % 16.63/2.96 | DELTA: instantiating (42) with fresh symbol all_31_0 gives: % 16.63/2.96 | (43) $i(all_31_0) & icext(uri_ex_Clique, all_31_0) & % 16.63/2.96 | iext(uri_ex_sameCliqueAs, uri_ex_JoesGang, all_31_0) % 16.63/2.96 | % 16.63/2.96 | ALPHA: (43) implies: % 16.63/2.96 | (44) iext(uri_ex_sameCliqueAs, uri_ex_JoesGang, all_31_0) % 16.63/2.96 | (45) $i(all_31_0) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (13) with uri_ex_sameCliqueAs, uri_owl_sameAs, % 16.63/2.96 | uri_ex_JoesGang, all_31_0, simplifying with (6), (7), (11), (25), % 16.63/2.96 | (44), (45) gives: % 16.63/2.96 | (46) iext(uri_owl_sameAs, uri_ex_JoesGang, all_31_0) % 16.63/2.96 | % 16.63/2.96 | GROUND_INST: instantiating (12) with uri_ex_JoesGang, all_31_0, simplifying % 16.63/2.96 | with (7), (45), (46) gives: % 16.63/2.96 | (47) all_31_0 = uri_ex_JoesGang % 16.63/2.97 | % 16.63/2.97 | REDUCE: (44), (47) imply: % 16.63/2.97 | (48) iext(uri_ex_sameCliqueAs, uri_ex_JoesGang, uri_ex_JoesGang) % 16.63/2.97 | % 16.63/2.97 | GROUND_INST: instantiating (10) with uri_foaf_knows, all_11_2, uri_rdf_type, % 16.63/2.97 | all_11_1, uri_ex_sameCliqueAs, all_11_0, all_11_3, uri_ex_alice, % 16.63/2.97 | uri_ex_JoesGang, uri_ex_JoesGang, uri_ex_bob, simplifying with % 16.63/2.97 | (1), (2), (3), (4), (6), (7), (16), (19), (26), (27), (28), (29), % 16.63/2.97 | (30), (31), (32), (35), (36), (37), (38), (40), (48) gives: % 16.63/2.97 | (49) $false % 16.63/2.97 | % 16.63/2.97 | CLOSE: (49) is inconsistent. % 16.63/2.97 | % 16.63/2.97 End of proof % 16.63/2.97 % SZS output end Proof for theBenchmark % 16.63/2.97 % 16.63/2.97 2392ms %------------------------------------------------------------------------------