%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n010.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:14 AM UTC 2026
% Result : Theorem 21.67s 3.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL636+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 : n010.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 16:11:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.23/0.49 start to proof:theBenchmark.p
% 21.67/3.32 % Version : CSI_E---1.1
% 21.67/3.32 % Problem : theBenchmark.p
% 21.67/3.32 % Proof found!
% 21.67/3.32 % SZS status Theorem for theBenchmark.p
% 21.67/3.32 % SZS output start Proof
% 21.67/3.32 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(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))|~(((~(p6(X1))&~(p106(X1)))&p105(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1)))))))|~((~(p105(X2))&p104(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1)))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1)))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1)))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1))|~(p105(X1))))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1)|~(p105(X1))))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1))|~(p104(X1))))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1)|~(p104(X1))))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1))|~(p103(X1))))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1)|~(p103(X1))))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1))|~(p102(X1))))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1)|~(p102(X1))))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1))|~(p101(X1))))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1)|~(p101(X1))))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1))|~(p100(X1))))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1)|~(p100(X1))))|~(p1(X2))))|~(p100(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2))))))))))))))&![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((((((((((((((((((~(![X2]:((~(r1(X1,X2))|~(((~(p6(X2))&~(p106(X2)))&p105(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p106(X2)))&p105(X2)))))))|~((~(p105(X1))&p104(X1))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p5(X2))&~(p105(X2)))&p104(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p5(X2)&~(p105(X2)))&p104(X2)))))))|~((~(p104(X1))&p103(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p4(X2))&~(p104(X2)))&p103(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p104(X2)))&p103(X2)))))))|~((~(p103(X1))&p102(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p3(X2))&~(p103(X2)))&p102(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p3(X2)&~(p103(X2)))&p102(X2)))))))|~((~(p102(X1))&p101(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p2(X2))&~(p102(X2)))&p101(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p102(X2)))&p101(X2)))))))|~((~(p101(X1))&p100(X1)))))&(((![X2]:((~(r1(X1,X2))|~(p6(X2))|~(p105(X2))))|p6(X1))&(![X2]:((~(r1(X1,X2))|p6(X2)|~(p105(X2))))|~(p6(X1))))|~(p105(X1))))&(((![X2]:((~(r1(X1,X2))|~(p5(X2))|~(p104(X2))))|p5(X1))&(![X2]:((~(r1(X1,X2))|p5(X2)|~(p104(X2))))|~(p5(X1))))|~(p104(X1))))&(((![X2]:((~(r1(X1,X2))|~(p4(X2))|~(p103(X2))))|p4(X1))&(![X2]:((~(r1(X1,X2))|p4(X2)|~(p103(X2))))|~(p4(X1))))|~(p103(X1))))&(((![X2]:((~(r1(X1,X2))|~(p3(X2))|~(p102(X2))))|p3(X1))&(![X2]:((~(r1(X1,X2))|p3(X2)|~(p102(X2))))|~(p3(X1))))|~(p102(X1))))&(((![X2]:((~(r1(X1,X2))|~(p2(X2))|~(p101(X2))))|p2(X1))&(![X2]:((~(r1(X1,X2))|p2(X2)|~(p101(X2))))|~(p2(X1))))|~(p101(X1))))&(((![X2]:((~(r1(X1,X2))|~(p1(X2))|~(p100(X2))))|p1(X1))&(![X2]:((~(r1(X1,X2))|p1(X2)|~(p100(X2))))|~(p1(X1))))|~(p100(X1))))&(p105(X1)|~(p106(X1))))&(p104(X1)|~(p105(X1))))&(p103(X1)|~(p104(X1))))&(p102(X1)|~(p103(X1))))&(p101(X1)|~(p102(X1))))&(p100(X1)|~(p101(X1)))))))))))))&![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((((((((((((((((((~(![X1]:((~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1)))))))|~((~(p105(X2))&p104(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1)))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1)))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1)))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1))|~(p105(X1))))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1)|~(p105(X1))))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1))|~(p104(X1))))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1)|~(p104(X1))))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1))|~(p103(X1))))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1)|~(p103(X1))))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1))|~(p102(X1))))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1)|~(p102(X1))))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1))|~(p101(X1))))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1)|~(p101(X1))))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1))|~(p100(X1))))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1)|~(p100(X1))))|~(p1(X2))))|~(p100(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2)))))))))))&![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((((((((((((((((((~(![X2]:((~(r1(X1,X2))|~(((~(p6(X2))&~(p106(X2)))&p105(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p106(X2)))&p105(X2)))))))|~((~(p105(X1))&p104(X1))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p5(X2))&~(p105(X2)))&p104(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p5(X2)&~(p105(X2)))&p104(X2)))))))|~((~(p104(X1))&p103(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p4(X2))&~(p104(X2)))&p103(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p104(X2)))&p103(X2)))))))|~((~(p103(X1))&p102(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p3(X2))&~(p103(X2)))&p102(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p3(X2)&~(p103(X2)))&p102(X2)))))))|~((~(p102(X1))&p101(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p2(X2))&~(p102(X2)))&p101(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p102(X2)))&p101(X2)))))))|~((~(p101(X1))&p100(X1)))))&(((![X2]:((~(r1(X1,X2))|~(p6(X2))|~(p105(X2))))|p6(X1))&(![X2]:((~(r1(X1,X2))|p6(X2)|~(p105(X2))))|~(p6(X1))))|~(p105(X1))))&(((![X2]:((~(r1(X1,X2))|~(p5(X2))|~(p104(X2))))|p5(X1))&(![X2]:((~(r1(X1,X2))|p5(X2)|~(p104(X2))))|~(p5(X1))))|~(p104(X1))))&(((![X2]:((~(r1(X1,X2))|~(p4(X2))|~(p103(X2))))|p4(X1))&(![X2]:((~(r1(X1,X2))|p4(X2)|~(p103(X2))))|~(p4(X1))))|~(p103(X1))))&(((![X2]:((~(r1(X1,X2))|~(p3(X2))|~(p102(X2))))|p3(X1))&(![X2]:((~(r1(X1,X2))|p3(X2)|~(p102(X2))))|~(p3(X1))))|~(p102(X1))))&(((![X2]:((~(r1(X1,X2))|~(p2(X2))|~(p101(X2))))|p2(X1))&(![X2]:((~(r1(X1,X2))|p2(X2)|~(p101(X2))))|~(p2(X1))))|~(p101(X1))))&(((![X2]:((~(r1(X1,X2))|~(p1(X2))|~(p100(X2))))|p1(X1))&(![X2]:((~(r1(X1,X2))|p1(X2)|~(p100(X2))))|~(p1(X1))))|~(p100(X1))))&(p105(X1)|~(p106(X1))))&(p104(X1)|~(p105(X1))))&(p103(X1)|~(p104(X1))))&(p102(X1)|~(p103(X1))))&(p101(X1)|~(p102(X1))))&(p100(X1)|~(p101(X1)))))))))&![X2]:((~(r1(X1,X2))|((((((((((((((((((~(![X1]:((~(r1(X2,X1))|~(((~(p6(X1))&~(p106(X1)))&p105(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p6(X1)&~(p106(X1)))&p105(X1)))))))|~((~(p105(X2))&p104(X2))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p5(X1))&~(p105(X1)))&p104(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p5(X1)&~(p105(X1)))&p104(X1)))))))|~((~(p104(X2))&p103(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p4(X1))&~(p104(X1)))&p103(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p4(X1)&~(p104(X1)))&p103(X1)))))))|~((~(p103(X2))&p102(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p3(X1))&~(p103(X1)))&p102(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p3(X1)&~(p103(X1)))&p102(X1)))))))|~((~(p102(X2))&p101(X2)))))&((~(![X1]:((~(r1(X2,X1))|~(((~(p2(X1))&~(p102(X1)))&p101(X1))))))&~(![X1]:((~(r1(X2,X1))|~(((p2(X1)&~(p102(X1)))&p101(X1)))))))|~((~(p101(X2))&p100(X2)))))&(((![X1]:((~(r1(X2,X1))|~(p6(X1))|~(p105(X1))))|p6(X2))&(![X1]:((~(r1(X2,X1))|p6(X1)|~(p105(X1))))|~(p6(X2))))|~(p105(X2))))&(((![X1]:((~(r1(X2,X1))|~(p5(X1))|~(p104(X1))))|p5(X2))&(![X1]:((~(r1(X2,X1))|p5(X1)|~(p104(X1))))|~(p5(X2))))|~(p104(X2))))&(((![X1]:((~(r1(X2,X1))|~(p4(X1))|~(p103(X1))))|p4(X2))&(![X1]:((~(r1(X2,X1))|p4(X1)|~(p103(X1))))|~(p4(X2))))|~(p103(X2))))&(((![X1]:((~(r1(X2,X1))|~(p3(X1))|~(p102(X1))))|p3(X2))&(![X1]:((~(r1(X2,X1))|p3(X1)|~(p102(X1))))|~(p3(X2))))|~(p102(X2))))&(((![X1]:((~(r1(X2,X1))|~(p2(X1))|~(p101(X1))))|p2(X2))&(![X1]:((~(r1(X2,X1))|p2(X1)|~(p101(X1))))|~(p2(X2))))|~(p101(X2))))&(((![X1]:((~(r1(X2,X1))|~(p1(X1))|~(p100(X1))))|p1(X2))&(![X1]:((~(r1(X2,X1))|p1(X1)|~(p100(X1))))|~(p1(X2))))|~(p100(X2))))&(p105(X2)|~(p106(X2))))&(p104(X2)|~(p105(X2))))&(p103(X2)|~(p104(X2))))&(p102(X2)|~(p103(X2))))&(p101(X2)|~(p102(X2))))&(p100(X2)|~(p101(X2)))))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p6(X2))&~(p106(X2)))&p105(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p6(X2)&~(p106(X2)))&p105(X2)))))))|~((~(p105(X1))&p104(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p5(X2))&~(p105(X2)))&p104(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p5(X2)&~(p105(X2)))&p104(X2)))))))|~((~(p104(X1))&p103(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p4(X2))&~(p104(X2)))&p103(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p4(X2)&~(p104(X2)))&p103(X2)))))))|~((~(p103(X1))&p102(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p3(X2))&~(p103(X2)))&p102(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p3(X2)&~(p103(X2)))&p102(X2)))))))|~((~(p102(X1))&p101(X1)))))&((~(![X2]:((~(r1(X1,X2))|~(((~(p2(X2))&~(p102(X2)))&p101(X2))))))&~(![X2]:((~(r1(X1,X2))|~(((p2(X2)&~(p102(X2)))&p101(X2)))))))|~((~(p101(X1))&p100(X1)))))&(((![X2]:((~(r1(X1,X2))|~(p6(X2))|~(p105(X2))))|p6(X1))&(![X2]:((~(r1(X1,X2))|p6(X2)|~(p105(X2))))|~(p6(X1))))|~(p105(X1))))&(((![X2]:((~(r1(X1,X2))|~(p5(X2))|~(p104(X2))))|p5(X1))&(![X2]:((~(r1(X1,X2))|p5(X2)|~(p104(X2))))|~(p5(X1))))|~(p104(X1))))&(((![X2]:((~(r1(X1,X2))|~(p4(X2))|~(p103(X2))))|p4(X1))&(![X2]:((~(r1(X1,X2))|p4(X2)|~(p103(X2))))|~(p4(X1))))|~(p103(X1))))&(((![X2]:((~(r1(X1,X2))|~(p3(X2))|~(p102(X2))))|p3(X1))&(![X2]:((~(r1(X1,X2))|p3(X2)|~(p102(X2))))|~(p3(X1))))|~(p102(X1))))&(((![X2]:((~(r1(X1,X2))|~(p2(X2))|~(p101(X2))))|p2(X1))&(![X2]:((~(r1(X1,X2))|p2(X2)|~(p101(X2))))|~(p2(X1))))|~(p101(X1))))&(((![X2]:((~(r1(X1,X2))|~(p1(X2))|~(p100(X2))))|p1(X1))&(![X2]:((~(r1(X1,X2))|p1(X2)|~(p100(X2))))|~(p1(X1))))|~(p100(X1))))&(p105(X1)|~(p106(X1))))&(p104(X1)|~(p105(X1))))&(p103(X1)|~(p104(X1))))&(p102(X1)|~(p103(X1))))&(p101(X1)|~(p102(X1))))&(p100(X1)|~(p101(X1))))&~(p101(X1)))&p100(X1))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 21.67/3.32 fof(c_0_1, plain, ![X2]:((epred1_1(X2)<=>((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), introduced(definition)).
% 21.67/3.32 fof(c_0_2, plain, ![X1]:((epred2_1(X1)<=>((((((((((((((((((~(![X2]:((~r1(X1,X2)|~(((~p6(X2)&~p106(X2))&p105(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p106(X2))&p105(X2)))))))|~((~p105(X1)&p104(X1))))&((~(![X2]:((~r1(X1,X2)|~(((~p5(X2)&~p105(X2))&p104(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p5(X2)&~p105(X2))&p104(X2)))))))|~((~p104(X1)&p103(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p4(X2)&~p104(X2))&p103(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p104(X2))&p103(X2)))))))|~((~p103(X1)&p102(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p3(X2)&~p103(X2))&p102(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p3(X2)&~p103(X2))&p102(X2)))))))|~((~p102(X1)&p101(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p2(X2)&~p102(X2))&p101(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p102(X2))&p101(X2)))))))|~((~p101(X1)&p100(X1)))))&(((![X2]:((~r1(X1,X2)|~p6(X2)|~p105(X2)))|p6(X1))&(![X2]:((~r1(X1,X2)|p6(X2)|~p105(X2)))|~p6(X1)))|~p105(X1)))&(((![X2]:((~r1(X1,X2)|~p5(X2)|~p104(X2)))|p5(X1))&(![X2]:((~r1(X1,X2)|p5(X2)|~p104(X2)))|~p5(X1)))|~p104(X1)))&(((![X2]:((~r1(X1,X2)|~p4(X2)|~p103(X2)))|p4(X1))&(![X2]:((~r1(X1,X2)|p4(X2)|~p103(X2)))|~p4(X1)))|~p103(X1)))&(((![X2]:((~r1(X1,X2)|~p3(X2)|~p102(X2)))|p3(X1))&(![X2]:((~r1(X1,X2)|p3(X2)|~p102(X2)))|~p3(X1)))|~p102(X1)))&(((![X2]:((~r1(X1,X2)|~p2(X2)|~p101(X2)))|p2(X1))&(![X2]:((~r1(X1,X2)|p2(X2)|~p101(X2)))|~p2(X1)))|~p101(X1)))&(((![X2]:((~r1(X1,X2)|~p1(X2)|~p100(X2)))|p1(X1))&(![X2]:((~r1(X1,X2)|p1(X2)|~p100(X2)))|~p1(X1)))|~p100(X1)))&(p105(X1)|~p106(X1)))&(p104(X1)|~p105(X1)))&(p103(X1)|~p104(X1)))&(p102(X1)|~p103(X1)))&(p101(X1)|~p102(X1)))&(p100(X1)|~p101(X1))))), introduced(definition)).
% 21.67/3.32 fof(c_0_3, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2))))))))))))|~((((((((((((((((((((((((![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|epred1_1(X2)))))))))))&![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|epred2_1(X1))))))))))&![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|epred1_1(X2))))))))&![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|epred2_1(X1))))))&![X2]:((~r1(X1,X2)|epred1_1(X2))))&((~(![X2]:((~r1(X1,X2)|~(((~p6(X2)&~p106(X2))&p105(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p106(X2))&p105(X2)))))))|~((~p105(X1)&p104(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p5(X2)&~p105(X2))&p104(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p5(X2)&~p105(X2))&p104(X2)))))))|~((~p104(X1)&p103(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p4(X2)&~p104(X2))&p103(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p104(X2))&p103(X2)))))))|~((~p103(X1)&p102(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p3(X2)&~p103(X2))&p102(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p3(X2)&~p103(X2))&p102(X2)))))))|~((~p102(X1)&p101(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p2(X2)&~p102(X2))&p101(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p102(X2))&p101(X2)))))))|~((~p101(X1)&p100(X1)))))&(((![X2]:((~r1(X1,X2)|~p6(X2)|~p105(X2)))|p6(X1))&(![X2]:((~r1(X1,X2)|p6(X2)|~p105(X2)))|~p6(X1)))|~p105(X1)))&(((![X2]:((~r1(X1,X2)|~p5(X2)|~p104(X2)))|p5(X1))&(![X2]:((~r1(X1,X2)|p5(X2)|~p104(X2)))|~p5(X1)))|~p104(X1)))&(((![X2]:((~r1(X1,X2)|~p4(X2)|~p103(X2)))|p4(X1))&(![X2]:((~r1(X1,X2)|p4(X2)|~p103(X2)))|~p4(X1)))|~p103(X1)))&(((![X2]:((~r1(X1,X2)|~p3(X2)|~p102(X2)))|p3(X1))&(![X2]:((~r1(X1,X2)|p3(X2)|~p102(X2)))|~p3(X1)))|~p102(X1)))&(((![X2]:((~r1(X1,X2)|~p2(X2)|~p101(X2)))|p2(X1))&(![X2]:((~r1(X1,X2)|p2(X2)|~p101(X2)))|~p2(X1)))|~p101(X1)))&(((![X2]:((~r1(X1,X2)|~p1(X2)|~p100(X2)))|p1(X1))&(![X2]:((~r1(X1,X2)|p1(X2)|~p100(X2)))|~p1(X1)))|~p100(X1)))&(p105(X1)|~p106(X1)))&(p104(X1)|~p105(X1)))&(p103(X1)|~p104(X1)))&(p102(X1)|~p103(X1)))&(p101(X1)|~p102(X1)))&(p100(X1)|~p101(X1)))&~p101(X1))&p100(X1)))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1]), c_0_2]), c_0_1]), c_0_2]), c_0_1])).
% 21.67/3.32 fof(c_0_4, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X34, X35, X36, X37, X38, X39, X40, X41, X42, X43, X44, X45]:(((~r1(esk1_0,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|(~r1(X7,X8)|p3(X8))))))&((((((((((((((((((((((((~r1(esk1_0,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|epred1_1(X13))))))&(~r1(esk1_0,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|epred2_1(X17))))))&(~r1(esk1_0,X18)|(~r1(X18,X19)|(~r1(X19,X20)|epred1_1(X20)))))&(~r1(esk1_0,X21)|(~r1(X21,X22)|epred2_1(X22))))&(~r1(esk1_0,X23)|epred1_1(X23)))&(((r1(esk1_0,esk2_0)|(p105(esk1_0)|~p104(esk1_0)))&(((~p6(esk2_0)|(p105(esk1_0)|~p104(esk1_0)))&(~p106(esk2_0)|(p105(esk1_0)|~p104(esk1_0))))&(p105(esk2_0)|(p105(esk1_0)|~p104(esk1_0)))))&((r1(esk1_0,esk3_0)|(p105(esk1_0)|~p104(esk1_0)))&(((p6(esk3_0)|(p105(esk1_0)|~p104(esk1_0)))&(~p106(esk3_0)|(p105(esk1_0)|~p104(esk1_0))))&(p105(esk3_0)|(p105(esk1_0)|~p104(esk1_0)))))))&(((r1(esk1_0,esk4_0)|(p104(esk1_0)|~p103(esk1_0)))&(((~p5(esk4_0)|(p104(esk1_0)|~p103(esk1_0)))&(~p105(esk4_0)|(p104(esk1_0)|~p103(esk1_0))))&(p104(esk4_0)|(p104(esk1_0)|~p103(esk1_0)))))&((r1(esk1_0,esk5_0)|(p104(esk1_0)|~p103(esk1_0)))&(((p5(esk5_0)|(p104(esk1_0)|~p103(esk1_0)))&(~p105(esk5_0)|(p104(esk1_0)|~p103(esk1_0))))&(p104(esk5_0)|(p104(esk1_0)|~p103(esk1_0)))))))&(((r1(esk1_0,esk6_0)|(p103(esk1_0)|~p102(esk1_0)))&(((~p4(esk6_0)|(p103(esk1_0)|~p102(esk1_0)))&(~p104(esk6_0)|(p103(esk1_0)|~p102(esk1_0))))&(p103(esk6_0)|(p103(esk1_0)|~p102(esk1_0)))))&((r1(esk1_0,esk7_0)|(p103(esk1_0)|~p102(esk1_0)))&(((p4(esk7_0)|(p103(esk1_0)|~p102(esk1_0)))&(~p104(esk7_0)|(p103(esk1_0)|~p102(esk1_0))))&(p103(esk7_0)|(p103(esk1_0)|~p102(esk1_0)))))))&(((r1(esk1_0,esk8_0)|(p102(esk1_0)|~p101(esk1_0)))&(((~p3(esk8_0)|(p102(esk1_0)|~p101(esk1_0)))&(~p103(esk8_0)|(p102(esk1_0)|~p101(esk1_0))))&(p102(esk8_0)|(p102(esk1_0)|~p101(esk1_0)))))&((r1(esk1_0,esk9_0)|(p102(esk1_0)|~p101(esk1_0)))&(((p3(esk9_0)|(p102(esk1_0)|~p101(esk1_0)))&(~p103(esk9_0)|(p102(esk1_0)|~p101(esk1_0))))&(p102(esk9_0)|(p102(esk1_0)|~p101(esk1_0)))))))&(((r1(esk1_0,esk10_0)|(p101(esk1_0)|~p100(esk1_0)))&(((~p2(esk10_0)|(p101(esk1_0)|~p100(esk1_0)))&(~p102(esk10_0)|(p101(esk1_0)|~p100(esk1_0))))&(p101(esk10_0)|(p101(esk1_0)|~p100(esk1_0)))))&((r1(esk1_0,esk11_0)|(p101(esk1_0)|~p100(esk1_0)))&(((p2(esk11_0)|(p101(esk1_0)|~p100(esk1_0)))&(~p102(esk11_0)|(p101(esk1_0)|~p100(esk1_0))))&(p101(esk11_0)|(p101(esk1_0)|~p100(esk1_0)))))))&((~r1(esk1_0,X34)|~p6(X34)|~p105(X34)|p6(esk1_0)|~p105(esk1_0))&(~r1(esk1_0,X35)|p6(X35)|~p105(X35)|~p6(esk1_0)|~p105(esk1_0))))&((~r1(esk1_0,X36)|~p5(X36)|~p104(X36)|p5(esk1_0)|~p104(esk1_0))&(~r1(esk1_0,X37)|p5(X37)|~p104(X37)|~p5(esk1_0)|~p104(esk1_0))))&((~r1(esk1_0,X38)|~p4(X38)|~p103(X38)|p4(esk1_0)|~p103(esk1_0))&(~r1(esk1_0,X39)|p4(X39)|~p103(X39)|~p4(esk1_0)|~p103(esk1_0))))&((~r1(esk1_0,X40)|~p3(X40)|~p102(X40)|p3(esk1_0)|~p102(esk1_0))&(~r1(esk1_0,X41)|p3(X41)|~p102(X41)|~p3(esk1_0)|~p102(esk1_0))))&((~r1(esk1_0,X42)|~p2(X42)|~p101(X42)|p2(esk1_0)|~p101(esk1_0))&(~r1(esk1_0,X43)|p2(X43)|~p101(X43)|~p2(esk1_0)|~p101(esk1_0))))&((~r1(esk1_0,X44)|~p1(X44)|~p100(X44)|p1(esk1_0)|~p100(esk1_0))&(~r1(esk1_0,X45)|p1(X45)|~p100(X45)|~p1(esk1_0)|~p100(esk1_0))))&(p105(esk1_0)|~p106(esk1_0)))&(p104(esk1_0)|~p105(esk1_0)))&(p103(esk1_0)|~p104(esk1_0)))&(p102(esk1_0)|~p103(esk1_0)))&(p101(esk1_0)|~p102(esk1_0)))&(p100(esk1_0)|~p101(esk1_0)))&~p101(esk1_0))&p100(esk1_0)))), 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])])])])])])).
% 21.67/3.32 cnf(c_0_5, negated_conjecture, (r1(esk1_0,esk11_0)|p101(esk1_0)|~p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_6, negated_conjecture, (p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_7, negated_conjecture, (~p101(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 fof(c_0_8, plain, ![X2]:((epred1_1(X2)=>((((((((((((((((((~(![X1]:((~r1(X2,X1)|~(((~p6(X1)&~p106(X1))&p105(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p6(X1)&~p106(X1))&p105(X1)))))))|~((~p105(X2)&p104(X2))))&((~(![X1]:((~r1(X2,X1)|~(((~p5(X1)&~p105(X1))&p104(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p5(X1)&~p105(X1))&p104(X1)))))))|~((~p104(X2)&p103(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p4(X1)&~p104(X1))&p103(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p4(X1)&~p104(X1))&p103(X1)))))))|~((~p103(X2)&p102(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p3(X1)&~p103(X1))&p102(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p3(X1)&~p103(X1))&p102(X1)))))))|~((~p102(X2)&p101(X2)))))&((~(![X1]:((~r1(X2,X1)|~(((~p2(X1)&~p102(X1))&p101(X1))))))&~(![X1]:((~r1(X2,X1)|~(((p2(X1)&~p102(X1))&p101(X1)))))))|~((~p101(X2)&p100(X2)))))&(((![X1]:((~r1(X2,X1)|~p6(X1)|~p105(X1)))|p6(X2))&(![X1]:((~r1(X2,X1)|p6(X1)|~p105(X1)))|~p6(X2)))|~p105(X2)))&(((![X1]:((~r1(X2,X1)|~p5(X1)|~p104(X1)))|p5(X2))&(![X1]:((~r1(X2,X1)|p5(X1)|~p104(X1)))|~p5(X2)))|~p104(X2)))&(((![X1]:((~r1(X2,X1)|~p4(X1)|~p103(X1)))|p4(X2))&(![X1]:((~r1(X2,X1)|p4(X1)|~p103(X1)))|~p4(X2)))|~p103(X2)))&(((![X1]:((~r1(X2,X1)|~p3(X1)|~p102(X1)))|p3(X2))&(![X1]:((~r1(X2,X1)|p3(X1)|~p102(X1)))|~p3(X2)))|~p102(X2)))&(((![X1]:((~r1(X2,X1)|~p2(X1)|~p101(X1)))|p2(X2))&(![X1]:((~r1(X2,X1)|p2(X1)|~p101(X1)))|~p2(X2)))|~p101(X2)))&(((![X1]:((~r1(X2,X1)|~p1(X1)|~p100(X1)))|p1(X2))&(![X1]:((~r1(X2,X1)|p1(X1)|~p100(X1)))|~p1(X2)))|~p100(X2)))&(p105(X2)|~p106(X2)))&(p104(X2)|~p105(X2)))&(p103(X2)|~p104(X2)))&(p102(X2)|~p103(X2)))&(p101(X2)|~p102(X2)))&(p100(X2)|~p101(X2))))), inference(split_equiv,[status(thm)],[c_0_1])).
% 21.67/3.32 cnf(c_0_9, negated_conjecture, (epred1_1(X5)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_10, negated_conjecture, (r1(esk1_0,esk11_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_5, c_0_6])]), c_0_7])).
% 21.67/3.32 fof(c_0_11, plain, ![X46, X57, X58, X59, X60, X61, X62, X63, X64, X65, X66, X67, X68]:((((((((((((((((((((r1(X46,esk12_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46))&(((~p6(esk12_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46))&(~p106(esk12_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46)))&(p105(esk12_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46))))&((r1(X46,esk13_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46))&(((p6(esk13_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46))&(~p106(esk13_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46)))&(p105(esk13_1(X46))|(p105(X46)|~p104(X46))|~epred1_1(X46)))))&(((r1(X46,esk14_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))&(((~p5(esk14_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))&(~p105(esk14_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46)))&(p104(esk14_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))))&((r1(X46,esk15_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))&(((p5(esk15_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))&(~p105(esk15_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46)))&(p104(esk15_1(X46))|(p104(X46)|~p103(X46))|~epred1_1(X46))))))&(((r1(X46,esk16_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))&(((~p4(esk16_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))&(~p104(esk16_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46)))&(p103(esk16_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))))&((r1(X46,esk17_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))&(((p4(esk17_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))&(~p104(esk17_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46)))&(p103(esk17_1(X46))|(p103(X46)|~p102(X46))|~epred1_1(X46))))))&(((r1(X46,esk18_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))&(((~p3(esk18_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))&(~p103(esk18_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46)))&(p102(esk18_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))))&((r1(X46,esk19_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))&(((p3(esk19_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))&(~p103(esk19_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46)))&(p102(esk19_1(X46))|(p102(X46)|~p101(X46))|~epred1_1(X46))))))&(((r1(X46,esk20_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))&(((~p2(esk20_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))&(~p102(esk20_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46)))&(p101(esk20_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))))&((r1(X46,esk21_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))&(((p2(esk21_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))&(~p102(esk21_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46)))&(p101(esk21_1(X46))|(p101(X46)|~p100(X46))|~epred1_1(X46))))))&((~r1(X46,X57)|~p6(X57)|~p105(X57)|p6(X46)|~p105(X46)|~epred1_1(X46))&(~r1(X46,X58)|p6(X58)|~p105(X58)|~p6(X46)|~p105(X46)|~epred1_1(X46))))&((~r1(X46,X59)|~p5(X59)|~p104(X59)|p5(X46)|~p104(X46)|~epred1_1(X46))&(~r1(X46,X60)|p5(X60)|~p104(X60)|~p5(X46)|~p104(X46)|~epred1_1(X46))))&((~r1(X46,X61)|~p4(X61)|~p103(X61)|p4(X46)|~p103(X46)|~epred1_1(X46))&(~r1(X46,X62)|p4(X62)|~p103(X62)|~p4(X46)|~p103(X46)|~epred1_1(X46))))&((~r1(X46,X63)|~p3(X63)|~p102(X63)|p3(X46)|~p102(X46)|~epred1_1(X46))&(~r1(X46,X64)|p3(X64)|~p102(X64)|~p3(X46)|~p102(X46)|~epred1_1(X46))))&((~r1(X46,X65)|~p2(X65)|~p101(X65)|p2(X46)|~p101(X46)|~epred1_1(X46))&(~r1(X46,X66)|p2(X66)|~p101(X66)|~p2(X46)|~p101(X46)|~epred1_1(X46))))&((~r1(X46,X67)|~p1(X67)|~p100(X67)|p1(X46)|~p100(X46)|~epred1_1(X46))&(~r1(X46,X68)|p1(X68)|~p100(X68)|~p1(X46)|~p100(X46)|~epred1_1(X46))))&(p105(X46)|~p106(X46)|~epred1_1(X46)))&(p104(X46)|~p105(X46)|~epred1_1(X46)))&(p103(X46)|~p104(X46)|~epred1_1(X46)))&(p102(X46)|~p103(X46)|~epred1_1(X46)))&(p101(X46)|~p102(X46)|~epred1_1(X46)))&(p100(X46)|~p101(X46)|~epred1_1(X46)))), 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_8])])])])])])).
% 21.67/3.32 cnf(c_0_12, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_13, negated_conjecture, (p101(esk11_0)|p101(esk1_0)|~p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_14, negated_conjecture, (p101(esk1_0)|~p102(esk11_0)|~p100(esk1_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 fof(c_0_15, plain, ![X1]:((epred2_1(X1)=>((((((((((((((((((~(![X2]:((~r1(X1,X2)|~(((~p6(X2)&~p106(X2))&p105(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p6(X2)&~p106(X2))&p105(X2)))))))|~((~p105(X1)&p104(X1))))&((~(![X2]:((~r1(X1,X2)|~(((~p5(X2)&~p105(X2))&p104(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p5(X2)&~p105(X2))&p104(X2)))))))|~((~p104(X1)&p103(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p4(X2)&~p104(X2))&p103(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p4(X2)&~p104(X2))&p103(X2)))))))|~((~p103(X1)&p102(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p3(X2)&~p103(X2))&p102(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p3(X2)&~p103(X2))&p102(X2)))))))|~((~p102(X1)&p101(X1)))))&((~(![X2]:((~r1(X1,X2)|~(((~p2(X2)&~p102(X2))&p101(X2))))))&~(![X2]:((~r1(X1,X2)|~(((p2(X2)&~p102(X2))&p101(X2)))))))|~((~p101(X1)&p100(X1)))))&(((![X2]:((~r1(X1,X2)|~p6(X2)|~p105(X2)))|p6(X1))&(![X2]:((~r1(X1,X2)|p6(X2)|~p105(X2)))|~p6(X1)))|~p105(X1)))&(((![X2]:((~r1(X1,X2)|~p5(X2)|~p104(X2)))|p5(X1))&(![X2]:((~r1(X1,X2)|p5(X2)|~p104(X2)))|~p5(X1)))|~p104(X1)))&(((![X2]:((~r1(X1,X2)|~p4(X2)|~p103(X2)))|p4(X1))&(![X2]:((~r1(X1,X2)|p4(X2)|~p103(X2)))|~p4(X1)))|~p103(X1)))&(((![X2]:((~r1(X1,X2)|~p3(X2)|~p102(X2)))|p3(X1))&(![X2]:((~r1(X1,X2)|p3(X2)|~p102(X2)))|~p3(X1)))|~p102(X1)))&(((![X2]:((~r1(X1,X2)|~p2(X2)|~p101(X2)))|p2(X1))&(![X2]:((~r1(X1,X2)|p2(X2)|~p101(X2)))|~p2(X1)))|~p101(X1)))&(((![X2]:((~r1(X1,X2)|~p1(X2)|~p100(X2)))|p1(X1))&(![X2]:((~r1(X1,X2)|p1(X2)|~p100(X2)))|~p1(X1)))|~p100(X1)))&(p105(X1)|~p106(X1)))&(p104(X1)|~p105(X1)))&(p103(X1)|~p104(X1)))&(p102(X1)|~p103(X1)))&(p101(X1)|~p102(X1)))&(p100(X1)|~p101(X1))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 21.67/3.32 cnf(c_0_16, negated_conjecture, (epred2_1(X2)|~r1(esk1_0,X1)|~r1(X1,X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_17, negated_conjecture, (epred1_1(X3)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_18, negated_conjecture, (epred2_1(X4)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_19, negated_conjecture, (epred1_1(X1)|~r1(esk11_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 21.67/3.32 cnf(c_0_20, plain, (r1(X1,esk18_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_21, negated_conjecture, (epred1_1(esk11_0)), inference(spm,[status(thm)],[c_0_12, c_0_10])).
% 21.67/3.32 cnf(c_0_22, negated_conjecture, (p101(esk11_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_6])]), c_0_7])).
% 21.67/3.32 cnf(c_0_23, negated_conjecture, (~p102(esk11_0)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_6])]), c_0_7])).
% 21.67/3.32 fof(c_0_24, plain, ![X69, X80, X81, X82, X83, X84, X85, X86, X87, X88, X89, X90, X91]:((((((((((((((((((((r1(X69,esk22_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69))&(((~p6(esk22_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69))&(~p106(esk22_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69)))&(p105(esk22_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69))))&((r1(X69,esk23_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69))&(((p6(esk23_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69))&(~p106(esk23_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69)))&(p105(esk23_1(X69))|(p105(X69)|~p104(X69))|~epred2_1(X69)))))&(((r1(X69,esk24_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))&(((~p5(esk24_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))&(~p105(esk24_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69)))&(p104(esk24_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))))&((r1(X69,esk25_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))&(((p5(esk25_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))&(~p105(esk25_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69)))&(p104(esk25_1(X69))|(p104(X69)|~p103(X69))|~epred2_1(X69))))))&(((r1(X69,esk26_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))&(((~p4(esk26_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))&(~p104(esk26_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69)))&(p103(esk26_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))))&((r1(X69,esk27_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))&(((p4(esk27_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))&(~p104(esk27_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69)))&(p103(esk27_1(X69))|(p103(X69)|~p102(X69))|~epred2_1(X69))))))&(((r1(X69,esk28_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))&(((~p3(esk28_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))&(~p103(esk28_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69)))&(p102(esk28_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))))&((r1(X69,esk29_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))&(((p3(esk29_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))&(~p103(esk29_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69)))&(p102(esk29_1(X69))|(p102(X69)|~p101(X69))|~epred2_1(X69))))))&(((r1(X69,esk30_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))&(((~p2(esk30_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))&(~p102(esk30_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69)))&(p101(esk30_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))))&((r1(X69,esk31_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))&(((p2(esk31_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))&(~p102(esk31_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69)))&(p101(esk31_1(X69))|(p101(X69)|~p100(X69))|~epred2_1(X69))))))&((~r1(X69,X80)|~p6(X80)|~p105(X80)|p6(X69)|~p105(X69)|~epred2_1(X69))&(~r1(X69,X81)|p6(X81)|~p105(X81)|~p6(X69)|~p105(X69)|~epred2_1(X69))))&((~r1(X69,X82)|~p5(X82)|~p104(X82)|p5(X69)|~p104(X69)|~epred2_1(X69))&(~r1(X69,X83)|p5(X83)|~p104(X83)|~p5(X69)|~p104(X69)|~epred2_1(X69))))&((~r1(X69,X84)|~p4(X84)|~p103(X84)|p4(X69)|~p103(X69)|~epred2_1(X69))&(~r1(X69,X85)|p4(X85)|~p103(X85)|~p4(X69)|~p103(X69)|~epred2_1(X69))))&((~r1(X69,X86)|~p3(X86)|~p102(X86)|p3(X69)|~p102(X69)|~epred2_1(X69))&(~r1(X69,X87)|p3(X87)|~p102(X87)|~p3(X69)|~p102(X69)|~epred2_1(X69))))&((~r1(X69,X88)|~p2(X88)|~p101(X88)|p2(X69)|~p101(X69)|~epred2_1(X69))&(~r1(X69,X89)|p2(X89)|~p101(X89)|~p2(X69)|~p101(X69)|~epred2_1(X69))))&((~r1(X69,X90)|~p1(X90)|~p100(X90)|p1(X69)|~p100(X69)|~epred2_1(X69))&(~r1(X69,X91)|p1(X91)|~p100(X91)|~p1(X69)|~p100(X69)|~epred2_1(X69))))&(p105(X69)|~p106(X69)|~epred2_1(X69)))&(p104(X69)|~p105(X69)|~epred2_1(X69)))&(p103(X69)|~p104(X69)|~epred2_1(X69)))&(p102(X69)|~p103(X69)|~epred2_1(X69)))&(p101(X69)|~p102(X69)|~epred2_1(X69)))&(p100(X69)|~p101(X69)|~epred2_1(X69)))), 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_15])])])])])])).
% 21.67/3.32 cnf(c_0_25, negated_conjecture, (epred2_1(X1)|~r1(esk11_0,X1)), inference(spm,[status(thm)],[c_0_16, c_0_10])).
% 21.67/3.32 cnf(c_0_26, negated_conjecture, (epred1_1(X1)|~r1(esk11_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_17, c_0_10])).
% 21.67/3.32 cnf(c_0_27, negated_conjecture, (epred2_1(X1)|~r1(esk11_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_18, c_0_10])).
% 21.67/3.32 cnf(c_0_28, plain, (epred1_1(X1)|~r1(esk18_1(esk11_0),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_19, c_0_20]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_29, plain, (r1(X1,esk27_1(X1))|p103(X1)|~p102(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_30, plain, (epred2_1(esk18_1(esk11_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_20]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_31, plain, (epred1_1(X1)|~r1(esk18_1(esk11_0),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_20]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_32, plain, (epred2_1(X1)|~r1(esk18_1(esk11_0),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_20]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_33, plain, (p101(X1)|~p102(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_34, plain, (epred1_1(X1)|p103(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))|~r1(esk27_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_30])])).
% 21.67/3.32 cnf(c_0_35, plain, (p102(esk18_1(X1))|p102(X1)|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_36, plain, (epred1_1(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_29]), c_0_30])])).
% 21.67/3.32 cnf(c_0_37, plain, (epred2_1(X1)|p103(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))|~r1(esk27_1(esk18_1(esk11_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_29]), c_0_30])])).
% 21.67/3.32 cnf(c_0_38, plain, (p101(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))), inference(spm,[status(thm)],[c_0_33, c_0_30])).
% 21.67/3.32 cnf(c_0_39, plain, (epred1_1(X1)|p103(esk18_1(esk11_0))|~r1(esk27_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_40, plain, (r1(X1,esk15_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_41, plain, (epred1_1(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_42, plain, (epred2_1(X1)|p103(esk18_1(esk11_0))|~r1(esk27_1(esk18_1(esk11_0)),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_43, plain, (r1(X1,esk28_1(X1))|p102(X1)|~p101(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_44, plain, (p101(esk18_1(esk11_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_45, plain, (epred1_1(X1)|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p103(esk27_1(esk18_1(esk11_0)))|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_41])).
% 21.67/3.32 cnf(c_0_46, plain, (p103(esk27_1(X1))|p103(X1)|~p102(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_47, plain, (epred2_1(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p103(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_40]), c_0_41])).
% 21.67/3.32 cnf(c_0_48, plain, (p101(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_49, plain, (epred1_1(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_43]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_50, plain, (epred1_1(X1)|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p102(esk18_1(esk11_0))|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_51, plain, (epred2_1(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_52, negated_conjecture, (p3(X5)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 21.67/3.32 cnf(c_0_53, plain, (p102(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_54, plain, (epred1_1(X1)|p102(esk18_1(esk11_0))|~r1(esk28_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_43]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_55, plain, (r1(X1,esk17_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_56, plain, (epred2_1(X1)|p102(esk18_1(esk11_0))|~r1(esk28_1(esk18_1(esk11_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_43]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_57, plain, (p101(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|~p102(esk28_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_48, c_0_49])).
% 21.67/3.32 cnf(c_0_58, plain, (p102(esk28_1(X1))|p102(X1)|~p101(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_59, plain, (epred1_1(X1)|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_60, plain, (r1(X1,esk23_1(X1))|p105(X1)|~p104(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_61, plain, (epred2_1(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_62, negated_conjecture, (p3(X1)|~r1(esk11_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_52, c_0_10])).
% 21.67/3.32 cnf(c_0_63, plain, (p102(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~p103(esk27_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_53, c_0_41])).
% 21.67/3.32 cnf(c_0_64, plain, (epred1_1(X1)|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|~p102(esk28_1(esk18_1(esk11_0)))|~r1(esk17_1(esk28_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_49])).
% 21.67/3.32 cnf(c_0_65, plain, (epred2_1(esk17_1(esk28_1(esk18_1(esk11_0))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|~p102(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_55]), c_0_49])).
% 21.67/3.32 cnf(c_0_66, plain, (p101(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_67, plain, (epred1_1(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p104(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_60]), c_0_61])).
% 21.67/3.32 cnf(c_0_68, plain, (p104(esk15_1(X1))|p104(X1)|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_69, plain, (p3(X1)|~r1(esk18_1(esk11_0),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_20]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_70, plain, (p103(X1)|~p104(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_71, plain, (p102(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_72, plain, (epred1_1(X1)|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|~r1(esk17_1(esk28_1(esk18_1(esk11_0))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_73, plain, (r1(X1,esk25_1(X1))|p104(X1)|~p103(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_74, plain, (epred2_1(esk17_1(esk28_1(esk18_1(esk11_0))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_75, plain, (epred2_1(esk18_1(esk28_1(esk18_1(esk11_0))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_20]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_76, plain, (epred1_1(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p103(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_41])).
% 21.67/3.32 cnf(c_0_77, plain, (p103(esk18_1(esk11_0))|p3(X1)|~p102(esk18_1(esk11_0))|~r1(esk27_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_29]), c_0_30])])).
% 21.67/3.32 cnf(c_0_78, plain, (p103(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p104(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_70, c_0_61])).
% 21.67/3.32 cnf(c_0_79, plain, (p102(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_80, plain, (epred1_1(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p103(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_74])).
% 21.67/3.32 cnf(c_0_81, plain, (p103(esk17_1(X1))|p103(X1)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_82, plain, (p102(X1)|~p103(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_83, plain, (p102(esk18_1(esk11_0))|p3(X1)|~r1(esk28_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_43]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_84, plain, (p101(esk18_1(esk28_1(esk18_1(esk11_0))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|~p102(esk18_1(esk28_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_33, c_0_75])).
% 21.67/3.32 cnf(c_0_85, plain, (p104(X1)|~p105(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_86, plain, (p105(esk23_1(X1))|p105(X1)|~p104(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_87, plain, (epred1_1(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_88, plain, (p103(esk18_1(esk11_0))|p3(X1)|~r1(esk27_1(esk18_1(esk11_0)),X2)|~r1(X2,X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_89, plain, (p103(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p103(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_68]), c_0_41])).
% 21.67/3.32 cnf(c_0_90, plain, (epred1_1(X1)|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~r1(esk17_1(esk27_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_55]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_91, plain, (epred2_1(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_55]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_92, plain, (epred1_1(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p102(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_81]), c_0_49])).
% 21.67/3.32 cnf(c_0_93, plain, (p102(esk17_1(esk28_1(esk18_1(esk11_0))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|~p103(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_82, c_0_74])).
% 21.67/3.32 cnf(c_0_94, plain, (p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p3(X1)|~r1(esk18_1(esk28_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_20]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_95, plain, (p101(esk18_1(esk28_1(esk18_1(esk11_0))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_35]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_96, plain, (p104(esk23_1(X1))|p105(X1)|~epred2_1(X1)|~epred1_1(esk23_1(X1))|~p104(X1)), inference(spm,[status(thm)],[c_0_85, c_0_86])).
% 21.67/3.32 cnf(c_0_97, plain, (epred1_1(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_98, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(X1)|~p103(esk27_1(esk18_1(esk11_0)))|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_40]), c_0_41])).
% 21.67/3.32 cnf(c_0_99, plain, (p103(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_100, plain, (epred1_1(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|~p103(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_73]), c_0_91])).
% 21.67/3.32 cnf(c_0_101, plain, (p102(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~p103(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_82, c_0_91])).
% 21.67/3.32 cnf(c_0_102, plain, (p103(X1)|~p104(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_103, plain, (epred1_1(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_104, plain, (p102(esk17_1(esk28_1(esk18_1(esk11_0))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|~p102(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_81]), c_0_49])).
% 21.67/3.32 cnf(c_0_105, plain, (p102(X1)|~p3(esk28_1(X1))|~p101(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_106, plain, (p102(esk18_1(esk28_1(esk18_1(esk11_0))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p3(esk28_1(esk18_1(esk28_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_43]), c_0_95]), c_0_75])).
% 21.67/3.32 cnf(c_0_107, plain, (p103(esk18_1(esk11_0))|p104(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p104(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_61])).
% 21.67/3.32 cnf(c_0_108, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(X1)|~p102(esk18_1(esk11_0))|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_109, plain, (p103(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_110, plain, (epred1_1(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_81]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_111, plain, (p102(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_81]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_112, plain, (p102(esk18_1(esk11_0))|p103(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p104(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_102, c_0_103])).
% 21.67/3.32 cnf(c_0_113, plain, (p104(esk25_1(X1))|p104(X1)|~p103(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_114, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p3(X1)|~p102(esk28_1(esk18_1(esk11_0)))|~r1(esk17_1(esk28_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_55]), c_0_49])).
% 21.67/3.32 cnf(c_0_115, plain, (p102(esk17_1(esk28_1(esk18_1(esk11_0))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_116, plain, (epred1_1(X1)|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|~r1(esk18_1(esk28_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_20]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_117, plain, (p102(esk18_1(esk28_1(esk18_1(esk11_0))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_106]), c_0_95]), c_0_75])).
% 21.67/3.32 cnf(c_0_118, plain, (p103(esk18_1(esk11_0))|p104(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p103(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_68]), c_0_41])).
% 21.67/3.32 cnf(c_0_119, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(X1)|~r1(esk15_1(esk27_1(esk18_1(esk11_0))),X1)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_120, plain, (epred1_1(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_73]), c_0_109]), c_0_61])).
% 21.67/3.32 cnf(c_0_121, plain, (p103(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|~p104(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_102, c_0_110])).
% 21.67/3.32 cnf(c_0_122, plain, (epred1_1(esk27_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_29]), c_0_111]), c_0_91])).
% 21.67/3.32 cnf(c_0_123, plain, (p102(esk18_1(esk11_0))|p103(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p103(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_113]), c_0_74])).
% 21.67/3.32 cnf(c_0_124, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p3(X1)|~r1(esk17_1(esk28_1(esk18_1(esk11_0))),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_114, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_125, plain, (epred1_1(esk27_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk17_1(esk28_1(esk18_1(esk11_0))))|p103(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_29]), c_0_115]), c_0_74])).
% 21.67/3.32 cnf(c_0_126, plain, (epred1_1(esk27_1(esk18_1(esk28_1(esk18_1(esk11_0)))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_29]), c_0_117]), c_0_75])).
% 21.67/3.32 cnf(c_0_127, plain, (p3(X1)|~r1(X1,X2)|~p3(X2)|~p102(X2)|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_128, plain, (p102(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|~p103(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_82, c_0_61])).
% 21.67/3.32 cnf(c_0_129, plain, (p103(esk18_1(esk11_0))|p104(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_118, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_130, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|~p104(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_60]), c_0_61])).
% 21.67/3.32 cnf(c_0_131, plain, (p103(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))|~p104(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_102, c_0_120])).
% 21.67/3.32 cnf(c_0_132, plain, (p103(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|~p103(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_113]), c_0_91])).
% 21.67/3.32 cnf(c_0_133, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p3(X1)|~r1(esk17_1(esk27_1(esk18_1(esk11_0))),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_55]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_134, plain, (p3(X1)|~r1(X1,X2)|~p3(X2)|~p102(X2)|~p102(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_135, plain, (p102(esk27_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|~p103(esk27_1(esk17_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_122])).
% 21.67/3.32 cnf(c_0_136, plain, (p102(esk18_1(esk11_0))|p103(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p102(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_81]), c_0_49])).
% 21.67/3.32 cnf(c_0_137, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|p3(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|~p103(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_73]), c_0_74])).
% 21.67/3.32 cnf(c_0_138, plain, (p102(esk27_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk17_1(esk28_1(esk18_1(esk11_0))))|p103(esk28_1(esk18_1(esk11_0)))|~p103(esk27_1(esk17_1(esk28_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_125])).
% 21.67/3.32 cnf(c_0_139, plain, (p102(esk27_1(esk18_1(esk28_1(esk18_1(esk11_0)))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))|~p103(esk27_1(esk18_1(esk28_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_126])).
% 21.67/3.32 cnf(c_0_140, plain, (p104(X1)|p3(X1)|~epred1_1(X1)|~p102(esk15_1(X1))|~p103(X1)|~p3(esk15_1(X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_40]), c_0_53])).
% 21.67/3.32 cnf(c_0_141, plain, (p102(esk15_1(esk27_1(esk18_1(esk11_0))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_128, c_0_109])).
% 21.67/3.32 cnf(c_0_142, plain, (p103(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p104(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_102, c_0_97])).
% 21.67/3.32 cnf(c_0_143, plain, (p103(esk18_1(esk11_0))|p104(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_144, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|~p103(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_68]), c_0_41])).
% 21.67/3.32 cnf(c_0_145, plain, (p102(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))|~p103(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_120])).
% 21.67/3.32 cnf(c_0_146, plain, (p103(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_131, c_0_113]), c_0_109]), c_0_61])).
% 21.67/3.32 cnf(c_0_147, plain, (p102(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|~p103(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_110])).
% 21.67/3.32 cnf(c_0_148, plain, (p103(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_81]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_149, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|p3(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|~p103(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_133, c_0_73]), c_0_91])).
% 21.67/3.32 cnf(c_0_150, plain, (p103(X1)|p3(X1)|~epred2_1(X1)|~p102(esk27_1(X1))|~p102(X1)|~p3(esk27_1(X1))), inference(spm,[status(thm)],[c_0_134, c_0_29])).
% 21.67/3.32 cnf(c_0_151, plain, (p102(esk27_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_46]), c_0_111]), c_0_91])).
% 21.67/3.32 cnf(c_0_152, plain, (p103(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p3(esk27_1(esk17_1(esk27_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_133, c_0_29]), c_0_111]), c_0_91])).
% 21.67/3.32 cnf(c_0_153, plain, (p103(X1)|p3(X1)|~epred1_1(X1)|~p102(esk17_1(X1))|~p102(X1)|~p3(esk17_1(X1))), inference(spm,[status(thm)],[c_0_127, c_0_55])).
% 21.67/3.32 cnf(c_0_154, plain, (p102(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|~p103(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_103])).
% 21.67/3.32 cnf(c_0_155, plain, (p102(esk18_1(esk11_0))|p103(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_136, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_156, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|p3(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|~p102(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_137, c_0_81]), c_0_49])).
% 21.67/3.32 cnf(c_0_157, plain, (p102(esk27_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk17_1(esk28_1(esk18_1(esk11_0))))|p103(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_138, c_0_46]), c_0_115]), c_0_74])).
% 21.67/3.32 cnf(c_0_158, plain, (p102(esk18_1(esk11_0))|p103(esk17_1(esk28_1(esk18_1(esk11_0))))|p103(esk28_1(esk18_1(esk11_0)))|p3(esk27_1(esk17_1(esk28_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_29]), c_0_115]), c_0_74])).
% 21.67/3.32 cnf(c_0_159, plain, (p102(esk27_1(esk18_1(esk28_1(esk18_1(esk11_0)))))|p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_139, c_0_46]), c_0_117]), c_0_75])).
% 21.67/3.32 cnf(c_0_160, plain, (p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))|p3(esk27_1(esk18_1(esk28_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_29]), c_0_117]), c_0_75])).
% 21.67/3.32 cnf(c_0_161, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk27_1(esk18_1(esk11_0)))|~p103(esk27_1(esk18_1(esk11_0)))|~p3(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_140, c_0_141]), c_0_41])).
% 21.67/3.32 cnf(c_0_162, plain, (p102(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|~p103(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(spm,[status(thm)],[c_0_53, c_0_97])).
% 21.67/3.32 cnf(c_0_163, plain, (p103(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_142, c_0_143])).
% 21.67/3.32 cnf(c_0_164, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|~p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_144, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_165, plain, (p104(X1)|p3(X1)|~epred2_1(X1)|~p102(esk25_1(X1))|~p103(X1)|~p3(esk25_1(X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_134, c_0_73]), c_0_82])).
% 21.67/3.32 cnf(c_0_166, plain, (p102(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_145, c_0_146])).
% 21.67/3.32 cnf(c_0_167, plain, (p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk25_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_73]), c_0_109]), c_0_61])).
% 21.67/3.32 cnf(c_0_168, plain, (p102(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_147, c_0_148])).
% 21.67/3.32 cnf(c_0_169, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|p3(esk25_1(esk17_1(esk27_1(esk18_1(esk11_0)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_81]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_170, plain, (p103(esk17_1(esk27_1(esk18_1(esk11_0))))|p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p3(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_151]), c_0_152]), c_0_111]), c_0_91])).
% 21.67/3.32 cnf(c_0_171, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p3(esk28_1(esk18_1(esk11_0)))|~p102(esk28_1(esk18_1(esk11_0)))|~p3(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_153, c_0_115]), c_0_49])).
% 21.67/3.32 cnf(c_0_172, plain, (p102(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))|p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_154, c_0_155])).
% 21.67/3.32 cnf(c_0_173, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|p3(esk25_1(esk17_1(esk28_1(esk18_1(esk11_0)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_156, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_174, plain, (p102(esk18_1(esk11_0))|p103(esk17_1(esk28_1(esk18_1(esk11_0))))|p103(esk28_1(esk18_1(esk11_0)))|p3(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_157]), c_0_158]), c_0_115]), c_0_74])).
% 21.67/3.32 cnf(c_0_175, plain, (p102(X1)|~p3(esk18_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_176, plain, (p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))|p3(esk18_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_159]), c_0_160]), c_0_117]), c_0_75])).
% 21.67/3.32 cnf(c_0_177, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk27_1(esk18_1(esk11_0)))|~p102(esk18_1(esk11_0))|~p3(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_161, c_0_46]), c_0_30])])).
% 21.67/3.32 cnf(c_0_178, plain, (p105(X1)|p3(X1)|~epred2_1(X1)|~p102(esk23_1(X1))|~p102(X1)|~p104(X1)|~p3(esk23_1(X1))), inference(spm,[status(thm)],[c_0_134, c_0_60])).
% 21.67/3.32 cnf(c_0_179, plain, (p102(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))|p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(spm,[status(thm)],[c_0_162, c_0_163])).
% 21.67/3.32 cnf(c_0_180, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk23_1(esk15_1(esk27_1(esk18_1(esk11_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_164, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_181, plain, (p103(esk18_1(esk11_0))|p104(esk15_1(esk27_1(esk18_1(esk11_0))))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_165, c_0_166]), c_0_167]), c_0_109]), c_0_61])).
% 21.67/3.32 cnf(c_0_182, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p3(esk27_1(esk18_1(esk11_0)))|~p3(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_153, c_0_111]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_183, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|p3(esk17_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_165, c_0_168]), c_0_169]), c_0_170]), c_0_91])).
% 21.67/3.32 cnf(c_0_184, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p3(esk28_1(esk18_1(esk11_0)))|~p3(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_171, c_0_58]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_185, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|p3(esk17_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_165, c_0_172]), c_0_173]), c_0_174]), c_0_74])).
% 21.67/3.32 cnf(c_0_186, plain, (p102(X1)|~p103(esk18_1(X1))|~p101(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_187, plain, (p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))|p103(esk18_1(esk28_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_175, c_0_176]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_188, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk27_1(esk18_1(esk11_0)))|~p3(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_189, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk15_1(esk27_1(esk18_1(esk11_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_178, c_0_179]), c_0_180]), c_0_181]), c_0_141]), c_0_61])).
% 21.67/3.32 cnf(c_0_190, plain, (p103(X1)|~p104(esk17_1(X1))|~p102(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_191, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p104(esk17_1(esk27_1(esk18_1(esk11_0))))|p3(esk27_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_182, c_0_183])).
% 21.67/3.32 cnf(c_0_192, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p104(esk17_1(esk28_1(esk18_1(esk11_0))))|p3(esk28_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_184, c_0_185])).
% 21.67/3.32 cnf(c_0_193, plain, (p102(esk28_1(esk18_1(esk11_0)))|p102(esk18_1(esk11_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_186, c_0_187]), c_0_66]), c_0_49])).
% 21.67/3.32 cnf(c_0_194, plain, (p103(esk18_1(esk11_0))|p3(esk18_1(esk11_0))|~p102(esk18_1(esk11_0))|~p3(esk27_1(esk18_1(esk11_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_79]), c_0_30])])).
% 21.67/3.32 cnf(c_0_195, plain, (p104(X1)|~p105(esk15_1(X1))|~p103(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 21.67/3.32 cnf(c_0_196, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p105(esk15_1(esk27_1(esk18_1(esk11_0))))|p3(esk27_1(esk18_1(esk11_0)))), inference(spm,[status(thm)],[c_0_188, c_0_189])).
% 21.67/3.32 cnf(c_0_197, plain, (p103(esk27_1(esk18_1(esk11_0)))|p103(esk18_1(esk11_0))|p3(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_190, c_0_191]), c_0_79]), c_0_41])).
% 21.67/3.32 cnf(c_0_198, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))|p3(esk28_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_190, c_0_192]), c_0_193]), c_0_49])).
% 21.67/3.32 cnf(c_0_199, plain, (p103(esk18_1(esk11_0))|p3(esk18_1(esk11_0))|~p3(esk27_1(esk18_1(esk11_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_194, c_0_35]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_200, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk27_1(esk18_1(esk11_0)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_195, c_0_196]), c_0_197]), c_0_41])).
% 21.67/3.32 cnf(c_0_201, plain, (p102(X1)|~p103(esk28_1(X1))|~p101(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_202, plain, (p102(esk18_1(esk11_0))|p103(esk28_1(esk18_1(esk11_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_198]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_203, plain, (p103(X1)|~p104(esk27_1(X1))|~p102(X1)|~epred2_1(X1)), inference(split_conjunct,[status(thm)],[c_0_24])).
% 21.67/3.32 cnf(c_0_204, plain, (p103(esk18_1(esk11_0))|p104(esk27_1(esk18_1(esk11_0)))|p3(esk18_1(esk11_0))), inference(spm,[status(thm)],[c_0_199, c_0_200])).
% 21.67/3.32 cnf(c_0_205, plain, (p102(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_201, c_0_202]), c_0_30]), c_0_44])])).
% 21.67/3.32 cnf(c_0_206, plain, (p103(esk18_1(esk11_0))|p3(esk18_1(esk11_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_203, c_0_204]), c_0_30]), c_0_205])])).
% 21.67/3.32 cnf(c_0_207, plain, (p103(esk18_1(esk11_0))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_175, c_0_206]), c_0_21]), c_0_22])]), c_0_23])).
% 21.67/3.32 cnf(c_0_208, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_186, c_0_207]), c_0_21]), c_0_22])]), c_0_23]), ['proof']).
% 21.67/3.32 % SZS output end Proof
% 21.67/3.32 % User time : 2.682 s
% 21.67/3.32 % System time : 0.013 s
% 21.67/3.32 % Total time : 2.695 s
% 21.67/3.32 % User time : 2.685 s
% 21.67/3.32 % System time : 0.018 s
% 21.67/3.32 % Total time : 2.702 s
% 21.67/3.32
%------------------------------------------------------------------------------