%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS146+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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 01:53:19 PM UTC 2026
% Result : Theorem 3.92s 0.95s
% Output : Proof 3.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 20
% Syntax : Number of formulae : 135 ( 39 unt; 0 def)
% Number of atoms : 617 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 777 ( 295 ~; 400 |; 71 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 48 ( 2 sgn 34 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X] :
( cC116(X)
<=> ( cC80(X)
& cC114(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(f10_nnf,plain,
! [X] :
( ( ~ cC80(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC80(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X] :
( ( ~ cC80(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC80(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c30,plain,
( ~ cC80(X0)
| ~ cC114(X0)
| cC116(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f9,axiom,
! [X] :
( cC114(X)
<=> ( ~ cC112(X)
& ~ cC96(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f9_nnf,plain,
! [X] :
( ( cC112(X)
| cC96(X)
| cC114(X) )
& ( ( ~ cC112(X)
& ~ cC96(X) )
| ~ cC114(X) ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] :
( ( cC112(X)
| cC96(X)
| cC114(X) )
& ( ( ~ cC112(X)
& ~ cC96(X) )
| ~ cC114(X) ) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c27,plain,
( cC112(X0)
| cC96(X0)
| cC114(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f76,axiom,
~ cC96(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_76) ).
fof(f76_nnf,plain,
~ cC96(iV822576),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
~ cC96(iV822576),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c210,plain,
~ cC96(iV822576),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(p237,plain,
( cC112(iV822576)
| cC114(iV822576) ),
inference(resolution,[status(thm)],[c27,c210]) ).
cnf(p240,plain,
( cC112(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(resolution,[status(thm)],[c30,p237]) ).
fof(f57,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC76(X)
& ~ cC78(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_57) ).
fof(f57_nnf,plain,
! [X] :
( ( cC76(X)
| cC78(X)
| cC80(X) )
& ( ( ~ cC76(X)
& ~ cC78(X) )
| ~ cC80(X) ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X] :
( ( cC76(X)
| cC78(X)
| cC80(X) )
& ( ( ~ cC76(X)
& ~ cC78(X) )
| ~ cC80(X) ) ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c171,plain,
( cC76(X0)
| cC78(X0)
| cC80(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f88,axiom,
~ cC78(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_88) ).
fof(f88_nnf,plain,
~ cC78(iV822576),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
~ cC78(iV822576),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c222,plain,
~ cC78(iV822576),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(p260,plain,
( cC76(iV822576)
| cC80(iV822576) ),
inference(resolution,[status(thm)],[c171,c222]) ).
fof(f86,axiom,
~ cC76(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_86) ).
fof(f86_nnf,plain,
~ cC76(iV822576),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
~ cC76(iV822576),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c220,plain,
~ cC76(iV822576),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(p263,plain,
cC80(iV822576),
inference(resolution,[status(thm)],[p260,c220]) ).
cnf(p280,plain,
( cC112(iV822576)
| cC116(iV822576) ),
inference(resolution,[status(thm)],[p240,p263]) ).
fof(f21,axiom,
! [X] :
( cC136(X)
<=> ( ~ cC134(X)
& cC116(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
fof(f21_nnf,plain,
! [X] :
( ( cC134(X)
| ~ cC116(X)
| cC136(X) )
& ( ( ~ cC134(X)
& cC116(X) )
| ~ cC136(X) ) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X] :
( ( cC134(X)
| ~ cC116(X)
| cC136(X) )
& ( ( ~ cC134(X)
& cC116(X) )
| ~ cC136(X) ) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c63,plain,
( cC134(X0)
| ~ cC116(X0)
| cC136(X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p281,plain,
( cC134(iV822576)
| cC136(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p280,c63]) ).
fof(f65,axiom,
! [X] :
( cC96(X)
<=> ( cC2(X)
& ~ cC94(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_65) ).
fof(f65_nnf,plain,
! [X] :
( ( ~ cC2(X)
| cC94(X)
| cC96(X) )
& ( ( cC2(X)
& ~ cC94(X) )
| ~ cC96(X) ) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X] :
( ( ~ cC2(X)
| cC94(X)
| cC96(X) )
& ( ( cC2(X)
& ~ cC94(X) )
| ~ cC96(X) ) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c195,plain,
( ~ cC2(X0)
| cC94(X0)
| cC96(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
fof(f89,axiom,
cC2(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_89) ).
fof(f89_nnf,plain,
cC2(iV822576),
inference(nnf_transformation,[status(thm)],[f89]) ).
cnf(c223,plain,
cC2(iV822576),
inference(cnf_transformation,[status(esa)],[f89_nnf]) ).
cnf(p269,plain,
( cC94(iV822576)
| cC96(iV822576) ),
inference(resolution,[status(thm)],[c195,c223]) ).
fof(f1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f1_nnf,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c3,plain,
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f0_nnf,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
cowlThing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f91,conjecture,
( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f91_neg,negated_conjecture,
~ ( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f91]) ).
fof(f91_nnf,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f91_neg]) ).
fof(f91_sk,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ( ~ xsd_integer(sk14)
& ~ xsd_string(sk14) )
| ( xsd_integer(sk14)
& xsd_string(sk14) )
| cowlNothing(sk13)
| ~ cowlThing(sk13) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13,sk14])],[f91_nnf]) ).
cnf(c226,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sk14)
| xsd_string(sk14)
| cowlNothing(sk13)
| ~ cowlThing(sk13) ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(p229,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sk14)
| xsd_string(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[c0,c226]) ).
cnf(p231,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_string(sk14)
| cowlNothing(sk13)
| xsd_string(sk14) ),
inference(resolution,[status(thm)],[c3,p229]) ).
cnf(p232,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14) ),
inference(factoring,[status(thm)],[p231]) ).
cnf(p270,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576) ),
inference(resolution,[status(thm)],[p269,p232]) ).
cnf(p271,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576) ),
inference(resolution,[status(thm)],[p270,c0]) ).
fof(f44,axiom,
! [X] :
( cC58(X)
<=> ( cC56(X)
& cC34(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
fof(f44_nnf,plain,
! [X] :
( ( ~ cC56(X)
| ~ cC34(X)
| cC58(X) )
& ( ( cC56(X)
& cC34(X) )
| ~ cC58(X) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [X] :
( ( ~ cC56(X)
| ~ cC34(X)
| cC58(X) )
& ( ( cC56(X)
& cC34(X) )
| ~ cC58(X) ) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c132,plain,
( ~ cC56(X0)
| ~ cC34(X0)
| cC58(X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f74,axiom,
cC34(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_74) ).
fof(f74_nnf,plain,
cC34(iV822576),
inference(nnf_transformation,[status(thm)],[f74]) ).
cnf(c208,plain,
cC34(iV822576),
inference(cnf_transformation,[status(esa)],[f74_nnf]) ).
cnf(p257,plain,
( ~ cC56(iV822576)
| cC58(iV822576) ),
inference(resolution,[status(thm)],[c132,c208]) ).
fof(f43,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC10(X)
& cC4(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
fof(f43_nnf,plain,
! [X] :
( ( cC10(X)
| ~ cC4(X)
| cC56(X) )
& ( ( ~ cC10(X)
& cC4(X) )
| ~ cC56(X) ) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [X] :
( ( cC10(X)
| ~ cC4(X)
| cC56(X) )
& ( ( ~ cC10(X)
& cC4(X) )
| ~ cC56(X) ) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c129,plain,
( cC10(X0)
| ~ cC4(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
fof(f75,axiom,
cC4(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_75) ).
fof(f75_nnf,plain,
cC4(iV822576),
inference(nnf_transformation,[status(thm)],[f75]) ).
cnf(c209,plain,
cC4(iV822576),
inference(cnf_transformation,[status(esa)],[f75_nnf]) ).
cnf(p256,plain,
( cC10(iV822576)
| cC56(iV822576) ),
inference(resolution,[status(thm)],[c129,c209]) ).
cnf(p258,plain,
( cC10(iV822576)
| cC58(iV822576) ),
inference(resolution,[status(thm)],[p257,p256]) ).
cnf(p272,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576) ),
inference(resolution,[status(thm)],[p271,p258]) ).
cnf(p283,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p280,p272]) ).
cnf(p284,plain,
( cC10(iV822576)
| cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p283,p256]) ).
cnf(p285,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(factoring,[status(thm)],[p284]) ).
fof(f8,axiom,
! [X] :
( cC112(X)
<=> ( cC4(X)
& ~ cC110(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(f8_nnf,plain,
! [X] :
( ( ~ cC4(X)
| cC110(X)
| cC112(X) )
& ( ( cC4(X)
& ~ cC110(X) )
| ~ cC112(X) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] :
( ( ~ cC4(X)
| cC110(X)
| cC112(X) )
& ( ( cC4(X)
& ~ cC110(X) )
| ~ cC112(X) ) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c24,plain,
( ~ cC4(X0)
| cC110(X0)
| cC112(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p235,plain,
( cC110(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[c24,c209]) ).
fof(f87,axiom,
~ cC112(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_87) ).
fof(f87_nnf,plain,
~ cC112(iV822576),
inference(nnf_transformation,[status(thm)],[f87]) ).
fof(f87_sk,plain,
~ cC112(iV822576),
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c221,plain,
~ cC112(iV822576),
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(p236,plain,
cC110(iV822576),
inference(resolution,[status(thm)],[p235,c221]) ).
cnf(p287,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p285,p236]) ).
cnf(p288,plain,
( cC112(iV822576)
| cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p287,p237]) ).
cnf(p289,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(factoring,[status(thm)],[p288]) ).
cnf(p303,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576)
| cC134(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p281,p289]) ).
cnf(p305,plain,
( cC10(iV822576)
| ~ cC80(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC134(iV822576)
| cC112(iV822576) ),
inference(factoring,[status(thm)],[p303]) ).
cnf(p306,plain,
( cC10(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC134(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p305,p263]) ).
fof(f71,axiom,
~ cC134(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_71) ).
fof(f71_nnf,plain,
~ cC134(iV822576),
inference(nnf_transformation,[status(thm)],[f71]) ).
fof(f71_sk,plain,
~ cC134(iV822576),
inference(skolemisation,[status(esa)],[f71_nnf]) ).
cnf(c205,plain,
~ cC134(iV822576),
inference(cnf_transformation,[status(esa)],[f71_sk]) ).
cnf(p307,plain,
( cC10(iV822576)
| cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p306,c205]) ).
fof(f84,axiom,
~ cC10(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_84) ).
fof(f84_nnf,plain,
~ cC10(iV822576),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
~ cC10(iV822576),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c218,plain,
~ cC10(iV822576),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(p308,plain,
( cowlNothing(sk13)
| xsd_string(sk14)
| cC96(iV822576)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p307,c218]) ).
cnf(p309,plain,
( cowlNothing(sk13)
| xsd_string(sk14)
| cC112(iV822576) ),
inference(resolution,[status(thm)],[p308,c210]) ).
cnf(p310,plain,
( cowlNothing(sk13)
| xsd_string(sk14) ),
inference(resolution,[status(thm)],[p309,c221]) ).
cnf(c227,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_string(sk14)
| xsd_integer(sk14)
| cowlNothing(sk13)
| ~ cowlThing(sk13) ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(p230,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_string(sk14)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[c0,c227]) ).
cnf(p311,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p310,p230]) ).
cnf(p313,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(factoring,[status(thm)],[p311]) ).
cnf(p315,plain,
( cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p313,p269]) ).
cnf(p316,plain,
( cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p315,c0]) ).
cnf(p317,plain,
( cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p316,p258]) ).
cnf(p318,plain,
( cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p317,p280]) ).
cnf(p319,plain,
( cC10(iV822576)
| cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p318,p256]) ).
cnf(p320,plain,
( cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(factoring,[status(thm)],[p319]) ).
cnf(p322,plain,
( cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p320,p236]) ).
cnf(p323,plain,
( cC112(iV822576)
| cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p322,p237]) ).
cnf(p324,plain,
( cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(p325,plain,
( cC134(iV822576)
| cC112(iV822576)
| cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p324,p281]) ).
cnf(p326,plain,
( cC134(iV822576)
| cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| ~ cC80(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(factoring,[status(thm)],[p325]) ).
cnf(p327,plain,
( cC134(iV822576)
| cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p326,p263]) ).
cnf(p328,plain,
( cC112(iV822576)
| cC10(iV822576)
| cC96(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p327,c205]) ).
cnf(p329,plain,
( cC112(iV822576)
| cC96(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p328,c218]) ).
cnf(p330,plain,
( cC112(iV822576)
| xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p329,c210]) ).
cnf(p331,plain,
( xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p330,c221]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p312,plain,
( ~ xsd_integer(sk14)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p310,c2]) ).
cnf(p332,plain,
( cowlNothing(sk13)
| cowlNothing(sk13) ),
inference(resolution,[status(thm)],[p331,p312]) ).
cnf(p333,plain,
cowlNothing(sk13),
inference(factoring,[status(thm)],[p332]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p334,plain,
$false,
inference(resolution,[status(thm)],[p333,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS146+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 19:32:09 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.92/0.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.92/0.95 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------