%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:51:29 AM UTC 2026
% Result : Theorem 42.39s 10.96s
% Output : CNFRefutation 42.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 6
% Syntax : Number of formulae : 53 ( 20 unt; 0 def)
% Number of atoms : 197 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 231 ( 87 ~; 84 |; 52 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 21 con; 0-1 aty)
% Number of variables : 105 ( 12 sgn 18 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(owl_bool_intersectionof_class_003,axiom,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('theBenchmark.p',owl_bool_intersectionof_class_003) ).
fof(owl_rdfsext_domain,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
file('theBenchmark.p',owl_rdfsext_domain) ).
fof(owl_restrict_hasvalue,axiom,
! [Z,P,A] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_hasValue,Z,A) )
=> ! [X] :
( icext(Z,X)
<=> iext(P,X,A) ) ),
file('theBenchmark.p',owl_restrict_hasvalue) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('theBenchmark.p',rdfs_cext_def) ).
fof(testcase_premise_fullish_012_Template_Class,axiom,
? [BNODE_l1,BNODE_l2,BNODE_l3,BNODE_r] :
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)
& iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain)
& iext(uri_rdf_type,BNODE_r,uri_owl_Restriction)
& iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l3,BNODE_r)
& iext(uri_rdf_rest,BNODE_l2,BNODE_l3)
& iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ),
file('theBenchmark.p',testcase_premise_fullish_012_Template_Class) ).
fof(testcase_conclusion_fullish_012_Template_Class,conjecture,
( iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
& iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
file('theBenchmark.p',testcase_conclusion_fullish_012_Template_Class) ).
fof(testcase_conclusion_fullish_012_Template_Class_neg,negated_conjecture,
~ ( iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
& iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_012_Template_Class]) ).
cnf(c_172,plain,
( icext(D,V7)
| ~ icext(V6,V7)
| ~ iext(uri_owl_intersectionOf,V6,A)
| ~ iext(uri_rdf_rest,E,uri_rdf_nil)
| ~ iext(uri_rdf_first,E,F)
| ~ iext(uri_rdf_rest,C,E)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_intersectionof_class_003]) ).
cnf(c_173,plain,
( icext(F,V7)
| ~ icext(V6,V7)
| ~ iext(uri_owl_intersectionOf,V6,A)
| ~ iext(uri_rdf_rest,E,uri_rdf_nil)
| ~ iext(uri_rdf_first,E,F)
| ~ iext(uri_rdf_rest,C,E)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_bool_intersectionof_class_003]) ).
cnf(c_253,plain,
( icext(B,C)
| ~ iext(A,C,D)
| ~ iext(uri_rdfs_domain,A,B) ),
inference(clausify,[status(thm)],[owl_rdfsext_domain]) ).
cnf(c_269,plain,
( iext(C,D,B)
| ~ icext(A,D)
| ~ iext(uri_owl_onProperty,A,C)
| ~ iext(uri_owl_hasValue,A,B) ),
inference(clausify,[status(thm)],[owl_restrict_hasvalue]) ).
cnf(c_278,plain,
( icext(B,A)
| ~ iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
cnf(c_279,plain,
( ~ icext(B,A)
| iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
fof(nnf_52,plain,
? [BNODE_l1,BNODE_l2,BNODE_l3,BNODE_r] :
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person)
& iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain)
& iext(uri_rdf_type,BNODE_r,uri_owl_Restriction)
& iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l3,BNODE_r)
& iext(uri_rdf_rest,BNODE_l2,BNODE_l3)
& iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_012_Template_Class]) ).
fof(sk_testcase_premise_fullish_012_Template_Class,plain,
( iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))
& iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute)
& iext(uri_owl_hasValue,sK3,uri_foaf_Person)
& iext(uri_owl_onProperty,sK3,uri_rdfs_domain)
& iext(uri_rdf_type,sK3,uri_owl_Restriction)
& iext(uri_rdf_rest,sK2,uri_rdf_nil)
& iext(uri_rdf_first,sK2,sK3)
& iext(uri_rdf_rest,sK1,sK2)
& iext(uri_rdf_first,sK1,uri_owl_FunctionalProperty)
& iext(uri_rdf_rest,sK0,sK1)
& iext(uri_rdf_first,sK0,uri_owl_DatatypeProperty)
& iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK0)
& iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(BNODE_l1,sK0),skolemize(BNODE_l2,sK1),skolemize(BNODE_l3,sK2),skolemize(BNODE_r,sK3)],[nnf_52]) ).
cnf(c_309,plain,
iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,sK0),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_310,plain,
iext(uri_rdf_first,sK0,uri_owl_DatatypeProperty),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_311,plain,
iext(uri_rdf_rest,sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_312,plain,
iext(uri_rdf_first,sK1,uri_owl_FunctionalProperty),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_313,plain,
iext(uri_rdf_rest,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_314,plain,
iext(uri_rdf_first,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_315,plain,
iext(uri_rdf_rest,sK2,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_317,plain,
iext(uri_owl_onProperty,sK3,uri_rdfs_domain),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_318,plain,
iext(uri_owl_hasValue,sK3,uri_foaf_Person),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_319,plain,
iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_320,plain,
iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_012_Template_Class]) ).
cnf(c_321,negated_conjecture,
( ~ iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)
| ~ iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty) ),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_012_Template_Class_neg]) ).
cnf(c_1170,plain,
icext(uri_ex_PersonAttribute,uri_ex_name),
inference(resolve,[status(thm)],[c_278,c_319]) ).
cnf(c_9583,plain,
( icext(B,F)
| ~ icext(E,F)
| ~ iext(uri_owl_intersectionOf,E,sK0)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK0,A) ),
inference(resolve,[status(thm)],[c_172,c_310]) ).
cnf(c_9584,plain,
( icext(A,E)
| ~ icext(D,E)
| ~ iext(uri_owl_intersectionOf,D,sK0)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_9583,c_311]) ).
cnf(c_9585,plain,
( icext(uri_owl_FunctionalProperty,D)
| ~ icext(C,D)
| ~ iext(uri_owl_intersectionOf,C,sK0)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK1,A) ),
inference(resolve,[status(thm)],[c_9584,c_312]) ).
cnf(c_9586,plain,
( icext(uri_owl_FunctionalProperty,C)
| ~ icext(B,C)
| ~ iext(uri_owl_intersectionOf,B,sK0)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK2,A) ),
inference(resolve,[status(thm)],[c_9585,c_313]) ).
cnf(c_9587,plain,
( icext(uri_owl_FunctionalProperty,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK0)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_9586,c_314]) ).
cnf(c_9588,plain,
( icext(uri_owl_FunctionalProperty,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK0) ),
inference(resolve,[status(thm)],[c_9587,c_315]) ).
cnf(c_9589,plain,
( icext(uri_owl_FunctionalProperty,A)
| ~ icext(uri_ex_PersonAttribute,A) ),
inference(resolve,[status(thm)],[c_9588,c_309]) ).
cnf(c_1459,plain,
icext(uri_owl_FunctionalProperty,uri_ex_name),
inference(resolve,[status(thm)],[c_9589,c_1170]) ).
cnf(c_1471,plain,
iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty),
inference(resolve,[status(thm)],[c_1459,c_279]) ).
cnf(c_1472,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person),
inference(resolve,[status(thm)],[c_1471,c_321]) ).
cnf(c_9590,plain,
( icext(D,F)
| ~ icext(E,F)
| ~ iext(uri_owl_intersectionOf,E,sK0)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK0,A) ),
inference(resolve,[status(thm)],[c_173,c_310]) ).
cnf(c_9591,plain,
( icext(C,E)
| ~ icext(D,E)
| ~ iext(uri_owl_intersectionOf,D,sK0)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK1,B)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_9590,c_311]) ).
cnf(c_9592,plain,
( icext(B,D)
| ~ icext(C,D)
| ~ iext(uri_owl_intersectionOf,C,sK0)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK1,A) ),
inference(resolve,[status(thm)],[c_9591,c_312]) ).
cnf(c_9593,plain,
( icext(A,C)
| ~ icext(B,C)
| ~ iext(uri_owl_intersectionOf,B,sK0)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK2,A) ),
inference(resolve,[status(thm)],[c_9592,c_313]) ).
cnf(c_9594,plain,
( icext(sK3,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK0)
| ~ iext(uri_rdf_rest,sK2,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_9593,c_314]) ).
cnf(c_9595,plain,
( icext(sK3,B)
| ~ icext(A,B)
| ~ iext(uri_owl_intersectionOf,A,sK0) ),
inference(resolve,[status(thm)],[c_9594,c_315]) ).
cnf(c_9596,plain,
( icext(sK3,A)
| ~ icext(uri_ex_PersonAttribute,A) ),
inference(resolve,[status(thm)],[c_9595,c_309]) ).
cnf(c_1491,plain,
icext(sK3,uri_ex_name),
inference(resolve,[status(thm)],[c_9596,c_1170]) ).
cnf(c_9597,plain,
( iext(A,B,uri_foaf_Person)
| ~ icext(sK3,B)
| ~ iext(uri_owl_onProperty,sK3,A) ),
inference(resolve,[status(thm)],[c_269,c_318]) ).
cnf(c_9598,plain,
( iext(uri_rdfs_domain,A,uri_foaf_Person)
| ~ icext(sK3,A) ),
inference(resolve,[status(thm)],[c_9597,c_317]) ).
cnf(c_7671,plain,
iext(uri_rdfs_domain,uri_ex_name,uri_foaf_Person),
inference(resolve,[status(thm)],[c_9598,c_1491]) ).
cnf(c_9599,plain,
( icext(uri_foaf_Person,A)
| ~ iext(uri_ex_name,A,B) ),
inference(resolve,[status(thm)],[c_253,c_7671]) ).
cnf(c_9500,plain,
icext(uri_foaf_Person,uri_ex_alice),
inference(resolve,[status(thm)],[c_9599,c_320]) ).
cnf(c_9600,plain,
iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person),
inference(resolve,[status(thm)],[c_9500,c_279]) ).
cnf(c_9582,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1472,c_9600]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB012+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n015.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sat Sep 26 11:46:34 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.38 % Process 3955826 was started by sandbox on n015,
% 0.10/5.38 % Sat Sep 26 11:46:34 2026
% 0.10/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/5.40
% 0.13/5.40 % From the command line: assign(max_seconds, 300).
% 0.13/5.40
% 0.13/5.40 % SInE: 79 to sos, 60 to usable, of 139 axioms (tolerance 2.00, depth 0 fixpoint).
% 42.39/10.96
% 42.39/10.96 % given #500 (T,wt=13): 4614 -iext(uri_rdfs_subPropertyOf,uri_rdf_type,A) | iext(A,uri_owl_DatatypeProperty,uri_rdfs_Class). [resolve(4598,a,141,b)].
% 42.39/10.96
% 42.39/10.96 % SZS status Theorem for theBenchmark
% 42.39/10.96
% 42.39/10.96 % Proof 1 at 4.86 (+ 0.51) seconds.
% 42.39/10.96 % Length of proof is 32.
% 42.39/10.96 % Level of proof is 6.
% 42.39/10.96 % Maximum clause weight is 139.000.
% 42.39/10.96 % Given clauses 871.
% 42.39/10.96
% 42.39/10.96 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------