%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWB025+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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:04:30 PM UTC 2026
% Result : Theorem 10.38s 2.30s
% Output : CNFRefutation 10.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 74 ( 35 unt; 0 def)
% Number of atoms : 337 ( 0 equ)
% Maximal formula atoms : 18 ( 4 avg)
% Number of connectives : 431 ( 168 ~; 167 |; 89 &)
% ( 5 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-3 aty)
% Number of variables : 163 ( 0 sgn 143 !; 20 ?; 55 :)
% Comments :
%------------------------------------------------------------------------------
fof(f389,axiom,
! [X0,X1,X2,X3,X4] :
( ( 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) )
=> ( iext(uri_owl_propertyChainAxiom,X0,X1)
<=> ( ! [X5,X6,X7] :
( ( iext(X4,X6,X7)
& iext(X2,X5,X6) )
=> iext(X0,X5,X7) )
& ip(X4)
& ip(X2)
& ip(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_chain_002) ).
fof(f391,axiom,
! [X0,X1] :
( iext(uri_owl_inverseOf,X0,X1)
<=> ( ! [X2,X3] :
( iext(X0,X2,X3)
<=> iext(X1,X3,X2) )
& ip(X1)
& ip(X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB001+0.ax',owl_inv) ).
fof(f559,conjecture,
( iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
& iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties) ).
fof(f560,negated_conjecture,
~ ( iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
& iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(negated_conjecture,[status(cth)],[f559]) ).
fof(f561,axiom,
? [X0,X1,X2,X3,X4] :
( iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)
& iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly)
& iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob)
& iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave)
& iext(uri_owl_inverseOf,X4,uri_ex_hasFather)
& iext(uri_rdf_rest,X3,uri_rdf_nil)
& iext(uri_rdf_first,X3,X4)
& iext(uri_rdf_rest,X2,X3)
& iext(uri_rdf_first,X2,uri_ex_hasUncle)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,X2)
& iext(uri_rdf_rest,X1,uri_rdf_nil)
& iext(uri_rdf_first,X1,uri_ex_hasFather)
& iext(uri_rdf_rest,X0,X1)
& iext(uri_rdf_first,X0,uri_ex_hasCousin)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties) ).
fof(f842,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( iext(uri_owl_propertyChainAxiom,X0,X1)
<=> ( ! [X5,X6,X7] :
( ~ iext(X4,X6,X7)
| ~ iext(X2,X5,X6)
| iext(X0,X5,X7) )
& ip(X4)
& ip(X2)
& ip(X0) ) ) ),
inference(ennf_transformation,[],[f389]) ).
fof(f843,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( iext(uri_owl_propertyChainAxiom,X0,X1)
<=> ( ! [X5,X6,X7] :
( ~ iext(X4,X6,X7)
| ~ iext(X2,X5,X6)
| iext(X0,X5,X7) )
& ip(X4)
& ip(X2)
& ip(X0) ) ) ),
inference(flattening,[],[f842]) ).
fof(f980,plain,
( ~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
| ~ iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(ennf_transformation,[],[f560]) ).
fof(f1397,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( ( ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ( ! [X5,X6,X7] :
( ~ iext(X4,X6,X7)
| ~ iext(X2,X5,X6)
| iext(X0,X5,X7) )
& ip(X4)
& ip(X2)
& ip(X0) ) )
& ( ? [X5,X6,X7] :
( iext(X4,X6,X7)
& iext(X2,X5,X6)
& ~ iext(X0,X5,X7) )
| ~ ip(X4)
| ~ ip(X2)
| ~ ip(X0)
| iext(uri_owl_propertyChainAxiom,X0,X1) ) ) ),
inference(nnf_transformation,[],[f843]) ).
fof(f1398,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( ( ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ( ! [X5,X6,X7] :
( ~ iext(X4,X6,X7)
| ~ iext(X2,X5,X6)
| iext(X0,X5,X7) )
& ip(X4)
& ip(X2)
& ip(X0) ) )
& ( ? [X5,X6,X7] :
( iext(X4,X6,X7)
& iext(X2,X5,X6)
& ~ iext(X0,X5,X7) )
| ~ ip(X4)
| ~ ip(X2)
| ~ ip(X0)
| iext(uri_owl_propertyChainAxiom,X0,X1) ) ) ),
inference(flattening,[],[f1397]) ).
fof(f1399,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( ( ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ( ! [X8,X9,X10] :
( ~ iext(X4,X9,X10)
| ~ iext(X2,X8,X9)
| iext(X0,X8,X10) )
& ip(X4)
& ip(X2)
& ip(X0) ) )
& ( ? [X5,X6,X7] :
( iext(X4,X6,X7)
& iext(X2,X5,X6)
& ~ iext(X0,X5,X7) )
| ~ ip(X4)
| ~ ip(X2)
| ~ ip(X0)
| iext(uri_owl_propertyChainAxiom,X0,X1) ) ) ),
inference(rectify,[],[f1398]) ).
fof(f1400,plain,
! [X0,X1,X2,X3,X4] :
( ~ 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)
| ( ( ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ( ! [X8,X9,X10] :
( ~ iext(X4,X9,X10)
| ~ iext(X2,X8,X9)
| iext(X0,X8,X10) )
& ip(X4)
& ip(X2)
& ip(X0) ) )
& ( ( iext(X4,sK212(X0,X2,X4),sK213(X0,X2,X4))
& iext(X2,sK211(X0,X2,X4),sK212(X0,X2,X4))
& ~ iext(X0,sK211(X0,X2,X4),sK213(X0,X2,X4)) )
| ~ ip(X4)
| ~ ip(X2)
| ~ ip(X0)
| iext(uri_owl_propertyChainAxiom,X0,X1) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK211,sK212,sK213]),skolemize(X5,sK211(X0,X2,X4)),skolemize(X6,sK212(X0,X2,X4)),skolemize(X7,sK213(X0,X2,X4))],[f1399]) ).
fof(f1407,plain,
! [X0,X1] :
( ( ~ iext(uri_owl_inverseOf,X0,X1)
| ( ! [X2,X3] :
( ( ~ iext(X0,X2,X3)
| iext(X1,X3,X2) )
& ( ~ iext(X1,X3,X2)
| iext(X0,X2,X3) ) )
& ip(X1)
& ip(X0) ) )
& ( ? [X2,X3] :
( ( iext(X0,X2,X3)
| iext(X1,X3,X2) )
& ( ~ iext(X0,X2,X3)
| ~ iext(X1,X3,X2) ) )
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ) ),
inference(nnf_transformation,[],[f391]) ).
fof(f1408,plain,
! [X0,X1] :
( ( ~ iext(uri_owl_inverseOf,X0,X1)
| ( ! [X2,X3] :
( ( ~ iext(X0,X2,X3)
| iext(X1,X3,X2) )
& ( ~ iext(X1,X3,X2)
| iext(X0,X2,X3) ) )
& ip(X1)
& ip(X0) ) )
& ( ? [X2,X3] :
( ( iext(X0,X2,X3)
| iext(X1,X3,X2) )
& ( ~ iext(X0,X2,X3)
| ~ iext(X1,X3,X2) ) )
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ) ),
inference(flattening,[],[f1407]) ).
fof(f1409,plain,
! [X0,X1] :
( ( ~ iext(uri_owl_inverseOf,X0,X1)
| ( ! [X4,X5] :
( ( ~ iext(X0,X4,X5)
| iext(X1,X5,X4) )
& ( ~ iext(X1,X5,X4)
| iext(X0,X4,X5) ) )
& ip(X1)
& ip(X0) ) )
& ( ? [X2,X3] :
( ( iext(X0,X2,X3)
| iext(X1,X3,X2) )
& ( ~ iext(X0,X2,X3)
| ~ iext(X1,X3,X2) ) )
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ) ),
inference(rectify,[],[f1408]) ).
fof(f1410,plain,
! [X0,X1] :
( ( ~ iext(uri_owl_inverseOf,X0,X1)
| ( ! [X4,X5] :
( ( ~ iext(X0,X4,X5)
| iext(X1,X5,X4) )
& ( ~ iext(X1,X5,X4)
| iext(X0,X4,X5) ) )
& ip(X1)
& ip(X0) ) )
& ( ( ( iext(X0,sK218(X0,X1),sK219(X0,X1))
| iext(X1,sK219(X0,X1),sK218(X0,X1)) )
& ( ~ iext(X0,sK218(X0,X1),sK219(X0,X1))
| ~ iext(X1,sK219(X0,X1),sK218(X0,X1)) ) )
| ~ ip(X1)
| ~ ip(X0)
| iext(uri_owl_inverseOf,X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK218,sK219]),skolemize(X2,sK218(X0,X1)),skolemize(X3,sK219(X0,X1))],[f1409]) ).
fof(f1460,plain,
( iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)
& iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly)
& iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob)
& iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave)
& iext(uri_owl_inverseOf,sK255,uri_ex_hasFather)
& iext(uri_rdf_rest,sK254,uri_rdf_nil)
& iext(uri_rdf_first,sK254,sK255)
& iext(uri_rdf_rest,sK253,sK254)
& iext(uri_rdf_first,sK253,uri_ex_hasUncle)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK253)
& iext(uri_rdf_rest,sK252,uri_rdf_nil)
& iext(uri_rdf_first,sK252,uri_ex_hasFather)
& iext(uri_rdf_rest,sK251,sK252)
& iext(uri_rdf_first,sK251,uri_ex_hasCousin)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK251) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK251,sK252,sK253,sK254,sK255]),skolemize(X0,sK251),skolemize(X1,sK252),skolemize(X2,sK253),skolemize(X3,sK254),skolemize(X4,sK255)],[f561]) ).
fof(f2483,plain,
! [X2,X3,X10,X0,X1,X8,X9,X4] :
( ~ 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)
| ~ iext(uri_owl_propertyChainAxiom,X0,X1)
| ~ iext(X4,X9,X10)
| ~ iext(X2,X8,X9)
| iext(X0,X8,X10) ),
inference(cnf_transformation,[],[f1400]) ).
fof(f2503,plain,
! [X0,X1,X4,X5] :
( ~ iext(uri_owl_inverseOf,X0,X1)
| ~ iext(X1,X5,X4)
| iext(X0,X4,X5) ),
inference(cnf_transformation,[],[f1410]) ).
fof(f2750,plain,
( ~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
| ~ iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(cnf_transformation,[],[f980]) ).
fof(f2751,plain,
iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave),
inference(cnf_transformation,[],[f1460]) ).
fof(f2752,plain,
iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly),
inference(cnf_transformation,[],[f1460]) ).
fof(f2753,plain,
iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob),
inference(cnf_transformation,[],[f1460]) ).
fof(f2754,plain,
iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave),
inference(cnf_transformation,[],[f1460]) ).
fof(f2755,plain,
iext(uri_owl_inverseOf,sK255,uri_ex_hasFather),
inference(cnf_transformation,[],[f1460]) ).
fof(f2756,plain,
iext(uri_rdf_rest,sK254,uri_rdf_nil),
inference(cnf_transformation,[],[f1460]) ).
fof(f2757,plain,
iext(uri_rdf_first,sK254,sK255),
inference(cnf_transformation,[],[f1460]) ).
fof(f2758,plain,
iext(uri_rdf_rest,sK253,sK254),
inference(cnf_transformation,[],[f1460]) ).
fof(f2759,plain,
iext(uri_rdf_first,sK253,uri_ex_hasUncle),
inference(cnf_transformation,[],[f1460]) ).
fof(f2760,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK253),
inference(cnf_transformation,[],[f1460]) ).
fof(f2761,plain,
iext(uri_rdf_rest,sK252,uri_rdf_nil),
inference(cnf_transformation,[],[f1460]) ).
fof(f2762,plain,
iext(uri_rdf_first,sK252,uri_ex_hasFather),
inference(cnf_transformation,[],[f1460]) ).
fof(f2763,plain,
iext(uri_rdf_rest,sK251,sK252),
inference(cnf_transformation,[],[f1460]) ).
fof(f2764,plain,
iext(uri_rdf_first,sK251,uri_ex_hasCousin),
inference(cnf_transformation,[],[f1460]) ).
fof(f2765,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK251),
inference(cnf_transformation,[],[f1460]) ).
tcf(c_1065,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( iext(X7,X1,X4)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil)
| ~ iext(uri_owl_propertyChainAxiom,X7,X5)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X3)
| ~ iext(uri_rdf_first,X5,X0)
| ~ iext(X3,X2,X4)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[],[f2483]) ).
tcf(c_1082,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( iext(X3,X2,X1)
| ~ iext(uri_owl_inverseOf,X3,X0)
| ~ iext(X0,X1,X2) ),
inference(cnf_transformation,[],[f2503]) ).
tcf(c_1326,negated_conjecture,
( ~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
| ~ iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(cnf_transformation,[],[f2750]) ).
tcf(c_1327,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK251),
inference(cnf_transformation,[],[f2765]) ).
tcf(c_1328,plain,
iext(uri_rdf_first,sK251,uri_ex_hasCousin),
inference(cnf_transformation,[],[f2764]) ).
tcf(c_1329,plain,
iext(uri_rdf_rest,sK251,sK252),
inference(cnf_transformation,[],[f2763]) ).
tcf(c_1330,plain,
iext(uri_rdf_first,sK252,uri_ex_hasFather),
inference(cnf_transformation,[],[f2762]) ).
tcf(c_1331,plain,
iext(uri_rdf_rest,sK252,uri_rdf_nil),
inference(cnf_transformation,[],[f2761]) ).
tcf(c_1332,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK253),
inference(cnf_transformation,[],[f2760]) ).
tcf(c_1333,plain,
iext(uri_rdf_first,sK253,uri_ex_hasUncle),
inference(cnf_transformation,[],[f2759]) ).
tcf(c_1334,plain,
iext(uri_rdf_rest,sK253,sK254),
inference(cnf_transformation,[],[f2758]) ).
tcf(c_1335,plain,
iext(uri_rdf_first,sK254,sK255),
inference(cnf_transformation,[],[f2757]) ).
tcf(c_1336,plain,
iext(uri_rdf_rest,sK254,uri_rdf_nil),
inference(cnf_transformation,[],[f2756]) ).
tcf(c_1337,plain,
iext(uri_owl_inverseOf,sK255,uri_ex_hasFather),
inference(cnf_transformation,[],[f2755]) ).
tcf(c_1338,plain,
iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave),
inference(cnf_transformation,[],[f2754]) ).
tcf(c_1339,plain,
iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob),
inference(cnf_transformation,[],[f2753]) ).
tcf(c_1340,plain,
iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly),
inference(cnf_transformation,[],[f2752]) ).
tcf(c_1341,plain,
iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave),
inference(cnf_transformation,[],[f2751]) ).
tcf(c_1506,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( iext(X4,uri_ex_alice,X1)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,uri_ex_hasCousin)
| ~ iext(uri_owl_propertyChainAxiom,X4,X3)
| ~ iext(uri_rdf_rest,X3,X2)
| ~ iext(uri_rdf_first,X2,X0)
| ~ iext(X0,uri_ex_bob,X1) ),
inference(superposition,[status(thm)],[c_1339,c_1065]) ).
tcf(c_1905,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( iext(X2,uri_ex_alice,X1)
| ~ iext(uri_rdf_rest,X3,sK252)
| ~ iext(uri_rdf_first,sK252,X0)
| ~ iext(uri_rdf_first,X3,uri_ex_hasCousin)
| ~ iext(uri_owl_propertyChainAxiom,X2,X3)
| ~ iext(X0,uri_ex_bob,X1) ),
inference(superposition,[status(thm)],[c_1331,c_1506]) ).
tcf(c_2419,plain,
! [X0: $i,X1: $i,X2: $i] :
( iext(X0,uri_ex_alice,X2)
| ~ iext(uri_ex_hasFather,uri_ex_bob,X2)
| ~ iext(uri_rdf_rest,X1,sK252)
| ~ iext(uri_rdf_first,X1,uri_ex_hasCousin)
| ~ iext(uri_owl_propertyChainAxiom,X0,X1) ),
inference(superposition,[status(thm)],[c_1330,c_1905]) ).
tcf(c_2771,plain,
! [X0: $i] :
( iext(uri_ex_hasUncle,uri_ex_alice,X0)
| ~ iext(uri_rdf_rest,sK251,sK252)
| ~ iext(uri_rdf_first,sK251,uri_ex_hasCousin)
| ~ iext(uri_ex_hasFather,uri_ex_bob,X0) ),
inference(superposition,[status(thm)],[c_1327,c_2419]) ).
tcf(c_3020,plain,
! [X0: $i] :
( iext(uri_ex_hasUncle,uri_ex_alice,X0)
| ~ iext(uri_ex_hasFather,uri_ex_bob,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2771,c_1328,c_1329,c_2771]) ).
tcf(c_3027,plain,
iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),
inference(superposition,[status(thm)],[c_1340,c_3020]) ).
tcf(c_17752,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( iext(X4,uri_ex_bob,X1)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X4,X3)
| ~ iext(uri_rdf_rest,X3,X2)
| ~ iext(uri_rdf_first,X2,X0)
| ~ iext(X0,uri_ex_dave,X1) ),
inference(superposition,[status(thm)],[c_1341,c_1065]) ).
tcf(c_18130,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( iext(X2,uri_ex_bob,X1)
| ~ iext(uri_rdf_rest,X3,sK254)
| ~ iext(uri_rdf_first,sK254,X0)
| ~ iext(uri_rdf_first,X3,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X2,X3)
| ~ iext(X0,uri_ex_dave,X1) ),
inference(superposition,[status(thm)],[c_1336,c_17752]) ).
tcf(c_18660,plain,
! [X0: $i,X1: $i,X2: $i] :
( iext(X0,uri_ex_bob,X2)
| ~ iext(sK255,uri_ex_dave,X2)
| ~ iext(uri_rdf_rest,X1,sK254)
| ~ iext(uri_rdf_first,X1,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X0,X1) ),
inference(superposition,[status(thm)],[c_1335,c_18130]) ).
tcf(c_19115,plain,
! [X0: $i] :
( iext(uri_ex_hasCousin,uri_ex_bob,X0)
| ~ iext(uri_rdf_rest,sK253,sK254)
| ~ iext(uri_rdf_first,sK253,uri_ex_hasUncle)
| ~ iext(sK255,uri_ex_dave,X0) ),
inference(superposition,[status(thm)],[c_1332,c_18660]) ).
tcf(c_19642,plain,
! [X0: $i] :
( iext(uri_ex_hasCousin,uri_ex_bob,X0)
| ~ iext(sK255,uri_ex_dave,X0) ),
inference(global_subsumption_just,[status(thm)],[c_19115,c_1333,c_1334,c_19115]) ).
tcf(c_23211,negated_conjecture,
~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),
inference(global_subsumption_just,[status(thm)],[c_1326,c_1326,c_3027]) ).
tcf(c_23266,plain,
! [X0: $i] :
( iext(X0,uri_ex_dave,uri_ex_alice)
| ~ iext(uri_owl_inverseOf,X0,uri_ex_hasFather) ),
inference(superposition,[status(thm)],[c_1338,c_1082]) ).
tcf(c_23445,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( iext(X4,uri_ex_bob,X1)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil)
| ~ iext(uri_rdf_first,X3,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X4,X3)
| ~ iext(uri_rdf_rest,X3,X2)
| ~ iext(uri_rdf_first,X2,X0)
| ~ iext(X0,uri_ex_dave,X1) ),
inference(superposition,[status(thm)],[c_1341,c_1065]) ).
tcf(c_23523,plain,
iext(sK255,uri_ex_dave,uri_ex_alice),
inference(superposition,[status(thm)],[c_1337,c_23266]) ).
tcf(c_23906,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( iext(X2,uri_ex_bob,X1)
| ~ iext(uri_rdf_rest,X3,sK254)
| ~ iext(uri_rdf_first,sK254,X0)
| ~ iext(uri_rdf_first,X3,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X2,X3)
| ~ iext(X0,uri_ex_dave,X1) ),
inference(superposition,[status(thm)],[c_1336,c_23445]) ).
tcf(c_24474,plain,
! [X0: $i,X1: $i,X2: $i] :
( iext(X0,uri_ex_bob,X2)
| ~ iext(sK255,uri_ex_dave,X2)
| ~ iext(uri_rdf_rest,X1,sK254)
| ~ iext(uri_rdf_first,X1,uri_ex_hasUncle)
| ~ iext(uri_owl_propertyChainAxiom,X0,X1) ),
inference(superposition,[status(thm)],[c_1335,c_23906]) ).
tcf(c_25139,plain,
! [X0: $i] :
( iext(uri_ex_hasCousin,uri_ex_bob,X0)
| ~ iext(uri_rdf_rest,sK253,sK254)
| ~ iext(uri_rdf_first,sK253,uri_ex_hasUncle)
| ~ iext(sK255,uri_ex_dave,X0) ),
inference(superposition,[status(thm)],[c_1332,c_24474]) ).
tcf(c_25768,plain,
! [X0: $i] :
( iext(uri_ex_hasCousin,uri_ex_bob,X0)
| ~ iext(sK255,uri_ex_dave,X0) ),
inference(global_subsumption_just,[status(thm)],[c_25139,c_19642]) ).
tcf(c_25774,plain,
iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),
inference(superposition,[status(thm)],[c_23523,c_25768]) ).
tcf(c_25775,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_23211,c_25774]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB025+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n018.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 15:35:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.45 % Proving...
% 10.38/2.30 % SZS status Started for theBenchmark.p
% 10.38/2.30 % SZS status Theorem for theBenchmark.p
% 10.38/2.30
% 10.38/2.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 10.38/2.30
% 10.38/2.30 % ------ iProver source info
% 10.38/2.30
% 10.38/2.30 % git: date: 2026-07-19 20:42:38 +0200
% 10.38/2.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 10.38/2.30 % git: non_committed_changes: false
% 10.38/2.30
% 10.38/2.30 % ------ Parsing...
% 10.38/2.30 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 % ------ Problem Properties
% 10.38/2.30
% 10.38/2.30 %
% 10.38/2.30 % clauses 1293
% 10.38/2.30 % conjectures 1
% 10.38/2.30 % EPR 832
% 10.38/2.30 % Horn 1018
% 10.38/2.30 % unary 221
% 10.38/2.30 % binary 548
% 10.38/2.30 % lits 4075
% 10.38/2.30 % lits eq 197
% 10.38/2.30 % fd_pure 0
% 10.38/2.30 % fd_pseudo 0
% 10.38/2.30 % fd_cond 0
% 10.38/2.30 % fd_pseudo_cond 66
% 10.38/2.30 % AC symbols 0
% 10.38/2.30
% 10.38/2.30 % ------ Input Options Time Limit: Unbounded
% 10.38/2.30
% 10.38/2.30
% 10.38/2.30 % ------
% 10.38/2.30 % Current options:
% 10.38/2.30 % ------
% 10.38/2.30
% 10.38/2.30
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % ------ Proving...
% 10.38/2.30 %
% 10.38/2.30
% 10.38/2.30 % SZS status Theorem for theBenchmark.p
% 10.38/2.30
% 10.38/2.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 10.38/2.30
% 10.38/2.30
%------------------------------------------------------------------------------