%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:53:20 PM UTC 2026
% Result : Theorem 5.81s 11.27s
% Output : Proof 5.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 129
% Number of leaves : 58
% Syntax : Number of formulae : 408 ( 106 unt; 0 def)
% Number of atoms : 4162 ( 0 equ)
% Maximal formula atoms : 56 ( 10 avg)
% Number of connectives : 7050 (3296 ~;3428 |; 285 &)
% ( 41 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 55 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 62 ( 61 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-1 aty)
% Number of variables : 203 ( 2 sgn 134 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f73,axiom,
! [X] :
( cC74(X)
<=> ( ~ cC72(X)
& ~ cC18(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f73_nnf,plain,
! [X] :
( ( cC72(X)
| cC18(X)
| cC74(X) )
& ( ( ~ cC72(X)
& ~ cC18(X) )
| ~ cC74(X) ) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [X] :
( ( cC72(X)
| cC18(X)
| cC74(X) )
& ( ( ~ cC72(X)
& ~ cC18(X) )
| ~ cC74(X) ) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c215,plain,
( cC72(X0)
| cC18(X0)
| cC74(X0) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
fof(f192,axiom,
~ cC74(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_192) ).
fof(f192_nnf,plain,
~ cC74(iV21030),
inference(nnf_transformation,[status(thm)],[f192]) ).
fof(f192_sk,plain,
~ cC74(iV21030),
inference(skolemisation,[status(esa)],[f192_nnf]) ).
cnf(c358,plain,
~ cC74(iV21030),
inference(cnf_transformation,[status(esa)],[f192_sk]) ).
cnf(p1296,plain,
( cC72(iV21030)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[c215,c358]) ).
fof(f69,axiom,
! [X] :
( cC66(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_69) ).
fof(f69_nnf,plain,
! [X] :
( ( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC66(X) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC66(X) ) ),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [X,Y] :
( ( cC2(Y)
| ~ rR1(X,Y)
| cC66(X) )
& ( ( ~ cC2(sk29(X))
& rR1(X,sk29(X)) )
| ~ cC66(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk29])],[f69_nnf]) ).
cnf(c203,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC66(X0) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
fof(f209,axiom,
rR1(iV21030,iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_209) ).
fof(f209_nnf,plain,
rR1(iV21030,iV21032),
inference(nnf_transformation,[status(thm)],[f209]) ).
cnf(c375,plain,
rR1(iV21030,iV21032),
inference(cnf_transformation,[status(esa)],[f209_nnf]) ).
cnf(p1209,plain,
( cC2(iV21032)
| cC66(iV21030) ),
inference(resolution,[status(thm)],[c203,c375]) ).
fof(f62,axiom,
! [X] :
( cC52(X)
<=> ( ~ cC50(X)
& ~ cC12(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_62) ).
fof(f62_nnf,plain,
! [X] :
( ( cC50(X)
| cC12(X)
| cC52(X) )
& ( ( ~ cC50(X)
& ~ cC12(X) )
| ~ cC52(X) ) ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [X] :
( ( cC50(X)
| cC12(X)
| cC52(X) )
& ( ( ~ cC50(X)
& ~ cC12(X) )
| ~ cC52(X) ) ),
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c183,plain,
( cC50(X0)
| cC12(X0)
| cC52(X0) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
fof(f168,axiom,
~ cC52(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_168) ).
fof(f168_nnf,plain,
~ cC52(iV21029),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
~ cC52(iV21029),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c334,plain,
~ cC52(iV21029),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(p1141,plain,
( cC50(iV21029)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[c183,c334]) ).
fof(f50,axiom,
! [X] :
( cC30(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_50) ).
fof(f50_nnf,plain,
! [X] :
( ( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC30(X) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC30(X) ) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [X,Y] :
( ( cC12(Y)
| ~ rR1(X,Y)
| cC30(X) )
& ( ( ~ cC12(sk22(X))
& rR1(X,sk22(X)) )
| ~ cC30(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk22])],[f50_nnf]) ).
cnf(c148,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC30(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
fof(f153,axiom,
rR1(iV21027,iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_153) ).
fof(f153_nnf,plain,
rR1(iV21027,iV21035),
inference(nnf_transformation,[status(thm)],[f153]) ).
cnf(c319,plain,
rR1(iV21027,iV21035),
inference(cnf_transformation,[status(esa)],[f153_nnf]) ).
cnf(p867,plain,
( cC12(iV21035)
| cC30(iV21027) ),
inference(resolution,[status(thm)],[c148,c319]) ).
fof(f86,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_86) ).
fof(f86_nnf,plain,
! [X] :
( ( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(nnf_transformation,[status(thm)],[f86]) ).
fof(f86_sk,plain,
! [X] :
( ( ~ cC180(X)
| ~ cC158(X)
| cTEST(X) )
& ( ( cC180(X)
& cC158(X) )
| ~ cTEST(X) ) ),
inference(skolemisation,[status(esa)],[f86_nnf]) ).
cnf(c251,plain,
( cC180(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
fof(f89,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_89) ).
fof(f89_nnf,plain,
cTEST(iV21026),
inference(nnf_transformation,[status(thm)],[f89]) ).
cnf(c255,plain,
cTEST(iV21026),
inference(cnf_transformation,[status(esa)],[f89_nnf]) ).
cnf(p524,plain,
cC180(iV21026),
inference(resolution,[status(thm)],[c251,c255]) ).
fof(f44,axiom,
! [X] :
( cC180(X)
<=> ( cC174(X)
& ~ cC178(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_44) ).
fof(f44_nnf,plain,
! [X] :
( ( ~ cC174(X)
| cC178(X)
| cC180(X) )
& ( ( cC174(X)
& ~ cC178(X) )
| ~ cC180(X) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [X] :
( ( ~ cC174(X)
| cC178(X)
| cC180(X) )
& ( ( cC174(X)
& ~ cC178(X) )
| ~ cC180(X) ) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c129,plain,
( cC174(X0)
| ~ cC180(X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p533,plain,
cC174(iV21026),
inference(resolution,[status(thm)],[p524,c129]) ).
fof(f41,axiom,
! [X] :
( cC174(X)
<=> ( ~ cC172(X)
& cC168(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(f41_nnf,plain,
! [X] :
( ( cC172(X)
| ~ cC168(X)
| cC174(X) )
& ( ( ~ cC172(X)
& cC168(X) )
| ~ cC174(X) ) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X] :
( ( cC172(X)
| ~ cC168(X)
| cC174(X) )
& ( ( ~ cC172(X)
& cC168(X) )
| ~ cC174(X) ) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c119,plain,
( cC168(X0)
| ~ cC174(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p534,plain,
cC168(iV21026),
inference(resolution,[status(thm)],[p533,c119]) ).
cnf(c250,plain,
( cC158(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[status(esa)],[f86_sk]) ).
cnf(p468,plain,
cC158(iV21026),
inference(resolution,[status(thm)],[c250,c255]) ).
fof(f32,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_32) ).
fof(f32_nnf,plain,
! [X] :
( ( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [X] :
( ( ~ cC156(X)
| ~ cC22(X)
| cC158(X) )
& ( ( cC156(X)
& cC22(X) )
| ~ cC158(X) ) ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c93,plain,
( cC156(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p470,plain,
cC156(iV21026),
inference(resolution,[status(thm)],[p468,c93]) ).
fof(f31,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_31) ).
fof(f31_nnf,plain,
! [X] :
( ( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X] :
( ( ~ cC138(X)
| ~ cC154(X)
| cC156(X) )
& ( ( cC138(X)
& cC154(X) )
| ~ cC156(X) ) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c90,plain,
( cC138(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p474,plain,
cC138(iV21026),
inference(resolution,[status(thm)],[p470,c90]) ).
fof(f21,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
fof(f21_nnf,plain,
! [X] :
( ( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X] :
( ( ~ cC134(X)
| ~ cC136(X)
| cC138(X) )
& ( ( cC134(X)
& cC136(X) )
| ~ cC138(X) ) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c60,plain,
( cC134(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p479,plain,
cC134(iV21026),
inference(resolution,[status(thm)],[p474,c60]) ).
fof(f19,axiom,
! [X] :
( cC134(X)
<=> ( cC116(X)
& cC132(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_19) ).
fof(f19_nnf,plain,
! [X] :
( ( ~ cC116(X)
| ~ cC132(X)
| cC134(X) )
& ( ( cC116(X)
& cC132(X) )
| ~ cC134(X) ) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X] :
( ( ~ cC116(X)
| ~ cC132(X)
| cC134(X) )
& ( ( cC116(X)
& cC132(X) )
| ~ cC134(X) ) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c55,plain,
( cC116(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p492,plain,
cC116(iV21026),
inference(resolution,[status(thm)],[p479,c55]) ).
fof(f10,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_10) ).
fof(f10_nnf,plain,
! [X] :
( ( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X] :
( ( ~ cC112(X)
| ~ cC114(X)
| cC116(X) )
& ( ( cC112(X)
& cC114(X) )
| ~ cC116(X) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c28,plain,
( cC112(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p494,plain,
cC112(iV21026),
inference(resolution,[status(thm)],[p492,c28]) ).
fof(f8,axiom,
! [X] :
( cC112(X)
<=> ( cC110(X)
& cC90(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
fof(f8_nnf,plain,
! [X] :
( ( ~ cC110(X)
| ~ cC90(X)
| cC112(X) )
& ( ( cC110(X)
& cC90(X) )
| ~ cC112(X) ) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] :
( ( ~ cC110(X)
| ~ cC90(X)
| cC112(X) )
& ( ( cC110(X)
& cC90(X) )
| ~ cC112(X) ) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c22,plain,
( cC90(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p495,plain,
cC90(iV21026),
inference(resolution,[status(thm)],[p494,c22]) ).
fof(f82,axiom,
! [X] :
( cC90(X)
<=> ( cC86(X)
& cC88(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
fof(f82_nnf,plain,
! [X] :
( ( ~ cC86(X)
| ~ cC88(X)
| cC90(X) )
& ( ( cC86(X)
& cC88(X) )
| ~ cC90(X) ) ),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [X] :
( ( ~ cC86(X)
| ~ cC88(X)
| cC90(X) )
& ( ( cC86(X)
& cC88(X) )
| ~ cC90(X) ) ),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c239,plain,
( cC86(X0)
| ~ cC90(X0) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(p497,plain,
cC86(iV21026),
inference(resolution,[status(thm)],[p495,c239]) ).
fof(f80,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_80) ).
fof(f80_nnf,plain,
! [X] :
( ( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(nnf_transformation,[status(thm)],[f80]) ).
fof(f80_sk,plain,
! [X] :
( ( ~ cC84(X)
| ~ cC82(X)
| cC86(X) )
& ( ( cC84(X)
& cC82(X) )
| ~ cC86(X) ) ),
inference(skolemisation,[status(esa)],[f80_nnf]) ).
cnf(c233,plain,
( cC82(X0)
| ~ cC86(X0) ),
inference(cnf_transformation,[status(esa)],[f80_sk]) ).
cnf(p499,plain,
cC82(iV21026),
inference(resolution,[status(thm)],[p497,c233]) ).
fof(f78,axiom,
! [X] :
( cC82(X)
<=> ( cC64(X)
& cC80(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_78) ).
fof(f78_nnf,plain,
! [X] :
( ( ~ cC64(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC64(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(nnf_transformation,[status(thm)],[f78]) ).
fof(f78_sk,plain,
! [X] :
( ( ~ cC64(X)
| ~ cC80(X)
| cC82(X) )
& ( ( cC64(X)
& cC80(X) )
| ~ cC82(X) ) ),
inference(skolemisation,[status(esa)],[f78_nnf]) ).
cnf(c229,plain,
( cC64(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(p501,plain,
cC64(iV21026),
inference(resolution,[status(thm)],[p499,c229]) ).
fof(f68,axiom,
! [X] :
( cC64(X)
<=> ( cC60(X)
& cC62(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_68) ).
fof(f68_nnf,plain,
! [X] :
( ( ~ cC60(X)
| ~ cC62(X)
| cC64(X) )
& ( ( cC60(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(nnf_transformation,[status(thm)],[f68]) ).
fof(f68_sk,plain,
! [X] :
( ( ~ cC60(X)
| ~ cC62(X)
| cC64(X) )
& ( ( cC60(X)
& cC62(X) )
| ~ cC64(X) ) ),
inference(skolemisation,[status(esa)],[f68_nnf]) ).
cnf(c199,plain,
( cC60(X0)
| ~ cC64(X0) ),
inference(cnf_transformation,[status(esa)],[f68_sk]) ).
cnf(p505,plain,
cC60(iV21026),
inference(resolution,[status(thm)],[p501,c199]) ).
fof(f66,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f66_nnf,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [X] :
( ( ~ cC42(X)
| ~ cC58(X)
| cC60(X) )
& ( ( cC42(X)
& cC58(X) )
| ~ cC60(X) ) ),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c194,plain,
( cC42(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p507,plain,
cC42(iV21026),
inference(resolution,[status(thm)],[p505,c194]) ).
fof(f57,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
fof(f57_nnf,plain,
! [X] :
( ( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X] :
( ( ~ cC38(X)
| ~ cC40(X)
| cC42(X) )
& ( ( cC38(X)
& cC40(X) )
| ~ cC42(X) ) ),
inference(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c167,plain,
( cC38(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p509,plain,
cC38(iV21026),
inference(resolution,[status(thm)],[p507,c167]) ).
fof(f54,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_54) ).
fof(f54_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC36(X)
| cC38(X) )
& ( ( cTOP(X)
& cC36(X) )
| ~ cC38(X) ) ),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c158,plain,
( cC36(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(p510,plain,
cC36(iV21026),
inference(resolution,[status(thm)],[p509,c158]) ).
cnf(c92,plain,
( cC22(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p469,plain,
cC22(iV21026),
inference(resolution,[status(thm)],[p468,c92]) ).
fof(f46,axiom,
! [X] :
( cC22(X)
<=> ( cC20(X)
& cC16(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_46) ).
fof(f46_nnf,plain,
! [X] :
( ( ~ cC20(X)
| ~ cC16(X)
| cC22(X) )
& ( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
! [X] :
( ( ~ cC20(X)
| ~ cC16(X)
| cC22(X) )
& ( ( cC20(X)
& cC16(X) )
| ~ cC22(X) ) ),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c134,plain,
( cC16(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p471,plain,
cC16(iV21026),
inference(resolution,[status(thm)],[p469,c134]) ).
fof(f79,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
fof(f79_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC84(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(nnf_transformation,[status(thm)],[f79]) ).
fof(f79_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC84(X) )
& ( cTOP(X)
| ~ cC84(X) ) ),
inference(skolemisation,[status(esa)],[f79_nnf]) ).
cnf(c232,plain,
( ~ cTOP(X0)
| cC84(X0) ),
inference(cnf_transformation,[status(esa)],[f79_sk]) ).
fof(f88,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_88) ).
fof(f88_nnf,plain,
cTOP(iV21026),
inference(nnf_transformation,[status(thm)],[f88]) ).
cnf(c254,plain,
cTOP(iV21026),
inference(cnf_transformation,[status(esa)],[f88_nnf]) ).
cnf(p463,plain,
cC84(iV21026),
inference(resolution,[status(thm)],[c232,c254]) ).
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(f242,conjecture,
( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f242_neg,negated_conjecture,
~ ( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(negated_conjecture,[status(cth)],[f242]) ).
fof(f242_nnf,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [X] :
( ( ~ xsd_integer(X)
& ~ xsd_string(X) )
| ( xsd_integer(X)
& xsd_string(X) ) )
| ? [X] :
( cowlNothing(X)
| ~ cowlThing(X) ) ),
inference(nnf_transformation,[status(thm)],[f242_neg]) ).
fof(f242_sk,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ( ~ xsd_integer(sk37)
& ~ xsd_string(sk37) )
| ( xsd_integer(sk37)
& xsd_string(sk37) )
| cowlNothing(sk36)
| ~ cowlThing(sk36) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk36,sk37])],[f242_nnf]) ).
cnf(c409,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sk37)
| xsd_string(sk37)
| cowlNothing(sk36)
| ~ cowlThing(sk36) ),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(p412,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sk37)
| xsd_string(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[c0,c409]) ).
cnf(p414,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_string(sk37)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[c3,p412]) ).
cnf(p415,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(factoring,[status(thm)],[p414]) ).
cnf(p416,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p415,c0]) ).
cnf(p464,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p463,p416]) ).
cnf(p477,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p471,p464]) ).
cnf(p511,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p510,p477]) ).
cnf(p512,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p511,p507]) ).
fof(f81,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_81) ).
fof(f81_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC88(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC88(X) )
& ( cTOP(X)
| ~ cC88(X) ) ),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c237,plain,
( ~ cTOP(X0)
| cC88(X0) ),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(p465,plain,
cC88(iV21026),
inference(resolution,[status(thm)],[c237,c254]) ).
cnf(p513,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p512,p465]) ).
cnf(p514,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p513,p497]) ).
cnf(p535,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p533,p514]) ).
cnf(c135,plain,
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p472,plain,
cC20(iV21026),
inference(resolution,[status(thm)],[p469,c135]) ).
cnf(p536,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p535,p472]) ).
cnf(p537,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p536,p470]) ).
cnf(p538,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p537,p505]) ).
cnf(p539,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p538,p509]) ).
cnf(p540,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p539,p468]) ).
fof(f33,axiom,
! [X] :
( cC16(X)
<=> ( cC10(X)
& cC14(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
fof(f33_nnf,plain,
! [X] :
( ( ~ cC10(X)
| ~ cC14(X)
| cC16(X) )
& ( ( cC10(X)
& cC14(X) )
| ~ cC16(X) ) ),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [X] :
( ( ~ cC10(X)
| ~ cC14(X)
| cC16(X) )
& ( ( cC10(X)
& cC14(X) )
| ~ cC16(X) ) ),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c96,plain,
( cC10(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p476,plain,
cC10(iV21026),
inference(resolution,[status(thm)],[p471,c96]) ).
cnf(p541,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p540,p476]) ).
cnf(p542,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p541,p479]) ).
cnf(p543,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p542,p469]) ).
cnf(p544,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p534,p543]) ).
cnf(c193,plain,
( cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(p506,plain,
cC58(iV21026),
inference(resolution,[status(thm)],[p505,c193]) ).
fof(f65,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f65_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC56(X)
| cC58(X) )
& ( ( cTOP(X)
& cC56(X) )
| ~ cC58(X) ) ),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c190,plain,
( cC56(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(p508,plain,
cC56(iV21026),
inference(resolution,[status(thm)],[p506,c190]) ).
cnf(p545,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p544,p508]) ).
cnf(c228,plain,
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[status(esa)],[f78_sk]) ).
cnf(p500,plain,
cC80(iV21026),
inference(resolution,[status(thm)],[p499,c228]) ).
fof(f77,axiom,
! [X] :
( cC80(X)
<=> ( cC78(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_77) ).
fof(f77_nnf,plain,
! [X] :
( ( ~ cC78(X)
| ~ cTOP(X)
| cC80(X) )
& ( ( cC78(X)
& cTOP(X) )
| ~ cC80(X) ) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [X] :
( ( ~ cC78(X)
| ~ cTOP(X)
| cC80(X) )
& ( ( cC78(X)
& cTOP(X) )
| ~ cC80(X) ) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c226,plain,
( cC78(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(p504,plain,
cC78(iV21026),
inference(resolution,[status(thm)],[p500,c226]) ).
cnf(p546,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p545,p504]) ).
cnf(p547,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p546,p506]) ).
cnf(c89,plain,
( cC154(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(p473,plain,
cC154(iV21026),
inference(resolution,[status(thm)],[p470,c89]) ).
fof(f30,axiom,
! [X] :
( cC154(X)
<=> ( cC152(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f30_nnf,plain,
! [X] :
( ( ~ cC152(X)
| ~ cTOP(X)
| cC154(X) )
& ( ( cC152(X)
& cTOP(X) )
| ~ cC154(X) ) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X] :
( ( ~ cC152(X)
| ~ cTOP(X)
| cC154(X) )
& ( ( cC152(X)
& cTOP(X) )
| ~ cC154(X) ) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c87,plain,
( cC152(X0)
| ~ cC154(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p478,plain,
cC152(iV21026),
inference(resolution,[status(thm)],[p473,c87]) ).
cnf(p548,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p547,p478]) ).
fof(f56,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_56) ).
fof(f56_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC40(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC40(X) )
& ( cTOP(X)
| ~ cC40(X) ) ),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c165,plain,
( ~ cTOP(X0)
| cC40(X0) ),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(p451,plain,
cC40(iV21026),
inference(resolution,[status(thm)],[c165,c254]) ).
cnf(p549,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p548,p451]) ).
cnf(c54,plain,
( cC132(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p491,plain,
cC132(iV21026),
inference(resolution,[status(thm)],[p479,c54]) ).
cnf(p550,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p549,p491]) ).
fof(f18,axiom,
! [X] :
( cC132(X)
<=> ( cC130(X)
& cTOP(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f18_nnf,plain,
! [X] :
( ( ~ cC130(X)
| ~ cTOP(X)
| cC132(X) )
& ( ( cC130(X)
& cTOP(X) )
| ~ cC132(X) ) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X] :
( ( ~ cC130(X)
| ~ cTOP(X)
| cC132(X) )
& ( ( cC130(X)
& cTOP(X) )
| ~ cC132(X) ) ),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c52,plain,
( cC130(X0)
| ~ cC132(X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p493,plain,
cC130(iV21026),
inference(resolution,[status(thm)],[p491,c52]) ).
cnf(p552,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p550,p493]) ).
fof(f67,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(f67_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC62(X) )
& ( cTOP(X)
| ~ cC62(X) ) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c197,plain,
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(p454,plain,
cC62(iV21026),
inference(resolution,[status(thm)],[c197,c254]) ).
cnf(p553,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p552,p454]) ).
cnf(p554,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p553,p473]) ).
cnf(p555,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p554,p500]) ).
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(p482,plain,
cC8(iV21026),
inference(resolution,[status(thm)],[p476,c4]) ).
cnf(p556,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p555,p482]) ).
fof(f20,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_20) ).
fof(f20_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC136(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC136(X) )
& ( cTOP(X)
| ~ cC136(X) ) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c58,plain,
( ~ cTOP(X0)
| cC136(X0) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p434,plain,
cC136(iV21026),
inference(resolution,[status(thm)],[c58,c254]) ).
cnf(p557,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p556,p434]) ).
cnf(p558,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p557,p494]) ).
cnf(p559,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p558,p524]) ).
fof(f9,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
fof(f9_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| cC114(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] :
( ( ~ cTOP(X)
| cC114(X) )
& ( cTOP(X)
| ~ cC114(X) ) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c26,plain,
( ~ cTOP(X0)
| cC114(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p418,plain,
cC114(iV21026),
inference(resolution,[status(thm)],[c26,c254]) ).
cnf(p560,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p559,p418]) ).
cnf(p561,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p560,p501]) ).
cnf(c23,plain,
( cC110(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p496,plain,
cC110(iV21026),
inference(resolution,[status(thm)],[p494,c23]) ).
cnf(p562,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p561,p496]) ).
cnf(p563,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p562,p492]) ).
cnf(p564,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p563,p499]) ).
cnf(p565,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p564,p474]) ).
cnf(c5,plain,
( cC4(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p483,plain,
cC4(iV21026),
inference(resolution,[status(thm)],[p476,c5]) ).
cnf(p572,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p565,p483]) ).
fof(f7,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
fof(f7_nnf,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X] :
( ( ~ cTOP(X)
| ~ cC108(X)
| cC110(X) )
& ( ( cTOP(X)
& cC108(X) )
| ~ cC110(X) ) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c19,plain,
( cC108(X0)
| ~ cC110(X0) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p498,plain,
cC108(iV21026),
inference(resolution,[status(thm)],[p496,c19]) ).
cnf(p573,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p572,p498]) ).
cnf(c95,plain,
( cC14(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p475,plain,
cC14(iV21026),
inference(resolution,[status(thm)],[p471,c95]) ).
cnf(p574,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p573,p475]) ).
cnf(p575,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p574,p495]) ).
cnf(p576,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p575,c0]) ).
cnf(p894,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035) ),
inference(resolution,[status(thm)],[p867,p576]) ).
fof(f47,axiom,
! [X] :
( cC24(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_47) ).
fof(f47_nnf,plain,
! [X] :
( ( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC24(X) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC24(X) ) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [X,Y] :
( ( cC2(Y)
| ~ rR1(X,Y)
| cC24(X) )
& ( ( ~ cC2(sk20(X))
& rR1(X,sk20(X)) )
| ~ cC24(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk20])],[f47_nnf]) ).
cnf(c139,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC24(X0) ),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
fof(f152,axiom,
rR1(iV21027,iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_152) ).
fof(f152_nnf,plain,
rR1(iV21027,iV21036),
inference(nnf_transformation,[status(thm)],[f152]) ).
cnf(c318,plain,
rR1(iV21027,iV21036),
inference(cnf_transformation,[status(esa)],[f152_nnf]) ).
cnf(p745,plain,
( cC2(iV21036)
| cC24(iV21027) ),
inference(resolution,[status(thm)],[c139,c318]) ).
fof(f240,axiom,
~ cC2(iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_240) ).
fof(f240_nnf,plain,
~ cC2(iV21036),
inference(nnf_transformation,[status(thm)],[f240]) ).
fof(f240_sk,plain,
~ cC2(iV21036),
inference(skolemisation,[status(esa)],[f240_nnf]) ).
cnf(c406,plain,
~ cC2(iV21036),
inference(cnf_transformation,[status(esa)],[f240_sk]) ).
cnf(p777,plain,
cC24(iV21027),
inference(resolution,[status(thm)],[p745,c406]) ).
cnf(p897,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035) ),
inference(resolution,[status(thm)],[p894,p777]) ).
cnf(p898,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035) ),
inference(resolution,[status(thm)],[p897,c0]) ).
cnf(p1256,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[p1141,p898]) ).
fof(f59,axiom,
! [X] :
( cC46(X)
<=> ( ~ cC44(X)
& ~ cC12(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_59) ).
fof(f59_nnf,plain,
! [X] :
( ( cC44(X)
| cC12(X)
| cC46(X) )
& ( ( ~ cC44(X)
& ~ cC12(X) )
| ~ cC46(X) ) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [X] :
( ( cC44(X)
| cC12(X)
| cC46(X) )
& ( ( ~ cC44(X)
& ~ cC12(X) )
| ~ cC46(X) ) ),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c174,plain,
( cC44(X0)
| cC12(X0)
| cC46(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f157,axiom,
~ cC46(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_157) ).
fof(f157_nnf,plain,
~ cC46(iV21029),
inference(nnf_transformation,[status(thm)],[f157]) ).
fof(f157_sk,plain,
~ cC46(iV21029),
inference(skolemisation,[status(esa)],[f157_nnf]) ).
cnf(c323,plain,
~ cC46(iV21029),
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(p1074,plain,
( cC44(iV21029)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[c174,c323]) ).
cnf(p1265,plain,
( cC12(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[p1256,p1074]) ).
cnf(p1297,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029) ),
inference(factoring,[status(thm)],[p1265]) ).
cnf(p1298,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[p1297,c0]) ).
cnf(p1387,plain,
( ~ cC72(iV21030)
| cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029)
| cC2(iV21032) ),
inference(resolution,[status(thm)],[p1209,p1298]) ).
cnf(p1927,plain,
( cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029)
| cC2(iV21032)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[p1296,p1387]) ).
fof(f214,axiom,
~ cC2(iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_214) ).
fof(f214_nnf,plain,
~ cC2(iV21032),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
~ cC2(iV21032),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c380,plain,
~ cC2(iV21032),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
cnf(p2016,plain,
( cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029)
| cC18(iV21030) ),
inference(resolution,[status(thm)],[p1927,c380]) ).
fof(f202,axiom,
~ cC18(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_202) ).
fof(f202_nnf,plain,
~ cC18(iV21030),
inference(nnf_transformation,[status(thm)],[f202]) ).
fof(f202_sk,plain,
~ cC18(iV21030),
inference(skolemisation,[status(esa)],[f202_nnf]) ).
cnf(c368,plain,
~ cC18(iV21030),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
cnf(p2017,plain,
( cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21035)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[p2016,c368]) ).
fof(f232,axiom,
~ cC12(iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_232) ).
fof(f232_nnf,plain,
~ cC12(iV21035),
inference(nnf_transformation,[status(thm)],[f232]) ).
fof(f232_sk,plain,
~ cC12(iV21035),
inference(skolemisation,[status(esa)],[f232_nnf]) ).
cnf(c398,plain,
~ cC12(iV21035),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
cnf(p2018,plain,
( cowlNothing(sk36)
| xsd_string(sk37)
| cC12(iV21029) ),
inference(resolution,[status(thm)],[p2017,c398]) ).
fof(f163,axiom,
~ cC12(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f163_nnf,plain,
~ cC12(iV21029),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
~ cC12(iV21029),
inference(skolemisation,[status(esa)],[f163_nnf]) ).
cnf(c329,plain,
~ cC12(iV21029),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(p2019,plain,
( cowlNothing(sk36)
| xsd_string(sk37) ),
inference(resolution,[status(thm)],[p2018,c329]) ).
cnf(c410,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_string(sk37)
| xsd_integer(sk37)
| cowlNothing(sk36)
| ~ cowlThing(sk36) ),
inference(cnf_transformation,[status(esa)],[f242_sk]) ).
cnf(p413,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_string(sk37)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[c0,c410]) ).
cnf(p2021,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2019,p413]) ).
cnf(p2023,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(factoring,[status(thm)],[p2021]) ).
cnf(p2024,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2023,c0]) ).
cnf(p2025,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2024,p463]) ).
cnf(p2026,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2025,p471]) ).
cnf(p2027,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2026,p510]) ).
cnf(p2028,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2027,p507]) ).
cnf(p2029,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2028,p465]) ).
cnf(p2030,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2029,p497]) ).
cnf(p2031,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2030,p533]) ).
cnf(p2032,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2031,p472]) ).
cnf(p2076,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2032,p470]) ).
cnf(p2077,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2076,p505]) ).
cnf(p2078,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2077,p509]) ).
cnf(p2079,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2078,p468]) ).
cnf(p2080,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2079,p476]) ).
cnf(p2081,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2080,p479]) ).
cnf(p2082,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2081,p469]) ).
cnf(p2083,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2082,p534]) ).
cnf(p2127,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2083,p508]) ).
cnf(p2128,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2127,p504]) ).
cnf(p2129,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2128,p506]) ).
cnf(p2130,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2129,p478]) ).
cnf(p2131,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2130,p451]) ).
cnf(p2132,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2131,p491]) ).
cnf(p2134,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2132,p493]) ).
cnf(p2135,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2134,p454]) ).
cnf(p2137,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2135,p473]) ).
cnf(p2138,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2137,p500]) ).
cnf(p2139,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2138,p482]) ).
cnf(p2140,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2139,p434]) ).
cnf(p2184,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2140,p494]) ).
cnf(p2185,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2184,p524]) ).
cnf(p2186,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2185,p418]) ).
cnf(p2187,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2186,p501]) ).
cnf(p2188,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2187,p496]) ).
cnf(p2189,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2188,p492]) ).
cnf(p2190,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2189,p499]) ).
cnf(p2191,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2190,p474]) ).
cnf(p2235,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2191,p483]) ).
cnf(p2236,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2235,p498]) ).
cnf(p2237,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2236,p475]) ).
cnf(p2238,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2237,p495]) ).
cnf(p2239,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2238,c0]) ).
cnf(p2241,plain,
( cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2239,p867]) ).
cnf(p2341,plain,
( cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2241,p777]) ).
cnf(p2342,plain,
( cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2341,c0]) ).
fof(f61,axiom,
! [X] :
( cC50(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
fof(f61_nnf,plain,
! [X] :
( ( ! [Y] :
( cC12(Y)
| ~ rR1(X,Y) )
| cC50(X) )
& ( ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) )
| ~ cC50(X) ) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [X,Y] :
( ( cC12(Y)
| ~ rR1(X,Y)
| cC50(X) )
& ( ( ~ cC12(sk27(X))
& rR1(X,sk27(X)) )
| ~ cC50(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27])],[f61_nnf]) ).
cnf(c180,plain,
( cC12(X1)
| ~ rR1(X0,X1)
| cC50(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
fof(f182,axiom,
rR1(iV21029,iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_182) ).
fof(f182_nnf,plain,
rR1(iV21029,iV21033),
inference(nnf_transformation,[status(thm)],[f182]) ).
cnf(c348,plain,
rR1(iV21029,iV21033),
inference(cnf_transformation,[status(esa)],[f182_nnf]) ).
cnf(p1117,plain,
( cC12(iV21033)
| cC50(iV21029) ),
inference(resolution,[status(thm)],[c180,c348]) ).
cnf(p2344,plain,
( cC12(iV21033)
| cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2342,p1117]) ).
fof(f58,axiom,
! [X] :
( cC44(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_58) ).
fof(f58_nnf,plain,
! [X] :
( ( ! [Y] :
( cC2(Y)
| ~ rR1(X,Y) )
| cC44(X) )
& ( ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) )
| ~ cC44(X) ) ),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [X,Y] :
( ( cC2(Y)
| ~ rR1(X,Y)
| cC44(X) )
& ( ( ~ cC2(sk25(X))
& rR1(X,sk25(X)) )
| ~ cC44(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk25])],[f58_nnf]) ).
cnf(c171,plain,
( cC2(X1)
| ~ rR1(X0,X1)
| cC44(X0) ),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
fof(f181,axiom,
rR1(iV21029,iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_181) ).
fof(f181_nnf,plain,
rR1(iV21029,iV21034),
inference(nnf_transformation,[status(thm)],[f181]) ).
cnf(c347,plain,
rR1(iV21029,iV21034),
inference(cnf_transformation,[status(esa)],[f181_nnf]) ).
cnf(p1049,plain,
( cC2(iV21034)
| cC44(iV21029) ),
inference(resolution,[status(thm)],[c171,c347]) ).
cnf(p2349,plain,
( cC2(iV21034)
| cC12(iV21033)
| cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2344,p1049]) ).
cnf(p2375,plain,
( cC2(iV21034)
| cC12(iV21033)
| cC12(iV21035)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2349,c0]) ).
cnf(p2376,plain,
( cC2(iV21032)
| cC2(iV21034)
| cC12(iV21033)
| cC12(iV21035)
| ~ cC72(iV21030)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2375,p1209]) ).
cnf(p2381,plain,
( cC18(iV21030)
| cC2(iV21032)
| cC2(iV21034)
| cC12(iV21033)
| cC12(iV21035)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2376,p1296]) ).
cnf(p2392,plain,
( cC18(iV21030)
| cC2(iV21034)
| cC12(iV21033)
| cC12(iV21035)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2381,c380]) ).
fof(f228,axiom,
~ cC2(iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_228) ).
fof(f228_nnf,plain,
~ cC2(iV21034),
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
~ cC2(iV21034),
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c394,plain,
~ cC2(iV21034),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(p2393,plain,
( cC18(iV21030)
| cC12(iV21033)
| cC12(iV21035)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2392,c394]) ).
cnf(p2394,plain,
( cC12(iV21033)
| cC12(iV21035)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2393,c368]) ).
fof(f222,axiom,
~ cC12(iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_222) ).
fof(f222_nnf,plain,
~ cC12(iV21033),
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
~ cC12(iV21033),
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c388,plain,
~ cC12(iV21033),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(p2395,plain,
( cC12(iV21035)
| xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2394,c388]) ).
cnf(p2396,plain,
( xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2395,c398]) ).
cnf(c2,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p2022,plain,
( ~ xsd_integer(sk37)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2019,c2]) ).
cnf(p2397,plain,
( cowlNothing(sk36)
| cowlNothing(sk36) ),
inference(resolution,[status(thm)],[p2396,p2022]) ).
cnf(p2398,plain,
cowlNothing(sk36),
inference(factoring,[status(thm)],[p2397]) ).
cnf(c1,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p2399,plain,
$false,
inference(resolution,[status(thm)],[p2398,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/10.40 % Computer : n026.cluster.edu
% 0.11/10.40 % Model : x86_64 x86_64
% 0.11/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.40 % Memory : 8046.5625MB
% 0.11/10.40 % OS : Linux 6.8.0-71-generic
% 0.11/10.40 % CPULimit : 300
% 0.11/10.40 % WCLimit : 300
% 0.11/10.40 % DateTime : Wed Sep 23 19:34:49 UTC 2026
% 0.11/10.40 % CPUTime :
% 0.11/10.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.81/11.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.81/11.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------