%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWB026+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 : n011.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.11s 0.45s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 53 ( 24 unt; 0 def)
% Number of atoms : 150 ( 21 equ)
% Maximal formula atoms : 15 ( 2 avg)
% Number of connectives : 149 ( 52 ~; 51 |; 38 &)
% ( 5 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-1 aty)
% Number of variables : 69 ( 4 sgn 31 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(rdf_type_ip,axiom,
! [P] :
( iext(uri_rdf_type,P,uri_rdf_Property)
<=> ip(P) ),
file('theBenchmark.p',rdf_type_ip) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('theBenchmark.p',rdfs_cext_def) ).
fof(rdfs_domain_main,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('theBenchmark.p',rdfs_domain_main) ).
fof(owl_enum_class_001,axiom,
! [Z,S1,A1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,A1) )
=> ( iext(uri_owl_oneOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> X = A1 )
& ic(Z) ) ) ),
file('theBenchmark.p',owl_enum_class_001) ).
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(testcase_premise_fullish_026_Inferred_Property_Characteristics_I,axiom,
? [BNODE_x1,BNODE_x2,BNODE_l1,BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,uri_ex_u)
& iext(uri_owl_oneOf,BNODE_x2,BNODE_l2)
& iext(uri_rdfs_range,uri_ex_p,BNODE_x2)
& iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l1,uri_ex_w)
& iext(uri_owl_oneOf,BNODE_x1,BNODE_l1)
& iext(uri_rdfs_domain,uri_ex_p,BNODE_x1) ),
file('theBenchmark.p',testcase_premise_fullish_026_Inferred_Property_Characteristics_I) ).
fof(testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I,conjecture,
iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
file('theBenchmark.p',testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I) ).
fof(testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I_neg,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I]) ).
cnf(c_9,plain,
( ip(A)
| ~ iext(uri_rdf_type,A,uri_rdf_Property) ),
inference(clausify,[status(thm)],[rdf_type_ip]) ).
fof(nnf_5,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_5]) ).
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_11,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_12,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_13,plain,
( sK2(A) != sK0(A)
| ~ ip(A)
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(split_conjunct,[status(thm)],[sk_owl_char_inversefunctional]) ).
cnf(c_22,plain,
( ~ icext(B,A)
| iext(uri_rdf_type,A,B) ),
inference(clausify,[status(thm)],[rdfs_cext_def]) ).
cnf(c_23,plain,
( icext(B,C)
| ~ iext(A,C,D)
| ~ iext(uri_rdfs_domain,A,B) ),
inference(clausify,[status(thm)],[rdfs_domain_main]) ).
fof(rdfs_domain_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('theBenchmark.p',rdfs_domain_domain) ).
cnf(c_24,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(clausify,[status(thm)],[rdfs_domain_domain]) ).
cnf(c_25,plain,
( B = D
| ~ icext(C,D)
| ~ iext(uri_owl_oneOf,C,A)
| ~ iext(uri_rdf_rest,A,uri_rdf_nil)
| ~ iext(uri_rdf_first,A,B) ),
inference(clausify,[status(thm)],[owl_enum_class_001]) ).
fof(nnf_6,plain,
? [BNODE_x1,BNODE_x2,BNODE_l1,BNODE_l2] :
( iext(uri_rdf_rest,BNODE_l2,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l2,uri_ex_u)
& iext(uri_owl_oneOf,BNODE_x2,BNODE_l2)
& iext(uri_rdfs_range,uri_ex_p,BNODE_x2)
& iext(uri_rdf_rest,BNODE_l1,uri_rdf_nil)
& iext(uri_rdf_first,BNODE_l1,uri_ex_w)
& iext(uri_owl_oneOf,BNODE_x1,BNODE_l1)
& iext(uri_rdfs_domain,uri_ex_p,BNODE_x1) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_026_Inferred_Property_Characteristics_I]) ).
fof(sk_testcase_premise_fullish_026_Inferred_Property_Characteristics_I,plain,
( iext(uri_rdf_rest,sK7,uri_rdf_nil)
& iext(uri_rdf_first,sK7,uri_ex_u)
& iext(uri_owl_oneOf,sK6,sK7)
& iext(uri_rdfs_range,uri_ex_p,sK6)
& iext(uri_rdf_rest,sK4,uri_rdf_nil)
& iext(uri_rdf_first,sK4,uri_ex_w)
& iext(uri_owl_oneOf,sK3,sK4)
& iext(uri_rdfs_domain,uri_ex_p,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK6,sK7]),skolemize(BNODE_x1,sK3),skolemize(BNODE_x2,sK6),skolemize(BNODE_l1,sK4),skolemize(BNODE_l2,sK7)],[nnf_6]) ).
cnf(c_28,plain,
iext(uri_rdfs_domain,uri_ex_p,sK3),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_026_Inferred_Property_Characteristics_I]) ).
cnf(c_29,plain,
iext(uri_owl_oneOf,sK3,sK4),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_026_Inferred_Property_Characteristics_I]) ).
cnf(c_30,plain,
iext(uri_rdf_first,sK4,uri_ex_w),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_026_Inferred_Property_Characteristics_I]) ).
cnf(c_31,plain,
iext(uri_rdf_rest,sK4,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[sk_testcase_premise_fullish_026_Inferred_Property_Characteristics_I]) ).
cnf(c_36,negated_conjecture,
~ iext(uri_rdf_type,uri_ex_p,uri_owl_InverseFunctionalProperty),
inference(clausify,[status(thm)],[testcase_conclusion_fullish_026_Inferred_Property_Characteristics_I_neg]) ).
cnf(c_38,plain,
( ~ iext(uri_rdf_type,A,uri_rdf_Property)
| iext(A,sK0(A),sK1(A))
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(resolve,[status(thm)],[c_11,c_9]) ).
cnf(c_39,plain,
( ~ iext(uri_rdf_type,A,uri_rdf_Property)
| iext(A,sK2(A),sK1(A))
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(resolve,[status(thm)],[c_12,c_9]) ).
cnf(c_40,plain,
( ~ iext(uri_rdf_type,A,uri_rdf_Property)
| sK2(A) != sK0(A)
| icext(uri_owl_InverseFunctionalProperty,A) ),
inference(resolve,[status(thm)],[c_13,c_9]) ).
cnf(c_42,plain,
( icext(uri_rdf_Property,A)
| ~ iext(uri_rdfs_domain,A,B) ),
inference(resolve,[status(thm)],[c_24,c_23]) ).
cnf(c_46,plain,
( icext(sK3,A)
| ~ iext(uri_ex_p,A,B) ),
inference(resolve,[status(thm)],[c_28,c_23]) ).
cnf(c_154,plain,
( A = B
| ~ icext(sK3,B)
| ~ iext(uri_rdf_rest,sK4,uri_rdf_nil)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_29,c_25]) ).
cnf(c_49,plain,
( A = B
| ~ icext(sK3,B)
| ~ iext(uri_rdf_first,sK4,A) ),
inference(resolve,[status(thm)],[c_31,c_154]) ).
cnf(c_89,negated_conjecture,
~ icext(uri_owl_InverseFunctionalProperty,uri_ex_p),
inference(resolve,[status(thm)],[c_22,c_36]) ).
cnf(c_91,plain,
icext(uri_rdf_Property,uri_ex_p),
inference(resolve,[status(thm)],[c_42,c_28]) ).
cnf(c_95,plain,
iext(uri_rdf_type,uri_ex_p,uri_rdf_Property),
inference(resolve,[status(thm)],[c_91,c_22]) ).
cnf(c_155,plain,
( sK2(uri_ex_p) != sK0(uri_ex_p)
| icext(uri_owl_InverseFunctionalProperty,uri_ex_p) ),
inference(resolve,[status(thm)],[c_95,c_40]) ).
cnf(c_101,plain,
sK2(uri_ex_p) != sK0(uri_ex_p),
inference(resolve,[status(thm)],[c_89,c_155]) ).
cnf(c_156,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_95,c_39]) ).
cnf(c_102,plain,
iext(uri_ex_p,sK2(uri_ex_p),sK1(uri_ex_p)),
inference(resolve,[status(thm)],[c_89,c_156]) ).
cnf(c_157,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_95,c_38]) ).
cnf(c_103,plain,
iext(uri_ex_p,sK0(uri_ex_p),sK1(uri_ex_p)),
inference(resolve,[status(thm)],[c_89,c_157]) ).
cnf(c_112,plain,
( uri_ex_w = A
| ~ icext(sK3,A) ),
inference(resolve,[status(thm)],[c_49,c_30]) ).
cnf(c_140,plain,
icext(sK3,sK2(uri_ex_p)),
inference(resolve,[status(thm)],[c_102,c_46]) ).
cnf(c_158,plain,
uri_ex_w = sK2(uri_ex_p),
inference(resolve,[status(thm)],[c_140,c_112]) ).
cnf(c_142,plain,
sK2(uri_ex_p) = uri_ex_w,
inference(copy,[status(thm)],[c_158]) ).
cnf(c_159,plain,
uri_ex_w != sK0(uri_ex_p),
inference(paramod,[status(thm)],[c_142,c_101]) ).
cnf(c_146,plain,
sK0(uri_ex_p) != uri_ex_w,
inference(copy,[status(thm)],[c_159]) ).
cnf(c_160,plain,
uri_ex_w != sK0(uri_ex_p),
inference(copy,[status(thm)],[c_146]) ).
cnf(c_151,plain,
~ icext(sK3,sK0(uri_ex_p)),
inference(resolve,[status(thm)],[c_112,c_160]) ).
cnf(c_152,plain,
~ iext(uri_ex_p,sK0(uri_ex_p),A),
inference(resolve,[status(thm)],[c_46,c_151]) ).
cnf(c_153,plain,
$false,
inference(resolve,[status(thm)],[c_152,c_103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB026+2 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.39 % Computer : n011.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sat Sep 26 11:50:45 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.39 % Process 427410 was started by sandbox2 on n011,
% 0.11/0.39 % Sat Sep 26 11:50:45 2026
% 0.11/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.40
% 0.11/0.40 % From the command line: assign(max_seconds, 300).
% 0.11/0.45
% 0.11/0.45 % SZS status Theorem for theBenchmark
% 0.11/0.45
% 0.11/0.45 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.11/0.45 % Length of proof is 39.
% 0.11/0.45 % Level of proof is 11.
% 0.11/0.45 % Maximum clause weight is 23.000.
% 0.11/0.45 % Given clauses 100.
% 0.11/0.45
% 0.11/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------