%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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:21 PM UTC 2026
% Result : Theorem 3.53s 0.91s
% Output : Proof 3.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 28
% Syntax : Number of formulae : 167 ( 55 unt; 0 def)
% Number of atoms : 813 ( 0 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 1143 ( 497 ~; 528 |; 103 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-1 aty)
% Number of variables : 109 ( 2 sgn 64 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f82,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( cC80(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
fof(f82_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC80(Y)
| ~ rR1(X,Y) )
| cC82(X) )
& ( ? [Y] :
( cC80(Y)
& rR1(X,Y) )
| ~ cC82(X) ) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [X,Y] :
( ( ~ cC80(Y)
| ~ rR1(X,Y)
| cC82(X) )
& ( ( cC80(sk67(X))
& rR1(X,sk67(X)) )
| ~ cC82(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk67])],[f82_nnf]) ).
cnf(c205,plain,
( ~ cC80(X1)
| ~ rR1(X0,X1)
| cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
fof(f103,axiom,
rR1(iV8467,iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_103) ).
fof(f103_nnf,plain,
rR1(iV8467,iV8471),
inference(nnf_transformation,[status(thm)],[f103]) ).
cnf(c247,plain,
rR1(iV8467,iV8471),
inference(cnf_transformation,[status(esa)],[f103_nnf]) ).
cnf(p1109,plain,
( ~ cC80(iV8471)
| cC82(iV8467) ),
inference(resolution,[status(thm)],[c205,c247]) ).
fof(f80,axiom,
! [X] :
( cC80(X)
<=> ( cC2xcomp(X)
& cC78xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_80) ).
fof(f80_nnf,plain,
! [X] :
( ( ~ cC2xcomp(X)
| ~ cC78xcomp(X)
| cC80(X) )
& ( ( cC2xcomp(X)
& cC78xcomp(X) )
| ~ cC80(X) ) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [X] :
( ( ~ cC2xcomp(X)
| ~ cC78xcomp(X)
| cC80(X) )
& ( ( cC2xcomp(X)
& cC78xcomp(X) )
| ~ cC80(X) ) ),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c200,plain,
( ~ cC2xcomp(X0)
| ~ cC78xcomp(X0)
| cC80(X0) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
fof(f118,axiom,
cC78xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_118) ).
fof(f118_nnf,plain,
cC78xcomp(iV8471),
inference(nnf_transformation,[status(thm)],[f118]) ).
cnf(c262,plain,
cC78xcomp(iV8471),
inference(cnf_transformation,[status(esa)],[f118_nnf]) ).
cnf(p1085,plain,
( ~ cC2xcomp(iV8471)
| cC80(iV8471) ),
inference(resolution,[status(thm)],[c200,c262]) ).
fof(f119,axiom,
cC2xcomp(iV8471),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_119) ).
fof(f119_nnf,plain,
cC2xcomp(iV8471),
inference(nnf_transformation,[status(thm)],[f119]) ).
cnf(c263,plain,
cC2xcomp(iV8471),
inference(cnf_transformation,[status(esa)],[f119_nnf]) ).
cnf(p1105,plain,
cC80(iV8471),
inference(resolution,[status(thm)],[p1085,c263]) ).
cnf(p1134,plain,
cC82(iV8467),
inference(resolution,[status(thm)],[p1109,p1105]) ).
fof(f79,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
fof(f79_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC6xcomp(Y)
| ~ rR1(X,Y) )
| cC8(X) )
& ( ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) )
| ~ cC8(X) ) ),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [X,Y] :
( ( ~ cC6xcomp(Y)
| ~ rR1(X,Y)
| cC8(X) )
& ( ( cC6xcomp(sk65(X))
& rR1(X,sk65(X)) )
| ~ cC8(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk65])],[f79_nnf]) ).
cnf(c197,plain,
( ~ cC6xcomp(X1)
| ~ rR1(X0,X1)
| cC8(X0) ),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
fof(f105,axiom,
rR1(iV8467,iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_105) ).
fof(f105_nnf,plain,
rR1(iV8467,iV8469),
inference(nnf_transformation,[status(thm)],[f105]) ).
cnf(c249,plain,
rR1(iV8467,iV8469),
inference(cnf_transformation,[status(esa)],[f105_nnf]) ).
cnf(p1056,plain,
( ~ cC6xcomp(iV8469)
| cC8(iV8467) ),
inference(resolution,[status(thm)],[c197,c249]) ).
fof(f113,axiom,
cC6xcomp(iV8469),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
fof(f113_nnf,plain,
cC6xcomp(iV8469),
inference(nnf_transformation,[status(thm)],[f113]) ).
cnf(c257,plain,
cC6xcomp(iV8469),
inference(cnf_transformation,[status(esa)],[f113_nnf]) ).
cnf(p1080,plain,
cC8(iV8467),
inference(resolution,[status(thm)],[p1056,c257]) ).
fof(f35,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_35) ).
fof(f35_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC4(X) ) ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [X,Y] :
( ( ~ cC2xcomp(Y)
| ~ rR1(X,Y)
| cC4(X) )
& ( ( cC2xcomp(sk29(X))
& rR1(X,sk29(X)) )
| ~ cC4(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk29])],[f35_nnf]) ).
cnf(c87,plain,
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC4(X0) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p538,plain,
( ~ cC2xcomp(iV8471)
| cC4(iV8467) ),
inference(resolution,[status(thm)],[c87,c247]) ).
cnf(p583,plain,
cC4(iV8467),
inference(resolution,[status(thm)],[p538,c263]) ).
fof(f13,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
fof(f13_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC20(X) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X,Y] :
( ( ~ cC2xcomp(Y)
| ~ rR1(X,Y)
| cC20(X) )
& ( ( cC2xcomp(sk9(X))
& rR1(X,sk9(X)) )
| ~ cC20(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9])],[f13_nnf]) ).
cnf(c33,plain,
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC20(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p366,plain,
( ~ cC2xcomp(iV8471)
| cC20(iV8467) ),
inference(resolution,[status(thm)],[c33,c247]) ).
cnf(p376,plain,
cC20(iV8467),
inference(resolution,[status(thm)],[p366,c263]) ).
fof(f1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/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/sandbox2/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(f134,conjecture,
( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f134_neg,negated_conjecture,
~ ( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f134]) ).
fof(f134_nnf,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f134_neg]) ).
fof(f134_sk,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ( ~ xsd_integer(sk80)
& ~ xsd_string(sk80) )
| ( xsd_integer(sk80)
& xsd_string(sk80) )
| cowlNothing(sk79)
| ~ cowlThing(sk79) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk79,sk80])],[f134_nnf]) ).
cnf(c279,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sk80)
| xsd_string(sk80)
| cowlNothing(sk79)
| ~ cowlThing(sk79) ),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(p282,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sk80)
| xsd_string(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[c0,c279]) ).
cnf(p284,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_string(sk80)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[c3,p282]) ).
cnf(p285,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(factoring,[status(thm)],[p284]) ).
cnf(p377,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p376,p285]) ).
cnf(p585,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p583,p377]) ).
cnf(p1081,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1080,p585]) ).
cnf(p1137,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1134,p1081]) ).
fof(f62,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( cC60(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_62) ).
fof(f62_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC60(Y)
| ~ rR1(X,Y) )
| cC62(X) )
& ( ? [Y] :
( cC60(Y)
& rR1(X,Y) )
| ~ cC62(X) ) ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [X,Y] :
( ( ~ cC60(Y)
| ~ rR1(X,Y)
| cC62(X) )
& ( ( cC60(sk51(X))
& rR1(X,sk51(X)) )
| ~ cC62(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk51])],[f62_nnf]) ).
cnf(c154,plain,
( ~ cC60(X1)
| ~ rR1(X0,X1)
| cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
fof(f110,axiom,
rR1(iV8467,iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_110) ).
fof(f110_nnf,plain,
rR1(iV8467,iV8472),
inference(nnf_transformation,[status(thm)],[f110]) ).
cnf(c254,plain,
rR1(iV8467,iV8472),
inference(cnf_transformation,[status(esa)],[f110_nnf]) ).
cnf(p815,plain,
( ~ cC60(iV8472)
| cC62(iV8467) ),
inference(resolution,[status(thm)],[c154,c254]) ).
fof(f61,axiom,
! [X] :
( cC60(X)
<=> ( cC58(X)
& cC2xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
fof(f61_nnf,plain,
! [X] :
( ( ~ cC58(X)
| ~ cC2xcomp(X)
| cC60(X) )
& ( ( cC58(X)
& cC2xcomp(X) )
| ~ cC60(X) ) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [X] :
( ( ~ cC58(X)
| ~ cC2xcomp(X)
| cC60(X) )
& ( ( cC58(X)
& cC2xcomp(X) )
| ~ cC60(X) ) ),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c151,plain,
( ~ cC58(X0)
| ~ cC2xcomp(X0)
| cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
fof(f122,axiom,
cC2xcomp(iV8472),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_122) ).
fof(f122_nnf,plain,
cC2xcomp(iV8472),
inference(nnf_transformation,[status(thm)],[f122]) ).
cnf(c266,plain,
cC2xcomp(iV8472),
inference(cnf_transformation,[status(esa)],[f122_nnf]) ).
cnf(p797,plain,
( ~ cC58(iV8472)
| cC60(iV8472) ),
inference(resolution,[status(thm)],[c151,c266]) ).
fof(f57,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
fof(f57_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC2(Y)
| ~ rR1(X,Y) )
| cC58(X) )
& ( ? [Y] :
( cC2(Y)
& rR1(X,Y) )
| ~ cC58(X) ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X,Y] :
( ( ~ cC2(Y)
| ~ rR1(X,Y)
| cC58(X) )
& ( ( cC2(sk47(X))
& rR1(X,sk47(X)) )
| ~ cC58(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk47])],[f57_nnf]) ).
cnf(c141,plain,
( ~ cC2(X1)
| ~ rR1(X0,X1)
| cC58(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f124,axiom,
rR1(iV8472,iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_124) ).
fof(f124_nnf,plain,
rR1(iV8472,iV8476),
inference(nnf_transformation,[status(thm)],[f124]) ).
cnf(c268,plain,
rR1(iV8472,iV8476),
inference(cnf_transformation,[status(esa)],[f124_nnf]) ).
cnf(p728,plain,
( ~ cC2(iV8476)
| cC58(iV8472) ),
inference(resolution,[status(thm)],[c141,c268]) ).
fof(f132,axiom,
cC2(iV8476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_132) ).
fof(f132_nnf,plain,
cC2(iV8476),
inference(nnf_transformation,[status(thm)],[f132]) ).
cnf(c276,plain,
cC2(iV8476),
inference(cnf_transformation,[status(esa)],[f132_nnf]) ).
cnf(p739,plain,
cC58(iV8472),
inference(resolution,[status(thm)],[p728,c276]) ).
cnf(p806,plain,
cC60(iV8472),
inference(resolution,[status(thm)],[p797,p739]) ).
cnf(p828,plain,
cC62(iV8467),
inference(resolution,[status(thm)],[p815,p806]) ).
cnf(p1139,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1137,p828]) ).
fof(f5,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cTOP(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
fof(f5_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cTOP(Y)
| ~ rR1(X,Y) )
| cC14(X) )
& ( ? [Y] :
( cTOP(Y)
& rR1(X,Y) )
| ~ cC14(X) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( ( ~ cTOP(Y)
| ~ rR1(X,Y)
| cC14(X) )
& ( ( cTOP(sk2(X))
& rR1(X,sk2(X)) )
| ~ cC14(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f5_nnf]) ).
cnf(c14,plain,
( ~ cTOP(X1)
| ~ rR1(X0,X1)
| cC14(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
fof(f104,axiom,
rR1(iV8467,iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_104) ).
fof(f104_nnf,plain,
rR1(iV8467,iV8470),
inference(nnf_transformation,[status(thm)],[f104]) ).
cnf(c248,plain,
rR1(iV8467,iV8470),
inference(cnf_transformation,[status(esa)],[f104_nnf]) ).
cnf(p296,plain,
( ~ cTOP(iV8470)
| cC14(iV8467) ),
inference(resolution,[status(thm)],[c14,c248]) ).
fof(f116,axiom,
cTOP(iV8470),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_116) ).
fof(f116_nnf,plain,
cTOP(iV8470),
inference(nnf_transformation,[status(thm)],[f116]) ).
cnf(c260,plain,
cTOP(iV8470),
inference(cnf_transformation,[status(esa)],[f116_nnf]) ).
cnf(p305,plain,
cC14(iV8467),
inference(resolution,[status(thm)],[p296,c260]) ).
cnf(p1140,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1139,p305]) ).
fof(f29,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
fof(f29_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC32xcomp(Y)
| ~ rR1(X,Y) )
| cC34(X) )
& ( ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) )
| ~ cC34(X) ) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,Y] :
( ( ~ cC32xcomp(Y)
| ~ rR1(X,Y)
| cC34(X) )
& ( ( cC32xcomp(sk23(X))
& rR1(X,sk23(X)) )
| ~ cC34(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk23])],[f29_nnf]) ).
cnf(c72,plain,
( ~ cC32xcomp(X1)
| ~ rR1(X0,X1)
| cC34(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f106,axiom,
rR1(iV8467,iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_106) ).
fof(f106_nnf,plain,
rR1(iV8467,iV8474),
inference(nnf_transformation,[status(thm)],[f106]) ).
cnf(c250,plain,
rR1(iV8467,iV8474),
inference(cnf_transformation,[status(esa)],[f106_nnf]) ).
cnf(p460,plain,
( ~ cC32xcomp(iV8474)
| cC34(iV8467) ),
inference(resolution,[status(thm)],[c72,c250]) ).
fof(f127,axiom,
cC32xcomp(iV8474),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_127) ).
fof(f127_nnf,plain,
cC32xcomp(iV8474),
inference(nnf_transformation,[status(thm)],[f127]) ).
cnf(c271,plain,
cC32xcomp(iV8474),
inference(cnf_transformation,[status(esa)],[f127_nnf]) ).
cnf(p473,plain,
cC34(iV8467),
inference(resolution,[status(thm)],[p460,c271]) ).
cnf(p1142,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1140,p473]) ).
fof(f2,axiom,
! [X] :
( cC10(X)
<=> ( cC8(X)
& cC4(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f2_nnf,plain,
! [X] :
( ( ~ cC8(X)
| ~ cC4(X)
| cC10(X) )
& ( ( cC8(X)
& cC4(X) )
| ~ cC10(X) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] :
( ( ~ cC8(X)
| ~ cC4(X)
| cC10(X) )
& ( ( cC8(X)
& cC4(X) )
| ~ cC10(X) ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c6,plain,
( ~ cC8(X0)
| ~ cC4(X0)
| cC10(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p584,plain,
( ~ cC8(iV8467)
| cC10(iV8467) ),
inference(resolution,[status(thm)],[p583,c6]) ).
cnf(p1082,plain,
cC10(iV8467),
inference(resolution,[status(thm)],[p1080,p584]) ).
cnf(p1143,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1142,p1082]) ).
cnf(p1144,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1143,c0]) ).
fof(f44,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_44) ).
fof(f44_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC48(X) )
& ( ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) )
| ~ cC48(X) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [X,Y] :
( ( ~ cC2xcomp(Y)
| ~ rR1(X,Y)
| cC48(X) )
& ( ( cC2xcomp(sk36(X))
& rR1(X,sk36(X)) )
| ~ cC48(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk36])],[f44_nnf]) ).
cnf(c110,plain,
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC48(X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p625,plain,
( ~ cC2xcomp(iV8471)
| cC48(iV8467) ),
inference(resolution,[status(thm)],[c110,c247]) ).
cnf(p641,plain,
cC48(iV8467),
inference(resolution,[status(thm)],[p625,c263]) ).
cnf(p1145,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1144,p641]) ).
cnf(p1146,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1145,c0]) ).
cnf(p1147,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1146,p1105]) ).
cnf(p1148,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1147,p739]) ).
cnf(p1149,plain,
( ~ cowlThing(iV8472)
| cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1148,p806]) ).
cnf(p1175,plain,
( cowlNothing(sk79)
| xsd_string(sk80) ),
inference(resolution,[status(thm)],[p1149,c0]) ).
cnf(c280,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_string(sk80)
| xsd_integer(sk80)
| cowlNothing(sk79)
| ~ cowlThing(sk79) ),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
cnf(p283,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_string(sk80)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[c0,c280]) ).
cnf(p1176,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1175,p283]) ).
cnf(p1178,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(factoring,[status(thm)],[p1176]) ).
cnf(p1179,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1178,p376]) ).
cnf(p1180,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1179,p583]) ).
cnf(p1181,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1180,p1080]) ).
cnf(p1182,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1181,p1134]) ).
cnf(p1184,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1182,p828]) ).
cnf(p1185,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1184,p305]) ).
cnf(p1186,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1185,p473]) ).
cnf(p1187,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1186,p1082]) ).
cnf(p1188,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1187,c0]) ).
cnf(p1189,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1188,p641]) ).
cnf(p1190,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1189,c0]) ).
cnf(p1191,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1190,p1105]) ).
cnf(p1192,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1191,p739]) ).
cnf(p1193,plain,
( ~ cowlThing(iV8472)
| xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1192,p806]) ).
cnf(p1194,plain,
( xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1193,c0]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1177,plain,
( ~ xsd_integer(sk80)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1175,c2]) ).
cnf(p1195,plain,
( cowlNothing(sk79)
| cowlNothing(sk79) ),
inference(resolution,[status(thm)],[p1194,p1177]) ).
cnf(p1221,plain,
cowlNothing(sk79),
inference(factoring,[status(thm)],[p1195]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1222,plain,
$false,
inference(resolution,[status(thm)],[p1221,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n002.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Wed Sep 23 19:35:04 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.53/0.91 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.53/0.91 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------