%------------------------------------------------------------------------------ % File : Princess---230619 % Problem : SWB020+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 : n022.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:47 EDT 2023 % Result : Theorem 73.06s 10.56s % Output : Proof 73.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWB020+2 : TPTP v8.1.2. Released v5.2.0. % 0.00/0.14 % Command : princess -inputFormat=tptp +threads -portfolio=casc +printProof -timeoutSec=%d %s % 0.18/0.36 % Computer : n022.cluster.edu % 0.18/0.36 % Model : x86_64 x86_64 % 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.36 % Memory : 8042.1875MB % 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.36 % CPULimit : 300 % 0.18/0.36 % WCLimit : 300 % 0.18/0.36 % DateTime : Sun Aug 27 06:56:40 EDT 2023 % 0.18/0.36 % CPUTime : % 0.21/0.65 ________ _____ % 0.21/0.65 ___ __ \_________(_)________________________________ % 0.21/0.65 __ /_/ /_ ___/_ /__ __ \ ___/ _ \_ ___/_ ___/ % 0.21/0.65 _ ____/_ / _ / _ / / / /__ / __/(__ )_(__ ) % 0.21/0.65 /_/ /_/ /_/ /_/ /_/\___/ \___//____/ /____/ % 0.21/0.65 % 0.21/0.65 A Theorem Prover for First-Order Logic modulo Linear Integer Arithmetic % 0.21/0.65 (2023-06-19) % 0.21/0.65 % 0.21/0.65 (c) Philipp Rümmer, 2009-2023 % 0.21/0.65 Contributors: Peter Backeman, Peter Baumgartner, Angelo Brillout, Zafer Esen, % 0.21/0.65 Amanda Stjerna. % 0.21/0.65 Free software under BSD-3-Clause. % 0.21/0.65 % 0.21/0.65 For more information, visit http://www.philipp.ruemmer.org/princess.shtml % 0.21/0.65 % 0.21/0.65 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.21/0.67 Running up to 7 provers in parallel. % 0.21/0.68 Prover 0: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1042961893 % 0.21/0.68 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-1571432423 % 0.21/0.68 Prover 2: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMinimalAndEmpty -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1065072994 % 0.21/0.68 Prover 5: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -realRatSaturationRounds=1 -ignoreQuantifiers -constructProofs=never -generateTriggers=complete -randomSeed=1259561288 % 0.21/0.68 Prover 3: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=1922548996 % 0.21/0.68 Prover 6: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximalOutermost -realRatSaturationRounds=0 -ignoreQuantifiers -constructProofs=never -generateTriggers=all -randomSeed=-1399714365 % 0.21/0.68 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=1868514696 % 2.30/1.17 Prover 4: Preprocessing ... % 2.83/1.18 Prover 1: Preprocessing ... % 2.83/1.23 Prover 6: Preprocessing ... % 2.83/1.23 Prover 5: Preprocessing ... % 2.83/1.23 Prover 2: Preprocessing ... % 2.83/1.23 Prover 3: Preprocessing ... % 2.83/1.23 Prover 0: Preprocessing ... % 5.99/1.65 Prover 5: Proving ... % 6.31/1.71 Prover 2: Proving ... % 7.06/1.79 Prover 3: Constructing countermodel ... % 7.06/1.81 Prover 6: Proving ... % 7.06/1.82 Prover 1: Constructing countermodel ... % 19.61/3.70 Prover 4: Constructing countermodel ... % 23.59/4.03 Prover 0: Proving ... % 25.29/4.26 Prover 3: gave up % 25.29/4.27 Prover 7: Options: +triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allUni -realRatSaturationRounds=1 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-236303470 % 25.29/4.33 Prover 7: Preprocessing ... % 25.29/4.45 Prover 7: Warning: ignoring some quantifiers % 25.29/4.47 Prover 7: Constructing countermodel ... % 63.55/9.37 Prover 2: stopped % 63.55/9.39 Prover 8: Options: +triggersInConjecture +genTotalityAxioms -tightFunctionScopes -clausifier=none -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -realRatSaturationRounds=0 +ignoreQuantifiers -constructProofs=always -generateTriggers=all -randomSeed=-200781089 % 64.75/9.45 Prover 8: Preprocessing ... % 65.98/9.62 Prover 8: Warning: ignoring some quantifiers % 65.98/9.62 Prover 8: Constructing countermodel ... % 73.06/10.55 Prover 7: Found proof (size 34) % 73.06/10.55 Prover 7: proved (6268ms) % 73.06/10.55 Prover 0: stopped % 73.06/10.55 Prover 8: stopped % 73.06/10.55 Prover 1: stopped % 73.06/10.55 Prover 5: stopped % 73.06/10.55 Prover 4: stopped % 73.06/10.55 Prover 6: stopped % 73.06/10.55 % 73.06/10.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p % 73.06/10.56 % 73.06/10.56 % SZS output start Proof for theBenchmark % 73.06/10.57 Assumptions after simplification: % 73.06/10.57 --------------------------------- % 73.06/10.57 % 73.06/10.57 (owl_bool_complementof_class) % 73.39/10.58 $i(uri_owl_complementOf) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 73.39/10.58 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v1, v2) | ~ icext(v0, v2) | ~ % 73.39/10.58 iext(uri_owl_complementOf, v0, v1)) & ? [v0: $i] : ! [v1: $i] : ! [v2: % 73.39/10.58 $i] : ( ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_complementOf, v1, % 73.39/10.58 v2) | icext(v2, v0) | icext(v1, v0)) & ! [v0: $i] : ! [v1: $i] : ( ~ % 73.39/10.58 $i(v1) | ~ $i(v0) | ~ iext(uri_owl_complementOf, v0, v1) | ic(v1)) & ! % 73.39/10.58 [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.58 iext(uri_owl_complementOf, v0, v1) | ic(v0)) % 73.39/10.58 % 73.39/10.58 (owl_bool_intersectionof_class_002) % 73.39/10.60 $i(uri_owl_intersectionOf) & $i(uri_rdf_nil) & $i(uri_rdf_rest) & % 73.39/10.60 $i(uri_rdf_first) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! % 73.39/10.60 [v4: $i] : ! [v5: $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 73.39/10.60 $i(v1) | ~ $i(v0) | ~ icext(v4, v5) | ~ icext(v2, v5) | ~ % 73.39/10.60 iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.60 uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v3, % 73.39/10.60 v4) | ~ iext(uri_rdf_first, v1, v2) | icext(v0, v5)) & ! [v0: $i] : ! % 73.39/10.60 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ $i(v5) % 73.39/10.60 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, % 73.39/10.60 v5) | ~ iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.60 uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v3, % 73.39/10.60 v4) | ~ iext(uri_rdf_first, v1, v2) | icext(v4, v5)) & ! [v0: $i] : ! % 73.39/10.60 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ( ~ $i(v5) % 73.39/10.60 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, % 73.39/10.60 v5) | ~ iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.60 uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v3, % 73.39/10.60 v4) | ~ iext(uri_rdf_first, v1, v2) | icext(v2, v5)) & ! [v0: $i] : ! % 73.39/10.60 [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | % 73.39/10.60 ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ ic(v4) | ~ ic(v2) | ~ ic(v0) | ~ % 73.39/10.60 iext(uri_rdf_rest, v3, uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.60 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 73.39/10.60 iext(uri_owl_intersectionOf, v0, v1) | ? [v5: $i] : ($i(v5) & ( ~ icext(v4, % 73.39/10.60 v5) | ~ icext(v2, v5) | ~ icext(v0, v5)) & (icext(v0, v5) | % 73.39/10.60 (icext(v4, v5) & icext(v2, v5))))) & ! [v0: $i] : ! [v1: $i] : ! [v2: % 73.39/10.60 $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 73.39/10.60 $i(v1) | ~ $i(v0) | ~ iext(uri_owl_intersectionOf, v0, v1) | ~ % 73.39/10.60 iext(uri_rdf_rest, v3, uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.60 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v4)) & ! % 73.39/10.60 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) % 73.39/10.60 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.60 iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.60 uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v3, % 73.39/10.60 v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v2)) & ! [v0: $i] : ! [v1: $i] % 73.39/10.60 : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ( ~ $i(v4) | ~ $i(v3) | ~ $i(v2) % 73.39/10.60 | ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_intersectionOf, v0, v1) | ~ % 73.39/10.60 iext(uri_rdf_rest, v3, uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.60 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v0)) % 73.39/10.60 % 73.39/10.60 (owl_bool_unionof_class_003) % 73.39/10.61 $i(uri_owl_unionOf) & $i(uri_rdf_nil) & $i(uri_rdf_rest) & $i(uri_rdf_first) & % 73.39/10.61 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 73.39/10.61 $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ % 73.39/10.61 $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v6, v7) | % 73.39/10.61 ~ iext(uri_owl_unionOf, v0, v1) | ~ iext(uri_rdf_rest, v5, uri_rdf_nil) | % 73.39/10.61 ~ iext(uri_rdf_rest, v3, v5) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.61 iext(uri_rdf_first, v5, v6) | ~ iext(uri_rdf_first, v3, v4) | ~ % 73.39/10.61 iext(uri_rdf_first, v1, v2) | icext(v0, v7)) & ! [v0: $i] : ! [v1: $i] : % 73.39/10.61 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 73.39/10.61 $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) % 73.39/10.61 | ~ $i(v1) | ~ $i(v0) | ~ icext(v4, v7) | ~ iext(uri_owl_unionOf, v0, % 73.39/10.61 v1) | ~ iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, % 73.39/10.61 v5) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.61 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | icext(v0, % 73.39/10.61 v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] % 73.39/10.61 : ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) % 73.39/10.61 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v2, % 73.39/10.61 v7) | ~ iext(uri_owl_unionOf, v0, v1) | ~ iext(uri_rdf_rest, v5, % 73.39/10.61 uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ iext(uri_rdf_rest, v1, % 73.39/10.61 v3) | ~ iext(uri_rdf_first, v5, v6) | ~ iext(uri_rdf_first, v3, v4) | ~ % 73.39/10.61 iext(uri_rdf_first, v1, v2) | icext(v0, v7)) & ! [v0: $i] : ! [v1: $i] : % 73.39/10.61 ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ! [v7: % 73.39/10.61 $i] : ( ~ $i(v7) | ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) % 73.39/10.61 | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, v7) | ~ iext(uri_owl_unionOf, v0, % 73.39/10.61 v1) | ~ iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, % 73.39/10.61 v5) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.61 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | icext(v6, v7) % 73.39/10.61 | icext(v4, v7) | icext(v2, v7)) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : % 73.39/10.61 ! [v3: $i] : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) % 73.39/10.61 | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ ic(v6) | ~ % 73.39/10.61 ic(v4) | ~ ic(v2) | ~ ic(v0) | ~ iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ % 73.39/10.61 iext(uri_rdf_rest, v3, v5) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.61 iext(uri_rdf_first, v5, v6) | ~ iext(uri_rdf_first, v3, v4) | ~ % 73.39/10.61 iext(uri_rdf_first, v1, v2) | iext(uri_owl_unionOf, v0, v1) | ? [v7: $i] : % 73.39/10.61 ($i(v7) & ( ~ icext(v0, v7) | ( ~ icext(v6, v7) & ~ icext(v4, v7) & ~ % 73.39/10.61 icext(v2, v7))) & (icext(v6, v7) | icext(v4, v7) | icext(v2, v7) | % 73.39/10.62 icext(v0, v7)))) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] % 73.39/10.62 : ! [v4: $i] : ! [v5: $i] : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) % 73.39/10.62 | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_unionOf, % 73.39/10.62 v0, v1) | ~ iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, % 73.39/10.62 v3, v5) | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | % 73.39/10.62 ~ iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v6)) & % 73.39/10.62 ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: % 73.39/10.62 $i] : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ % 73.39/10.62 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_unionOf, v0, v1) | ~ % 73.39/10.62 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 73.39/10.62 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.62 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v4)) & ! % 73.39/10.62 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 73.39/10.62 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 73.39/10.62 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_unionOf, v0, v1) | ~ % 73.39/10.62 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 73.39/10.62 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.62 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v2)) & ! % 73.39/10.62 [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : ! [v5: $i] % 73.39/10.62 : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | % 73.39/10.62 ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_unionOf, v0, v1) | ~ % 73.39/10.62 iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 73.39/10.62 iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.62 iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | ic(v0)) % 73.39/10.62 % 73.39/10.62 (owl_eqdis_disjointwith) % 73.39/10.62 $i(uri_owl_disjointWith) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ % 73.39/10.62 $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ icext(v1, v2) | ~ icext(v0, v2) | ~ % 73.39/10.62 iext(uri_owl_disjointWith, v0, v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) % 73.39/10.62 | ~ $i(v0) | ~ ic(v1) | ~ ic(v0) | iext(uri_owl_disjointWith, v0, v1) | % 73.39/10.62 ? [v2: $i] : ($i(v2) & icext(v1, v2) & icext(v0, v2))) & ! [v0: $i] : ! % 73.39/10.62 [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ iext(uri_owl_disjointWith, v0, v1) | % 73.39/10.62 ic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.62 iext(uri_owl_disjointWith, v0, v1) | ic(v0)) % 73.39/10.62 % 73.39/10.62 (owl_rdfsext_subclassof) % 73.39/10.62 $i(uri_rdfs_subClassOf) & ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) % 73.39/10.62 | ~ $i(v1) | ~ $i(v0) | ~ icext(v0, v2) | ~ iext(uri_rdfs_subClassOf, % 73.39/10.62 v0, v1) | icext(v1, v2)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ % 73.39/10.62 $i(v0) | ~ ic(v1) | ~ ic(v0) | iext(uri_rdfs_subClassOf, v0, v1) | ? [v2: % 73.39/10.62 $i] : ($i(v2) & icext(v0, v2) & ~ icext(v1, v2))) & ! [v0: $i] : ! [v1: % 73.39/10.62 $i] : ( ~ $i(v1) | ~ $i(v0) | ~ iext(uri_rdfs_subClassOf, v0, v1) | % 73.39/10.62 ic(v1)) & ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.62 iext(uri_rdfs_subClassOf, v0, v1) | ic(v0)) % 73.39/10.62 % 73.39/10.62 (testcase_conclusion_fullish_020_Logical_Complications) % 73.39/10.62 $i(uri_ex_c3) & $i(uri_ex_d) & $i(uri_rdfs_subClassOf) & ~ % 73.39/10.62 iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3) % 73.39/10.62 % 73.39/10.62 (testcase_premise_fullish_020_Logical_Complications) % 73.39/10.62 $i(uri_ex_c2) & $i(uri_ex_c1) & $i(uri_ex_c) & $i(uri_ex_c3) & $i(uri_ex_d) & % 73.39/10.62 $i(uri_rdfs_subClassOf) & $i(uri_owl_unionOf) & $i(uri_owl_intersectionOf) & % 73.39/10.62 $i(uri_rdf_nil) & $i(uri_rdf_rest) & $i(uri_rdf_first) & % 73.39/10.62 $i(uri_owl_complementOf) & $i(uri_owl_disjointWith) & ? [v0: $i] : ? [v1: % 73.39/10.62 $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : ? [v5: $i] : ? [v6: $i] : % 73.39/10.62 ($i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) & $i(v1) & $i(v0) & % 73.39/10.62 iext(uri_rdfs_subClassOf, uri_ex_d, v0) & iext(uri_owl_unionOf, uri_ex_c, % 73.39/10.62 v2) & iext(uri_owl_intersectionOf, v0, v5) & iext(uri_rdf_rest, v6, % 73.39/10.62 uri_rdf_nil) & iext(uri_rdf_rest, v5, v6) & iext(uri_rdf_rest, v4, % 73.39/10.62 uri_rdf_nil) & iext(uri_rdf_rest, v3, v4) & iext(uri_rdf_rest, v2, v3) & % 73.39/10.62 iext(uri_rdf_first, v6, v1) & iext(uri_rdf_first, v5, uri_ex_c) & % 73.39/10.62 iext(uri_rdf_first, v4, uri_ex_c3) & iext(uri_rdf_first, v3, uri_ex_c2) & % 73.39/10.63 iext(uri_rdf_first, v2, uri_ex_c1) & iext(uri_owl_complementOf, v1, % 73.39/10.63 uri_ex_c2) & iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1)) % 73.39/10.63 % 73.39/10.63 Further assumptions not needed in the proof: % 73.39/10.63 -------------------------------------------- % 73.39/10.63 owl_prop_disjointwith_ext % 73.39/10.63 % 73.39/10.63 Those formulas are unsatisfiable: % 73.39/10.63 --------------------------------- % 73.39/10.63 % 73.39/10.63 Begin of proof % 73.39/10.63 | % 73.39/10.63 | ALPHA: (testcase_conclusion_fullish_020_Logical_Complications) implies: % 73.39/10.63 | (1) ~ iext(uri_rdfs_subClassOf, uri_ex_d, uri_ex_c3) % 73.39/10.63 | % 73.39/10.63 | ALPHA: (testcase_premise_fullish_020_Logical_Complications) implies: % 73.39/10.63 | (2) $i(uri_ex_d) % 73.39/10.63 | (3) $i(uri_ex_c3) % 73.39/10.63 | (4) $i(uri_ex_c) % 73.39/10.63 | (5) $i(uri_ex_c1) % 73.39/10.63 | (6) $i(uri_ex_c2) % 73.39/10.63 | (7) ? [v0: $i] : ? [v1: $i] : ? [v2: $i] : ? [v3: $i] : ? [v4: $i] : % 73.39/10.63 | ? [v5: $i] : ? [v6: $i] : ($i(v6) & $i(v5) & $i(v4) & $i(v3) & $i(v2) % 73.39/10.63 | & $i(v1) & $i(v0) & iext(uri_rdfs_subClassOf, uri_ex_d, v0) & % 73.39/10.63 | iext(uri_owl_unionOf, uri_ex_c, v2) & iext(uri_owl_intersectionOf, % 73.39/10.63 | v0, v5) & iext(uri_rdf_rest, v6, uri_rdf_nil) & iext(uri_rdf_rest, % 73.39/10.63 | v5, v6) & iext(uri_rdf_rest, v4, uri_rdf_nil) & iext(uri_rdf_rest, % 73.39/10.63 | v3, v4) & iext(uri_rdf_rest, v2, v3) & iext(uri_rdf_first, v6, v1) % 73.39/10.63 | & iext(uri_rdf_first, v5, uri_ex_c) & iext(uri_rdf_first, v4, % 73.39/10.63 | uri_ex_c3) & iext(uri_rdf_first, v3, uri_ex_c2) & % 73.39/10.63 | iext(uri_rdf_first, v2, uri_ex_c1) & iext(uri_owl_complementOf, v1, % 73.39/10.63 | uri_ex_c2) & iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1)) % 73.39/10.63 | % 73.39/10.63 | ALPHA: (owl_eqdis_disjointwith) implies: % 73.39/10.63 | (8) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ ic(v1) | ~ % 73.39/10.63 | ic(v0) | iext(uri_owl_disjointWith, v0, v1) | ? [v2: $i] : ($i(v2) & % 73.39/10.63 | icext(v1, v2) & icext(v0, v2))) % 73.39/10.63 | (9) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 73.39/10.63 | $i(v0) | ~ icext(v1, v2) | ~ icext(v0, v2) | ~ % 73.39/10.63 | iext(uri_owl_disjointWith, v0, v1)) % 73.39/10.63 | % 73.39/10.63 | ALPHA: (owl_rdfsext_subclassof) implies: % 73.39/10.63 | (10) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.63 | iext(uri_rdfs_subClassOf, v0, v1) | ic(v0)) % 73.39/10.64 | (11) ! [v0: $i] : ! [v1: $i] : ( ~ $i(v1) | ~ $i(v0) | ~ ic(v1) | ~ % 73.39/10.64 | ic(v0) | iext(uri_rdfs_subClassOf, v0, v1) | ? [v2: $i] : ($i(v2) & % 73.39/10.64 | icext(v0, v2) & ~ icext(v1, v2))) % 73.39/10.64 | (12) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 73.39/10.64 | $i(v0) | ~ icext(v0, v2) | ~ iext(uri_rdfs_subClassOf, v0, v1) | % 73.39/10.64 | icext(v1, v2)) % 73.39/10.64 | % 73.39/10.64 | ALPHA: (owl_bool_unionof_class_003) implies: % 73.39/10.64 | (13) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 73.39/10.64 | ! [v5: $i] : ! [v6: $i] : ( ~ $i(v6) | ~ $i(v5) | ~ $i(v4) | ~ % 73.39/10.64 | $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | ~ % 73.39/10.64 | iext(uri_owl_unionOf, v0, v1) | ~ iext(uri_rdf_rest, v5, % 73.39/10.64 | uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) | ~ % 73.39/10.64 | iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | ~ % 73.39/10.64 | iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 73.39/10.64 | ic(v6)) % 73.39/10.64 | (14) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 73.39/10.64 | ! [v5: $i] : ! [v6: $i] : ! [v7: $i] : ( ~ $i(v7) | ~ $i(v6) | ~ % 73.39/10.64 | $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ $i(v1) | ~ $i(v0) | % 73.39/10.64 | ~ icext(v0, v7) | ~ iext(uri_owl_unionOf, v0, v1) | ~ % 73.39/10.64 | iext(uri_rdf_rest, v5, uri_rdf_nil) | ~ iext(uri_rdf_rest, v3, v5) % 73.39/10.64 | | ~ iext(uri_rdf_rest, v1, v3) | ~ iext(uri_rdf_first, v5, v6) | % 73.39/10.64 | ~ iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 73.39/10.64 | icext(v6, v7) | icext(v4, v7) | icext(v2, v7)) % 73.39/10.64 | % 73.39/10.64 | ALPHA: (owl_bool_intersectionof_class_002) implies: % 73.39/10.64 | (15) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 73.39/10.64 | ! [v5: $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 73.39/10.64 | $i(v1) | ~ $i(v0) | ~ icext(v0, v5) | ~ % 73.39/10.64 | iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.64 | uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.64 | iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 73.39/10.64 | icext(v2, v5)) % 73.39/10.64 | (16) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ! [v3: $i] : ! [v4: $i] : % 73.39/10.64 | ! [v5: $i] : ( ~ $i(v5) | ~ $i(v4) | ~ $i(v3) | ~ $i(v2) | ~ % 73.39/10.64 | $i(v1) | ~ $i(v0) | ~ icext(v0, v5) | ~ % 73.39/10.64 | iext(uri_owl_intersectionOf, v0, v1) | ~ iext(uri_rdf_rest, v3, % 73.39/10.64 | uri_rdf_nil) | ~ iext(uri_rdf_rest, v1, v3) | ~ % 73.39/10.64 | iext(uri_rdf_first, v3, v4) | ~ iext(uri_rdf_first, v1, v2) | % 73.39/10.64 | icext(v4, v5)) % 73.39/10.64 | % 73.39/10.64 | ALPHA: (owl_bool_complementof_class) implies: % 73.39/10.65 | (17) ! [v0: $i] : ! [v1: $i] : ! [v2: $i] : ( ~ $i(v2) | ~ $i(v1) | ~ % 73.39/10.65 | $i(v0) | ~ icext(v1, v2) | ~ icext(v0, v2) | ~ % 73.39/10.65 | iext(uri_owl_complementOf, v0, v1)) % 73.39/10.65 | % 73.39/10.65 | DELTA: instantiating (7) with fresh symbols all_11_0, all_11_1, all_11_2, % 73.39/10.65 | all_11_3, all_11_4, all_11_5, all_11_6 gives: % 73.39/10.65 | (18) $i(all_11_0) & $i(all_11_1) & $i(all_11_2) & $i(all_11_3) & % 73.39/10.65 | $i(all_11_4) & $i(all_11_5) & $i(all_11_6) & iext(uri_rdfs_subClassOf, % 73.39/10.65 | uri_ex_d, all_11_6) & iext(uri_owl_unionOf, uri_ex_c, all_11_4) & % 73.39/10.65 | iext(uri_owl_intersectionOf, all_11_6, all_11_1) & iext(uri_rdf_rest, % 73.39/10.65 | all_11_0, uri_rdf_nil) & iext(uri_rdf_rest, all_11_1, all_11_0) & % 73.39/10.65 | iext(uri_rdf_rest, all_11_2, uri_rdf_nil) & iext(uri_rdf_rest, % 73.39/10.65 | all_11_3, all_11_2) & iext(uri_rdf_rest, all_11_4, all_11_3) & % 73.39/10.65 | iext(uri_rdf_first, all_11_0, all_11_5) & iext(uri_rdf_first, % 73.39/10.65 | all_11_1, uri_ex_c) & iext(uri_rdf_first, all_11_2, uri_ex_c3) & % 73.39/10.65 | iext(uri_rdf_first, all_11_3, uri_ex_c2) & iext(uri_rdf_first, % 73.39/10.65 | all_11_4, uri_ex_c1) & iext(uri_owl_complementOf, all_11_5, % 73.75/10.65 | uri_ex_c2) & iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1) % 73.75/10.65 | % 73.75/10.65 | ALPHA: (18) implies: % 73.75/10.65 | (19) iext(uri_owl_disjointWith, uri_ex_d, uri_ex_c1) % 73.75/10.65 | (20) iext(uri_owl_complementOf, all_11_5, uri_ex_c2) % 73.75/10.65 | (21) iext(uri_rdf_first, all_11_4, uri_ex_c1) % 73.75/10.65 | (22) iext(uri_rdf_first, all_11_3, uri_ex_c2) % 73.75/10.65 | (23) iext(uri_rdf_first, all_11_2, uri_ex_c3) % 73.75/10.65 | (24) iext(uri_rdf_first, all_11_1, uri_ex_c) % 73.75/10.65 | (25) iext(uri_rdf_first, all_11_0, all_11_5) % 73.75/10.65 | (26) iext(uri_rdf_rest, all_11_4, all_11_3) % 73.75/10.65 | (27) iext(uri_rdf_rest, all_11_3, all_11_2) % 73.75/10.65 | (28) iext(uri_rdf_rest, all_11_2, uri_rdf_nil) % 73.75/10.65 | (29) iext(uri_rdf_rest, all_11_1, all_11_0) % 73.75/10.65 | (30) iext(uri_rdf_rest, all_11_0, uri_rdf_nil) % 73.75/10.65 | (31) iext(uri_owl_intersectionOf, all_11_6, all_11_1) % 73.75/10.65 | (32) iext(uri_owl_unionOf, uri_ex_c, all_11_4) % 73.75/10.65 | (33) iext(uri_rdfs_subClassOf, uri_ex_d, all_11_6) % 73.75/10.65 | (34) $i(all_11_6) % 73.75/10.65 | (35) $i(all_11_5) % 73.75/10.65 | (36) $i(all_11_4) % 73.75/10.65 | (37) $i(all_11_3) % 73.75/10.65 | (38) $i(all_11_2) % 73.75/10.65 | (39) $i(all_11_1) % 73.75/10.65 | (40) $i(all_11_0) % 73.75/10.65 | % 73.75/10.66 | GROUND_INST: instantiating (13) with uri_ex_c, all_11_4, uri_ex_c1, all_11_3, % 73.75/10.66 | uri_ex_c2, all_11_2, uri_ex_c3, simplifying with (3), (4), (5), % 73.75/10.66 | (6), (21), (22), (23), (26), (27), (28), (32), (36), (37), (38) % 73.75/10.66 | gives: % 73.75/10.66 | (41) ic(uri_ex_c3) % 73.75/10.66 | % 73.75/10.66 | GROUND_INST: instantiating (10) with uri_ex_d, all_11_6, simplifying with (2), % 73.75/10.66 | (33), (34) gives: % 73.75/10.66 | (42) ic(uri_ex_d) % 73.75/10.66 | % 73.75/10.66 | GROUND_INST: instantiating (8) with uri_ex_d, uri_ex_d, simplifying with (2), % 73.75/10.66 | (42) gives: % 73.75/10.66 | (43) iext(uri_owl_disjointWith, uri_ex_d, uri_ex_d) | ? [v0: $i] : ($i(v0) % 73.75/10.66 | & icext(uri_ex_d, v0)) % 73.75/10.66 | % 73.75/10.66 | GROUND_INST: instantiating (11) with uri_ex_d, uri_ex_c3, simplifying with % 73.75/10.66 | (1), (2), (3), (41), (42) gives: % 73.75/10.66 | (44) ? [v0: $i] : ($i(v0) & icext(uri_ex_d, v0) & ~ icext(uri_ex_c3, v0)) % 73.75/10.66 | % 73.75/10.66 | DELTA: instantiating (44) with fresh symbol all_29_0 gives: % 73.75/10.66 | (45) $i(all_29_0) & icext(uri_ex_d, all_29_0) & ~ icext(uri_ex_c3, % 73.75/10.66 | all_29_0) % 73.75/10.66 | % 73.75/10.66 | ALPHA: (45) implies: % 73.75/10.66 | (46) ~ icext(uri_ex_c3, all_29_0) % 73.75/10.66 | (47) icext(uri_ex_d, all_29_0) % 73.75/10.66 | (48) $i(all_29_0) % 73.75/10.66 | % 73.75/10.66 | GROUND_INST: instantiating (12) with uri_ex_d, all_11_6, all_29_0, simplifying % 73.75/10.66 | with (2), (33), (34), (47), (48) gives: % 73.75/10.66 | (49) icext(all_11_6, all_29_0) % 73.75/10.66 | % 73.75/10.66 | GROUND_INST: instantiating (9) with uri_ex_d, uri_ex_d, all_29_0, simplifying % 73.75/10.66 | with (2), (47), (48) gives: % 73.75/10.66 | (50) ~ iext(uri_owl_disjointWith, uri_ex_d, uri_ex_d) % 73.75/10.66 | % 73.75/10.66 | BETA: splitting (43) gives: % 73.75/10.66 | % 73.75/10.66 | Case 1: % 73.75/10.66 | | % 73.75/10.66 | | (51) iext(uri_owl_disjointWith, uri_ex_d, uri_ex_d) % 73.75/10.66 | | % 73.75/10.66 | | PRED_UNIFY: (50), (51) imply: % 73.75/10.66 | | (52) $false % 73.75/10.66 | | % 73.75/10.66 | | CLOSE: (52) is inconsistent. % 73.75/10.66 | | % 73.75/10.66 | Case 2: % 73.75/10.66 | | % 73.75/10.66 | | % 73.75/10.67 | | GROUND_INST: instantiating (14) with uri_ex_c, all_11_4, uri_ex_c1, % 73.75/10.67 | | all_11_3, uri_ex_c2, all_11_2, uri_ex_c3, all_29_0, simplifying % 73.75/10.67 | | with (3), (4), (5), (6), (21), (22), (23), (26), (27), (28), % 73.75/10.67 | | (32), (36), (37), (38), (46), (48) gives: % 73.85/10.67 | | (53) ~ icext(uri_ex_c, all_29_0) | icext(uri_ex_c2, all_29_0) | % 73.85/10.67 | | icext(uri_ex_c1, all_29_0) % 73.85/10.67 | | % 73.85/10.67 | | GROUND_INST: instantiating (16) with all_11_6, all_11_1, uri_ex_c, all_11_0, % 73.85/10.67 | | all_11_5, all_29_0, simplifying with (4), (24), (25), (29), % 73.85/10.67 | | (30), (31), (34), (35), (39), (40), (48), (49) gives: % 73.85/10.67 | | (54) icext(all_11_5, all_29_0) % 73.85/10.67 | | % 73.85/10.67 | | GROUND_INST: instantiating (15) with all_11_6, all_11_1, uri_ex_c, all_11_0, % 73.85/10.67 | | all_11_5, all_29_0, simplifying with (4), (24), (25), (29), % 73.85/10.67 | | (30), (31), (34), (35), (39), (40), (48), (49) gives: % 73.85/10.67 | | (55) icext(uri_ex_c, all_29_0) % 73.85/10.67 | | % 73.85/10.67 | | GROUND_INST: instantiating (9) with uri_ex_d, uri_ex_c1, all_29_0, % 73.85/10.67 | | simplifying with (2), (5), (19), (47), (48) gives: % 73.85/10.67 | | (56) ~ icext(uri_ex_c1, all_29_0) % 73.85/10.67 | | % 73.85/10.67 | | BETA: splitting (53) gives: % 73.85/10.67 | | % 73.85/10.67 | | Case 1: % 73.85/10.67 | | | % 73.85/10.67 | | | (57) ~ icext(uri_ex_c, all_29_0) % 73.85/10.67 | | | % 73.85/10.67 | | | PRED_UNIFY: (55), (57) imply: % 73.85/10.67 | | | (58) $false % 73.85/10.67 | | | % 73.85/10.67 | | | CLOSE: (58) is inconsistent. % 73.85/10.67 | | | % 73.85/10.67 | | Case 2: % 73.85/10.67 | | | % 73.85/10.67 | | | (59) icext(uri_ex_c2, all_29_0) | icext(uri_ex_c1, all_29_0) % 73.85/10.67 | | | % 73.85/10.67 | | | BETA: splitting (59) gives: % 73.85/10.67 | | | % 73.85/10.67 | | | Case 1: % 73.85/10.67 | | | | % 73.85/10.68 | | | | (60) icext(uri_ex_c2, all_29_0) % 73.85/10.68 | | | | % 73.85/10.68 | | | | GROUND_INST: instantiating (17) with all_11_5, uri_ex_c2, all_29_0, % 73.85/10.68 | | | | simplifying with (6), (20), (35), (48), (54), (60) gives: % 73.85/10.68 | | | | (61) $false % 73.85/10.68 | | | | % 73.85/10.68 | | | | CLOSE: (61) is inconsistent. % 73.85/10.68 | | | | % 73.85/10.68 | | | Case 2: % 73.85/10.68 | | | | % 73.85/10.68 | | | | (62) icext(uri_ex_c1, all_29_0) % 73.85/10.68 | | | | % 73.85/10.68 | | | | PRED_UNIFY: (56), (62) imply: % 73.85/10.68 | | | | (63) $false % 73.85/10.68 | | | | % 73.85/10.68 | | | | CLOSE: (63) is inconsistent. % 73.85/10.68 | | | | % 73.85/10.68 | | | End of split % 73.85/10.68 | | | % 73.85/10.68 | | End of split % 73.85/10.68 | | % 73.85/10.68 | End of split % 73.85/10.68 | % 73.85/10.68 End of proof % 73.85/10.68 % SZS output end Proof for theBenchmark % 73.85/10.68 % 73.85/10.68 10023ms %------------------------------------------------------------------------------