%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWB022+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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 : Fri Sep 25 03:03:49 PM UTC 2026
% Result : Theorem 30.87s 4.93s
% Output : Proof 30.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 4
% Syntax : Number of formulae : 58 ( 25 unt; 0 def)
% Number of atoms : 234 ( 0 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 270 ( 94 ~; 88 |; 83 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-5 aty)
% Number of variables : 118 ( 0 sgn 36 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f388,axiom,
! [P,S1,P1,S2,P2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,P2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,P1) )
=> ( iext(uri_owl_propertyChainAxiom,P,S1)
<=> ( ! [Y0,Y1,Y2] :
( ( iext(P2,Y1,Y2)
& iext(P1,Y0,Y1) )
=> iext(P,Y0,Y2) )
& ip(P2)
& ip(P1)
& ip(P) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_chain_002) ).
fof(f388_nnf,plain,
! [P,S1,P1,S2,P2] :
( ( ( ? [Y0,Y1,Y2] :
( ~ iext(P,Y0,Y2)
& iext(P2,Y1,Y2)
& iext(P1,Y0,Y1) )
| ~ ip(P2)
| ~ ip(P1)
| ~ ip(P)
| iext(uri_owl_propertyChainAxiom,P,S1) )
& ( ( ! [Y0,Y1,Y2] :
( iext(P,Y0,Y2)
| ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) )
& ip(P2)
& ip(P1)
& ip(P) )
| ~ iext(uri_owl_propertyChainAxiom,P,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(nnf_transformation,[status(thm)],[f388]) ).
fof(f388_sk,plain,
! [S1,P1,S2,P2,P,Y0,Y1,Y2] :
( ( ( ( ~ iext(P,sk159(P,S1,P1,S2,P2),sk161(P,S1,P1,S2,P2))
& iext(P2,sk160(P,S1,P1,S2,P2),sk161(P,S1,P1,S2,P2))
& iext(P1,sk159(P,S1,P1,S2,P2),sk160(P,S1,P1,S2,P2)) )
| ~ ip(P2)
| ~ ip(P1)
| ~ ip(P)
| iext(uri_owl_propertyChainAxiom,P,S1) )
& ( ( ( iext(P,Y0,Y2)
| ~ iext(P2,Y1,Y2)
| ~ iext(P1,Y0,Y1) )
& ip(P2)
& ip(P1)
& ip(P) )
| ~ iext(uri_owl_propertyChainAxiom,P,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,P2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,P1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk159,sk160,sk161])],[f388_nnf]) ).
cnf(c1148,plain,
( iext(X0,X5,X7)
| ~ iext(X4,X6,X7)
| ~ iext(X2,X5,X6)
| ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f388_sk]) ).
fof(f559,axiom,
? [BNODE_pL,BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33] :
( iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_Z)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_Y)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_X)
& iext(uri_skos_memberList,uri_ex_MyOrderedCollection,BNODE_l31)
& iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_rdf_rest)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,BNODE_pL)
& iext(uri_owl_propertyChainAxiom,BNODE_pL,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_rdf_first)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,BNODE_pL)
& iext(uri_owl_propertyChainAxiom,uri_skos_member,BNODE_l11)
& iext(uri_rdfs_subPropertyOf,uri_skos_memberList,BNODE_pL) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_022_List_Member_Access) ).
fof(f559_nnf,plain,
? [BNODE_pL,BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33] :
( iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_Z)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_Y)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_X)
& iext(uri_skos_memberList,uri_ex_MyOrderedCollection,BNODE_l31)
& iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_rdf_rest)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,BNODE_pL)
& iext(uri_owl_propertyChainAxiom,BNODE_pL,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_rdf_first)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,BNODE_pL)
& iext(uri_owl_propertyChainAxiom,uri_skos_member,BNODE_l11)
& iext(uri_rdfs_subPropertyOf,uri_skos_memberList,BNODE_pL) ),
inference(nnf_transformation,[status(thm)],[f559]) ).
fof(f559_sk,plain,
( iext(uri_rdf_rest,sk206,uri_rdf_nil)
& iext(uri_rdf_first,sk206,uri_ex_Z)
& iext(uri_rdf_rest,sk205,sk206)
& iext(uri_rdf_first,sk205,uri_ex_Y)
& iext(uri_rdf_rest,sk204,sk205)
& iext(uri_rdf_first,sk204,uri_ex_X)
& iext(uri_skos_memberList,uri_ex_MyOrderedCollection,sk204)
& iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection)
& iext(uri_rdf_rest,sk203,uri_rdf_nil)
& iext(uri_rdf_first,sk203,uri_rdf_rest)
& iext(uri_rdf_rest,sk202,sk203)
& iext(uri_rdf_first,sk202,sk199)
& iext(uri_owl_propertyChainAxiom,sk199,sk202)
& iext(uri_rdf_rest,sk201,uri_rdf_nil)
& iext(uri_rdf_first,sk201,uri_rdf_first)
& iext(uri_rdf_rest,sk200,sk201)
& iext(uri_rdf_first,sk200,sk199)
& iext(uri_owl_propertyChainAxiom,uri_skos_member,sk200)
& iext(uri_rdfs_subPropertyOf,uri_skos_memberList,sk199) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk199,sk200,sk201,sk202,sk203,sk204,sk205,sk206])],[f559_nnf]) ).
cnf(c1414,plain,
iext(uri_rdf_first,sk202,sk199),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4034,plain,
( iext(X2,X3,X5)
| ~ iext(X1,X4,X5)
| ~ iext(sk199,X3,X4)
| ~ iext(uri_owl_propertyChainAxiom,X2,sk202)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk202,X0) ),
inference(resolution,[status(thm)],[c1148,c1414]) ).
cnf(c1415,plain,
iext(uri_rdf_rest,sk202,sk203),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4218,plain,
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(sk199,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sk202)
| ~ iext(uri_rdf_rest,sk203,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk203,X0) ),
inference(resolution,[status(thm)],[p4034,c1415]) ).
cnf(c1416,plain,
iext(uri_rdf_first,sk203,uri_rdf_rest),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4219,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_rest,X2,X3)
| ~ iext(sk199,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk202)
| ~ iext(uri_rdf_rest,sk203,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p4218,c1416]) ).
cnf(c1417,plain,
iext(uri_rdf_rest,sk203,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4220,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_rest,X2,X3)
| ~ iext(sk199,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk202) ),
inference(resolution,[status(thm)],[p4219,c1417]) ).
cnf(c1413,plain,
iext(uri_owl_propertyChainAxiom,sk199,sk202),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4221,plain,
( iext(sk199,X0,X2)
| ~ iext(uri_rdf_rest,X1,X2)
| ~ iext(sk199,X0,X1) ),
inference(resolution,[status(thm)],[p4220,c1413]) ).
fof(f72,axiom,
! [P,Q] :
( iext(uri_rdfs_subPropertyOf,P,Q)
=> ( ! [X,Y] :
( iext(P,X,Y)
=> iext(Q,X,Y) )
& ip(Q)
& ip(P) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdfs_subpropertyof_main) ).
fof(f72_nnf,plain,
! [P,Q] :
( ( ! [X,Y] :
( iext(Q,X,Y)
| ~ iext(P,X,Y) )
& ip(Q)
& ip(P) )
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(nnf_transformation,[status(thm)],[f72]) ).
fof(f72_sk,plain,
! [P,Q,X,Y] :
( ( ( iext(Q,X,Y)
| ~ iext(P,X,Y) )
& ip(Q)
& ip(P) )
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(skolemisation,[status(esa)],[f72_nnf]) ).
cnf(c81,plain,
( iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f72_sk]) ).
cnf(c1407,plain,
iext(uri_rdfs_subPropertyOf,uri_skos_memberList,sk199),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p1994,plain,
( iext(sk199,X0,X1)
| ~ iext(uri_skos_memberList,X0,X1) ),
inference(resolution,[status(thm)],[c81,c1407]) ).
cnf(c1419,plain,
iext(uri_skos_memberList,uri_ex_MyOrderedCollection,sk204),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p1995,plain,
iext(sk199,uri_ex_MyOrderedCollection,sk204),
inference(resolution,[status(thm)],[p1994,c1419]) ).
cnf(p4223,plain,
( iext(sk199,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_rest,sk204,X0) ),
inference(resolution,[status(thm)],[p4221,p1995]) ).
cnf(c1421,plain,
iext(uri_rdf_rest,sk204,sk205),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4225,plain,
iext(sk199,uri_ex_MyOrderedCollection,sk205),
inference(resolution,[status(thm)],[p4223,c1421]) ).
cnf(p4227,plain,
( iext(sk199,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_rest,sk205,X0) ),
inference(resolution,[status(thm)],[p4225,p4221]) ).
cnf(c1423,plain,
iext(uri_rdf_rest,sk205,sk206),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4230,plain,
iext(sk199,uri_ex_MyOrderedCollection,sk206),
inference(resolution,[status(thm)],[p4227,c1423]) ).
cnf(c1409,plain,
iext(uri_rdf_first,sk200,sk199),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4032,plain,
( iext(X2,X3,X5)
| ~ iext(X1,X4,X5)
| ~ iext(sk199,X3,X4)
| ~ iext(uri_owl_propertyChainAxiom,X2,sk200)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk200,X0) ),
inference(resolution,[status(thm)],[c1148,c1409]) ).
cnf(c1410,plain,
iext(uri_rdf_rest,sk200,sk201),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4208,plain,
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(sk199,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sk200)
| ~ iext(uri_rdf_rest,sk201,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk201,X0) ),
inference(resolution,[status(thm)],[p4032,c1410]) ).
cnf(c1411,plain,
iext(uri_rdf_first,sk201,uri_rdf_first),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4209,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(sk199,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk200)
| ~ iext(uri_rdf_rest,sk201,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p4208,c1411]) ).
cnf(c1412,plain,
iext(uri_rdf_rest,sk201,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4210,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(sk199,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk200) ),
inference(resolution,[status(thm)],[p4209,c1412]) ).
cnf(c1408,plain,
iext(uri_owl_propertyChainAxiom,uri_skos_member,sk200),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4211,plain,
( iext(uri_skos_member,X0,X2)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(sk199,X0,X1) ),
inference(resolution,[status(thm)],[p4210,c1408]) ).
cnf(p4231,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk206,X0) ),
inference(resolution,[status(thm)],[p4230,p4211]) ).
cnf(c1424,plain,
iext(uri_rdf_first,sk206,uri_ex_Z),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4233,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),
inference(resolution,[status(thm)],[p4231,c1424]) ).
cnf(p4226,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk205,X0) ),
inference(resolution,[status(thm)],[p4225,p4211]) ).
cnf(c1422,plain,
iext(uri_rdf_first,sk205,uri_ex_Y),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4228,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),
inference(resolution,[status(thm)],[p4226,c1422]) ).
cnf(p4213,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk204,X0) ),
inference(resolution,[status(thm)],[p4211,p1995]) ).
cnf(c1420,plain,
iext(uri_rdf_first,sk204,uri_ex_X),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(p4215,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),
inference(resolution,[status(thm)],[p4213,c1420]) ).
fof(f558,conjecture,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
& iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)
& iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_022_List_Member_Access) ).
fof(f558_neg,negated_conjecture,
~ ( iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
& iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)
& iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) ),
inference(negated_conjecture,[status(cth)],[f558]) ).
fof(f558_nnf,plain,
( ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) ),
inference(nnf_transformation,[status(thm)],[f558_neg]) ).
fof(f558_sk,plain,
( ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) ),
inference(skolemisation,[status(esa)],[f558_nnf]) ).
cnf(c1406,plain,
( ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) ),
inference(cnf_transformation,[status(esa)],[f558_sk]) ).
cnf(p4216,plain,
( ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)
| ~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y) ),
inference(resolution,[status(thm)],[p4215,c1406]) ).
cnf(p4229,plain,
~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),
inference(resolution,[status(thm)],[p4228,p4216]) ).
cnf(p4234,plain,
$false,
inference(resolution,[status(thm)],[p4233,p4229]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB022+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.40 % Computer : n019.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Thu Sep 24 15:31:19 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 30.87/4.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.87/4.93 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------