%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS153+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 : n026.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 14.29s 2.38s
% Output : Proof 14.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 146
% Number of leaves : 53
% Syntax : Number of formulae : 390 ( 134 unt; 0 def)
% Number of atoms : 4847 ( 0 equ)
% Maximal formula atoms : 51 ( 12 avg)
% Number of connectives : 7487 (3030 ~;4236 |; 198 &)
% ( 22 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 50 ( 13 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 15 con; 0-1 aty)
% Number of variables : 127 ( 2 sgn 80 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f39,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_39) ).
fof(f39_nnf,plain,
! [X] :
( ( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X,Y] :
( ( cC12(Y)
| ~ rR1(X,Y)
| cC60(X) )
& ( ( ~ cC12(sk18(X))
& rR1(X,sk18(X)) )
| ~ cC60(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk18])],[f39_nnf]) ).
cnf(c117,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
fof(f96,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(f96_nnf,plain,
rR1(iV16453,iV16461),
inference(nnf_transformation,[status(thm)],[f96]) ).
cnf(c214,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[status(esa)],[f96_nnf]) ).
cnf(p727,plain,
( cC12(iV16461)
| cC60(iV16453) ),
inference(resolution,[status(thm)],[c117,c214]) ).
fof(f40,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC58(X)
& cC60(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(f40_nnf,plain,
! [X] :
( ( cC58(X)
| ~ cC60(X)
| cC62(X) )
& ( ( ~ cC58(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X] :
( ( cC58(X)
| ~ cC60(X)
| cC62(X) )
& ( ( ~ cC58(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c120,plain,
( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p944,plain,
( cC58(iV16453)
| cC62(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p727,c120]) ).
fof(f47,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& ~ cC74(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_47) ).
fof(f47_nnf,plain,
! [X] :
( ( ~ cC62(X)
| cC74(X)
| cC76(X) )
& ( ( cC62(X)
& ~ cC74(X) )
| ~ cC76(X) ) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X] :
( ( ~ cC62(X)
| cC74(X)
| cC76(X) )
& ( ( cC62(X)
& ~ cC74(X) )
| ~ cC76(X) ) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c141,plain,
( ~ cC62(X0)
| cC74(X0)
| cC76(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p4250,plain,
( cC74(iV16453)
| cC76(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p944,c141]) ).
fof(f60,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_60) ).
fof(f60_nnf,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c178,plain,
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
fof(f64,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(f64_nnf,plain,
rR1(iV16439,iV16440),
inference(nnf_transformation,[status(thm)],[f64]) ).
cnf(c182,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[status(esa)],[f64_nnf]) ).
cnf(p1205,plain,
cC98(iV16440),
inference(resolution,[status(thm)],[c178,c182]) ).
fof(f58,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& ~ cC96(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_58) ).
fof(f58_nnf,plain,
! [X] :
( ( ~ cC82(X)
| cC96(X)
| cC98(X) )
& ( ( cC82(X)
& ~ cC96(X) )
| ~ cC98(X) ) ),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [X] :
( ( ~ cC82(X)
| cC96(X)
| cC98(X) )
& ( ( cC82(X)
& ~ cC96(X) )
| ~ cC98(X) ) ),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c173,plain,
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(p1211,plain,
cC82(iV16440),
inference(resolution,[status(thm)],[p1205,c173]) ).
fof(f50,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& ~ cC78(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_50) ).
fof(f50_nnf,plain,
! [X] :
( ( ~ cC80(X)
| cC78(X)
| cC82(X) )
& ( ( cC80(X)
& ~ cC78(X) )
| ~ cC82(X) ) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [X] :
( ( ~ cC80(X)
| cC78(X)
| cC82(X) )
& ( ( cC80(X)
& ~ cC78(X) )
| ~ cC82(X) ) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c149,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(p1216,plain,
cC80(iV16440),
inference(resolution,[status(thm)],[p1211,c149]) ).
fof(f59,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_59) ).
fof(f59_nnf,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c176,plain,
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f61,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
fof(f61_nnf,plain,
cTEST(iV16439),
inference(nnf_transformation,[status(thm)],[f61]) ).
cnf(c179,plain,
cTEST(iV16439),
inference(cnf_transformation,[status(esa)],[f61_nnf]) ).
cnf(p399,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[c176,c179]) ).
cnf(c175,plain,
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(p376,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[c175,c179]) ).
fof(f6,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
fof(f6_nnf,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c17,plain,
( cC106(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p378,plain,
cC106(iV16439),
inference(resolution,[status(thm)],[p376,c17]) ).
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(f200,conjecture,
( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f200_neg,negated_conjecture,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f200]) ).
fof(f200_nnf,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f200_neg]) ).
fof(f200_sk,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ( ~ xsd_integer(sk29)
& ~ xsd_string(sk29) )
| ( xsd_integer(sk29)
& xsd_string(sk29) )
| cowlNothing(sk28)
| ~ cowlThing(sk28) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk28,sk29])],[f200_nnf]) ).
cnf(c319,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sk29)
| xsd_string(sk29)
| cowlNothing(sk28)
| ~ cowlThing(sk28) ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
cnf(p322,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sk29)
| xsd_string(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[c0,c319]) ).
cnf(p324,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_string(sk29)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[c3,p322]) ).
cnf(p325,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(factoring,[status(thm)],[p324]) ).
cnf(p379,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p378,p325]) ).
cnf(c16,plain,
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p377,plain,
cC28(iV16439),
inference(resolution,[status(thm)],[p376,c16]) ).
cnf(p381,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p379,p377]) ).
cnf(p400,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p399,p381]) ).
cnf(p402,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p400,c0]) ).
cnf(p403,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p402,p376]) ).
fof(f5,axiom,
! [X] :
( cC106(X)
<=> ( cC104(X)
& ~ cC100(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
fof(f5_nnf,plain,
! [X] :
( ( ~ cC104(X)
| cC100(X)
| cC106(X) )
& ( ( cC104(X)
& ~ cC100(X) )
| ~ cC106(X) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] :
( ( ~ cC104(X)
| cC100(X)
| cC106(X) )
& ( ( cC104(X)
& ~ cC100(X) )
| ~ cC106(X) ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c14,plain,
( cC104(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p380,plain,
cC104(iV16439),
inference(resolution,[status(thm)],[p378,c14]) ).
cnf(p404,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p403,p380]) ).
cnf(p1225,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1216,p404]) ).
cnf(p1228,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1225,c0]) ).
cnf(p1229,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1228,p1211]) ).
cnf(p1230,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1229,p1205]) ).
cnf(p1231,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1230,c0]) ).
fof(f27,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& ~ cC36(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(f27_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& ~ cC36(X) )
| ~ cC38(X) ) ),
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c81,plain,
( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ),
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
fof(f79,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
fof(f79_nnf,plain,
cTOP(iV16448),
inference(nnf_transformation,[status(thm)],[f79]) ).
cnf(c197,plain,
cTOP(iV16448),
inference(cnf_transformation,[status(esa)],[f79_nnf]) ).
cnf(p588,plain,
( cC36(iV16448)
| cC38(iV16448) ),
inference(resolution,[status(thm)],[c81,c197]) ).
cnf(p1232,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p1231,p588]) ).
cnf(p4251,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p944,p1232]) ).
cnf(p4252,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p4251,c0]) ).
cnf(p13580,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p4250,p4252]) ).
cnf(p13582,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13580]) ).
cnf(p13584,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13582]) ).
cnf(p13585,plain,
( cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13584,p727]) ).
cnf(p13587,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13585]) ).
fof(f29,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
fof(f29_nnf,plain,
! [X] :
( ( ! [Y] :
( cC8(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ( ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,Y] :
( ( cC8(Y)
| ~ rR1(X,Y)
| cC42(X) )
& ( ( ~ cC8(sk14(X))
& rR1(X,sk14(X)) )
| ~ cC42(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f29_nnf]) ).
cnf(c87,plain,
( cC8(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
fof(f107,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_107) ).
fof(f107_nnf,plain,
rR1(iV16455,iV16460),
inference(nnf_transformation,[status(thm)],[f107]) ).
cnf(c225,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[status(esa)],[f107_nnf]) ).
cnf(p628,plain,
( cC8(iV16460)
| cC42(iV16455) ),
inference(resolution,[status(thm)],[c87,c225]) ).
fof(f30,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& ~ cC40(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f30_nnf,plain,
! [X] :
( ( ~ cC42(X)
| cC40(X)
| cC44(X) )
& ( ( cC42(X)
& ~ cC40(X) )
| ~ cC44(X) ) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X] :
( ( ~ cC42(X)
| cC40(X)
| cC44(X) )
& ( ( cC42(X)
& ~ cC40(X) )
| ~ cC44(X) ) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c90,plain,
( ~ cC42(X0)
| cC40(X0)
| cC44(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p769,plain,
( cC40(iV16455)
| cC44(iV16455)
| cC8(iV16460) ),
inference(resolution,[status(thm)],[p628,c90]) ).
cnf(p13589,plain,
( cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13587,p769]) ).
cnf(p13590,plain,
( cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13589,c0]) ).
fof(f36,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& cC44(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_36) ).
fof(f36_nnf,plain,
! [X] :
( ( cC54(X)
| ~ cC44(X)
| cC56(X) )
& ( ( ~ cC54(X)
& cC44(X) )
| ~ cC56(X) ) ),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [X] :
( ( cC54(X)
| ~ cC44(X)
| cC56(X) )
& ( ( ~ cC54(X)
& cC44(X) )
| ~ cC56(X) ) ),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c108,plain,
( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p3265,plain,
( cC54(iV16455)
| cC56(iV16455)
| cC40(iV16455)
| cC8(iV16460) ),
inference(resolution,[status(thm)],[p769,c108]) ).
cnf(p13591,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13590,p3265]) ).
cnf(p13592,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13591]) ).
cnf(p13594,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13592]) ).
cnf(p13595,plain,
( cC8(iV16460)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13594,p628]) ).
cnf(p13596,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(factoring,[status(thm)],[p13595]) ).
cnf(p13597,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13596,c0]) ).
fof(f113,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
fof(f113_nnf,plain,
cTOP(iV16457),
inference(nnf_transformation,[status(thm)],[f113]) ).
cnf(c231,plain,
cTOP(iV16457),
inference(cnf_transformation,[status(esa)],[f113_nnf]) ).
cnf(p589,plain,
( cC36(iV16457)
| cC38(iV16457) ),
inference(resolution,[status(thm)],[c81,c231]) ).
cnf(p13600,plain,
( cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13597,p589]) ).
fof(f43,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC66(X)
& ~ cC64(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(f43_nnf,plain,
! [X] :
( ( cC66(X)
| cC64(X)
| cC68(X) )
& ( ( ~ cC66(X)
& ~ cC64(X) )
| ~ cC68(X) ) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [X] :
( ( cC66(X)
| cC64(X)
| cC68(X) )
& ( ( ~ cC66(X)
& ~ cC64(X) )
| ~ cC68(X) ) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c129,plain,
( cC66(X0)
| cC64(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p13601,plain,
( cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13600,c129]) ).
cnf(p13602,plain,
( cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13601,c0]) ).
fof(f53,axiom,
! [X] :
( cC88(X)
<=> ( ~ cC86(X)
& ~ cC84(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_53) ).
fof(f53_nnf,plain,
! [X] :
( ( cC86(X)
| cC84(X)
| cC88(X) )
& ( ( ~ cC86(X)
& ~ cC84(X) )
| ~ cC88(X) ) ),
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
! [X] :
( ( cC86(X)
| cC84(X)
| cC88(X) )
& ( ( ~ cC86(X)
& ~ cC84(X) )
| ~ cC88(X) ) ),
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c159,plain,
( cC86(X0)
| cC84(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(p13603,plain,
( cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13602,c159]) ).
fof(f33,axiom,
! [X] :
( cC50(X)
<=> ( ~ cC48(X)
& ~ cC46(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
fof(f33_nnf,plain,
! [X] :
( ( cC48(X)
| cC46(X)
| cC50(X) )
& ( ( ~ cC48(X)
& ~ cC46(X) )
| ~ cC50(X) ) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [X] :
( ( cC48(X)
| cC46(X)
| cC50(X) )
& ( ( ~ cC48(X)
& ~ cC46(X) )
| ~ cC50(X) ) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c99,plain,
( cC48(X0)
| cC46(X0)
| cC50(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p13604,plain,
( cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13603,c99]) ).
fof(f25,axiom,
! [X] :
( cC34(X)
<=> ( ~ cC30(X)
& ~ cC32(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_25) ).
fof(f25_nnf,plain,
! [X] :
( ( cC30(X)
| cC32(X)
| cC34(X) )
& ( ( ~ cC30(X)
& ~ cC32(X) )
| ~ cC34(X) ) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X] :
( ( cC30(X)
| cC32(X)
| cC34(X) )
& ( ( ~ cC30(X)
& ~ cC32(X) )
| ~ cC34(X) ) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c75,plain,
( cC30(X0)
| cC32(X0)
| cC34(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p13605,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13604,c75]) ).
cnf(p13606,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13605,c0]) ).
fof(f28,axiom,
! [X] :
( cC40(X)
<=> ? [Y] :
( ~ cC38(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_28) ).
fof(f28_nnf,plain,
! [X] :
( ( ! [Y] :
( cC38(Y)
| ~ rR1(X,Y) )
| cC40(X) )
& ( ? [Y] :
( ~ cC38(Y)
& rR1(X,Y) )
| ~ cC40(X) ) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y] :
( ( cC38(Y)
| ~ rR1(X,Y)
| cC40(X) )
& ( ( ~ cC38(sk13(X))
& rR1(X,sk13(X)) )
| ~ cC40(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f28_nnf]) ).
cnf(c84,plain,
( cC38(X1)
| ~ rR1(X0,X1)
| cC40(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(p610,plain,
( cC38(iV16460)
| cC40(iV16455) ),
inference(resolution,[status(thm)],[c84,c225]) ).
fof(f98,axiom,
~ cC40(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_98) ).
fof(f98_nnf,plain,
~ cC40(iV16455),
inference(nnf_transformation,[status(thm)],[f98]) ).
fof(f98_sk,plain,
~ cC40(iV16455),
inference(skolemisation,[status(esa)],[f98_nnf]) ).
cnf(c216,plain,
~ cC40(iV16455),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(p741,plain,
cC38(iV16460),
inference(resolution,[status(thm)],[p610,c216]) ).
cnf(p13607,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13606,p741]) ).
fof(f37,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( ~ cC56(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_37) ).
fof(f37_nnf,plain,
! [X] :
( ( ! [Y] :
( cC56(Y)
| ~ rR1(X,Y) )
| cC58(X) )
& ( ? [Y] :
( ~ cC56(Y)
& rR1(X,Y) )
| ~ cC58(X) ) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X,Y] :
( ( cC56(Y)
| ~ rR1(X,Y)
| cC58(X) )
& ( ( ~ cC56(sk17(X))
& rR1(X,sk17(X)) )
| ~ cC58(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk17])],[f37_nnf]) ).
cnf(c111,plain,
( cC56(X1)
| ~ rR1(X0,X1)
| cC58(X0) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(p690,plain,
( cC56(iV16461)
| cC58(iV16453) ),
inference(resolution,[status(thm)],[c111,c214]) ).
fof(f91,axiom,
~ cC58(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_91) ).
fof(f91_nnf,plain,
~ cC58(iV16453),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
~ cC58(iV16453),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c209,plain,
~ cC58(iV16453),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(p838,plain,
cC56(iV16461),
inference(resolution,[status(thm)],[p690,c209]) ).
cnf(c106,plain,
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p839,plain,
cC44(iV16461),
inference(resolution,[status(thm)],[p838,c106]) ).
cnf(p13608,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13607,p839]) ).
cnf(p13609,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13608,c0]) ).
cnf(p13610,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13609,p838]) ).
cnf(c89,plain,
( cC42(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p840,plain,
cC42(iV16461),
inference(resolution,[status(thm)],[p839,c89]) ).
cnf(p13611,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13610,p840]) ).
cnf(p13612,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13611,c0]) ).
fof(f157,axiom,
rR1(iV16461,iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_157) ).
fof(f157_nnf,plain,
rR1(iV16461,iV16462),
inference(nnf_transformation,[status(thm)],[f157]) ).
cnf(c275,plain,
rR1(iV16461,iV16462),
inference(cnf_transformation,[status(esa)],[f157_nnf]) ).
cnf(p611,plain,
( cC38(iV16462)
| cC40(iV16461) ),
inference(resolution,[status(thm)],[c84,c275]) ).
fof(f147,axiom,
~ cC40(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_147) ).
fof(f147_nnf,plain,
~ cC40(iV16461),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
~ cC40(iV16461),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c265,plain,
~ cC40(iV16461),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(p742,plain,
cC38(iV16462),
inference(resolution,[status(thm)],[p611,c265]) ).
cnf(p13613,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13612,p742]) ).
fof(f48,axiom,
! [X] :
( cC78(X)
<=> ? [Y] :
( ~ cC76(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_48) ).
fof(f48_nnf,plain,
! [X] :
( ( ! [Y] :
( cC76(Y)
| ~ rR1(X,Y) )
| cC78(X) )
& ( ? [Y] :
( ~ cC76(Y)
& rR1(X,Y) )
| ~ cC78(X) ) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [X,Y] :
( ( cC76(Y)
| ~ rR1(X,Y)
| cC78(X) )
& ( ( ~ cC76(sk22(X))
& rR1(X,sk22(X)) )
| ~ cC78(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk22])],[f48_nnf]) ).
cnf(c144,plain,
( cC76(X1)
| ~ rR1(X0,X1)
| cC78(X0) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
fof(f73,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f73_nnf,plain,
rR1(iV16440,iV16463),
inference(nnf_transformation,[status(thm)],[f73]) ).
cnf(c191,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[status(esa)],[f73_nnf]) ).
cnf(p927,plain,
( cC76(iV16463)
| cC78(iV16440) ),
inference(resolution,[status(thm)],[c144,c191]) ).
fof(f70,axiom,
~ cC78(iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_70) ).
fof(f70_nnf,plain,
~ cC78(iV16440),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
~ cC78(iV16440),
inference(skolemisation,[status(esa)],[f70_nnf]) ).
cnf(c188,plain,
~ cC78(iV16440),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
cnf(p1054,plain,
cC76(iV16463),
inference(resolution,[status(thm)],[p927,c188]) ).
cnf(c140,plain,
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p1055,plain,
cC62(iV16463),
inference(resolution,[status(thm)],[p1054,c140]) ).
cnf(p13614,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13613,p1055]) ).
cnf(p13615,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13614,c0]) ).
cnf(p13616,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13615,p1054]) ).
cnf(c118,plain,
( cC60(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p1056,plain,
cC60(iV16463),
inference(resolution,[status(thm)],[p1055,c118]) ).
cnf(p13617,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13616,p1056]) ).
fof(f177,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_177) ).
fof(f177_nnf,plain,
rR1(iV16463,iV16464),
inference(nnf_transformation,[status(thm)],[f177]) ).
cnf(c295,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[status(esa)],[f177_nnf]) ).
cnf(p693,plain,
( cC56(iV16464)
| cC58(iV16463) ),
inference(resolution,[status(thm)],[c111,c295]) ).
fof(f174,axiom,
~ cC58(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(f174_nnf,plain,
~ cC58(iV16463),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
~ cC58(iV16463),
inference(skolemisation,[status(esa)],[f174_nnf]) ).
cnf(c292,plain,
~ cC58(iV16463),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
cnf(p879,plain,
cC56(iV16464),
inference(resolution,[status(thm)],[p693,c292]) ).
cnf(p880,plain,
cC44(iV16464),
inference(resolution,[status(thm)],[p879,c106]) ).
cnf(p13618,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13617,p880]) ).
cnf(p13619,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13618,c0]) ).
cnf(p13622,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13619,p879]) ).
cnf(p881,plain,
cC42(iV16464),
inference(resolution,[status(thm)],[p880,c89]) ).
cnf(p13623,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13622,p881]) ).
cnf(p13624,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| ~ cC38(iV16465)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13623,c0]) ).
fof(f188,axiom,
rR1(iV16464,iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_188) ).
fof(f188_nnf,plain,
rR1(iV16464,iV16465),
inference(nnf_transformation,[status(thm)],[f188]) ).
cnf(c306,plain,
rR1(iV16464,iV16465),
inference(cnf_transformation,[status(esa)],[f188_nnf]) ).
cnf(p613,plain,
( cC38(iV16465)
| cC40(iV16464) ),
inference(resolution,[status(thm)],[c84,c306]) ).
fof(f179,axiom,
~ cC40(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_179) ).
fof(f179_nnf,plain,
~ cC40(iV16464),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
~ cC40(iV16464),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c297,plain,
~ cC40(iV16464),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(p745,plain,
cC38(iV16465),
inference(resolution,[status(thm)],[p613,c297]) ).
cnf(p13625,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13624,p745]) ).
fof(f123,axiom,
~ cC86(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(f123_nnf,plain,
~ cC86(iV16459),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
~ cC86(iV16459),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c241,plain,
~ cC86(iV16459),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(p13626,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13625,c241]) ).
fof(f132,axiom,
~ cC84(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_132) ).
fof(f132_nnf,plain,
~ cC84(iV16459),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
~ cC84(iV16459),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c250,plain,
~ cC84(iV16459),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(p13627,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13626,c250]) ).
fof(f92,axiom,
~ cC74(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_92) ).
fof(f92_nnf,plain,
~ cC74(iV16453),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
~ cC74(iV16453),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c210,plain,
~ cC74(iV16453),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(p13628,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13627,c210]) ).
fof(f127,axiom,
~ cC66(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_127) ).
fof(f127_nnf,plain,
~ cC66(iV16459),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
~ cC66(iV16459),
inference(skolemisation,[status(esa)],[f127_nnf]) ).
cnf(c245,plain,
~ cC66(iV16459),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(p13629,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13628,c245]) ).
fof(f133,axiom,
~ cC64(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_133) ).
fof(f133_nnf,plain,
~ cC64(iV16459),
inference(nnf_transformation,[status(thm)],[f133]) ).
fof(f133_sk,plain,
~ cC64(iV16459),
inference(skolemisation,[status(esa)],[f133_nnf]) ).
cnf(c251,plain,
~ cC64(iV16459),
inference(cnf_transformation,[status(esa)],[f133_sk]) ).
cnf(p13630,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC58(iV16453)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13629,c251]) ).
cnf(p13631,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13630,c209]) ).
fof(f103,axiom,
~ cC54(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_103) ).
fof(f103_nnf,plain,
~ cC54(iV16455),
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
~ cC54(iV16455),
inference(skolemisation,[status(esa)],[f103_nnf]) ).
cnf(c221,plain,
~ cC54(iV16455),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(p13632,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13631,c221]) ).
fof(f120,axiom,
~ cC48(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f120_nnf,plain,
~ cC48(iV16459),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
~ cC48(iV16459),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c238,plain,
~ cC48(iV16459),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(p13633,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13632,c238]) ).
fof(f124,axiom,
~ cC46(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_124) ).
fof(f124_nnf,plain,
~ cC46(iV16459),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
~ cC46(iV16459),
inference(skolemisation,[status(esa)],[f124_nnf]) ).
cnf(c242,plain,
~ cC46(iV16459),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
cnf(p13634,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13633,c242]) ).
cnf(p13635,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC36(iV16457)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13634,c216]) ).
fof(f108,axiom,
~ cC36(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_108) ).
fof(f108_nnf,plain,
~ cC36(iV16457),
inference(nnf_transformation,[status(thm)],[f108]) ).
fof(f108_sk,plain,
~ cC36(iV16457),
inference(skolemisation,[status(esa)],[f108_nnf]) ).
cnf(c226,plain,
~ cC36(iV16457),
inference(cnf_transformation,[status(esa)],[f108_sk]) ).
cnf(p13636,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC8(iV16460)
| cC36(iV16448)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13635,c226]) ).
fof(f76,axiom,
~ cC36(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_76) ).
fof(f76_nnf,plain,
~ cC36(iV16448),
inference(nnf_transformation,[status(thm)],[f76]) ).
fof(f76_sk,plain,
~ cC36(iV16448),
inference(skolemisation,[status(esa)],[f76_nnf]) ).
cnf(c194,plain,
~ cC36(iV16448),
inference(cnf_transformation,[status(esa)],[f76_sk]) ).
cnf(p13637,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC8(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13636,c194]) ).
fof(f135,axiom,
~ cC32(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_135) ).
fof(f135_nnf,plain,
~ cC32(iV16459),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
~ cC32(iV16459),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c253,plain,
~ cC32(iV16459),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(p13638,plain,
( cC30(iV16459)
| cC8(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13637,c253]) ).
fof(f121,axiom,
~ cC30(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
fof(f121_nnf,plain,
~ cC30(iV16459),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
~ cC30(iV16459),
inference(skolemisation,[status(esa)],[f121_nnf]) ).
cnf(c239,plain,
~ cC30(iV16459),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
cnf(p13639,plain,
( cC8(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29)
| cC12(iV16461) ),
inference(resolution,[status(thm)],[p13638,c239]) ).
fof(f151,axiom,
~ cC12(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_151) ).
fof(f151_nnf,plain,
~ cC12(iV16461),
inference(nnf_transformation,[status(thm)],[f151]) ).
fof(f151_sk,plain,
~ cC12(iV16461),
inference(skolemisation,[status(esa)],[f151_nnf]) ).
cnf(c269,plain,
~ cC12(iV16461),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
cnf(p13640,plain,
( cC8(iV16460)
| cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p13639,c269]) ).
fof(f141,axiom,
~ cC8(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_141) ).
fof(f141_nnf,plain,
~ cC8(iV16460),
inference(nnf_transformation,[status(thm)],[f141]) ).
fof(f141_sk,plain,
~ cC8(iV16460),
inference(skolemisation,[status(esa)],[f141_nnf]) ).
cnf(c259,plain,
~ cC8(iV16460),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
cnf(p13642,plain,
( cowlNothing(sk28)
| xsd_string(sk29) ),
inference(resolution,[status(thm)],[p13640,c259]) ).
cnf(c320,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_string(sk29)
| xsd_integer(sk29)
| cowlNothing(sk28)
| ~ cowlThing(sk28) ),
inference(cnf_transformation,[status(esa)],[f200_sk]) ).
cnf(p323,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_string(sk29)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[c0,c320]) ).
cnf(p13645,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13642,p323]) ).
cnf(p13647,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13645]) ).
cnf(p13648,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13647,p378]) ).
cnf(p13651,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13648,p377]) ).
cnf(p13652,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13651,p399]) ).
cnf(p13653,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13652,c0]) ).
cnf(p13654,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13653,p376]) ).
cnf(p13657,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13654,p380]) ).
cnf(p13658,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13657,p1216]) ).
cnf(p13659,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13658,c0]) ).
cnf(p13660,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13659,p1211]) ).
cnf(p13663,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13660,p1205]) ).
cnf(p13664,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13663,c0]) ).
cnf(p13665,plain,
( cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13664,p588]) ).
cnf(p13666,plain,
( cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13665,p944]) ).
cnf(p13670,plain,
( cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13666,c0]) ).
cnf(p13671,plain,
( cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13670,p4250]) ).
cnf(p13674,plain,
( cC74(iV16453)
| cC58(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13671]) ).
cnf(p13676,plain,
( cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13674]) ).
cnf(p13677,plain,
( cC12(iV16461)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13676,p727]) ).
cnf(p13679,plain,
( cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13677]) ).
cnf(p13682,plain,
( cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13679,p769]) ).
cnf(p13683,plain,
( cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13682,c0]) ).
cnf(p13684,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13683,p3265]) ).
cnf(p13685,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13684]) ).
cnf(p13687,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13685]) ).
cnf(p13688,plain,
( cC8(iV16460)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13687,p628]) ).
cnf(p13689,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(factoring,[status(thm)],[p13688]) ).
cnf(p13690,plain,
( cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13689,c0]) ).
cnf(p13693,plain,
( cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13690,p589]) ).
cnf(p13694,plain,
( cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13693,c129]) ).
cnf(p13695,plain,
( cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13694,c0]) ).
cnf(p13696,plain,
( cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13695,c159]) ).
cnf(p13697,plain,
( cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13696,c99]) ).
cnf(p13698,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13697,c75]) ).
cnf(p13699,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13698,c0]) ).
cnf(p13700,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13699,p741]) ).
cnf(p13701,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13700,p839]) ).
cnf(p13702,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13701,c0]) ).
cnf(p13703,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13702,p838]) ).
cnf(p13704,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13703,p840]) ).
cnf(p13706,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13704,c0]) ).
cnf(p13707,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13706,p742]) ).
cnf(p13708,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13707,p1055]) ).
cnf(p13709,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13708,c0]) ).
cnf(p13711,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13709,p1054]) ).
cnf(p13712,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13711,p1056]) ).
cnf(p13713,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13712,p880]) ).
cnf(p13714,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13713,c0]) ).
cnf(p13715,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13714,p879]) ).
cnf(p13716,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13715,p881]) ).
cnf(p13717,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| ~ cC38(iV16465)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13716,c0]) ).
cnf(p13718,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC86(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13717,p745]) ).
cnf(p13721,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC84(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13718,c241]) ).
cnf(p13722,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC74(iV16453)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13721,c250]) ).
cnf(p13723,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC66(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13722,c210]) ).
cnf(p13724,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC64(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13723,c245]) ).
cnf(p13725,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC58(iV16453)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13724,c251]) ).
cnf(p13726,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC54(iV16455)
| cC40(iV16455)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13725,c209]) ).
cnf(p13727,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC48(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13726,c221]) ).
cnf(p13728,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC46(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13727,c238]) ).
cnf(p13731,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC36(iV16457)
| cC40(iV16455)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13728,c242]) ).
cnf(p13732,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC36(iV16457)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13731,c216]) ).
cnf(p13733,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC8(iV16460)
| cC12(iV16461)
| cC36(iV16448)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13732,c226]) ).
cnf(p13734,plain,
( cC30(iV16459)
| cC32(iV16459)
| cC8(iV16460)
| cC12(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13733,c194]) ).
cnf(p13735,plain,
( cC30(iV16459)
| cC8(iV16460)
| cC12(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13734,c253]) ).
cnf(p13736,plain,
( cC8(iV16460)
| cC12(iV16461)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13735,c239]) ).
cnf(p13737,plain,
( cC8(iV16460)
| xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13736,c269]) ).
cnf(p13739,plain,
( xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13737,c259]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p13646,plain,
( ~ xsd_integer(sk29)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13642,c2]) ).
cnf(p13740,plain,
( cowlNothing(sk28)
| cowlNothing(sk28) ),
inference(resolution,[status(thm)],[p13739,p13646]) ).
cnf(p13741,plain,
cowlNothing(sk28),
inference(factoring,[status(thm)],[p13740]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p13742,plain,
$false,
inference(resolution,[status(thm)],[p13741,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 19:34:53 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.29/2.38 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.29/2.38 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------