%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SWB004+2 : TPTP v9.0.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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 : Fri Jul 25 04:05:08 PM UTC 2025
% Result : Theorem 11.28s 1.78s
% Output : CNFRefutation 11.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 14
% Syntax : Number of formulae : 77 ( 27 unt; 0 def)
% Number of atoms : 171 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 164 ( 70 ~; 72 |; 12 &)
% ( 8 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 39 ( 1 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(testcase_conclusion_fullish_004_Axiomatic_Triples,plain,
( iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
& iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
& iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
& iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_004_Axiomatic_Triples) ).
fof(testcase_conclusion_fullish_004_Axiomatic_Triples_negated,plain,
~ ( iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)
& iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
& iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
& iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
& iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(negate_conjecture,[status(cth)],[testcase_conclusion_fullish_004_Axiomatic_Triples]) ).
cnf(29,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(cnf,[status(esa)],[testcase_conclusion_fullish_004_Axiomatic_Triples_negated]) ).
cnf(l0,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(instantiation,[status(thm)],[29]) ).
fof(owl_rdfsext_subclassof,plain,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ic(C1)
& ic(C2)
& ! [X] :
( icext(C1,X)
=> icext(C2,X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_rdfsext_subclassof) ).
cnf(20,plain,
( ~ icext(X0,sK1(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X1,X0) ),
inference(cnf,[status(esa)],[owl_rdfsext_subclassof]) ).
cnf(l7,plain,
( ~ icext(uri_owl_Thing,sK1(uri_owl_Class,uri_owl_Thing))
| ~ ic(uri_owl_Class)
| ~ ic(uri_owl_Thing)
| iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing) ),
inference(instantiation,[status(thm)],[20]) ).
fof(owl_class_thing_ext,plain,
! [X] :
( icext(uri_owl_Thing,X)
<=> ir(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_thing_ext) ).
cnf(15,plain,
( ~ ir(X0)
| icext(uri_owl_Thing,X0) ),
inference(cnf,[status(esa)],[owl_class_thing_ext]) ).
cnf(l17,plain,
( ~ ir(sK1(uri_owl_Class,uri_owl_Thing))
| icext(uri_owl_Thing,sK1(uri_owl_Class,uri_owl_Thing)) ),
inference(instantiation,[status(thm)],[15]) ).
fof(rdfs_cext_def,plain,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdfs_cext_def) ).
cnf(2,plain,
( ~ icext(X0,X1)
| iext(uri_rdf_type,X1,X0) ),
inference(cnf,[status(esa)],[rdfs_cext_def]) ).
cnf(l1,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(instantiation,[status(thm)],[2]) ).
fof(simple_ir,plain,
! [X] : ir(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',simple_ir) ).
cnf(0,plain,
ir(X0),
inference(cnf,[status(esa)],[simple_ir]) ).
cnf(l40,plain,
ir(sK1(uri_owl_Class,uri_owl_Thing)),
inference(instantiation,[status(thm)],[0]) ).
cnf(19,plain,
( ~ ic(X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,X0,X1)
| icext(X0,sK1(X0,X1)) ),
inference(cnf,[status(esa)],[owl_rdfsext_subclassof]) ).
cnf(l10,plain,
( ~ ic(uri_rdfs_Datatype)
| ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| icext(uri_rdfs_Datatype,sK1(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(instantiation,[status(thm)],[19]) ).
fof(owl_class_classowl_type,plain,
ic(uri_owl_Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_classowl_type) ).
cnf(4,plain,
ic(uri_owl_Class),
inference(cnf,[status(esa)],[owl_class_classowl_type]) ).
cnf(l38,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
fof(owl_class_datatype_type,plain,
ic(uri_rdfs_Datatype),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_datatype_type) ).
cnf(10,plain,
ic(uri_rdfs_Datatype),
inference(cnf,[status(esa)],[owl_class_datatype_type]) ).
cnf(l11,plain,
ic(uri_rdfs_Datatype),
inference(instantiation,[status(thm)],[10]) ).
fof(owl_class_datatype_ext,plain,
! [X] :
( icext(uri_rdfs_Datatype,X)
<=> idc(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_datatype_ext) ).
cnf(11,plain,
( ~ icext(uri_rdfs_Datatype,X0)
| idc(X0) ),
inference(cnf,[status(esa)],[owl_class_datatype_ext]) ).
cnf(l74,plain,
( ~ icext(uri_rdfs_Datatype,sK1(uri_rdfs_Datatype,uri_owl_Class))
| idc(sK1(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l2,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| iext(uri_rdf_type,uri_owl_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[2]) ).
cnf(18,plain,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| ~ icext(X0,X2)
| icext(X1,X2) ),
inference(cnf,[status(esa)],[owl_rdfsext_subclassof]) ).
cnf(l4,plain,
( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Thing)
| ~ icext(uri_rdfs_Class,uri_owl_Class)
| icext(uri_owl_Thing,uri_owl_Class) ),
inference(instantiation,[status(thm)],[18]) ).
fof(owl_eqdis_equivalentclass,plain,
! [C1,C2] :
( iext(uri_owl_equivalentClass,C1,C2)
<=> ( ic(C1)
& ic(C2)
& ! [X] :
( icext(C1,X)
<=> icext(C2,X) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_eqdis_equivalentclass) ).
cnf(25,plain,
( ~ ic(X0)
| ~ ic(X1)
| iext(uri_owl_equivalentClass,X0,X1)
| icext(X0,sK2(X0,X1))
| sP0(X1,X0) ),
inference(cnf,[status(esa)],[owl_eqdis_equivalentclass]) ).
cnf(l3,plain,
( ~ ic(uri_owl_Class)
| ~ ic(uri_rdfs_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| icext(uri_owl_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| sP0(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[25]) ).
fof(owl_parts_idc_cond_set,plain,
! [X] :
( idc(X)
=> ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_parts_idc_cond_set) ).
cnf(3,plain,
( ~ idc(X0)
| ic(X0) ),
inference(cnf,[status(esa)],[owl_parts_idc_cond_set]) ).
cnf(l551,plain,
( ~ idc(sK1(uri_rdfs_Datatype,uri_owl_Class))
| ic(sK1(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(instantiation,[status(thm)],[3]) ).
fof(owl_class_classrdfs_ext,plain,
! [X] :
( icext(uri_rdfs_Class,X)
<=> ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_classrdfs_ext) ).
cnf(9,plain,
( ~ ic(X0)
| icext(uri_rdfs_Class,X0) ),
inference(cnf,[status(esa)],[owl_class_classrdfs_ext]) ).
cnf(l18,plain,
( ~ ic(uri_owl_Class)
| icext(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[9]) ).
fof(owl_class_thing_type,plain,
ic(uri_owl_Thing),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_thing_type) ).
cnf(13,plain,
ic(uri_owl_Thing),
inference(cnf,[status(esa)],[owl_class_thing_type]) ).
cnf(l24,plain,
ic(uri_owl_Thing),
inference(instantiation,[status(thm)],[13]) ).
cnf(l21,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
cnf(l9,plain,
( ~ icext(uri_owl_Thing,sK1(uri_rdfs_Class,uri_owl_Thing))
| ~ ic(uri_rdfs_Class)
| ~ ic(uri_owl_Thing)
| iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Thing) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l79,plain,
ic(uri_owl_Thing),
inference(instantiation,[status(thm)],[13]) ).
cnf(l39,plain,
( ~ ir(sK1(uri_rdfs_Class,uri_owl_Thing))
| icext(uri_owl_Thing,sK1(uri_rdfs_Class,uri_owl_Thing)) ),
inference(instantiation,[status(thm)],[15]) ).
fof(owl_class_classrdfs_type,plain,
ic(uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_classrdfs_type) ).
cnf(7,plain,
ic(uri_rdfs_Class),
inference(cnf,[status(esa)],[owl_class_classrdfs_type]) ).
cnf(l34,plain,
ic(uri_rdfs_Class),
inference(instantiation,[status(thm)],[7]) ).
cnf(l8,plain,
ic(uri_rdfs_Class),
inference(instantiation,[status(thm)],[7]) ).
cnf(l25,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
cnf(l48,plain,
ir(sK1(uri_rdfs_Class,uri_owl_Thing)),
inference(instantiation,[status(thm)],[0]) ).
cnf(28,plain,
( icext(X0,sK2(X1,X0))
| ~ sP0(X0,X1) ),
inference(cnf,[status(esa)],[owl_eqdis_equivalentclass]) ).
cnf(l5,plain,
( icext(uri_rdfs_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ~ sP0(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l16,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
fof(owl_class_classowl_ext,plain,
! [X] :
( icext(uri_owl_Class,X)
<=> ic(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_class_classowl_ext) ).
cnf(6,plain,
( ~ ic(X0)
| icext(uri_owl_Class,X0) ),
inference(cnf,[status(esa)],[owl_class_classowl_ext]) ).
cnf(l564,plain,
( ~ ic(sK1(uri_rdfs_Datatype,uri_owl_Class))
| icext(uri_owl_Class,sK1(uri_rdfs_Datatype,uri_owl_Class)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l6,plain,
( ~ ic(uri_owl_Class)
| icext(uri_owl_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l573,plain,
( ~ icext(uri_owl_Class,sK1(uri_rdfs_Datatype,uri_owl_Class))
| ~ ic(uri_rdfs_Datatype)
| ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(27,plain,
( ~ icext(X0,sK2(X0,X1))
| ~ sP0(X1,X0) ),
inference(cnf,[status(esa)],[owl_eqdis_equivalentclass]) ).
cnf(l14,plain,
( ~ icext(uri_owl_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ~ sP0(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l720,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
cnf(8,plain,
( ~ icext(uri_rdfs_Class,X0)
| ic(X0) ),
inference(cnf,[status(esa)],[owl_class_classrdfs_ext]) ).
cnf(l36,plain,
( ~ icext(uri_rdfs_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ic(sK2(uri_owl_Class,uri_rdfs_Class)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l12,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
cnf(26,plain,
( ~ icext(X0,sK2(X1,X0))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X1,X0)
| sP0(X0,X1) ),
inference(cnf,[status(esa)],[owl_eqdis_equivalentclass]) ).
cnf(l73,plain,
( ~ icext(uri_rdfs_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ~ ic(uri_owl_Class)
| ~ ic(uri_rdfs_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| sP0(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l949,plain,
ic(uri_rdfs_Datatype),
inference(instantiation,[status(thm)],[10]) ).
cnf(l176,plain,
ic(uri_rdfs_Class),
inference(instantiation,[status(thm)],[7]) ).
cnf(l174,plain,
ic(uri_owl_Class),
inference(instantiation,[status(thm)],[4]) ).
cnf(l182,plain,
( ~ ic(sK2(uri_owl_Class,uri_rdfs_Class))
| icext(uri_rdfs_Class,sK2(uri_owl_Class,uri_rdfs_Class)) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(5,plain,
( ~ icext(uri_owl_Class,X0)
| ic(X0) ),
inference(cnf,[status(esa)],[owl_class_classowl_ext]) ).
cnf(l183,plain,
( ~ icext(uri_owl_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ic(sK2(uri_owl_Class,uri_rdfs_Class)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l280,plain,
( ~ ic(sK2(uri_owl_Class,uri_rdfs_Class))
| icext(uri_owl_Class,sK2(uri_owl_Class,uri_rdfs_Class)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l541,plain,
( ~ icext(uri_owl_Class,sK2(uri_owl_Class,uri_rdfs_Class))
| ~ sP0(uri_rdfs_Class,uri_owl_Class) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l7,l17,l1,l40,l10,l38,l11,l74,l2,l4,l3,l551,l18,l24,l21,l9,l79,l39,l34,l8,l25,l48,l5,l16,l564,l6,l573,l14,l720,l36,l12,l73,l949,l176,l174,l182,l183,l280,l541]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : SWB004+2 : TPTP v9.0.0. Released v5.2.0.
% 0.07/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Jul 22 03:52:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.35 % launching worker at depth: 11
% 0.19/0.40 % launching worker at depth: 12
% 3.04/0.73 % launching worker at depth: 13
% 11.28/1.78 % SZS status Theorem for theBenchmark
% 11.28/1.78 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------