%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sun Jul 17 03:29:06 EDT 2022
% Result : Theorem 0.45s 0.63s
% Output : Refutation 0.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 64
% Syntax : Number of clauses : 165 ( 68 unt; 3 nHn; 163 RR)
% Number of literals : 1425 ( 0 equ;1259 neg)
% Maximal clause size : 49 ( 8 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 44 ( 43 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 35 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
cowlThing(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
cnf(2,axiom,
~ cowlNothing(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
cnf(3,axiom,
( ~ xsd_string(X)
| ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
cnf(4,axiom,
( xsd_string(X)
| xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
cnf(25,axiom,
( cC104(X)
| ~ rR1(X,Y)
| ~ cC102xcomp(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
cnf(29,axiom,
( ~ cC108(X)
| cC28(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
cnf(30,axiom,
( ~ cC108(X)
| cC106(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
cnf(130,axiom,
( cC34(X)
| ~ cC30xcomp(X)
| ~ cC32xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_52) ).
cnf(142,axiom,
( cC38(X)
| ~ cTOP(X)
| ~ cC36xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_57) ).
cnf(160,axiom,
( cC42(X)
| ~ rR1(X,Y)
| ~ cC8xcomp(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_65) ).
cnf(163,axiom,
( cC44(X)
| ~ cC40xcomp(X)
| ~ cC42(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_66) ).
cnf(180,axiom,
( cC50(X)
| ~ cC46xcomp(X)
| ~ cC48xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_73) ).
cnf(200,axiom,
( ~ cC56(X)
| cC44(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_82) ).
cnf(201,axiom,
( cC56(X)
| ~ cC54xcomp(X)
| ~ cC44(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_82) ).
cnf(222,axiom,
( cC60(X)
| ~ rR1(X,Y)
| ~ cC12xcomp(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_91) ).
cnf(225,axiom,
( cC62(X)
| ~ cC60(X)
| ~ cC58xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_92) ).
cnf(244,axiom,
( cC68(X)
| ~ cC64xcomp(X)
| ~ cC66xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_100) ).
cnf(271,axiom,
( ~ cC76(X)
| cC62(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_112) ).
cnf(272,axiom,
( cC76(X)
| ~ cC74xcomp(X)
| ~ cC62(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_112) ).
cnf(288,axiom,
( cC80(X)
| ~ rR1(X,Y)
| ~ cC16xcomp(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_119) ).
cnf(310,axiom,
( cC88(X)
| ~ cC84xcomp(X)
| ~ cC86xcomp(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_128) ).
cnf(344,axiom,
( ~ cC98(X)
| cC82(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_143) ).
cnf(348,axiom,
( ~ cTEST(X)
| cC108(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_145) ).
cnf(349,axiom,
( ~ cTEST(X)
| cC130(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_145) ).
cnf(351,axiom,
( ~ rR1(iV16439,X)
| cC98(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_146) ).
cnf(353,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_149) ).
cnf(354,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_150) ).
cnf(359,axiom,
( ~ rR1(iV16440,X)
| cC76(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_156) ).
cnf(360,axiom,
cC102xcomp(iV16440),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_157) ).
cnf(362,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_159) ).
cnf(363,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_163) ).
cnf(368,axiom,
cC36xcomp(iV16448),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_168) ).
cnf(373,axiom,
cC74xcomp(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_174) ).
cnf(376,axiom,
( ~ rR1(iV16453,X)
| cC56(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_178) ).
cnf(379,axiom,
cC58xcomp(iV16453),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_181) ).
cnf(380,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_182) ).
cnf(382,axiom,
cC40xcomp(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_185) ).
cnf(385,axiom,
( ~ rR1(iV16455,X)
| cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_188) ).
cnf(387,axiom,
cC54xcomp(iV16455),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_190) ).
cnf(390,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_193) ).
cnf(393,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_197) ).
cnf(397,axiom,
cC36xcomp(iV16457),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_201) ).
cnf(404,axiom,
cC30xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_209) ).
cnf(405,axiom,
cC84xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_210) ).
cnf(407,axiom,
cC46xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_212) ).
cnf(408,axiom,
cC64xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_213) ).
cnf(410,axiom,
cC86xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_215) ).
cnf(411,axiom,
cC32xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_216) ).
cnf(412,axiom,
cC48xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_217) ).
cnf(416,axiom,
cC66xcomp(iV16459),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_221) ).
cnf(421,axiom,
cC8xcomp(iV16460),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_227) ).
cnf(430,axiom,
cC12xcomp(iV16461),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_237) ).
cnf(434,axiom,
( ~ rR1(iV16461,X)
| cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_241) ).
cnf(436,axiom,
rR1(iV16461,iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_243) ).
cnf(441,axiom,
cC8xcomp(iV16462),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_249) ).
cnf(448,axiom,
cC16xcomp(iV16463),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_257) ).
cnf(452,axiom,
( ~ rR1(iV16463,X)
| cC56(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_261) ).
cnf(454,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_263) ).
cnf(455,axiom,
( ~ rR1(iV16464,X)
| cC38(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_265) ).
cnf(457,axiom,
cC12xcomp(iV16464),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_267) ).
cnf(464,axiom,
rR1(iV16464,iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_274) ).
cnf(469,axiom,
cC8xcomp(iV16465),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_280) ).
cnf(475,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV115')
| cowlNothing('SKOLEMAAAV115')
| ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cowlThing(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16455)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
cnf(476,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[475,2,1]) ).
cnf(477,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV115')
| cowlNothing('SKOLEMAAAV115')
| xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cowlThing(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16455)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC38(iV16465)
| ~ cowlThing(iV16465) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
cnf(478,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[477,2,1]) ).
cnf(479,plain,
cC108(iV16439),
inference('HYPERRESOLVE',[status(thm)],[348,353]) ).
cnf(480,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[476,479]) ).
cnf(481,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC130(iV16439)
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[478,479]) ).
cnf(482,plain,
cC130(iV16439),
inference('HYPERRESOLVE',[status(thm)],[349,353]) ).
cnf(483,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[480,482]) ).
cnf(484,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC98(iV16440)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[481,482]) ).
cnf(518,plain,
cC98(iV16440),
inference('HYPERRESOLVE',[status(thm)],[351,354]) ).
cnf(519,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[483,518]) ).
cnf(520,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[484,518]) ).
cnf(523,plain,
cC76(iV16463),
inference('HYPERRESOLVE',[status(thm)],[359,362]) ).
cnf(524,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[519,523]) ).
cnf(525,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[520,523]) ).
cnf(530,plain,
cC56(iV16461),
inference('HYPERRESOLVE',[status(thm)],[376,380]) ).
cnf(531,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[524,530]) ).
cnf(532,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16460)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[525,530]) ).
cnf(533,plain,
cC38(iV16460),
inference('HYPERRESOLVE',[status(thm)],[385,390]) ).
cnf(534,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[531,533]) ).
cnf(535,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[532,533]) ).
cnf(536,plain,
cC38(iV16462),
inference('HYPERRESOLVE',[status(thm)],[434,436]) ).
cnf(537,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[534,536]) ).
cnf(538,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[535,536]) ).
cnf(539,plain,
cC56(iV16464),
inference('HYPERRESOLVE',[status(thm)],[452,454]) ).
cnf(540,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[537,539]) ).
cnf(541,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16465) ),
inference('REWRITE',[status(thm)],[538,539]) ).
cnf(542,plain,
cC38(iV16465),
inference('HYPERRESOLVE',[status(thm)],[455,464]) ).
cnf(543,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[540,542]) ).
cnf(544,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC34(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[541,542]) ).
cnf(563,plain,
cC34(iV16459),
inference('HYPERRESOLVE',[status(thm)],[130,404,411]) ).
cnf(564,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[543,563]) ).
cnf(565,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC38(iV16457)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[544,563]) ).
cnf(573,plain,
cC38(iV16457),
inference('HYPERRESOLVE',[status(thm)],[142,393,397]) ).
cnf(574,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[564,573]) ).
cnf(575,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC38(iV16448)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[565,573]) ).
cnf(576,plain,
cC38(iV16448),
inference('HYPERRESOLVE',[status(thm)],[142,363,368]) ).
cnf(577,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[574,576]) ).
cnf(578,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[575,576]) ).
cnf(589,plain,
cC50(iV16459),
inference('HYPERRESOLVE',[status(thm)],[180,407,412]) ).
cnf(590,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[577,589]) ).
cnf(591,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[578,589]) ).
cnf(611,plain,
cC68(iV16459),
inference('HYPERRESOLVE',[status(thm)],[244,408,416]) ).
cnf(612,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC88(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[590,611]) ).
cnf(613,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC88(iV16459)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[591,611]) ).
cnf(630,plain,
cC88(iV16459),
inference('HYPERRESOLVE',[status(thm)],[310,405,410]) ).
cnf(631,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[612,630]) ).
cnf(632,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC104(iV16439)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[613,630]) ).
cnf(640,plain,
cC104(iV16439),
inference('HYPERRESOLVE',[status(thm)],[25,354,360]) ).
cnf(641,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[631,640]) ).
cnf(642,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC42(iV16464)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[632,640]) ).
cnf(643,plain,
cC42(iV16464),
inference('HYPERRESOLVE',[status(thm)],[160,464,469]) ).
cnf(644,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[641,643]) ).
cnf(645,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[642,643]) ).
cnf(646,plain,
cC42(iV16461),
inference('HYPERRESOLVE',[status(thm)],[160,436,441]) ).
cnf(647,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[644,646]) ).
cnf(648,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[645,646]) ).
cnf(649,plain,
cC42(iV16455),
inference('HYPERRESOLVE',[status(thm)],[160,390,421]) ).
cnf(650,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[647,649]) ).
cnf(651,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[648,649]) ).
cnf(652,plain,
cC60(iV16463),
inference('HYPERRESOLVE',[status(thm)],[222,454,457]) ).
cnf(653,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[650,652]) ).
cnf(654,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[651,652]) ).
cnf(655,plain,
cC60(iV16453),
inference('HYPERRESOLVE',[status(thm)],[222,380,430]) ).
cnf(656,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[653,655]) ).
cnf(657,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC80(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[654,655]) ).
cnf(658,plain,
cC80(iV16440),
inference('HYPERRESOLVE',[status(thm)],[288,362,448]) ).
cnf(659,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[656,658]) ).
cnf(660,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[657,658]) ).
cnf(661,plain,
cC106(iV16439),
inference('HYPERRESOLVE',[status(thm)],[30,479]) ).
cnf(662,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC28(iV16439)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[659,661]) ).
cnf(663,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC28(iV16439)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[660,661]) ).
cnf(664,plain,
cC28(iV16439),
inference('HYPERRESOLVE',[status(thm)],[29,479]) ).
cnf(665,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[662,664]) ).
cnf(666,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[663,664]) ).
cnf(669,plain,
cC82(iV16440),
inference('HYPERRESOLVE',[status(thm)],[344,518]) ).
cnf(670,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[665,669]) ).
cnf(671,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC62(iV16463)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[666,669]) ).
cnf(679,plain,
cC62(iV16463),
inference('HYPERRESOLVE',[status(thm)],[271,523]) ).
cnf(680,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[670,679]) ).
cnf(681,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[671,679]) ).
cnf(695,plain,
cC44(iV16461),
inference('HYPERRESOLVE',[status(thm)],[200,530]) ).
cnf(696,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[680,695]) ).
cnf(697,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC44(iV16464) ),
inference('REWRITE',[status(thm)],[681,695]) ).
cnf(701,plain,
cC44(iV16464),
inference('HYPERRESOLVE',[status(thm)],[200,539]) ).
cnf(702,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455) ),
inference('REWRITE',[status(thm)],[696,701]) ).
cnf(703,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455)
| ~ cC44(iV16455) ),
inference('REWRITE',[status(thm)],[697,701]) ).
cnf(718,plain,
cC44(iV16455),
inference('HYPERRESOLVE',[status(thm)],[163,649,382]) ).
cnf(719,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455) ),
inference('REWRITE',[status(thm)],[702,718]) ).
cnf(720,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC56(iV16455) ),
inference('REWRITE',[status(thm)],[703,718]) ).
cnf(725,plain,
cC62(iV16453),
inference('HYPERRESOLVE',[status(thm)],[225,655,379]) ).
cnf(726,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC56(iV16455) ),
inference('REWRITE',[status(thm)],[719,725]) ).
cnf(727,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453)
| ~ cC56(iV16455) ),
inference('REWRITE',[status(thm)],[720,725]) ).
cnf(781,plain,
cC56(iV16455),
inference('HYPERRESOLVE',[status(thm)],[201,718,387]) ).
cnf(782,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453) ),
inference('REWRITE',[status(thm)],[726,781]) ).
cnf(783,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116')
| ~ cC76(iV16453) ),
inference('REWRITE',[status(thm)],[727,781]) ).
cnf(784,plain,
cC76(iV16453),
inference('HYPERRESOLVE',[status(thm)],[272,725,373]) ).
cnf(785,plain,
( ~ xsd_string('SKOLEMAAAV116')
| xsd_integer('SKOLEMAAAV116') ),
inference('REWRITE',[status(thm)],[782,784]) ).
cnf(786,plain,
( xsd_string('SKOLEMAAAV116')
| ~ xsd_integer('SKOLEMAAAV116') ),
inference('REWRITE',[status(thm)],[783,784]) ).
cnf(787,plain,
xsd_integer('SKOLEMAAAV116'),
inference('HYPERRESOLVE',[status(thm)],[785,4]) ).
cnf(788,plain,
xsd_string('SKOLEMAAAV116'),
inference('REWRITE',[status(thm)],[786,787]) ).
cnf(789,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[3,788]),787]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% 0.11/0.12 % Command : run-snark %s %d
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Tue Jun 7 08:07:03 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.44 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45 *
% 0.18/0.45 *
% 0.18/0.46 #<PACKAGE "SNARK-USER">
% 0.18/0.46 *
% 0.18/0.46 SNARK-TPTP-OPTIONS
% 0.18/0.46 *
% 0.18/0.46 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.18/0.46 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.18/0.46 (USE-FACTORING :POS)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.18/0.46 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.18/0.46 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.18/0.46 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.18/0.46 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.18/0.46 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.18/0.46 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.18/0.46 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.18/0.46 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.18/0.46 (DECLARE-TPTP-SYMBOLS2))
% 0.18/0.46 *
% 0.18/0.46 "."
% 0.18/0.46 *
% 0.18/0.46 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-07T08:07:03
% 0.18/0.46 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n025.cluster.edu at 2022-06-07T08:07:03
% 0.45/0.63
% 0.45/0.63
% 0.45/0.63 #||
% 0.45/0.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.45/0.63 % SZS output start Refutation
% See solution above
% 0.45/0.66 ||#
% 0.45/0.66
% 0.45/0.66 ; Summary of computation:
% 0.45/0.66 ; 1179 formulas have been input or derived (from 576 formulas).
% 0.45/0.66 ; 789 (67%) were retained. Of these,
% 0.45/0.66 ; 68 ( 9%) were simplified or subsumed later,
% 0.45/0.66 ; 721 (91%) are still being kept.
% 0.45/0.66 ;
% 0.45/0.66 ; Run time in seconds excluding printing time:
% 0.45/0.66 ; 0.039 22% Read assertion file (1 call)
% 0.45/0.66 ; 0.015 9% Assert (287 calls)
% 0.45/0.66 ; 0.039 22% Process new row (1,076 calls)
% 0.45/0.66 ; 0.013 7% Resolution (1,150 calls)
% 0.45/0.66 ; 0.002 1% Paramodulation (575 calls)
% 0.45/0.66 ; 0.000 0% Factoring (44 calls)
% 0.45/0.66 ; 0.001 1% Condensing (498 calls)
% 0.45/0.66 ; 0.008 5% Forward subsumption (498 calls)
% 0.45/0.66 ; 0.009 5% Backward subsumption (498 calls)
% 0.45/0.66 ; 0.011 6% Forward simplification (1,076 calls)
% 0.45/0.66 ; 0.012 7% Backward simplification (787 calls)
% 0.45/0.66 ; 0.000 0% Ordering (144 calls)
% 0.45/0.67 ; 0.000 0% Sortal reasoning (32 calls)
% 0.45/0.67 ; 0.002 1% Purity testing (1 call)
% 0.45/0.67 ; 0.025 14% Other
% 0.45/0.67 ; 0.176 Total
% 0.45/0.67 ; 0.208 Real time
% 0.45/0.67 ;
% 0.45/0.67 ; Term-hash-array has 808 terms in all.
% 0.45/0.67 ; Feature-vector-row-index has 432 entries (434 at peak, 498 added, 66 deleted).
% 0.45/0.67 ; Feature-vector-row-index has 355 nodes (398 at peak, 1,624 added, 1,269 deleted).
% 0.45/0.67 ; Retrieved 790 possibly forward subsuming rows in 498 calls.
% 0.45/0.67 ; Retrieved 477 possibly backward subsumed rows in 498 calls.
% 0.45/0.67 ; Path-index has 826 entries (826 at peak, 1,419 added, 593 deleted).
% 0.45/0.67 ; Path-index has 1,404 nodes (1,404 at peak, 1,997 added, 593 deleted).
% 0.45/0.67 ; Trie-index has 826 entries (826 at peak, 1,419 added, 593 deleted).
% 0.45/0.67 ; Trie-index has 1,433 nodes (1,433 at peak, 2,026 added, 593 deleted).
% 0.45/0.67 ; Retrieved 320 generalization terms in 815 calls.
% 0.45/0.67 ; Retrieved 288 instance terms in 288 calls.
% 0.45/0.67 ; Retrieved 8,775 unifiable terms in 3,121 calls.
% 0.45/0.67 ;
% 0.45/0.67 ; The agenda of rows to give has 164 entries:
% 0.45/0.67 ; 1 with value (4 4) 6 with value (4 6) 28 with value (4 8)
% 0.45/0.67 ; 33 with value (4 5) 89 with value (4 7) 7 with value (4 9)
% 0.45/0.67 Evaluation took:
% 0.45/0.67 0.208 seconds of real time
% 0.45/0.67 0.183611 seconds of user run time
% 0.45/0.67 0.024198 seconds of system run time
% 0.45/0.67 [Run times include 0.012 seconds GC run time.]
% 0.45/0.67 0 calls to %EVAL
% 0.45/0.67 0 page faults and
% 0.45/0.67 32,741,536 bytes consed.
% 0.45/0.67 :PROOF-FOUND
% 0.45/0.67 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-07T08:07:04
% 0.45/0.67 :PROOF-FOUND
% 0.45/0.67 *
%------------------------------------------------------------------------------