%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS159+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:22 PM UTC 2026
% Result : Theorem 6.34s 1.34s
% Output : Proof 6.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 116
% Number of leaves : 74
% Syntax : Number of formulae : 485 ( 89 unt; 0 def)
% Number of atoms : 4355 ( 0 equ)
% Maximal formula atoms : 56 ( 8 avg)
% Number of connectives : 7249 (3379 ~;3484 |; 323 &)
% ( 63 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 88 ( 87 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 6 con; 0-1 aty)
% Number of variables : 390 ( 20 sgn 238 !; 50 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f161,axiom,
! [X] :
( cC74(X)
<=> ( cC18xcomp(X)
& cC72xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_161) ).
fof(f161_nnf,plain,
! [X] :
( ( ~ cC18xcomp(X)
| ~ cC72xcomp(X)
| cC74(X) )
& ( ( cC18xcomp(X)
& cC72xcomp(X) )
| ~ cC74(X) ) ),
inference(nnf_transformation,[status(thm)],[f161]) ).
fof(f161_sk,plain,
! [X] :
( ( ~ cC18xcomp(X)
| ~ cC72xcomp(X)
| cC74(X) )
& ( ( cC18xcomp(X)
& cC72xcomp(X) )
| ~ cC74(X) ) ),
inference(skolemisation,[status(esa)],[f161_nnf]) ).
cnf(c391,plain,
( ~ cC18xcomp(X0)
| ~ cC72xcomp(X0)
| cC74(X0) ),
inference(cnf_transformation,[status(esa)],[f161_sk]) ).
fof(f160,axiom,
! [X] :
( cC72xcomp(X)
<=> ~ ? [Y] : ra_Px24(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_160) ).
fof(f160_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px24(X,Y)
| cC72xcomp(X) )
& ( ! [Y] : ~ ra_Px24(X,Y)
| ~ cC72xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f160]) ).
fof(f160_sk,plain,
! [X,Y] :
( ( ra_Px24(X,sk119(X))
| cC72xcomp(X) )
& ( ~ ra_Px24(X,Y)
| ~ cC72xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk119])],[f160_nnf]) ).
cnf(c388,plain,
( ra_Px24(X0,sk119(X0))
| cC72xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f160_sk]) ).
fof(f158,axiom,
! [X] :
( cC72(X)
<=> ? [Y0] : ra_Px24(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_158) ).
fof(f158_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px24(X,Y0)
| cC72(X) )
& ( ? [Y0] : ra_Px24(X,Y0)
| ~ cC72(X) ) ),
inference(nnf_transformation,[status(thm)],[f158]) ).
fof(f158_sk,plain,
! [X,Y0] :
( ( ~ ra_Px24(X,Y0)
| cC72(X) )
& ( ra_Px24(X,sk117(X))
| ~ cC72(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk117])],[f158_nnf]) ).
cnf(c383,plain,
( ~ ra_Px24(X0,X1)
| cC72(X0) ),
inference(cnf_transformation,[status(esa)],[f158_sk]) ).
cnf(p1008,plain,
( cC72(X0)
| cC72xcomp(X0) ),
inference(resolution,[status(thm)],[c388,c383]) ).
cnf(p1147,plain,
( cC72(X0)
| ~ cC18xcomp(X0)
| cC74(X0) ),
inference(resolution,[status(thm)],[c391,p1008]) ).
fof(f293,axiom,
cC18xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_293) ).
fof(f293_nnf,plain,
cC18xcomp(iV21030),
inference(nnf_transformation,[status(thm)],[f293]) ).
cnf(c559,plain,
cC18xcomp(iV21030),
inference(cnf_transformation,[status(esa)],[f293_nnf]) ).
cnf(p1266,plain,
( cC72(iV21030)
| cC74(iV21030) ),
inference(resolution,[status(thm)],[p1147,c559]) ).
fof(f162,axiom,
! [X] :
( cC74(X)
<=> ? [Y0] : ra_Px87(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_162) ).
fof(f162_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px87(X,Y0)
| cC74(X) )
& ( ? [Y0] : ra_Px87(X,Y0)
| ~ cC74(X) ) ),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
! [X,Y0] :
( ( ~ ra_Px87(X,Y0)
| cC74(X) )
& ( ra_Px87(X,sk120(X))
| ~ cC74(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk120])],[f162_nnf]) ).
cnf(c392,plain,
( ra_Px87(X0,sk120(X0))
| ~ cC74(X0) ),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(p1268,plain,
( ra_Px87(iV21030,sk120(iV21030))
| cC72(iV21030) ),
inference(resolution,[status(thm)],[p1266,c392]) ).
fof(f163,axiom,
! [X] :
( cC74xcomp(X)
<=> ~ ? [Y] : ra_Px87(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f163_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px87(X,Y)
| cC74xcomp(X) )
& ( ! [Y] : ~ ra_Px87(X,Y)
| ~ cC74xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
! [X,Y] :
( ( ra_Px87(X,sk121(X))
| cC74xcomp(X) )
& ( ~ ra_Px87(X,Y)
| ~ cC74xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk121])],[f163_nnf]) ).
cnf(c394,plain,
( ~ ra_Px87(X0,X1)
| ~ cC74xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
fof(f307,axiom,
cC74xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_307) ).
fof(f307_nnf,plain,
cC74xcomp(iV21030),
inference(nnf_transformation,[status(thm)],[f307]) ).
cnf(c573,plain,
cC74xcomp(iV21030),
inference(cnf_transformation,[status(esa)],[f307_nnf]) ).
cnf(p746,plain,
~ ra_Px87(iV21030,X0),
inference(resolution,[status(thm)],[c394,c573]) ).
cnf(p1270,plain,
cC72(iV21030),
inference(resolution,[status(thm)],[p1268,p746]) ).
fof(f137,axiom,
! [X] :
( cC52(X)
<=> ( cC12xcomp(X)
& cC50xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_137) ).
fof(f137_nnf,plain,
! [X] :
( ( ~ cC12xcomp(X)
| ~ cC50xcomp(X)
| cC52(X) )
& ( ( cC12xcomp(X)
& cC50xcomp(X) )
| ~ cC52(X) ) ),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
! [X] :
( ( ~ cC12xcomp(X)
| ~ cC50xcomp(X)
| cC52(X) )
& ( ( cC12xcomp(X)
& cC50xcomp(X) )
| ~ cC52(X) ) ),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c333,plain,
( ~ cC12xcomp(X0)
| ~ cC50xcomp(X0)
| cC52(X0) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
fof(f134,axiom,
! [X] :
( cC50(X)
<=> ~ ? [Y] : ra_Px16(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_134) ).
fof(f134_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px16(X,Y)
| cC50(X) )
& ( ! [Y] : ~ ra_Px16(X,Y)
| ~ cC50(X) ) ),
inference(nnf_transformation,[status(thm)],[f134]) ).
fof(f134_sk,plain,
! [X,Y] :
( ( ra_Px16(X,sk100(X))
| cC50(X) )
& ( ~ ra_Px16(X,Y)
| ~ cC50(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk100])],[f134_nnf]) ).
cnf(c326,plain,
( ra_Px16(X0,sk100(X0))
| cC50(X0) ),
inference(cnf_transformation,[status(esa)],[f134_sk]) ).
fof(f135,axiom,
! [X] :
( cC50xcomp(X)
<=> ? [Y0] : ra_Px16(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_135) ).
fof(f135_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px16(X,Y0)
| cC50xcomp(X) )
& ( ? [Y0] : ra_Px16(X,Y0)
| ~ cC50xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
! [X,Y0] :
( ( ~ ra_Px16(X,Y0)
| cC50xcomp(X) )
& ( ra_Px16(X,sk101(X))
| ~ cC50xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk101])],[f135_nnf]) ).
cnf(c328,plain,
( ~ ra_Px16(X0,X1)
| cC50xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(p983,plain,
( cC50xcomp(X0)
| cC50(X0) ),
inference(resolution,[status(thm)],[c326,c328]) ).
cnf(p1123,plain,
( cC50(X0)
| ~ cC12xcomp(X0)
| cC52(X0) ),
inference(resolution,[status(thm)],[c333,p983]) ).
fof(f265,axiom,
cC12xcomp(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_265) ).
fof(f265_nnf,plain,
cC12xcomp(iV21029),
inference(nnf_transformation,[status(thm)],[f265]) ).
cnf(c531,plain,
cC12xcomp(iV21029),
inference(cnf_transformation,[status(esa)],[f265_nnf]) ).
cnf(p1226,plain,
( cC50(iV21029)
| cC52(iV21029) ),
inference(resolution,[status(thm)],[p1123,c531]) ).
fof(f136,axiom,
! [X] :
( cC52(X)
<=> ? [Y0] : ra_Px89(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_136) ).
fof(f136_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px89(X,Y0)
| cC52(X) )
& ( ? [Y0] : ra_Px89(X,Y0)
| ~ cC52(X) ) ),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
! [X,Y0] :
( ( ~ ra_Px89(X,Y0)
| cC52(X) )
& ( ra_Px89(X,sk102(X))
| ~ cC52(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk102])],[f136_nnf]) ).
cnf(c329,plain,
( ra_Px89(X0,sk102(X0))
| ~ cC52(X0) ),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
cnf(p1233,plain,
( ra_Px89(iV21029,sk102(iV21029))
| cC50(iV21029) ),
inference(resolution,[status(thm)],[p1226,c329]) ).
fof(f138,axiom,
! [X] :
( cC52xcomp(X)
<=> ~ ? [Y] : ra_Px89(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_138) ).
fof(f138_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px89(X,Y)
| cC52xcomp(X) )
& ( ! [Y] : ~ ra_Px89(X,Y)
| ~ cC52xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f138]) ).
fof(f138_sk,plain,
! [X,Y] :
( ( ra_Px89(X,sk103(X))
| cC52xcomp(X) )
& ( ~ ra_Px89(X,Y)
| ~ cC52xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk103])],[f138_nnf]) ).
cnf(c334,plain,
( ~ ra_Px89(X0,X1)
| ~ cC52xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f138_sk]) ).
fof(f268,axiom,
cC52xcomp(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_268) ).
fof(f268_nnf,plain,
cC52xcomp(iV21029),
inference(nnf_transformation,[status(thm)],[f268]) ).
cnf(c534,plain,
cC52xcomp(iV21029),
inference(cnf_transformation,[status(esa)],[f268_nnf]) ).
cnf(p741,plain,
~ ra_Px89(iV21029,X0),
inference(resolution,[status(thm)],[c334,c534]) ).
cnf(p1238,plain,
cC50(iV21029),
inference(resolution,[status(thm)],[p1233,p741]) ).
fof(f105,axiom,
! [X] :
( cC26(X)
<=> ( cC2xcomp(X)
& cC24xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_105) ).
fof(f105_nnf,plain,
! [X] :
( ( ~ cC2xcomp(X)
| ~ cC24xcomp(X)
| cC26(X) )
& ( ( cC2xcomp(X)
& cC24xcomp(X) )
| ~ cC26(X) ) ),
inference(nnf_transformation,[status(thm)],[f105]) ).
fof(f105_sk,plain,
! [X] :
( ( ~ cC2xcomp(X)
| ~ cC24xcomp(X)
| cC26(X) )
& ( ( cC2xcomp(X)
& cC24xcomp(X) )
| ~ cC26(X) ) ),
inference(skolemisation,[status(esa)],[f105_nnf]) ).
cnf(c256,plain,
( ~ cC2xcomp(X0)
| ~ cC24xcomp(X0)
| cC26(X0) ),
inference(cnf_transformation,[status(esa)],[f105_sk]) ).
fof(f103,axiom,
! [X] :
( cC24xcomp(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_103) ).
fof(f103_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px5(X,Y)
| cC24xcomp(X) )
& ( ! [Y] : ~ ra_Px5(X,Y)
| ~ cC24xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f103]) ).
fof(f103_sk,plain,
! [X,Y] :
( ( ra_Px5(X,sk76(X))
| cC24xcomp(X) )
& ( ~ ra_Px5(X,Y)
| ~ cC24xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk76])],[f103_nnf]) ).
cnf(c251,plain,
( ra_Px5(X0,sk76(X0))
| cC24xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
fof(f101,axiom,
! [X] :
( cC24(X)
<=> ? [Y0] : ra_Px5(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_101) ).
fof(f101_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px5(X,Y0)
| cC24(X) )
& ( ? [Y0] : ra_Px5(X,Y0)
| ~ cC24(X) ) ),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
! [X,Y0] :
( ( ~ ra_Px5(X,Y0)
| cC24(X) )
& ( ra_Px5(X,sk74(X))
| ~ cC24(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk74])],[f101_nnf]) ).
cnf(c246,plain,
( ~ ra_Px5(X0,X1)
| cC24(X0) ),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(p932,plain,
( cC24(X0)
| cC24xcomp(X0) ),
inference(resolution,[status(thm)],[c251,c246]) ).
cnf(p1089,plain,
( cC24(X0)
| ~ cC2xcomp(X0)
| cC26(X0) ),
inference(resolution,[status(thm)],[c256,p932]) ).
fof(f237,axiom,
cC2xcomp(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_237) ).
fof(f237_nnf,plain,
cC2xcomp(iV21027),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c503,plain,
cC2xcomp(iV21027),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p1157,plain,
( cC24(iV21027)
| cC26(iV21027) ),
inference(resolution,[status(thm)],[p1089,c503]) ).
fof(f104,axiom,
! [X] :
( cC26(X)
<=> ? [Y0] : ra_Px92(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_104) ).
fof(f104_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px92(X,Y0)
| cC26(X) )
& ( ? [Y0] : ra_Px92(X,Y0)
| ~ cC26(X) ) ),
inference(nnf_transformation,[status(thm)],[f104]) ).
fof(f104_sk,plain,
! [X,Y0] :
( ( ~ ra_Px92(X,Y0)
| cC26(X) )
& ( ra_Px92(X,sk77(X))
| ~ cC26(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk77])],[f104_nnf]) ).
cnf(c252,plain,
( ra_Px92(X0,sk77(X0))
| ~ cC26(X0) ),
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
cnf(p1164,plain,
( ra_Px92(iV21027,sk77(iV21027))
| cC24(iV21027) ),
inference(resolution,[status(thm)],[p1157,c252]) ).
fof(f106,axiom,
! [X] :
( cC26xcomp(X)
<=> ~ ? [Y] : ra_Px92(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_106) ).
fof(f106_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px92(X,Y)
| cC26xcomp(X) )
& ( ! [Y] : ~ ra_Px92(X,Y)
| ~ cC26xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f106]) ).
fof(f106_sk,plain,
! [X,Y] :
( ( ra_Px92(X,sk78(X))
| cC26xcomp(X) )
& ( ~ ra_Px92(X,Y)
| ~ cC26xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk78])],[f106_nnf]) ).
cnf(c257,plain,
( ~ ra_Px92(X0,X1)
| ~ cC26xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f106_sk]) ).
fof(f242,axiom,
cC26xcomp(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_242) ).
fof(f242_nnf,plain,
cC26xcomp(iV21027),
inference(nnf_transformation,[status(thm)],[f242]) ).
cnf(c508,plain,
cC26xcomp(iV21027),
inference(cnf_transformation,[status(esa)],[f242_nnf]) ).
cnf(p730,plain,
~ ra_Px92(iV21027,X0),
inference(resolution,[status(thm)],[c257,c508]) ).
cnf(p1170,plain,
cC24(iV21027),
inference(resolution,[status(thm)],[p1164,p730]) ).
fof(f114,axiom,
! [X] :
( cC32(X)
<=> ( cC30xcomp(X)
& cC2xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_114) ).
fof(f114_nnf,plain,
! [X] :
( ( ~ cC30xcomp(X)
| ~ cC2xcomp(X)
| cC32(X) )
& ( ( cC30xcomp(X)
& cC2xcomp(X) )
| ~ cC32(X) ) ),
inference(nnf_transformation,[status(thm)],[f114]) ).
fof(f114_sk,plain,
! [X] :
( ( ~ cC30xcomp(X)
| ~ cC2xcomp(X)
| cC32(X) )
& ( ( cC30xcomp(X)
& cC2xcomp(X) )
| ~ cC32(X) ) ),
inference(skolemisation,[status(esa)],[f114_nnf]) ).
cnf(c277,plain,
( ~ cC30xcomp(X0)
| ~ cC2xcomp(X0)
| cC32(X0) ),
inference(cnf_transformation,[status(esa)],[f114_sk]) ).
cnf(p1090,plain,
( ~ cC30xcomp(iV21027)
| cC32(iV21027) ),
inference(resolution,[status(thm)],[c277,c503]) ).
fof(f112,axiom,
! [X] :
( cC30xcomp(X)
<=> ~ ? [Y] : ra_Px8(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_112) ).
fof(f112_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px8(X,Y)
| cC30xcomp(X) )
& ( ! [Y] : ~ ra_Px8(X,Y)
| ~ cC30xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f112]) ).
fof(f112_sk,plain,
! [X,Y] :
( ( ra_Px8(X,sk84(X))
| cC30xcomp(X) )
& ( ~ ra_Px8(X,Y)
| ~ cC30xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk84])],[f112_nnf]) ).
cnf(c272,plain,
( ra_Px8(X0,sk84(X0))
| cC30xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f112_sk]) ).
fof(f110,axiom,
! [X] :
( cC30(X)
<=> ? [Y0] : ra_Px8(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_110) ).
fof(f110_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px8(X,Y0)
| cC30(X) )
& ( ? [Y0] : ra_Px8(X,Y0)
| ~ cC30(X) ) ),
inference(nnf_transformation,[status(thm)],[f110]) ).
fof(f110_sk,plain,
! [X,Y0] :
( ( ~ ra_Px8(X,Y0)
| cC30(X) )
& ( ra_Px8(X,sk82(X))
| ~ cC30(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk82])],[f110_nnf]) ).
cnf(c267,plain,
( ~ ra_Px8(X0,X1)
| cC30(X0) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(p935,plain,
( cC30(X0)
| cC30xcomp(X0) ),
inference(resolution,[status(thm)],[c272,c267]) ).
cnf(p1096,plain,
( cC30(iV21027)
| cC32(iV21027) ),
inference(resolution,[status(thm)],[p1090,p935]) ).
fof(f113,axiom,
! [X] :
( cC32(X)
<=> ~ ? [Y] : ra_Px91(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
fof(f113_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px91(X,Y)
| cC32(X) )
& ( ! [Y] : ~ ra_Px91(X,Y)
| ~ cC32(X) ) ),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [X,Y] :
( ( ra_Px91(X,sk85(X))
| cC32(X) )
& ( ~ ra_Px91(X,Y)
| ~ cC32(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk85])],[f113_nnf]) ).
cnf(c273,plain,
( ~ ra_Px91(X0,X1)
| ~ cC32(X0) ),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(p1100,plain,
( ~ ra_Px91(iV21027,X0)
| cC30(iV21027) ),
inference(resolution,[status(thm)],[p1096,c273]) ).
fof(f115,axiom,
! [X] :
( cC32xcomp(X)
<=> ? [Y0] : ra_Px91(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_115) ).
fof(f115_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px91(X,Y0)
| cC32xcomp(X) )
& ( ? [Y0] : ra_Px91(X,Y0)
| ~ cC32xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
! [X,Y0] :
( ( ~ ra_Px91(X,Y0)
| cC32xcomp(X) )
& ( ra_Px91(X,sk86(X))
| ~ cC32xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk86])],[f115_nnf]) ).
cnf(c278,plain,
( ra_Px91(X0,sk86(X0))
| ~ cC32xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
fof(f250,axiom,
cC32xcomp(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_250) ).
fof(f250_nnf,plain,
cC32xcomp(iV21027),
inference(nnf_transformation,[status(thm)],[f250]) ).
cnf(c516,plain,
cC32xcomp(iV21027),
inference(cnf_transformation,[status(esa)],[f250_nnf]) ).
cnf(p937,plain,
ra_Px91(iV21027,sk86(iV21027)),
inference(resolution,[status(thm)],[c278,c516]) ).
cnf(p1104,plain,
cC30(iV21027),
inference(resolution,[status(thm)],[p1100,p937]) ).
fof(f186,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_186) ).
fof(f186_nnf,plain,
! [X] :
( ( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [X] :
( ( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c451,plain,
( cC180(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
fof(f221,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_221) ).
fof(f221_nnf,plain,
cTEST(iV21026),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c487,plain,
cTEST(iV21026),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p666,plain,
cC180(iV21026),
inference(resolution,[status(thm)],[c451,c487]) ).
fof(f96,axiom,
! [X] :
( cC180(X)
<=> ( cC178xcomp(X)
& cC174(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(f96_nnf,plain,
! [X] :
( ( ~ cC178xcomp(X)
| ~ cC174(X)
| cC180(X) )
& ( ( cC178xcomp(X)
& cC174(X) )
| ~ cC180(X) ) ),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [X] :
( ( ~ cC178xcomp(X)
| ~ cC174(X)
| cC180(X) )
& ( ( cC178xcomp(X)
& cC174(X) )
| ~ cC180(X) ) ),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c232,plain,
( cC174(X0)
| ~ cC180(X0) ),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(p667,plain,
cC174(iV21026),
inference(resolution,[status(thm)],[p666,c232]) ).
fof(f87,axiom,
! [X] :
( cC174(X)
<=> ( cC168(X)
& cC172xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
fof(f87_nnf,plain,
! [X] :
( ( ~ cC168(X)
| ~ cC172xcomp(X)
| cC174(X) )
& ( ( cC168(X)
& cC172xcomp(X) )
| ~ cC174(X) ) ),
inference(nnf_transformation,[status(thm)],[f87]) ).
fof(f87_sk,plain,
! [X] :
( ( ~ cC168(X)
| ~ cC172xcomp(X)
| cC174(X) )
& ( ( cC168(X)
& cC172xcomp(X) )
| ~ cC174(X) ) ),
inference(skolemisation,[status(esa)],[f87_nnf]) ).
cnf(c212,plain,
( cC168(X0)
| ~ cC174(X0) ),
inference(cnf_transformation,[status(esa)],[f87_sk]) ).
cnf(p677,plain,
cC168(iV21026),
inference(resolution,[status(thm)],[p667,c212]) ).
cnf(c450,plain,
( cC158(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(p622,plain,
cC158(iV21026),
inference(resolution,[status(thm)],[c450,c487]) ).
fof(f66,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f66_nnf,plain,
! [X] :
( ( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [X] :
( ( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c161,plain,
( cC156(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p624,plain,
cC156(iV21026),
inference(resolution,[status(thm)],[p622,c161]) ).
fof(f65,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f65_nnf,plain,
! [X] :
( ( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X] :
( ( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c158,plain,
( cC138(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(p628,plain,
cC138(iV21026),
inference(resolution,[status(thm)],[p624,c158]) ).
fof(f43,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(f43_nnf,plain,
! [X] :
( ( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [X] :
( ( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c104,plain,
( cC134(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p632,plain,
cC134(iV21026),
inference(resolution,[status(thm)],[p628,c104]) ).
fof(f41,axiom,
! [X] :
( cC134(X)
<=> ( cC132(X)
& cC116(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(f41_nnf,plain,
! [X] :
( ( ~ cC132(X)
| ~ cC116(X)
| cC134(X) )
& ( ( cC132(X)
& cC116(X) )
| ~ cC134(X) ) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X] :
( ( ~ cC132(X)
| ~ cC116(X)
| cC134(X) )
& ( ( cC132(X)
& cC116(X) )
| ~ cC134(X) ) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c98,plain,
( cC116(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p635,plain,
cC116(iV21026),
inference(resolution,[status(thm)],[p632,c98]) ).
fof(f18,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f18_nnf,plain,
! [X] :
( ( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X] :
( ( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c44,plain,
( cC112(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p637,plain,
cC112(iV21026),
inference(resolution,[status(thm)],[p635,c44]) ).
fof(f16,axiom,
! [X] :
( cC112(X)
<=> ( cC90(X)
& cC110(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_16) ).
fof(f16_nnf,plain,
! [X] :
( ( ~ cC90(X)
| ~ cC110(X)
| cC112(X) )
& ( ( cC90(X)
& cC110(X) )
| ~ cC112(X) ) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X] :
( ( ~ cC90(X)
| ~ cC110(X)
| cC112(X) )
& ( ( cC90(X)
& cC110(X) )
| ~ cC112(X) ) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c39,plain,
( cC90(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p640,plain,
cC90(iV21026),
inference(resolution,[status(thm)],[p637,c39]) ).
fof(f174,axiom,
! [X] :
( cC90(X)
<=> ( cC88(X)
& cC86(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(f174_nnf,plain,
! [X] :
( ( ~ cC88(X)
| ~ cC86(X)
| cC90(X) )
& ( ( cC88(X)
& cC86(X) )
| ~ cC90(X) ) ),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
! [X] :
( ( ~ cC88(X)
| ~ cC86(X)
| cC90(X) )
& ( ( cC88(X)
& cC86(X) )
| ~ cC90(X) ) ),
inference(skolemisation,[status(esa)],[f174_nnf]) ).
cnf(c422,plain,
( cC86(X0)
| ~ cC90(X0) ),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
cnf(p642,plain,
cC86(iV21026),
inference(resolution,[status(thm)],[p640,c422]) ).
fof(f172,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_172) ).
fof(f172_nnf,plain,
! [X] :
( ( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
! [X] :
( ( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(skolemisation,[status(esa)],[f172_nnf]) ).
cnf(c417,plain,
( cC82(X0)
| ~ cC86(X0) ),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(p649,plain,
cC82(iV21026),
inference(resolution,[status(thm)],[p642,c417]) ).
fof(f170,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& cC64(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_170) ).
fof(f170_nnf,plain,
! [X] :
( ( ~ cC80(X)
| ~ cC64(X)
| cC82(X) )
& ( ( cC80(X)
& cC64(X) )
| ~ cC82(X) ) ),
inference(nnf_transformation,[status(thm)],[f170]) ).
fof(f170_sk,plain,
! [X] :
( ( ~ cC80(X)
| ~ cC64(X)
| cC82(X) )
& ( ( cC80(X)
& cC64(X) )
| ~ cC82(X) ) ),
inference(skolemisation,[status(esa)],[f170_nnf]) ).
cnf(c412,plain,
( cC64(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
cnf(p650,plain,
cC64(iV21026),
inference(resolution,[status(thm)],[p649,c412]) ).
fof(f148,axiom,
! [X] :
( cC64(X)
<=> ( cC62(X)
& cC60(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_148) ).
fof(f148_nnf,plain,
! [X] :
( ( ~ cC62(X)
| ~ cC60(X)
| cC64(X) )
& ( ( cC62(X)
& cC60(X) )
| ~ cC64(X) ) ),
inference(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [X] :
( ( ~ cC62(X)
| ~ cC60(X)
| cC64(X) )
& ( ( cC62(X)
& cC60(X) )
| ~ cC64(X) ) ),
inference(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c358,plain,
( cC60(X0)
| ~ cC64(X0) ),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(p652,plain,
cC60(iV21026),
inference(resolution,[status(thm)],[p650,c358]) ).
fof(f146,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(f146_nnf,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c353,plain,
( cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
cnf(p654,plain,
cC58(iV21026),
inference(resolution,[status(thm)],[p652,c353]) ).
fof(f143,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_143) ).
fof(f143_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c346,plain,
( cC56(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
cnf(p656,plain,
cC56(iV21026),
inference(resolution,[status(thm)],[p654,c346]) ).
cnf(c38,plain,
( cC110(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p639,plain,
cC110(iV21026),
inference(resolution,[status(thm)],[p637,c38]) ).
fof(f15,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
fof(f15_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c35,plain,
( cC108(X0)
| ~ cC110(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p641,plain,
cC108(iV21026),
inference(resolution,[status(thm)],[p639,c35]) ).
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(f342,conjecture,
( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f342_neg,negated_conjecture,
~ ( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f342]) ).
fof(f342_nnf,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f342_neg]) ).
fof(f342_sk,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ( ~ xsd_integer(sk137)
& ~ xsd_string(sk137) )
| ( xsd_integer(sk137)
& xsd_string(sk137) )
| cowlNothing(sk136)
| ~ cowlThing(sk136) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk136,sk137])],[f342_nnf]) ).
cnf(c609,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sk137)
| xsd_string(sk137)
| cowlNothing(sk136)
| ~ cowlThing(sk136) ),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(p612,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sk137)
| xsd_string(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[c0,c609]) ).
cnf(p614,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_string(sk137)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[c3,p612]) ).
cnf(p615,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(factoring,[status(thm)],[p614]) ).
cnf(p643,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p641,p615]) ).
fof(f122,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_122) ).
fof(f122_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC40(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC40(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c297,plain,
( ~ cTOP(X0)
| cC40(X0) ),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
fof(f190,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_190) ).
fof(f190_nnf,plain,
cTOP(iV21026),
inference(nnf_transformation,[status(thm)],[f190]) ).
cnf(c456,plain,
cTOP(iV21026),
inference(cnf_transformation,[status(esa)],[f190_nnf]) ).
cnf(p618,plain,
cC40(iV21026),
inference(resolution,[status(thm)],[c297,c456]) ).
cnf(p644,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p643,p618]) ).
fof(f42,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_42) ).
fof(f42_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC136(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC136(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c102,plain,
( ~ cTOP(X0)
| cC136(X0) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p617,plain,
cC136(iV21026),
inference(resolution,[status(thm)],[c102,c456]) ).
cnf(p645,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p644,p617]) ).
cnf(c160,plain,
( cC22(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p623,plain,
cC22(iV21026),
inference(resolution,[status(thm)],[p622,c160]) ).
fof(f100,axiom,
! [X] :
( cC22(X)
<=> ( cC16(X)
& cC20(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(f100_nnf,plain,
! [X] :
( ( ~ cC16(X)
| ~ cC20(X)
| cC22(X) )
& ( ( cC16(X)
& cC20(X) )
| ~ cC22(X) ) ),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [X] :
( ( ~ cC16(X)
| ~ cC20(X)
| cC22(X) )
& ( ( cC16(X)
& cC20(X) )
| ~ cC22(X) ) ),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c243,plain,
( cC16(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(p626,plain,
cC16(iV21026),
inference(resolution,[status(thm)],[p623,c243]) ).
fof(f67,axiom,
! [X] :
( cC16(X)
<=> ( cC14(X)
& cC10(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(f67_nnf,plain,
! [X] :
( ( ~ cC14(X)
| ~ cC10(X)
| cC16(X) )
& ( ( cC14(X)
& cC10(X) )
| ~ cC16(X) ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [X] :
( ( ~ cC14(X)
| ~ cC10(X)
| cC16(X) )
& ( ( cC14(X)
& cC10(X) )
| ~ cC16(X) ) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c163,plain,
( cC10(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p629,plain,
cC10(iV21026),
inference(resolution,[status(thm)],[p626,c163]) ).
cnf(p646,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p645,p629]) ).
cnf(p647,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p646,p640]) ).
cnf(p648,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p647,c0]) ).
cnf(p657,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p654,p648]) ).
cnf(p659,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p656,p657]) ).
cnf(p660,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p659,p622]) ).
cnf(p661,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p660,p639]) ).
cnf(p662,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p661,p623]) ).
cnf(p663,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p662,p652]) ).
cnf(c157,plain,
( cC154(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(p627,plain,
cC154(iV21026),
inference(resolution,[status(thm)],[p624,c157]) ).
cnf(p664,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p663,p627]) ).
cnf(p668,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p666,p664]) ).
cnf(c413,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
cnf(p651,plain,
cC80(iV21026),
inference(resolution,[status(thm)],[p649,c413]) ).
fof(f169,axiom,
! [X] :
( cC80(X)
<=> ( cTOP(X)
& cC78(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_169) ).
fof(f169_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC78(X)
| cC80(X) )
& ( ( cTOP(X)
& cC78(X) )
| ~ cC80(X) ) ),
inference(nnf_transformation,[status(thm)],[f169]) ).
fof(f169_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC78(X)
| cC80(X) )
& ( ( cTOP(X)
& cC78(X) )
| ~ cC80(X) ) ),
inference(skolemisation,[status(esa)],[f169_nnf]) ).
cnf(c409,plain,
( cC78(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[status(esa)],[f169_sk]) ).
cnf(p653,plain,
cC78(iV21026),
inference(resolution,[status(thm)],[p651,c409]) ).
cnf(p669,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p668,p653]) ).
cnf(p670,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p669,p626]) ).
cnf(c99,plain,
( cC132(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p636,plain,
cC132(iV21026),
inference(resolution,[status(thm)],[p632,c99]) ).
cnf(p671,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p670,p636]) ).
fof(f17,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
fof(f17_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC114(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC114(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c42,plain,
( ~ cTOP(X0)
| cC114(X0) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p616,plain,
cC114(iV21026),
inference(resolution,[status(thm)],[c42,c456]) ).
cnf(p672,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p671,p616]) ).
cnf(c242,plain,
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(p625,plain,
cC20(iV21026),
inference(resolution,[status(thm)],[p623,c242]) ).
cnf(p673,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p672,p625]) ).
fof(f171,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_171) ).
fof(f171_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC84(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(nnf_transformation,[status(thm)],[f171]) ).
fof(f171_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC84(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(skolemisation,[status(esa)],[f171_nnf]) ).
cnf(c416,plain,
( ~ cTOP(X0)
| cC84(X0) ),
inference(cnf_transformation,[status(esa)],[f171_sk]) ).
cnf(p620,plain,
cC84(iV21026),
inference(resolution,[status(thm)],[c416,c456]) ).
cnf(p674,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p673,p620]) ).
cnf(c354,plain,
( cC42(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
cnf(p655,plain,
cC42(iV21026),
inference(resolution,[status(thm)],[p652,c354]) ).
fof(f123,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(f123_nnf,plain,
! [X] :
( ( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [X] :
( ( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c299,plain,
( cC38(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(p658,plain,
cC38(iV21026),
inference(resolution,[status(thm)],[p655,c299]) ).
cnf(p675,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p674,p658]) ).
cnf(p676,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p675,p628]) ).
cnf(p678,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p667,p676]) ).
fof(f147,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_147) ).
fof(f147_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c357,plain,
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(p619,plain,
cC62(iV21026),
inference(resolution,[status(thm)],[c357,c456]) ).
cnf(p679,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p678,p619]) ).
fof(f2,axiom,
! [X] :
( cC10(X)
<=> ( cC4(X)
& cC8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f2_nnf,plain,
! [X] :
( ( ~ cC4(X)
| ~ cC8(X)
| cC10(X) )
& ( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] :
( ( ~ cC4(X)
| ~ cC8(X)
| cC10(X) )
& ( ( cC4(X)
& cC8(X) )
| ~ cC10(X) ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c4,plain,
( cC8(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p633,plain,
cC8(iV21026),
inference(resolution,[status(thm)],[p629,c4]) ).
cnf(p680,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p679,p633]) ).
fof(f120,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f120_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c290,plain,
( cC36(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(p665,plain,
cC36(iV21026),
inference(resolution,[status(thm)],[p658,c290]) ).
cnf(p681,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p680,p665]) ).
cnf(p682,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p681,p637]) ).
cnf(p683,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p682,p650]) ).
cnf(p684,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p683,p635]) ).
cnf(p685,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p684,p649]) ).
cnf(c164,plain,
( cC14(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p630,plain,
cC14(iV21026),
inference(resolution,[status(thm)],[p626,c164]) ).
cnf(p686,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p685,p630]) ).
fof(f64,axiom,
! [X] :
( cC154(X)
<=> ( cTOP(X)
& cC152(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(f64_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC152(X)
| cC154(X) )
& ( ( cTOP(X)
& cC152(X) )
| ~ cC154(X) ) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC152(X)
| cC154(X) )
& ( ( cTOP(X)
& cC152(X) )
| ~ cC154(X) ) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c154,plain,
( cC152(X0)
| ~ cC154(X0) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(p631,plain,
cC152(iV21026),
inference(resolution,[status(thm)],[p627,c154]) ).
cnf(p687,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p686,p631]) ).
cnf(p688,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p687,p651]) ).
fof(f173,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_173) ).
fof(f173_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC88(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(nnf_transformation,[status(thm)],[f173]) ).
fof(f173_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC88(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(skolemisation,[status(esa)],[f173_nnf]) ).
cnf(c421,plain,
( ~ cTOP(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
cnf(p621,plain,
cC88(iV21026),
inference(resolution,[status(thm)],[c421,c456]) ).
cnf(p689,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p688,p621]) ).
fof(f40,axiom,
! [X] :
( cC132(X)
<=> ( cTOP(X)
& cC130(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(f40_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC130(X)
| cC132(X) )
& ( ( cTOP(X)
& cC130(X) )
| ~ cC132(X) ) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC130(X)
| cC132(X) )
& ( ( cTOP(X)
& cC130(X) )
| ~ cC132(X) ) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c95,plain,
( cC130(X0)
| ~ cC132(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p638,plain,
cC130(iV21026),
inference(resolution,[status(thm)],[p636,c95]) ).
cnf(p690,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p689,p638]) ).
cnf(p691,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p677,p690]) ).
cnf(c5,plain,
( cC4(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p634,plain,
cC4(iV21026),
inference(resolution,[status(thm)],[p629,c5]) ).
cnf(p692,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p691,p634]) ).
cnf(p693,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p692,p632]) ).
cnf(p694,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p693,p655]) ).
cnf(p695,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p694,p624]) ).
cnf(p696,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p695,p642]) ).
cnf(p1105,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1104,p696]) ).
cnf(p1109,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1105,c0]) ).
cnf(p1174,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1170,p1109]) ).
cnf(p1242,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1238,p1174]) ).
fof(f128,axiom,
! [X] :
( cC46(X)
<=> ( cC12xcomp(X)
& cC44xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_128) ).
fof(f128_nnf,plain,
! [X] :
( ( ~ cC12xcomp(X)
| ~ cC44xcomp(X)
| cC46(X) )
& ( ( cC12xcomp(X)
& cC44xcomp(X) )
| ~ cC46(X) ) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [X] :
( ( ~ cC12xcomp(X)
| ~ cC44xcomp(X)
| cC46(X) )
& ( ( cC12xcomp(X)
& cC44xcomp(X) )
| ~ cC46(X) ) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c312,plain,
( ~ cC12xcomp(X0)
| ~ cC44xcomp(X0)
| cC46(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f124,axiom,
! [X] :
( cC44(X)
<=> ~ ? [Y] : ra_Px13(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_124) ).
fof(f124_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px13(X,Y)
| cC44(X) )
& ( ! [Y] : ~ ra_Px13(X,Y)
| ~ cC44(X) ) ),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [X,Y] :
( ( ra_Px13(X,sk91(X))
| cC44(X) )
& ( ~ ra_Px13(X,Y)
| ~ cC44(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk91])],[f124_nnf]) ).
cnf(c302,plain,
( ra_Px13(X0,sk91(X0))
| cC44(X0) ),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
fof(f126,axiom,
! [X] :
( cC44xcomp(X)
<=> ? [Y0] : ra_Px13(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_126) ).
fof(f126_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px13(X,Y0)
| cC44xcomp(X) )
& ( ? [Y0] : ra_Px13(X,Y0)
| ~ cC44xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [X,Y0] :
( ( ~ ra_Px13(X,Y0)
| cC44xcomp(X) )
& ( ra_Px13(X,sk93(X))
| ~ cC44xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk93])],[f126_nnf]) ).
cnf(c307,plain,
( ~ ra_Px13(X0,X1)
| cC44xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(p979,plain,
( cC44xcomp(X0)
| cC44(X0) ),
inference(resolution,[status(thm)],[c302,c307]) ).
cnf(p1122,plain,
( cC44(X0)
| ~ cC12xcomp(X0)
| cC46(X0) ),
inference(resolution,[status(thm)],[c312,p979]) ).
cnf(p1196,plain,
( cC44(iV21029)
| cC46(iV21029) ),
inference(resolution,[status(thm)],[p1122,c531]) ).
fof(f127,axiom,
! [X] :
( cC46(X)
<=> ? [Y0] : ra_Px90(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_127) ).
fof(f127_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px90(X,Y0)
| cC46(X) )
& ( ? [Y0] : ra_Px90(X,Y0)
| ~ cC46(X) ) ),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [X,Y0] :
( ( ~ ra_Px90(X,Y0)
| cC46(X) )
& ( ra_Px90(X,sk94(X))
| ~ cC46(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk94])],[f127_nnf]) ).
cnf(c308,plain,
( ra_Px90(X0,sk94(X0))
| ~ cC46(X0) ),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(p1203,plain,
( ra_Px90(iV21029,sk94(iV21029))
| cC44(iV21029) ),
inference(resolution,[status(thm)],[p1196,c308]) ).
fof(f129,axiom,
! [X] :
( cC46xcomp(X)
<=> ~ ? [Y] : ra_Px90(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_129) ).
fof(f129_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px90(X,Y)
| cC46xcomp(X) )
& ( ! [Y] : ~ ra_Px90(X,Y)
| ~ cC46xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [X,Y] :
( ( ra_Px90(X,sk95(X))
| cC46xcomp(X) )
& ( ~ ra_Px90(X,Y)
| ~ cC46xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk95])],[f129_nnf]) ).
cnf(c313,plain,
( ~ ra_Px90(X0,X1)
| ~ cC46xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
fof(f272,axiom,
cC46xcomp(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_272) ).
fof(f272_nnf,plain,
cC46xcomp(iV21029),
inference(nnf_transformation,[status(thm)],[f272]) ).
cnf(c538,plain,
cC46xcomp(iV21029),
inference(cnf_transformation,[status(esa)],[f272_nnf]) ).
cnf(p737,plain,
~ ra_Px90(iV21029,X0),
inference(resolution,[status(thm)],[c313,c538]) ).
cnf(p1208,plain,
cC44(iV21029),
inference(resolution,[status(thm)],[p1203,p737]) ).
cnf(p1243,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1242,p1208]) ).
cnf(p1244,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1243,c0]) ).
cnf(p1274,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1270,p1244]) ).
fof(f153,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC18xcomp(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_153) ).
fof(f153_nnf,plain,
! [X] :
( ( ~ cC66xcomp(X)
| ~ cC18xcomp(X)
| cC68(X) )
& ( ( cC66xcomp(X)
& cC18xcomp(X) )
| ~ cC68(X) ) ),
inference(nnf_transformation,[status(thm)],[f153]) ).
fof(f153_sk,plain,
! [X] :
( ( ~ cC66xcomp(X)
| ~ cC18xcomp(X)
| cC68(X) )
& ( ( cC66xcomp(X)
& cC18xcomp(X) )
| ~ cC68(X) ) ),
inference(skolemisation,[status(esa)],[f153_nnf]) ).
cnf(c372,plain,
( ~ cC66xcomp(X0)
| ~ cC18xcomp(X0)
| cC68(X0) ),
inference(cnf_transformation,[status(esa)],[f153_sk]) ).
cnf(p1125,plain,
( ~ cC66xcomp(iV21030)
| cC68(iV21030) ),
inference(resolution,[status(thm)],[c372,c559]) ).
fof(f151,axiom,
! [X] :
( cC66xcomp(X)
<=> ~ ? [Y] : ra_Px21(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_151) ).
fof(f151_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px21(X,Y)
| cC66xcomp(X) )
& ( ! [Y] : ~ ra_Px21(X,Y)
| ~ cC66xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f151]) ).
fof(f151_sk,plain,
! [X,Y] :
( ( ra_Px21(X,sk111(X))
| cC66xcomp(X) )
& ( ~ ra_Px21(X,Y)
| ~ cC66xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk111])],[f151_nnf]) ).
cnf(c367,plain,
( ra_Px21(X0,sk111(X0))
| cC66xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
fof(f149,axiom,
! [X] :
( cC66(X)
<=> ? [Y0] : ra_Px21(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_149) ).
fof(f149_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px21(X,Y0)
| cC66(X) )
& ( ? [Y0] : ra_Px21(X,Y0)
| ~ cC66(X) ) ),
inference(nnf_transformation,[status(thm)],[f149]) ).
fof(f149_sk,plain,
! [X,Y0] :
( ( ~ ra_Px21(X,Y0)
| cC66(X) )
& ( ra_Px21(X,sk109(X))
| ~ cC66(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk109])],[f149_nnf]) ).
cnf(c362,plain,
( ~ ra_Px21(X0,X1)
| cC66(X0) ),
inference(cnf_transformation,[status(esa)],[f149_sk]) ).
cnf(p995,plain,
( cC66(X0)
| cC66xcomp(X0) ),
inference(resolution,[status(thm)],[c367,c362]) ).
cnf(p1127,plain,
( cC66(iV21030)
| cC68(iV21030) ),
inference(resolution,[status(thm)],[p1125,p995]) ).
fof(f152,axiom,
! [X] :
( cC68(X)
<=> ~ ? [Y] : ra_Px88(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_152) ).
fof(f152_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px88(X,Y)
| cC68(X) )
& ( ! [Y] : ~ ra_Px88(X,Y)
| ~ cC68(X) ) ),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [X,Y] :
( ( ra_Px88(X,sk112(X))
| cC68(X) )
& ( ~ ra_Px88(X,Y)
| ~ cC68(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk112])],[f152_nnf]) ).
cnf(c368,plain,
( ~ ra_Px88(X0,X1)
| ~ cC68(X0) ),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
cnf(p1128,plain,
( ~ ra_Px88(iV21030,X0)
| cC66(iV21030) ),
inference(resolution,[status(thm)],[p1127,c368]) ).
fof(f154,axiom,
! [X] :
( cC68xcomp(X)
<=> ? [Y0] : ra_Px88(X,Y0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_154) ).
fof(f154_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px88(X,Y0)
| cC68xcomp(X) )
& ( ? [Y0] : ra_Px88(X,Y0)
| ~ cC68xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f154]) ).
fof(f154_sk,plain,
! [X,Y0] :
( ( ~ ra_Px88(X,Y0)
| cC68xcomp(X) )
& ( ra_Px88(X,sk113(X))
| ~ cC68xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk113])],[f154_nnf]) ).
cnf(c373,plain,
( ra_Px88(X0,sk113(X0))
| ~ cC68xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f154_sk]) ).
fof(f291,axiom,
cC68xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_291) ).
fof(f291_nnf,plain,
cC68xcomp(iV21030),
inference(nnf_transformation,[status(thm)],[f291]) ).
cnf(c557,plain,
cC68xcomp(iV21030),
inference(cnf_transformation,[status(esa)],[f291_nnf]) ).
cnf(p999,plain,
ra_Px88(iV21030,sk113(iV21030)),
inference(resolution,[status(thm)],[c373,c557]) ).
cnf(p1129,plain,
cC66(iV21030),
inference(resolution,[status(thm)],[p1128,p999]) ).
cnf(p1275,plain,
( ~ cowlThing(iV21030)
| cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1274,p1129]) ).
cnf(p1276,plain,
( cowlNothing(sk136)
| xsd_string(sk137) ),
inference(resolution,[status(thm)],[p1275,c0]) ).
cnf(c610,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_string(sk137)
| xsd_integer(sk137)
| cowlNothing(sk136)
| ~ cowlThing(sk136) ),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(p613,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_string(sk137)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[c0,c610]) ).
cnf(p1277,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1276,p613]) ).
cnf(p1279,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(factoring,[status(thm)],[p1277]) ).
cnf(p1280,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1279,p641]) ).
cnf(p1281,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1280,p618]) ).
cnf(p1282,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1281,p617]) ).
cnf(p1283,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1282,p629]) ).
cnf(p1284,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1283,p640]) ).
cnf(p1285,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1284,c0]) ).
cnf(p1286,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1285,p654]) ).
cnf(p1287,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1286,p656]) ).
cnf(p1288,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1287,p622]) ).
cnf(p1289,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1288,p639]) ).
cnf(p1290,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1289,p623]) ).
cnf(p1291,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1290,p652]) ).
cnf(p1292,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1291,p627]) ).
cnf(p1293,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1292,p666]) ).
cnf(p1294,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1293,p653]) ).
cnf(p1295,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1294,p626]) ).
cnf(p1296,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1295,p636]) ).
cnf(p1297,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1296,p616]) ).
cnf(p1298,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1297,p625]) ).
cnf(p1299,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1298,p620]) ).
cnf(p1300,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1299,p658]) ).
cnf(p1301,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1300,p628]) ).
cnf(p1302,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1301,p667]) ).
cnf(p1303,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1302,p619]) ).
cnf(p1304,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1303,p633]) ).
cnf(p1305,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1304,p665]) ).
cnf(p1306,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1305,p637]) ).
cnf(p1307,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1306,p650]) ).
cnf(p1308,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1307,p635]) ).
cnf(p1309,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1308,p649]) ).
cnf(p1310,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1309,p630]) ).
cnf(p1311,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1310,p631]) ).
cnf(p1312,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1311,p651]) ).
cnf(p1313,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1312,p621]) ).
cnf(p1314,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1313,p638]) ).
cnf(p1315,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1314,p677]) ).
cnf(p1316,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1315,p634]) ).
cnf(p1317,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1316,p632]) ).
cnf(p1318,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1317,p655]) ).
cnf(p1319,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1318,p624]) ).
cnf(p1320,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1319,p642]) ).
cnf(p1321,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1320,p1104]) ).
cnf(p1322,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1321,c0]) ).
cnf(p1323,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1322,p1170]) ).
cnf(p1324,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1323,p1238]) ).
cnf(p1325,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1324,p1208]) ).
cnf(p1326,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1325,c0]) ).
cnf(p1327,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1326,p1270]) ).
cnf(p1328,plain,
( ~ cowlThing(iV21030)
| xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1327,p1129]) ).
cnf(p1329,plain,
( xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1328,c0]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1278,plain,
( ~ xsd_integer(sk137)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1276,c2]) ).
cnf(p1330,plain,
( cowlNothing(sk136)
| cowlNothing(sk136) ),
inference(resolution,[status(thm)],[p1329,p1278]) ).
cnf(p1331,plain,
cowlNothing(sk136),
inference(factoring,[status(thm)],[p1330]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1332,plain,
$false,
inference(resolution,[status(thm)],[p1331,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 19:32:33 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.34/1.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.34/1.34 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------