%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB025+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 08:51:35 AM UTC 2026
% Result : Theorem 0.14s 5.51s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 4
% Syntax : Number of formulae : 43 ( 20 unt; 0 def)
% Number of atoms : 154 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 168 ( 57 ~; 53 |; 53 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 17 con; 0-0 aty)
% Number of variables : 82 ( 0 sgn 12 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(owl_chain_002,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('theBenchmark.p',owl_chain_002) ).
fof(owl_inv,axiom,
! [P1,P2] :
( iext(uri_owl_inverseOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
<=> iext(P2,Y,X) )
& ip(P2)
& ip(P1) ) ),
file('theBenchmark.p',owl_inv) ).
fof(testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties,axiom,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l3] :
( 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,BNODE_l3,uri_ex_hasFather)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,BNODE_l3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11) ),
file('theBenchmark.p',testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties) ).
fof(testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties,conjecture,
( iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
& iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
file('theBenchmark.p',testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties) ).
fof(testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties_neg,negated_conjecture,
~ ( iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
& iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_8,plain,
( iext(E,F,V7)
| ~ iext(D,V6,V7)
| ~ iext(B,F,V6)
| ~ iext(uri_owl_propertyChainAxiom,E,A)
| ~ iext(uri_rdf_rest,C,uri_rdf_nil)
| ~ iext(uri_rdf_first,C,D)
| ~ iext(uri_rdf_rest,A,C)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_chain_002]) ).
cnf(c_15,plain,
( ~ iext(B,D,C)
| iext(A,C,D)
| ~ iext(uri_owl_inverseOf,A,B) ),
inference(clausify,[status(thm)],[owl_inv]) ).
fof(nnf_3,plain,
? [BNODE_l11,BNODE_l12,BNODE_l21,BNODE_l22,BNODE_l3] :
( 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,BNODE_l3,uri_ex_hasFather)
& iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l22,BNODE_l3)
& iext(uri_rdf_rest,BNODE_l21,BNODE_l22)
& iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21)
& iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather)
& iext(uri_rdf_rest,BNODE_l11,BNODE_l12)
& iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
fof(sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties,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,sK4,uri_ex_hasFather)
& iext(uri_rdf_rest,sK3,uri_rdf_nil)
& iext(uri_rdf_first,sK3,sK4)
& iext(uri_rdf_rest,sK2,sK3)
& iext(uri_rdf_first,sK2,uri_ex_hasUncle)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK2)
& iext(uri_rdf_rest,sK1,uri_rdf_nil)
& iext(uri_rdf_first,sK1,uri_ex_hasFather)
& iext(uri_rdf_rest,sK0,sK1)
& iext(uri_rdf_first,sK0,uri_ex_hasCousin)
& iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(BNODE_l11,sK0),skolemize(BNODE_l12,sK1),skolemize(BNODE_l21,sK2),skolemize(BNODE_l22,sK3),skolemize(BNODE_l3,sK4)],[nnf_3]) ).
cnf(c_18,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK0),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_19,plain,
iext(uri_rdf_first,sK0,uri_ex_hasCousin),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_20,plain,
iext(uri_rdf_rest,sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_21,plain,
iext(uri_rdf_first,sK1,uri_ex_hasFather),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_22,plain,
iext(uri_rdf_rest,sK1,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_23,plain,
iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK2),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_24,plain,
iext(uri_rdf_first,sK2,uri_ex_hasUncle),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_25,plain,
iext(uri_rdf_rest,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_26,plain,
iext(uri_rdf_first,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_27,plain,
iext(uri_rdf_rest,sK3,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_28,plain,
iext(uri_owl_inverseOf,sK4,uri_ex_hasFather),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_29,plain,
iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_30,plain,
iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_31,plain,
iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_32,plain,
iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties]) ).
cnf(c_33,negated_conjecture,
( ~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)
| ~ iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly) ),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties_neg]) ).
cnf(c_1036,plain,
( ~ iext(uri_ex_hasFather,B,A)
| iext(sK4,A,B) ),
inference(resolve,[status(thm)],[c_15,c_28]) ).
cnf(c_848,plain,
iext(sK4,uri_ex_dave,uri_ex_alice),
inference(resolve,[status(thm)],[c_1036,c_29]) ).
cnf(c_1037,plain,
( iext(C,D,F)
| ~ iext(B,E,F)
| ~ iext(uri_ex_hasCousin,D,E)
| ~ iext(uri_owl_propertyChainAxiom,C,sK0)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK0,A) ),
inference(resolve,[status(thm)],[c_8,c_19]) ).
cnf(c_1038,plain,
( iext(B,C,E)
| ~ iext(A,D,E)
| ~ iext(uri_ex_hasCousin,C,D)
| ~ iext(uri_owl_propertyChainAxiom,B,sK0)
| ~ iext(uri_rdf_rest,sK1,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK1,A) ),
inference(resolve,[status(thm)],[c_1037,c_20]) ).
cnf(c_1039,plain,
( iext(A,B,D)
| ~ iext(uri_ex_hasFather,C,D)
| ~ iext(uri_ex_hasCousin,B,C)
| ~ iext(uri_owl_propertyChainAxiom,A,sK0)
| ~ iext(uri_rdf_rest,sK1,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_1038,c_21]) ).
cnf(c_1040,plain,
( iext(A,B,D)
| ~ iext(uri_ex_hasFather,C,D)
| ~ iext(uri_ex_hasCousin,B,C)
| ~ iext(uri_owl_propertyChainAxiom,A,sK0) ),
inference(resolve,[status(thm)],[c_1039,c_22]) ).
cnf(c_1041,plain,
( iext(uri_ex_hasUncle,A,C)
| ~ iext(uri_ex_hasFather,B,C)
| ~ iext(uri_ex_hasCousin,A,B) ),
inference(resolve,[status(thm)],[c_1040,c_18]) ).
cnf(c_1042,plain,
( iext(uri_ex_hasUncle,uri_ex_alice,A)
| ~ iext(uri_ex_hasFather,uri_ex_bob,A) ),
inference(resolve,[status(thm)],[c_1041,c_30]) ).
cnf(c_886,plain,
iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),
inference(resolve,[status(thm)],[c_1042,c_31]) ).
cnf(c_898,negated_conjecture,
~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),
inference(resolve,[status(thm)],[c_886,c_33]) ).
cnf(c_1043,plain,
( iext(C,D,F)
| ~ iext(B,E,F)
| ~ iext(uri_ex_hasUncle,D,E)
| ~ iext(uri_owl_propertyChainAxiom,C,sK2)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK2,A) ),
inference(resolve,[status(thm)],[c_8,c_24]) ).
cnf(c_1044,plain,
( iext(B,C,E)
| ~ iext(A,D,E)
| ~ iext(uri_ex_hasUncle,C,D)
| ~ iext(uri_owl_propertyChainAxiom,B,sK2)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_1043,c_25]) ).
cnf(c_1045,plain,
( iext(A,B,D)
| ~ iext(sK4,C,D)
| ~ iext(uri_ex_hasUncle,B,C)
| ~ iext(uri_owl_propertyChainAxiom,A,sK2)
| ~ iext(uri_rdf_rest,sK3,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_1044,c_26]) ).
cnf(c_1046,plain,
( iext(A,B,D)
| ~ iext(sK4,C,D)
| ~ iext(uri_ex_hasUncle,B,C)
| ~ iext(uri_owl_propertyChainAxiom,A,sK2) ),
inference(resolve,[status(thm)],[c_1045,c_27]) ).
cnf(c_1047,plain,
( iext(uri_ex_hasCousin,A,C)
| ~ iext(sK4,B,C)
| ~ iext(uri_ex_hasUncle,A,B) ),
inference(resolve,[status(thm)],[c_1046,c_23]) ).
cnf(c_1048,plain,
( iext(uri_ex_hasCousin,uri_ex_bob,A)
| ~ iext(sK4,uri_ex_dave,A) ),
inference(resolve,[status(thm)],[c_1047,c_32]) ).
cnf(c_1049,negated_conjecture,
~ iext(sK4,uri_ex_dave,uri_ex_alice),
inference(resolve,[status(thm)],[c_1048,c_898]) ).
cnf(c_1035,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_848,c_1049]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB025+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n017.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sat Sep 26 11:45:39 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.37 % Process 624178 was started by sandbox on n017,
% 0.09/5.37 % Sat Sep 26 11:45:39 2026
% 0.09/5.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/5.38
% 0.09/5.38 % From the command line: assign(max_seconds, 300).
% 0.14/5.51
% 0.14/5.51 % SZS status Theorem for theBenchmark
% 0.14/5.51
% 0.14/5.51 % Proof 1 at 0.10 (+ 0.02) seconds.
% 0.14/5.51 % Length of proof is 26.
% 0.14/5.51 % Level of proof is 4.
% 0.14/5.51 % Maximum clause weight is 37.000.
% 0.14/5.51 % Given clauses 146.
% 0.14/5.51
% 0.14/5.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------