%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWB022+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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 5.22s 1.11s
% Output : Proof 5.22s
% 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(f1,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(f1_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)],[f1]) ).
fof(f1_sk,plain,
! [S1,P1,S2,P2,P,Y0,Y1,Y2] :
( ( ( ( ~ iext(P,sk0(P,S1,P1,S2,P2),sk2(P,S1,P1,S2,P2))
& iext(P2,sk1(P,S1,P1,S2,P2),sk2(P,S1,P1,S2,P2))
& iext(P1,sk0(P,S1,P1,S2,P2),sk1(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,[sk0,sk1,sk2])],[f1_nnf]) ).
cnf(c6,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)],[f1_sk]) ).
fof(f3,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(f3_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)],[f3]) ).
fof(f3_sk,plain,
( iext(uri_rdf_rest,sk10,uri_rdf_nil)
& iext(uri_rdf_first,sk10,uri_ex_Z)
& iext(uri_rdf_rest,sk9,sk10)
& iext(uri_rdf_first,sk9,uri_ex_Y)
& iext(uri_rdf_rest,sk8,sk9)
& iext(uri_rdf_first,sk8,uri_ex_X)
& iext(uri_skos_memberList,uri_ex_MyOrderedCollection,sk8)
& iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection)
& iext(uri_rdf_rest,sk7,uri_rdf_nil)
& iext(uri_rdf_first,sk7,uri_rdf_rest)
& iext(uri_rdf_rest,sk6,sk7)
& iext(uri_rdf_first,sk6,sk3)
& iext(uri_owl_propertyChainAxiom,sk3,sk6)
& iext(uri_rdf_rest,sk5,uri_rdf_nil)
& iext(uri_rdf_first,sk5,uri_rdf_first)
& iext(uri_rdf_rest,sk4,sk5)
& iext(uri_rdf_first,sk4,sk3)
& iext(uri_owl_propertyChainAxiom,uri_skos_member,sk4)
& iext(uri_rdfs_subPropertyOf,uri_skos_memberList,sk3) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10])],[f3_nnf]) ).
cnf(c18,plain,
iext(uri_rdf_first,sk6,sk3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p81,plain,
( iext(X2,X3,X5)
| ~ iext(X1,X4,X5)
| ~ iext(sk3,X3,X4)
| ~ iext(uri_owl_propertyChainAxiom,X2,sk6)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk6,X0) ),
inference(resolution,[status(thm)],[c6,c18]) ).
cnf(c19,plain,
iext(uri_rdf_rest,sk6,sk7),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p300,plain,
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(sk3,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk7,X0) ),
inference(resolution,[status(thm)],[p81,c19]) ).
cnf(c20,plain,
iext(uri_rdf_first,sk7,uri_rdf_rest),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p490,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_rest,X2,X3)
| ~ iext(sk3,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p300,c20]) ).
cnf(c21,plain,
iext(uri_rdf_rest,sk7,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p491,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_rest,X2,X3)
| ~ iext(sk3,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk6) ),
inference(resolution,[status(thm)],[p490,c21]) ).
cnf(c17,plain,
iext(uri_owl_propertyChainAxiom,sk3,sk6),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p492,plain,
( iext(sk3,X0,X2)
| ~ iext(uri_rdf_rest,X1,X2)
| ~ iext(sk3,X0,X1) ),
inference(resolution,[status(thm)],[p491,c17]) ).
fof(f0,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(f0_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)],[f0]) ).
fof(f0_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)],[f0_nnf]) ).
cnf(c2,plain,
( iext(X1,X2,X3)
| ~ iext(X0,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(c11,plain,
iext(uri_rdfs_subPropertyOf,uri_skos_memberList,sk3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p33,plain,
( iext(sk3,X0,X1)
| ~ iext(uri_skos_memberList,X0,X1) ),
inference(resolution,[status(thm)],[c2,c11]) ).
cnf(c23,plain,
iext(uri_skos_memberList,uri_ex_MyOrderedCollection,sk8),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p50,plain,
iext(sk3,uri_ex_MyOrderedCollection,sk8),
inference(resolution,[status(thm)],[p33,c23]) ).
cnf(p494,plain,
( iext(sk3,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_rest,sk8,X0) ),
inference(resolution,[status(thm)],[p492,p50]) ).
cnf(c25,plain,
iext(uri_rdf_rest,sk8,sk9),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p495,plain,
iext(sk3,uri_ex_MyOrderedCollection,sk9),
inference(resolution,[status(thm)],[p494,c25]) ).
cnf(p497,plain,
( iext(sk3,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_rest,sk9,X0) ),
inference(resolution,[status(thm)],[p495,p492]) ).
cnf(c27,plain,
iext(uri_rdf_rest,sk9,sk10),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p500,plain,
iext(sk3,uri_ex_MyOrderedCollection,sk10),
inference(resolution,[status(thm)],[p497,c27]) ).
cnf(c13,plain,
iext(uri_rdf_first,sk4,sk3),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p79,plain,
( iext(X2,X3,X5)
| ~ iext(X1,X4,X5)
| ~ iext(sk3,X3,X4)
| ~ iext(uri_owl_propertyChainAxiom,X2,sk4)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk4,X0) ),
inference(resolution,[status(thm)],[c6,c13]) ).
cnf(c14,plain,
iext(uri_rdf_rest,sk4,sk5),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p293,plain,
( iext(X1,X2,X4)
| ~ iext(X0,X3,X4)
| ~ iext(sk3,X2,X3)
| ~ iext(uri_owl_propertyChainAxiom,X1,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk5,X0) ),
inference(resolution,[status(thm)],[p79,c14]) ).
cnf(c15,plain,
iext(uri_rdf_first,sk5,uri_rdf_first),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p482,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(sk3,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p293,c15]) ).
cnf(c16,plain,
iext(uri_rdf_rest,sk5,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p483,plain,
( iext(X0,X1,X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(sk3,X1,X2)
| ~ iext(uri_owl_propertyChainAxiom,X0,sk4) ),
inference(resolution,[status(thm)],[p482,c16]) ).
cnf(c12,plain,
iext(uri_owl_propertyChainAxiom,uri_skos_member,sk4),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p484,plain,
( iext(uri_skos_member,X0,X2)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(sk3,X0,X1) ),
inference(resolution,[status(thm)],[p483,c12]) ).
cnf(p501,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk10,X0) ),
inference(resolution,[status(thm)],[p500,p484]) ).
cnf(c28,plain,
iext(uri_rdf_first,sk10,uri_ex_Z),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p504,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),
inference(resolution,[status(thm)],[p501,c28]) ).
cnf(p496,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk9,X0) ),
inference(resolution,[status(thm)],[p495,p484]) ).
cnf(c26,plain,
iext(uri_rdf_first,sk9,uri_ex_Y),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p498,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),
inference(resolution,[status(thm)],[p496,c26]) ).
cnf(p486,plain,
( iext(uri_skos_member,uri_ex_MyOrderedCollection,X0)
| ~ iext(uri_rdf_first,sk8,X0) ),
inference(resolution,[status(thm)],[p484,p50]) ).
cnf(c24,plain,
iext(uri_rdf_first,sk8,uri_ex_X),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p487,plain,
iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),
inference(resolution,[status(thm)],[p486,c24]) ).
fof(f2,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(f2_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)],[f2]) ).
fof(f2_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)],[f2_neg]) ).
fof(f2_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)],[f2_nnf]) ).
cnf(c10,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)],[f2_sk]) ).
cnf(p488,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)],[p487,c10]) ).
cnf(p499,plain,
~ iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),
inference(resolution,[status(thm)],[p498,p488]) ).
cnf(p505,plain,
$false,
inference(resolution,[status(thm)],[p504,p499]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB022+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 15:31:48 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.22/1.11 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.22/1.11 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------