%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n012.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:48 PM UTC 2026
% Result : Theorem 5.23s 1.13s
% Output : Proof 5.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 8
% Syntax : Number of formulae : 169 ( 31 unt; 0 def)
% Number of atoms : 878 ( 189 equ)
% Maximal formula atoms : 26 ( 5 avg)
% Number of connectives : 1135 ( 426 ~; 547 |; 149 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 23 con; 0-7 aty)
% Number of variables : 369 ( 30 sgn 81 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,A3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A3
| X = A2
| X = A1 ) )
& ic(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_enum_class_003) ).
fof(f4_nnf,plain,
! [Z,S1,A1,S2,A2,S3,A3] :
( ( ( ? [X] :
( ( ( X = A3
| X = A2
| X = A1 )
& ~ icext(Z,X) )
| ( X != A3
& X != A2
& X != A1
& icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( ( X != A3
& X != A2
& X != A1 )
| icext(Z,X) )
& ( X = A3
| X = A2
| X = A1
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [S1,A1,S2,A2,S3,A3,Z,X] :
( ( ( ( ( sk2(Z,S1,A1,S2,A2,S3,A3) = A3
| sk2(Z,S1,A1,S2,A2,S3,A3) = A2
| sk2(Z,S1,A1,S2,A2,S3,A3) = A1 )
& ~ icext(Z,sk2(Z,S1,A1,S2,A2,S3,A3)) )
| ( sk2(Z,S1,A1,S2,A2,S3,A3) != A3
& sk2(Z,S1,A1,S2,A2,S3,A3) != A2
& sk2(Z,S1,A1,S2,A2,S3,A3) != A1
& icext(Z,sk2(Z,S1,A1,S2,A2,S3,A3)) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ( ( X != A3
& X != A2
& X != A1 )
| icext(Z,X) )
& ( X = A3
| X = A2
| X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,A3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f4_nnf]) ).
cnf(c27,plain,
( X7 = X6
| X7 = X4
| X7 = X2
| ~ icext(X0,X7)
| ~ iext(uri_owl_oneOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
fof(f7,axiom,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33,BNODE_l41,BNODE_l42] :
( iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_l41,BNODE_l42)
& iext(uri_rdf_first,BNODE_l41,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41)
& iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_premise_fullish_021_Composite_Enumerations) ).
fof(f7_nnf,plain,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l31,BNODE_l32,BNODE_l33,BNODE_l41,BNODE_l42] :
( iext(uri_rdf_rest,BNODE_l42,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l42,uri_ex_c2)
& iext(uri_rdf_rest,BNODE_l41,BNODE_l42)
& iext(uri_rdf_first,BNODE_l41,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,BNODE_l41)
& iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l33,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l32,BNODE_l33)
& iext(uri_rdf_first,BNODE_l32,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l31,BNODE_l32)
& iext(uri_rdf_first,BNODE_l31,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,BNODE_l31)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,uri_ex_w3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_w2)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,BNODE_l11) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
( iext(uri_rdf_rest,sk12,uri_rdf_nil)
& iext(uri_rdf_first,sk12,uri_ex_c2)
& iext(uri_rdf_rest,sk11,sk12)
& iext(uri_rdf_first,sk11,uri_ex_c1)
& iext(uri_owl_unionOf,uri_ex_c4,sk11)
& iext(uri_rdf_rest,sk10,uri_rdf_nil)
& iext(uri_rdf_first,sk10,uri_ex_w3)
& iext(uri_rdf_rest,sk9,sk10)
& iext(uri_rdf_first,sk9,uri_ex_w2)
& iext(uri_rdf_rest,sk8,sk9)
& iext(uri_rdf_first,sk8,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c3,sk8)
& iext(uri_rdf_rest,sk7,uri_rdf_nil)
& iext(uri_rdf_first,sk7,uri_ex_w3)
& iext(uri_rdf_rest,sk6,sk7)
& iext(uri_rdf_first,sk6,uri_ex_w2)
& iext(uri_owl_oneOf,uri_ex_c2,sk6)
& iext(uri_rdf_rest,sk5,uri_rdf_nil)
& iext(uri_rdf_first,sk5,uri_ex_w2)
& iext(uri_rdf_rest,sk4,sk5)
& iext(uri_rdf_first,sk4,uri_ex_w1)
& iext(uri_owl_oneOf,uri_ex_c1,sk4) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12])],[f7_nnf]) ).
cnf(c59,plain,
iext(uri_rdf_first,sk8,uri_ex_w1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1226,plain,
( X5 = X3
| X5 = X1
| X5 = uri_ex_w1
| ~ icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,sk8)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk8,X0) ),
inference(resolution,[status(thm)],[c27,c59]) ).
cnf(c60,plain,
iext(uri_rdf_rest,sk8,sk9),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1560,plain,
( X4 = X2
| X4 = X0
| X4 = uri_ex_w1
| ~ icext(X3,X4)
| ~ iext(uri_owl_oneOf,X3,sk8)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sk9,X1)
| ~ iext(uri_rdf_first,sk9,X0) ),
inference(resolution,[status(thm)],[p1226,c60]) ).
cnf(c61,plain,
iext(uri_rdf_first,sk9,uri_ex_w2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1570,plain,
( X3 = X1
| X3 = uri_ex_w2
| X3 = uri_ex_w1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,sk8)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk9,X0) ),
inference(resolution,[status(thm)],[p1560,c61]) ).
cnf(c62,plain,
iext(uri_rdf_rest,sk9,sk10),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1579,plain,
( X2 = X0
| X2 = uri_ex_w2
| X2 = uri_ex_w1
| ~ icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk10,X0) ),
inference(resolution,[status(thm)],[p1570,c62]) ).
cnf(c63,plain,
iext(uri_rdf_first,sk10,uri_ex_w3),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1588,plain,
( X1 = uri_ex_w3
| X1 = uri_ex_w2
| X1 = uri_ex_w1
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p1579,c63]) ).
cnf(c64,plain,
iext(uri_rdf_rest,sk10,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1595,plain,
( X1 = uri_ex_w3
| X1 = uri_ex_w2
| X1 = uri_ex_w1
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8) ),
inference(resolution,[status(thm)],[p1588,c64]) ).
cnf(c58,plain,
iext(uri_owl_oneOf,uri_ex_c3,sk8),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1602,plain,
( X0 = uri_ex_w3
| X0 = uri_ex_w2
| X0 = uri_ex_w1
| ~ icext(uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[p1595,c58]) ).
fof(f3,axiom,
! [Z,S1,A1,S2,A2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,A2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( X = A2
| X = A1 ) )
& ic(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_enum_class_002) ).
fof(f3_nnf,plain,
! [Z,S1,A1,S2,A2] :
( ( ( ? [X] :
( ( ( X = A2
| X = A1 )
& ~ icext(Z,X) )
| ( X != A2
& X != A1
& icext(Z,X) ) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ! [X] :
( ( ( X != A2
& X != A1 )
| icext(Z,X) )
& ( X = A2
| X = A1
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [S1,A1,S2,A2,Z,X] :
( ( ( ( ( sk1(Z,S1,A1,S2,A2) = A2
| sk1(Z,S1,A1,S2,A2) = A1 )
& ~ icext(Z,sk1(Z,S1,A1,S2,A2)) )
| ( sk1(Z,S1,A1,S2,A2) != A2
& sk1(Z,S1,A1,S2,A2) != A1
& icext(Z,sk1(Z,S1,A1,S2,A2)) )
| ~ ic(Z)
| iext(uri_owl_oneOf,Z,S1) )
& ( ( ( ( X != A2
& X != A1 )
| icext(Z,X) )
& ( X = A2
| X = A1
| ~ icext(Z,X) )
& ic(Z) )
| ~ iext(uri_owl_oneOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,A2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,A1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f3_nnf]) ).
cnf(c17,plain,
( X5 = X4
| X5 = X2
| ~ icext(X0,X5)
| ~ iext(uri_owl_oneOf,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)],[f3_sk]) ).
cnf(c54,plain,
iext(uri_rdf_first,sk6,uri_ex_w2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p502,plain,
( X3 = X1
| X3 = uri_ex_w2
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,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)],[c17,c54]) ).
cnf(c55,plain,
iext(uri_rdf_rest,sk6,sk7),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p575,plain,
( X2 = X0
| X2 = uri_ex_w2
| ~ icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk7,X0) ),
inference(resolution,[status(thm)],[p502,c55]) ).
cnf(c56,plain,
iext(uri_rdf_first,sk7,uri_ex_w3),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p579,plain,
( X1 = uri_ex_w3
| X1 = uri_ex_w2
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p575,c56]) ).
cnf(c57,plain,
iext(uri_rdf_rest,sk7,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p582,plain,
( X1 = uri_ex_w3
| X1 = uri_ex_w2
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6) ),
inference(resolution,[status(thm)],[p579,c57]) ).
cnf(c53,plain,
iext(uri_owl_oneOf,uri_ex_c2,sk6),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p585,plain,
( X0 = uri_ex_w3
| X0 = uri_ex_w2
| ~ icext(uri_ex_c2,X0) ),
inference(resolution,[status(thm)],[p582,c53]) ).
fof(f2,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
| icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_bool_unionof_class_002) ).
fof(f2_nnf,plain,
! [Z,S1,C1,S2,C2] :
( ( ( ? [X] :
( ( ( icext(C2,X)
| icext(C1,X) )
& ~ icext(Z,X) )
| ( ~ icext(C2,X)
& ~ icext(C1,X)
& icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,S1) )
& ( ( ! [X] :
( ( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(Z,X) )
& ( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [S1,C1,S2,C2,Z,X] :
( ( ( ( ( icext(C2,sk0(Z,S1,C1,S2,C2))
| icext(C1,sk0(Z,S1,C1,S2,C2)) )
& ~ icext(Z,sk0(Z,S1,C1,S2,C2)) )
| ( ~ icext(C2,sk0(Z,S1,C1,S2,C2))
& ~ icext(C1,sk0(Z,S1,C1,S2,C2))
& icext(Z,sk0(Z,S1,C1,S2,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_unionOf,Z,S1) )
& ( ( ( ( ~ icext(C2,X)
& ~ icext(C1,X) )
| icext(Z,X) )
& ( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f2_nnf]) ).
cnf(c7,plain,
( icext(X4,X5)
| icext(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_unionOf,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)],[f2_sk]) ).
cnf(c66,plain,
iext(uri_rdf_first,sk11,uri_ex_c1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p432,plain,
( icext(X1,X3)
| icext(uri_ex_c1,X3)
| ~ icext(X2,X3)
| ~ iext(uri_owl_unionOf,X2,sk11)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk11,X0) ),
inference(resolution,[status(thm)],[c7,c66]) ).
cnf(c67,plain,
iext(uri_rdf_rest,sk11,sk12),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p475,plain,
( icext(X0,X2)
| icext(uri_ex_c1,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk12,X0) ),
inference(resolution,[status(thm)],[p432,c67]) ).
cnf(c68,plain,
iext(uri_rdf_first,sk12,uri_ex_c2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p477,plain,
( icext(uri_ex_c2,X1)
| icext(uri_ex_c1,X1)
| ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p475,c68]) ).
cnf(c69,plain,
iext(uri_rdf_rest,sk12,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p478,plain,
( icext(uri_ex_c2,X1)
| icext(uri_ex_c1,X1)
| ~ icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11) ),
inference(resolution,[status(thm)],[p477,c69]) ).
cnf(c65,plain,
iext(uri_owl_unionOf,uri_ex_c4,sk11),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p479,plain,
( icext(uri_ex_c2,X0)
| icext(uri_ex_c1,X0)
| ~ icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[p478,c65]) ).
fof(f5,axiom,
! [C1,C2] :
( iext(uri_owl_equivalentClass,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
<=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_eqdis_equivalentclass) ).
fof(f5_nnf,plain,
! [C1,C2] :
( ( ? [X] :
( ( icext(C2,X)
& ~ icext(C1,X) )
| ( ~ icext(C2,X)
& icext(C1,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ( ( ! [X] :
( ( ~ icext(C2,X)
| icext(C1,X) )
& ( icext(C2,X)
| ~ icext(C1,X) ) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [C1,C2,X] :
( ( ( icext(C2,sk3(C1,C2))
& ~ icext(C1,sk3(C1,C2)) )
| ( ~ icext(C2,sk3(C1,C2))
& icext(C1,sk3(C1,C2)) )
| ~ ic(C2)
| ~ ic(C1)
| iext(uri_owl_equivalentClass,C1,C2) )
& ( ( ( ~ icext(C2,X)
| icext(C1,X) )
& ( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_owl_equivalentClass,C1,C2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3])],[f5_nnf]) ).
cnf(c44,plain,
( icext(X1,sk3(X0,X1))
| icext(X0,sk3(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f0,axiom,
! [X,Y] :
( iext(uri_owl_oneOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_prop_oneof_ext) ).
fof(f0_nnf,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_oneOf,X,Y) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_oneOf,X,Y) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( ic(X0)
| ~ iext(uri_owl_oneOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p72,plain,
ic(uri_ex_c3),
inference(resolution,[status(thm)],[c0,c58]) ).
cnf(p82,plain,
( icext(X0,sk3(uri_ex_c3,X0))
| icext(uri_ex_c3,sk3(uri_ex_c3,X0))
| ~ ic(X0)
| iext(uri_owl_equivalentClass,uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[c44,p72]) ).
fof(f1,axiom,
! [X,Y] :
( iext(uri_owl_unionOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',owl_prop_unionof_ext) ).
fof(f1_nnf,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_unionOf,X,Y) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_unionOf,X,Y) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c2,plain,
( ic(X0)
| ~ iext(uri_owl_unionOf,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p73,plain,
ic(uri_ex_c4),
inference(resolution,[status(thm)],[c2,c65]) ).
cnf(p97,plain,
( icext(uri_ex_c4,sk3(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p82,p73]) ).
cnf(p480,plain,
( icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| icext(uri_ex_c2,sk3(uri_ex_c3,uri_ex_c4))
| icext(uri_ex_c1,sk3(uri_ex_c3,uri_ex_c4)) ),
inference(resolution,[status(thm)],[p479,p97]) ).
cnf(p594,plain,
( icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| icext(uri_ex_c1,sk3(uri_ex_c3,uri_ex_c4))
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolution,[status(thm)],[p585,p480]) ).
cnf(c49,plain,
iext(uri_rdf_first,sk4,uri_ex_w1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p500,plain,
( X3 = X1
| X3 = uri_ex_w1
| ~ icext(X2,X3)
| ~ iext(uri_owl_oneOf,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)],[c17,c49]) ).
cnf(c50,plain,
iext(uri_rdf_rest,sk4,sk5),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p524,plain,
( X2 = X0
| X2 = uri_ex_w1
| ~ icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk5,X0) ),
inference(resolution,[status(thm)],[p500,c50]) ).
cnf(c51,plain,
iext(uri_rdf_first,sk5,uri_ex_w2),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p528,plain,
( X1 = uri_ex_w2
| X1 = uri_ex_w1
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p524,c51]) ).
cnf(c52,plain,
iext(uri_rdf_rest,sk5,uri_rdf_nil),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p531,plain,
( X1 = uri_ex_w2
| X1 = uri_ex_w1
| ~ icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk4) ),
inference(resolution,[status(thm)],[p528,c52]) ).
cnf(c48,plain,
iext(uri_owl_oneOf,uri_ex_c1,sk4),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p534,plain,
( X0 = uri_ex_w2
| X0 = uri_ex_w1
| ~ icext(uri_ex_c1,X0) ),
inference(resolution,[status(thm)],[p531,c48]) ).
cnf(p703,plain,
( sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(resolution,[status(thm)],[p594,p534]) ).
cnf(p832,plain,
( sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2 ),
inference(factoring,[status(thm)],[p703]) ).
cnf(p1613,plain,
( sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p1602,p832]) ).
cnf(p2492,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p1613]) ).
cnf(p2495,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2492]) ).
cnf(p2497,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w3
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2495]) ).
cnf(c19,plain,
( X5 != X4
| icext(X0,X5)
| ~ iext(uri_owl_oneOf,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)],[f3_sk]) ).
cnf(p365,plain,
( X3 != X1
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,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)],[c19,c54]) ).
cnf(p385,plain,
( X2 != X0
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk7,X0) ),
inference(resolution,[status(thm)],[p365,c55]) ).
cnf(p387,plain,
( X1 != uri_ex_w3
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p385,c56]) ).
cnf(p389,plain,
( X1 != uri_ex_w3
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6) ),
inference(resolution,[status(thm)],[p387,c57]) ).
cnf(p391,plain,
( X0 != uri_ex_w3
| icext(uri_ex_c2,X0) ),
inference(resolution,[status(thm)],[p389,c53]) ).
cnf(p2499,plain,
( icext(uri_ex_c2,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2497,p391]) ).
cnf(c9,plain,
( ~ icext(X4,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,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)],[f2_sk]) ).
cnf(p243,plain,
( ~ icext(X1,X3)
| icext(X2,X3)
| ~ iext(uri_owl_unionOf,X2,sk11)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk11,X0) ),
inference(resolution,[status(thm)],[c9,c66]) ).
cnf(p259,plain,
( ~ icext(X0,X2)
| icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk12,X0) ),
inference(resolution,[status(thm)],[p243,c67]) ).
cnf(p260,plain,
( ~ icext(uri_ex_c2,X1)
| icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p259,c68]) ).
cnf(p261,plain,
( ~ icext(uri_ex_c2,X1)
| icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11) ),
inference(resolution,[status(thm)],[p260,c69]) ).
cnf(p262,plain,
( ~ icext(uri_ex_c2,X0)
| icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[p261,c65]) ).
cnf(p2503,plain,
( icext(uri_ex_c4,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2499,p262]) ).
cnf(c45,plain,
( ~ icext(X0,sk3(X0,X1))
| ~ icext(X1,sk3(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_owl_equivalentClass,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p105,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,X0))
| ~ icext(X0,sk3(uri_ex_c3,X0))
| ~ ic(X0)
| iext(uri_owl_equivalentClass,uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[c45,p72]) ).
cnf(p128,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| ~ icext(uri_ex_c4,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p105,p73]) ).
cnf(p2508,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2503,p128]) ).
cnf(p2509,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2508]) ).
cnf(c30,plain,
( X7 != X6
| icext(X0,X7)
| ~ iext(uri_owl_oneOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1050,plain,
( X5 != X3
| icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,sk8)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk8,X0) ),
inference(resolution,[status(thm)],[c30,c59]) ).
cnf(p1076,plain,
( X4 != X2
| icext(X3,X4)
| ~ iext(uri_owl_oneOf,X3,sk8)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sk9,X1)
| ~ iext(uri_rdf_first,sk9,X0) ),
inference(resolution,[status(thm)],[p1050,c60]) ).
cnf(p1078,plain,
( X3 != X1
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,sk8)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk9,X0) ),
inference(resolution,[status(thm)],[p1076,c61]) ).
cnf(p1080,plain,
( X2 != X0
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk10,X0) ),
inference(resolution,[status(thm)],[p1078,c62]) ).
cnf(p1082,plain,
( X1 != uri_ex_w3
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p1080,c63]) ).
cnf(p1084,plain,
( X1 != uri_ex_w3
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8) ),
inference(resolution,[status(thm)],[p1082,c64]) ).
cnf(p1086,plain,
( X0 != uri_ex_w3
| icext(uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[p1084,c58]) ).
cnf(p2500,plain,
( icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2497,p1086]) ).
cnf(p2513,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2509,p2500]) ).
cnf(p2529,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2513]) ).
cnf(p2532,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2529]) ).
cnf(p2534,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w2
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2532]) ).
cnf(c18,plain,
( X5 != X2
| icext(X0,X5)
| ~ iext(uri_owl_oneOf,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)],[f3_sk]) ).
cnf(p283,plain,
( X3 != uri_ex_w2
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,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)],[c18,c54]) ).
cnf(p325,plain,
( X2 != uri_ex_w2
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk7,X0) ),
inference(resolution,[status(thm)],[p283,c55]) ).
cnf(p327,plain,
( X1 != uri_ex_w2
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6)
| ~ iext(uri_rdf_rest,sk7,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p325,c56]) ).
cnf(p329,plain,
( X1 != uri_ex_w2
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk6) ),
inference(resolution,[status(thm)],[p327,c57]) ).
cnf(p331,plain,
( X0 != uri_ex_w2
| icext(uri_ex_c2,X0) ),
inference(resolution,[status(thm)],[p329,c53]) ).
cnf(p2536,plain,
( icext(uri_ex_c2,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2534,p331]) ).
cnf(p2539,plain,
( icext(uri_ex_c4,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2536,p262]) ).
cnf(p2540,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2539,p128]) ).
cnf(p2541,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2540]) ).
cnf(c29,plain,
( X7 != X4
| icext(X0,X7)
| ~ iext(uri_owl_oneOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p944,plain,
( X5 != X1
| icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,sk8)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk8,X0) ),
inference(resolution,[status(thm)],[c29,c59]) ).
cnf(p1021,plain,
( X4 != X0
| icext(X3,X4)
| ~ iext(uri_owl_oneOf,X3,sk8)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sk9,X1)
| ~ iext(uri_rdf_first,sk9,X0) ),
inference(resolution,[status(thm)],[p944,c60]) ).
cnf(p1023,plain,
( X3 != uri_ex_w2
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,sk8)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk9,X0) ),
inference(resolution,[status(thm)],[p1021,c61]) ).
cnf(p1025,plain,
( X2 != uri_ex_w2
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk10,X0) ),
inference(resolution,[status(thm)],[p1023,c62]) ).
cnf(p1027,plain,
( X1 != uri_ex_w2
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p1025,c63]) ).
cnf(p1029,plain,
( X1 != uri_ex_w2
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8) ),
inference(resolution,[status(thm)],[p1027,c64]) ).
cnf(p1031,plain,
( X0 != uri_ex_w2
| icext(uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[p1029,c58]) ).
cnf(p2538,plain,
( icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2534,p1031]) ).
cnf(p2543,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(resolution,[status(thm)],[p2541,p2538]) ).
cnf(p2544,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2543]) ).
cnf(p2546,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| sk3(uri_ex_c3,uri_ex_c4) = uri_ex_w1 ),
inference(factoring,[status(thm)],[p2544]) ).
cnf(p281,plain,
( X3 != uri_ex_w1
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,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)],[c18,c49]) ).
cnf(p312,plain,
( X2 != uri_ex_w1
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk5,X0) ),
inference(resolution,[status(thm)],[p281,c50]) ).
cnf(p314,plain,
( X1 != uri_ex_w1
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk4)
| ~ iext(uri_rdf_rest,sk5,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p312,c51]) ).
cnf(p316,plain,
( X1 != uri_ex_w1
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk4) ),
inference(resolution,[status(thm)],[p314,c52]) ).
cnf(p318,plain,
( X0 != uri_ex_w1
| icext(uri_ex_c1,X0) ),
inference(resolution,[status(thm)],[p316,c48]) ).
cnf(p2548,plain,
( icext(uri_ex_c1,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p2546,p318]) ).
cnf(c8,plain,
( ~ icext(X2,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,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)],[f2_sk]) ).
cnf(p197,plain,
( ~ icext(uri_ex_c1,X3)
| icext(X2,X3)
| ~ iext(uri_owl_unionOf,X2,sk11)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk11,X0) ),
inference(resolution,[status(thm)],[c8,c66]) ).
cnf(p223,plain,
( ~ icext(uri_ex_c1,X2)
| icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk12,X0) ),
inference(resolution,[status(thm)],[p197,c67]) ).
cnf(p224,plain,
( ~ icext(uri_ex_c1,X1)
| icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11)
| ~ iext(uri_rdf_rest,sk12,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p223,c68]) ).
cnf(p225,plain,
( ~ icext(uri_ex_c1,X1)
| icext(X0,X1)
| ~ iext(uri_owl_unionOf,X0,sk11) ),
inference(resolution,[status(thm)],[p224,c69]) ).
cnf(p226,plain,
( ~ icext(uri_ex_c1,X0)
| icext(uri_ex_c4,X0) ),
inference(resolution,[status(thm)],[p225,c65]) ).
cnf(p2550,plain,
( icext(uri_ex_c4,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p2548,p226]) ).
cnf(p2551,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p2550,p128]) ).
cnf(p2552,plain,
( ~ icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(factoring,[status(thm)],[p2551]) ).
cnf(c28,plain,
( X7 != X2
| icext(X0,X7)
| ~ iext(uri_owl_oneOf,X0,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X1,X3)
| ~ iext(uri_rdf_first,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p872,plain,
( X5 != uri_ex_w1
| icext(X4,X5)
| ~ iext(uri_owl_oneOf,X4,sk8)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X0,X2)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk8,X0) ),
inference(resolution,[status(thm)],[c28,c59]) ).
cnf(p917,plain,
( X4 != uri_ex_w1
| icext(X3,X4)
| ~ iext(uri_owl_oneOf,X3,sk8)
| ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_rdf_rest,sk9,X1)
| ~ iext(uri_rdf_first,sk9,X0) ),
inference(resolution,[status(thm)],[p872,c60]) ).
cnf(p919,plain,
( X3 != uri_ex_w1
| icext(X2,X3)
| ~ iext(uri_owl_oneOf,X2,sk8)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sk9,X0) ),
inference(resolution,[status(thm)],[p917,c61]) ).
cnf(p921,plain,
( X2 != uri_ex_w1
| icext(X1,X2)
| ~ iext(uri_owl_oneOf,X1,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil)
| ~ iext(uri_rdf_first,sk10,X0) ),
inference(resolution,[status(thm)],[p919,c62]) ).
cnf(p923,plain,
( X1 != uri_ex_w1
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8)
| ~ iext(uri_rdf_rest,sk10,uri_rdf_nil) ),
inference(resolution,[status(thm)],[p921,c63]) ).
cnf(p925,plain,
( X1 != uri_ex_w1
| icext(X0,X1)
| ~ iext(uri_owl_oneOf,X0,sk8) ),
inference(resolution,[status(thm)],[p923,c64]) ).
cnf(p927,plain,
( X0 != uri_ex_w1
| icext(uri_ex_c3,X0) ),
inference(resolution,[status(thm)],[p925,c58]) ).
cnf(p2549,plain,
( icext(uri_ex_c3,sk3(uri_ex_c3,uri_ex_c4))
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p2546,p927]) ).
cnf(p2554,plain,
( iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)
| iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4) ),
inference(resolution,[status(thm)],[p2552,p2549]) ).
cnf(p2555,plain,
iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(factoring,[status(thm)],[p2554]) ).
fof(f6,conjecture,
iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_conclusion_fullish_021_Composite_Enumerations) ).
fof(f6_neg,negated_conjecture,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f6_nnf,plain,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(nnf_transformation,[status(thm)],[f6_neg]) ).
fof(f6_sk,plain,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c47,plain,
~ iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p2556,plain,
$false,
inference(resolution,[status(thm)],[p2555,c47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWB021+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Thu Sep 24 15:30:50 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.29 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.23/1.13 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.23/1.13 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------