%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL668+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:25 AM UTC 2026
% Result : Theorem 19.59s 3.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL668+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 5 06:12:27 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 19.59/3.04 % Version : CSI_E---1.1
% 19.59/3.04 % Problem : theBenchmark.p
% 19.59/3.04 % Proof found!
% 19.59/3.04 % SZS status Theorem for theBenchmark.p
% 19.59/3.04 % SZS output start Proof
% 19.59/3.04 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 19.59/3.04 fof(main, conjecture, ~(?[X1]:(~((![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|(((((((((((((((((((((((((~(p52(X1))&~(p50(X1)))&~(p48(X1)))&~(p46(X1)))&~(p44(X1)))&~(p42(X1)))&~(p40(X1)))&~(p38(X1)))&~(p36(X1)))&~(p34(X1)))&~(p32(X1)))&~(p30(X1)))&~(p28(X1)))&~(p26(X1)))&~(p24(X1)))&~(p22(X1)))&~(p20(X1)))&~(p18(X1)))&~(p16(X1)))&~(p14(X1)))&~(p12(X1)))&~(p10(X1)))&~(p8(X1)))&~(p6(X1)))&~(p4(X1)))&~(p2(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p27(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p25(X1))&~(p1(X1)))|(p1(X1)&p25(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p26(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p24(X1))&~(p25(X1)))|(p25(X1)&p24(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p25(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p23(X1))&~(p24(X1)))|(p24(X1)&p23(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p24(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p22(X1))&~(p23(X1)))|(p23(X1)&p22(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p23(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p21(X1))&~(p22(X1)))|(p22(X1)&p21(X1)))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p22(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p20(X1))&~(p21(X1)))|(p21(X1)&p20(X1)))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p21(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p19(X1))&~(p20(X1)))|(p20(X1)&p19(X1)))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p20(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p18(X1))&~(p19(X1)))|(p19(X1)&p18(X1)))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p19(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p17(X1))&~(p18(X1)))|(p18(X1)&p17(X1)))))))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p18(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p16(X1))&~(p17(X1)))|(p17(X1)&p16(X1)))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p17(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p15(X1))&~(p16(X1)))|(p16(X1)&p15(X1)))))))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p16(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p14(X1))&~(p15(X1)))|(p15(X1)&p14(X1)))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p15(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p13(X1))&~(p14(X1)))|(p14(X1)&p13(X1)))))))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p14(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p12(X1))&~(p13(X1)))|(p13(X1)&p12(X1)))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p13(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p11(X1))&~(p12(X1)))|(p12(X1)&p11(X1)))))))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p12(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p10(X1))&~(p11(X1)))|(p11(X1)&p10(X1)))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p11(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p9(X1))&~(p10(X1)))|(p10(X1)&p9(X1)))))))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p10(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p8(X1))&~(p9(X1)))|(p9(X1)&p8(X1)))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p9(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p7(X1))&~(p8(X1)))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~(r1(X2,X1))|p8(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p6(X1))&~(p7(X1)))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~(r1(X1,X2))|p7(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p6(X1)))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~(r1(X2,X1))|p6(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p5(X1)))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~(r1(X1,X2))|p5(X2)))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p4(X1)))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~(r1(X2,X1))|p4(X1)))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p3(X1)))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(![X2]:((~(r1(X1,X2))|~(~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(((~(p1(X1))&~(p2(X1)))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|(((((((((((((((((((((((((p26(X1)&p25(X1))&p24(X1))&p23(X1))&p22(X1))&p21(X1))&p20(X1))&p19(X1))&p18(X1))&p17(X1))&p16(X1))&p15(X1))&p14(X1))&p13(X1))&p12(X1))&p11(X1))&p10(X1))&p9(X1))&p8(X1))&p7(X1))&p6(X1))&p5(X1))&p4(X1))&p3(X1))&p2(X1))&p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 19.59/3.04 fof(c_0_2, plain, ![X2]:((epred1_1(X2)<=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p8(X1))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p8(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p7(X1))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~r1(X1,X2)|p7(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p6(X1))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 19.59/3.04 fof(c_0_3, plain, ![X2]:((epred1_1(X2)=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p8(X1))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p8(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p7(X1))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~r1(X1,X2)|p7(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p6(X1))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 19.59/3.04 fof(c_0_4, plain, ![X59, X60, X61, X62, X63, X64, X65, X66, X67, X68, X70, X71, X72, X73, X74, X75, X76, X77, X78, X80, X81, X82, X83, X84, X85, X86, X87, X89, X90, X91, X92, X93, X94, X95, X97, X98, X99, X100, X101, X102, X104, X105, X106, X107, X108, X110, X111, X112, X113]:(((((p7(X68)|p8(X68)|~r1(X67,X68)|~r1(X66,X67)|~r1(X65,X66)|~r1(X64,X65)|~r1(X63,X64)|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~epred1_1(X59))&(~p8(X68)|~p7(X68)|~r1(X67,X68)|~r1(X66,X67)|~r1(X65,X66)|~r1(X64,X65)|~r1(X63,X64)|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~epred1_1(X59)))&((r1(X59,esk55_1(X59))|~epred1_1(X59))&(~p8(esk55_1(X59))|~epred1_1(X59))))&((((p6(X78)|p7(X78)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(X59,X70)|~epred1_1(X59))&(~p7(X78)|~p6(X78)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(X59,X70)|~epred1_1(X59)))&((r1(X70,esk56_2(X59,X70))|~r1(X59,X70)|~epred1_1(X59))&(~p7(esk56_2(X59,X70))|~r1(X59,X70)|~epred1_1(X59))))&((((p5(X87)|p6(X87)|~r1(X86,X87)|~r1(X85,X86)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(X81,X82)|~r1(X80,X81)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p6(X87)|~p5(X87)|~r1(X86,X87)|~r1(X85,X86)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(X81,X82)|~r1(X80,X81)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59)))&((r1(X80,esk57_3(X59,X70,X80))|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p6(esk57_3(X59,X70,X80))|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))))&((((p4(X95)|p5(X95)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(X89,X90)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p5(X95)|~p4(X95)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(X89,X90)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59)))&((r1(X89,esk58_4(X59,X70,X80,X89))|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p5(esk58_4(X59,X70,X80,X89))|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))))&((((p3(X102)|p4(X102)|~r1(X101,X102)|~r1(X100,X101)|~r1(X99,X100)|~r1(X98,X99)|~r1(X97,X98)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p4(X102)|~p3(X102)|~r1(X101,X102)|~r1(X100,X101)|~r1(X99,X100)|~r1(X98,X99)|~r1(X97,X98)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59)))&((r1(X97,esk59_5(X59,X70,X80,X89,X97))|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p4(esk59_5(X59,X70,X80,X89,X97))|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))))&((((p2(X108)|p3(X108)|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p3(X108)|~p2(X108)|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59)))&((r1(X104,esk60_6(X59,X70,X80,X89,X97,X104))|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p3(esk60_6(X59,X70,X80,X89,X97,X104))|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))))&((p1(X113)|p2(X113)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X104,X110)|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59))&(~p2(X113)|~p1(X113)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X104,X110)|~r1(X97,X104)|~r1(X89,X97)|~r1(X80,X89)|~r1(X70,X80)|~r1(X59,X70)|~epred1_1(X59)))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])])).
% 19.59/3.04 fof(c_0_5, plain, ![X3]:(r1(X3,X3)), inference(variable_rename,[status(thm)],[reflexivity])).
% 19.59/3.04 cnf(c_0_6, plain, (~p8(X1)|~p7(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.04 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 19.59/3.04 cnf(c_0_8, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 19.59/3.04 cnf(c_0_9, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X2)), inference(spm,[status(thm)],[c_0_8, c_0_7])).
% 19.59/3.04 cnf(c_0_10, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X2)), inference(spm,[status(thm)],[c_0_9, c_0_7])).
% 19.59/3.04 fof(c_0_11, plain, ![X2]:((epred2_1(X2)<=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p14(X1))|(p14(X1)&p13(X1)))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p14(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p13(X1))|(p13(X1)&p12(X1)))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p13(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p12(X1))|(p12(X1)&p11(X1)))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p12(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p11(X1))|(p11(X1)&p10(X1)))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p11(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p10(X1))|(p10(X1)&p9(X1)))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p10(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p9(X1))|(p9(X1)&p8(X1)))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p9(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p8(X1))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p8(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p7(X1))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~r1(X1,X2)|p7(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p6(X1))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 19.59/3.04 cnf(c_0_12, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X2)), inference(spm,[status(thm)],[c_0_10, c_0_7])).
% 19.59/3.04 fof(c_0_13, plain, ![X2]:((epred2_1(X2)=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p14(X1))|(p14(X1)&p13(X1)))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p14(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p13(X1))|(p13(X1)&p12(X1)))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p13(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p12(X1))|(p12(X1)&p11(X1)))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p12(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p11(X1))|(p11(X1)&p10(X1)))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p11(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p10(X1))|(p10(X1)&p9(X1)))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p10(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p9(X1))|(p9(X1)&p8(X1)))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p9(X2)))|~(![X2]:((~r1(X1,X2)|epred1_1(X2))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_11]), c_0_2])).
% 19.59/3.04 fof(c_0_14, plain, ![X2]:((epred4_1(X2)<=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p25(X1)&~p1(X1))|(p1(X1)&p25(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p26(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p24(X1)&~p25(X1))|(p25(X1)&p24(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p25(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p23(X1)&~p24(X1))|(p24(X1)&p23(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p24(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p22(X1)&~p23(X1))|(p23(X1)&p22(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p23(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p21(X1)&~p22(X1))|(p22(X1)&p21(X1)))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p22(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p20(X1)&~p21(X1))|(p21(X1)&p20(X1)))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p21(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p19(X1)&~p20(X1))|(p20(X1)&p19(X1)))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p20(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p18(X1)&~p19(X1))|(p19(X1)&p18(X1)))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p19(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p17(X1)&~p18(X1))|(p18(X1)&p17(X1)))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p18(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p16(X1)&~p17(X1))|(p17(X1)&p16(X1)))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p17(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p15(X1)&~p16(X1))|(p16(X1)&p15(X1)))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p16(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p14(X1)&~p15(X1))|(p15(X1)&p14(X1)))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p15(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p14(X1))|(p14(X1)&p13(X1)))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p14(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p13(X1))|(p13(X1)&p12(X1)))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p13(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p12(X1))|(p12(X1)&p11(X1)))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p12(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p11(X1))|(p11(X1)&p10(X1)))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p11(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p10(X1))|(p10(X1)&p9(X1)))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p10(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p9(X1))|(p9(X1)&p8(X1)))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p9(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p8(X1))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p8(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p7(X1))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~r1(X1,X2)|p7(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p6(X1))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 19.59/3.04 fof(c_0_15, plain, ![X2]:((epred3_1(X2)<=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p19(X1)&~p20(X1))|(p20(X1)&p19(X1)))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p20(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p18(X1)&~p19(X1))|(p19(X1)&p18(X1)))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p19(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p17(X1)&~p18(X1))|(p18(X1)&p17(X1)))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p18(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p16(X1)&~p17(X1))|(p17(X1)&p16(X1)))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p17(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p15(X1)&~p16(X1))|(p16(X1)&p15(X1)))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p16(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p14(X1)&~p15(X1))|(p15(X1)&p14(X1)))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p15(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p13(X1)&~p14(X1))|(p14(X1)&p13(X1)))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p14(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p12(X1)&~p13(X1))|(p13(X1)&p12(X1)))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p13(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p11(X1)&~p12(X1))|(p12(X1)&p11(X1)))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p12(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p10(X1)&~p11(X1))|(p11(X1)&p10(X1)))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p11(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p9(X1)&~p10(X1))|(p10(X1)&p9(X1)))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p10(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p8(X1)&~p9(X1))|(p9(X1)&p8(X1)))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p9(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p7(X1)&~p8(X1))|(p8(X1)&p7(X1)))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p8(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p7(X1))|(p7(X1)&p6(X1)))))))))))))))))))))|![X2]:((~r1(X1,X2)|p7(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p6(X1))|(p6(X1)&p5(X1)))))))))))))))))))|![X1]:((~r1(X2,X1)|p6(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p5(X1))|(p5(X1)&p4(X1)))))))))))))))))|![X2]:((~r1(X1,X2)|p5(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p4(X1))|(p4(X1)&p3(X1)))))))))))))))|![X1]:((~r1(X2,X1)|p4(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p3(X1))|(p3(X1)&p2(X1)))))))))))))|![X2]:((~r1(X1,X2)|p3(X2)))|~(![X2]:((~r1(X1,X2)|~(~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p1(X1)&~p2(X1))|(p2(X1)&p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), introduced(definition)).
% 19.59/3.04 cnf(c_0_16, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X2)), inference(spm,[status(thm)],[c_0_12, c_0_7])).
% 19.59/3.04 fof(c_0_17, plain, ![X114, X115, X116, X117, X118, X119, X120, X121, X122, X123, X124, X125, X126, X127, X128, X129, X131, X132, X133, X134, X135, X136, X137, X138, X139, X140, X141, X142, X143, X144, X145, X147, X148, X149, X150, X151, X152, X153, X154, X155, X156, X157, X158, X159, X160, X162, X163, X164, X165, X166, X167, X168, X169, X170, X171, X172, X173, X174, X176, X177, X178, X179, X180, X181, X182, X183, X184, X185, X186, X187, X189, X190, X191, X192, X193, X194, X195, X196, X197, X198, X199, X201]:(((((p13(X129)|p14(X129)|~r1(X128,X129)|~r1(X127,X128)|~r1(X126,X127)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(X122,X123)|~r1(X121,X122)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(X117,X118)|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~epred2_1(X114))&(~p14(X129)|~p13(X129)|~r1(X128,X129)|~r1(X127,X128)|~r1(X126,X127)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(X122,X123)|~r1(X121,X122)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(X117,X118)|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~epred2_1(X114)))&((r1(X114,esk61_1(X114))|~epred2_1(X114))&(~p14(esk61_1(X114))|~epred2_1(X114))))&((((p12(X145)|p13(X145)|~r1(X144,X145)|~r1(X143,X144)|~r1(X142,X143)|~r1(X141,X142)|~r1(X140,X141)|~r1(X139,X140)|~r1(X138,X139)|~r1(X137,X138)|~r1(X136,X137)|~r1(X135,X136)|~r1(X134,X135)|~r1(X133,X134)|~r1(X132,X133)|~r1(X131,X132)|~r1(X114,X131)|~epred2_1(X114))&(~p13(X145)|~p12(X145)|~r1(X144,X145)|~r1(X143,X144)|~r1(X142,X143)|~r1(X141,X142)|~r1(X140,X141)|~r1(X139,X140)|~r1(X138,X139)|~r1(X137,X138)|~r1(X136,X137)|~r1(X135,X136)|~r1(X134,X135)|~r1(X133,X134)|~r1(X132,X133)|~r1(X131,X132)|~r1(X114,X131)|~epred2_1(X114)))&((r1(X131,esk62_2(X114,X131))|~r1(X114,X131)|~epred2_1(X114))&(~p13(esk62_2(X114,X131))|~r1(X114,X131)|~epred2_1(X114))))&((((p11(X160)|p12(X160)|~r1(X159,X160)|~r1(X158,X159)|~r1(X157,X158)|~r1(X156,X157)|~r1(X155,X156)|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(X148,X149)|~r1(X147,X148)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p12(X160)|~p11(X160)|~r1(X159,X160)|~r1(X158,X159)|~r1(X157,X158)|~r1(X156,X157)|~r1(X155,X156)|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(X148,X149)|~r1(X147,X148)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114)))&((r1(X147,esk63_3(X114,X131,X147))|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p12(esk63_3(X114,X131,X147))|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))))&((((p10(X174)|p11(X174)|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(X164,X165)|~r1(X163,X164)|~r1(X162,X163)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p11(X174)|~p10(X174)|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(X164,X165)|~r1(X163,X164)|~r1(X162,X163)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114)))&((r1(X162,esk64_4(X114,X131,X147,X162))|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p11(esk64_4(X114,X131,X147,X162))|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))))&((((p9(X187)|p10(X187)|~r1(X186,X187)|~r1(X185,X186)|~r1(X184,X185)|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(X179,X180)|~r1(X178,X179)|~r1(X177,X178)|~r1(X176,X177)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p10(X187)|~p9(X187)|~r1(X186,X187)|~r1(X185,X186)|~r1(X184,X185)|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(X179,X180)|~r1(X178,X179)|~r1(X177,X178)|~r1(X176,X177)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114)))&((r1(X176,esk65_5(X114,X131,X147,X162,X176))|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p10(esk65_5(X114,X131,X147,X162,X176))|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))))&((((p8(X199)|p9(X199)|~r1(X198,X199)|~r1(X197,X198)|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(X193,X194)|~r1(X192,X193)|~r1(X191,X192)|~r1(X190,X191)|~r1(X189,X190)|~r1(X176,X189)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p9(X199)|~p8(X199)|~r1(X198,X199)|~r1(X197,X198)|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(X193,X194)|~r1(X192,X193)|~r1(X191,X192)|~r1(X190,X191)|~r1(X189,X190)|~r1(X176,X189)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114)))&((r1(X189,esk66_6(X114,X131,X147,X162,X176,X189))|~r1(X176,X189)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))&(~p9(esk66_6(X114,X131,X147,X162,X176,X189))|~r1(X176,X189)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))))&(~r1(X189,X201)|epred1_1(X201)|~r1(X176,X189)|~r1(X162,X176)|~r1(X147,X162)|~r1(X131,X147)|~r1(X114,X131)|~epred2_1(X114))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_13])])])])])])).
% 19.59/3.04 fof(c_0_18, plain, ![X2]:((epred4_1(X2)=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p25(X1)&~p1(X1))|(p1(X1)&p25(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p26(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p24(X1)&~p25(X1))|(p25(X1)&p24(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p25(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p23(X1)&~p24(X1))|(p24(X1)&p23(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p24(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p22(X1)&~p23(X1))|(p23(X1)&p22(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p23(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p21(X1)&~p22(X1))|(p22(X1)&p21(X1)))))))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p22(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p20(X1)&~p21(X1))|(p21(X1)&p20(X1)))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p21(X2)))|~(![X2]:((~r1(X1,X2)|epred3_1(X2))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_14]), c_0_15])).
% 19.59/3.04 fof(c_0_19, plain, ![X2]:((epred3_1(X2)=>~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p19(X1)&~p20(X1))|(p20(X1)&p19(X1)))))))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p20(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p18(X1)&~p19(X1))|(p19(X1)&p18(X1)))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p19(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p17(X1)&~p18(X1))|(p18(X1)&p17(X1)))))))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p18(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p16(X1)&~p17(X1))|(p17(X1)&p16(X1)))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p17(X2)))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p15(X1)&~p16(X1))|(p16(X1)&p15(X1)))))))))))))))))))))))))))))))))))))))|![X1]:((~r1(X2,X1)|p16(X1)))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(((~p14(X1)&~p15(X1))|(p15(X1)&p14(X1)))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p15(X2)))|~(![X2]:((~r1(X1,X2)|epred2_1(X2))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_15]), c_0_11])).
% 19.59/3.04 cnf(c_0_20, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X2)), inference(spm,[status(thm)],[c_0_16, c_0_7])).
% 19.59/3.04 fof(c_0_21, negated_conjecture, ~(~(?[X1]:(~((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|(((((((((((((((((((((((((~p52(X1)&~p50(X1))&~p48(X1))&~p46(X1))&~p44(X1))&~p42(X1))&~p40(X1))&~p38(X1))&~p36(X1))&~p34(X1))&~p32(X1))&~p30(X1))&~p28(X1))&~p26(X1))&~p24(X1))&~p22(X1))&~p20(X1))&~p18(X1))&~p16(X1))&~p14(X1))&~p12(X1))&~p10(X1))&~p8(X1))&~p6(X1))&~p4(X1))&~p2(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|p27(X2)))|~(![X2]:((~r1(X1,X2)|epred4_1(X2))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|(((((((((((((((((((((((((p26(X1)&p25(X1))&p24(X1))&p23(X1))&p22(X1))&p21(X1))&p20(X1))&p19(X1))&p18(X1))&p17(X1))&p16(X1))&p15(X1))&p14(X1))&p13(X1))&p12(X1))&p11(X1))&p10(X1))&p9(X1))&p8(X1))&p7(X1))&p6(X1))&p5(X1))&p4(X1))&p3(X1))&p2(X1))&p1(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_14])).
% 19.59/3.04 cnf(c_0_22, plain, (~p7(X1)|~p6(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.04 cnf(c_0_23, plain, (epred1_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~epred2_1(X7)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.04 fof(c_0_24, plain, ![X326, X327, X328, X329, X330, X331, X332, X333, X334, X335, X336, X337, X338, X339, X340, X341, X342, X343, X344, X345, X346, X347, X348, X349, X350, X351, X352, X353, X355, X356, X357, X358, X359, X360, X361, X362, X363, X364, X365, X366, X367, X368, X369, X370, X371, X372, X373, X374, X375, X376, X377, X378, X379, X380, X381, X383, X384, X385, X386, X387, X388, X389, X390, X391, X392, X393, X394, X395, X396, X397, X398, X399, X400, X401, X402, X403, X404, X405, X406, X407, X408, X410, X411, X412, X413, X414, X415, X416, X417, X418, X419, X420, X421, X422, X423, X424, X425, X426, X427, X428, X429, X430, X431, X432, X433, X434, X436, X437, X438, X439, X440, X441, X442, X443, X444, X445, X446, X447, X448, X449, X450, X451, X452, X453, X454, X455, X456, X457, X458, X459, X461, X462, X463, X464, X465, X466, X467, X468, X469, X470, X471, X472, X473, X474, X475, X476, X477, X478, X479, X480, X481, X482, X483, X485]:(((((p25(X353)|p1(X353)|~r1(X352,X353)|~r1(X351,X352)|~r1(X350,X351)|~r1(X349,X350)|~r1(X348,X349)|~r1(X347,X348)|~r1(X346,X347)|~r1(X345,X346)|~r1(X344,X345)|~r1(X343,X344)|~r1(X342,X343)|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(X337,X338)|~r1(X336,X337)|~r1(X335,X336)|~r1(X334,X335)|~r1(X333,X334)|~r1(X332,X333)|~r1(X331,X332)|~r1(X330,X331)|~r1(X329,X330)|~r1(X328,X329)|~r1(X327,X328)|~r1(X326,X327)|~epred4_1(X326))&(~p1(X353)|~p25(X353)|~r1(X352,X353)|~r1(X351,X352)|~r1(X350,X351)|~r1(X349,X350)|~r1(X348,X349)|~r1(X347,X348)|~r1(X346,X347)|~r1(X345,X346)|~r1(X344,X345)|~r1(X343,X344)|~r1(X342,X343)|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(X337,X338)|~r1(X336,X337)|~r1(X335,X336)|~r1(X334,X335)|~r1(X333,X334)|~r1(X332,X333)|~r1(X331,X332)|~r1(X330,X331)|~r1(X329,X330)|~r1(X328,X329)|~r1(X327,X328)|~r1(X326,X327)|~epred4_1(X326)))&((r1(X326,esk73_1(X326))|~epred4_1(X326))&(~p26(esk73_1(X326))|~epred4_1(X326))))&((((p24(X381)|p25(X381)|~r1(X380,X381)|~r1(X379,X380)|~r1(X378,X379)|~r1(X377,X378)|~r1(X376,X377)|~r1(X375,X376)|~r1(X374,X375)|~r1(X373,X374)|~r1(X372,X373)|~r1(X371,X372)|~r1(X370,X371)|~r1(X369,X370)|~r1(X368,X369)|~r1(X367,X368)|~r1(X366,X367)|~r1(X365,X366)|~r1(X364,X365)|~r1(X363,X364)|~r1(X362,X363)|~r1(X361,X362)|~r1(X360,X361)|~r1(X359,X360)|~r1(X358,X359)|~r1(X357,X358)|~r1(X356,X357)|~r1(X355,X356)|~r1(X326,X355)|~epred4_1(X326))&(~p25(X381)|~p24(X381)|~r1(X380,X381)|~r1(X379,X380)|~r1(X378,X379)|~r1(X377,X378)|~r1(X376,X377)|~r1(X375,X376)|~r1(X374,X375)|~r1(X373,X374)|~r1(X372,X373)|~r1(X371,X372)|~r1(X370,X371)|~r1(X369,X370)|~r1(X368,X369)|~r1(X367,X368)|~r1(X366,X367)|~r1(X365,X366)|~r1(X364,X365)|~r1(X363,X364)|~r1(X362,X363)|~r1(X361,X362)|~r1(X360,X361)|~r1(X359,X360)|~r1(X358,X359)|~r1(X357,X358)|~r1(X356,X357)|~r1(X355,X356)|~r1(X326,X355)|~epred4_1(X326)))&((r1(X355,esk74_2(X326,X355))|~r1(X326,X355)|~epred4_1(X326))&(~p25(esk74_2(X326,X355))|~r1(X326,X355)|~epred4_1(X326))))&((((p23(X408)|p24(X408)|~r1(X407,X408)|~r1(X406,X407)|~r1(X405,X406)|~r1(X404,X405)|~r1(X403,X404)|~r1(X402,X403)|~r1(X401,X402)|~r1(X400,X401)|~r1(X399,X400)|~r1(X398,X399)|~r1(X397,X398)|~r1(X396,X397)|~r1(X395,X396)|~r1(X394,X395)|~r1(X393,X394)|~r1(X392,X393)|~r1(X391,X392)|~r1(X390,X391)|~r1(X389,X390)|~r1(X388,X389)|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(X384,X385)|~r1(X383,X384)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p24(X408)|~p23(X408)|~r1(X407,X408)|~r1(X406,X407)|~r1(X405,X406)|~r1(X404,X405)|~r1(X403,X404)|~r1(X402,X403)|~r1(X401,X402)|~r1(X400,X401)|~r1(X399,X400)|~r1(X398,X399)|~r1(X397,X398)|~r1(X396,X397)|~r1(X395,X396)|~r1(X394,X395)|~r1(X393,X394)|~r1(X392,X393)|~r1(X391,X392)|~r1(X390,X391)|~r1(X389,X390)|~r1(X388,X389)|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(X384,X385)|~r1(X383,X384)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326)))&((r1(X383,esk75_3(X326,X355,X383))|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p24(esk75_3(X326,X355,X383))|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))))&((((p22(X434)|p23(X434)|~r1(X433,X434)|~r1(X432,X433)|~r1(X431,X432)|~r1(X430,X431)|~r1(X429,X430)|~r1(X428,X429)|~r1(X427,X428)|~r1(X426,X427)|~r1(X425,X426)|~r1(X424,X425)|~r1(X423,X424)|~r1(X422,X423)|~r1(X421,X422)|~r1(X420,X421)|~r1(X419,X420)|~r1(X418,X419)|~r1(X417,X418)|~r1(X416,X417)|~r1(X415,X416)|~r1(X414,X415)|~r1(X413,X414)|~r1(X412,X413)|~r1(X411,X412)|~r1(X410,X411)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p23(X434)|~p22(X434)|~r1(X433,X434)|~r1(X432,X433)|~r1(X431,X432)|~r1(X430,X431)|~r1(X429,X430)|~r1(X428,X429)|~r1(X427,X428)|~r1(X426,X427)|~r1(X425,X426)|~r1(X424,X425)|~r1(X423,X424)|~r1(X422,X423)|~r1(X421,X422)|~r1(X420,X421)|~r1(X419,X420)|~r1(X418,X419)|~r1(X417,X418)|~r1(X416,X417)|~r1(X415,X416)|~r1(X414,X415)|~r1(X413,X414)|~r1(X412,X413)|~r1(X411,X412)|~r1(X410,X411)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326)))&((r1(X410,esk76_4(X326,X355,X383,X410))|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p23(esk76_4(X326,X355,X383,X410))|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))))&((((p21(X459)|p22(X459)|~r1(X458,X459)|~r1(X457,X458)|~r1(X456,X457)|~r1(X455,X456)|~r1(X454,X455)|~r1(X453,X454)|~r1(X452,X453)|~r1(X451,X452)|~r1(X450,X451)|~r1(X449,X450)|~r1(X448,X449)|~r1(X447,X448)|~r1(X446,X447)|~r1(X445,X446)|~r1(X444,X445)|~r1(X443,X444)|~r1(X442,X443)|~r1(X441,X442)|~r1(X440,X441)|~r1(X439,X440)|~r1(X438,X439)|~r1(X437,X438)|~r1(X436,X437)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p22(X459)|~p21(X459)|~r1(X458,X459)|~r1(X457,X458)|~r1(X456,X457)|~r1(X455,X456)|~r1(X454,X455)|~r1(X453,X454)|~r1(X452,X453)|~r1(X451,X452)|~r1(X450,X451)|~r1(X449,X450)|~r1(X448,X449)|~r1(X447,X448)|~r1(X446,X447)|~r1(X445,X446)|~r1(X444,X445)|~r1(X443,X444)|~r1(X442,X443)|~r1(X441,X442)|~r1(X440,X441)|~r1(X439,X440)|~r1(X438,X439)|~r1(X437,X438)|~r1(X436,X437)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326)))&((r1(X436,esk77_5(X326,X355,X383,X410,X436))|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p22(esk77_5(X326,X355,X383,X410,X436))|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))))&((((p20(X483)|p21(X483)|~r1(X482,X483)|~r1(X481,X482)|~r1(X480,X481)|~r1(X479,X480)|~r1(X478,X479)|~r1(X477,X478)|~r1(X476,X477)|~r1(X475,X476)|~r1(X474,X475)|~r1(X473,X474)|~r1(X472,X473)|~r1(X471,X472)|~r1(X470,X471)|~r1(X469,X470)|~r1(X468,X469)|~r1(X467,X468)|~r1(X466,X467)|~r1(X465,X466)|~r1(X464,X465)|~r1(X463,X464)|~r1(X462,X463)|~r1(X461,X462)|~r1(X436,X461)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p21(X483)|~p20(X483)|~r1(X482,X483)|~r1(X481,X482)|~r1(X480,X481)|~r1(X479,X480)|~r1(X478,X479)|~r1(X477,X478)|~r1(X476,X477)|~r1(X475,X476)|~r1(X474,X475)|~r1(X473,X474)|~r1(X472,X473)|~r1(X471,X472)|~r1(X470,X471)|~r1(X469,X470)|~r1(X468,X469)|~r1(X467,X468)|~r1(X466,X467)|~r1(X465,X466)|~r1(X464,X465)|~r1(X463,X464)|~r1(X462,X463)|~r1(X461,X462)|~r1(X436,X461)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326)))&((r1(X461,esk78_6(X326,X355,X383,X410,X436,X461))|~r1(X436,X461)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))&(~p21(esk78_6(X326,X355,X383,X410,X436,X461))|~r1(X436,X461)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))))&(~r1(X461,X485)|epred3_1(X485)|~r1(X436,X461)|~r1(X410,X436)|~r1(X383,X410)|~r1(X355,X383)|~r1(X326,X355)|~epred4_1(X326))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_18])])])])])])).
% 19.59/3.04 fof(c_0_25, plain, ![X202, X203, X204, X205, X206, X207, X208, X209, X210, X211, X212, X213, X214, X215, X216, X217, X218, X219, X220, X221, X222, X223, X225, X226, X227, X228, X229, X230, X231, X232, X233, X234, X235, X236, X237, X238, X239, X240, X241, X242, X243, X244, X245, X247, X248, X249, X250, X251, X252, X253, X254, X255, X256, X257, X258, X259, X260, X261, X262, X263, X264, X265, X266, X268, X269, X270, X271, X272, X273, X274, X275, X276, X277, X278, X279, X280, X281, X282, X283, X284, X285, X286, X288, X289, X290, X291, X292, X293, X294, X295, X296, X297, X298, X299, X300, X301, X302, X303, X304, X305, X307, X308, X309, X310, X311, X312, X313, X314, X315, X316, X317, X318, X319, X320, X321, X322, X323, X325]:(((((p19(X223)|p20(X223)|~r1(X222,X223)|~r1(X221,X222)|~r1(X220,X221)|~r1(X219,X220)|~r1(X218,X219)|~r1(X217,X218)|~r1(X216,X217)|~r1(X215,X216)|~r1(X214,X215)|~r1(X213,X214)|~r1(X212,X213)|~r1(X211,X212)|~r1(X210,X211)|~r1(X209,X210)|~r1(X208,X209)|~r1(X207,X208)|~r1(X206,X207)|~r1(X205,X206)|~r1(X204,X205)|~r1(X203,X204)|~r1(X202,X203)|~epred3_1(X202))&(~p20(X223)|~p19(X223)|~r1(X222,X223)|~r1(X221,X222)|~r1(X220,X221)|~r1(X219,X220)|~r1(X218,X219)|~r1(X217,X218)|~r1(X216,X217)|~r1(X215,X216)|~r1(X214,X215)|~r1(X213,X214)|~r1(X212,X213)|~r1(X211,X212)|~r1(X210,X211)|~r1(X209,X210)|~r1(X208,X209)|~r1(X207,X208)|~r1(X206,X207)|~r1(X205,X206)|~r1(X204,X205)|~r1(X203,X204)|~r1(X202,X203)|~epred3_1(X202)))&((r1(X202,esk67_1(X202))|~epred3_1(X202))&(~p20(esk67_1(X202))|~epred3_1(X202))))&((((p18(X245)|p19(X245)|~r1(X244,X245)|~r1(X243,X244)|~r1(X242,X243)|~r1(X241,X242)|~r1(X240,X241)|~r1(X239,X240)|~r1(X238,X239)|~r1(X237,X238)|~r1(X236,X237)|~r1(X235,X236)|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(X228,X229)|~r1(X227,X228)|~r1(X226,X227)|~r1(X225,X226)|~r1(X202,X225)|~epred3_1(X202))&(~p19(X245)|~p18(X245)|~r1(X244,X245)|~r1(X243,X244)|~r1(X242,X243)|~r1(X241,X242)|~r1(X240,X241)|~r1(X239,X240)|~r1(X238,X239)|~r1(X237,X238)|~r1(X236,X237)|~r1(X235,X236)|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(X228,X229)|~r1(X227,X228)|~r1(X226,X227)|~r1(X225,X226)|~r1(X202,X225)|~epred3_1(X202)))&((r1(X225,esk68_2(X202,X225))|~r1(X202,X225)|~epred3_1(X202))&(~p19(esk68_2(X202,X225))|~r1(X202,X225)|~epred3_1(X202))))&((((p17(X266)|p18(X266)|~r1(X265,X266)|~r1(X264,X265)|~r1(X263,X264)|~r1(X262,X263)|~r1(X261,X262)|~r1(X260,X261)|~r1(X259,X260)|~r1(X258,X259)|~r1(X257,X258)|~r1(X256,X257)|~r1(X255,X256)|~r1(X254,X255)|~r1(X253,X254)|~r1(X252,X253)|~r1(X251,X252)|~r1(X250,X251)|~r1(X249,X250)|~r1(X248,X249)|~r1(X247,X248)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p18(X266)|~p17(X266)|~r1(X265,X266)|~r1(X264,X265)|~r1(X263,X264)|~r1(X262,X263)|~r1(X261,X262)|~r1(X260,X261)|~r1(X259,X260)|~r1(X258,X259)|~r1(X257,X258)|~r1(X256,X257)|~r1(X255,X256)|~r1(X254,X255)|~r1(X253,X254)|~r1(X252,X253)|~r1(X251,X252)|~r1(X250,X251)|~r1(X249,X250)|~r1(X248,X249)|~r1(X247,X248)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202)))&((r1(X247,esk69_3(X202,X225,X247))|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p18(esk69_3(X202,X225,X247))|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))))&((((p16(X286)|p17(X286)|~r1(X285,X286)|~r1(X284,X285)|~r1(X283,X284)|~r1(X282,X283)|~r1(X281,X282)|~r1(X280,X281)|~r1(X279,X280)|~r1(X278,X279)|~r1(X277,X278)|~r1(X276,X277)|~r1(X275,X276)|~r1(X274,X275)|~r1(X273,X274)|~r1(X272,X273)|~r1(X271,X272)|~r1(X270,X271)|~r1(X269,X270)|~r1(X268,X269)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p17(X286)|~p16(X286)|~r1(X285,X286)|~r1(X284,X285)|~r1(X283,X284)|~r1(X282,X283)|~r1(X281,X282)|~r1(X280,X281)|~r1(X279,X280)|~r1(X278,X279)|~r1(X277,X278)|~r1(X276,X277)|~r1(X275,X276)|~r1(X274,X275)|~r1(X273,X274)|~r1(X272,X273)|~r1(X271,X272)|~r1(X270,X271)|~r1(X269,X270)|~r1(X268,X269)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202)))&((r1(X268,esk70_4(X202,X225,X247,X268))|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p17(esk70_4(X202,X225,X247,X268))|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))))&((((p15(X305)|p16(X305)|~r1(X304,X305)|~r1(X303,X304)|~r1(X302,X303)|~r1(X301,X302)|~r1(X300,X301)|~r1(X299,X300)|~r1(X298,X299)|~r1(X297,X298)|~r1(X296,X297)|~r1(X295,X296)|~r1(X294,X295)|~r1(X293,X294)|~r1(X292,X293)|~r1(X291,X292)|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p16(X305)|~p15(X305)|~r1(X304,X305)|~r1(X303,X304)|~r1(X302,X303)|~r1(X301,X302)|~r1(X300,X301)|~r1(X299,X300)|~r1(X298,X299)|~r1(X297,X298)|~r1(X296,X297)|~r1(X295,X296)|~r1(X294,X295)|~r1(X293,X294)|~r1(X292,X293)|~r1(X291,X292)|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202)))&((r1(X288,esk71_5(X202,X225,X247,X268,X288))|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p16(esk71_5(X202,X225,X247,X268,X288))|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))))&((((p14(X323)|p15(X323)|~r1(X322,X323)|~r1(X321,X322)|~r1(X320,X321)|~r1(X319,X320)|~r1(X318,X319)|~r1(X317,X318)|~r1(X316,X317)|~r1(X315,X316)|~r1(X314,X315)|~r1(X313,X314)|~r1(X312,X313)|~r1(X311,X312)|~r1(X310,X311)|~r1(X309,X310)|~r1(X308,X309)|~r1(X307,X308)|~r1(X288,X307)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p15(X323)|~p14(X323)|~r1(X322,X323)|~r1(X321,X322)|~r1(X320,X321)|~r1(X319,X320)|~r1(X318,X319)|~r1(X317,X318)|~r1(X316,X317)|~r1(X315,X316)|~r1(X314,X315)|~r1(X313,X314)|~r1(X312,X313)|~r1(X311,X312)|~r1(X310,X311)|~r1(X309,X310)|~r1(X308,X309)|~r1(X307,X308)|~r1(X288,X307)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202)))&((r1(X307,esk72_6(X202,X225,X247,X268,X288,X307))|~r1(X288,X307)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))&(~p15(esk72_6(X202,X225,X247,X268,X288,X307))|~r1(X288,X307)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))))&(~r1(X307,X325)|epred2_1(X325)|~r1(X288,X307)|~r1(X268,X288)|~r1(X247,X268)|~r1(X225,X247)|~r1(X202,X225)|~epred3_1(X202))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])])])).
% 19.59/3.04 cnf(c_0_26, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X2)), inference(spm,[status(thm)],[c_0_20, c_0_7])).
% 19.59/3.04 fof(c_0_27, negated_conjecture, ![X32]:(((((r1(esk1_0,esk2_0)&(r1(esk2_0,esk3_0)&(r1(esk3_0,esk4_0)&(r1(esk4_0,esk5_0)&(r1(esk5_0,esk6_0)&(r1(esk6_0,esk7_0)&(r1(esk7_0,esk8_0)&(r1(esk8_0,esk9_0)&(r1(esk9_0,esk10_0)&(r1(esk10_0,esk11_0)&(r1(esk11_0,esk12_0)&(r1(esk12_0,esk13_0)&(r1(esk13_0,esk14_0)&(r1(esk14_0,esk15_0)&(r1(esk15_0,esk16_0)&(r1(esk16_0,esk17_0)&(r1(esk17_0,esk18_0)&(r1(esk18_0,esk19_0)&(r1(esk19_0,esk20_0)&(r1(esk20_0,esk21_0)&(r1(esk21_0,esk22_0)&(r1(esk22_0,esk23_0)&(r1(esk23_0,esk24_0)&(r1(esk24_0,esk25_0)&(r1(esk25_0,esk26_0)&(r1(esk26_0,esk27_0)&(p52(esk27_0)|p50(esk27_0)|p48(esk27_0)|p46(esk27_0)|p44(esk27_0)|p42(esk27_0)|p40(esk27_0)|p38(esk27_0)|p36(esk27_0)|p34(esk27_0)|p32(esk27_0)|p30(esk27_0)|p28(esk27_0)|p26(esk27_0)|p24(esk27_0)|p22(esk27_0)|p20(esk27_0)|p18(esk27_0)|p16(esk27_0)|p14(esk27_0)|p12(esk27_0)|p10(esk27_0)|p8(esk27_0)|p6(esk27_0)|p4(esk27_0)|p2(esk27_0))))))))))))))))))))))))))))&(r1(esk1_0,esk28_0)&~p27(esk28_0)))&(~r1(esk1_0,X32)|epred4_1(X32)))&(r1(esk1_0,esk29_0)&(r1(esk29_0,esk30_0)&(r1(esk30_0,esk31_0)&(r1(esk31_0,esk32_0)&(r1(esk32_0,esk33_0)&(r1(esk33_0,esk34_0)&(r1(esk34_0,esk35_0)&(r1(esk35_0,esk36_0)&(r1(esk36_0,esk37_0)&(r1(esk37_0,esk38_0)&(r1(esk38_0,esk39_0)&(r1(esk39_0,esk40_0)&(r1(esk40_0,esk41_0)&(r1(esk41_0,esk42_0)&(r1(esk42_0,esk43_0)&(r1(esk43_0,esk44_0)&(r1(esk44_0,esk45_0)&(r1(esk45_0,esk46_0)&(r1(esk46_0,esk47_0)&(r1(esk47_0,esk48_0)&(r1(esk48_0,esk49_0)&(r1(esk49_0,esk50_0)&(r1(esk50_0,esk51_0)&(r1(esk51_0,esk52_0)&(r1(esk52_0,esk53_0)&(r1(esk53_0,esk54_0)&(~p26(esk54_0)|~p25(esk54_0)|~p24(esk54_0)|~p23(esk54_0)|~p22(esk54_0)|~p21(esk54_0)|~p20(esk54_0)|~p19(esk54_0)|~p18(esk54_0)|~p17(esk54_0)|~p16(esk54_0)|~p15(esk54_0)|~p14(esk54_0)|~p13(esk54_0)|~p12(esk54_0)|~p11(esk54_0)|~p10(esk54_0)|~p9(esk54_0)|~p8(esk54_0)|~p7(esk54_0)|~p6(esk54_0)|~p5(esk54_0)|~p4(esk54_0)|~p3(esk54_0)|~p2(esk54_0)|~p1(esk54_0)))))))))))))))))))))))))))))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])])])).
% 19.59/3.04 cnf(c_0_28, plain, (~epred1_1(X1)|~p7(X2)|~p6(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_22, c_0_7])).
% 19.59/3.04 cnf(c_0_29, plain, (epred1_1(X1)|~epred2_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_23, c_0_7])).
% 19.59/3.04 cnf(c_0_30, plain, (p25(X1)|p1(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_31, plain, (p20(X1)|p21(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_32, plain, (p21(X1)|p22(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_33, plain, (p22(X1)|p23(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_34, plain, (p23(X1)|p24(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_35, plain, (~p1(X1)|~p25(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_36, plain, (~p21(X1)|~p20(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_37, plain, (~p22(X1)|~p21(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_38, plain, (~p23(X1)|~p22(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_39, plain, (p24(X1)|p25(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.04 cnf(c_0_40, plain, (~p24(X1)|~p23(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.05 cnf(c_0_41, plain, (~p25(X1)|~p24(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~r1(X23,X22)|~r1(X24,X23)|~r1(X25,X24)|~r1(X26,X25)|~r1(X27,X26)|~r1(X28,X27)|~epred4_1(X28)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.05 cnf(c_0_42, plain, (p14(X1)|p15(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_43, plain, (p15(X1)|p16(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_44, plain, (p16(X1)|p17(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_45, plain, (p17(X1)|p18(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_46, plain, (p18(X1)|p19(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_47, plain, (~p15(X1)|~p14(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_48, plain, (~p16(X1)|~p15(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_49, plain, (~p17(X1)|~p16(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_50, plain, (p19(X1)|p20(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_51, plain, (~p18(X1)|~p17(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_52, plain, (~p19(X1)|~p18(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_53, plain, (~p20(X1)|~p19(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~r1(X17,X16)|~r1(X18,X17)|~r1(X19,X18)|~r1(X20,X19)|~r1(X21,X20)|~r1(X22,X21)|~epred3_1(X22)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_54, plain, (p8(X1)|p9(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_55, plain, (~p9(X1)|~p8(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_56, plain, (p13(X1)|p14(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_57, plain, (~p14(X1)|~p13(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_58, plain, (p2(X1)|p3(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_59, plain, (p3(X1)|p4(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_60, plain, (p4(X1)|p5(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_61, plain, (~p3(X1)|~p2(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_62, plain, (p5(X1)|p6(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_63, plain, (~p4(X1)|~p3(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_64, plain, (~p5(X1)|~p4(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_65, plain, (~p6(X1)|~p5(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_66, plain, (p6(X1)|p7(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_67, plain, (p7(X1)|p8(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_68, plain, (epred2_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~epred3_1(X7)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 19.59/3.05 cnf(c_0_69, plain, (~epred1_1(X1)|~p7(X2)|~p8(X2)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_26, c_0_7])).
% 19.59/3.05 cnf(c_0_70, negated_conjecture, (epred4_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 19.59/3.05 cnf(c_0_71, negated_conjecture, (r1(esk1_0,esk2_0)), inference(split_conjunct,[status(thm)],[c_0_27])).
% 19.59/3.05 cnf(c_0_72, plain, (~epred1_1(X1)|~p7(X2)|~p6(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X2)), inference(spm,[status(thm)],[c_0_28, c_0_7])).
% 19.59/3.05 cnf(c_0_73, plain, (epred1_1(X1)|~epred2_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X1)), inference(spm,[status(thm)],[c_0_29, c_0_7])).
% 19.59/3.05 cnf(c_0_74, plain, (p1(X1)|p25(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_30, c_0_7])).
% 19.59/3.05 cnf(c_0_75, plain, (p21(X1)|p20(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_31, c_0_7])).
% 19.59/3.05 cnf(c_0_76, plain, (p21(X1)|p22(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_32, c_0_7])).
% 19.59/3.05 cnf(c_0_77, plain, (p23(X1)|p22(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_33, c_0_7])).
% 19.59/3.05 cnf(c_0_78, plain, (p23(X1)|p24(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_34, c_0_7])).
% 19.59/3.05 cnf(c_0_79, plain, (~epred4_1(X1)|~p1(X2)|~p25(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_35, c_0_7])).
% 19.59/3.05 cnf(c_0_80, plain, (~epred4_1(X1)|~p21(X2)|~p20(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_36, c_0_7])).
% 19.59/3.05 cnf(c_0_81, plain, (~epred4_1(X1)|~p21(X2)|~p22(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_37, c_0_7])).
% 19.59/3.05 cnf(c_0_82, plain, (~epred4_1(X1)|~p23(X2)|~p22(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_38, c_0_7])).
% 19.59/3.05 cnf(c_0_83, plain, (p25(X1)|p24(X1)|~epred4_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X1)), inference(spm,[status(thm)],[c_0_39, c_0_7])).
% 19.59/3.05 cnf(c_0_84, plain, (~epred4_1(X1)|~p23(X2)|~p24(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_40, c_0_7])).
% 19.59/3.05 cnf(c_0_85, plain, (~epred4_1(X1)|~p25(X2)|~p24(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X22)|~r1(X22,X23)|~r1(X23,X24)|~r1(X24,X25)|~r1(X25,X26)|~r1(X26,X27)|~r1(X27,X2)), inference(spm,[status(thm)],[c_0_41, c_0_7])).
% 19.59/3.05 cnf(c_0_86, plain, (p15(X1)|p14(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_42, c_0_7])).
% 19.59/3.05 cnf(c_0_87, plain, (p15(X1)|p16(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_43, c_0_7])).
% 19.59/3.05 cnf(c_0_88, plain, (p17(X1)|p16(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_44, c_0_7])).
% 19.59/3.05 cnf(c_0_89, plain, (p17(X1)|p18(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_45, c_0_7])).
% 19.59/3.05 cnf(c_0_90, plain, (p19(X1)|p18(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_46, c_0_7])).
% 19.59/3.05 cnf(c_0_91, plain, (~epred3_1(X1)|~p15(X2)|~p14(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_47, c_0_7])).
% 19.59/3.05 cnf(c_0_92, plain, (~epred3_1(X1)|~p15(X2)|~p16(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_48, c_0_7])).
% 19.59/3.05 cnf(c_0_93, plain, (~epred3_1(X1)|~p17(X2)|~p16(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_49, c_0_7])).
% 19.59/3.05 cnf(c_0_94, plain, (p19(X1)|p20(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X1)), inference(spm,[status(thm)],[c_0_50, c_0_7])).
% 19.59/3.05 cnf(c_0_95, plain, (~epred3_1(X1)|~p17(X2)|~p18(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_51, c_0_7])).
% 19.59/3.05 cnf(c_0_96, plain, (~epred3_1(X1)|~p19(X2)|~p18(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_52, c_0_7])).
% 19.59/3.05 cnf(c_0_97, plain, (~epred3_1(X1)|~p19(X2)|~p20(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X16)|~r1(X16,X17)|~r1(X17,X18)|~r1(X18,X19)|~r1(X19,X20)|~r1(X20,X21)|~r1(X21,X2)), inference(spm,[status(thm)],[c_0_53, c_0_7])).
% 19.59/3.05 cnf(c_0_98, plain, (p9(X1)|p8(X1)|~epred2_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X1)), inference(spm,[status(thm)],[c_0_54, c_0_7])).
% 19.59/3.05 cnf(c_0_99, plain, (~epred2_1(X1)|~p9(X2)|~p8(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X2)), inference(spm,[status(thm)],[c_0_55, c_0_7])).
% 19.59/3.05 cnf(c_0_100, plain, (p13(X1)|p14(X1)|~epred2_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X1)), inference(spm,[status(thm)],[c_0_56, c_0_7])).
% 19.59/3.05 cnf(c_0_101, plain, (~epred2_1(X1)|~p13(X2)|~p14(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X10)|~r1(X10,X11)|~r1(X11,X12)|~r1(X12,X13)|~r1(X13,X14)|~r1(X14,X15)|~r1(X15,X2)), inference(spm,[status(thm)],[c_0_57, c_0_7])).
% 19.59/3.05 cnf(c_0_102, plain, (p3(X1)|p2(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_58, c_0_7])).
% 19.59/3.05 cnf(c_0_103, plain, (p3(X1)|p4(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_59, c_0_7])).
% 19.59/3.05 cnf(c_0_104, plain, (p5(X1)|p4(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_60, c_0_7])).
% 19.59/3.05 cnf(c_0_105, plain, (~epred1_1(X1)|~p3(X2)|~p2(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_61, c_0_7])).
% 19.59/3.05 cnf(c_0_106, plain, (p5(X1)|p6(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_62, c_0_7])).
% 19.59/3.05 cnf(c_0_107, plain, (~epred1_1(X1)|~p3(X2)|~p4(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_63, c_0_7])).
% 19.59/3.05 cnf(c_0_108, plain, (~epred1_1(X1)|~p5(X2)|~p4(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_64, c_0_7])).
% 19.59/3.05 cnf(c_0_109, plain, (~epred1_1(X1)|~p5(X2)|~p6(X2)|~r1(X1,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X2)), inference(spm,[status(thm)],[c_0_65, c_0_7])).
% 19.59/3.05 cnf(c_0_110, plain, (p7(X1)|p6(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_66, c_0_7])).
% 19.59/3.05 cnf(c_0_111, plain, (p7(X1)|p8(X1)|~epred1_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)|~r1(X8,X9)|~r1(X9,X1)), inference(spm,[status(thm)],[c_0_67, c_0_7])).
% 19.59/3.05 cnf(c_0_112, plain, (epred2_1(X1)|~epred3_1(X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X1)), inference(spm,[status(thm)],[c_0_68, c_0_7])).
% 19.59/3.05 cnf(c_0_113, plain, (~epred1_1(X1)|~p7(X1)|~p8(X1)), inference(spm,[status(thm)],[c_0_69, c_0_7])).
% 19.59/3.05 cnf(c_0_114, plain, (p9(X1)|p10(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_115, plain, (p10(X1)|p11(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_116, plain, (p11(X1)|p12(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_117, plain, (p12(X1)|p13(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_118, plain, (~p10(X1)|~p9(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_119, plain, (~p11(X1)|~p10(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_120, plain, (~p12(X1)|~p11(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_121, plain, (~p13(X1)|~p12(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~r1(X11,X10)|~r1(X12,X11)|~r1(X13,X12)|~r1(X14,X13)|~r1(X15,X14)|~r1(X16,X15)|~epred2_1(X16)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 19.59/3.05 cnf(c_0_122, plain, (p1(X1)|p2(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_123, plain, (~p2(X1)|~p1(X1)|~r1(X2,X1)|~r1(X3,X2)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X8,X7)|~r1(X9,X8)|~r1(X10,X9)|~epred1_1(X10)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 19.59/3.05 cnf(c_0_124, plain, (epred3_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~epred4_1(X7)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 19.59/3.05 cnf(c_0_125, negated_conjecture, (epred4_1(esk2_0)), inference(spm,[status(thm)],[c_0_70, c_0_71])).
% 19.59/3.05 cnf(c_0_126, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_72, c_0_73, c_0_74, c_0_75, c_0_76, c_0_77, c_0_78, c_0_79, c_0_80, c_0_81, c_0_82, c_0_83, c_0_84, c_0_85, c_0_86, c_0_87, c_0_88, c_0_89, c_0_90, c_0_91, c_0_92, c_0_93, c_0_94, c_0_95, c_0_96, c_0_97, c_0_98, c_0_99, c_0_100, c_0_101, c_0_102, c_0_103, c_0_104, c_0_105, c_0_106, c_0_107, c_0_108, c_0_109, c_0_110, c_0_111, c_0_112, c_0_113, c_0_114, c_0_115, c_0_116, c_0_117, c_0_118, c_0_119, c_0_120, c_0_121, c_0_122, c_0_123, c_0_124, c_0_125, c_0_7]), ['proof']).
% 19.59/3.05 % SZS output end Proof
% 19.59/3.05 % User time : 2.348 s
% 19.59/3.05 % System time : 0.029 s
% 19.59/3.05 % Total time : 2.377 s
% 19.59/3.05 % User time : 11.381 s
% 19.59/3.05 % System time : 0.157 s
% 19.59/3.05 % Total time : 11.538 s
% 19.59/3.05
%------------------------------------------------------------------------------