%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS161+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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:22 PM UTC 2026
% Result : Theorem 5.57s 1.31s
% Output : Proof 5.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 102
% Number of leaves : 63
% Syntax : Number of formulae : 373 ( 165 unt; 0 def)
% Number of atoms : 3282 ( 0 equ)
% Maximal formula atoms : 51 ( 8 avg)
% Number of connectives : 5524 (2615 ~;2706 |; 183 &)
% ( 19 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 50 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 15 con; 0-1 aty)
% Number of variables : 101 ( 2 sgn 67 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f146,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(f146_nnf,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
! [X] :
( cC98(X)
| ~ rR1(iV16439,X) ),
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c350,plain,
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
fof(f150,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(f150_nnf,plain,
rR1(iV16439,iV16440),
inference(nnf_transformation,[status(thm)],[f150]) ).
cnf(c354,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[status(esa)],[f150_nnf]) ).
cnf(p1785,plain,
cC98(iV16440),
inference(resolution,[status(thm)],[c350,c354]) ).
fof(f145,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_145) ).
fof(f145_nnf,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(nnf_transformation,[status(thm)],[f145]) ).
fof(f145_sk,plain,
! [X] :
( ( ~ cC130(X)
| ~ cC108(X)
| cTEST(X) )
& ( ( cC130(X)
& cC108(X) )
| ~ cTEST(X) ) ),
inference(skolemisation,[status(esa)],[f145_nnf]) ).
cnf(c348,plain,
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
fof(f149,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_149) ).
fof(f149_nnf,plain,
cTEST(iV16439),
inference(nnf_transformation,[status(thm)],[f149]) ).
cnf(c353,plain,
cTEST(iV16439),
inference(cnf_transformation,[status(esa)],[f149_nnf]) ).
cnf(p539,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[c348,c353]) ).
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(f286,conjecture,
( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f286_neg,negated_conjecture,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f286]) ).
fof(f286_nnf,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f286_neg]) ).
fof(f286_sk,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ( ~ xsd_integer(sk115)
& ~ xsd_string(sk115) )
| ( xsd_integer(sk115)
& xsd_string(sk115) )
| cowlNothing(sk114)
| ~ cowlThing(sk114) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk114,sk115])],[f286_nnf]) ).
cnf(c491,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sk115)
| xsd_string(sk115)
| cowlNothing(sk114)
| ~ cowlThing(sk114) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(p494,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sk115)
| xsd_string(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[c0,c491]) ).
cnf(p496,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_string(sk115)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[c3,p494]) ).
cnf(p497,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(factoring,[status(thm)],[p496]) ).
cnf(p540,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p539,p497]) ).
cnf(c347,plain,
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(p527,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[c347,c353]) ).
cnf(p541,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p540,p527]) ).
fof(f12,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_12) ).
fof(f12_nnf,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] :
( ( ~ cC106(X)
| ~ cC28(X)
| cC108(X) )
& ( ( cC106(X)
& cC28(X) )
| ~ cC108(X) ) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c29,plain,
( cC106(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p529,plain,
cC106(iV16439),
inference(resolution,[status(thm)],[p527,c29]) ).
fof(f11,axiom,
! [X] :
( cC106(X)
<=> ( cC100xcomp(X)
& cC104(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
fof(f11_nnf,plain,
! [X] :
( ( ~ cC100xcomp(X)
| ~ cC104(X)
| cC106(X) )
& ( ( cC100xcomp(X)
& cC104(X) )
| ~ cC106(X) ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] :
( ( ~ cC100xcomp(X)
| ~ cC104(X)
| cC106(X) )
& ( ( cC100xcomp(X)
& cC104(X) )
| ~ cC106(X) ) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c25,plain,
( cC104(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p530,plain,
cC104(iV16439),
inference(resolution,[status(thm)],[p529,c25]) ).
cnf(p542,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p541,p530]) ).
cnf(p543,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p542,p529]) ).
cnf(c28,plain,
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p528,plain,
cC28(iV16439),
inference(resolution,[status(thm)],[p527,c28]) ).
cnf(p544,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p543,p528]) ).
cnf(p545,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p544,c0]) ).
cnf(p1791,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1785,p545]) ).
fof(f119,axiom,
! [X] :
( cC80(X)
<=> ? [Y] :
( cC16xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_119) ).
fof(f119_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC16xcomp(Y)
| ~ rR1(X,Y) )
| cC80(X) )
& ( ? [Y] :
( cC16xcomp(Y)
& rR1(X,Y) )
| ~ cC80(X) ) ),
inference(nnf_transformation,[status(thm)],[f119]) ).
fof(f119_sk,plain,
! [X,Y] :
( ( ~ cC16xcomp(Y)
| ~ rR1(X,Y)
| cC80(X) )
& ( ( cC16xcomp(sk93(X))
& rR1(X,sk93(X)) )
| ~ cC80(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk93])],[f119_nnf]) ).
cnf(c287,plain,
( ~ cC16xcomp(X1)
| ~ rR1(X0,X1)
| cC80(X0) ),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
fof(f159,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_159) ).
fof(f159_nnf,plain,
rR1(iV16440,iV16463),
inference(nnf_transformation,[status(thm)],[f159]) ).
cnf(c363,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[status(esa)],[f159_nnf]) ).
cnf(p1504,plain,
( ~ cC16xcomp(iV16463)
| cC80(iV16440) ),
inference(resolution,[status(thm)],[c287,c363]) ).
fof(f257,axiom,
cC16xcomp(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_257) ).
fof(f257_nnf,plain,
cC16xcomp(iV16463),
inference(nnf_transformation,[status(thm)],[f257]) ).
cnf(c461,plain,
cC16xcomp(iV16463),
inference(cnf_transformation,[status(esa)],[f257_nnf]) ).
cnf(p1542,plain,
cC80(iV16440),
inference(resolution,[status(thm)],[p1504,c461]) ).
cnf(p1793,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1791,p1542]) ).
fof(f120,axiom,
! [X] :
( cC82(X)
<=> ( cC78xcomp(X)
& cC80(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f120_nnf,plain,
! [X] :
( ( ~ cC78xcomp(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC78xcomp(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [X] :
( ( ~ cC78xcomp(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC78xcomp(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c290,plain,
( ~ cC78xcomp(X0)
| ~ cC80(X0)
| cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(p1545,plain,
( ~ cC78xcomp(iV16440)
| cC82(iV16440) ),
inference(resolution,[status(thm)],[p1542,c290]) ).
fof(f158,axiom,
cC78xcomp(iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_158) ).
fof(f158_nnf,plain,
cC78xcomp(iV16440),
inference(nnf_transformation,[status(thm)],[f158]) ).
cnf(c362,plain,
cC78xcomp(iV16440),
inference(cnf_transformation,[status(esa)],[f158_nnf]) ).
cnf(p1592,plain,
cC82(iV16440),
inference(resolution,[status(thm)],[p1545,c362]) ).
cnf(p1794,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1793,p1592]) ).
cnf(p1795,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1794,c0]) ).
fof(f57,axiom,
! [X] :
( cC38(X)
<=> ( cC36xcomp(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
fof(f57_nnf,plain,
! [X] :
( ( ~ cC36xcomp(X)
| ~ cTOP(X)
| cC38(X) )
& ( ( cC36xcomp(X)
& cTOP(X) )
| ~ cC38(X) ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X] :
( ( ~ cC36xcomp(X)
| ~ cTOP(X)
| cC38(X) )
& ( ( cC36xcomp(X)
& cTOP(X) )
| ~ cC38(X) ) ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c141,plain,
( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f163,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f163_nnf,plain,
cTOP(iV16448),
inference(nnf_transformation,[status(thm)],[f163]) ).
cnf(c367,plain,
cTOP(iV16448),
inference(cnf_transformation,[status(esa)],[f163_nnf]) ).
cnf(p861,plain,
( ~ cC36xcomp(iV16448)
| cC38(iV16448) ),
inference(resolution,[status(thm)],[c141,c367]) ).
fof(f168,axiom,
cC36xcomp(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_168) ).
fof(f168_nnf,plain,
cC36xcomp(iV16448),
inference(nnf_transformation,[status(thm)],[f168]) ).
cnf(c372,plain,
cC36xcomp(iV16448),
inference(cnf_transformation,[status(esa)],[f168_nnf]) ).
cnf(p885,plain,
cC38(iV16448),
inference(resolution,[status(thm)],[p861,c372]) ).
cnf(p1797,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1795,p885]) ).
cnf(p1798,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1797,c0]) ).
fof(f112,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& cC74xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_112) ).
fof(f112_nnf,plain,
! [X] :
( ( ~ cC62(X)
| ~ cC74xcomp(X)
| cC76(X) )
& ( ( cC62(X)
& cC74xcomp(X) )
| ~ cC76(X) ) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
! [X] :
( ( ~ cC62(X)
| ~ cC74xcomp(X)
| cC76(X) )
& ( ( cC62(X)
& cC74xcomp(X) )
| ~ cC76(X) ) ),
inference(skolemisation,[status(esa)],[f112_nnf]) ).
cnf(c271,plain,
( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
fof(f174,axiom,
cC74xcomp(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(f174_nnf,plain,
cC74xcomp(iV16453),
inference(nnf_transformation,[status(thm)],[f174]) ).
cnf(c378,plain,
cC74xcomp(iV16453),
inference(cnf_transformation,[status(esa)],[f174_nnf]) ).
cnf(p1420,plain,
( ~ cC62(iV16453)
| cC76(iV16453) ),
inference(resolution,[status(thm)],[c271,c378]) ).
fof(f91,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_91) ).
fof(f91_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC12xcomp(Y)
| ~ rR1(X,Y) )
| cC60(X) )
& ( ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) )
| ~ cC60(X) ) ),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
! [X,Y] :
( ( ~ cC12xcomp(Y)
| ~ rR1(X,Y)
| cC60(X) )
& ( ( cC12xcomp(sk70(X))
& rR1(X,sk70(X)) )
| ~ cC60(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk70])],[f91_nnf]) ).
cnf(c221,plain,
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
fof(f182,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_182) ).
fof(f182_nnf,plain,
rR1(iV16453,iV16461),
inference(nnf_transformation,[status(thm)],[f182]) ).
cnf(c386,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[status(esa)],[f182_nnf]) ).
cnf(p1195,plain,
( ~ cC12xcomp(iV16461)
| cC60(iV16453) ),
inference(resolution,[status(thm)],[c221,c386]) ).
fof(f237,axiom,
cC12xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_237) ).
fof(f237_nnf,plain,
cC12xcomp(iV16461),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c441,plain,
cC12xcomp(iV16461),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p1224,plain,
cC60(iV16453),
inference(resolution,[status(thm)],[p1195,c441]) ).
fof(f92,axiom,
! [X] :
( cC62(X)
<=> ( cC58xcomp(X)
& cC60(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_92) ).
fof(f92_nnf,plain,
! [X] :
( ( ~ cC58xcomp(X)
| ~ cC60(X)
| cC62(X) )
& ( ( cC58xcomp(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [X] :
( ( ~ cC58xcomp(X)
| ~ cC60(X)
| cC62(X) )
& ( ( cC58xcomp(X)
& cC60(X) )
| ~ cC62(X) ) ),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c224,plain,
( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(p1227,plain,
( ~ cC58xcomp(iV16453)
| cC62(iV16453) ),
inference(resolution,[status(thm)],[p1224,c224]) ).
fof(f181,axiom,
cC58xcomp(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_181) ).
fof(f181_nnf,plain,
cC58xcomp(iV16453),
inference(nnf_transformation,[status(thm)],[f181]) ).
cnf(c385,plain,
cC58xcomp(iV16453),
inference(cnf_transformation,[status(esa)],[f181_nnf]) ).
cnf(p1277,plain,
cC62(iV16453),
inference(resolution,[status(thm)],[p1227,c385]) ).
cnf(p1423,plain,
cC76(iV16453),
inference(resolution,[status(thm)],[p1420,p1277]) ).
cnf(p1799,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1798,p1423]) ).
cnf(p1800,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1799,p1277]) ).
cnf(p1802,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1800,c0]) ).
cnf(p1803,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1802,p1224]) ).
fof(f82,axiom,
! [X] :
( cC56(X)
<=> ( cC44(X)
& cC54xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
fof(f82_nnf,plain,
! [X] :
( ( ~ cC44(X)
| ~ cC54xcomp(X)
| cC56(X) )
& ( ( cC44(X)
& cC54xcomp(X) )
| ~ cC56(X) ) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [X] :
( ( ~ cC44(X)
| ~ cC54xcomp(X)
| cC56(X) )
& ( ( cC44(X)
& cC54xcomp(X) )
| ~ cC56(X) ) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c200,plain,
( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
fof(f190,axiom,
cC54xcomp(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_190) ).
fof(f190_nnf,plain,
cC54xcomp(iV16455),
inference(nnf_transformation,[status(thm)],[f190]) ).
cnf(c394,plain,
cC54xcomp(iV16455),
inference(cnf_transformation,[status(esa)],[f190_nnf]) ).
cnf(p1113,plain,
( ~ cC44(iV16455)
| cC56(iV16455) ),
inference(resolution,[status(thm)],[c200,c394]) ).
fof(f66,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& cC40xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f66_nnf,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC40xcomp(X)
| cC44(X) )
& ( ( cC42(X)
& cC40xcomp(X) )
| ~ cC44(X) ) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC40xcomp(X)
| cC44(X) )
& ( ( cC42(X)
& cC40xcomp(X) )
| ~ cC44(X) ) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c162,plain,
( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
fof(f185,axiom,
cC40xcomp(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_185) ).
fof(f185_nnf,plain,
cC40xcomp(iV16455),
inference(nnf_transformation,[status(thm)],[f185]) ).
cnf(c389,plain,
cC40xcomp(iV16455),
inference(cnf_transformation,[status(esa)],[f185_nnf]) ).
cnf(p952,plain,
( ~ cC42(iV16455)
| cC44(iV16455) ),
inference(resolution,[status(thm)],[c162,c389]) ).
fof(f65,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f65_nnf,plain,
! [X] :
( ( ! [Y] :
( ~ cC8xcomp(Y)
| ~ rR1(X,Y) )
| cC42(X) )
& ( ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) )
| ~ cC42(X) ) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X,Y] :
( ( ~ cC8xcomp(Y)
| ~ rR1(X,Y)
| cC42(X) )
& ( ( cC8xcomp(sk50(X))
& rR1(X,sk50(X)) )
| ~ cC42(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk50])],[f65_nnf]) ).
cnf(c159,plain,
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
fof(f193,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_193) ).
fof(f193_nnf,plain,
rR1(iV16455,iV16460),
inference(nnf_transformation,[status(thm)],[f193]) ).
cnf(c397,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[status(esa)],[f193_nnf]) ).
cnf(p941,plain,
( ~ cC8xcomp(iV16460)
| cC42(iV16455) ),
inference(resolution,[status(thm)],[c159,c397]) ).
fof(f227,axiom,
cC8xcomp(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_227) ).
fof(f227_nnf,plain,
cC8xcomp(iV16460),
inference(nnf_transformation,[status(thm)],[f227]) ).
cnf(c431,plain,
cC8xcomp(iV16460),
inference(cnf_transformation,[status(esa)],[f227_nnf]) ).
cnf(p961,plain,
cC42(iV16455),
inference(resolution,[status(thm)],[p941,c431]) ).
cnf(p1026,plain,
cC44(iV16455),
inference(resolution,[status(thm)],[p952,p961]) ).
cnf(p1137,plain,
cC56(iV16455),
inference(resolution,[status(thm)],[p1113,p1026]) ).
cnf(p1804,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1803,p1137]) ).
cnf(p1805,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1804,p1026]) ).
cnf(p1806,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1805,p961]) ).
cnf(p1807,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1806,c0]) ).
fof(f197,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_197) ).
fof(f197_nnf,plain,
cTOP(iV16457),
inference(nnf_transformation,[status(thm)],[f197]) ).
cnf(c401,plain,
cTOP(iV16457),
inference(cnf_transformation,[status(esa)],[f197_nnf]) ).
cnf(p862,plain,
( ~ cC36xcomp(iV16457)
| cC38(iV16457) ),
inference(resolution,[status(thm)],[c141,c401]) ).
fof(f201,axiom,
cC36xcomp(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_201) ).
fof(f201_nnf,plain,
cC36xcomp(iV16457),
inference(nnf_transformation,[status(thm)],[f201]) ).
cnf(c405,plain,
cC36xcomp(iV16457),
inference(cnf_transformation,[status(esa)],[f201_nnf]) ).
cnf(p888,plain,
cC38(iV16457),
inference(resolution,[status(thm)],[p862,c405]) ).
cnf(p1808,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1807,p888]) ).
cnf(p1809,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1808,c0]) ).
fof(f73,axiom,
! [X] :
( cC50(X)
<=> ( cC48xcomp(X)
& cC46xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f73_nnf,plain,
! [X] :
( ( ~ cC48xcomp(X)
| ~ cC46xcomp(X)
| cC50(X) )
& ( ( cC48xcomp(X)
& cC46xcomp(X) )
| ~ cC50(X) ) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [X] :
( ( ~ cC48xcomp(X)
| ~ cC46xcomp(X)
| cC50(X) )
& ( ( cC48xcomp(X)
& cC46xcomp(X) )
| ~ cC50(X) ) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c179,plain,
( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
fof(f212,axiom,
cC46xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_212) ).
fof(f212_nnf,plain,
cC46xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f212]) ).
cnf(c416,plain,
cC46xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f212_nnf]) ).
cnf(p1038,plain,
( ~ cC48xcomp(iV16459)
| cC50(iV16459) ),
inference(resolution,[status(thm)],[c179,c416]) ).
fof(f217,axiom,
cC48xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_217) ).
fof(f217_nnf,plain,
cC48xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f217]) ).
cnf(c421,plain,
cC48xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f217_nnf]) ).
cnf(p1040,plain,
cC50(iV16459),
inference(resolution,[status(thm)],[p1038,c421]) ).
cnf(p1811,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1809,p1040]) ).
fof(f128,axiom,
! [X] :
( cC88(X)
<=> ( cC86xcomp(X)
& cC84xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_128) ).
fof(f128_nnf,plain,
! [X] :
( ( ~ cC86xcomp(X)
| ~ cC84xcomp(X)
| cC88(X) )
& ( ( cC86xcomp(X)
& cC84xcomp(X) )
| ~ cC88(X) ) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [X] :
( ( ~ cC86xcomp(X)
| ~ cC84xcomp(X)
| cC88(X) )
& ( ( cC86xcomp(X)
& cC84xcomp(X) )
| ~ cC88(X) ) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c309,plain,
( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f210,axiom,
cC84xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_210) ).
fof(f210_nnf,plain,
cC84xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f210]) ).
cnf(c414,plain,
cC84xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f210_nnf]) ).
cnf(p1625,plain,
( ~ cC86xcomp(iV16459)
| cC88(iV16459) ),
inference(resolution,[status(thm)],[c309,c414]) ).
fof(f215,axiom,
cC86xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_215) ).
fof(f215_nnf,plain,
cC86xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f215]) ).
cnf(c419,plain,
cC86xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f215_nnf]) ).
cnf(p1628,plain,
cC88(iV16459),
inference(resolution,[status(thm)],[p1625,c419]) ).
cnf(p1812,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1811,p1628]) ).
fof(f52,axiom,
! [X] :
( cC34(X)
<=> ( cC32xcomp(X)
& cC30xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_52) ).
fof(f52_nnf,plain,
! [X] :
( ( ~ cC32xcomp(X)
| ~ cC30xcomp(X)
| cC34(X) )
& ( ( cC32xcomp(X)
& cC30xcomp(X) )
| ~ cC34(X) ) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [X] :
( ( ~ cC32xcomp(X)
| ~ cC30xcomp(X)
| cC34(X) )
& ( ( cC32xcomp(X)
& cC30xcomp(X) )
| ~ cC34(X) ) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c129,plain,
( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f209,axiom,
cC30xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_209) ).
fof(f209_nnf,plain,
cC30xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f209]) ).
cnf(c413,plain,
cC30xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f209_nnf]) ).
cnf(p825,plain,
( ~ cC32xcomp(iV16459)
| cC34(iV16459) ),
inference(resolution,[status(thm)],[c129,c413]) ).
fof(f216,axiom,
cC32xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_216) ).
fof(f216_nnf,plain,
cC32xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f216]) ).
cnf(c420,plain,
cC32xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f216_nnf]) ).
cnf(p832,plain,
cC34(iV16459),
inference(resolution,[status(thm)],[p825,c420]) ).
cnf(p1813,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1812,p832]) ).
fof(f100,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC64xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(f100_nnf,plain,
! [X] :
( ( ~ cC66xcomp(X)
| ~ cC64xcomp(X)
| cC68(X) )
& ( ( cC66xcomp(X)
& cC64xcomp(X) )
| ~ cC68(X) ) ),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [X] :
( ( ~ cC66xcomp(X)
| ~ cC64xcomp(X)
| cC68(X) )
& ( ( cC66xcomp(X)
& cC64xcomp(X) )
| ~ cC68(X) ) ),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c243,plain,
( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
fof(f213,axiom,
cC64xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_213) ).
fof(f213_nnf,plain,
cC64xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f213]) ).
cnf(c417,plain,
cC64xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f213_nnf]) ).
cnf(p1287,plain,
( ~ cC66xcomp(iV16459)
| cC68(iV16459) ),
inference(resolution,[status(thm)],[c243,c417]) ).
fof(f221,axiom,
cC66xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_221) ).
fof(f221_nnf,plain,
cC66xcomp(iV16459),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c425,plain,
cC66xcomp(iV16459),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p1289,plain,
cC68(iV16459),
inference(resolution,[status(thm)],[p1287,c425]) ).
cnf(p1814,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1813,p1289]) ).
cnf(p1816,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1814,c0]) ).
fof(f225,axiom,
cTOP(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_225) ).
fof(f225_nnf,plain,
cTOP(iV16460),
inference(nnf_transformation,[status(thm)],[f225]) ).
cnf(c429,plain,
cTOP(iV16460),
inference(cnf_transformation,[status(esa)],[f225_nnf]) ).
cnf(p863,plain,
( ~ cC36xcomp(iV16460)
| cC38(iV16460) ),
inference(resolution,[status(thm)],[c141,c429]) ).
fof(f228,axiom,
cC36xcomp(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_228) ).
fof(f228_nnf,plain,
cC36xcomp(iV16460),
inference(nnf_transformation,[status(thm)],[f228]) ).
cnf(c432,plain,
cC36xcomp(iV16460),
inference(cnf_transformation,[status(esa)],[f228_nnf]) ).
cnf(p891,plain,
cC38(iV16460),
inference(resolution,[status(thm)],[p863,c432]) ).
cnf(p1817,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1816,p891]) ).
cnf(p1818,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1817,c0]) ).
fof(f243,axiom,
rR1(iV16461,iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_243) ).
fof(f243_nnf,plain,
rR1(iV16461,iV16462),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c447,plain,
rR1(iV16461,iV16462),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(p942,plain,
( ~ cC8xcomp(iV16462)
| cC42(iV16461) ),
inference(resolution,[status(thm)],[c159,c447]) ).
fof(f249,axiom,
cC8xcomp(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_249) ).
fof(f249_nnf,plain,
cC8xcomp(iV16462),
inference(nnf_transformation,[status(thm)],[f249]) ).
cnf(c453,plain,
cC8xcomp(iV16462),
inference(cnf_transformation,[status(esa)],[f249_nnf]) ).
cnf(p979,plain,
cC42(iV16461),
inference(resolution,[status(thm)],[p942,c453]) ).
cnf(p1819,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1818,p979]) ).
fof(f240,axiom,
cC54xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_240) ).
fof(f240_nnf,plain,
cC54xcomp(iV16461),
inference(nnf_transformation,[status(thm)],[f240]) ).
cnf(c444,plain,
cC54xcomp(iV16461),
inference(cnf_transformation,[status(esa)],[f240_nnf]) ).
cnf(p1114,plain,
( ~ cC44(iV16461)
| cC56(iV16461) ),
inference(resolution,[status(thm)],[c200,c444]) ).
fof(f234,axiom,
cC40xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_234) ).
fof(f234_nnf,plain,
cC40xcomp(iV16461),
inference(nnf_transformation,[status(thm)],[f234]) ).
cnf(c438,plain,
cC40xcomp(iV16461),
inference(cnf_transformation,[status(esa)],[f234_nnf]) ).
cnf(p953,plain,
( ~ cC42(iV16461)
| cC44(iV16461) ),
inference(resolution,[status(thm)],[c162,c438]) ).
cnf(p1027,plain,
cC44(iV16461),
inference(resolution,[status(thm)],[p953,p979]) ).
cnf(p1155,plain,
cC56(iV16461),
inference(resolution,[status(thm)],[p1114,p1027]) ).
cnf(p1821,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1819,p1155]) ).
cnf(p1822,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1821,p1027]) ).
cnf(p1823,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1822,c0]) ).
fof(f247,axiom,
cTOP(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_247) ).
fof(f247_nnf,plain,
cTOP(iV16462),
inference(nnf_transformation,[status(thm)],[f247]) ).
cnf(c451,plain,
cTOP(iV16462),
inference(cnf_transformation,[status(esa)],[f247_nnf]) ).
cnf(p864,plain,
( ~ cC36xcomp(iV16462)
| cC38(iV16462) ),
inference(resolution,[status(thm)],[c141,c451]) ).
fof(f252,axiom,
cC36xcomp(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_252) ).
fof(f252_nnf,plain,
cC36xcomp(iV16462),
inference(nnf_transformation,[status(thm)],[f252]) ).
cnf(c456,plain,
cC36xcomp(iV16462),
inference(cnf_transformation,[status(esa)],[f252_nnf]) ).
cnf(p894,plain,
cC38(iV16462),
inference(resolution,[status(thm)],[p864,c456]) ).
cnf(p1824,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1823,p894]) ).
cnf(p1826,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1824,c0]) ).
fof(f255,axiom,
cC74xcomp(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_255) ).
fof(f255_nnf,plain,
cC74xcomp(iV16463),
inference(nnf_transformation,[status(thm)],[f255]) ).
cnf(c459,plain,
cC74xcomp(iV16463),
inference(cnf_transformation,[status(esa)],[f255_nnf]) ).
cnf(p1421,plain,
( ~ cC62(iV16463)
| cC76(iV16463) ),
inference(resolution,[status(thm)],[c271,c459]) ).
fof(f263,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_263) ).
fof(f263_nnf,plain,
rR1(iV16463,iV16464),
inference(nnf_transformation,[status(thm)],[f263]) ).
cnf(c467,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[status(esa)],[f263_nnf]) ).
cnf(p1198,plain,
( ~ cC12xcomp(iV16464)
| cC60(iV16463) ),
inference(resolution,[status(thm)],[c221,c467]) ).
fof(f267,axiom,
cC12xcomp(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_267) ).
fof(f267_nnf,plain,
cC12xcomp(iV16464),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c471,plain,
cC12xcomp(iV16464),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(p1249,plain,
cC60(iV16463),
inference(resolution,[status(thm)],[p1198,c471]) ).
cnf(p1252,plain,
( ~ cC58xcomp(iV16463)
| cC62(iV16463) ),
inference(resolution,[status(thm)],[p1249,c224]) ).
fof(f262,axiom,
cC58xcomp(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_262) ).
fof(f262_nnf,plain,
cC58xcomp(iV16463),
inference(nnf_transformation,[status(thm)],[f262]) ).
cnf(c466,plain,
cC58xcomp(iV16463),
inference(cnf_transformation,[status(esa)],[f262_nnf]) ).
cnf(p1279,plain,
cC62(iV16463),
inference(resolution,[status(thm)],[p1252,c466]) ).
cnf(p1425,plain,
cC76(iV16463),
inference(resolution,[status(thm)],[p1421,p1279]) ).
cnf(p1827,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1826,p1425]) ).
cnf(p1828,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1827,p1279]) ).
cnf(p1829,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1828,c0]) ).
cnf(p1831,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1829,p1249]) ).
fof(f270,axiom,
cC54xcomp(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_270) ).
fof(f270_nnf,plain,
cC54xcomp(iV16464),
inference(nnf_transformation,[status(thm)],[f270]) ).
cnf(c474,plain,
cC54xcomp(iV16464),
inference(cnf_transformation,[status(esa)],[f270_nnf]) ).
cnf(p1115,plain,
( ~ cC44(iV16464)
| cC56(iV16464) ),
inference(resolution,[status(thm)],[c200,c474]) ).
fof(f266,axiom,
cC40xcomp(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_266) ).
fof(f266_nnf,plain,
cC40xcomp(iV16464),
inference(nnf_transformation,[status(thm)],[f266]) ).
cnf(c470,plain,
cC40xcomp(iV16464),
inference(cnf_transformation,[status(esa)],[f266_nnf]) ).
cnf(p954,plain,
( ~ cC42(iV16464)
| cC44(iV16464) ),
inference(resolution,[status(thm)],[c162,c470]) ).
fof(f274,axiom,
rR1(iV16464,iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_274) ).
fof(f274_nnf,plain,
rR1(iV16464,iV16465),
inference(nnf_transformation,[status(thm)],[f274]) ).
cnf(c478,plain,
rR1(iV16464,iV16465),
inference(cnf_transformation,[status(esa)],[f274_nnf]) ).
cnf(p944,plain,
( ~ cC8xcomp(iV16465)
| cC42(iV16464) ),
inference(resolution,[status(thm)],[c159,c478]) ).
fof(f280,axiom,
cC8xcomp(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_280) ).
fof(f280_nnf,plain,
cC8xcomp(iV16465),
inference(nnf_transformation,[status(thm)],[f280]) ).
cnf(c484,plain,
cC8xcomp(iV16465),
inference(cnf_transformation,[status(esa)],[f280_nnf]) ).
cnf(p997,plain,
cC42(iV16464),
inference(resolution,[status(thm)],[p944,c484]) ).
cnf(p1028,plain,
cC44(iV16464),
inference(resolution,[status(thm)],[p954,p997]) ).
cnf(p1158,plain,
cC56(iV16464),
inference(resolution,[status(thm)],[p1115,p1028]) ).
cnf(p1832,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1831,p1158]) ).
cnf(p1833,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1832,p997]) ).
cnf(p1834,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1833,p1028]) ).
cnf(p1836,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1834,c0]) ).
fof(f277,axiom,
cTOP(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_277) ).
fof(f277_nnf,plain,
cTOP(iV16465),
inference(nnf_transformation,[status(thm)],[f277]) ).
cnf(c481,plain,
cTOP(iV16465),
inference(cnf_transformation,[status(esa)],[f277_nnf]) ).
cnf(p865,plain,
( ~ cC36xcomp(iV16465)
| cC38(iV16465) ),
inference(resolution,[status(thm)],[c141,c481]) ).
fof(f282,axiom,
cC36xcomp(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_282) ).
fof(f282_nnf,plain,
cC36xcomp(iV16465),
inference(nnf_transformation,[status(thm)],[f282]) ).
cnf(c486,plain,
cC36xcomp(iV16465),
inference(cnf_transformation,[status(esa)],[f282_nnf]) ).
cnf(p896,plain,
cC38(iV16465),
inference(resolution,[status(thm)],[p865,c486]) ).
cnf(p1837,plain,
( ~ cowlThing(iV16465)
| cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1836,p896]) ).
cnf(p1838,plain,
( cowlNothing(sk114)
| xsd_string(sk115) ),
inference(resolution,[status(thm)],[p1837,c0]) ).
cnf(c492,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_string(sk115)
| xsd_integer(sk115)
| cowlNothing(sk114)
| ~ cowlThing(sk114) ),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
cnf(p495,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_string(sk115)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[c0,c492]) ).
cnf(p1839,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1838,p495]) ).
cnf(p1842,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(factoring,[status(thm)],[p1839]) ).
cnf(p1843,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1842,p539]) ).
cnf(p1844,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1843,p527]) ).
cnf(p1846,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1844,p530]) ).
cnf(p1847,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1846,p529]) ).
cnf(p1848,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1847,p528]) ).
cnf(p1849,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1848,c0]) ).
cnf(p1851,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1849,p1785]) ).
cnf(p1852,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1851,p1542]) ).
cnf(p1853,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1852,p1592]) ).
cnf(p1854,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1853,c0]) ).
cnf(p1856,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1854,p885]) ).
cnf(p1857,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1856,c0]) ).
cnf(p1858,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1857,p1423]) ).
cnf(p1859,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1858,p1277]) ).
cnf(p1861,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1859,c0]) ).
cnf(p1862,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1861,p1224]) ).
cnf(p1863,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1862,p1137]) ).
cnf(p1864,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1863,p1026]) ).
cnf(p1866,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1864,p961]) ).
cnf(p1867,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1866,c0]) ).
cnf(p1868,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1867,p888]) ).
cnf(p1869,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1868,c0]) ).
cnf(p1871,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1869,p1040]) ).
cnf(p1872,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1871,p1628]) ).
cnf(p1873,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1872,p832]) ).
cnf(p1874,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1873,p1289]) ).
cnf(p1875,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1874,c0]) ).
cnf(p1876,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1875,p891]) ).
cnf(p1877,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1876,c0]) ).
cnf(p1878,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1877,p979]) ).
cnf(p1879,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1878,p1155]) ).
cnf(p1880,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1879,p1027]) ).
cnf(p1881,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1880,c0]) ).
cnf(p1882,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1881,p894]) ).
cnf(p1883,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1882,c0]) ).
cnf(p1884,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1883,p1425]) ).
cnf(p1885,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1884,p1279]) ).
cnf(p1886,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1885,c0]) ).
cnf(p1887,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1886,p1249]) ).
cnf(p1888,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1887,p1158]) ).
cnf(p1889,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1888,p997]) ).
cnf(p1890,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1889,p1028]) ).
cnf(p1891,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1890,c0]) ).
cnf(p1892,plain,
( ~ cowlThing(iV16465)
| xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1891,p896]) ).
cnf(p1893,plain,
( xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1892,c0]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1840,plain,
( ~ xsd_integer(sk115)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1838,c2]) ).
cnf(p1894,plain,
( cowlNothing(sk114)
| cowlNothing(sk114) ),
inference(resolution,[status(thm)],[p1893,p1840]) ).
cnf(p1895,plain,
cowlNothing(sk114),
inference(factoring,[status(thm)],[p1894]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1896,plain,
$false,
inference(resolution,[status(thm)],[p1895,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 19:38:27 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.57/1.31 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.57/1.31 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------