%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS167+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 07:46:14 AM UTC 2026
% Result : Theorem 0.07s 15.47s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 5
% Syntax : Number of formulae : 109 ( 14 unt; 0 def)
% Number of atoms : 399 ( 40 equ)
% Maximal formula atoms : 24 ( 3 avg)
% Number of connectives : 435 ( 145 ~; 239 |; 42 &)
% ( 7 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-1 aty)
% Number of variables : 92 ( 8 sgn 50 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_2,axiom,
! [X] :
( cc1(X)
<=> ( ! [Y0,Y1] :
( ( rp(X,Y1)
& rp(X,Y0) )
=> Y0 = Y1 )
& ? [Y0] : rp(X,Y0) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_3,axiom,
! [X] :
( cc2(X)
<=> ( ! [Y0,Y1] :
( ( rp(X,Y1)
& rp(X,Y0) )
=> Y0 = Y1 )
& ? [Y0] : rp(X,Y0) ) ),
file('theBenchmark.p',axiom_3) ).
fof(the_axiom,conjecture,
( ! [X] :
( cc1(X)
<=> cc2(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( ! [X] :
( cc1(X)
<=> cc2(X) )
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_22,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_23,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_24,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_25,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
fof(nnf_11,plain,
! [X] :
( ( ? [Y0,Y1] :
( Y1 != Y0
& rp(X,Y1)
& rp(X,Y0) )
| ! [X3] : ~ rp(X,X3)
| cc1(X) )
& ( ( ! [X1,X2] :
( X2 = X1
| ~ rp(X,X2)
| ~ rp(X,X1) )
& ? [X0] : rp(X,X0) )
| ~ cc1(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_2]) ).
fof(sk_axiom_2_sk,plain,
! [X] :
( ( ( sK2(X) != sK1(X)
& rp(X,sK2(X))
& rp(X,sK1(X)) )
| ! [X3] : ~ rp(X,X3)
| cc1(X) )
& ( ( ! [X1,X2] :
( X2 = X1
| ~ rp(X,X2)
| ~ rp(X,X1) )
& rp(X,sK0(X)) )
| ~ cc1(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0(X)),skolemize(Y0,sK1(X)),skolemize(Y1,sK2(X))],[nnf_11]) ).
fof(sk_axiom_2,plain,
( ! [VAR_0,VAR_1] :
( sK2(VAR_0) != sK1(VAR_0)
| ~ rp(VAR_0,VAR_1)
| cc1(VAR_0) )
& ! [VAR_0,VAR_1] :
( rp(VAR_0,sK2(VAR_0))
| ~ rp(VAR_0,VAR_1)
| cc1(VAR_0) )
& ! [VAR_0,VAR_1] :
( rp(VAR_0,sK1(VAR_0))
| ~ rp(VAR_0,VAR_1)
| cc1(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = VAR_1
| ~ rp(VAR_0,VAR_2)
| ~ rp(VAR_0,VAR_1)
| ~ cc1(VAR_0) )
& ! [VAR_0] :
( rp(VAR_0,sK0(VAR_0))
| ~ cc1(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_2_sk]) ).
cnf(c_26,plain,
( rp(A,sK0(A))
| ~ cc1(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_2]) ).
cnf(c_27,plain,
( C = B
| ~ rp(A,C)
| ~ rp(A,B)
| ~ cc1(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_2]) ).
cnf(c_28,plain,
( rp(A,sK1(A))
| ~ rp(A,B)
| cc1(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_2]) ).
cnf(c_29,plain,
( rp(A,sK2(A))
| ~ rp(A,B)
| cc1(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_2]) ).
cnf(c_30,plain,
( sK2(A) != sK1(A)
| ~ rp(A,B)
| cc1(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_2]) ).
fof(nnf_12,plain,
! [X] :
( ( ? [Y0,Y1] :
( Y1 != Y0
& rp(X,Y1)
& rp(X,Y0) )
| ! [X3] : ~ rp(X,X3)
| cc2(X) )
& ( ( ! [X1,X2] :
( X2 = X1
| ~ rp(X,X2)
| ~ rp(X,X1) )
& ? [X0] : rp(X,X0) )
| ~ cc2(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_3]) ).
fof(sk_axiom_3_sk,plain,
! [X] :
( ( ( sK5(X) != sK4(X)
& rp(X,sK5(X))
& rp(X,sK4(X)) )
| ! [X3] : ~ rp(X,X3)
| cc2(X) )
& ( ( ! [X1,X2] :
( X2 = X1
| ~ rp(X,X2)
| ~ rp(X,X1) )
& rp(X,sK3(X)) )
| ~ cc2(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3(X)),skolemize(Y0,sK4(X)),skolemize(Y1,sK5(X))],[nnf_12]) ).
fof(sk_axiom_3,plain,
( ! [VAR_0,VAR_1] :
( sK5(VAR_0) != sK4(VAR_0)
| ~ rp(VAR_0,VAR_1)
| cc2(VAR_0) )
& ! [VAR_0,VAR_1] :
( rp(VAR_0,sK5(VAR_0))
| ~ rp(VAR_0,VAR_1)
| cc2(VAR_0) )
& ! [VAR_0,VAR_1] :
( rp(VAR_0,sK4(VAR_0))
| ~ rp(VAR_0,VAR_1)
| cc2(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = VAR_1
| ~ rp(VAR_0,VAR_2)
| ~ rp(VAR_0,VAR_1)
| ~ cc2(VAR_0) )
& ! [VAR_0] :
( rp(VAR_0,sK3(VAR_0))
| ~ cc2(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_3_sk]) ).
cnf(c_31,plain,
( rp(A,sK3(A))
| ~ cc2(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_3]) ).
cnf(c_32,plain,
( C = B
| ~ rp(A,C)
| ~ rp(A,B)
| ~ cc2(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_3]) ).
cnf(c_33,plain,
( rp(A,sK4(A))
| ~ rp(A,B)
| cc2(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_3]) ).
cnf(c_34,plain,
( rp(A,sK5(A))
| ~ rp(A,B)
| cc2(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_3]) ).
cnf(c_35,plain,
( sK5(A) != sK4(A)
| ~ rp(A,B)
| cc2(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_3]) ).
fof(nnf_13,plain,
( ? [X] :
( ( ~ cc2(X)
| ~ cc1(X) )
& ( cc2(X)
| cc1(X) ) )
| ? [X3] :
( ( xsd_integer(X3)
| ~ xsd_string(X3) )
& ( ~ xsd_integer(X3)
| xsd_string(X3) ) )
| ? [X1] :
( cowlNothing(X1)
| ~ cowlThing(X1) ) ),
inference(fof_nnf,[status(thm)],[the_axiom_neg]) ).
fof(sk_the_axiom_neg_sk,plain,
( ( ( ~ cc2(sK8)
| ~ cc1(sK8) )
& ( cc2(sK8)
| cc1(sK8) ) )
| ( ( xsd_integer(sK7)
| ~ xsd_string(sK7) )
& ( ~ xsd_integer(sK7)
| xsd_string(sK7) ) )
| cowlNothing(sK6)
| ~ cowlThing(sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8]),skolemize(X1,sK6),skolemize(X3,sK7),skolemize(X,sK8)],[nnf_13]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) )
& ( cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) )
& ( ~ cc2(sK8)
| ~ cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) )
& ( cc2(sK8)
| cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_36,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_307,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6) ),
inference(resolve,[status(thm)],[c_22,c_36]) ).
cnf(c_37,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_23,c_307]) ).
cnf(c_38,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_308,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7)
| cowlNothing(sK6) ),
inference(resolve,[status(thm)],[c_22,c_38]) ).
cnf(c_39,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| ~ xsd_integer(sK7)
| xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_23,c_308]) ).
cnf(c_40,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_309,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6) ),
inference(resolve,[status(thm)],[c_22,c_40]) ).
cnf(c_41,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_23,c_309]) ).
cnf(c_42,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6)
| ~ cowlThing(sK6) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_310,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7)
| cowlNothing(sK6) ),
inference(resolve,[status(thm)],[c_22,c_42]) ).
cnf(c_43,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7)
| ~ xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_23,c_310]) ).
cnf(c_311,negated_conjecture,
( xsd_string(sK7)
| cc2(sK8)
| cc1(sK8)
| xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_37,c_25]) ).
cnf(c_46,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| xsd_string(sK7) ),
inference(copy,[status(thm)],[c_311]) ).
cnf(c_312,negated_conjecture,
( xsd_string(sK7)
| ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_39,c_25]) ).
cnf(c_47,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_string(sK7) ),
inference(copy,[status(thm)],[c_312]) ).
cnf(c_313,negated_conjecture,
( xsd_integer(sK7)
| cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7) ),
inference(resolve,[status(thm)],[c_41,c_25]) ).
cnf(c_48,negated_conjecture,
( cc2(sK8)
| cc1(sK8)
| xsd_integer(sK7) ),
inference(copy,[status(thm)],[c_313]) ).
cnf(c_314,negated_conjecture,
( xsd_integer(sK7)
| ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7) ),
inference(resolve,[status(thm)],[c_43,c_25]) ).
cnf(c_49,negated_conjecture,
( ~ cc2(sK8)
| ~ cc1(sK8)
| xsd_integer(sK7) ),
inference(copy,[status(thm)],[c_314]) ).
cnf(c_50,plain,
( ~ xsd_integer(sK7)
| cc2(sK8)
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_46,c_24]) ).
cnf(c_315,plain,
( cc2(sK8)
| cc1(sK8)
| cc2(sK8)
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_50,c_48]) ).
cnf(c_316,plain,
( cc2(sK8)
| cc2(sK8)
| cc1(sK8) ),
inference(copy,[status(thm)],[c_315]) ).
cnf(c_66,plain,
( cc2(sK8)
| cc1(sK8) ),
inference(copy,[status(thm)],[c_316]) ).
cnf(c_78,plain,
( B = A
| ~ rp(sK8,B)
| ~ rp(sK8,A)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_66,c_27]) ).
cnf(c_79,plain,
( rp(sK8,sK0(sK8))
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_66,c_26]) ).
cnf(c_82,plain,
( rp(sK8,sK3(sK8))
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_66,c_31]) ).
cnf(c_317,plain,
( sK5(sK8) != sK4(sK8)
| cc2(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_79,c_35]) ).
cnf(c_87,plain,
( sK5(sK8) != sK4(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_317]) ).
cnf(c_318,plain,
( rp(sK8,sK5(sK8))
| cc2(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_79,c_34]) ).
cnf(c_88,plain,
( rp(sK8,sK5(sK8))
| cc2(sK8) ),
inference(copy,[status(thm)],[c_318]) ).
cnf(c_319,plain,
( rp(sK8,sK4(sK8))
| cc2(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_79,c_33]) ).
cnf(c_89,plain,
( rp(sK8,sK4(sK8))
| cc2(sK8) ),
inference(copy,[status(thm)],[c_319]) ).
cnf(c_320,plain,
( sK2(sK8) != sK1(sK8)
| cc1(sK8)
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_82,c_30]) ).
cnf(c_96,plain,
( sK2(sK8) != sK1(sK8)
| cc1(sK8) ),
inference(copy,[status(thm)],[c_320]) ).
cnf(c_321,plain,
( rp(sK8,sK2(sK8))
| cc1(sK8)
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_82,c_29]) ).
cnf(c_97,plain,
( rp(sK8,sK2(sK8))
| cc1(sK8) ),
inference(copy,[status(thm)],[c_321]) ).
cnf(c_322,plain,
( rp(sK8,sK1(sK8))
| cc1(sK8)
| cc1(sK8) ),
inference(resolve,[status(thm)],[c_82,c_28]) ).
cnf(c_98,plain,
( rp(sK8,sK1(sK8))
| cc1(sK8) ),
inference(copy,[status(thm)],[c_322]) ).
cnf(c_323,plain,
( cc2(sK8)
| A = sK0(sK8)
| ~ rp(sK8,A)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_78,c_79]) ).
cnf(c_324,plain,
( cc2(sK8)
| sK0(sK8) = A
| ~ rp(sK8,A)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_323]) ).
cnf(c_101,plain,
( sK0(sK8) = A
| ~ rp(sK8,A)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_324]) ).
cnf(c_118,plain,
( ~ cc2(sK8)
| xsd_integer(sK7)
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_97,c_49]) ).
cnf(c_119,plain,
( ~ cc2(sK8)
| xsd_string(sK7)
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_97,c_47]) ).
cnf(c_126,plain,
( ~ cc2(sK8)
| xsd_integer(sK7)
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_98,c_49]) ).
cnf(c_127,plain,
( ~ cc2(sK8)
| xsd_string(sK7)
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_98,c_47]) ).
cnf(c_325,plain,
( cc2(sK8)
| sK0(sK8) = sK4(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_101,c_89]) ).
cnf(c_326,plain,
( cc2(sK8)
| sK4(sK8) = sK0(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_194,plain,
( sK4(sK8) = sK0(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_326]) ).
cnf(c_327,plain,
( cc2(sK8)
| sK0(sK8) = sK5(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_101,c_88]) ).
cnf(c_328,plain,
( cc2(sK8)
| sK5(sK8) = sK0(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_327]) ).
cnf(c_195,plain,
( sK5(sK8) = sK0(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_328]) ).
cnf(c_329,plain,
( sK5(sK8) != sK0(sK8)
| cc2(sK8)
| cc2(sK8) ),
inference(paramod,[status(thm)],[c_194,c_87]) ).
cnf(c_220,plain,
( sK5(sK8) != sK0(sK8)
| cc2(sK8) ),
inference(copy,[status(thm)],[c_329]) ).
cnf(c_330,plain,
( cc2(sK8)
| cc2(sK8) ),
inference(resolve,[status(thm)],[c_220,c_195]) ).
cnf(c_248,plain,
cc2(sK8),
inference(copy,[status(thm)],[c_330]) ).
cnf(c_253,plain,
( xsd_string(sK7)
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_248,c_127]) ).
cnf(c_254,plain,
( xsd_integer(sK7)
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_248,c_126]) ).
cnf(c_255,plain,
( xsd_string(sK7)
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_248,c_119]) ).
cnf(c_256,plain,
( xsd_integer(sK7)
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_248,c_118]) ).
cnf(c_257,negated_conjecture,
( ~ cc1(sK8)
| xsd_integer(sK7) ),
inference(resolve,[status(thm)],[c_248,c_49]) ).
cnf(c_258,negated_conjecture,
( ~ cc1(sK8)
| xsd_string(sK7) ),
inference(resolve,[status(thm)],[c_248,c_47]) ).
cnf(c_260,plain,
rp(sK8,sK3(sK8)),
inference(resolve,[status(thm)],[c_248,c_31]) ).
cnf(c_331,plain,
( sK3(sK8) = A
| ~ rp(sK8,A)
| ~ cc2(sK8) ),
inference(resolve,[status(thm)],[c_260,c_32]) ).
cnf(c_262,plain,
( sK3(sK8) = A
| ~ rp(sK8,A) ),
inference(resolve,[status(thm)],[c_248,c_331]) ).
cnf(c_268,plain,
( ~ xsd_integer(sK7)
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_253,c_24]) ).
cnf(c_278,plain,
( ~ xsd_integer(sK7)
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_255,c_24]) ).
cnf(c_332,plain,
( rp(sK8,sK1(sK8))
| rp(sK8,sK1(sK8)) ),
inference(resolve,[status(thm)],[c_268,c_254]) ).
cnf(c_286,plain,
rp(sK8,sK1(sK8)),
inference(copy,[status(thm)],[c_332]) ).
cnf(c_333,plain,
( rp(sK8,sK2(sK8))
| rp(sK8,sK2(sK8)) ),
inference(resolve,[status(thm)],[c_278,c_256]) ).
cnf(c_292,plain,
rp(sK8,sK2(sK8)),
inference(copy,[status(thm)],[c_333]) ).
cnf(c_296,plain,
sK3(sK8) = sK2(sK8),
inference(resolve,[status(thm)],[c_262,c_292]) ).
cnf(c_334,plain,
sK3(sK8) = sK1(sK8),
inference(resolve,[status(thm)],[c_262,c_286]) ).
cnf(c_297,plain,
sK2(sK8) = sK1(sK8),
inference(paramod,[status(thm)],[c_296,c_334]) ).
cnf(c_335,plain,
( sK1(sK8) != sK1(sK8)
| cc1(sK8) ),
inference(paramod,[status(thm)],[c_297,c_96]) ).
cnf(c_301,plain,
cc1(sK8),
inference(copy,[status(thm)],[c_335]) ).
cnf(c_302,negated_conjecture,
xsd_string(sK7),
inference(resolve,[status(thm)],[c_301,c_258]) ).
cnf(c_303,negated_conjecture,
xsd_integer(sK7),
inference(resolve,[status(thm)],[c_301,c_257]) ).
cnf(c_336,plain,
~ xsd_integer(sK7),
inference(resolve,[status(thm)],[c_302,c_24]) ).
cnf(c_306,plain,
$false,
inference(resolve,[status(thm)],[c_303,c_336]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS167+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/15.41 % CPULimit : 300
% 0.07/15.41 % WCLimit : 300
% 0.07/15.41 % DateTime : Fri Sep 25 19:42:11 UTC 2026
% 0.07/15.41 % CPUTime :
% 0.07/15.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/15.42 % Process 3578769 was started by sandbox on n006,
% 0.07/15.42 % Fri Sep 25 19:42:11 2026
% 0.07/15.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/15.42
% 0.07/15.42 % From the command line: assign(max_seconds, 300).
% 0.07/15.47
% 0.07/15.47 % SZS status Theorem for theBenchmark
% 0.07/15.47
% 0.07/15.47 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.07/15.47 % Length of proof is 69.
% 0.07/15.47 % Level of proof is 18.
% 0.07/15.47 % Maximum clause weight is 14.000.
% 0.07/15.47 % Given clauses 97.
% 0.07/15.47
% 0.07/15.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------