%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : KRS154+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n022.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:27 EDT 2022
% Result : Theorem 1.99s 2.19s
% Output : Refutation 1.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 26
% Syntax : Number of clauses : 39 ( 25 unt; 3 nHn; 37 RR)
% Number of literals : 103 ( 0 equ; 63 neg)
% Maximal clause size : 13 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 12 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ cowlNothing(A),
file('KRS154+1.p',unknown),
[] ).
cnf(2,axiom,
( ~ xsd_string(A)
| ~ xsd_integer(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(32,axiom,
( cC110(A)
| ~ cC102xcomp(A)
| ~ cC108xcomp(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(44,axiom,
( cC114(A)
| ~ cC112xcomp(A)
| ~ cC96xcomp(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(47,axiom,
( cC116(A)
| ~ cC114(A)
| ~ cC80(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(93,axiom,
( cC136(A)
| ~ cC134xcomp(A)
| ~ cC116(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(203,axiom,
( cC56(A)
| ~ cC4(A)
| ~ cC10xcomp(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(206,axiom,
( cC58(A)
| ~ cC34(A)
| ~ cC56(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(260,axiom,
( cC80(A)
| ~ cC78xcomp(A)
| ~ cC76xcomp(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(299,axiom,
( cC94(A)
| ~ cC86xcomp(A)
| ~ cC92xcomp(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(321,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
file('KRS154+1.p',unknown),
[] ).
cnf(322,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[321]),1]),
[iquote('copy,321,unit_del,1')] ).
cnf(323,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
file('KRS154+1.p',unknown),
[] ).
cnf(324,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[323]),1]),
[iquote('copy,323,unit_del,1')] ).
cnf(325,axiom,
cowlThing(A),
file('KRS154+1.p',unknown),
[] ).
cnf(326,axiom,
( xsd_string(A)
| xsd_integer(A) ),
file('KRS154+1.p',unknown),
[] ).
cnf(367,axiom,
cC102xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(368,axiom,
cC108xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(369,axiom,
cC4(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(371,axiom,
cC112xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(372,axiom,
cC76xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(373,axiom,
cC96xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(377,axiom,
cC78xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(378,axiom,
cC134xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(379,axiom,
cC86xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(380,axiom,
cC34(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(383,axiom,
cC10xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(384,axiom,
cC92xcomp(iV822576),
file('KRS154+1.p',unknown),
[] ).
cnf(385,plain,
cC110(iV822576),
inference(hyper,[status(thm)],[368,32,367]),
[iquote('hyper,368,32,367')] ).
cnf(386,plain,
cC114(iV822576),
inference(hyper,[status(thm)],[373,44,371]),
[iquote('hyper,373,44,371')] ).
cnf(389,plain,
cC80(iV822576),
inference(hyper,[status(thm)],[377,260,372]),
[iquote('hyper,377,260,372')] ).
cnf(401,plain,
cC56(iV822576),
inference(hyper,[status(thm)],[383,203,369]),
[iquote('hyper,383,203,369')] ).
cnf(405,plain,
cC94(iV822576),
inference(hyper,[status(thm)],[384,299,379]),
[iquote('hyper,384,299,379')] ).
cnf(407,plain,
cC116(iV822576),
inference(hyper,[status(thm)],[389,47,386]),
[iquote('hyper,389,47,386')] ).
cnf(410,plain,
cC58(iV822576),
inference(hyper,[status(thm)],[401,206,380]),
[iquote('hyper,401,206,380')] ).
cnf(413,plain,
cC136(iV822576),
inference(hyper,[status(thm)],[407,93,378]),
[iquote('hyper,407,93,378')] ).
cnf(414,plain,
xsd_integer(dollar_c2),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[413,324,325,326,410,407,386,325,405,389,385,401])]),
[iquote('hyper,413,324,325,326,410,407,386,325,405,389,385,401,factor_simp')] ).
cnf(415,plain,
xsd_string(dollar_c2),
inference(hyper,[status(thm)],[414,322,325,410,407,386,325,405,389,385,413,401]),
[iquote('hyper,414,322,325,410,407,386,325,405,389,385,413,401')] ).
cnf(416,plain,
$false,
inference(hyper,[status(thm)],[415,2,414]),
[iquote('hyper,415,2,414')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS154+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.13 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n022.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:33:20 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.99/2.17 ----- Otter 3.3f, August 2004 -----
% 1.99/2.17 The process was started by sandbox on n022.cluster.edu,
% 1.99/2.17 Wed Jul 27 03:33:20 2022
% 1.99/2.17 The command was "./otter". The process ID is 28770.
% 1.99/2.17
% 1.99/2.17 set(prolog_style_variables).
% 1.99/2.17 set(auto).
% 1.99/2.17 dependent: set(auto1).
% 1.99/2.17 dependent: set(process_input).
% 1.99/2.17 dependent: clear(print_kept).
% 1.99/2.17 dependent: clear(print_new_demod).
% 1.99/2.17 dependent: clear(print_back_demod).
% 1.99/2.17 dependent: clear(print_back_sub).
% 1.99/2.17 dependent: set(control_memory).
% 1.99/2.17 dependent: assign(max_mem, 12000).
% 1.99/2.17 dependent: assign(pick_given_ratio, 4).
% 1.99/2.17 dependent: assign(stats_level, 1).
% 1.99/2.17 dependent: assign(max_seconds, 10800).
% 1.99/2.17 clear(print_given).
% 1.99/2.17
% 1.99/2.17 formula_list(usable).
% 1.99/2.17 all X (cowlThing(X)& -cowlNothing(X)).
% 1.99/2.17 all X (xsd_string(X)<-> -xsd_integer(X)).
% 1.99/2.17 all X (cC10(X)<-> -(exists Y ra_Px16(X,Y))).
% 1.99/2.17 all X (cC10xcomp(X)<-> (exists Y0 ra_Px16(X,Y0))).
% 1.99/2.17 all X (cC100(X)<-> (exists Y (rR1(X,Y)&cC98(Y)))).
% 1.99/2.17 all X (cC100(X)<-> -(exists Y ra_Px49(X,Y))).
% 1.99/2.17 all X (cC100xcomp(X)<-> (exists Y0 ra_Px49(X,Y0))).
% 1.99/2.17 all X (cC102(X)<-> (exists Y0 ra_Px35(X,Y0))).
% 1.99/2.17 all X (cC102(X)<->cC34(X)&cC100(X)).
% 1.99/2.17 all X (cC102xcomp(X)<-> -(exists Y ra_Px35(X,Y))).
% 1.99/2.17 all X (cC104(X)<->cC4(X)&cC34(X)).
% 1.99/2.17 all X (cC106(X)<-> (exists Y (rR1(X,Y)&cC104(Y)))).
% 1.99/2.17 all X (cC108(X)<->cC34xcomp(X)&cC106(X)).
% 1.99/2.17 all X (cC108(X)<-> (exists Y0 ra_Px36(X,Y0))).
% 1.99/2.17 all X (cC108xcomp(X)<-> -(exists Y ra_Px36(X,Y))).
% 1.99/2.17 all X (cC110(X)<->cC102xcomp(X)&cC108xcomp(X)).
% 1.99/2.17 all X (cC110(X)<-> -(exists Y ra_Px37(X,Y))).
% 1.99/2.17 all X (cC110xcomp(X)<-> (exists Y0 ra_Px37(X,Y0))).
% 1.99/2.17 all X (cC112(X)<->cC4(X)&cC110xcomp(X)).
% 1.99/2.17 all X (cC112(X)<-> (exists Y0 ra_Px39(X,Y0))).
% 1.99/2.17 all X (cC112xcomp(X)<-> -(exists Y ra_Px39(X,Y))).
% 1.99/2.17 all X (cC114(X)<->cC112xcomp(X)&cC96xcomp(X)).
% 1.99/2.17 all X (cC116(X)<->cC114(X)&cC80(X)).
% 1.99/2.17 all X (cC118(X)<->cC4(X)&cC10xcomp(X)).
% 1.99/2.17 all X (cC12(X)<->cC10(X)&cC4xcomp(X)).
% 1.99/2.17 all X (cC12(X)<-> (exists Y0 ra_Px3(X,Y0))).
% 1.99/2.17 all X (cC12xcomp(X)<-> -(exists Y ra_Px3(X,Y))).
% 1.99/2.17 all X (cC120(X)<->cC118(X)&cC34(X)).
% 1.99/2.17 all X (cC122(X)<-> (exists Y (rR1(X,Y)&cC120(Y)))).
% 1.99/2.17 all X (cC124(X)<->cC4(X)&cC10xcomp(X)).
% 1.99/2.17 all X (cC126(X)<->cC34xcomp(X)&cC124(X)).
% 1.99/2.17 all X (cC128(X)<-> (exists Y (rR1(X,Y)&cC126(Y)))).
% 1.99/2.17 all X (cC130(X)<->cC128(X)&cC122(X)).
% 1.99/2.17 all X (cC130(X)<-> (exists Y0 ra_Px44(X,Y0))).
% 1.99/2.17 all X (cC130xcomp(X)<-> -(exists Y ra_Px44(X,Y))).
% 1.99/2.17 all X (cC132(X)<->cC2(X)&cC4xcomp(X)).
% 1.99/2.17 all X (cC132(X)<-> (exists Y0 ra_Px48(X,Y0))).
% 1.99/2.17 all X (cC132xcomp(X)<-> -(exists Y ra_Px48(X,Y))).
% 1.99/2.17 all X (cC134(X)<->cC130xcomp(X)&cC132(X)).
% 1.99/2.17 all X (cC134(X)<-> (exists Y0 ra_Px45(X,Y0))).
% 1.99/2.17 all X (cC134xcomp(X)<-> -(exists Y ra_Px45(X,Y))).
% 1.99/2.17 all X (cC136(X)<-> -(exists Y ra_Px46(X,Y))).
% 1.99/2.17 all X (cC136(X)<->cC134xcomp(X)&cC116(X)).
% 1.99/2.17 all X (cC136xcomp(X)<-> (exists Y0 ra_Px46(X,Y0))).
% 1.99/2.17 all X (cC138(X)<-> (exists Y (rR1(X,Y)&cC136xcomp(Y)))).
% 1.99/2.17 all X (cC138(X)<-> (exists Y0 ra_Px47(X,Y0))).
% 1.99/2.17 all X (cC138xcomp(X)<-> -(exists Y ra_Px47(X,Y))).
% 1.99/2.17 all X (cC14(X)<->cC12xcomp(X)&cC8xcomp(X)).
% 1.99/2.17 all X (cC140(X)<->cC74(X)&cC138xcomp(X)).
% 1.99/2.17 all X (cC16(X)<-> -(exists Y ra_Px4(X,Y))).
% 1.99/2.17 all X (cC16xcomp(X)<-> (exists Y0 ra_Px4(X,Y0))).
% 1.99/2.17 all X (cC18(X)<->cC2(X)&cC16xcomp(X)).
% 1.99/2.17 all X (cC18(X)<-> (exists Y0 ra_Px56(X,Y0))).
% 1.99/2.17 all X (cC18xcomp(X)<-> -(exists Y ra_Px56(X,Y))).
% 1.99/2.17 all X (cC2(X)<-> -(exists Y ra_Px22(X,Y))).
% 1.99/2.17 all X (cC2xcomp(X)<-> (exists Y0 ra_Px22(X,Y0))).
% 1.99/2.17 all X (cC20(X)<-> (exists Y (rR1(X,Y)&cC18(Y)))).
% 1.99/2.17 all X (cC22(X)<->cC16(X)&cC20(X)).
% 1.99/2.17 all X (cC22(X)<-> (exists Y0 ra_Px6(X,Y0))).
% 1.99/2.17 all X (cC22xcomp(X)<-> -(exists Y ra_Px6(X,Y))).
% 1.99/2.17 all X (cC24(X)<->cC16(X)&cC2(X)).
% 1.99/2.17 all X (cC26(X)<-> (exists Y (rR1(X,Y)&cC24(Y)))).
% 1.99/2.17 all X (cC28(X)<-> -(exists Y ra_Px7(X,Y))).
% 1.99/2.17 all X (cC28(X)<->cC26(X)&cC16xcomp(X)).
% 1.99/2.17 all X (cC28xcomp(X)<-> (exists Y0 ra_Px7(X,Y0))).
% 1.99/2.17 all X (cC30(X)<-> (exists Y0 ra_Px8(X,Y0))).
% 1.99/2.17 all X (cC30(X)<->cC22xcomp(X)&cC28xcomp(X)).
% 1.99/2.17 all X (cC30xcomp(X)<-> -(exists Y ra_Px8(X,Y))).
% 1.99/2.17 all X (cC32(X)<->cC2(X)&cC30xcomp(X)).
% 1.99/2.17 all X (cC32(X)<-> (exists Y0 ra_Px14(X,Y0))).
% 1.99/2.17 all X (cC32xcomp(X)<-> -(exists Y ra_Px14(X,Y))).
% 1.99/2.17 all X (cC34(X)<-> (exists Y0 ra_Px9(X,Y0))).
% 1.99/2.17 all X (cC34xcomp(X)<-> -(exists Y ra_Px9(X,Y))).
% 1.99/2.17 all X (cC36(X)<->cC34xcomp(X)&cC4(X)).
% 1.99/2.17 all X (cC38(X)<-> (exists Y (rR1(X,Y)&cC36(Y)))).
% 1.99/2.17 all X (cC4(X)<-> -(exists Y ra_Px1(X,Y))).
% 1.99/2.17 all X (cC4xcomp(X)<-> (exists Y0 ra_Px1(X,Y0))).
% 1.99/2.17 all X (cC40(X)<-> (exists Y0 ra_Px11(X,Y0))).
% 1.99/2.17 all X (cC40(X)<->cC34(X)&cC38(X)).
% 1.99/2.17 all X (cC40xcomp(X)<-> -(exists Y ra_Px11(X,Y))).
% 1.99/2.17 all X (cC42(X)<->cC4(X)&cC34(X)).
% 1.99/2.17 all X (cC44(X)<-> (exists Y (rR1(X,Y)&cC42(Y)))).
% 1.99/2.17 all X (cC46(X)<-> (exists Y0 ra_Px12(X,Y0))).
% 1.99/2.17 all X (cC46(X)<->cC34xcomp(X)&cC44(X)).
% 1.99/2.17 all X (cC46xcomp(X)<-> -(exists Y ra_Px12(X,Y))).
% 1.99/2.17 all X (cC48(X)<-> -(exists Y ra_Px13(X,Y))).
% 1.99/2.17 all X (cC48(X)<->cC40xcomp(X)&cC46xcomp(X)).
% 1.99/2.17 all X (cC48xcomp(X)<-> (exists Y0 ra_Px13(X,Y0))).
% 1.99/2.17 all X (cC50(X)<-> (exists Y0 ra_Px15(X,Y0))).
% 1.99/2.17 all X (cC50(X)<->cC4(X)&cC48xcomp(X)).
% 1.99/2.17 all X (cC50xcomp(X)<-> -(exists Y ra_Px15(X,Y))).
% 1.99/2.17 all X (cC52(X)<->cC32xcomp(X)&cC50xcomp(X)).
% 1.99/2.17 all X (cC54(X)<->cC14(X)&cC52(X)).
% 1.99/2.17 all X (cC56(X)<->cC4(X)&cC10xcomp(X)).
% 1.99/2.17 all X (cC58(X)<->cC34(X)&cC56(X)).
% 1.99/2.17 all X (cC6(X)<->cC2(X)&cC4xcomp(X)).
% 1.99/2.17 all X (cC60(X)<-> (exists Y (rR1(X,Y)&cC58(Y)))).
% 1.99/2.17 all X (cC62(X)<->cC4(X)&cC10xcomp(X)).
% 1.99/2.17 all X (cC64(X)<->cC34xcomp(X)&cC62(X)).
% 1.99/2.17 all X (cC66(X)<-> (exists Y (rR1(X,Y)&cC64(Y)))).
% 1.99/2.17 all X (cC68(X)<->cC66(X)&cC60(X)).
% 1.99/2.17 all X (cC68(X)<-> (exists Y0 ra_Px20(X,Y0))).
% 1.99/2.17 all X (cC68xcomp(X)<-> -(exists Y ra_Px20(X,Y))).
% 1.99/2.17 all X (cC70(X)<->cC2(X)&cC4xcomp(X)).
% 1.99/2.17 all X (cC72(X)<-> (exists Y0 ra_Px21(X,Y0))).
% 1.99/2.17 all X (cC72(X)<->cC70(X)&cC68xcomp(X)).
% 1.99/2.17 all X (cC72xcomp(X)<-> -(exists Y ra_Px21(X,Y))).
% 1.99/2.17 all X (cC74(X)<->cC54(X)&cC72xcomp(X)).
% 1.99/2.17 all X (cC76(X)<-> (exists Y0 ra_Px24(X,Y0))).
% 1.99/2.17 all X (cC76(X)<->cC4(X)&cC2xcomp(X)).
% 1.99/2.17 all X (cC76xcomp(X)<-> -(exists Y ra_Px24(X,Y))).
% 1.99/2.17 all X (cC78(X)<->cC10(X)&cC4xcomp(X)).
% 1.99/2.17 all X (cC78(X)<-> -(exists Y ra_Px25(X,Y))).
% 1.99/2.17 all X (cC78xcomp(X)<-> (exists Y0 ra_Px25(X,Y0))).
% 1.99/2.17 all X (cC8(X)<-> (exists Y0 ra_Px2(X,Y0))).
% 1.99/2.17 all X (cC8(X)<->cC4(X)&cC2xcomp(X)).
% 1.99/2.17 all X (cC8xcomp(X)<-> -(exists Y ra_Px2(X,Y))).
% 1.99/2.17 all X (cC80(X)<->cC78xcomp(X)&cC76xcomp(X)).
% 1.99/2.17 all X (cC82(X)<-> (exists Y0 ra_Px65(X,Y0))).
% 1.99/2.17 all X (cC82(X)<->cC2(X)&cC16xcomp(X)).
% 1.99/2.17 all X (cC82xcomp(X)<-> -(exists Y ra_Px65(X,Y))).
% 1.99/2.17 all X (cC84(X)<-> (exists Y0 ra_Px53(X,Y0))).
% 1.99/2.17 all X (cC84(X)<-> (exists Y (rR1(X,Y)&cC82(Y)))).
% 1.99/2.17 all X (cC84xcomp(X)<-> -(exists Y ra_Px53(X,Y))).
% 1.99/2.17 all X (cC86(X)<->cC16(X)&cC84(X)).
% 1.99/2.17 all X (cC86(X)<-> -(exists Y ra_Px28(X,Y))).
% 1.99/2.17 all X (cC86xcomp(X)<-> (exists Y0 ra_Px28(X,Y0))).
% 1.99/2.17 all X (cC88(X)<->cC16(X)&cC2(X)).
% 1.99/2.17 all X (cC88(X)<-> -(exists Y ra_Px64(X,Y))).
% 1.99/2.17 all X (cC88xcomp(X)<-> (exists Y0 ra_Px64(X,Y0))).
% 1.99/2.17 all X (cC90(X)<-> (exists Y (rR1(X,Y)&cC88(Y)))).
% 1.99/2.17 all X (cC90(X)<-> -(exists Y ra_Px52(X,Y))).
% 1.99/2.17 all X (cC90xcomp(X)<-> (exists Y0 ra_Px52(X,Y0))).
% 1.99/2.17 all X (cC92(X)<-> (exists Y0 ra_Px29(X,Y0))).
% 1.99/2.17 all X (cC92(X)<->cC90(X)&cC16xcomp(X)).
% 1.99/2.17 all X (cC92xcomp(X)<-> -(exists Y ra_Px29(X,Y))).
% 1.99/2.17 all X (cC94(X)<->cC86xcomp(X)&cC92xcomp(X)).
% 1.99/2.17 all X (cC94(X)<-> (exists Y0 ra_Px30(X,Y0))).
% 1.99/2.17 all X (cC94xcomp(X)<-> -(exists Y ra_Px30(X,Y))).
% 1.99/2.17 all X (cC96(X)<-> (exists Y0 ra_Px38(X,Y0))).
% 1.99/2.17 all X (cC96(X)<->cC2(X)&cC94xcomp(X)).
% 1.99/2.17 all X (cC96xcomp(X)<-> -(exists Y ra_Px38(X,Y))).
% 1.99/2.17 all X (cC98(X)<-> (exists Y0 ra_Px63(X,Y0))).
% 1.99/2.17 all X (cC98(X)<->cC34xcomp(X)&cC4(X)).
% 1.99/2.17 all X (cC98xcomp(X)<-> -(exists Y ra_Px63(X,Y))).
% 1.99/2.17 all X (cTEST(X)<->cC6(X)&cC140(X)).
% 1.99/2.17 cC16(iV822576).
% 1.99/2.17 cC102xcomp(iV822576).
% 1.99/2.17 cC108xcomp(iV822576).
% 1.99/2.17 cC4(iV822576).
% 1.99/2.17 cC18xcomp(iV822576).
% 1.99/2.17 cC112xcomp(iV822576).
% 1.99/2.17 cC76xcomp(iV822576).
% 1.99/2.17 cC96xcomp(iV822576).
% 1.99/2.17 cC132xcomp(iV822576).
% 1.99/2.17 cC100xcomp(iV822576).
% 1.99/2.17 all X (rR1(iV822576,X)->cC98xcomp(X)).
% 1.99/2.17 cC90xcomp(iV822576).
% 1.99/2.17 cC78xcomp(iV822576).
% 1.99/2.17 all X (rR1(iV822576,X)->cC82xcomp(X)).
% 1.99/2.17 cC134xcomp(iV822576).
% 1.99/2.17 cC86xcomp(iV822576).
% 1.99/2.17 cC34(iV822576).
% 1.99/2.17 cC84xcomp(iV822576).
% 1.99/2.17 all X (rR1(iV822576,X)->cC88xcomp(X)).
% 1.99/2.17 cC2(iV822576).
% 1.99/2.17 cowlThing(iV822576).
% 1.99/2.17 cC10xcomp(iV822576).
% 1.99/2.17 cC92xcomp(iV822576).
% 1.99/2.17 -((all X (cowlThing(X)& -cowlNothing(X)))& (all X (xsd_string(X)<-> -xsd_integer(X)))&cC58(iV822576)&cC116(iV822576)&cC114(iV822576)&cowlThing(iV822576)&cC94(iV822576)&cC80(iV822576)&cC110(iV822576)&cC136(iV822576)&cC56(iV822576)).
% 1.99/2.17 end_of_list.
% 1.99/2.17
% 1.99/2.17 -------> usable clausifies to:
% 1.99/2.17
% 1.99/2.17 list(usable).
% 1.99/2.17 0 [] cowlThing(X).
% 1.99/2.17 0 [] -cowlNothing(X).
% 1.99/2.17 0 [] -xsd_string(X)| -xsd_integer(X).
% 1.99/2.17 0 [] xsd_string(X)|xsd_integer(X).
% 1.99/2.17 0 [] -cC10(X)| -ra_Px16(X,Y).
% 1.99/2.17 0 [] cC10(X)|ra_Px16(X,$f1(X)).
% 1.99/2.17 0 [] -cC10xcomp(X)|ra_Px16(X,$f2(X)).
% 1.99/2.17 0 [] cC10xcomp(X)| -ra_Px16(X,Y0).
% 1.99/2.17 0 [] -cC100(X)|rR1(X,$f3(X)).
% 1.99/2.17 0 [] -cC100(X)|cC98($f3(X)).
% 1.99/2.17 0 [] cC100(X)| -rR1(X,Y)| -cC98(Y).
% 1.99/2.17 0 [] -cC100(X)| -ra_Px49(X,Y).
% 1.99/2.17 0 [] cC100(X)|ra_Px49(X,$f4(X)).
% 1.99/2.17 0 [] -cC100xcomp(X)|ra_Px49(X,$f5(X)).
% 1.99/2.17 0 [] cC100xcomp(X)| -ra_Px49(X,Y0).
% 1.99/2.17 0 [] -cC102(X)|ra_Px35(X,$f6(X)).
% 1.99/2.17 0 [] cC102(X)| -ra_Px35(X,Y0).
% 1.99/2.17 0 [] -cC102(X)|cC34(X).
% 1.99/2.17 0 [] -cC102(X)|cC100(X).
% 1.99/2.17 0 [] cC102(X)| -cC34(X)| -cC100(X).
% 1.99/2.17 0 [] -cC102xcomp(X)| -ra_Px35(X,Y).
% 1.99/2.17 0 [] cC102xcomp(X)|ra_Px35(X,$f7(X)).
% 1.99/2.17 0 [] -cC104(X)|cC4(X).
% 1.99/2.17 0 [] -cC104(X)|cC34(X).
% 1.99/2.17 0 [] cC104(X)| -cC4(X)| -cC34(X).
% 1.99/2.17 0 [] -cC106(X)|rR1(X,$f8(X)).
% 1.99/2.17 0 [] -cC106(X)|cC104($f8(X)).
% 1.99/2.17 0 [] cC106(X)| -rR1(X,Y)| -cC104(Y).
% 1.99/2.17 0 [] -cC108(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC108(X)|cC106(X).
% 1.99/2.17 0 [] cC108(X)| -cC34xcomp(X)| -cC106(X).
% 1.99/2.17 0 [] -cC108(X)|ra_Px36(X,$f9(X)).
% 1.99/2.17 0 [] cC108(X)| -ra_Px36(X,Y0).
% 1.99/2.17 0 [] -cC108xcomp(X)| -ra_Px36(X,Y).
% 1.99/2.17 0 [] cC108xcomp(X)|ra_Px36(X,$f10(X)).
% 1.99/2.17 0 [] -cC110(X)|cC102xcomp(X).
% 1.99/2.17 0 [] -cC110(X)|cC108xcomp(X).
% 1.99/2.17 0 [] cC110(X)| -cC102xcomp(X)| -cC108xcomp(X).
% 1.99/2.17 0 [] -cC110(X)| -ra_Px37(X,Y).
% 1.99/2.17 0 [] cC110(X)|ra_Px37(X,$f11(X)).
% 1.99/2.17 0 [] -cC110xcomp(X)|ra_Px37(X,$f12(X)).
% 1.99/2.17 0 [] cC110xcomp(X)| -ra_Px37(X,Y0).
% 1.99/2.17 0 [] -cC112(X)|cC4(X).
% 1.99/2.17 0 [] -cC112(X)|cC110xcomp(X).
% 1.99/2.17 0 [] cC112(X)| -cC4(X)| -cC110xcomp(X).
% 1.99/2.17 0 [] -cC112(X)|ra_Px39(X,$f13(X)).
% 1.99/2.17 0 [] cC112(X)| -ra_Px39(X,Y0).
% 1.99/2.17 0 [] -cC112xcomp(X)| -ra_Px39(X,Y).
% 1.99/2.17 0 [] cC112xcomp(X)|ra_Px39(X,$f14(X)).
% 1.99/2.17 0 [] -cC114(X)|cC112xcomp(X).
% 1.99/2.17 0 [] -cC114(X)|cC96xcomp(X).
% 1.99/2.17 0 [] cC114(X)| -cC112xcomp(X)| -cC96xcomp(X).
% 1.99/2.17 0 [] -cC116(X)|cC114(X).
% 1.99/2.17 0 [] -cC116(X)|cC80(X).
% 1.99/2.17 0 [] cC116(X)| -cC114(X)| -cC80(X).
% 1.99/2.17 0 [] -cC118(X)|cC4(X).
% 1.99/2.17 0 [] -cC118(X)|cC10xcomp(X).
% 1.99/2.17 0 [] cC118(X)| -cC4(X)| -cC10xcomp(X).
% 1.99/2.17 0 [] -cC12(X)|cC10(X).
% 1.99/2.17 0 [] -cC12(X)|cC4xcomp(X).
% 1.99/2.17 0 [] cC12(X)| -cC10(X)| -cC4xcomp(X).
% 1.99/2.17 0 [] -cC12(X)|ra_Px3(X,$f15(X)).
% 1.99/2.17 0 [] cC12(X)| -ra_Px3(X,Y0).
% 1.99/2.17 0 [] -cC12xcomp(X)| -ra_Px3(X,Y).
% 1.99/2.17 0 [] cC12xcomp(X)|ra_Px3(X,$f16(X)).
% 1.99/2.17 0 [] -cC120(X)|cC118(X).
% 1.99/2.17 0 [] -cC120(X)|cC34(X).
% 1.99/2.17 0 [] cC120(X)| -cC118(X)| -cC34(X).
% 1.99/2.17 0 [] -cC122(X)|rR1(X,$f17(X)).
% 1.99/2.17 0 [] -cC122(X)|cC120($f17(X)).
% 1.99/2.17 0 [] cC122(X)| -rR1(X,Y)| -cC120(Y).
% 1.99/2.17 0 [] -cC124(X)|cC4(X).
% 1.99/2.17 0 [] -cC124(X)|cC10xcomp(X).
% 1.99/2.17 0 [] cC124(X)| -cC4(X)| -cC10xcomp(X).
% 1.99/2.17 0 [] -cC126(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC126(X)|cC124(X).
% 1.99/2.17 0 [] cC126(X)| -cC34xcomp(X)| -cC124(X).
% 1.99/2.17 0 [] -cC128(X)|rR1(X,$f18(X)).
% 1.99/2.17 0 [] -cC128(X)|cC126($f18(X)).
% 1.99/2.17 0 [] cC128(X)| -rR1(X,Y)| -cC126(Y).
% 1.99/2.17 0 [] -cC130(X)|cC128(X).
% 1.99/2.17 0 [] -cC130(X)|cC122(X).
% 1.99/2.17 0 [] cC130(X)| -cC128(X)| -cC122(X).
% 1.99/2.17 0 [] -cC130(X)|ra_Px44(X,$f19(X)).
% 1.99/2.17 0 [] cC130(X)| -ra_Px44(X,Y0).
% 1.99/2.17 0 [] -cC130xcomp(X)| -ra_Px44(X,Y).
% 1.99/2.17 0 [] cC130xcomp(X)|ra_Px44(X,$f20(X)).
% 1.99/2.17 0 [] -cC132(X)|cC2(X).
% 1.99/2.17 0 [] -cC132(X)|cC4xcomp(X).
% 1.99/2.17 0 [] cC132(X)| -cC2(X)| -cC4xcomp(X).
% 1.99/2.17 0 [] -cC132(X)|ra_Px48(X,$f21(X)).
% 1.99/2.17 0 [] cC132(X)| -ra_Px48(X,Y0).
% 1.99/2.17 0 [] -cC132xcomp(X)| -ra_Px48(X,Y).
% 1.99/2.17 0 [] cC132xcomp(X)|ra_Px48(X,$f22(X)).
% 1.99/2.17 0 [] -cC134(X)|cC130xcomp(X).
% 1.99/2.17 0 [] -cC134(X)|cC132(X).
% 1.99/2.17 0 [] cC134(X)| -cC130xcomp(X)| -cC132(X).
% 1.99/2.17 0 [] -cC134(X)|ra_Px45(X,$f23(X)).
% 1.99/2.17 0 [] cC134(X)| -ra_Px45(X,Y0).
% 1.99/2.17 0 [] -cC134xcomp(X)| -ra_Px45(X,Y).
% 1.99/2.17 0 [] cC134xcomp(X)|ra_Px45(X,$f24(X)).
% 1.99/2.17 0 [] -cC136(X)| -ra_Px46(X,Y).
% 1.99/2.17 0 [] cC136(X)|ra_Px46(X,$f25(X)).
% 1.99/2.17 0 [] -cC136(X)|cC134xcomp(X).
% 1.99/2.17 0 [] -cC136(X)|cC116(X).
% 1.99/2.17 0 [] cC136(X)| -cC134xcomp(X)| -cC116(X).
% 1.99/2.17 0 [] -cC136xcomp(X)|ra_Px46(X,$f26(X)).
% 1.99/2.17 0 [] cC136xcomp(X)| -ra_Px46(X,Y0).
% 1.99/2.17 0 [] -cC138(X)|rR1(X,$f27(X)).
% 1.99/2.17 0 [] -cC138(X)|cC136xcomp($f27(X)).
% 1.99/2.17 0 [] cC138(X)| -rR1(X,Y)| -cC136xcomp(Y).
% 1.99/2.17 0 [] -cC138(X)|ra_Px47(X,$f28(X)).
% 1.99/2.17 0 [] cC138(X)| -ra_Px47(X,Y0).
% 1.99/2.17 0 [] -cC138xcomp(X)| -ra_Px47(X,Y).
% 1.99/2.17 0 [] cC138xcomp(X)|ra_Px47(X,$f29(X)).
% 1.99/2.17 0 [] -cC14(X)|cC12xcomp(X).
% 1.99/2.17 0 [] -cC14(X)|cC8xcomp(X).
% 1.99/2.17 0 [] cC14(X)| -cC12xcomp(X)| -cC8xcomp(X).
% 1.99/2.17 0 [] -cC140(X)|cC74(X).
% 1.99/2.17 0 [] -cC140(X)|cC138xcomp(X).
% 1.99/2.17 0 [] cC140(X)| -cC74(X)| -cC138xcomp(X).
% 1.99/2.17 0 [] -cC16(X)| -ra_Px4(X,Y).
% 1.99/2.17 0 [] cC16(X)|ra_Px4(X,$f30(X)).
% 1.99/2.17 0 [] -cC16xcomp(X)|ra_Px4(X,$f31(X)).
% 1.99/2.17 0 [] cC16xcomp(X)| -ra_Px4(X,Y0).
% 1.99/2.17 0 [] -cC18(X)|cC2(X).
% 1.99/2.17 0 [] -cC18(X)|cC16xcomp(X).
% 1.99/2.17 0 [] cC18(X)| -cC2(X)| -cC16xcomp(X).
% 1.99/2.17 0 [] -cC18(X)|ra_Px56(X,$f32(X)).
% 1.99/2.17 0 [] cC18(X)| -ra_Px56(X,Y0).
% 1.99/2.17 0 [] -cC18xcomp(X)| -ra_Px56(X,Y).
% 1.99/2.17 0 [] cC18xcomp(X)|ra_Px56(X,$f33(X)).
% 1.99/2.17 0 [] -cC2(X)| -ra_Px22(X,Y).
% 1.99/2.17 0 [] cC2(X)|ra_Px22(X,$f34(X)).
% 1.99/2.17 0 [] -cC2xcomp(X)|ra_Px22(X,$f35(X)).
% 1.99/2.17 0 [] cC2xcomp(X)| -ra_Px22(X,Y0).
% 1.99/2.17 0 [] -cC20(X)|rR1(X,$f36(X)).
% 1.99/2.17 0 [] -cC20(X)|cC18($f36(X)).
% 1.99/2.17 0 [] cC20(X)| -rR1(X,Y)| -cC18(Y).
% 1.99/2.17 0 [] -cC22(X)|cC16(X).
% 1.99/2.17 0 [] -cC22(X)|cC20(X).
% 1.99/2.17 0 [] cC22(X)| -cC16(X)| -cC20(X).
% 1.99/2.17 0 [] -cC22(X)|ra_Px6(X,$f37(X)).
% 1.99/2.17 0 [] cC22(X)| -ra_Px6(X,Y0).
% 1.99/2.17 0 [] -cC22xcomp(X)| -ra_Px6(X,Y).
% 1.99/2.17 0 [] cC22xcomp(X)|ra_Px6(X,$f38(X)).
% 1.99/2.17 0 [] -cC24(X)|cC16(X).
% 1.99/2.17 0 [] -cC24(X)|cC2(X).
% 1.99/2.17 0 [] cC24(X)| -cC16(X)| -cC2(X).
% 1.99/2.17 0 [] -cC26(X)|rR1(X,$f39(X)).
% 1.99/2.17 0 [] -cC26(X)|cC24($f39(X)).
% 1.99/2.17 0 [] cC26(X)| -rR1(X,Y)| -cC24(Y).
% 1.99/2.17 0 [] -cC28(X)| -ra_Px7(X,Y).
% 1.99/2.17 0 [] cC28(X)|ra_Px7(X,$f40(X)).
% 1.99/2.17 0 [] -cC28(X)|cC26(X).
% 1.99/2.17 0 [] -cC28(X)|cC16xcomp(X).
% 1.99/2.17 0 [] cC28(X)| -cC26(X)| -cC16xcomp(X).
% 1.99/2.17 0 [] -cC28xcomp(X)|ra_Px7(X,$f41(X)).
% 1.99/2.17 0 [] cC28xcomp(X)| -ra_Px7(X,Y0).
% 1.99/2.17 0 [] -cC30(X)|ra_Px8(X,$f42(X)).
% 1.99/2.17 0 [] cC30(X)| -ra_Px8(X,Y0).
% 1.99/2.17 0 [] -cC30(X)|cC22xcomp(X).
% 1.99/2.17 0 [] -cC30(X)|cC28xcomp(X).
% 1.99/2.17 0 [] cC30(X)| -cC22xcomp(X)| -cC28xcomp(X).
% 1.99/2.17 0 [] -cC30xcomp(X)| -ra_Px8(X,Y).
% 1.99/2.17 0 [] cC30xcomp(X)|ra_Px8(X,$f43(X)).
% 1.99/2.17 0 [] -cC32(X)|cC2(X).
% 1.99/2.17 0 [] -cC32(X)|cC30xcomp(X).
% 1.99/2.17 0 [] cC32(X)| -cC2(X)| -cC30xcomp(X).
% 1.99/2.17 0 [] -cC32(X)|ra_Px14(X,$f44(X)).
% 1.99/2.17 0 [] cC32(X)| -ra_Px14(X,Y0).
% 1.99/2.17 0 [] -cC32xcomp(X)| -ra_Px14(X,Y).
% 1.99/2.17 0 [] cC32xcomp(X)|ra_Px14(X,$f45(X)).
% 1.99/2.17 0 [] -cC34(X)|ra_Px9(X,$f46(X)).
% 1.99/2.17 0 [] cC34(X)| -ra_Px9(X,Y0).
% 1.99/2.17 0 [] -cC34xcomp(X)| -ra_Px9(X,Y).
% 1.99/2.17 0 [] cC34xcomp(X)|ra_Px9(X,$f47(X)).
% 1.99/2.17 0 [] -cC36(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC36(X)|cC4(X).
% 1.99/2.17 0 [] cC36(X)| -cC34xcomp(X)| -cC4(X).
% 1.99/2.17 0 [] -cC38(X)|rR1(X,$f48(X)).
% 1.99/2.17 0 [] -cC38(X)|cC36($f48(X)).
% 1.99/2.17 0 [] cC38(X)| -rR1(X,Y)| -cC36(Y).
% 1.99/2.17 0 [] -cC4(X)| -ra_Px1(X,Y).
% 1.99/2.17 0 [] cC4(X)|ra_Px1(X,$f49(X)).
% 1.99/2.17 0 [] -cC4xcomp(X)|ra_Px1(X,$f50(X)).
% 1.99/2.17 0 [] cC4xcomp(X)| -ra_Px1(X,Y0).
% 1.99/2.17 0 [] -cC40(X)|ra_Px11(X,$f51(X)).
% 1.99/2.17 0 [] cC40(X)| -ra_Px11(X,Y0).
% 1.99/2.17 0 [] -cC40(X)|cC34(X).
% 1.99/2.17 0 [] -cC40(X)|cC38(X).
% 1.99/2.17 0 [] cC40(X)| -cC34(X)| -cC38(X).
% 1.99/2.17 0 [] -cC40xcomp(X)| -ra_Px11(X,Y).
% 1.99/2.17 0 [] cC40xcomp(X)|ra_Px11(X,$f52(X)).
% 1.99/2.17 0 [] -cC42(X)|cC4(X).
% 1.99/2.17 0 [] -cC42(X)|cC34(X).
% 1.99/2.17 0 [] cC42(X)| -cC4(X)| -cC34(X).
% 1.99/2.17 0 [] -cC44(X)|rR1(X,$f53(X)).
% 1.99/2.17 0 [] -cC44(X)|cC42($f53(X)).
% 1.99/2.17 0 [] cC44(X)| -rR1(X,Y)| -cC42(Y).
% 1.99/2.17 0 [] -cC46(X)|ra_Px12(X,$f54(X)).
% 1.99/2.17 0 [] cC46(X)| -ra_Px12(X,Y0).
% 1.99/2.17 0 [] -cC46(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC46(X)|cC44(X).
% 1.99/2.17 0 [] cC46(X)| -cC34xcomp(X)| -cC44(X).
% 1.99/2.17 0 [] -cC46xcomp(X)| -ra_Px12(X,Y).
% 1.99/2.17 0 [] cC46xcomp(X)|ra_Px12(X,$f55(X)).
% 1.99/2.17 0 [] -cC48(X)| -ra_Px13(X,Y).
% 1.99/2.17 0 [] cC48(X)|ra_Px13(X,$f56(X)).
% 1.99/2.17 0 [] -cC48(X)|cC40xcomp(X).
% 1.99/2.17 0 [] -cC48(X)|cC46xcomp(X).
% 1.99/2.17 0 [] cC48(X)| -cC40xcomp(X)| -cC46xcomp(X).
% 1.99/2.17 0 [] -cC48xcomp(X)|ra_Px13(X,$f57(X)).
% 1.99/2.17 0 [] cC48xcomp(X)| -ra_Px13(X,Y0).
% 1.99/2.17 0 [] -cC50(X)|ra_Px15(X,$f58(X)).
% 1.99/2.17 0 [] cC50(X)| -ra_Px15(X,Y0).
% 1.99/2.17 0 [] -cC50(X)|cC4(X).
% 1.99/2.17 0 [] -cC50(X)|cC48xcomp(X).
% 1.99/2.17 0 [] cC50(X)| -cC4(X)| -cC48xcomp(X).
% 1.99/2.17 0 [] -cC50xcomp(X)| -ra_Px15(X,Y).
% 1.99/2.17 0 [] cC50xcomp(X)|ra_Px15(X,$f59(X)).
% 1.99/2.17 0 [] -cC52(X)|cC32xcomp(X).
% 1.99/2.17 0 [] -cC52(X)|cC50xcomp(X).
% 1.99/2.17 0 [] cC52(X)| -cC32xcomp(X)| -cC50xcomp(X).
% 1.99/2.17 0 [] -cC54(X)|cC14(X).
% 1.99/2.17 0 [] -cC54(X)|cC52(X).
% 1.99/2.17 0 [] cC54(X)| -cC14(X)| -cC52(X).
% 1.99/2.17 0 [] -cC56(X)|cC4(X).
% 1.99/2.17 0 [] -cC56(X)|cC10xcomp(X).
% 1.99/2.17 0 [] cC56(X)| -cC4(X)| -cC10xcomp(X).
% 1.99/2.17 0 [] -cC58(X)|cC34(X).
% 1.99/2.17 0 [] -cC58(X)|cC56(X).
% 1.99/2.17 0 [] cC58(X)| -cC34(X)| -cC56(X).
% 1.99/2.17 0 [] -cC6(X)|cC2(X).
% 1.99/2.17 0 [] -cC6(X)|cC4xcomp(X).
% 1.99/2.17 0 [] cC6(X)| -cC2(X)| -cC4xcomp(X).
% 1.99/2.17 0 [] -cC60(X)|rR1(X,$f60(X)).
% 1.99/2.17 0 [] -cC60(X)|cC58($f60(X)).
% 1.99/2.17 0 [] cC60(X)| -rR1(X,Y)| -cC58(Y).
% 1.99/2.17 0 [] -cC62(X)|cC4(X).
% 1.99/2.17 0 [] -cC62(X)|cC10xcomp(X).
% 1.99/2.17 0 [] cC62(X)| -cC4(X)| -cC10xcomp(X).
% 1.99/2.17 0 [] -cC64(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC64(X)|cC62(X).
% 1.99/2.17 0 [] cC64(X)| -cC34xcomp(X)| -cC62(X).
% 1.99/2.17 0 [] -cC66(X)|rR1(X,$f61(X)).
% 1.99/2.17 0 [] -cC66(X)|cC64($f61(X)).
% 1.99/2.17 0 [] cC66(X)| -rR1(X,Y)| -cC64(Y).
% 1.99/2.17 0 [] -cC68(X)|cC66(X).
% 1.99/2.17 0 [] -cC68(X)|cC60(X).
% 1.99/2.17 0 [] cC68(X)| -cC66(X)| -cC60(X).
% 1.99/2.17 0 [] -cC68(X)|ra_Px20(X,$f62(X)).
% 1.99/2.17 0 [] cC68(X)| -ra_Px20(X,Y0).
% 1.99/2.17 0 [] -cC68xcomp(X)| -ra_Px20(X,Y).
% 1.99/2.17 0 [] cC68xcomp(X)|ra_Px20(X,$f63(X)).
% 1.99/2.17 0 [] -cC70(X)|cC2(X).
% 1.99/2.17 0 [] -cC70(X)|cC4xcomp(X).
% 1.99/2.17 0 [] cC70(X)| -cC2(X)| -cC4xcomp(X).
% 1.99/2.17 0 [] -cC72(X)|ra_Px21(X,$f64(X)).
% 1.99/2.17 0 [] cC72(X)| -ra_Px21(X,Y0).
% 1.99/2.17 0 [] -cC72(X)|cC70(X).
% 1.99/2.17 0 [] -cC72(X)|cC68xcomp(X).
% 1.99/2.17 0 [] cC72(X)| -cC70(X)| -cC68xcomp(X).
% 1.99/2.17 0 [] -cC72xcomp(X)| -ra_Px21(X,Y).
% 1.99/2.17 0 [] cC72xcomp(X)|ra_Px21(X,$f65(X)).
% 1.99/2.17 0 [] -cC74(X)|cC54(X).
% 1.99/2.17 0 [] -cC74(X)|cC72xcomp(X).
% 1.99/2.17 0 [] cC74(X)| -cC54(X)| -cC72xcomp(X).
% 1.99/2.17 0 [] -cC76(X)|ra_Px24(X,$f66(X)).
% 1.99/2.17 0 [] cC76(X)| -ra_Px24(X,Y0).
% 1.99/2.17 0 [] -cC76(X)|cC4(X).
% 1.99/2.17 0 [] -cC76(X)|cC2xcomp(X).
% 1.99/2.17 0 [] cC76(X)| -cC4(X)| -cC2xcomp(X).
% 1.99/2.17 0 [] -cC76xcomp(X)| -ra_Px24(X,Y).
% 1.99/2.17 0 [] cC76xcomp(X)|ra_Px24(X,$f67(X)).
% 1.99/2.17 0 [] -cC78(X)|cC10(X).
% 1.99/2.17 0 [] -cC78(X)|cC4xcomp(X).
% 1.99/2.17 0 [] cC78(X)| -cC10(X)| -cC4xcomp(X).
% 1.99/2.17 0 [] -cC78(X)| -ra_Px25(X,Y).
% 1.99/2.17 0 [] cC78(X)|ra_Px25(X,$f68(X)).
% 1.99/2.17 0 [] -cC78xcomp(X)|ra_Px25(X,$f69(X)).
% 1.99/2.17 0 [] cC78xcomp(X)| -ra_Px25(X,Y0).
% 1.99/2.17 0 [] -cC8(X)|ra_Px2(X,$f70(X)).
% 1.99/2.17 0 [] cC8(X)| -ra_Px2(X,Y0).
% 1.99/2.17 0 [] -cC8(X)|cC4(X).
% 1.99/2.17 0 [] -cC8(X)|cC2xcomp(X).
% 1.99/2.17 0 [] cC8(X)| -cC4(X)| -cC2xcomp(X).
% 1.99/2.17 0 [] -cC8xcomp(X)| -ra_Px2(X,Y).
% 1.99/2.17 0 [] cC8xcomp(X)|ra_Px2(X,$f71(X)).
% 1.99/2.17 0 [] -cC80(X)|cC78xcomp(X).
% 1.99/2.17 0 [] -cC80(X)|cC76xcomp(X).
% 1.99/2.17 0 [] cC80(X)| -cC78xcomp(X)| -cC76xcomp(X).
% 1.99/2.17 0 [] -cC82(X)|ra_Px65(X,$f72(X)).
% 1.99/2.17 0 [] cC82(X)| -ra_Px65(X,Y0).
% 1.99/2.17 0 [] -cC82(X)|cC2(X).
% 1.99/2.17 0 [] -cC82(X)|cC16xcomp(X).
% 1.99/2.17 0 [] cC82(X)| -cC2(X)| -cC16xcomp(X).
% 1.99/2.17 0 [] -cC82xcomp(X)| -ra_Px65(X,Y).
% 1.99/2.17 0 [] cC82xcomp(X)|ra_Px65(X,$f73(X)).
% 1.99/2.17 0 [] -cC84(X)|ra_Px53(X,$f74(X)).
% 1.99/2.17 0 [] cC84(X)| -ra_Px53(X,Y0).
% 1.99/2.17 0 [] -cC84(X)|rR1(X,$f75(X)).
% 1.99/2.17 0 [] -cC84(X)|cC82($f75(X)).
% 1.99/2.17 0 [] cC84(X)| -rR1(X,Y)| -cC82(Y).
% 1.99/2.17 0 [] -cC84xcomp(X)| -ra_Px53(X,Y).
% 1.99/2.17 0 [] cC84xcomp(X)|ra_Px53(X,$f76(X)).
% 1.99/2.17 0 [] -cC86(X)|cC16(X).
% 1.99/2.17 0 [] -cC86(X)|cC84(X).
% 1.99/2.17 0 [] cC86(X)| -cC16(X)| -cC84(X).
% 1.99/2.17 0 [] -cC86(X)| -ra_Px28(X,Y).
% 1.99/2.17 0 [] cC86(X)|ra_Px28(X,$f77(X)).
% 1.99/2.17 0 [] -cC86xcomp(X)|ra_Px28(X,$f78(X)).
% 1.99/2.17 0 [] cC86xcomp(X)| -ra_Px28(X,Y0).
% 1.99/2.17 0 [] -cC88(X)|cC16(X).
% 1.99/2.17 0 [] -cC88(X)|cC2(X).
% 1.99/2.17 0 [] cC88(X)| -cC16(X)| -cC2(X).
% 1.99/2.17 0 [] -cC88(X)| -ra_Px64(X,Y).
% 1.99/2.17 0 [] cC88(X)|ra_Px64(X,$f79(X)).
% 1.99/2.17 0 [] -cC88xcomp(X)|ra_Px64(X,$f80(X)).
% 1.99/2.17 0 [] cC88xcomp(X)| -ra_Px64(X,Y0).
% 1.99/2.17 0 [] -cC90(X)|rR1(X,$f81(X)).
% 1.99/2.17 0 [] -cC90(X)|cC88($f81(X)).
% 1.99/2.17 0 [] cC90(X)| -rR1(X,Y)| -cC88(Y).
% 1.99/2.17 0 [] -cC90(X)| -ra_Px52(X,Y).
% 1.99/2.17 0 [] cC90(X)|ra_Px52(X,$f82(X)).
% 1.99/2.17 0 [] -cC90xcomp(X)|ra_Px52(X,$f83(X)).
% 1.99/2.17 0 [] cC90xcomp(X)| -ra_Px52(X,Y0).
% 1.99/2.17 0 [] -cC92(X)|ra_Px29(X,$f84(X)).
% 1.99/2.17 0 [] cC92(X)| -ra_Px29(X,Y0).
% 1.99/2.17 0 [] -cC92(X)|cC90(X).
% 1.99/2.17 0 [] -cC92(X)|cC16xcomp(X).
% 1.99/2.17 0 [] cC92(X)| -cC90(X)| -cC16xcomp(X).
% 1.99/2.17 0 [] -cC92xcomp(X)| -ra_Px29(X,Y).
% 1.99/2.17 0 [] cC92xcomp(X)|ra_Px29(X,$f85(X)).
% 1.99/2.17 0 [] -cC94(X)|cC86xcomp(X).
% 1.99/2.17 0 [] -cC94(X)|cC92xcomp(X).
% 1.99/2.17 0 [] cC94(X)| -cC86xcomp(X)| -cC92xcomp(X).
% 1.99/2.17 0 [] -cC94(X)|ra_Px30(X,$f86(X)).
% 1.99/2.17 0 [] cC94(X)| -ra_Px30(X,Y0).
% 1.99/2.17 0 [] -cC94xcomp(X)| -ra_Px30(X,Y).
% 1.99/2.17 0 [] cC94xcomp(X)|ra_Px30(X,$f87(X)).
% 1.99/2.17 0 [] -cC96(X)|ra_Px38(X,$f88(X)).
% 1.99/2.17 0 [] cC96(X)| -ra_Px38(X,Y0).
% 1.99/2.17 0 [] -cC96(X)|cC2(X).
% 1.99/2.17 0 [] -cC96(X)|cC94xcomp(X).
% 1.99/2.17 0 [] cC96(X)| -cC2(X)| -cC94xcomp(X).
% 1.99/2.17 0 [] -cC96xcomp(X)| -ra_Px38(X,Y).
% 1.99/2.17 0 [] cC96xcomp(X)|ra_Px38(X,$f89(X)).
% 1.99/2.17 0 [] -cC98(X)|ra_Px63(X,$f90(X)).
% 1.99/2.17 0 [] cC98(X)| -ra_Px63(X,Y0).
% 1.99/2.17 0 [] -cC98(X)|cC34xcomp(X).
% 1.99/2.17 0 [] -cC98(X)|cC4(X).
% 1.99/2.17 0 [] cC98(X)| -cC34xcomp(X)| -cC4(X).
% 1.99/2.17 0 [] -cC98xcomp(X)| -ra_Px63(X,Y).
% 1.99/2.17 0 [] cC98xcomp(X)|ra_Px63(X,$f91(X)).
% 1.99/2.17 0 [] -cTEST(X)|cC6(X).
% 1.99/2.17 0 [] -cTEST(X)|cC140(X).
% 1.99/2.17 0 [] cTEST(X)| -cC6(X)| -cC140(X).
% 1.99/2.17 0 [] cC16(iV822576).
% 1.99/2.17 0 [] cC102xcomp(iV822576).
% 1.99/2.17 0 [] cC108xcomp(iV822576).
% 1.99/2.17 0 [] cC4(iV822576).
% 1.99/2.17 0 [] cC18xcomp(iV822576).
% 1.99/2.17 0 [] cC112xcomp(iV822576).
% 1.99/2.17 0 [] cC76xcomp(iV822576).
% 1.99/2.17 0 [] cC96xcomp(iV822576).
% 1.99/2.17 0 [] cC132xcomp(iV822576).
% 1.99/2.17 0 [] cC100xcomp(iV822576).
% 1.99/2.17 0 [] -rR1(iV822576,X)|cC98xcomp(X).
% 1.99/2.17 0 [] cC90xcomp(iV822576).
% 1.99/2.17 0 [] cC78xcomp(iV822576).
% 1.99/2.17 0 [] -rR1(iV822576,X)|cC82xcomp(X).
% 1.99/2.17 0 [] cC134xcomp(iV822576).
% 1.99/2.17 0 [] cC86xcomp(iV822576).
% 1.99/2.17 0 [] cC34(iV822576).
% 1.99/2.17 0 [] cC84xcomp(iV822576).
% 1.99/2.17 0 [] -rR1(iV822576,X)|cC88xcomp(X).
% 1.99/2.17 0 [] cC2(iV822576).
% 1.99/2.17 0 [] cowlThing(iV822576).
% 1.99/2.17 0 [] cC10xcomp(iV822576).
% 1.99/2.17 0 [] cC92xcomp(iV822576).
% 1.99/2.17 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cC58(iV822576)| -cC116(iV822576)| -cC114(iV822576)| -cowlThing(iV822576)| -cC94(iV822576)| -cC80(iV822576)| -cC110(iV822576)| -cC136(iV822576)| -cC56(iV822576).
% 1.99/2.17 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cC58(iV822576)| -cC116(iV822576)| -cC114(iV822576)| -cowlThing(iV822576)| -cC94(iV822576)| -cC80(iV822576)| -cC110(iV822576)| -cC136(iV822576)| -cC56(iV822576).
% 1.99/2.18 end_of_list.
% 1.99/2.18
% 1.99/2.18 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=13.
% 1.99/2.18
% 1.99/2.18 This is a non-Horn set without equality. The strategy will
% 1.99/2.18 be ordered hyper_res, unit deletion, and factoring, with
% 1.99/2.18 satellites in sos and with nuclei in usable.
% 1.99/2.18
% 1.99/2.18 dependent: set(hyper_res).
% 1.99/2.18 dependent: set(factor).
% 1.99/2.18 dependent: set(unit_deletion).
% 1.99/2.18
% 1.99/2.18 ------------> process usable:
% 1.99/2.18 ** KEPT (pick-wt=2): 1 [] -cowlNothing(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 2 [] -xsd_string(A)| -xsd_integer(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 3 [] -cC10(A)| -ra_Px16(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 4 [] -cC10xcomp(A)|ra_Px16(A,$f2(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 5 [] cC10xcomp(A)| -ra_Px16(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 6 [] -cC100(A)|rR1(A,$f3(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 7 [] -cC100(A)|cC98($f3(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 8 [] cC100(A)| -rR1(A,B)| -cC98(B).
% 1.99/2.18 ** KEPT (pick-wt=5): 9 [] -cC100(A)| -ra_Px49(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 10 [] -cC100xcomp(A)|ra_Px49(A,$f5(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 11 [] cC100xcomp(A)| -ra_Px49(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 12 [] -cC102(A)|ra_Px35(A,$f6(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 13 [] cC102(A)| -ra_Px35(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 14 [] -cC102(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 15 [] -cC102(A)|cC100(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 16 [] cC102(A)| -cC34(A)| -cC100(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 17 [] -cC102xcomp(A)| -ra_Px35(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 18 [] -cC104(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 19 [] -cC104(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 20 [] cC104(A)| -cC4(A)| -cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 21 [] -cC106(A)|rR1(A,$f8(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 22 [] -cC106(A)|cC104($f8(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 23 [] cC106(A)| -rR1(A,B)| -cC104(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 24 [] -cC108(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 25 [] -cC108(A)|cC106(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 26 [] cC108(A)| -cC34xcomp(A)| -cC106(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 27 [] -cC108(A)|ra_Px36(A,$f9(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 28 [] cC108(A)| -ra_Px36(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 29 [] -cC108xcomp(A)| -ra_Px36(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 30 [] -cC110(A)|cC102xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 31 [] -cC110(A)|cC108xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 32 [] cC110(A)| -cC102xcomp(A)| -cC108xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 33 [] -cC110(A)| -ra_Px37(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 34 [] -cC110xcomp(A)|ra_Px37(A,$f12(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 35 [] cC110xcomp(A)| -ra_Px37(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 36 [] -cC112(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 37 [] -cC112(A)|cC110xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 38 [] cC112(A)| -cC4(A)| -cC110xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 39 [] -cC112(A)|ra_Px39(A,$f13(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 40 [] cC112(A)| -ra_Px39(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 41 [] -cC112xcomp(A)| -ra_Px39(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 42 [] -cC114(A)|cC112xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 43 [] -cC114(A)|cC96xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 44 [] cC114(A)| -cC112xcomp(A)| -cC96xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 45 [] -cC116(A)|cC114(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 46 [] -cC116(A)|cC80(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 47 [] cC116(A)| -cC114(A)| -cC80(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 48 [] -cC118(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 49 [] -cC118(A)|cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 50 [] cC118(A)| -cC4(A)| -cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 51 [] -cC12(A)|cC10(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 52 [] -cC12(A)|cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 53 [] cC12(A)| -cC10(A)| -cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 54 [] -cC12(A)|ra_Px3(A,$f15(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 55 [] cC12(A)| -ra_Px3(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 56 [] -cC12xcomp(A)| -ra_Px3(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 57 [] -cC120(A)|cC118(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 58 [] -cC120(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 59 [] cC120(A)| -cC118(A)| -cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 60 [] -cC122(A)|rR1(A,$f17(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 61 [] -cC122(A)|cC120($f17(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 62 [] cC122(A)| -rR1(A,B)| -cC120(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 63 [] -cC124(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 64 [] -cC124(A)|cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 65 [] cC124(A)| -cC4(A)| -cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 66 [] -cC126(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 67 [] -cC126(A)|cC124(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 68 [] cC126(A)| -cC34xcomp(A)| -cC124(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 69 [] -cC128(A)|rR1(A,$f18(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 70 [] -cC128(A)|cC126($f18(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 71 [] cC128(A)| -rR1(A,B)| -cC126(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 72 [] -cC130(A)|cC128(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 73 [] -cC130(A)|cC122(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 74 [] cC130(A)| -cC128(A)| -cC122(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 75 [] -cC130(A)|ra_Px44(A,$f19(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 76 [] cC130(A)| -ra_Px44(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 77 [] -cC130xcomp(A)| -ra_Px44(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 78 [] -cC132(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 79 [] -cC132(A)|cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 80 [] cC132(A)| -cC2(A)| -cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 81 [] -cC132(A)|ra_Px48(A,$f21(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 82 [] cC132(A)| -ra_Px48(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 83 [] -cC132xcomp(A)| -ra_Px48(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 84 [] -cC134(A)|cC130xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 85 [] -cC134(A)|cC132(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 86 [] cC134(A)| -cC130xcomp(A)| -cC132(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 87 [] -cC134(A)|ra_Px45(A,$f23(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 88 [] cC134(A)| -ra_Px45(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 89 [] -cC134xcomp(A)| -ra_Px45(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 90 [] -cC136(A)| -ra_Px46(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 91 [] -cC136(A)|cC134xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 92 [] -cC136(A)|cC116(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 93 [] cC136(A)| -cC134xcomp(A)| -cC116(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 94 [] -cC136xcomp(A)|ra_Px46(A,$f26(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 95 [] cC136xcomp(A)| -ra_Px46(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 96 [] -cC138(A)|rR1(A,$f27(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 97 [] -cC138(A)|cC136xcomp($f27(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 98 [] cC138(A)| -rR1(A,B)| -cC136xcomp(B).
% 1.99/2.18 ** KEPT (pick-wt=6): 99 [] -cC138(A)|ra_Px47(A,$f28(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 100 [] cC138(A)| -ra_Px47(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 101 [] -cC138xcomp(A)| -ra_Px47(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 102 [] -cC14(A)|cC12xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 103 [] -cC14(A)|cC8xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 104 [] cC14(A)| -cC12xcomp(A)| -cC8xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 105 [] -cC140(A)|cC74(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 106 [] -cC140(A)|cC138xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 107 [] cC140(A)| -cC74(A)| -cC138xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 108 [] -cC16(A)| -ra_Px4(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 109 [] -cC16xcomp(A)|ra_Px4(A,$f31(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 110 [] cC16xcomp(A)| -ra_Px4(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 111 [] -cC18(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 112 [] -cC18(A)|cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 113 [] cC18(A)| -cC2(A)| -cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 114 [] -cC18(A)|ra_Px56(A,$f32(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 115 [] cC18(A)| -ra_Px56(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 116 [] -cC18xcomp(A)| -ra_Px56(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 117 [] -cC2(A)| -ra_Px22(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 118 [] -cC2xcomp(A)|ra_Px22(A,$f35(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 119 [] cC2xcomp(A)| -ra_Px22(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 120 [] -cC20(A)|rR1(A,$f36(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 121 [] -cC20(A)|cC18($f36(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 122 [] cC20(A)| -rR1(A,B)| -cC18(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 123 [] -cC22(A)|cC16(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 124 [] -cC22(A)|cC20(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 125 [] cC22(A)| -cC16(A)| -cC20(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 126 [] -cC22(A)|ra_Px6(A,$f37(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 127 [] cC22(A)| -ra_Px6(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 128 [] -cC22xcomp(A)| -ra_Px6(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 129 [] -cC24(A)|cC16(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 130 [] -cC24(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 131 [] cC24(A)| -cC16(A)| -cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 132 [] -cC26(A)|rR1(A,$f39(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 133 [] -cC26(A)|cC24($f39(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 134 [] cC26(A)| -rR1(A,B)| -cC24(B).
% 1.99/2.18 ** KEPT (pick-wt=5): 135 [] -cC28(A)| -ra_Px7(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 136 [] -cC28(A)|cC26(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 137 [] -cC28(A)|cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 138 [] cC28(A)| -cC26(A)| -cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 139 [] -cC28xcomp(A)|ra_Px7(A,$f41(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 140 [] cC28xcomp(A)| -ra_Px7(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 141 [] -cC30(A)|ra_Px8(A,$f42(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 142 [] cC30(A)| -ra_Px8(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 143 [] -cC30(A)|cC22xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 144 [] -cC30(A)|cC28xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 145 [] cC30(A)| -cC22xcomp(A)| -cC28xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 146 [] -cC30xcomp(A)| -ra_Px8(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 147 [] -cC32(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 148 [] -cC32(A)|cC30xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 149 [] cC32(A)| -cC2(A)| -cC30xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 150 [] -cC32(A)|ra_Px14(A,$f44(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 151 [] cC32(A)| -ra_Px14(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 152 [] -cC32xcomp(A)| -ra_Px14(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 153 [] -cC34(A)|ra_Px9(A,$f46(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 154 [] cC34(A)| -ra_Px9(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 155 [] -cC34xcomp(A)| -ra_Px9(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 156 [] -cC36(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 157 [] -cC36(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 158 [] cC36(A)| -cC34xcomp(A)| -cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 159 [] -cC38(A)|rR1(A,$f48(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 160 [] -cC38(A)|cC36($f48(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 161 [] cC38(A)| -rR1(A,B)| -cC36(B).
% 1.99/2.18 ** KEPT (pick-wt=5): 162 [] -cC4(A)| -ra_Px1(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 163 [] -cC4xcomp(A)|ra_Px1(A,$f50(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 164 [] cC4xcomp(A)| -ra_Px1(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 165 [] -cC40(A)|ra_Px11(A,$f51(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 166 [] cC40(A)| -ra_Px11(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 167 [] -cC40(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 168 [] -cC40(A)|cC38(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 169 [] cC40(A)| -cC34(A)| -cC38(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 170 [] -cC40xcomp(A)| -ra_Px11(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 171 [] -cC42(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 172 [] -cC42(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 173 [] cC42(A)| -cC4(A)| -cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 174 [] -cC44(A)|rR1(A,$f53(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 175 [] -cC44(A)|cC42($f53(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 176 [] cC44(A)| -rR1(A,B)| -cC42(B).
% 1.99/2.18 ** KEPT (pick-wt=6): 177 [] -cC46(A)|ra_Px12(A,$f54(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 178 [] cC46(A)| -ra_Px12(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 179 [] -cC46(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 180 [] -cC46(A)|cC44(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 181 [] cC46(A)| -cC34xcomp(A)| -cC44(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 182 [] -cC46xcomp(A)| -ra_Px12(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 183 [] -cC48(A)| -ra_Px13(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 184 [] -cC48(A)|cC40xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 185 [] -cC48(A)|cC46xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 186 [] cC48(A)| -cC40xcomp(A)| -cC46xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 187 [] -cC48xcomp(A)|ra_Px13(A,$f57(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 188 [] cC48xcomp(A)| -ra_Px13(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 189 [] -cC50(A)|ra_Px15(A,$f58(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 190 [] cC50(A)| -ra_Px15(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 191 [] -cC50(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 192 [] -cC50(A)|cC48xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 193 [] cC50(A)| -cC4(A)| -cC48xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 194 [] -cC50xcomp(A)| -ra_Px15(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 195 [] -cC52(A)|cC32xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 196 [] -cC52(A)|cC50xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 197 [] cC52(A)| -cC32xcomp(A)| -cC50xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 198 [] -cC54(A)|cC14(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 199 [] -cC54(A)|cC52(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 200 [] cC54(A)| -cC14(A)| -cC52(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 201 [] -cC56(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 202 [] -cC56(A)|cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 203 [] cC56(A)| -cC4(A)| -cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 204 [] -cC58(A)|cC34(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 205 [] -cC58(A)|cC56(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 206 [] cC58(A)| -cC34(A)| -cC56(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 207 [] -cC6(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 208 [] -cC6(A)|cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 209 [] cC6(A)| -cC2(A)| -cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 210 [] -cC60(A)|rR1(A,$f60(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 211 [] -cC60(A)|cC58($f60(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 212 [] cC60(A)| -rR1(A,B)| -cC58(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 213 [] -cC62(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 214 [] -cC62(A)|cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 215 [] cC62(A)| -cC4(A)| -cC10xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 216 [] -cC64(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 217 [] -cC64(A)|cC62(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 218 [] cC64(A)| -cC34xcomp(A)| -cC62(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 219 [] -cC66(A)|rR1(A,$f61(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 220 [] -cC66(A)|cC64($f61(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 221 [] cC66(A)| -rR1(A,B)| -cC64(B).
% 1.99/2.18 ** KEPT (pick-wt=4): 222 [] -cC68(A)|cC66(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 223 [] -cC68(A)|cC60(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 224 [] cC68(A)| -cC66(A)| -cC60(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 225 [] -cC68(A)|ra_Px20(A,$f62(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 226 [] cC68(A)| -ra_Px20(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 227 [] -cC68xcomp(A)| -ra_Px20(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 228 [] -cC70(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 229 [] -cC70(A)|cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 230 [] cC70(A)| -cC2(A)| -cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 231 [] -cC72(A)|ra_Px21(A,$f64(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 232 [] cC72(A)| -ra_Px21(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 233 [] -cC72(A)|cC70(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 234 [] -cC72(A)|cC68xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 235 [] cC72(A)| -cC70(A)| -cC68xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 236 [] -cC72xcomp(A)| -ra_Px21(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 237 [] -cC74(A)|cC54(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 238 [] -cC74(A)|cC72xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 239 [] cC74(A)| -cC54(A)| -cC72xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 240 [] -cC76(A)|ra_Px24(A,$f66(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 241 [] cC76(A)| -ra_Px24(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 242 [] -cC76(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 243 [] -cC76(A)|cC2xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 244 [] cC76(A)| -cC4(A)| -cC2xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 245 [] -cC76xcomp(A)| -ra_Px24(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 246 [] -cC78(A)|cC10(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 247 [] -cC78(A)|cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 248 [] cC78(A)| -cC10(A)| -cC4xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 249 [] -cC78(A)| -ra_Px25(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 250 [] -cC78xcomp(A)|ra_Px25(A,$f69(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 251 [] cC78xcomp(A)| -ra_Px25(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 252 [] -cC8(A)|ra_Px2(A,$f70(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 253 [] cC8(A)| -ra_Px2(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 254 [] -cC8(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 255 [] -cC8(A)|cC2xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 256 [] cC8(A)| -cC4(A)| -cC2xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 257 [] -cC8xcomp(A)| -ra_Px2(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 258 [] -cC80(A)|cC78xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 259 [] -cC80(A)|cC76xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 260 [] cC80(A)| -cC78xcomp(A)| -cC76xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 261 [] -cC82(A)|ra_Px65(A,$f72(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 262 [] cC82(A)| -ra_Px65(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 263 [] -cC82(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 264 [] -cC82(A)|cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 265 [] cC82(A)| -cC2(A)| -cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 266 [] -cC82xcomp(A)| -ra_Px65(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 267 [] -cC84(A)|ra_Px53(A,$f74(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 268 [] cC84(A)| -ra_Px53(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 269 [] -cC84(A)|rR1(A,$f75(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 270 [] -cC84(A)|cC82($f75(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 271 [] cC84(A)| -rR1(A,B)| -cC82(B).
% 1.99/2.18 ** KEPT (pick-wt=5): 272 [] -cC84xcomp(A)| -ra_Px53(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 273 [] -cC86(A)|cC16(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 274 [] -cC86(A)|cC84(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 275 [] cC86(A)| -cC16(A)| -cC84(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 276 [] -cC86(A)| -ra_Px28(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 277 [] -cC86xcomp(A)|ra_Px28(A,$f78(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 278 [] cC86xcomp(A)| -ra_Px28(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 279 [] -cC88(A)|cC16(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 280 [] -cC88(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 281 [] cC88(A)| -cC16(A)| -cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 282 [] -cC88(A)| -ra_Px64(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 283 [] -cC88xcomp(A)|ra_Px64(A,$f80(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 284 [] cC88xcomp(A)| -ra_Px64(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 285 [] -cC90(A)|rR1(A,$f81(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 286 [] -cC90(A)|cC88($f81(A)).
% 1.99/2.18 ** KEPT (pick-wt=7): 287 [] cC90(A)| -rR1(A,B)| -cC88(B).
% 1.99/2.18 ** KEPT (pick-wt=5): 288 [] -cC90(A)| -ra_Px52(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 289 [] -cC90xcomp(A)|ra_Px52(A,$f83(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 290 [] cC90xcomp(A)| -ra_Px52(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 291 [] -cC92(A)|ra_Px29(A,$f84(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 292 [] cC92(A)| -ra_Px29(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 293 [] -cC92(A)|cC90(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 294 [] -cC92(A)|cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 295 [] cC92(A)| -cC90(A)| -cC16xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 296 [] -cC92xcomp(A)| -ra_Px29(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 297 [] -cC94(A)|cC86xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 298 [] -cC94(A)|cC92xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 299 [] cC94(A)| -cC86xcomp(A)| -cC92xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 300 [] -cC94(A)|ra_Px30(A,$f86(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 301 [] cC94(A)| -ra_Px30(A,B).
% 1.99/2.18 ** KEPT (pick-wt=5): 302 [] -cC94xcomp(A)| -ra_Px30(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 303 [] -cC96(A)|ra_Px38(A,$f88(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 304 [] cC96(A)| -ra_Px38(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 305 [] -cC96(A)|cC2(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 306 [] -cC96(A)|cC94xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 307 [] cC96(A)| -cC2(A)| -cC94xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 308 [] -cC96xcomp(A)| -ra_Px38(A,B).
% 1.99/2.18 ** KEPT (pick-wt=6): 309 [] -cC98(A)|ra_Px63(A,$f90(A)).
% 1.99/2.18 ** KEPT (pick-wt=5): 310 [] cC98(A)| -ra_Px63(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 311 [] -cC98(A)|cC34xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 312 [] -cC98(A)|cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 313 [] cC98(A)| -cC34xcomp(A)| -cC4(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 314 [] -cC98xcomp(A)| -ra_Px63(A,B).
% 1.99/2.18 ** KEPT (pick-wt=4): 315 [] -cTEST(A)|cC6(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 316 [] -cTEST(A)|cC140(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 317 [] cTEST(A)| -cC6(A)| -cC140(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 318 [] -rR1(iV822576,A)|cC98xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 319 [] -rR1(iV822576,A)|cC82xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=5): 320 [] -rR1(iV822576,A)|cC88xcomp(A).
% 1.99/2.18 ** KEPT (pick-wt=24): 322 [copy,321,unit_del,1] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cC58(iV822576)| -cC116(iV822576)| -cC114(iV822576)| -cowlThing(iV822576)| -cC94(iV822576)| -cC80(iV822576)| -cC110(iV822576)| -cC136(iV822576)| -cC56(iV822576).
% 1.99/2.18 ** KEPT (pick-wt=24): 324 [copy,323,unit_del,1] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cC58(iV822576)| -cC116(iV822576)| -cC114(iV822576)| -cowlThing(iV822576)| -cC94(iV822576)| -cC80(iV822576)| -cC110(iV822576)| -cC136(iV822576)| -cC56(iV822576).
% 1.99/2.18
% 1.99/2.18 ------------> process sos:
% 1.99/2.18 ** KEPT (pick-wt=2): 325 [] cowlThing(A).
% 1.99/2.18 ** KEPT (pick-wt=4): 326 [] xsd_string(A)|xsd_integer(A).
% 1.99/2.18 ** KEPT (pick-wt=6): 327 [] cC10(A)|ra_Px16(A,$f1(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 328 [] cC100(A)|ra_Px49(A,$f4(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 329 [] cC102xcomp(A)|ra_Px35(A,$f7(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 330 [] cC108xcomp(A)|ra_Px36(A,$f10(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 331 [] cC110(A)|ra_Px37(A,$f11(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 332 [] cC112xcomp(A)|ra_Px39(A,$f14(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 333 [] cC12xcomp(A)|ra_Px3(A,$f16(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 334 [] cC130xcomp(A)|ra_Px44(A,$f20(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 335 [] cC132xcomp(A)|ra_Px48(A,$f22(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 336 [] cC134xcomp(A)|ra_Px45(A,$f24(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 337 [] cC136(A)|ra_Px46(A,$f25(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 338 [] cC138xcomp(A)|ra_Px47(A,$f29(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 339 [] cC16(A)|ra_Px4(A,$f30(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 340 [] cC18xcomp(A)|ra_Px56(A,$f33(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 341 [] cC2(A)|ra_Px22(A,$f34(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 342 [] cC22xcomp(A)|ra_Px6(A,$f38(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 343 [] cC28(A)|ra_Px7(A,$f40(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 344 [] cC30xcomp(A)|ra_Px8(A,$f43(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 345 [] cC32xcomp(A)|ra_Px14(A,$f45(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 346 [] cC34xcomp(A)|ra_Px9(A,$f47(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 347 [] cC4(A)|ra_Px1(A,$f49(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 348 [] cC40xcomp(A)|ra_Px11(A,$f52(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 349 [] cC46xcomp(A)|ra_Px12(A,$f55(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 350 [] cC48(A)|ra_Px13(A,$f56(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 351 [] cC50xcomp(A)|ra_Px15(A,$f59(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 352 [] cC68xcomp(A)|ra_Px20(A,$f63(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 353 [] cC72xcomp(A)|ra_Px21(A,$f65(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 354 [] cC76xcomp(A)|ra_Px24(A,$f67(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 355 [] cC78(A)|ra_Px25(A,$f68(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 356 [] cC8xcomp(A)|ra_Px2(A,$f71(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 357 [] cC82xcomp(A)|ra_Px65(A,$f73(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 358 [] cC84xcomp(A)|ra_Px53(A,$f76(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 359 [] cC86(A)|ra_Px28(A,$f77(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 360 [] cC88(A)|ra_Px64(A,$f79(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 361 [] cC90(A)|ra_Px52(A,$f82(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 362 [] cC92xcomp(A)|ra_Px29(A,$f85(A)).
% 1.99/2.18 ** KEPT (pick-wt=6): 363 [] cC94xcomp(A)|ra_Px30(A,$f87(A)).
% 1.99/2.19 ** KEPT (pick-wt=6): 364 [] cC96xcomp(A)|ra_Px38(A,$f89(A)).
% 1.99/2.19 ** KEPT (pick-wt=6): 365 [] cC98xcomp(A)|ra_Px63(A,$f91(A)).
% 1.99/2.19 ** KEPT (pick-wt=2): 366 [] cC16(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 367 [] cC102xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 368 [] cC108xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 369 [] cC4(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 370 [] cC18xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 371 [] cC112xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 372 [] cC76xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 373 [] cC96xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 374 [] cC132xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 375 [] cC100xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 376 [] cC90xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 377 [] cC78xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 378 [] cC134xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 379 [] cC86xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 380 [] cC34(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 381 [] cC84xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 382 [] cC2(iV822576).
% 1.99/2.19 Following clause subsumed by 325 during input processing: 0 [] cowlThing(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 383 [] cC10xcomp(iV822576).
% 1.99/2.19 ** KEPT (pick-wt=2): 384 [] cC92xcomp(iV822576).
% 1.99/2.19
% 1.99/2.19 ======= end of input processing =======
% 1.99/2.19
% 1.99/2.19 =========== start of search ===========
% 1.99/2.19
% 1.99/2.19 -------- PROOF --------
% 1.99/2.19
% 1.99/2.19 -----> EMPTY CLAUSE at 0.02 sec ----> 416 [hyper,415,2,414] $F.
% 1.99/2.19
% 1.99/2.19 Length of proof is 12. Level of proof is 5.
% 1.99/2.19
% 1.99/2.19 ---------------- PROOF ----------------
% 1.99/2.19 % SZS status Theorem
% 1.99/2.19 % SZS output start Refutation
% See solution above
% 1.99/2.19 ------------ end of proof -------------
% 1.99/2.19
% 1.99/2.19
% 1.99/2.19 Search stopped by max_proofs option.
% 1.99/2.19
% 1.99/2.19
% 1.99/2.19 Search stopped by max_proofs option.
% 1.99/2.19
% 1.99/2.19 ============ end of search ============
% 1.99/2.19
% 1.99/2.19 -------------- statistics -------------
% 1.99/2.19 clauses given 47
% 1.99/2.19 clauses generated 70
% 1.99/2.19 clauses kept 413
% 1.99/2.19 clauses forward subsumed 39
% 1.99/2.19 clauses back subsumed 2
% 1.99/2.19 Kbytes malloced 3906
% 1.99/2.19
% 1.99/2.19 ----------- times (seconds) -----------
% 1.99/2.19 user CPU time 0.02 (0 hr, 0 min, 0 sec)
% 1.99/2.19 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.99/2.19 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 1.99/2.19
% 1.99/2.19 That finishes the proof of the theorem.
% 1.99/2.19
% 1.99/2.19 Process 28770 finished Wed Jul 27 03:33:22 2022
% 1.99/2.19 Otter interrupted
% 1.99/2.19 PROOF FOUND
%------------------------------------------------------------------------------