%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWB029+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:37:12 PM UTC 2026
% Result : Theorem 36.69s 5.21s
% Output : CNFRefutation 24.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 42 ( 12 unt; 0 def)
% Number of atoms : 228 ( 0 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 294 ( 108 ~; 106 |; 71 &)
% ( 7 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 14 con; 0-4 aty)
% Number of variables : 109 ( 99 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Z,C] :
( iext(uri_owl_complementOf,Z,C)
=> ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,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_intersectionOf,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') ).
fof(f80,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,axiom,
? [BNODE_x,BNODE_y,BNODE_l1,BNODE_l2] :
( iext(uri_owl_complementOf,BNODE_y,uri_ex_A)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_y)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_A)
& iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)
& iext(uri_rdf_type,uri_ex_w,BNODE_x)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,plain,
! [Z,C] :
( ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f143,plain,
! [Z,C] :
( ( ! [X] :
( ( icext(C,X)
| icext(Z,X) )
& ( ~ icext(C,X)
| ~ icext(Z,X) ) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(NNF_transformation,[status(thm)],[f142]) ).
fof(f144,plain,
! [Z,C] :
( ( ! [X] :
( icext(C,X)
| icext(Z,X) )
& ! [X] :
( ~ icext(C,X)
| ~ icext(Z,X) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(miniscoping,[status(thm)],[f143]) ).
fof(f147,plain,
! [X0,X1,X2] :
( ~ icext(X1,X2)
| ~ icext(X0,X2)
| ~ iext(uri_owl_complementOf,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f167,plain,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
& icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) )
| ~ 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(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f168,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_intersectionOf,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_intersectionOf,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)],[f167]) ).
fof(f169,plain,
! [S1,C1,C2] :
( ( ! [Z] :
( ? [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_intersectionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ icext(C2,X)
| ~ icext(C1,X)
| icext(Z,X) )
& ! [X] :
( ( icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ! [S2] :
( ~ 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(miniscoping,[status(thm)],[f168]) ).
fof(f170,plain,
! [S1,C1,C2] :
( ( ! [Z] :
( ( ( ( icext(C2,sK2_skl(Z,C2,C1,S1))
& icext(C1,sK2_skl(Z,C2,C1,S1)) )
| icext(Z,sK2_skl(Z,C2,C1,S1)) )
& ( ~ icext(C2,sK2_skl(Z,C2,C1,S1))
| ~ icext(C1,sK2_skl(Z,C2,C1,S1))
| ~ icext(Z,sK2_skl(Z,C2,C1,S1)) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z)
| iext(uri_owl_intersectionOf,Z,S1) )
& ! [Z] :
( ( ! [X] :
( ~ icext(C2,X)
| ~ icext(C1,X)
| icext(Z,X) )
& ! [X] :
( ( icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ! [S2] :
( ~ 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(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(X,sK2_skl(Z,C2,C1,S1))],[f169]) ).
fof(f174,plain,
! [X0,X1,X2,X3,X4,X5] :
( icext(X1,X5)
| ~ icext(X4,X5)
| ~ iext(uri_owl_intersectionOf,X4,X0)
| ~ 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) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f175,plain,
! [X0,X1,X2,X3,X4,X5] :
( icext(X3,X5)
| ~ icext(X4,X5)
| ~ iext(uri_owl_intersectionOf,X4,X0)
| ~ 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) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f421,plain,
! [X,C] :
( ( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(NNF_transformation,[status(thm)],[f80]) ).
fof(f422,plain,
( ! [X,C] :
( ~ icext(C,X)
| iext(uri_rdf_type,X,C) )
& ! [X,C] :
( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(miniscoping,[status(thm)],[f421]) ).
fof(f423,plain,
! [X0,X1] :
( icext(X1,X0)
| ~ iext(uri_rdf_type,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f515,plain,
? [BNODE_y] :
( iext(uri_owl_complementOf,BNODE_y,uri_ex_A)
& ? [BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_y)
& ? [BNODE_l1] :
( iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_A)
& ? [BNODE_x] :
( iext(uri_owl_intersectionOf,BNODE_x,BNODE_l1)
& iext(uri_rdf_type,uri_ex_w,BNODE_x)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ) ) ) ),
inference(miniscoping,[status(thm)],[f141]) ).
fof(f516,plain,
( iext(uri_owl_complementOf,sK18_skl,uri_ex_A)
& iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)
& iext(uri_rdf_first,sK19_skl,sK18_skl)
& iext(uri_rdf_rest,sK20_skl,sK19_skl)
& iext(uri_rdf_first,sK20_skl,uri_ex_A)
& iext(uri_owl_intersectionOf,sK21_skl,sK20_skl)
& iext(uri_rdf_type,uri_ex_w,sK21_skl)
& iext(uri_rdf_type,uri_ex_B,uri_owl_Class)
& iext(uri_rdf_type,uri_ex_A,uri_owl_Class) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(BNODE_y,sK18_skl),skolemize(BNODE_l2,sK19_skl),skolemize(BNODE_l1,sK20_skl),skolemize(BNODE_x,sK21_skl)],[f515]) ).
fof(f519,plain,
iext(uri_rdf_type,uri_ex_w,sK21_skl),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f520,plain,
iext(uri_owl_intersectionOf,sK21_skl,sK20_skl),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f521,plain,
iext(uri_rdf_first,sK20_skl,uri_ex_A),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f522,plain,
iext(uri_rdf_rest,sK20_skl,sK19_skl),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f523,plain,
iext(uri_rdf_first,sK19_skl,sK18_skl),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f524,plain,
iext(uri_rdf_rest,sK19_skl,uri_rdf_nil),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f525,plain,
iext(uri_owl_complementOf,sK18_skl,uri_ex_A),
inference(cnf_transformation,[status(thm)],[f516]) ).
fof(f538,plain,
icext(sK21_skl,uri_ex_w),
inference(resolution,[status(thm)],[f423,f519]) ).
fof(f690,plain,
! [X0,X1,X2,X3] :
( icext(X1,X3)
| ~ icext(X2,X3)
| ~ iext(uri_owl_intersectionOf,X2,sK20_skl)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sK20_skl,X0) ),
inference(resolution,[status(thm)],[f521,f175]) ).
fof(f691,plain,
! [X0,X1,X2,X3] :
( icext(uri_ex_A,X3)
| ~ icext(X2,X3)
| ~ iext(uri_owl_intersectionOf,X2,sK20_skl)
| ~ iext(uri_rdf_rest,X0,uri_rdf_nil)
| ~ iext(uri_rdf_first,X0,X1)
| ~ iext(uri_rdf_rest,sK20_skl,X0) ),
inference(resolution,[status(thm)],[f521,f174]) ).
fof(f740,plain,
! [X0] :
( ~ icext(uri_ex_A,X0)
| ~ icext(sK18_skl,X0) ),
inference(resolution,[status(thm)],[f525,f147]) ).
fof(f3536,plain,
! [X0,X1,X2] :
( icext(X0,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,sK20_skl)
| ~ iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK19_skl,X0) ),
inference(resolution,[status(thm)],[f690,f522]) ).
fof(f3537,plain,
! [X0,X1,X2] :
( icext(X0,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,sK20_skl)
| ~ iext(uri_rdf_first,sK19_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3536,f524]) ).
fof(f3565,plain,
! [X0,X1,X2] :
( icext(uri_ex_A,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,sK20_skl)
| ~ iext(uri_rdf_rest,sK19_skl,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK19_skl,X0) ),
inference(resolution,[status(thm)],[f691,f522]) ).
fof(f3566,plain,
! [X0,X1,X2] :
( icext(uri_ex_A,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,sK20_skl)
| ~ iext(uri_rdf_first,sK19_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3565,f524]) ).
fof(f15047,plain,
! [X0,X1] :
( icext(sK18_skl,X1)
| ~ icext(X0,X1)
| ~ iext(uri_owl_intersectionOf,X0,sK20_skl) ),
inference(resolution,[status(thm)],[f3537,f523]) ).
fof(f15048,plain,
! [X0,X1] :
( icext(uri_ex_A,X1)
| ~ icext(X0,X1)
| ~ iext(uri_owl_intersectionOf,X0,sK20_skl) ),
inference(resolution,[status(thm)],[f3566,f523]) ).
fof(f17455,plain,
! [X0] :
( icext(sK18_skl,X0)
| ~ icext(sK21_skl,X0) ),
inference(resolution,[status(thm)],[f15047,f520]) ).
fof(f17547,plain,
icext(sK18_skl,uri_ex_w),
inference(resolution,[status(thm)],[f17455,f538]) ).
fof(f18405,plain,
! [X0] :
( icext(uri_ex_A,X0)
| ~ icext(sK21_skl,X0) ),
inference(resolution,[status(thm)],[f15048,f520]) ).
fof(f18408,plain,
icext(uri_ex_A,uri_ex_w),
inference(resolution,[status(thm)],[f18405,f538]) ).
fof(f18409,plain,
~ icext(sK18_skl,uri_ex_w),
inference(resolution,[status(thm)],[f18408,f740]) ).
fof(f18432,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f18409,f17547]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWB029+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n019.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 07:42:34 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 36.69/5.21 % Refutation found
% 36.69/5.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 36.69/5.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.69/5.43 % Elapsed time: 4.969543 seconds
% 2.69/5.43 % CPU time: 37.757651 seconds
% 2.69/5.43 % Total memory used: 167.495 MB
% 2.69/5.43 % Net memory used: 151.003 MB
%------------------------------------------------------------------------------