%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n003.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 : 300s
% DateTime : Wed Jul 27 13:01:28 EDT 2022
% Result : Theorem 2.10s 2.28s
% Output : Refutation 2.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 62
% Syntax : Number of clauses : 99 ( 67 unt; 3 nHn; 97 RR)
% Number of literals : 328 ( 0 equ; 228 neg)
% Maximal clause size : 49 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 32 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ cowlNothing(A),
file('KRS161+1.p',unknown),
[] ).
cnf(2,axiom,
( ~ xsd_string(A)
| ~ xsd_integer(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ cC106(A)
| cC104(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(24,axiom,
( ~ cC108(A)
| cC28(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ cC108(A)
| cC106(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(115,axiom,
( cC34(A)
| ~ cC30xcomp(A)
| ~ cC32xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(125,axiom,
( cC38(A)
| ~ cTOP(A)
| ~ cC36xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(140,axiom,
( cC42(A)
| ~ rR1(A,B)
| ~ cC8xcomp(B) ),
file('KRS161+1.p',unknown),
[] ).
cnf(142,axiom,
( ~ cC44(A)
| cC42(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(143,axiom,
( cC44(A)
| ~ cC40xcomp(A)
| ~ cC42(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(158,axiom,
( cC50(A)
| ~ cC46xcomp(A)
| ~ cC48xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ cC56(A)
| cC44(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(176,axiom,
( cC56(A)
| ~ cC54xcomp(A)
| ~ cC44(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(194,axiom,
( cC60(A)
| ~ rR1(A,B)
| ~ cC12xcomp(B) ),
file('KRS161+1.p',unknown),
[] ).
cnf(195,axiom,
( ~ cC62(A)
| cC60(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(197,axiom,
( cC62(A)
| ~ cC60(A)
| ~ cC58xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(214,axiom,
( cC68(A)
| ~ cC64xcomp(A)
| ~ cC66xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ cC76(A)
| cC62(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(238,axiom,
( cC76(A)
| ~ cC74xcomp(A)
| ~ cC62(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(252,axiom,
( ~ cC82(A)
| cC80(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(271,axiom,
( cC88(A)
| ~ cC84xcomp(A)
| ~ cC86xcomp(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(300,axiom,
( ~ cC98(A)
| cC82(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(303,axiom,
( ~ cTEST(A)
| cC108(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(304,axiom,
( ~ cTEST(A)
| cC130(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(306,axiom,
( ~ rR1(iV16439,A)
| cC98(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(308,axiom,
( ~ rR1(iV16440,A)
| cC76(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(314,axiom,
( ~ rR1(iV16453,A)
| cC56(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(338,axiom,
( ~ rR1(iV16463,A)
| cC56(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(347,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ 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('KRS161+1.p',unknown),
[] ).
cnf(348,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ 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) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[347]),1]),
[iquote('copy,347,unit_del,1')] ).
cnf(349,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ 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('KRS161+1.p',unknown),
[] ).
cnf(350,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ 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) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[349]),1]),
[iquote('copy,349,unit_del,1')] ).
cnf(351,axiom,
cowlThing(A),
file('KRS161+1.p',unknown),
[] ).
cnf(352,axiom,
( xsd_string(A)
| xsd_integer(A) ),
file('KRS161+1.p',unknown),
[] ).
cnf(397,axiom,
cTEST(iV16439),
file('KRS161+1.p',unknown),
[] ).
cnf(398,axiom,
rR1(iV16439,iV16440),
file('KRS161+1.p',unknown),
[] ).
cnf(404,axiom,
rR1(iV16440,iV16463),
file('KRS161+1.p',unknown),
[] ).
cnf(405,axiom,
cTOP(iV16448),
file('KRS161+1.p',unknown),
[] ).
cnf(407,axiom,
cC36xcomp(iV16448),
file('KRS161+1.p',unknown),
[] ).
cnf(411,axiom,
cC74xcomp(iV16453),
file('KRS161+1.p',unknown),
[] ).
cnf(414,axiom,
cC58xcomp(iV16453),
file('KRS161+1.p',unknown),
[] ).
cnf(415,axiom,
rR1(iV16453,iV16461),
file('KRS161+1.p',unknown),
[] ).
cnf(416,axiom,
cC40xcomp(iV16455),
file('KRS161+1.p',unknown),
[] ).
cnf(419,axiom,
cC54xcomp(iV16455),
file('KRS161+1.p',unknown),
[] ).
cnf(421,axiom,
rR1(iV16455,iV16460),
file('KRS161+1.p',unknown),
[] ).
cnf(422,axiom,
cTOP(iV16457),
file('KRS161+1.p',unknown),
[] ).
cnf(425,axiom,
cC36xcomp(iV16457),
file('KRS161+1.p',unknown),
[] ).
cnf(431,axiom,
cC30xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(432,axiom,
cC84xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(434,axiom,
cC46xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(435,axiom,
cC64xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(437,axiom,
cC86xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(438,axiom,
cC32xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(439,axiom,
cC48xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(443,axiom,
cC66xcomp(iV16459),
file('KRS161+1.p',unknown),
[] ).
cnf(444,axiom,
cTOP(iV16460),
file('KRS161+1.p',unknown),
[] ).
cnf(446,axiom,
cC8xcomp(iV16460),
file('KRS161+1.p',unknown),
[] ).
cnf(447,axiom,
cC36xcomp(iV16460),
file('KRS161+1.p',unknown),
[] ).
cnf(451,axiom,
cC12xcomp(iV16461),
file('KRS161+1.p',unknown),
[] ).
cnf(456,axiom,
cTOP(iV16462),
file('KRS161+1.p',unknown),
[] ).
cnf(459,axiom,
cC36xcomp(iV16462),
file('KRS161+1.p',unknown),
[] ).
cnf(466,axiom,
rR1(iV16463,iV16464),
file('KRS161+1.p',unknown),
[] ).
cnf(473,axiom,
cTOP(iV16465),
file('KRS161+1.p',unknown),
[] ).
cnf(476,axiom,
cC36xcomp(iV16465),
file('KRS161+1.p',unknown),
[] ).
cnf(480,plain,
cC130(iV16439),
inference(hyper,[status(thm)],[397,304]),
[iquote('hyper,397,304')] ).
cnf(481,plain,
cC108(iV16439),
inference(hyper,[status(thm)],[397,303]),
[iquote('hyper,397,303')] ).
cnf(485,plain,
cC38(iV16448),
inference(hyper,[status(thm)],[407,125,405]),
[iquote('hyper,407,125,405')] ).
cnf(497,plain,
cC38(iV16457),
inference(hyper,[status(thm)],[425,125,422]),
[iquote('hyper,425,125,422')] ).
cnf(510,plain,
cC88(iV16459),
inference(hyper,[status(thm)],[437,271,432]),
[iquote('hyper,437,271,432')] ).
cnf(511,plain,
cC34(iV16459),
inference(hyper,[status(thm)],[438,115,431]),
[iquote('hyper,438,115,431')] ).
cnf(512,plain,
cC50(iV16459),
inference(hyper,[status(thm)],[439,158,434]),
[iquote('hyper,439,158,434')] ).
cnf(513,plain,
cC68(iV16459),
inference(hyper,[status(thm)],[443,214,435]),
[iquote('hyper,443,214,435')] ).
cnf(514,plain,
cC38(iV16460),
inference(hyper,[status(thm)],[447,125,444]),
[iquote('hyper,447,125,444')] ).
cnf(515,plain,
cC38(iV16462),
inference(hyper,[status(thm)],[459,125,456]),
[iquote('hyper,459,125,456')] ).
cnf(516,plain,
cC38(iV16465),
inference(hyper,[status(thm)],[476,125,473]),
[iquote('hyper,476,125,473')] ).
cnf(517,plain,
cC106(iV16439),
inference(hyper,[status(thm)],[481,25]),
[iquote('hyper,481,25')] ).
cnf(518,plain,
cC28(iV16439),
inference(hyper,[status(thm)],[481,24]),
[iquote('hyper,481,24')] ).
cnf(519,plain,
cC104(iV16439),
inference(hyper,[status(thm)],[517,21]),
[iquote('hyper,517,21')] ).
cnf(520,plain,
cC98(iV16440),
inference(hyper,[status(thm)],[398,306]),
[iquote('hyper,398,306')] ).
cnf(521,plain,
cC82(iV16440),
inference(hyper,[status(thm)],[520,300]),
[iquote('hyper,520,300')] ).
cnf(522,plain,
cC80(iV16440),
inference(hyper,[status(thm)],[521,252]),
[iquote('hyper,521,252')] ).
cnf(533,plain,
cC76(iV16463),
inference(hyper,[status(thm)],[404,308]),
[iquote('hyper,404,308')] ).
cnf(534,plain,
cC62(iV16463),
inference(hyper,[status(thm)],[533,237]),
[iquote('hyper,533,237')] ).
cnf(535,plain,
cC60(iV16463),
inference(hyper,[status(thm)],[534,195]),
[iquote('hyper,534,195')] ).
cnf(548,plain,
cC56(iV16461),
inference(hyper,[status(thm)],[415,314]),
[iquote('hyper,415,314')] ).
cnf(549,plain,
cC60(iV16453),
inference(hyper,[status(thm)],[415,194,451]),
[iquote('hyper,415,194,451')] ).
cnf(550,plain,
cC44(iV16461),
inference(hyper,[status(thm)],[548,175]),
[iquote('hyper,548,175')] ).
cnf(551,plain,
cC62(iV16453),
inference(hyper,[status(thm)],[549,197,414]),
[iquote('hyper,549,197,414')] ).
cnf(552,plain,
cC42(iV16461),
inference(hyper,[status(thm)],[550,142]),
[iquote('hyper,550,142')] ).
cnf(553,plain,
cC76(iV16453),
inference(hyper,[status(thm)],[551,238,411]),
[iquote('hyper,551,238,411')] ).
cnf(554,plain,
cC42(iV16455),
inference(hyper,[status(thm)],[421,140,446]),
[iquote('hyper,421,140,446')] ).
cnf(555,plain,
cC44(iV16455),
inference(hyper,[status(thm)],[554,143,416]),
[iquote('hyper,554,143,416')] ).
cnf(556,plain,
cC56(iV16455),
inference(hyper,[status(thm)],[555,176,419]),
[iquote('hyper,555,176,419')] ).
cnf(557,plain,
cC56(iV16464),
inference(hyper,[status(thm)],[466,338]),
[iquote('hyper,466,338')] ).
cnf(558,plain,
cC44(iV16464),
inference(hyper,[status(thm)],[557,175]),
[iquote('hyper,557,175')] ).
cnf(559,plain,
cC42(iV16464),
inference(hyper,[status(thm)],[558,142]),
[iquote('hyper,558,142')] ).
cnf(560,plain,
xsd_integer(dollar_c2),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[559,350,351,352,480,481,519,517,518,351,520,522,521,351,485,351,553,551,351,549,556,555,554,351,497,351,512,510,511,513,351,514,351,552,548,550,351,515,351,533,534,351,535,557,558,351,516,351])]),
[iquote('hyper,559,350,351,352,480,481,519,517,518,351,520,522,521,351,485,351,553,551,351,549,556,555,554,351,497,351,512,510,511,513,351,514,351,552,548,550,351,515,351,533,534,351,535,557,558,351,516,351,factor_simp')] ).
cnf(561,plain,
xsd_string(dollar_c2),
inference(hyper,[status(thm)],[560,348,351,480,481,519,517,518,351,520,522,521,351,485,351,553,551,351,549,556,555,554,351,497,351,512,510,511,513,351,514,351,552,548,550,351,515,351,533,534,351,535,557,559,558,351,516,351]),
[iquote('hyper,560,348,351,480,481,519,517,518,351,520,522,521,351,485,351,553,551,351,549,556,555,554,351,497,351,512,510,511,513,351,514,351,552,548,550,351,515,351,533,534,351,535,557,559,558,351,516,351')] ).
cnf(562,plain,
$false,
inference(hyper,[status(thm)],[561,2,560]),
[iquote('hyper,561,2,560')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n003.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 : 300
% 0.12/0.33 % DateTime : Wed Jul 27 03:25:26 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.10/2.27 ----- Otter 3.3f, August 2004 -----
% 2.10/2.27 The process was started by sandbox2 on n003.cluster.edu,
% 2.10/2.27 Wed Jul 27 03:25:26 2022
% 2.10/2.27 The command was "./otter". The process ID is 32394.
% 2.10/2.27
% 2.10/2.27 set(prolog_style_variables).
% 2.10/2.27 set(auto).
% 2.10/2.27 dependent: set(auto1).
% 2.10/2.27 dependent: set(process_input).
% 2.10/2.27 dependent: clear(print_kept).
% 2.10/2.27 dependent: clear(print_new_demod).
% 2.10/2.27 dependent: clear(print_back_demod).
% 2.10/2.27 dependent: clear(print_back_sub).
% 2.10/2.27 dependent: set(control_memory).
% 2.10/2.27 dependent: assign(max_mem, 12000).
% 2.10/2.27 dependent: assign(pick_given_ratio, 4).
% 2.10/2.27 dependent: assign(stats_level, 1).
% 2.10/2.27 dependent: assign(max_seconds, 10800).
% 2.10/2.27 clear(print_given).
% 2.10/2.27
% 2.10/2.27 formula_list(usable).
% 2.10/2.27 all X (cowlThing(X)& -cowlNothing(X)).
% 2.10/2.27 all X (xsd_string(X)<-> -xsd_integer(X)).
% 2.10/2.27 all X (cC10(X)<->cC8(X)&cC6(X)).
% 2.10/2.27 all X (cC10(X)<-> -(exists Y ra_Px73(X,Y))).
% 2.10/2.27 all X (cC10xcomp(X)<-> (exists Y0 ra_Px73(X,Y0))).
% 2.10/2.27 all X (cC100(X)<-> (exists Y (rR1(X,Y)&cC98xcomp(Y)))).
% 2.10/2.27 all X (cC100(X)<-> -(exists Y ra_Px37(X,Y))).
% 2.10/2.27 all X (cC100xcomp(X)<-> (exists Y0 ra_Px37(X,Y0))).
% 2.10/2.27 all X (cC102(X)<-> (exists Y0 ra_Px36(X,Y0))).
% 2.10/2.27 all X (cC102xcomp(X)<-> -(exists Y ra_Px36(X,Y))).
% 2.10/2.27 all X (cC104(X)<-> (exists Y (rR1(X,Y)&cC102xcomp(Y)))).
% 2.10/2.27 all X (cC106(X)<->cC104(X)&cC100xcomp(X)).
% 2.10/2.27 all X (cC108(X)<->cC28(X)&cC106(X)).
% 2.10/2.27 all X (cC110(X)<->cC4xcomp(X)&cC12xcomp(X)).
% 2.10/2.27 all X (cC112(X)<->cC110(X)&cC102xcomp(X)).
% 2.10/2.27 all X (cC114(X)<-> (exists Y0 ra_Px41(X,Y0))).
% 2.10/2.27 all X (cC114xcomp(X)<-> -(exists Y ra_Px41(X,Y))).
% 2.10/2.27 all X (cC116(X)<->cC112(X)&cC114xcomp(X)).
% 2.10/2.27 all X (cC118(X)<-> (exists Y0 ra_Px42(X,Y0))).
% 2.10/2.27 all X (cC118xcomp(X)<-> -(exists Y ra_Px42(X,Y))).
% 2.10/2.27 all X (cC12(X)<-> (exists Y0 ra_Px18(X,Y0))).
% 2.10/2.27 all X (cC12xcomp(X)<-> -(exists Y ra_Px18(X,Y))).
% 2.10/2.27 all X (cC120(X)<->cC116(X)&cC118xcomp(X)).
% 2.10/2.27 all X (cC120(X)<-> -(exists Y ra_Px43(X,Y))).
% 2.10/2.27 all X (cC120xcomp(X)<-> (exists Y0 ra_Px43(X,Y0))).
% 2.10/2.27 all X (cC122(X)<-> (exists Y (rR1(X,Y)&cC120xcomp(Y)))).
% 2.10/2.27 all X (cC124(X)<-> (exists Y (rR1(X,Y)&cC122(Y)))).
% 2.10/2.27 all X (cC126(X)<-> (exists Y (rR1(X,Y)&cC124(Y)))).
% 2.10/2.27 all X (cC128(X)<-> (exists Y (rR1(X,Y)&cC126(Y)))).
% 2.10/2.27 all X (cC130(X)<-> (exists Y (rR1(X,Y)&cC128(Y)))).
% 2.10/2.27 all X (cC14(X)<-> (exists Y0 ra_Px74(X,Y0))).
% 2.10/2.27 all X (cC14(X)<->cC10(X)&cC12(X)).
% 2.10/2.27 all X (cC14xcomp(X)<-> -(exists Y ra_Px74(X,Y))).
% 2.10/2.27 all X (cC16(X)<-> (exists Y0 ra_Px27(X,Y0))).
% 2.10/2.27 all X (cC16xcomp(X)<-> -(exists Y ra_Px27(X,Y))).
% 2.10/2.27 all X (cC18(X)<-> -(exists Y ra_Px1(X,Y))).
% 2.10/2.27 all X (cC18(X)<->cC14(X)&cC16(X)).
% 2.10/2.27 all X (cC18xcomp(X)<-> (exists Y0 ra_Px1(X,Y0))).
% 2.10/2.27 all X (cC2(X)<-> (exists Y0 ra_Px2(X,Y0))).
% 2.10/2.27 all X (cC2xcomp(X)<-> -(exists Y ra_Px2(X,Y))).
% 2.10/2.27 all X (cC20(X)<-> (exists Y (rR1(X,Y)&cC18xcomp(Y)))).
% 2.10/2.27 all X (cC22(X)<-> (exists Y (rR1(X,Y)&cC20(Y)))).
% 2.10/2.27 all X (cC24(X)<-> (exists Y (rR1(X,Y)&cC22(Y)))).
% 2.10/2.27 all X (cC26(X)<-> (exists Y (rR1(X,Y)&cC24(Y)))).
% 2.10/2.27 all X (cC28(X)<-> (exists Y (rR1(X,Y)&cC26(Y)))).
% 2.10/2.27 all X (cC30(X)<-> -(exists Y ra_Px4(X,Y))).
% 2.10/2.27 all X (cC30(X)<->cC2(X)&cC4(X)).
% 2.10/2.27 all X (cC30xcomp(X)<-> (exists Y0 ra_Px4(X,Y0))).
% 2.10/2.27 all X (cC32(X)<-> (exists Y0 ra_Px5(X,Y0))).
% 2.10/2.27 all X (cC32(X)<->cC4xcomp(X)&cC2xcomp(X)).
% 2.10/2.27 all X (cC32xcomp(X)<-> -(exists Y ra_Px5(X,Y))).
% 2.10/2.27 all X (cC34(X)<-> (exists Y0 ra_Px6(X,Y0))).
% 2.10/2.27 all X (cC34(X)<->cC30xcomp(X)&cC32xcomp(X)).
% 2.10/2.27 all X (cC34xcomp(X)<-> -(exists Y ra_Px6(X,Y))).
% 2.10/2.27 all X (cC36(X)<-> -(exists Y ra_Px7(X,Y))).
% 2.10/2.27 all X (cC36(X)<-> (exists Y (rR1(X,Y)&cC34xcomp(Y)))).
% 2.10/2.27 all X (cC36xcomp(X)<-> (exists Y0 ra_Px7(X,Y0))).
% 2.10/2.27 all X (cC38(X)<->cTOP(X)&cC36xcomp(X)).
% 2.10/2.27 all X (cC38(X)<-> (exists Y0 ra_Px8(X,Y0))).
% 2.10/2.27 all X (cC38xcomp(X)<-> -(exists Y ra_Px8(X,Y))).
% 2.10/2.27 all X (cC4(X)<-> (exists Y0 ra_Px3(X,Y0))).
% 2.10/2.27 all X (cC4xcomp(X)<-> -(exists Y ra_Px3(X,Y))).
% 2.10/2.27 all X (cC40(X)<-> -(exists Y ra_Px10(X,Y))).
% 2.10/2.27 all X (cC40(X)<-> (exists Y (rR1(X,Y)&cC38xcomp(Y)))).
% 2.10/2.27 all X (cC40xcomp(X)<-> (exists Y0 ra_Px10(X,Y0))).
% 2.10/2.27 all X (cC42(X)<-> (exists Y (rR1(X,Y)&cC8xcomp(Y)))).
% 2.10/2.27 all X (cC44(X)<->cC40xcomp(X)&cC42(X)).
% 2.10/2.27 all X (cC46(X)<-> -(exists Y ra_Px13(X,Y))).
% 2.10/2.27 all X (cC46(X)<->cC8(X)&cC4(X)).
% 2.10/2.27 all X (cC46xcomp(X)<-> (exists Y0 ra_Px13(X,Y0))).
% 2.10/2.27 all X (cC48(X)<->cC4xcomp(X)&cC8xcomp(X)).
% 2.10/2.27 all X (cC48(X)<-> (exists Y0 ra_Px14(X,Y0))).
% 2.10/2.27 all X (cC48xcomp(X)<-> -(exists Y ra_Px14(X,Y))).
% 2.10/2.27 all X (cC50(X)<->cC46xcomp(X)&cC48xcomp(X)).
% 2.10/2.27 all X (cC50(X)<-> (exists Y0 ra_Px15(X,Y0))).
% 2.10/2.27 all X (cC50xcomp(X)<-> -(exists Y ra_Px15(X,Y))).
% 2.10/2.27 all X (cC52(X)<-> -(exists Y ra_Px49(X,Y))).
% 2.10/2.27 all X (cC52(X)<-> (exists Y (rR1(X,Y)&cC50xcomp(Y)))).
% 2.10/2.27 all X (cC52xcomp(X)<-> (exists Y0 ra_Px49(X,Y0))).
% 2.10/2.27 all X (cC54(X)<-> -(exists Y ra_Px16(X,Y))).
% 2.10/2.27 all X (cC54(X)<-> (exists Y (rR1(X,Y)&cC52(Y)))).
% 2.10/2.27 all X (cC54xcomp(X)<-> (exists Y0 ra_Px16(X,Y0))).
% 2.10/2.27 all X (cC56(X)<->cC54xcomp(X)&cC44(X)).
% 2.10/2.27 all X (cC56(X)<-> (exists Y0 ra_Px17(X,Y0))).
% 2.10/2.27 all X (cC56xcomp(X)<-> -(exists Y ra_Px17(X,Y))).
% 2.10/2.27 all X (cC58(X)<-> (exists Y (rR1(X,Y)&cC56xcomp(Y)))).
% 2.10/2.27 all X (cC58(X)<-> -(exists Y ra_Px19(X,Y))).
% 2.10/2.27 all X (cC58xcomp(X)<-> (exists Y0 ra_Px19(X,Y0))).
% 2.10/2.27 all X (cC6(X)<->cC2(X)&cC4(X)).
% 2.10/2.27 all X (cC6(X)<-> (exists Y0 ra_Px72(X,Y0))).
% 2.10/2.27 all X (cC6xcomp(X)<-> -(exists Y ra_Px72(X,Y))).
% 2.10/2.27 all X (cC60(X)<-> (exists Y (rR1(X,Y)&cC12xcomp(Y)))).
% 2.10/2.27 all X (cC62(X)<->cC60(X)&cC58xcomp(X)).
% 2.10/2.27 all X (cC64(X)<->cC8(X)&cC12(X)).
% 2.10/2.27 all X (cC64(X)<-> -(exists Y ra_Px22(X,Y))).
% 2.10/2.27 all X (cC64xcomp(X)<-> (exists Y0 ra_Px22(X,Y0))).
% 2.10/2.27 all X (cC66(X)<->cC12xcomp(X)&cC8xcomp(X)).
% 2.10/2.27 all X (cC66(X)<-> (exists Y0 ra_Px23(X,Y0))).
% 2.10/2.27 all X (cC66xcomp(X)<-> -(exists Y ra_Px23(X,Y))).
% 2.10/2.27 all X (cC68(X)<-> (exists Y0 ra_Px24(X,Y0))).
% 2.10/2.27 all X (cC68(X)<->cC64xcomp(X)&cC66xcomp(X)).
% 2.10/2.27 all X (cC68xcomp(X)<-> -(exists Y ra_Px24(X,Y))).
% 2.10/2.27 all X (cC70(X)<-> (exists Y (rR1(X,Y)&cC68xcomp(Y)))).
% 2.10/2.27 all X (cC70(X)<-> (exists Y0 ra_Px51(X,Y0))).
% 2.10/2.27 all X (cC70xcomp(X)<-> -(exists Y ra_Px51(X,Y))).
% 2.10/2.27 all X (cC72(X)<-> (exists Y (rR1(X,Y)&cC70(Y)))).
% 2.10/2.27 all X (cC72(X)<-> -(exists Y ra_Px58(X,Y))).
% 2.10/2.27 all X (cC72xcomp(X)<-> (exists Y0 ra_Px58(X,Y0))).
% 2.10/2.27 all X (cC74(X)<-> (exists Y (rR1(X,Y)&cC72(Y)))).
% 2.10/2.27 all X (cC74(X)<-> -(exists Y ra_Px25(X,Y))).
% 2.10/2.27 all X (cC74xcomp(X)<-> (exists Y0 ra_Px25(X,Y0))).
% 2.10/2.27 all X (cC76(X)<-> (exists Y0 ra_Px26(X,Y0))).
% 2.10/2.27 all X (cC76(X)<->cC74xcomp(X)&cC62(X)).
% 2.10/2.27 all X (cC76xcomp(X)<-> -(exists Y ra_Px26(X,Y))).
% 2.10/2.27 all X (cC78(X)<-> (exists Y (rR1(X,Y)&cC76xcomp(Y)))).
% 2.10/2.27 all X (cC78(X)<-> -(exists Y ra_Px28(X,Y))).
% 2.10/2.27 all X (cC78xcomp(X)<-> (exists Y0 ra_Px28(X,Y0))).
% 2.10/2.27 all X (cC8(X)<-> (exists Y0 ra_Px9(X,Y0))).
% 2.10/2.27 all X (cC8xcomp(X)<-> -(exists Y ra_Px9(X,Y))).
% 2.10/2.27 all X (cC80(X)<-> (exists Y (rR1(X,Y)&cC16xcomp(Y)))).
% 2.10/2.27 all X (cC82(X)<->cC80(X)&cC78xcomp(X)).
% 2.10/2.27 all X (cC84(X)<-> -(exists Y ra_Px31(X,Y))).
% 2.10/2.27 all X (cC84(X)<->cC2(X)&cC12(X)).
% 2.10/2.27 all X (cC84xcomp(X)<-> (exists Y0 ra_Px31(X,Y0))).
% 2.10/2.27 all X (cC86(X)<->cC12xcomp(X)&cC2xcomp(X)).
% 2.10/2.27 all X (cC86(X)<-> (exists Y0 ra_Px32(X,Y0))).
% 2.10/2.27 all X (cC86xcomp(X)<-> -(exists Y ra_Px32(X,Y))).
% 2.10/2.27 all X (cC88(X)<-> (exists Y0 ra_Px33(X,Y0))).
% 2.10/2.27 all X (cC88(X)<->cC84xcomp(X)&cC86xcomp(X)).
% 2.10/2.27 all X (cC88xcomp(X)<-> -(exists Y ra_Px33(X,Y))).
% 2.10/2.27 all X (cC90(X)<-> (exists Y0 ra_Px50(X,Y0))).
% 2.10/2.27 all X (cC90(X)<-> (exists Y (rR1(X,Y)&cC88xcomp(Y)))).
% 2.10/2.27 all X (cC90xcomp(X)<-> -(exists Y ra_Px50(X,Y))).
% 2.10/2.27 all X (cC92(X)<-> (exists Y0 ra_Px57(X,Y0))).
% 2.10/2.27 all X (cC92(X)<-> (exists Y (rR1(X,Y)&cC90(Y)))).
% 2.10/2.27 all X (cC92xcomp(X)<-> -(exists Y ra_Px57(X,Y))).
% 2.10/2.27 all X (cC94(X)<-> (exists Y (rR1(X,Y)&cC92(Y)))).
% 2.10/2.27 all X (cC94(X)<-> (exists Y0 ra_Px48(X,Y0))).
% 2.10/2.27 all X (cC94xcomp(X)<-> -(exists Y ra_Px48(X,Y))).
% 2.10/2.27 all X (cC96(X)<-> (exists Y (rR1(X,Y)&cC94(Y)))).
% 2.10/2.27 all X (cC96(X)<-> -(exists Y ra_Px34(X,Y))).
% 2.10/2.27 all X (cC96xcomp(X)<-> (exists Y0 ra_Px34(X,Y0))).
% 2.10/2.27 all X (cC98(X)<-> (exists Y0 ra_Px35(X,Y0))).
% 2.10/2.27 all X (cC98(X)<->cC96xcomp(X)&cC82(X)).
% 2.10/2.27 all X (cC98xcomp(X)<-> -(exists Y ra_Px35(X,Y))).
% 2.10/2.27 all X (cTEST(X)<->cC108(X)&cC130(X)).
% 2.10/2.27 all X (rR1(iV16439,X)->cC98(X)).
% 2.10/2.27 cowlThing(iV16439).
% 2.10/2.27 cC100xcomp(iV16439).
% 2.10/2.27 cTEST(iV16439).
% 2.10/2.27 rR1(iV16439,iV16440).
% 2.10/2.27 rR1(iV16439,iV16442).
% 2.10/2.27 rR1(iV16439,iV16441).
% 2.10/2.27 cowlThing(iV16440).
% 2.10/2.27 cC96xcomp(iV16440).
% 2.10/2.27 all X (rR1(iV16440,X)->cC94xcomp(X)).
% 2.10/2.27 all X (rR1(iV16440,X)->cC76(X)).
% 2.10/2.27 cC102xcomp(iV16440).
% 2.10/2.27 cC78xcomp(iV16440).
% 2.10/2.27 rR1(iV16440,iV16463).
% 2.10/2.27 cowlThing(iV16441).
% 2.10/2.27 cowlThing(iV16442).
% 2.10/2.27 cowlThing(iV16448).
% 2.10/2.27 cTOP(iV16448).
% 2.10/2.27 cC52xcomp(iV16448).
% 2.10/2.27 all X (rR1(iV16448,X)->cC50(X)).
% 2.10/2.27 all X (rR1(iV16448,X)->cC68(X)).
% 2.10/2.27 all X (rR1(iV16448,X)->cC34(X)).
% 2.10/2.27 cC36xcomp(iV16448).
% 2.10/2.27 cC90xcomp(iV16448).
% 2.10/2.27 all X (rR1(iV16448,X)->cC88(X)).
% 2.10/2.27 cC70xcomp(iV16448).
% 2.10/2.27 rR1(iV16448,iV16449).
% 2.10/2.27 cowlThing(iV16449).
% 2.10/2.27 cC74xcomp(iV16453).
% 2.10/2.27 cowlThing(iV16453).
% 2.10/2.27 all X (rR1(iV16453,X)->cC72xcomp(X)).
% 2.10/2.27 cC16xcomp(iV16453).
% 2.10/2.27 all X (rR1(iV16453,X)->cC56(X)).
% 2.10/2.27 all X (rR1(iV16453,X)->cC92xcomp(X)).
% 2.10/2.27 cC94xcomp(iV16453).
% 2.10/2.27 cC58xcomp(iV16453).
% 2.10/2.27 rR1(iV16453,iV16461).
% 2.10/2.27 all X (rR1(iV16455,X)->cC52xcomp(X)).
% 2.10/2.27 cowlThing(iV16455).
% 2.10/2.27 cC40xcomp(iV16455).
% 2.10/2.27 all X (rR1(iV16455,X)->cC90xcomp(X)).
% 2.10/2.27 cC12xcomp(iV16455).
% 2.10/2.27 all X (rR1(iV16455,X)->cC38(X)).
% 2.10/2.27 cC92xcomp(iV16455).
% 2.10/2.27 cC54xcomp(iV16455).
% 2.10/2.27 all X (rR1(iV16455,X)->cC70xcomp(X)).
% 2.10/2.27 cC72xcomp(iV16455).
% 2.10/2.27 rR1(iV16455,iV16460).
% 2.10/2.27 all X (rR1(iV16457,X)->cC68(X)).
% 2.10/2.27 cowlThing(iV16457).
% 2.10/2.27 all X (rR1(iV16457,X)->cC34(X)).
% 2.10/2.27 cTOP(iV16457).
% 2.10/2.27 cC52xcomp(iV16457).
% 2.10/2.27 cC8xcomp(iV16457).
% 2.10/2.27 all X (rR1(iV16457,X)->cC88(X)).
% 2.10/2.27 cC36xcomp(iV16457).
% 2.10/2.27 cC90xcomp(iV16457).
% 2.10/2.27 all X (rR1(iV16457,X)->cC50(X)).
% 2.10/2.27 cC70xcomp(iV16457).
% 2.10/2.27 cowlThing(iV16459).
% 2.10/2.27 cC14xcomp(iV16459).
% 2.10/2.27 cC8xcomp(iV16459).
% 2.10/2.27 cC10xcomp(iV16459).
% 2.10/2.27 cC30xcomp(iV16459).
% 2.10/2.27 cC84xcomp(iV16459).
% 2.10/2.27 cC12(iV16459).
% 2.10/2.27 cC46xcomp(iV16459).
% 2.10/2.27 cC64xcomp(iV16459).
% 2.10/2.27 cC4(iV16459).
% 2.10/2.27 cC86xcomp(iV16459).
% 2.10/2.27 cC32xcomp(iV16459).
% 2.10/2.27 cC48xcomp(iV16459).
% 2.10/2.27 cC18xcomp(iV16459).
% 2.10/2.27 cC2xcomp(iV16459).
% 2.10/2.27 cC6xcomp(iV16459).
% 2.10/2.27 cC66xcomp(iV16459).
% 2.10/2.27 all X (rR1(iV16460,X)->cC68(X)).
% 2.10/2.27 cowlThing(iV16460).
% 2.10/2.27 all X (rR1(iV16460,X)->cC34(X)).
% 2.10/2.27 cTOP(iV16460).
% 2.10/2.27 cC52xcomp(iV16460).
% 2.10/2.27 cC8xcomp(iV16460).
% 2.10/2.27 cC36xcomp(iV16460).
% 2.10/2.27 all X (rR1(iV16460,X)->cC50(X)).
% 2.10/2.27 all X (rR1(iV16460,X)->cC88(X)).
% 2.10/2.27 cC90xcomp(iV16460).
% 2.10/2.27 cC70xcomp(iV16460).
% 2.10/2.27 cowlThing(iV16461).
% 2.10/2.27 cC40xcomp(iV16461).
% 2.10/2.27 all X (rR1(iV16461,X)->cC90xcomp(X)).
% 2.10/2.27 all X (rR1(iV16461,X)->cC70xcomp(X)).
% 2.10/2.27 cC12xcomp(iV16461).
% 2.10/2.27 all X (rR1(iV16461,X)->cC52xcomp(X)).
% 2.10/2.27 cC92xcomp(iV16461).
% 2.10/2.27 cC54xcomp(iV16461).
% 2.10/2.27 all X (rR1(iV16461,X)->cC38(X)).
% 2.10/2.27 cC72xcomp(iV16461).
% 2.10/2.27 rR1(iV16461,iV16462).
% 2.10/2.27 all X (rR1(iV16462,X)->cC50(X)).
% 2.10/2.27 all X (rR1(iV16462,X)->cC68(X)).
% 2.10/2.27 cowlThing(iV16462).
% 2.10/2.27 cTOP(iV16462).
% 2.10/2.27 cC52xcomp(iV16462).
% 2.10/2.27 cC8xcomp(iV16462).
% 2.10/2.27 all X (rR1(iV16462,X)->cC34(X)).
% 2.10/2.27 all X (rR1(iV16462,X)->cC88(X)).
% 2.10/2.27 cC36xcomp(iV16462).
% 2.10/2.27 cC90xcomp(iV16462).
% 2.10/2.27 cC70xcomp(iV16462).
% 2.10/2.27 cC74xcomp(iV16463).
% 2.10/2.27 cowlThing(iV16463).
% 2.10/2.27 cC16xcomp(iV16463).
% 2.10/2.27 all X (rR1(iV16463,X)->cC92xcomp(X)).
% 2.10/2.27 all X (rR1(iV16463,X)->cC72xcomp(X)).
% 2.10/2.27 cC94xcomp(iV16463).
% 2.10/2.27 all X (rR1(iV16463,X)->cC56(X)).
% 2.10/2.27 cC58xcomp(iV16463).
% 2.10/2.27 rR1(iV16463,iV16464).
% 2.10/2.27 cowlThing(iV16464).
% 2.10/2.27 all X (rR1(iV16464,X)->cC38(X)).
% 2.10/2.27 cC40xcomp(iV16464).
% 2.10/2.27 cC12xcomp(iV16464).
% 2.10/2.27 all X (rR1(iV16464,X)->cC52xcomp(X)).
% 2.10/2.27 cC92xcomp(iV16464).
% 2.10/2.27 cC54xcomp(iV16464).
% 2.10/2.27 all X (rR1(iV16464,X)->cC90xcomp(X)).
% 2.10/2.27 all X (rR1(iV16464,X)->cC70xcomp(X)).
% 2.10/2.27 cC72xcomp(iV16464).
% 2.10/2.27 rR1(iV16464,iV16465).
% 2.10/2.27 all X (rR1(iV16465,X)->cC34(X)).
% 2.10/2.27 cowlThing(iV16465).
% 2.10/2.27 cTOP(iV16465).
% 2.10/2.27 all X (rR1(iV16465,X)->cC88(X)).
% 2.10/2.27 cC52xcomp(iV16465).
% 2.10/2.27 cC8xcomp(iV16465).
% 2.10/2.27 all X (rR1(iV16465,X)->cC68(X)).
% 2.10/2.27 cC36xcomp(iV16465).
% 2.10/2.27 cC90xcomp(iV16465).
% 2.10/2.27 all X (rR1(iV16465,X)->cC50(X)).
% 2.10/2.27 cC70xcomp(iV16465).
% 2.10/2.27 -((all X (cowlThing(X)& -cowlNothing(X)))& (all X (xsd_string(X)<-> -xsd_integer(X)))&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)).
% 2.10/2.27 end_of_list.
% 2.10/2.27
% 2.10/2.27 -------> usable clausifies to:
% 2.10/2.27
% 2.10/2.27 list(usable).
% 2.10/2.27 0 [] cowlThing(X).
% 2.10/2.27 0 [] -cowlNothing(X).
% 2.10/2.27 0 [] -xsd_string(X)| -xsd_integer(X).
% 2.10/2.27 0 [] xsd_string(X)|xsd_integer(X).
% 2.10/2.27 0 [] -cC10(X)|cC8(X).
% 2.10/2.27 0 [] -cC10(X)|cC6(X).
% 2.10/2.27 0 [] cC10(X)| -cC8(X)| -cC6(X).
% 2.10/2.27 0 [] -cC10(X)| -ra_Px73(X,Y).
% 2.10/2.27 0 [] cC10(X)|ra_Px73(X,$f1(X)).
% 2.10/2.27 0 [] -cC10xcomp(X)|ra_Px73(X,$f2(X)).
% 2.10/2.27 0 [] cC10xcomp(X)| -ra_Px73(X,Y0).
% 2.10/2.27 0 [] -cC100(X)|rR1(X,$f3(X)).
% 2.10/2.27 0 [] -cC100(X)|cC98xcomp($f3(X)).
% 2.10/2.27 0 [] cC100(X)| -rR1(X,Y)| -cC98xcomp(Y).
% 2.10/2.27 0 [] -cC100(X)| -ra_Px37(X,Y).
% 2.10/2.27 0 [] cC100(X)|ra_Px37(X,$f4(X)).
% 2.10/2.27 0 [] -cC100xcomp(X)|ra_Px37(X,$f5(X)).
% 2.10/2.27 0 [] cC100xcomp(X)| -ra_Px37(X,Y0).
% 2.10/2.27 0 [] -cC102(X)|ra_Px36(X,$f6(X)).
% 2.10/2.27 0 [] cC102(X)| -ra_Px36(X,Y0).
% 2.10/2.27 0 [] -cC102xcomp(X)| -ra_Px36(X,Y).
% 2.10/2.27 0 [] cC102xcomp(X)|ra_Px36(X,$f7(X)).
% 2.10/2.27 0 [] -cC104(X)|rR1(X,$f8(X)).
% 2.10/2.27 0 [] -cC104(X)|cC102xcomp($f8(X)).
% 2.10/2.27 0 [] cC104(X)| -rR1(X,Y)| -cC102xcomp(Y).
% 2.10/2.27 0 [] -cC106(X)|cC104(X).
% 2.10/2.27 0 [] -cC106(X)|cC100xcomp(X).
% 2.10/2.27 0 [] cC106(X)| -cC104(X)| -cC100xcomp(X).
% 2.10/2.27 0 [] -cC108(X)|cC28(X).
% 2.10/2.27 0 [] -cC108(X)|cC106(X).
% 2.10/2.27 0 [] cC108(X)| -cC28(X)| -cC106(X).
% 2.10/2.27 0 [] -cC110(X)|cC4xcomp(X).
% 2.10/2.27 0 [] -cC110(X)|cC12xcomp(X).
% 2.10/2.27 0 [] cC110(X)| -cC4xcomp(X)| -cC12xcomp(X).
% 2.10/2.27 0 [] -cC112(X)|cC110(X).
% 2.10/2.27 0 [] -cC112(X)|cC102xcomp(X).
% 2.10/2.27 0 [] cC112(X)| -cC110(X)| -cC102xcomp(X).
% 2.10/2.27 0 [] -cC114(X)|ra_Px41(X,$f9(X)).
% 2.10/2.27 0 [] cC114(X)| -ra_Px41(X,Y0).
% 2.10/2.27 0 [] -cC114xcomp(X)| -ra_Px41(X,Y).
% 2.10/2.27 0 [] cC114xcomp(X)|ra_Px41(X,$f10(X)).
% 2.10/2.27 0 [] -cC116(X)|cC112(X).
% 2.10/2.27 0 [] -cC116(X)|cC114xcomp(X).
% 2.10/2.27 0 [] cC116(X)| -cC112(X)| -cC114xcomp(X).
% 2.10/2.27 0 [] -cC118(X)|ra_Px42(X,$f11(X)).
% 2.10/2.27 0 [] cC118(X)| -ra_Px42(X,Y0).
% 2.10/2.27 0 [] -cC118xcomp(X)| -ra_Px42(X,Y).
% 2.10/2.27 0 [] cC118xcomp(X)|ra_Px42(X,$f12(X)).
% 2.10/2.27 0 [] -cC12(X)|ra_Px18(X,$f13(X)).
% 2.10/2.27 0 [] cC12(X)| -ra_Px18(X,Y0).
% 2.10/2.27 0 [] -cC12xcomp(X)| -ra_Px18(X,Y).
% 2.10/2.27 0 [] cC12xcomp(X)|ra_Px18(X,$f14(X)).
% 2.10/2.27 0 [] -cC120(X)|cC116(X).
% 2.10/2.27 0 [] -cC120(X)|cC118xcomp(X).
% 2.10/2.27 0 [] cC120(X)| -cC116(X)| -cC118xcomp(X).
% 2.10/2.27 0 [] -cC120(X)| -ra_Px43(X,Y).
% 2.10/2.27 0 [] cC120(X)|ra_Px43(X,$f15(X)).
% 2.10/2.27 0 [] -cC120xcomp(X)|ra_Px43(X,$f16(X)).
% 2.10/2.27 0 [] cC120xcomp(X)| -ra_Px43(X,Y0).
% 2.10/2.27 0 [] -cC122(X)|rR1(X,$f17(X)).
% 2.10/2.27 0 [] -cC122(X)|cC120xcomp($f17(X)).
% 2.10/2.27 0 [] cC122(X)| -rR1(X,Y)| -cC120xcomp(Y).
% 2.10/2.27 0 [] -cC124(X)|rR1(X,$f18(X)).
% 2.10/2.27 0 [] -cC124(X)|cC122($f18(X)).
% 2.10/2.27 0 [] cC124(X)| -rR1(X,Y)| -cC122(Y).
% 2.10/2.27 0 [] -cC126(X)|rR1(X,$f19(X)).
% 2.10/2.27 0 [] -cC126(X)|cC124($f19(X)).
% 2.10/2.27 0 [] cC126(X)| -rR1(X,Y)| -cC124(Y).
% 2.10/2.27 0 [] -cC128(X)|rR1(X,$f20(X)).
% 2.10/2.27 0 [] -cC128(X)|cC126($f20(X)).
% 2.10/2.27 0 [] cC128(X)| -rR1(X,Y)| -cC126(Y).
% 2.10/2.27 0 [] -cC130(X)|rR1(X,$f21(X)).
% 2.10/2.27 0 [] -cC130(X)|cC128($f21(X)).
% 2.10/2.27 0 [] cC130(X)| -rR1(X,Y)| -cC128(Y).
% 2.10/2.27 0 [] -cC14(X)|ra_Px74(X,$f22(X)).
% 2.10/2.27 0 [] cC14(X)| -ra_Px74(X,Y0).
% 2.10/2.27 0 [] -cC14(X)|cC10(X).
% 2.10/2.27 0 [] -cC14(X)|cC12(X).
% 2.10/2.27 0 [] cC14(X)| -cC10(X)| -cC12(X).
% 2.10/2.27 0 [] -cC14xcomp(X)| -ra_Px74(X,Y).
% 2.10/2.27 0 [] cC14xcomp(X)|ra_Px74(X,$f23(X)).
% 2.10/2.27 0 [] -cC16(X)|ra_Px27(X,$f24(X)).
% 2.10/2.27 0 [] cC16(X)| -ra_Px27(X,Y0).
% 2.10/2.27 0 [] -cC16xcomp(X)| -ra_Px27(X,Y).
% 2.10/2.27 0 [] cC16xcomp(X)|ra_Px27(X,$f25(X)).
% 2.10/2.27 0 [] -cC18(X)| -ra_Px1(X,Y).
% 2.10/2.27 0 [] cC18(X)|ra_Px1(X,$f26(X)).
% 2.10/2.27 0 [] -cC18(X)|cC14(X).
% 2.10/2.27 0 [] -cC18(X)|cC16(X).
% 2.10/2.27 0 [] cC18(X)| -cC14(X)| -cC16(X).
% 2.10/2.27 0 [] -cC18xcomp(X)|ra_Px1(X,$f27(X)).
% 2.10/2.27 0 [] cC18xcomp(X)| -ra_Px1(X,Y0).
% 2.10/2.27 0 [] -cC2(X)|ra_Px2(X,$f28(X)).
% 2.10/2.27 0 [] cC2(X)| -ra_Px2(X,Y0).
% 2.10/2.27 0 [] -cC2xcomp(X)| -ra_Px2(X,Y).
% 2.10/2.27 0 [] cC2xcomp(X)|ra_Px2(X,$f29(X)).
% 2.10/2.27 0 [] -cC20(X)|rR1(X,$f30(X)).
% 2.10/2.27 0 [] -cC20(X)|cC18xcomp($f30(X)).
% 2.10/2.27 0 [] cC20(X)| -rR1(X,Y)| -cC18xcomp(Y).
% 2.10/2.27 0 [] -cC22(X)|rR1(X,$f31(X)).
% 2.10/2.27 0 [] -cC22(X)|cC20($f31(X)).
% 2.10/2.27 0 [] cC22(X)| -rR1(X,Y)| -cC20(Y).
% 2.10/2.27 0 [] -cC24(X)|rR1(X,$f32(X)).
% 2.10/2.27 0 [] -cC24(X)|cC22($f32(X)).
% 2.10/2.27 0 [] cC24(X)| -rR1(X,Y)| -cC22(Y).
% 2.10/2.27 0 [] -cC26(X)|rR1(X,$f33(X)).
% 2.10/2.27 0 [] -cC26(X)|cC24($f33(X)).
% 2.10/2.27 0 [] cC26(X)| -rR1(X,Y)| -cC24(Y).
% 2.10/2.27 0 [] -cC28(X)|rR1(X,$f34(X)).
% 2.10/2.27 0 [] -cC28(X)|cC26($f34(X)).
% 2.10/2.27 0 [] cC28(X)| -rR1(X,Y)| -cC26(Y).
% 2.10/2.27 0 [] -cC30(X)| -ra_Px4(X,Y).
% 2.10/2.27 0 [] cC30(X)|ra_Px4(X,$f35(X)).
% 2.10/2.27 0 [] -cC30(X)|cC2(X).
% 2.10/2.27 0 [] -cC30(X)|cC4(X).
% 2.10/2.27 0 [] cC30(X)| -cC2(X)| -cC4(X).
% 2.10/2.27 0 [] -cC30xcomp(X)|ra_Px4(X,$f36(X)).
% 2.10/2.27 0 [] cC30xcomp(X)| -ra_Px4(X,Y0).
% 2.10/2.27 0 [] -cC32(X)|ra_Px5(X,$f37(X)).
% 2.10/2.27 0 [] cC32(X)| -ra_Px5(X,Y0).
% 2.10/2.27 0 [] -cC32(X)|cC4xcomp(X).
% 2.10/2.27 0 [] -cC32(X)|cC2xcomp(X).
% 2.10/2.27 0 [] cC32(X)| -cC4xcomp(X)| -cC2xcomp(X).
% 2.10/2.27 0 [] -cC32xcomp(X)| -ra_Px5(X,Y).
% 2.10/2.27 0 [] cC32xcomp(X)|ra_Px5(X,$f38(X)).
% 2.10/2.27 0 [] -cC34(X)|ra_Px6(X,$f39(X)).
% 2.10/2.27 0 [] cC34(X)| -ra_Px6(X,Y0).
% 2.10/2.27 0 [] -cC34(X)|cC30xcomp(X).
% 2.10/2.27 0 [] -cC34(X)|cC32xcomp(X).
% 2.10/2.27 0 [] cC34(X)| -cC30xcomp(X)| -cC32xcomp(X).
% 2.10/2.27 0 [] -cC34xcomp(X)| -ra_Px6(X,Y).
% 2.10/2.27 0 [] cC34xcomp(X)|ra_Px6(X,$f40(X)).
% 2.10/2.27 0 [] -cC36(X)| -ra_Px7(X,Y).
% 2.10/2.27 0 [] cC36(X)|ra_Px7(X,$f41(X)).
% 2.10/2.27 0 [] -cC36(X)|rR1(X,$f42(X)).
% 2.10/2.27 0 [] -cC36(X)|cC34xcomp($f42(X)).
% 2.10/2.27 0 [] cC36(X)| -rR1(X,Y)| -cC34xcomp(Y).
% 2.10/2.27 0 [] -cC36xcomp(X)|ra_Px7(X,$f43(X)).
% 2.10/2.27 0 [] cC36xcomp(X)| -ra_Px7(X,Y0).
% 2.10/2.27 0 [] -cC38(X)|cTOP(X).
% 2.10/2.27 0 [] -cC38(X)|cC36xcomp(X).
% 2.10/2.27 0 [] cC38(X)| -cTOP(X)| -cC36xcomp(X).
% 2.10/2.27 0 [] -cC38(X)|ra_Px8(X,$f44(X)).
% 2.10/2.27 0 [] cC38(X)| -ra_Px8(X,Y0).
% 2.10/2.27 0 [] -cC38xcomp(X)| -ra_Px8(X,Y).
% 2.10/2.27 0 [] cC38xcomp(X)|ra_Px8(X,$f45(X)).
% 2.10/2.27 0 [] -cC4(X)|ra_Px3(X,$f46(X)).
% 2.10/2.27 0 [] cC4(X)| -ra_Px3(X,Y0).
% 2.10/2.27 0 [] -cC4xcomp(X)| -ra_Px3(X,Y).
% 2.10/2.27 0 [] cC4xcomp(X)|ra_Px3(X,$f47(X)).
% 2.10/2.27 0 [] -cC40(X)| -ra_Px10(X,Y).
% 2.10/2.27 0 [] cC40(X)|ra_Px10(X,$f48(X)).
% 2.10/2.27 0 [] -cC40(X)|rR1(X,$f49(X)).
% 2.10/2.27 0 [] -cC40(X)|cC38xcomp($f49(X)).
% 2.10/2.27 0 [] cC40(X)| -rR1(X,Y)| -cC38xcomp(Y).
% 2.10/2.27 0 [] -cC40xcomp(X)|ra_Px10(X,$f50(X)).
% 2.10/2.27 0 [] cC40xcomp(X)| -ra_Px10(X,Y0).
% 2.10/2.27 0 [] -cC42(X)|rR1(X,$f51(X)).
% 2.10/2.27 0 [] -cC42(X)|cC8xcomp($f51(X)).
% 2.10/2.27 0 [] cC42(X)| -rR1(X,Y)| -cC8xcomp(Y).
% 2.10/2.27 0 [] -cC44(X)|cC40xcomp(X).
% 2.10/2.27 0 [] -cC44(X)|cC42(X).
% 2.10/2.27 0 [] cC44(X)| -cC40xcomp(X)| -cC42(X).
% 2.10/2.27 0 [] -cC46(X)| -ra_Px13(X,Y).
% 2.10/2.27 0 [] cC46(X)|ra_Px13(X,$f52(X)).
% 2.10/2.27 0 [] -cC46(X)|cC8(X).
% 2.10/2.27 0 [] -cC46(X)|cC4(X).
% 2.10/2.27 0 [] cC46(X)| -cC8(X)| -cC4(X).
% 2.10/2.27 0 [] -cC46xcomp(X)|ra_Px13(X,$f53(X)).
% 2.10/2.27 0 [] cC46xcomp(X)| -ra_Px13(X,Y0).
% 2.10/2.27 0 [] -cC48(X)|cC4xcomp(X).
% 2.10/2.27 0 [] -cC48(X)|cC8xcomp(X).
% 2.10/2.27 0 [] cC48(X)| -cC4xcomp(X)| -cC8xcomp(X).
% 2.10/2.27 0 [] -cC48(X)|ra_Px14(X,$f54(X)).
% 2.10/2.27 0 [] cC48(X)| -ra_Px14(X,Y0).
% 2.10/2.27 0 [] -cC48xcomp(X)| -ra_Px14(X,Y).
% 2.10/2.27 0 [] cC48xcomp(X)|ra_Px14(X,$f55(X)).
% 2.10/2.27 0 [] -cC50(X)|cC46xcomp(X).
% 2.10/2.27 0 [] -cC50(X)|cC48xcomp(X).
% 2.10/2.27 0 [] cC50(X)| -cC46xcomp(X)| -cC48xcomp(X).
% 2.10/2.27 0 [] -cC50(X)|ra_Px15(X,$f56(X)).
% 2.10/2.27 0 [] cC50(X)| -ra_Px15(X,Y0).
% 2.10/2.27 0 [] -cC50xcomp(X)| -ra_Px15(X,Y).
% 2.10/2.27 0 [] cC50xcomp(X)|ra_Px15(X,$f57(X)).
% 2.10/2.27 0 [] -cC52(X)| -ra_Px49(X,Y).
% 2.10/2.27 0 [] cC52(X)|ra_Px49(X,$f58(X)).
% 2.10/2.27 0 [] -cC52(X)|rR1(X,$f59(X)).
% 2.10/2.27 0 [] -cC52(X)|cC50xcomp($f59(X)).
% 2.10/2.27 0 [] cC52(X)| -rR1(X,Y)| -cC50xcomp(Y).
% 2.10/2.27 0 [] -cC52xcomp(X)|ra_Px49(X,$f60(X)).
% 2.10/2.27 0 [] cC52xcomp(X)| -ra_Px49(X,Y0).
% 2.10/2.27 0 [] -cC54(X)| -ra_Px16(X,Y).
% 2.10/2.27 0 [] cC54(X)|ra_Px16(X,$f61(X)).
% 2.10/2.27 0 [] -cC54(X)|rR1(X,$f62(X)).
% 2.10/2.27 0 [] -cC54(X)|cC52($f62(X)).
% 2.10/2.27 0 [] cC54(X)| -rR1(X,Y)| -cC52(Y).
% 2.10/2.27 0 [] -cC54xcomp(X)|ra_Px16(X,$f63(X)).
% 2.10/2.27 0 [] cC54xcomp(X)| -ra_Px16(X,Y0).
% 2.10/2.27 0 [] -cC56(X)|cC54xcomp(X).
% 2.10/2.27 0 [] -cC56(X)|cC44(X).
% 2.10/2.27 0 [] cC56(X)| -cC54xcomp(X)| -cC44(X).
% 2.10/2.27 0 [] -cC56(X)|ra_Px17(X,$f64(X)).
% 2.10/2.27 0 [] cC56(X)| -ra_Px17(X,Y0).
% 2.10/2.27 0 [] -cC56xcomp(X)| -ra_Px17(X,Y).
% 2.10/2.27 0 [] cC56xcomp(X)|ra_Px17(X,$f65(X)).
% 2.10/2.27 0 [] -cC58(X)|rR1(X,$f66(X)).
% 2.10/2.27 0 [] -cC58(X)|cC56xcomp($f66(X)).
% 2.10/2.27 0 [] cC58(X)| -rR1(X,Y)| -cC56xcomp(Y).
% 2.10/2.27 0 [] -cC58(X)| -ra_Px19(X,Y).
% 2.10/2.27 0 [] cC58(X)|ra_Px19(X,$f67(X)).
% 2.10/2.27 0 [] -cC58xcomp(X)|ra_Px19(X,$f68(X)).
% 2.10/2.27 0 [] cC58xcomp(X)| -ra_Px19(X,Y0).
% 2.10/2.27 0 [] -cC6(X)|cC2(X).
% 2.10/2.27 0 [] -cC6(X)|cC4(X).
% 2.10/2.27 0 [] cC6(X)| -cC2(X)| -cC4(X).
% 2.10/2.27 0 [] -cC6(X)|ra_Px72(X,$f69(X)).
% 2.10/2.27 0 [] cC6(X)| -ra_Px72(X,Y0).
% 2.10/2.27 0 [] -cC6xcomp(X)| -ra_Px72(X,Y).
% 2.10/2.27 0 [] cC6xcomp(X)|ra_Px72(X,$f70(X)).
% 2.10/2.27 0 [] -cC60(X)|rR1(X,$f71(X)).
% 2.10/2.27 0 [] -cC60(X)|cC12xcomp($f71(X)).
% 2.10/2.27 0 [] cC60(X)| -rR1(X,Y)| -cC12xcomp(Y).
% 2.10/2.27 0 [] -cC62(X)|cC60(X).
% 2.10/2.27 0 [] -cC62(X)|cC58xcomp(X).
% 2.10/2.27 0 [] cC62(X)| -cC60(X)| -cC58xcomp(X).
% 2.10/2.27 0 [] -cC64(X)|cC8(X).
% 2.10/2.27 0 [] -cC64(X)|cC12(X).
% 2.10/2.27 0 [] cC64(X)| -cC8(X)| -cC12(X).
% 2.10/2.27 0 [] -cC64(X)| -ra_Px22(X,Y).
% 2.10/2.27 0 [] cC64(X)|ra_Px22(X,$f72(X)).
% 2.10/2.27 0 [] -cC64xcomp(X)|ra_Px22(X,$f73(X)).
% 2.10/2.27 0 [] cC64xcomp(X)| -ra_Px22(X,Y0).
% 2.10/2.27 0 [] -cC66(X)|cC12xcomp(X).
% 2.10/2.27 0 [] -cC66(X)|cC8xcomp(X).
% 2.10/2.27 0 [] cC66(X)| -cC12xcomp(X)| -cC8xcomp(X).
% 2.10/2.27 0 [] -cC66(X)|ra_Px23(X,$f74(X)).
% 2.10/2.27 0 [] cC66(X)| -ra_Px23(X,Y0).
% 2.10/2.27 0 [] -cC66xcomp(X)| -ra_Px23(X,Y).
% 2.10/2.27 0 [] cC66xcomp(X)|ra_Px23(X,$f75(X)).
% 2.10/2.27 0 [] -cC68(X)|ra_Px24(X,$f76(X)).
% 2.10/2.27 0 [] cC68(X)| -ra_Px24(X,Y0).
% 2.10/2.27 0 [] -cC68(X)|cC64xcomp(X).
% 2.10/2.27 0 [] -cC68(X)|cC66xcomp(X).
% 2.10/2.27 0 [] cC68(X)| -cC64xcomp(X)| -cC66xcomp(X).
% 2.10/2.27 0 [] -cC68xcomp(X)| -ra_Px24(X,Y).
% 2.10/2.27 0 [] cC68xcomp(X)|ra_Px24(X,$f77(X)).
% 2.10/2.27 0 [] -cC70(X)|rR1(X,$f78(X)).
% 2.10/2.27 0 [] -cC70(X)|cC68xcomp($f78(X)).
% 2.10/2.27 0 [] cC70(X)| -rR1(X,Y)| -cC68xcomp(Y).
% 2.10/2.27 0 [] -cC70(X)|ra_Px51(X,$f79(X)).
% 2.10/2.27 0 [] cC70(X)| -ra_Px51(X,Y0).
% 2.10/2.27 0 [] -cC70xcomp(X)| -ra_Px51(X,Y).
% 2.10/2.27 0 [] cC70xcomp(X)|ra_Px51(X,$f80(X)).
% 2.10/2.27 0 [] -cC72(X)|rR1(X,$f81(X)).
% 2.10/2.27 0 [] -cC72(X)|cC70($f81(X)).
% 2.10/2.27 0 [] cC72(X)| -rR1(X,Y)| -cC70(Y).
% 2.10/2.27 0 [] -cC72(X)| -ra_Px58(X,Y).
% 2.10/2.27 0 [] cC72(X)|ra_Px58(X,$f82(X)).
% 2.10/2.27 0 [] -cC72xcomp(X)|ra_Px58(X,$f83(X)).
% 2.10/2.27 0 [] cC72xcomp(X)| -ra_Px58(X,Y0).
% 2.10/2.27 0 [] -cC74(X)|rR1(X,$f84(X)).
% 2.10/2.27 0 [] -cC74(X)|cC72($f84(X)).
% 2.10/2.27 0 [] cC74(X)| -rR1(X,Y)| -cC72(Y).
% 2.10/2.27 0 [] -cC74(X)| -ra_Px25(X,Y).
% 2.10/2.27 0 [] cC74(X)|ra_Px25(X,$f85(X)).
% 2.10/2.27 0 [] -cC74xcomp(X)|ra_Px25(X,$f86(X)).
% 2.10/2.27 0 [] cC74xcomp(X)| -ra_Px25(X,Y0).
% 2.10/2.27 0 [] -cC76(X)|ra_Px26(X,$f87(X)).
% 2.10/2.27 0 [] cC76(X)| -ra_Px26(X,Y0).
% 2.10/2.27 0 [] -cC76(X)|cC74xcomp(X).
% 2.10/2.27 0 [] -cC76(X)|cC62(X).
% 2.10/2.27 0 [] cC76(X)| -cC74xcomp(X)| -cC62(X).
% 2.10/2.27 0 [] -cC76xcomp(X)| -ra_Px26(X,Y).
% 2.10/2.27 0 [] cC76xcomp(X)|ra_Px26(X,$f88(X)).
% 2.10/2.27 0 [] -cC78(X)|rR1(X,$f89(X)).
% 2.10/2.27 0 [] -cC78(X)|cC76xcomp($f89(X)).
% 2.10/2.27 0 [] cC78(X)| -rR1(X,Y)| -cC76xcomp(Y).
% 2.10/2.27 0 [] -cC78(X)| -ra_Px28(X,Y).
% 2.10/2.27 0 [] cC78(X)|ra_Px28(X,$f90(X)).
% 2.10/2.27 0 [] -cC78xcomp(X)|ra_Px28(X,$f91(X)).
% 2.10/2.27 0 [] cC78xcomp(X)| -ra_Px28(X,Y0).
% 2.10/2.27 0 [] -cC8(X)|ra_Px9(X,$f92(X)).
% 2.10/2.27 0 [] cC8(X)| -ra_Px9(X,Y0).
% 2.10/2.27 0 [] -cC8xcomp(X)| -ra_Px9(X,Y).
% 2.10/2.27 0 [] cC8xcomp(X)|ra_Px9(X,$f93(X)).
% 2.10/2.27 0 [] -cC80(X)|rR1(X,$f94(X)).
% 2.10/2.27 0 [] -cC80(X)|cC16xcomp($f94(X)).
% 2.10/2.27 0 [] cC80(X)| -rR1(X,Y)| -cC16xcomp(Y).
% 2.10/2.27 0 [] -cC82(X)|cC80(X).
% 2.10/2.27 0 [] -cC82(X)|cC78xcomp(X).
% 2.10/2.27 0 [] cC82(X)| -cC80(X)| -cC78xcomp(X).
% 2.10/2.27 0 [] -cC84(X)| -ra_Px31(X,Y).
% 2.10/2.27 0 [] cC84(X)|ra_Px31(X,$f95(X)).
% 2.10/2.27 0 [] -cC84(X)|cC2(X).
% 2.10/2.27 0 [] -cC84(X)|cC12(X).
% 2.10/2.27 0 [] cC84(X)| -cC2(X)| -cC12(X).
% 2.10/2.27 0 [] -cC84xcomp(X)|ra_Px31(X,$f96(X)).
% 2.10/2.27 0 [] cC84xcomp(X)| -ra_Px31(X,Y0).
% 2.10/2.27 0 [] -cC86(X)|cC12xcomp(X).
% 2.10/2.27 0 [] -cC86(X)|cC2xcomp(X).
% 2.10/2.27 0 [] cC86(X)| -cC12xcomp(X)| -cC2xcomp(X).
% 2.10/2.27 0 [] -cC86(X)|ra_Px32(X,$f97(X)).
% 2.10/2.27 0 [] cC86(X)| -ra_Px32(X,Y0).
% 2.10/2.27 0 [] -cC86xcomp(X)| -ra_Px32(X,Y).
% 2.10/2.27 0 [] cC86xcomp(X)|ra_Px32(X,$f98(X)).
% 2.10/2.27 0 [] -cC88(X)|ra_Px33(X,$f99(X)).
% 2.10/2.27 0 [] cC88(X)| -ra_Px33(X,Y0).
% 2.10/2.27 0 [] -cC88(X)|cC84xcomp(X).
% 2.10/2.27 0 [] -cC88(X)|cC86xcomp(X).
% 2.10/2.27 0 [] cC88(X)| -cC84xcomp(X)| -cC86xcomp(X).
% 2.10/2.27 0 [] -cC88xcomp(X)| -ra_Px33(X,Y).
% 2.10/2.27 0 [] cC88xcomp(X)|ra_Px33(X,$f100(X)).
% 2.10/2.27 0 [] -cC90(X)|ra_Px50(X,$f101(X)).
% 2.10/2.27 0 [] cC90(X)| -ra_Px50(X,Y0).
% 2.10/2.27 0 [] -cC90(X)|rR1(X,$f102(X)).
% 2.10/2.27 0 [] -cC90(X)|cC88xcomp($f102(X)).
% 2.10/2.27 0 [] cC90(X)| -rR1(X,Y)| -cC88xcomp(Y).
% 2.10/2.27 0 [] -cC90xcomp(X)| -ra_Px50(X,Y).
% 2.10/2.27 0 [] cC90xcomp(X)|ra_Px50(X,$f103(X)).
% 2.10/2.27 0 [] -cC92(X)|ra_Px57(X,$f104(X)).
% 2.10/2.27 0 [] cC92(X)| -ra_Px57(X,Y0).
% 2.10/2.27 0 [] -cC92(X)|rR1(X,$f105(X)).
% 2.10/2.27 0 [] -cC92(X)|cC90($f105(X)).
% 2.10/2.27 0 [] cC92(X)| -rR1(X,Y)| -cC90(Y).
% 2.10/2.27 0 [] -cC92xcomp(X)| -ra_Px57(X,Y).
% 2.10/2.27 0 [] cC92xcomp(X)|ra_Px57(X,$f106(X)).
% 2.10/2.27 0 [] -cC94(X)|rR1(X,$f107(X)).
% 2.10/2.27 0 [] -cC94(X)|cC92($f107(X)).
% 2.10/2.27 0 [] cC94(X)| -rR1(X,Y)| -cC92(Y).
% 2.10/2.27 0 [] -cC94(X)|ra_Px48(X,$f108(X)).
% 2.10/2.27 0 [] cC94(X)| -ra_Px48(X,Y0).
% 2.10/2.27 0 [] -cC94xcomp(X)| -ra_Px48(X,Y).
% 2.10/2.27 0 [] cC94xcomp(X)|ra_Px48(X,$f109(X)).
% 2.10/2.27 0 [] -cC96(X)|rR1(X,$f110(X)).
% 2.10/2.27 0 [] -cC96(X)|cC94($f110(X)).
% 2.10/2.27 0 [] cC96(X)| -rR1(X,Y)| -cC94(Y).
% 2.10/2.27 0 [] -cC96(X)| -ra_Px34(X,Y).
% 2.10/2.27 0 [] cC96(X)|ra_Px34(X,$f111(X)).
% 2.10/2.27 0 [] -cC96xcomp(X)|ra_Px34(X,$f112(X)).
% 2.10/2.27 0 [] cC96xcomp(X)| -ra_Px34(X,Y0).
% 2.10/2.27 0 [] -cC98(X)|ra_Px35(X,$f113(X)).
% 2.10/2.27 0 [] cC98(X)| -ra_Px35(X,Y0).
% 2.10/2.27 0 [] -cC98(X)|cC96xcomp(X).
% 2.10/2.27 0 [] -cC98(X)|cC82(X).
% 2.10/2.27 0 [] cC98(X)| -cC96xcomp(X)| -cC82(X).
% 2.10/2.27 0 [] -cC98xcomp(X)| -ra_Px35(X,Y).
% 2.10/2.27 0 [] cC98xcomp(X)|ra_Px35(X,$f114(X)).
% 2.10/2.27 0 [] -cTEST(X)|cC108(X).
% 2.10/2.27 0 [] -cTEST(X)|cC130(X).
% 2.10/2.27 0 [] cTEST(X)| -cC108(X)| -cC130(X).
% 2.10/2.27 0 [] -rR1(iV16439,X)|cC98(X).
% 2.10/2.27 0 [] cowlThing(iV16439).
% 2.10/2.27 0 [] cC100xcomp(iV16439).
% 2.10/2.27 0 [] cTEST(iV16439).
% 2.10/2.27 0 [] rR1(iV16439,iV16440).
% 2.10/2.27 0 [] rR1(iV16439,iV16442).
% 2.10/2.27 0 [] rR1(iV16439,iV16441).
% 2.10/2.27 0 [] cowlThing(iV16440).
% 2.10/2.27 0 [] cC96xcomp(iV16440).
% 2.10/2.27 0 [] -rR1(iV16440,X)|cC94xcomp(X).
% 2.10/2.27 0 [] -rR1(iV16440,X)|cC76(X).
% 2.10/2.27 0 [] cC102xcomp(iV16440).
% 2.10/2.27 0 [] cC78xcomp(iV16440).
% 2.10/2.27 0 [] rR1(iV16440,iV16463).
% 2.10/2.27 0 [] cowlThing(iV16441).
% 2.10/2.27 0 [] cowlThing(iV16442).
% 2.10/2.27 0 [] cowlThing(iV16448).
% 2.10/2.27 0 [] cTOP(iV16448).
% 2.10/2.27 0 [] cC52xcomp(iV16448).
% 2.10/2.27 0 [] -rR1(iV16448,X)|cC50(X).
% 2.10/2.27 0 [] -rR1(iV16448,X)|cC68(X).
% 2.10/2.27 0 [] -rR1(iV16448,X)|cC34(X).
% 2.10/2.27 0 [] cC36xcomp(iV16448).
% 2.10/2.27 0 [] cC90xcomp(iV16448).
% 2.10/2.27 0 [] -rR1(iV16448,X)|cC88(X).
% 2.10/2.27 0 [] cC70xcomp(iV16448).
% 2.10/2.27 0 [] rR1(iV16448,iV16449).
% 2.10/2.27 0 [] cowlThing(iV16449).
% 2.10/2.27 0 [] cC74xcomp(iV16453).
% 2.10/2.27 0 [] cowlThing(iV16453).
% 2.10/2.27 0 [] -rR1(iV16453,X)|cC72xcomp(X).
% 2.10/2.27 0 [] cC16xcomp(iV16453).
% 2.10/2.27 0 [] -rR1(iV16453,X)|cC56(X).
% 2.10/2.27 0 [] -rR1(iV16453,X)|cC92xcomp(X).
% 2.10/2.27 0 [] cC94xcomp(iV16453).
% 2.10/2.27 0 [] cC58xcomp(iV16453).
% 2.10/2.27 0 [] rR1(iV16453,iV16461).
% 2.10/2.27 0 [] -rR1(iV16455,X)|cC52xcomp(X).
% 2.10/2.27 0 [] cowlThing(iV16455).
% 2.10/2.27 0 [] cC40xcomp(iV16455).
% 2.10/2.27 0 [] -rR1(iV16455,X)|cC90xcomp(X).
% 2.10/2.27 0 [] cC12xcomp(iV16455).
% 2.10/2.27 0 [] -rR1(iV16455,X)|cC38(X).
% 2.10/2.27 0 [] cC92xcomp(iV16455).
% 2.10/2.27 0 [] cC54xcomp(iV16455).
% 2.10/2.27 0 [] -rR1(iV16455,X)|cC70xcomp(X).
% 2.10/2.27 0 [] cC72xcomp(iV16455).
% 2.10/2.27 0 [] rR1(iV16455,iV16460).
% 2.10/2.27 0 [] -rR1(iV16457,X)|cC68(X).
% 2.10/2.27 0 [] cowlThing(iV16457).
% 2.10/2.27 0 [] -rR1(iV16457,X)|cC34(X).
% 2.10/2.27 0 [] cTOP(iV16457).
% 2.10/2.27 0 [] cC52xcomp(iV16457).
% 2.10/2.27 0 [] cC8xcomp(iV16457).
% 2.10/2.27 0 [] -rR1(iV16457,X)|cC88(X).
% 2.10/2.27 0 [] cC36xcomp(iV16457).
% 2.10/2.27 0 [] cC90xcomp(iV16457).
% 2.10/2.27 0 [] -rR1(iV16457,X)|cC50(X).
% 2.10/2.27 0 [] cC70xcomp(iV16457).
% 2.10/2.27 0 [] cowlThing(iV16459).
% 2.10/2.27 0 [] cC14xcomp(iV16459).
% 2.10/2.27 0 [] cC8xcomp(iV16459).
% 2.10/2.27 0 [] cC10xcomp(iV16459).
% 2.10/2.27 0 [] cC30xcomp(iV16459).
% 2.10/2.27 0 [] cC84xcomp(iV16459).
% 2.10/2.27 0 [] cC12(iV16459).
% 2.10/2.27 0 [] cC46xcomp(iV16459).
% 2.10/2.27 0 [] cC64xcomp(iV16459).
% 2.10/2.27 0 [] cC4(iV16459).
% 2.10/2.27 0 [] cC86xcomp(iV16459).
% 2.10/2.27 0 [] cC32xcomp(iV16459).
% 2.10/2.27 0 [] cC48xcomp(iV16459).
% 2.10/2.27 0 [] cC18xcomp(iV16459).
% 2.10/2.27 0 [] cC2xcomp(iV16459).
% 2.10/2.27 0 [] cC6xcomp(iV16459).
% 2.10/2.27 0 [] cC66xcomp(iV16459).
% 2.10/2.27 0 [] -rR1(iV16460,X)|cC68(X).
% 2.10/2.27 0 [] cowlThing(iV16460).
% 2.10/2.27 0 [] -rR1(iV16460,X)|cC34(X).
% 2.10/2.27 0 [] cTOP(iV16460).
% 2.10/2.27 0 [] cC52xcomp(iV16460).
% 2.10/2.27 0 [] cC8xcomp(iV16460).
% 2.10/2.27 0 [] cC36xcomp(iV16460).
% 2.10/2.27 0 [] -rR1(iV16460,X)|cC50(X).
% 2.10/2.27 0 [] -rR1(iV16460,X)|cC88(X).
% 2.10/2.27 0 [] cC90xcomp(iV16460).
% 2.10/2.27 0 [] cC70xcomp(iV16460).
% 2.10/2.27 0 [] cowlThing(iV16461).
% 2.10/2.27 0 [] cC40xcomp(iV16461).
% 2.10/2.27 0 [] -rR1(iV16461,X)|cC90xcomp(X).
% 2.10/2.27 0 [] -rR1(iV16461,X)|cC70xcomp(X).
% 2.10/2.27 0 [] cC12xcomp(iV16461).
% 2.10/2.27 0 [] -rR1(iV16461,X)|cC52xcomp(X).
% 2.10/2.27 0 [] cC92xcomp(iV16461).
% 2.10/2.27 0 [] cC54xcomp(iV16461).
% 2.10/2.27 0 [] -rR1(iV16461,X)|cC38(X).
% 2.10/2.27 0 [] cC72xcomp(iV16461).
% 2.10/2.27 0 [] rR1(iV16461,iV16462).
% 2.10/2.27 0 [] -rR1(iV16462,X)|cC50(X).
% 2.10/2.27 0 [] -rR1(iV16462,X)|cC68(X).
% 2.10/2.27 0 [] cowlThing(iV16462).
% 2.10/2.27 0 [] cTOP(iV16462).
% 2.10/2.27 0 [] cC52xcomp(iV16462).
% 2.10/2.27 0 [] cC8xcomp(iV16462).
% 2.10/2.27 0 [] -rR1(iV16462,X)|cC34(X).
% 2.10/2.27 0 [] -rR1(iV16462,X)|cC88(X).
% 2.10/2.27 0 [] cC36xcomp(iV16462).
% 2.10/2.27 0 [] cC90xcomp(iV16462).
% 2.10/2.27 0 [] cC70xcomp(iV16462).
% 2.10/2.27 0 [] cC74xcomp(iV16463).
% 2.10/2.27 0 [] cowlThing(iV16463).
% 2.10/2.27 0 [] cC16xcomp(iV16463).
% 2.10/2.27 0 [] -rR1(iV16463,X)|cC92xcomp(X).
% 2.10/2.27 0 [] -rR1(iV16463,X)|cC72xcomp(X).
% 2.10/2.27 0 [] cC94xcomp(iV16463).
% 2.10/2.27 0 [] -rR1(iV16463,X)|cC56(X).
% 2.10/2.27 0 [] cC58xcomp(iV16463).
% 2.10/2.27 0 [] rR1(iV16463,iV16464).
% 2.10/2.27 0 [] cowlThing(iV16464).
% 2.10/2.27 0 [] -rR1(iV16464,X)|cC38(X).
% 2.10/2.27 0 [] cC40xcomp(iV16464).
% 2.10/2.27 0 [] cC12xcomp(iV16464).
% 2.10/2.27 0 [] -rR1(iV16464,X)|cC52xcomp(X).
% 2.10/2.27 0 [] cC92xcomp(iV16464).
% 2.10/2.27 0 [] cC54xcomp(iV16464).
% 2.10/2.27 0 [] -rR1(iV16464,X)|cC90xcomp(X).
% 2.10/2.27 0 [] -rR1(iV16464,X)|cC70xcomp(X).
% 2.10/2.27 0 [] cC72xcomp(iV16464).
% 2.10/2.27 0 [] rR1(iV16464,iV16465).
% 2.10/2.27 0 [] -rR1(iV16465,X)|cC34(X).
% 2.10/2.27 0 [] cowlThing(iV16465).
% 2.10/2.27 0 [] cTOP(iV16465).
% 2.10/2.27 0 [] -rR1(iV16465,X)|cC88(X).
% 2.10/2.27 0 [] cC52xcomp(iV16465).
% 2.10/2.27 0 [] cC8xcomp(iV16465).
% 2.10/2.27 0 [] -rR1(iV16465,X)|cC68(X).
% 2.10/2.27 0 [] cC36xcomp(iV16465).
% 2.10/2.27 0 [] cC90xcomp(iV16465).
% 2.10/2.27 0 [] -rR1(iV16465,X)|cC50(X).
% 2.10/2.27 0 [] cC70xcomp(iV16465).
% 2.10/2.27 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)| -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).
% 2.10/2.27 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)| -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).
% 2.10/2.27 end_of_list.
% 2.10/2.27
% 2.10/2.27 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=49.
% 2.10/2.27
% 2.10/2.27 This is a non-Horn set without equality. The strategy will
% 2.10/2.27 be ordered hyper_res, unit deletion, and factoring, with
% 2.10/2.27 satellites in sos and with nuclei in usable.
% 2.10/2.27
% 2.10/2.27 dependent: set(hyper_res).
% 2.10/2.27 dependent: set(factor).
% 2.10/2.27 dependent: set(unit_deletion).
% 2.10/2.27
% 2.10/2.27 ------------> process usable:
% 2.10/2.27 ** KEPT (pick-wt=2): 1 [] -cowlNothing(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 2 [] -xsd_string(A)| -xsd_integer(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 3 [] -cC10(A)|cC8(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 4 [] -cC10(A)|cC6(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 5 [] cC10(A)| -cC8(A)| -cC6(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 6 [] -cC10(A)| -ra_Px73(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 7 [] -cC10xcomp(A)|ra_Px73(A,$f2(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 8 [] cC10xcomp(A)| -ra_Px73(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 9 [] -cC100(A)|rR1(A,$f3(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 10 [] -cC100(A)|cC98xcomp($f3(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 11 [] cC100(A)| -rR1(A,B)| -cC98xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=5): 12 [] -cC100(A)| -ra_Px37(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 13 [] -cC100xcomp(A)|ra_Px37(A,$f5(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 14 [] cC100xcomp(A)| -ra_Px37(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 15 [] -cC102(A)|ra_Px36(A,$f6(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 16 [] cC102(A)| -ra_Px36(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 17 [] -cC102xcomp(A)| -ra_Px36(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 18 [] -cC104(A)|rR1(A,$f8(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 19 [] -cC104(A)|cC102xcomp($f8(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 20 [] cC104(A)| -rR1(A,B)| -cC102xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=4): 21 [] -cC106(A)|cC104(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 22 [] -cC106(A)|cC100xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 23 [] cC106(A)| -cC104(A)| -cC100xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 24 [] -cC108(A)|cC28(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 25 [] -cC108(A)|cC106(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 26 [] cC108(A)| -cC28(A)| -cC106(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 27 [] -cC110(A)|cC4xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 28 [] -cC110(A)|cC12xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 29 [] cC110(A)| -cC4xcomp(A)| -cC12xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 30 [] -cC112(A)|cC110(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 31 [] -cC112(A)|cC102xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 32 [] cC112(A)| -cC110(A)| -cC102xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 33 [] -cC114(A)|ra_Px41(A,$f9(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 34 [] cC114(A)| -ra_Px41(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 35 [] -cC114xcomp(A)| -ra_Px41(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 36 [] -cC116(A)|cC112(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 37 [] -cC116(A)|cC114xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 38 [] cC116(A)| -cC112(A)| -cC114xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 39 [] -cC118(A)|ra_Px42(A,$f11(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 40 [] cC118(A)| -ra_Px42(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 41 [] -cC118xcomp(A)| -ra_Px42(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 42 [] -cC12(A)|ra_Px18(A,$f13(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 43 [] cC12(A)| -ra_Px18(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 44 [] -cC12xcomp(A)| -ra_Px18(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 45 [] -cC120(A)|cC116(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 46 [] -cC120(A)|cC118xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 47 [] cC120(A)| -cC116(A)| -cC118xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 48 [] -cC120(A)| -ra_Px43(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 49 [] -cC120xcomp(A)|ra_Px43(A,$f16(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 50 [] cC120xcomp(A)| -ra_Px43(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 51 [] -cC122(A)|rR1(A,$f17(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 52 [] -cC122(A)|cC120xcomp($f17(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 53 [] cC122(A)| -rR1(A,B)| -cC120xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 54 [] -cC124(A)|rR1(A,$f18(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 55 [] -cC124(A)|cC122($f18(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 56 [] cC124(A)| -rR1(A,B)| -cC122(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 57 [] -cC126(A)|rR1(A,$f19(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 58 [] -cC126(A)|cC124($f19(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 59 [] cC126(A)| -rR1(A,B)| -cC124(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 60 [] -cC128(A)|rR1(A,$f20(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 61 [] -cC128(A)|cC126($f20(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 62 [] cC128(A)| -rR1(A,B)| -cC126(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 63 [] -cC130(A)|rR1(A,$f21(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 64 [] -cC130(A)|cC128($f21(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 65 [] cC130(A)| -rR1(A,B)| -cC128(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 66 [] -cC14(A)|ra_Px74(A,$f22(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 67 [] cC14(A)| -ra_Px74(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 68 [] -cC14(A)|cC10(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 69 [] -cC14(A)|cC12(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 70 [] cC14(A)| -cC10(A)| -cC12(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 71 [] -cC14xcomp(A)| -ra_Px74(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 72 [] -cC16(A)|ra_Px27(A,$f24(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 73 [] cC16(A)| -ra_Px27(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 74 [] -cC16xcomp(A)| -ra_Px27(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 75 [] -cC18(A)| -ra_Px1(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 76 [] -cC18(A)|cC14(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 77 [] -cC18(A)|cC16(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 78 [] cC18(A)| -cC14(A)| -cC16(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 79 [] -cC18xcomp(A)|ra_Px1(A,$f27(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 80 [] cC18xcomp(A)| -ra_Px1(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 81 [] -cC2(A)|ra_Px2(A,$f28(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 82 [] cC2(A)| -ra_Px2(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 83 [] -cC2xcomp(A)| -ra_Px2(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 84 [] -cC20(A)|rR1(A,$f30(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 85 [] -cC20(A)|cC18xcomp($f30(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 86 [] cC20(A)| -rR1(A,B)| -cC18xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 87 [] -cC22(A)|rR1(A,$f31(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 88 [] -cC22(A)|cC20($f31(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 89 [] cC22(A)| -rR1(A,B)| -cC20(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 90 [] -cC24(A)|rR1(A,$f32(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 91 [] -cC24(A)|cC22($f32(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 92 [] cC24(A)| -rR1(A,B)| -cC22(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 93 [] -cC26(A)|rR1(A,$f33(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 94 [] -cC26(A)|cC24($f33(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 95 [] cC26(A)| -rR1(A,B)| -cC24(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 96 [] -cC28(A)|rR1(A,$f34(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 97 [] -cC28(A)|cC26($f34(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 98 [] cC28(A)| -rR1(A,B)| -cC26(B).
% 2.10/2.27 ** KEPT (pick-wt=5): 99 [] -cC30(A)| -ra_Px4(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 100 [] -cC30(A)|cC2(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 101 [] -cC30(A)|cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 102 [] cC30(A)| -cC2(A)| -cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 103 [] -cC30xcomp(A)|ra_Px4(A,$f36(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 104 [] cC30xcomp(A)| -ra_Px4(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 105 [] -cC32(A)|ra_Px5(A,$f37(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 106 [] cC32(A)| -ra_Px5(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 107 [] -cC32(A)|cC4xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 108 [] -cC32(A)|cC2xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 109 [] cC32(A)| -cC4xcomp(A)| -cC2xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 110 [] -cC32xcomp(A)| -ra_Px5(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 111 [] -cC34(A)|ra_Px6(A,$f39(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 112 [] cC34(A)| -ra_Px6(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 113 [] -cC34(A)|cC30xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 114 [] -cC34(A)|cC32xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 115 [] cC34(A)| -cC30xcomp(A)| -cC32xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 116 [] -cC34xcomp(A)| -ra_Px6(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 117 [] -cC36(A)| -ra_Px7(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 118 [] -cC36(A)|rR1(A,$f42(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 119 [] -cC36(A)|cC34xcomp($f42(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 120 [] cC36(A)| -rR1(A,B)| -cC34xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 121 [] -cC36xcomp(A)|ra_Px7(A,$f43(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 122 [] cC36xcomp(A)| -ra_Px7(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 123 [] -cC38(A)|cTOP(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 124 [] -cC38(A)|cC36xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 125 [] cC38(A)| -cTOP(A)| -cC36xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 126 [] -cC38(A)|ra_Px8(A,$f44(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 127 [] cC38(A)| -ra_Px8(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 128 [] -cC38xcomp(A)| -ra_Px8(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 129 [] -cC4(A)|ra_Px3(A,$f46(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 130 [] cC4(A)| -ra_Px3(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 131 [] -cC4xcomp(A)| -ra_Px3(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 132 [] -cC40(A)| -ra_Px10(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 133 [] -cC40(A)|rR1(A,$f49(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 134 [] -cC40(A)|cC38xcomp($f49(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 135 [] cC40(A)| -rR1(A,B)| -cC38xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 136 [] -cC40xcomp(A)|ra_Px10(A,$f50(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 137 [] cC40xcomp(A)| -ra_Px10(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 138 [] -cC42(A)|rR1(A,$f51(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 139 [] -cC42(A)|cC8xcomp($f51(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 140 [] cC42(A)| -rR1(A,B)| -cC8xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=4): 141 [] -cC44(A)|cC40xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 142 [] -cC44(A)|cC42(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 143 [] cC44(A)| -cC40xcomp(A)| -cC42(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 144 [] -cC46(A)| -ra_Px13(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 145 [] -cC46(A)|cC8(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 146 [] -cC46(A)|cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 147 [] cC46(A)| -cC8(A)| -cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 148 [] -cC46xcomp(A)|ra_Px13(A,$f53(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 149 [] cC46xcomp(A)| -ra_Px13(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 150 [] -cC48(A)|cC4xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 151 [] -cC48(A)|cC8xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 152 [] cC48(A)| -cC4xcomp(A)| -cC8xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 153 [] -cC48(A)|ra_Px14(A,$f54(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 154 [] cC48(A)| -ra_Px14(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 155 [] -cC48xcomp(A)| -ra_Px14(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 156 [] -cC50(A)|cC46xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 157 [] -cC50(A)|cC48xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 158 [] cC50(A)| -cC46xcomp(A)| -cC48xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 159 [] -cC50(A)|ra_Px15(A,$f56(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 160 [] cC50(A)| -ra_Px15(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 161 [] -cC50xcomp(A)| -ra_Px15(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 162 [] -cC52(A)| -ra_Px49(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 163 [] -cC52(A)|rR1(A,$f59(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 164 [] -cC52(A)|cC50xcomp($f59(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 165 [] cC52(A)| -rR1(A,B)| -cC50xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 166 [] -cC52xcomp(A)|ra_Px49(A,$f60(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 167 [] cC52xcomp(A)| -ra_Px49(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 168 [] -cC54(A)| -ra_Px16(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 169 [] -cC54(A)|rR1(A,$f62(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 170 [] -cC54(A)|cC52($f62(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 171 [] cC54(A)| -rR1(A,B)| -cC52(B).
% 2.10/2.27 ** KEPT (pick-wt=6): 172 [] -cC54xcomp(A)|ra_Px16(A,$f63(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 173 [] cC54xcomp(A)| -ra_Px16(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 174 [] -cC56(A)|cC54xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 175 [] -cC56(A)|cC44(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 176 [] cC56(A)| -cC54xcomp(A)| -cC44(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 177 [] -cC56(A)|ra_Px17(A,$f64(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 178 [] cC56(A)| -ra_Px17(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 179 [] -cC56xcomp(A)| -ra_Px17(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 180 [] -cC58(A)|rR1(A,$f66(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 181 [] -cC58(A)|cC56xcomp($f66(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 182 [] cC58(A)| -rR1(A,B)| -cC56xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=5): 183 [] -cC58(A)| -ra_Px19(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 184 [] -cC58xcomp(A)|ra_Px19(A,$f68(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 185 [] cC58xcomp(A)| -ra_Px19(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 186 [] -cC6(A)|cC2(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 187 [] -cC6(A)|cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 188 [] cC6(A)| -cC2(A)| -cC4(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 189 [] -cC6(A)|ra_Px72(A,$f69(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 190 [] cC6(A)| -ra_Px72(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 191 [] -cC6xcomp(A)| -ra_Px72(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 192 [] -cC60(A)|rR1(A,$f71(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 193 [] -cC60(A)|cC12xcomp($f71(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 194 [] cC60(A)| -rR1(A,B)| -cC12xcomp(B).
% 2.10/2.27 ** KEPT (pick-wt=4): 195 [] -cC62(A)|cC60(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 196 [] -cC62(A)|cC58xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 197 [] cC62(A)| -cC60(A)| -cC58xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 198 [] -cC64(A)|cC8(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 199 [] -cC64(A)|cC12(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 200 [] cC64(A)| -cC8(A)| -cC12(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 201 [] -cC64(A)| -ra_Px22(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 202 [] -cC64xcomp(A)|ra_Px22(A,$f73(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 203 [] cC64xcomp(A)| -ra_Px22(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 204 [] -cC66(A)|cC12xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 205 [] -cC66(A)|cC8xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 206 [] cC66(A)| -cC12xcomp(A)| -cC8xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 207 [] -cC66(A)|ra_Px23(A,$f74(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 208 [] cC66(A)| -ra_Px23(A,B).
% 2.10/2.27 ** KEPT (pick-wt=5): 209 [] -cC66xcomp(A)| -ra_Px23(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 210 [] -cC68(A)|ra_Px24(A,$f76(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 211 [] cC68(A)| -ra_Px24(A,B).
% 2.10/2.27 ** KEPT (pick-wt=4): 212 [] -cC68(A)|cC64xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=4): 213 [] -cC68(A)|cC66xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=6): 214 [] cC68(A)| -cC64xcomp(A)| -cC66xcomp(A).
% 2.10/2.27 ** KEPT (pick-wt=5): 215 [] -cC68xcomp(A)| -ra_Px24(A,B).
% 2.10/2.27 ** KEPT (pick-wt=6): 216 [] -cC70(A)|rR1(A,$f78(A)).
% 2.10/2.27 ** KEPT (pick-wt=5): 217 [] -cC70(A)|cC68xcomp($f78(A)).
% 2.10/2.27 ** KEPT (pick-wt=7): 218 [] cC70(A)| -rR1(A,B)| -cC68xcomp(B).
% 2.10/2.28 ** KEPT (pick-wt=6): 219 [] -cC70(A)|ra_Px51(A,$f79(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 220 [] cC70(A)| -ra_Px51(A,B).
% 2.10/2.28 ** KEPT (pick-wt=5): 221 [] -cC70xcomp(A)| -ra_Px51(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 222 [] -cC72(A)|rR1(A,$f81(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 223 [] -cC72(A)|cC70($f81(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 224 [] cC72(A)| -rR1(A,B)| -cC70(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 225 [] -cC72(A)| -ra_Px58(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 226 [] -cC72xcomp(A)|ra_Px58(A,$f83(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 227 [] cC72xcomp(A)| -ra_Px58(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 228 [] -cC74(A)|rR1(A,$f84(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 229 [] -cC74(A)|cC72($f84(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 230 [] cC74(A)| -rR1(A,B)| -cC72(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 231 [] -cC74(A)| -ra_Px25(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 232 [] -cC74xcomp(A)|ra_Px25(A,$f86(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 233 [] cC74xcomp(A)| -ra_Px25(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 234 [] -cC76(A)|ra_Px26(A,$f87(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 235 [] cC76(A)| -ra_Px26(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 236 [] -cC76(A)|cC74xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 237 [] -cC76(A)|cC62(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 238 [] cC76(A)| -cC74xcomp(A)| -cC62(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 239 [] -cC76xcomp(A)| -ra_Px26(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 240 [] -cC78(A)|rR1(A,$f89(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 241 [] -cC78(A)|cC76xcomp($f89(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 242 [] cC78(A)| -rR1(A,B)| -cC76xcomp(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 243 [] -cC78(A)| -ra_Px28(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 244 [] -cC78xcomp(A)|ra_Px28(A,$f91(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 245 [] cC78xcomp(A)| -ra_Px28(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 246 [] -cC8(A)|ra_Px9(A,$f92(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 247 [] cC8(A)| -ra_Px9(A,B).
% 2.10/2.28 ** KEPT (pick-wt=5): 248 [] -cC8xcomp(A)| -ra_Px9(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 249 [] -cC80(A)|rR1(A,$f94(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 250 [] -cC80(A)|cC16xcomp($f94(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 251 [] cC80(A)| -rR1(A,B)| -cC16xcomp(B).
% 2.10/2.28 ** KEPT (pick-wt=4): 252 [] -cC82(A)|cC80(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 253 [] -cC82(A)|cC78xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 254 [] cC82(A)| -cC80(A)| -cC78xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 255 [] -cC84(A)| -ra_Px31(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 256 [] -cC84(A)|cC2(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 257 [] -cC84(A)|cC12(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 258 [] cC84(A)| -cC2(A)| -cC12(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 259 [] -cC84xcomp(A)|ra_Px31(A,$f96(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 260 [] cC84xcomp(A)| -ra_Px31(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 261 [] -cC86(A)|cC12xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 262 [] -cC86(A)|cC2xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 263 [] cC86(A)| -cC12xcomp(A)| -cC2xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 264 [] -cC86(A)|ra_Px32(A,$f97(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 265 [] cC86(A)| -ra_Px32(A,B).
% 2.10/2.28 ** KEPT (pick-wt=5): 266 [] -cC86xcomp(A)| -ra_Px32(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 267 [] -cC88(A)|ra_Px33(A,$f99(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 268 [] cC88(A)| -ra_Px33(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 269 [] -cC88(A)|cC84xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 270 [] -cC88(A)|cC86xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 271 [] cC88(A)| -cC84xcomp(A)| -cC86xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 272 [] -cC88xcomp(A)| -ra_Px33(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 273 [] -cC90(A)|ra_Px50(A,$f101(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 274 [] cC90(A)| -ra_Px50(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 275 [] -cC90(A)|rR1(A,$f102(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 276 [] -cC90(A)|cC88xcomp($f102(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 277 [] cC90(A)| -rR1(A,B)| -cC88xcomp(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 278 [] -cC90xcomp(A)| -ra_Px50(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 279 [] -cC92(A)|ra_Px57(A,$f104(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 280 [] cC92(A)| -ra_Px57(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 281 [] -cC92(A)|rR1(A,$f105(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 282 [] -cC92(A)|cC90($f105(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 283 [] cC92(A)| -rR1(A,B)| -cC90(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 284 [] -cC92xcomp(A)| -ra_Px57(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 285 [] -cC94(A)|rR1(A,$f107(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 286 [] -cC94(A)|cC92($f107(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 287 [] cC94(A)| -rR1(A,B)| -cC92(B).
% 2.10/2.28 ** KEPT (pick-wt=6): 288 [] -cC94(A)|ra_Px48(A,$f108(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 289 [] cC94(A)| -ra_Px48(A,B).
% 2.10/2.28 ** KEPT (pick-wt=5): 290 [] -cC94xcomp(A)| -ra_Px48(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 291 [] -cC96(A)|rR1(A,$f110(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 292 [] -cC96(A)|cC94($f110(A)).
% 2.10/2.28 ** KEPT (pick-wt=7): 293 [] cC96(A)| -rR1(A,B)| -cC94(B).
% 2.10/2.28 ** KEPT (pick-wt=5): 294 [] -cC96(A)| -ra_Px34(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 295 [] -cC96xcomp(A)|ra_Px34(A,$f112(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 296 [] cC96xcomp(A)| -ra_Px34(A,B).
% 2.10/2.28 ** KEPT (pick-wt=6): 297 [] -cC98(A)|ra_Px35(A,$f113(A)).
% 2.10/2.28 ** KEPT (pick-wt=5): 298 [] cC98(A)| -ra_Px35(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 299 [] -cC98(A)|cC96xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 300 [] -cC98(A)|cC82(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 301 [] cC98(A)| -cC96xcomp(A)| -cC82(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 302 [] -cC98xcomp(A)| -ra_Px35(A,B).
% 2.10/2.28 ** KEPT (pick-wt=4): 303 [] -cTEST(A)|cC108(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 304 [] -cTEST(A)|cC130(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 305 [] cTEST(A)| -cC108(A)| -cC130(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 306 [] -rR1(iV16439,A)|cC98(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 307 [] -rR1(iV16440,A)|cC94xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 308 [] -rR1(iV16440,A)|cC76(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 309 [] -rR1(iV16448,A)|cC50(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 310 [] -rR1(iV16448,A)|cC68(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 311 [] -rR1(iV16448,A)|cC34(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 312 [] -rR1(iV16448,A)|cC88(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 313 [] -rR1(iV16453,A)|cC72xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 314 [] -rR1(iV16453,A)|cC56(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 315 [] -rR1(iV16453,A)|cC92xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 316 [] -rR1(iV16455,A)|cC52xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 317 [] -rR1(iV16455,A)|cC90xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 318 [] -rR1(iV16455,A)|cC38(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 319 [] -rR1(iV16455,A)|cC70xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 320 [] -rR1(iV16457,A)|cC68(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 321 [] -rR1(iV16457,A)|cC34(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 322 [] -rR1(iV16457,A)|cC88(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 323 [] -rR1(iV16457,A)|cC50(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 324 [] -rR1(iV16460,A)|cC68(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 325 [] -rR1(iV16460,A)|cC34(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 326 [] -rR1(iV16460,A)|cC50(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 327 [] -rR1(iV16460,A)|cC88(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 328 [] -rR1(iV16461,A)|cC90xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 329 [] -rR1(iV16461,A)|cC70xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 330 [] -rR1(iV16461,A)|cC52xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 331 [] -rR1(iV16461,A)|cC38(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 332 [] -rR1(iV16462,A)|cC50(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 333 [] -rR1(iV16462,A)|cC68(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 334 [] -rR1(iV16462,A)|cC34(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 335 [] -rR1(iV16462,A)|cC88(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 336 [] -rR1(iV16463,A)|cC92xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 337 [] -rR1(iV16463,A)|cC72xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 338 [] -rR1(iV16463,A)|cC56(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 339 [] -rR1(iV16464,A)|cC38(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 340 [] -rR1(iV16464,A)|cC52xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 341 [] -rR1(iV16464,A)|cC90xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 342 [] -rR1(iV16464,A)|cC70xcomp(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 343 [] -rR1(iV16465,A)|cC34(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 344 [] -rR1(iV16465,A)|cC88(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 345 [] -rR1(iV16465,A)|cC68(A).
% 2.10/2.28 ** KEPT (pick-wt=5): 346 [] -rR1(iV16465,A)|cC50(A).
% 2.10/2.28 ** KEPT (pick-wt=96): 348 [copy,347,unit_del,1] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)| -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).
% 2.10/2.28 ** KEPT (pick-wt=96): 350 [copy,349,unit_del,1] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)| -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).
% 2.10/2.28
% 2.10/2.28 ------------> process sos:
% 2.10/2.28 ** KEPT (pick-wt=2): 351 [] cowlThing(A).
% 2.10/2.28 ** KEPT (pick-wt=4): 352 [] xsd_string(A)|xsd_integer(A).
% 2.10/2.28 ** KEPT (pick-wt=6): 353 [] cC10(A)|ra_Px73(A,$f1(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 354 [] cC100(A)|ra_Px37(A,$f4(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 355 [] cC102xcomp(A)|ra_Px36(A,$f7(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 356 [] cC114xcomp(A)|ra_Px41(A,$f10(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 357 [] cC118xcomp(A)|ra_Px42(A,$f12(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 358 [] cC12xcomp(A)|ra_Px18(A,$f14(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 359 [] cC120(A)|ra_Px43(A,$f15(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 360 [] cC14xcomp(A)|ra_Px74(A,$f23(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 361 [] cC16xcomp(A)|ra_Px27(A,$f25(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 362 [] cC18(A)|ra_Px1(A,$f26(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 363 [] cC2xcomp(A)|ra_Px2(A,$f29(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 364 [] cC30(A)|ra_Px4(A,$f35(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 365 [] cC32xcomp(A)|ra_Px5(A,$f38(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 366 [] cC34xcomp(A)|ra_Px6(A,$f40(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 367 [] cC36(A)|ra_Px7(A,$f41(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 368 [] cC38xcomp(A)|ra_Px8(A,$f45(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 369 [] cC4xcomp(A)|ra_Px3(A,$f47(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 370 [] cC40(A)|ra_Px10(A,$f48(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 371 [] cC46(A)|ra_Px13(A,$f52(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 372 [] cC48xcomp(A)|ra_Px14(A,$f55(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 373 [] cC50xcomp(A)|ra_Px15(A,$f57(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 374 [] cC52(A)|ra_Px49(A,$f58(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 375 [] cC54(A)|ra_Px16(A,$f61(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 376 [] cC56xcomp(A)|ra_Px17(A,$f65(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 377 [] cC58(A)|ra_Px19(A,$f67(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 378 [] cC6xcomp(A)|ra_Px72(A,$f70(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 379 [] cC64(A)|ra_Px22(A,$f72(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 380 [] cC66xcomp(A)|ra_Px23(A,$f75(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 381 [] cC68xcomp(A)|ra_Px24(A,$f77(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 382 [] cC70xcomp(A)|ra_Px51(A,$f80(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 383 [] cC72(A)|ra_Px58(A,$f82(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 384 [] cC74(A)|ra_Px25(A,$f85(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 385 [] cC76xcomp(A)|ra_Px26(A,$f88(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 386 [] cC78(A)|ra_Px28(A,$f90(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 387 [] cC8xcomp(A)|ra_Px9(A,$f93(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 388 [] cC84(A)|ra_Px31(A,$f95(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 389 [] cC86xcomp(A)|ra_Px32(A,$f98(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 390 [] cC88xcomp(A)|ra_Px33(A,$f100(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 391 [] cC90xcomp(A)|ra_Px50(A,$f103(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 392 [] cC92xcomp(A)|ra_Px57(A,$f106(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 393 [] cC94xcomp(A)|ra_Px48(A,$f109(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 394 [] cC96(A)|ra_Px34(A,$f111(A)).
% 2.10/2.28 ** KEPT (pick-wt=6): 395 [] cC98xcomp(A)|ra_Px35(A,$f114(A)).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16439).
% 2.10/2.28 ** KEPT (pick-wt=2): 396 [] cC100xcomp(iV16439).
% 2.10/2.28 ** KEPT (pick-wt=2): 397 [] cTEST(iV16439).
% 2.10/2.28 ** KEPT (pick-wt=3): 398 [] rR1(iV16439,iV16440).
% 2.10/2.28 ** KEPT (pick-wt=3): 399 [] rR1(iV16439,iV16442).
% 2.10/2.28 ** KEPT (pick-wt=3): 400 [] rR1(iV16439,iV16441).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16440).
% 2.10/2.28 ** KEPT (pick-wt=2): 401 [] cC96xcomp(iV16440).
% 2.10/2.28 ** KEPT (pick-wt=2): 402 [] cC102xcomp(iV16440).
% 2.10/2.28 ** KEPT (pick-wt=2): 403 [] cC78xcomp(iV16440).
% 2.10/2.28 ** KEPT (pick-wt=3): 404 [] rR1(iV16440,iV16463).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16441).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16442).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=2): 405 [] cTOP(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=2): 406 [] cC52xcomp(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=2): 407 [] cC36xcomp(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=2): 408 [] cC90xcomp(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=2): 409 [] cC70xcomp(iV16448).
% 2.10/2.28 ** KEPT (pick-wt=3): 410 [] rR1(iV16448,iV16449).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16449).
% 2.10/2.28 ** KEPT (pick-wt=2): 411 [] cC74xcomp(iV16453).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16453).
% 2.10/2.28 ** KEPT (pick-wt=2): 412 [] cC16xcomp(iV16453).
% 2.10/2.28 ** KEPT (pick-wt=2): 413 [] cC94xcomp(iV16453).
% 2.10/2.28 ** KEPT (pick-wt=2): 414 [] cC58xcomp(iV16453).
% 2.10/2.28 ** KEPT (pick-wt=3): 415 [] rR1(iV16453,iV16461).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=2): 416 [] cC40xcomp(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=2): 417 [] cC12xcomp(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=2): 418 [] cC92xcomp(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=2): 419 [] cC54xcomp(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=2): 420 [] cC72xcomp(iV16455).
% 2.10/2.28 ** KEPT (pick-wt=3): 421 [] rR1(iV16455,iV16460).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 422 [] cTOP(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 423 [] cC52xcomp(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 424 [] cC8xcomp(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 425 [] cC36xcomp(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 426 [] cC90xcomp(iV16457).
% 2.10/2.28 ** KEPT (pick-wt=2): 427 [] cC70xcomp(iV16457).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 428 [] cC14xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 429 [] cC8xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 430 [] cC10xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 431 [] cC30xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 432 [] cC84xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 433 [] cC12(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 434 [] cC46xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 435 [] cC64xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 436 [] cC4(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 437 [] cC86xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 438 [] cC32xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 439 [] cC48xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 440 [] cC18xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 441 [] cC2xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 442 [] cC6xcomp(iV16459).
% 2.10/2.28 ** KEPT (pick-wt=2): 443 [] cC66xcomp(iV16459).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 444 [] cTOP(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 445 [] cC52xcomp(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 446 [] cC8xcomp(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 447 [] cC36xcomp(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 448 [] cC90xcomp(iV16460).
% 2.10/2.28 ** KEPT (pick-wt=2): 449 [] cC70xcomp(iV16460).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=2): 450 [] cC40xcomp(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=2): 451 [] cC12xcomp(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=2): 452 [] cC92xcomp(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=2): 453 [] cC54xcomp(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=2): 454 [] cC72xcomp(iV16461).
% 2.10/2.28 ** KEPT (pick-wt=3): 455 [] rR1(iV16461,iV16462).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 456 [] cTOP(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 457 [] cC52xcomp(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 458 [] cC8xcomp(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 459 [] cC36xcomp(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 460 [] cC90xcomp(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 461 [] cC70xcomp(iV16462).
% 2.10/2.28 ** KEPT (pick-wt=2): 462 [] cC74xcomp(iV16463).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16463).
% 2.10/2.28 ** KEPT (pick-wt=2): 463 [] cC16xcomp(iV16463).
% 2.10/2.28 ** KEPT (pick-wt=2): 464 [] cC94xcomp(iV16463).
% 2.10/2.28 ** KEPT (pick-wt=2): 465 [] cC58xcomp(iV16463).
% 2.10/2.28 ** KEPT (pick-wt=3): 466 [] rR1(iV16463,iV16464).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=2): 467 [] cC40xcomp(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=2): 468 [] cC12xcomp(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=2): 469 [] cC92xcomp(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=2): 470 [] cC54xcomp(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=2): 471 [] cC72xcomp(iV16464).
% 2.10/2.28 ** KEPT (pick-wt=3): 472 [] rR1(iV16464,iV16465).
% 2.10/2.28 Following clause subsumed by 351 during input processing: 0 [] cowlThing(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 473 [] cTOP(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 474 [] cC52xcomp(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 475 [] cC8xcomp(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 476 [] cC36xcomp(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 477 [] cC90xcomp(iV16465).
% 2.10/2.28 ** KEPT (pick-wt=2): 478 [] cC70xcomp(iV16465).
% 2.10/2.28
% 2.10/2.28 ======= end of input processing =======
% 2.10/2.28
% 2.10/2.28 =========== start of search ===========
% 2.10/2.28
% 2.10/2.28
% 2.10/2.28 Resetting weight limit to 2.
% 2.10/2.28
% 2.10/2.28
% 2.10/2.28 Resetting weight limit to 2.
% 2.10/2.28
% 2.10/2.28 sos_size=116
% 2.10/2.28
% 2.10/2.28 -------- PROOF --------
% 2.10/2.28
% 2.10/2.28 -----> EMPTY CLAUSE at 0.02 sec ----> 562 [hyper,561,2,560] $F.
% 2.10/2.28
% 2.10/2.28 Length of proof is 36. Level of proof is 5.
% 2.10/2.28
% 2.10/2.28 ---------------- PROOF ----------------
% 2.10/2.28 % SZS status Theorem
% 2.10/2.28 % SZS output start Refutation
% See solution above
% 2.10/2.28 ------------ end of proof -------------
% 2.10/2.28
% 2.10/2.28
% 2.10/2.28 Search stopped by max_proofs option.
% 2.10/2.28
% 2.10/2.28
% 2.10/2.28 Search stopped by max_proofs option.
% 2.10/2.28
% 2.10/2.28 ============ end of search ============
% 2.10/2.28
% 2.10/2.28 -------------- statistics -------------
% 2.10/2.28 clauses given 173
% 2.10/2.28 clauses generated 369
% 2.10/2.28 clauses kept 559
% 2.10/2.28 clauses forward subsumed 88
% 2.10/2.28 clauses back subsumed 2
% 2.10/2.28 Kbytes malloced 4882
% 2.10/2.28
% 2.10/2.28 ----------- times (seconds) -----------
% 2.10/2.28 user CPU time 0.02 (0 hr, 0 min, 0 sec)
% 2.10/2.28 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 2.10/2.28 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 2.10/2.28
% 2.10/2.28 That finishes the proof of the theorem.
% 2.10/2.28
% 2.10/2.28 Process 32394 finished Wed Jul 27 03:25:28 2022
% 2.10/2.28 Otter interrupted
% 2.10/2.28 PROOF FOUND
%------------------------------------------------------------------------------