%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB027+2 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 2.15s 0.77s
% Output : CNFRefutation 2.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 52 ( 19 unt; 0 def)
% Number of atoms : 176 ( 13 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 202 ( 78 ~; 77 |; 38 &)
% ( 6 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-1 aty)
% Number of variables : 100 ( 8 sgn 36 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('theBenchmark.p',rdfs_cext_def) ).
fof(owl_eqdis_sameas,axiom,
! [X,Y] :
( iext(uri_owl_sameAs,X,Y)
<=> X = Y ),
file('theBenchmark.p',owl_eqdis_sameas) ).
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_char_inversefunctional,axiom,
! [P] :
( icext(uri_owl_InverseFunctionalProperty,P)
<=> ( ! [X1,X2,Y] :
( ( iext(P,X2,Y)
& iext(P,X1,Y) )
=> X1 = X2 )
& ip(P) ) ),
file('theBenchmark.p',owl_char_inversefunctional) ).
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_027_Inferred_Property_Characteristics_II,axiom,
? [BNODE_l1,BNODE_l2,BNODE_v] :
( iext(uri_owl_inverseOf,BNODE_v,uri_ex_p)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_v)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1) ),
file('theBenchmark.p',testcase_premise_fullish_027_Inferred_Property_Characteristics_II) ).
fof(testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
file('theBenchmark.p',testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II) ).
fof(testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II_neg,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_9,plain,
( ~ icext(B,A)
| iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
cnf(c_10,plain,
( B = A
| ~ iext(uri_owl_sameAs,A,B) ),
inference(clausify,[status(thm)],[owl_eqdis_sameas]) ).
cnf(c_13,plain,
( ip(B)
| ~ 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(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]) ).
fof(nnf_4,plain,
! [P] :
( ( ? [X1,X2,Y] :
( X2 != X1
& iext(P,X2,Y)
& iext(P,X1,Y) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ( ( ! [X0,X3,X4] :
( X3 = X0
| ~ iext(P,X3,X4)
| ~ iext(P,X0,X4) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(fof_nnf,[status(thm)],[owl_char_inversefunctional]) ).
fof(sk_owl_char_inversefunctional_sk,plain,
! [P] :
( ( ( sK2(P) != sK0(P)
& iext(P,sK2(P),sK1(P))
& iext(P,sK0(P),sK1(P)) )
| ~ ip(P)
| icext(uri_owl_InverseFunctionalProperty,P) )
& ( ( ! [X0,X3,X4] :
( X3 = X0
| ~ iext(P,X3,X4)
| ~ iext(P,X0,X4) )
& ip(P) )
| ~ icext(uri_owl_InverseFunctionalProperty,P) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X1,sK0(P)),skolemize(X2,sK2(P)),skolemize(Y,sK1(P))],[nnf_4]) ).
fof(sk_owl_char_inversefunctional,plain,
( ! [VAR_0] :
( sK2(VAR_0) != sK0(VAR_0)
| ~ ip(VAR_0)
| icext(uri_owl_InverseFunctionalProperty,VAR_0) )
& ! [VAR_0] :
( iext(VAR_0,sK2(VAR_0),sK1(VAR_0))
| ~ ip(VAR_0)
| icext(uri_owl_InverseFunctionalProperty,VAR_0) )
& ! [VAR_0] :
( iext(VAR_0,sK0(VAR_0),sK1(VAR_0))
| ~ ip(VAR_0)
| icext(uri_owl_InverseFunctionalProperty,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_3 = VAR_1
| ~ iext(VAR_0,VAR_3,VAR_2)
| ~ iext(VAR_0,VAR_1,VAR_2)
| ~ icext(uri_owl_InverseFunctionalProperty,VAR_0) )
& ! [VAR_0] :
( ip(VAR_0)
| ~ icext(uri_owl_InverseFunctionalProperty,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_owl_char_inversefunctional_sk]) ).
cnf(c_21,plain,
( iext(A,sK0(A),sK1(A))
| ~ ip(A)
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(split_conjunct,[status(thm)],[sk_owl_char_inversefunctional]) ).
cnf(c_22,plain,
( iext(A,sK2(A),sK1(A))
| ~ ip(A)
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(split_conjunct,[status(thm)],[sk_owl_char_inversefunctional]) ).
cnf(c_23,plain,
( sK2(A) != sK0(A)
| ~ ip(A)
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(split_conjunct,[status(thm)],[sk_owl_char_inversefunctional]) ).
cnf(c_27,plain,
( ~ iext(B,D,C)
| iext(A,C,D)
| ~ iext(uri_owl_inverseOf,A,B) ),
inference(clausify,[status(thm)],[owl_inv]) ).
fof(nnf_6,plain,
? [BNODE_l1,BNODE_l2,BNODE_v] :
( iext(uri_owl_inverseOf,BNODE_v,uri_ex_p)
& iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,BNODE_v)
& iext(uri_rdf_rest,BNODE_l1,BNODE_l2)
& iext(uri_rdf_first,BNODE_l1,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,BNODE_l1) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
fof(sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II,plain,
( iext(uri_owl_inverseOf,sK5,uri_ex_p)
& iext(uri_rdf_rest,sK4,uri_rdf_nil)
& iext(uri_rdf_first,sK4,sK5)
& iext(uri_rdf_rest,sK3,sK4)
& iext(uri_rdf_first,sK3,uri_ex_p)
& iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(BNODE_l1,sK3),skolemize(BNODE_l2,sK4),skolemize(BNODE_v,sK5)],[nnf_6]) ).
cnf(c_30,plain,
iext(uri_owl_propertyChainAxiom,uri_owl_sameAs,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_31,plain,
iext(uri_rdf_first,sK3,uri_ex_p),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_32,plain,
iext(uri_rdf_rest,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_33,plain,
iext(uri_rdf_first,sK4,sK5),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_34,plain,
iext(uri_rdf_rest,sK4,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_35,plain,
iext(uri_owl_inverseOf,sK5,uri_ex_p),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_027_Inferred_Property_Characteristics_II]) ).
cnf(c_36,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_027_Inferred_Property_Characteristics_II_neg]) ).
cnf(c_161,plain,
( iext(uri_owl_sameAs,D,F)
| ~ iext(C,E,F)
| ~ iext(A,D,E)
| ~ iext(uri_rdf_rest,B,uri_rdf_nil)
| ~ iext(uri_rdf_first,B,C)
| ~ iext(uri_rdf_rest,sK3,B)
| ~ iext(uri_rdf_first,sK3,A) ),
inference(resolve,[status(thm)],[c_30,c_15]) ).
cnf(c_748,plain,
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,C,sK3)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK3,A) ),
inference(resolve,[status(thm)],[c_13,c_31]) ).
cnf(c_749,plain,
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,B,sK3)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_748,c_32]) ).
cnf(c_750,plain,
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,A,sK3)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_749,c_33]) ).
cnf(c_751,plain,
( ip(uri_ex_p)
| ~ iext(uri_owl_propertyChainAxiom,A,sK3) ),
inference(resolve,[status(thm)],[c_750,c_34]) ).
cnf(c_384,plain,
ip(uri_ex_p),
inference(resolve,[status(thm)],[c_751,c_30]) ).
cnf(c_512,plain,
( ~ iext(uri_ex_p,B,A)
| iext(sK5,A,B) ),
inference(resolve,[status(thm)],[c_35,c_27]) ).
cnf(c_532,negated_conjecture,
~ icext(uri_owl_InverseFunctionalProperty,uri_ex_p),
inference(resolve,[status(thm)],[c_9,c_36]) ).
cnf(c_752,plain,
( sK2(uri_ex_p) != sK0(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolve,[status(thm)],[c_384,c_23]) ).
cnf(c_616,plain,
sK2(uri_ex_p) != sK0(uri_ex_p),
inference(resolve,[status(thm)],[c_532,c_752]) ).
cnf(c_753,plain,
( iext(uri_ex_p,sK2(uri_ex_p),sK1(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolve,[status(thm)],[c_384,c_22]) ).
cnf(c_617,plain,
iext(uri_ex_p,sK2(uri_ex_p),sK1(uri_ex_p)),
inference(resolve,[status(thm)],[c_532,c_753]) ).
cnf(c_754,plain,
( iext(uri_ex_p,sK0(uri_ex_p),sK1(uri_ex_p))
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolve,[status(thm)],[c_384,c_21]) ).
cnf(c_618,plain,
iext(uri_ex_p,sK0(uri_ex_p),sK1(uri_ex_p)),
inference(resolve,[status(thm)],[c_532,c_754]) ).
cnf(c_755,plain,
sK0(uri_ex_p) != sK2(uri_ex_p),
inference(copy,[status(thm)],[c_616]) ).
cnf(c_635,plain,
~ iext(uri_owl_sameAs,sK2(uri_ex_p),sK0(uri_ex_p)),
inference(resolve,[status(thm)],[c_10,c_755]) ).
cnf(c_756,plain,
( iext(uri_owl_sameAs,C,E)
| ~ iext(B,D,E)
| ~ iext(uri_ex_p,C,D)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B)
| ~ iext(uri_rdf_rest,sK3,A) ),
inference(resolve,[status(thm)],[c_161,c_31]) ).
cnf(c_757,plain,
( iext(uri_owl_sameAs,B,D)
| ~ iext(A,C,D)
| ~ iext(uri_ex_p,B,C)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_756,c_32]) ).
cnf(c_758,plain,
( iext(uri_owl_sameAs,A,C)
| ~ iext(sK5,B,C)
| ~ iext(uri_ex_p,A,B)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil) ),
inference(resolve,[status(thm)],[c_757,c_33]) ).
cnf(c_759,plain,
( iext(uri_owl_sameAs,A,C)
| ~ iext(sK5,B,C)
| ~ iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_758,c_34]) ).
cnf(c_760,plain,
( iext(uri_owl_sameAs,sK2(uri_ex_p),A)
| ~ iext(sK5,sK1(uri_ex_p),A) ),
inference(resolve,[status(thm)],[c_759,c_617]) ).
cnf(c_742,plain,
~ iext(sK5,sK1(uri_ex_p),sK0(uri_ex_p)),
inference(resolve,[status(thm)],[c_760,c_635]) ).
cnf(c_761,plain,
iext(sK5,sK1(uri_ex_p),sK0(uri_ex_p)),
inference(resolve,[status(thm)],[c_618,c_512]) ).
cnf(c_747,plain,
$false,
inference(resolve,[status(thm)],[c_742,c_761]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWB027+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n015.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sat Sep 26 11:54:29 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.45 % Process 3962849 was started by sandbox2 on n015,
% 0.16/0.45 % Sat Sep 26 11:54:29 2026
% 0.16/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.46
% 0.16/0.46 % From the command line: assign(max_seconds, 300).
% 2.15/0.77
% 2.15/0.77 % SZS status Theorem for theBenchmark
% 2.15/0.77
% 2.15/0.77 % Proof 1 at 0.25 (+ 0.03) seconds.
% 2.15/0.77 % Length of proof is 32.
% 2.15/0.77 % Level of proof is 6.
% 2.15/0.77 % Maximum clause weight is 37.000.
% 2.15/0.77 % Given clauses 182.
% 2.15/0.77
% 2.15/0.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------