%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KRS154+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n014.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:54:17 PM UTC 2026
% Result : Theorem 2.94s 1.30s
% Output : CNFRefutation 2.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 24
% Syntax : Number of formulae : 122 ( 47 unt; 0 def)
% Number of atoms : 415 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 499 ( 206 ~; 203 |; 77 &)
% ( 12 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 65 ( 0 sgn 61 !; 4 ?; 16 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f16,axiom,
! [X0] :
( cC110(X0)
<=> ( cC108xcomp(X0)
& cC102xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f22,axiom,
! [X0] :
( cC114(X0)
<=> ( cC96xcomp(X0)
& cC112xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
fof(f23,axiom,
! [X0] :
( cC116(X0)
<=> ( cC80(X0)
& cC114(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(f43,axiom,
! [X0] :
( cC136(X0)
<=> ( cC116(X0)
& cC134xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_42) ).
fof(f94,axiom,
! [X0] :
( cC56(X0)
<=> ( cC10xcomp(X0)
& cC4(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_93) ).
fof(f95,axiom,
! [X0] :
( cC58(X0)
<=> ( cC56(X0)
& cC34(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_94) ).
fof(f118,axiom,
! [X0] :
( cC80(X0)
<=> ( cC76xcomp(X0)
& cC78xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_117) ).
fof(f137,axiom,
! [X0] :
( cC94(X0)
<=> ( cC92xcomp(X0)
& cC86xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_136) ).
fof(f148,axiom,
cC102xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_147) ).
fof(f149,axiom,
cC108xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_148) ).
fof(f150,axiom,
cC4(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_149) ).
fof(f152,axiom,
cC112xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_151) ).
fof(f153,axiom,
cC76xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_152) ).
fof(f154,axiom,
cC96xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_153) ).
fof(f159,axiom,
cC78xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_158) ).
fof(f161,axiom,
cC134xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_160) ).
fof(f162,axiom,
cC86xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_161) ).
fof(f163,axiom,
cC34(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_162) ).
fof(f167,axiom,
cowlThing(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_166) ).
fof(f168,axiom,
cC10xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_167) ).
fof(f169,axiom,
cC92xcomp(iV822576),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_168) ).
fof(f170,conjecture,
( cC56(iV822576)
& cC136(iV822576)
& cC110(iV822576)
& cC80(iV822576)
& cC94(iV822576)
& cowlThing(iV822576)
& cC114(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f171,negated_conjecture,
~ ( cC56(iV822576)
& cC136(iV822576)
& cC110(iV822576)
& cC80(iV822576)
& cC94(iV822576)
& cowlThing(iV822576)
& cC114(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negated_conjecture,[status(cth)],[f170]) ).
fof(f172,plain,
~ ( cC56(iV822576)
& cC136(iV822576)
& cC110(iV822576)
& cC80(iV822576)
& cC94(iV822576)
& cowlThing(iV822576)
& cC114(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(rectify,[],[f171]) ).
fof(f220,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(ennf_transformation,[],[f172]) ).
fof(f221,plain,
! [X0] :
( ( ~ xsd_string(X0)
| ~ xsd_integer(X0) )
& ( xsd_integer(X0)
| xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f256,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cC108xcomp(X0)
& cC102xcomp(X0) ) )
& ( ~ cC108xcomp(X0)
| ~ cC102xcomp(X0)
| cC110(X0) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f257,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cC108xcomp(X0)
& cC102xcomp(X0) ) )
& ( ~ cC108xcomp(X0)
| ~ cC102xcomp(X0)
| cC110(X0) ) ),
inference(flattening,[],[f256]) ).
fof(f272,plain,
! [X0] :
( ( ~ cC114(X0)
| ( cC96xcomp(X0)
& cC112xcomp(X0) ) )
& ( ~ cC96xcomp(X0)
| ~ cC112xcomp(X0)
| cC114(X0) ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f273,plain,
! [X0] :
( ( ~ cC114(X0)
| ( cC96xcomp(X0)
& cC112xcomp(X0) ) )
& ( ~ cC96xcomp(X0)
| ~ cC112xcomp(X0)
| cC114(X0) ) ),
inference(flattening,[],[f272]) ).
fof(f274,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC80(X0)
& cC114(X0) ) )
& ( ~ cC80(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(nnf_transformation,[],[f23]) ).
fof(f275,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC80(X0)
& cC114(X0) ) )
& ( ~ cC80(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(flattening,[],[f274]) ).
fof(f319,plain,
! [X0] :
( ( ~ cC136(X0)
| ( cC116(X0)
& cC134xcomp(X0) ) )
& ( ~ cC116(X0)
| ~ cC134xcomp(X0)
| cC136(X0) ) ),
inference(nnf_transformation,[],[f43]) ).
fof(f320,plain,
! [X0] :
( ( ~ cC136(X0)
| ( cC116(X0)
& cC134xcomp(X0) ) )
& ( ~ cC116(X0)
| ~ cC134xcomp(X0)
| cC136(X0) ) ),
inference(flattening,[],[f319]) ).
fof(f435,plain,
! [X0] :
( ( ~ cC56(X0)
| ( cC10xcomp(X0)
& cC4(X0) ) )
& ( ~ cC10xcomp(X0)
| ~ cC4(X0)
| cC56(X0) ) ),
inference(nnf_transformation,[],[f94]) ).
fof(f436,plain,
! [X0] :
( ( ~ cC56(X0)
| ( cC10xcomp(X0)
& cC4(X0) ) )
& ( ~ cC10xcomp(X0)
| ~ cC4(X0)
| cC56(X0) ) ),
inference(flattening,[],[f435]) ).
fof(f437,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cC56(X0)
& cC34(X0) ) )
& ( ~ cC56(X0)
| ~ cC34(X0)
| cC58(X0) ) ),
inference(nnf_transformation,[],[f95]) ).
fof(f438,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cC56(X0)
& cC34(X0) ) )
& ( ~ cC56(X0)
| ~ cC34(X0)
| cC58(X0) ) ),
inference(flattening,[],[f437]) ).
fof(f485,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cC76xcomp(X0)
& cC78xcomp(X0) ) )
& ( ~ cC76xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ) ),
inference(nnf_transformation,[],[f118]) ).
fof(f486,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cC76xcomp(X0)
& cC78xcomp(X0) ) )
& ( ~ cC76xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ) ),
inference(flattening,[],[f485]) ).
fof(f527,plain,
! [X0] :
( ( ~ cC94(X0)
| ( cC92xcomp(X0)
& cC86xcomp(X0) ) )
& ( ~ cC92xcomp(X0)
| ~ cC86xcomp(X0)
| cC94(X0) ) ),
inference(nnf_transformation,[],[f137]) ).
fof(f528,plain,
! [X0] :
( ( ~ cC94(X0)
| ( cC92xcomp(X0)
& cC86xcomp(X0) ) )
& ( ~ cC92xcomp(X0)
| ~ cC86xcomp(X0)
| cC94(X0) ) ),
inference(flattening,[],[f527]) ).
fof(f548,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ? [X1] :
( ( xsd_string(X1)
| ~ xsd_integer(X1) )
& ( ~ xsd_string(X1)
| xsd_integer(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(nnf_transformation,[],[f220]) ).
fof(f549,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ( ( xsd_string(sK81)
| ~ xsd_integer(sK81) )
& ( ~ xsd_string(sK81)
| xsd_integer(sK81) ) )
| cowlNothing(sK80)
| ~ cowlThing(sK80) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80,sK81]),skolemize(X0,sK80),skolemize(X1,sK81)],[f548]) ).
fof(f550,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f551,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f552,plain,
! [X0] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf_transformation,[],[f221]) ).
fof(f553,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f221]) ).
fof(f586,plain,
! [X0] :
( ~ cC108xcomp(X0)
| ~ cC102xcomp(X0)
| cC110(X0) ),
inference(cnf_transformation,[],[f257]) ).
fof(f600,plain,
! [X0] :
( ~ cC96xcomp(X0)
| ~ cC112xcomp(X0)
| cC114(X0) ),
inference(cnf_transformation,[],[f273]) ).
fof(f603,plain,
! [X0] :
( ~ cC80(X0)
| ~ cC114(X0)
| cC116(X0) ),
inference(cnf_transformation,[],[f275]) ).
fof(f651,plain,
! [X0] :
( ~ cC116(X0)
| ~ cC134xcomp(X0)
| cC136(X0) ),
inference(cnf_transformation,[],[f320]) ).
fof(f756,plain,
! [X0] :
( ~ cC10xcomp(X0)
| ~ cC4(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f436]) ).
fof(f759,plain,
! [X0] :
( ~ cC56(X0)
| ~ cC34(X0)
| cC58(X0) ),
inference(cnf_transformation,[],[f438]) ).
fof(f808,plain,
! [X0] :
( ~ cC76xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f486]) ).
fof(f849,plain,
! [X0] :
( ~ cC92xcomp(X0)
| ~ cC86xcomp(X0)
| cC94(X0) ),
inference(cnf_transformation,[],[f528]) ).
fof(f868,plain,
cC102xcomp(iV822576),
inference(cnf_transformation,[],[f148]) ).
fof(f869,plain,
cC108xcomp(iV822576),
inference(cnf_transformation,[],[f149]) ).
fof(f870,plain,
cC4(iV822576),
inference(cnf_transformation,[],[f150]) ).
fof(f872,plain,
cC112xcomp(iV822576),
inference(cnf_transformation,[],[f152]) ).
fof(f873,plain,
cC76xcomp(iV822576),
inference(cnf_transformation,[],[f153]) ).
fof(f874,plain,
cC96xcomp(iV822576),
inference(cnf_transformation,[],[f154]) ).
fof(f879,plain,
cC78xcomp(iV822576),
inference(cnf_transformation,[],[f159]) ).
fof(f881,plain,
cC134xcomp(iV822576),
inference(cnf_transformation,[],[f161]) ).
fof(f882,plain,
cC86xcomp(iV822576),
inference(cnf_transformation,[],[f162]) ).
fof(f883,plain,
cC34(iV822576),
inference(cnf_transformation,[],[f163]) ).
fof(f887,plain,
cowlThing(iV822576),
inference(cnf_transformation,[],[f167]) ).
fof(f888,plain,
cC10xcomp(iV822576),
inference(cnf_transformation,[],[f168]) ).
fof(f889,plain,
cC92xcomp(iV822576),
inference(cnf_transformation,[],[f169]) ).
fof(f890,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_string(sK81)
| ~ xsd_integer(sK81)
| cowlNothing(sK80)
| ~ cowlThing(sK80) ),
inference(cnf_transformation,[],[f549]) ).
fof(f891,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_string(sK81)
| xsd_integer(sK81)
| cowlNothing(sK80)
| ~ cowlThing(sK80) ),
inference(cnf_transformation,[],[f549]) ).
tcf(c_49,plain,
! [X0: $i] : cowlThing(X0),
inference(cnf_transformation,[],[f551]) ).
tcf(c_50,plain,
! [X0: $i] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f550]) ).
tcf(c_51,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f553]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f552]) ).
tcf(c_83,plain,
! [X0: $i] :
( cC110(X0)
| ~ cC108xcomp(X0)
| ~ cC102xcomp(X0) ),
inference(cnf_transformation,[],[f586]) ).
tcf(c_97,plain,
! [X0: $i] :
( cC114(X0)
| ~ cC96xcomp(X0)
| ~ cC112xcomp(X0) ),
inference(cnf_transformation,[],[f600]) ).
tcf(c_100,plain,
! [X0: $i] :
( cC116(X0)
| ~ cC80(X0)
| ~ cC114(X0) ),
inference(cnf_transformation,[],[f603]) ).
tcf(c_148,plain,
! [X0: $i] :
( cC136(X0)
| ~ cC134xcomp(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[],[f651]) ).
tcf(c_253,plain,
! [X0: $i] :
( cC56(X0)
| ~ cC4(X0)
| ~ cC10xcomp(X0) ),
inference(cnf_transformation,[],[f756]) ).
tcf(c_256,plain,
! [X0: $i] :
( cC58(X0)
| ~ cC56(X0)
| ~ cC34(X0) ),
inference(cnf_transformation,[],[f759]) ).
tcf(c_305,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC78xcomp(X0)
| ~ cC76xcomp(X0) ),
inference(cnf_transformation,[],[f808]) ).
tcf(c_346,plain,
! [X0: $i] :
( cC94(X0)
| ~ cC92xcomp(X0)
| ~ cC86xcomp(X0) ),
inference(cnf_transformation,[],[f849]) ).
tcf(c_367,plain,
cC102xcomp(iV822576),
inference(cnf_transformation,[],[f868]) ).
tcf(c_368,plain,
cC108xcomp(iV822576),
inference(cnf_transformation,[],[f869]) ).
tcf(c_369,plain,
cC4(iV822576),
inference(cnf_transformation,[],[f870]) ).
tcf(c_371,plain,
cC112xcomp(iV822576),
inference(cnf_transformation,[],[f872]) ).
tcf(c_372,plain,
cC76xcomp(iV822576),
inference(cnf_transformation,[],[f873]) ).
tcf(c_373,plain,
cC96xcomp(iV822576),
inference(cnf_transformation,[],[f874]) ).
tcf(c_378,plain,
cC78xcomp(iV822576),
inference(cnf_transformation,[],[f879]) ).
tcf(c_380,plain,
cC134xcomp(iV822576),
inference(cnf_transformation,[],[f881]) ).
tcf(c_381,plain,
cC86xcomp(iV822576),
inference(cnf_transformation,[],[f882]) ).
tcf(c_382,plain,
cC34(iV822576),
inference(cnf_transformation,[],[f883]) ).
tcf(c_386,plain,
cowlThing(iV822576),
inference(cnf_transformation,[],[f887]) ).
tcf(c_387,plain,
cC10xcomp(iV822576),
inference(cnf_transformation,[],[f888]) ).
tcf(c_388,plain,
cC92xcomp(iV822576),
inference(cnf_transformation,[],[f889]) ).
tcf(c_389,negated_conjecture,
( xsd_integer(sK81)
| cowlNothing(sK80)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ xsd_string(sK81)
| ~ cowlThing(sK80)
| ~ cowlThing(iV822576) ),
inference(cnf_transformation,[],[f891]) ).
tcf(c_390,negated_conjecture,
( xsd_string(sK81)
| cowlNothing(sK80)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ xsd_integer(sK81)
| ~ cowlThing(sK80)
| ~ cowlThing(iV822576) ),
inference(cnf_transformation,[],[f890]) ).
tcf(c_596,plain,
( cC94(iV822576)
| ~ cC92xcomp(iV822576)
| ~ cC86xcomp(iV822576) ),
inference(instantiation,[status(thm)],[c_346]) ).
tcf(c_601,plain,
( cC80(iV822576)
| ~ cC78xcomp(iV822576)
| ~ cC76xcomp(iV822576) ),
inference(instantiation,[status(thm)],[c_305]) ).
tcf(c_610,plain,
( cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC34(iV822576) ),
inference(instantiation,[status(thm)],[c_256]) ).
tcf(c_611,plain,
( cC56(iV822576)
| ~ cC4(iV822576)
| ~ cC10xcomp(iV822576) ),
inference(instantiation,[status(thm)],[c_253]) ).
tcf(c_624,plain,
( cC136(iV822576)
| ~ cC134xcomp(iV822576)
| ~ cC116(iV822576) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_633,plain,
( cC116(iV822576)
| ~ cC80(iV822576)
| ~ cC114(iV822576) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_634,plain,
( cC114(iV822576)
| ~ cC96xcomp(iV822576)
| ~ cC112xcomp(iV822576) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_636,plain,
( cC110(iV822576)
| ~ cC108xcomp(iV822576)
| ~ cC102xcomp(iV822576) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_653,negated_conjecture,
( xsd_string(sK81)
| cowlNothing(sK80)
| ~ xsd_integer(sK81)
| ~ cowlThing(sK80) ),
inference(global_subsumption_just,[status(thm)],[c_390,c_388,c_387,c_386,c_382,c_381,c_380,c_378,c_373,c_372,c_371,c_369,c_368,c_367,c_596,c_601,c_610,c_611,c_624,c_633,c_634,c_636,c_390]) ).
tcf(c_655,negated_conjecture,
( xsd_integer(sK81)
| cowlNothing(sK80)
| ~ xsd_string(sK81)
| ~ cowlThing(sK80) ),
inference(global_subsumption_just,[status(thm)],[c_389,c_388,c_387,c_386,c_382,c_381,c_380,c_378,c_373,c_372,c_371,c_369,c_368,c_367,c_596,c_601,c_610,c_611,c_624,c_633,c_634,c_636,c_389]) ).
tcf(c_657,plain,
! [X0: $i] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_658,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(renaming,[status(thm)],[c_657]) ).
tcf(c_659,plain,
! [X0: $i] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_660,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(renaming,[status(thm)],[c_659]) ).
tcf(c_2061,plain,
( xsd_integer(sK81)
| cowlNothing(sK80)
| ~ xsd_string(sK81) ),
inference(backward_subsumption_resolution,[status(thm)],[c_655,c_49]) ).
tcf(c_2062,plain,
( xsd_string(sK81)
| cowlNothing(sK80)
| ~ xsd_integer(sK81) ),
inference(backward_subsumption_resolution,[status(thm)],[c_653,c_49]) ).
tcf(c_2103,plain,
( xsd_string(sK81)
| ~ xsd_integer(sK81) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2062,c_50]) ).
tcf(c_2104,plain,
( xsd_integer(sK81)
| ~ xsd_string(sK81) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2061,c_50]) ).
tcf(c_2108,plain,
xsd_integer(sK81),
inference(backward_subsumption_resolution,[status(thm)],[c_2104,c_660]) ).
tcf(c_2110,plain,
xsd_string(sK81),
inference(backward_subsumption_resolution,[status(thm)],[c_2103,c_660]) ).
tcf(c_3566,plain,
~ xsd_integer(sK81),
inference(resolution,[status(thm)],[c_658,c_2110]) ).
tcf(c_3567,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_3566,c_2108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS154+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 19:32:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 2.94/1.30 % SZS status Started for theBenchmark.p
% 2.94/1.30 % SZS status Theorem for theBenchmark.p
% 2.94/1.30
% 2.94/1.30 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.94/1.30
% 2.94/1.30 % ------ iProver source info
% 2.94/1.30
% 2.94/1.30 % git: date: 2026-07-19 20:42:38 +0200
% 2.94/1.30 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.94/1.30 % git: non_committed_changes: false
% 2.94/1.30
% 2.94/1.30 % ------ Parsing...
% 2.94/1.30 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.94/1.30
% 2.94/1.30 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s%
% 2.94/1.30
% 2.94/1.30 % SZS status Theorem for theBenchmark.p
% 2.94/1.30
% 2.94/1.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.94/1.30
% 2.94/1.30
%------------------------------------------------------------------------------