%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL652+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n012.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:20 AM UTC 2026
% Result : Theorem 165.87s 21.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL652+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.01 % Command : java -jar mcs_scs.jar %d %s
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Fri Sep 4 19:53:57 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.08/0.35 start to proof:theBenchmark.p
% 165.87/21.35 % Version : CSI_E---1.1
% 165.87/21.35 % Problem : theBenchmark.p
% 165.87/21.35 % Proof found!
% 165.87/21.35 % SZS status Theorem for theBenchmark.p
% 165.87/21.35 % SZS output start Proof
% 165.87/21.35 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|~(p4(X2)))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1))))))))|~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1)))))))&p2(X2))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1))))))))))))))))|(~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p2(X2)))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1)))))))))))))))|(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p2(X1)))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1)))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 165.87/21.35 fof(c_0_1, plain, ![X1]:((epred3_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 165.87/21.35 fof(c_0_2, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|~p4(X2))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred3_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p2(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1])).
% 165.87/21.35 fof(c_0_3, plain, ![X1]:((epred2_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 165.87/21.35 fof(c_0_4, negated_conjecture, ![X4, X5, X6, X7, X10, X11, X12, X13, X14, X17, X18, X19, X20, X21, X23, X24, X25, X29, X34, X39, X44, X49, X54, X59, X64, X69, X74, X77, X79, X80, X81, X83, X84, X85, X87, X88, X89, X91, X92, X93, X95, X96, X97, X99, X100, X101, X103, X104, X105, X107, X108, X109, X111, X112, X113, X115, X116, X117]:((((((((~r1(esk1_0,X4)|~p4(X4))&(((r1(X5,esk3_1(X5))|(r1(X7,esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5))&(~r1(esk3_1(X5),X10)|~p1(X10)|(r1(X7,esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5)))&((r1(X5,esk3_1(X5))|(p1(esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5))&(~r1(esk3_1(X5),X10)|~p1(X10)|(p1(esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5)))))&(((((r1(X12,esk5_2(X11,X12))|(r1(X14,esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))&(~r1(esk5_2(X11,X12),X17)|~p1(X17)|(r1(X14,esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11)))&((r1(X12,esk5_2(X11,X12))|(p1(esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))&(~r1(esk5_2(X11,X12),X17)|~p1(X17)|(p1(esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))))&(~r1(X11,X18)|epred3_1(X18)|~r1(esk1_0,X11)))&((r1(X19,esk6_2(X11,X19))|(~r1(X19,X20)|(~r1(X20,X21)|p1(X21)))|~r1(X11,X19)|~r1(esk1_0,X11))&(~p1(esk6_2(X11,X19))|(~r1(X19,X20)|(~r1(X20,X21)|p1(X21)))|~r1(X11,X19)|~r1(esk1_0,X11)))))&((r1(X23,esk7_1(X23))|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25)))|~r1(esk1_0,X23))&(~p1(esk7_1(X23))|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25)))|~r1(esk1_0,X23))))&((r1(esk1_0,esk8_0)&(r1(esk8_0,esk9_0)&(~r1(esk9_0,X29)|p1(X29))))&(r1(esk8_0,esk10_0)&~p1(esk10_0))))&(((r1(esk1_0,esk11_0)&((r1(esk11_0,esk12_0)&(r1(esk12_0,esk13_0)&(~r1(esk13_0,X34)|p1(X34))))&(r1(esk12_0,esk14_0)&~p1(esk14_0))))&(((r1(esk11_0,esk15_0)&((r1(esk15_0,esk16_0)&(r1(esk16_0,esk17_0)&(~r1(esk17_0,X39)|p1(X39))))&(r1(esk16_0,esk18_0)&~p1(esk18_0))))&(((r1(esk15_0,esk19_0)&((r1(esk19_0,esk20_0)&(r1(esk20_0,esk21_0)&(~r1(esk21_0,X44)|p1(X44))))&(r1(esk20_0,esk22_0)&~p1(esk22_0))))&(((r1(esk19_0,esk23_0)&((r1(esk23_0,esk24_0)&(r1(esk24_0,esk25_0)&(~r1(esk25_0,X49)|p1(X49))))&(r1(esk24_0,esk26_0)&~p1(esk26_0))))&(((r1(esk23_0,esk27_0)&((r1(esk27_0,esk28_0)&(r1(esk28_0,esk29_0)&(~r1(esk29_0,X54)|p1(X54))))&(r1(esk28_0,esk30_0)&~p1(esk30_0))))&(((r1(esk27_0,esk31_0)&((r1(esk31_0,esk32_0)&(r1(esk32_0,esk33_0)&(~r1(esk33_0,X59)|p1(X59))))&(r1(esk32_0,esk34_0)&~p1(esk34_0))))&(((r1(esk31_0,esk35_0)&((r1(esk35_0,esk36_0)&(r1(esk36_0,esk37_0)&(~r1(esk37_0,X64)|p1(X64))))&(r1(esk36_0,esk38_0)&~p1(esk38_0))))&(((r1(esk35_0,esk39_0)&((r1(esk39_0,esk40_0)&(r1(esk40_0,esk41_0)&(~r1(esk41_0,X69)|p1(X69))))&(r1(esk40_0,esk42_0)&~p1(esk42_0))))&(((r1(esk39_0,esk43_0)&((r1(esk43_0,esk44_0)&(r1(esk44_0,esk45_0)&(~r1(esk45_0,X74)|p1(X74))))&(r1(esk44_0,esk46_0)&~p1(esk46_0))))&(r1(esk43_0,esk47_0)&((r1(X77,esk48_1(X77))|~r1(esk47_0,X77))&(~p2(esk48_1(X77))|~r1(esk47_0,X77)))))&((r1(X79,esk49_1(X79))|(~r1(esk43_0,X79)|(~r1(X79,X80)|(~r1(X80,X81)|~p1(X81)))))&(p1(esk49_1(X79))|(~r1(esk43_0,X79)|(~r1(X79,X80)|(~r1(X80,X81)|~p1(X81))))))))&((r1(X83,esk50_1(X83))|(~r1(esk39_0,X83)|(~r1(X83,X84)|(~r1(X84,X85)|~p1(X85)))))&(p1(esk50_1(X83))|(~r1(esk39_0,X83)|(~r1(X83,X84)|(~r1(X84,X85)|~p1(X85))))))))&((r1(X87,esk51_1(X87))|(~r1(esk35_0,X87)|(~r1(X87,X88)|(~r1(X88,X89)|~p1(X89)))))&(p1(esk51_1(X87))|(~r1(esk35_0,X87)|(~r1(X87,X88)|(~r1(X88,X89)|~p1(X89))))))))&((r1(X91,esk52_1(X91))|(~r1(esk31_0,X91)|(~r1(X91,X92)|(~r1(X92,X93)|~p1(X93)))))&(p1(esk52_1(X91))|(~r1(esk31_0,X91)|(~r1(X91,X92)|(~r1(X92,X93)|~p1(X93))))))))&((r1(X95,esk53_1(X95))|(~r1(esk27_0,X95)|(~r1(X95,X96)|(~r1(X96,X97)|~p1(X97)))))&(p1(esk53_1(X95))|(~r1(esk27_0,X95)|(~r1(X95,X96)|(~r1(X96,X97)|~p1(X97))))))))&((r1(X99,esk54_1(X99))|(~r1(esk23_0,X99)|(~r1(X99,X100)|(~r1(X100,X101)|~p1(X101)))))&(p1(esk54_1(X99))|(~r1(esk23_0,X99)|(~r1(X99,X100)|(~r1(X100,X101)|~p1(X101))))))))&((r1(X103,esk55_1(X103))|(~r1(esk19_0,X103)|(~r1(X103,X104)|(~r1(X104,X105)|~p1(X105)))))&(p1(esk55_1(X103))|(~r1(esk19_0,X103)|(~r1(X103,X104)|(~r1(X104,X105)|~p1(X105))))))))&((r1(X107,esk56_1(X107))|(~r1(esk15_0,X107)|(~r1(X107,X108)|(~r1(X108,X109)|~p1(X109)))))&(p1(esk56_1(X107))|(~r1(esk15_0,X107)|(~r1(X107,X108)|(~r1(X108,X109)|~p1(X109))))))))&((r1(X111,esk57_1(X111))|(~r1(esk11_0,X111)|(~r1(X111,X112)|(~r1(X112,X113)|~p1(X113)))))&(p1(esk57_1(X111))|(~r1(esk11_0,X111)|(~r1(X111,X112)|(~r1(X112,X113)|~p1(X113))))))))&((r1(X115,esk58_1(X115))|(~r1(esk1_0,X115)|(~r1(X115,X116)|(~r1(X116,X117)|~p1(X117)))))&(p1(esk58_1(X115))|(~r1(esk1_0,X115)|(~r1(X115,X116)|(~r1(X116,X117)|~p1(X117)))))))), 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_2])])])])])])).
% 165.87/21.35 fof(c_0_5, plain, ![X1]:((epred3_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred2_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1]), c_0_3])).
% 165.87/21.35 cnf(c_0_6, negated_conjecture, (epred3_1(X2)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_7, negated_conjecture, (r1(esk1_0,esk11_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 fof(c_0_8, plain, ![X191, X192, X193, X194, X197, X198, X199, X200, X201, X204, X205, X206, X207, X208, X211, X212, X213, X214, X215, X218, X219, X220, X221, X222, X224, X225, X226, X228, X229, X230, X232, X233, X234]:((((((r1(X192,esk86_2(X191,X192))|(r1(X194,esk85_4(X191,X192,X193,X194))|~r1(X193,X194)|~r1(X192,X193))|~r1(X191,X192)|~epred3_1(X191))&(~r1(esk86_2(X191,X192),X197)|~p1(X197)|(r1(X194,esk85_4(X191,X192,X193,X194))|~r1(X193,X194)|~r1(X192,X193))|~r1(X191,X192)|~epred3_1(X191)))&((r1(X192,esk86_2(X191,X192))|(p1(esk85_4(X191,X192,X193,X194))|~r1(X193,X194)|~r1(X192,X193))|~r1(X191,X192)|~epred3_1(X191))&(~r1(esk86_2(X191,X192),X197)|~p1(X197)|(p1(esk85_4(X191,X192,X193,X194))|~r1(X193,X194)|~r1(X192,X193))|~r1(X191,X192)|~epred3_1(X191))))&(((((r1(X199,esk88_3(X191,X198,X199))|(r1(X201,esk87_5(X191,X198,X199,X200,X201))|~r1(X200,X201)|~r1(X199,X200))|~r1(X198,X199)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk88_3(X191,X198,X199),X204)|~p1(X204)|(r1(X201,esk87_5(X191,X198,X199,X200,X201))|~r1(X200,X201)|~r1(X199,X200))|~r1(X198,X199)|~r1(X191,X198)|~epred3_1(X191)))&((r1(X199,esk88_3(X191,X198,X199))|(p1(esk87_5(X191,X198,X199,X200,X201))|~r1(X200,X201)|~r1(X199,X200))|~r1(X198,X199)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk88_3(X191,X198,X199),X204)|~p1(X204)|(p1(esk87_5(X191,X198,X199,X200,X201))|~r1(X200,X201)|~r1(X199,X200))|~r1(X198,X199)|~r1(X191,X198)|~epred3_1(X191))))&(((((r1(X206,esk90_4(X191,X198,X205,X206))|(r1(X208,esk89_6(X191,X198,X205,X206,X207,X208))|~r1(X207,X208)|~r1(X206,X207))|~r1(X205,X206)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk90_4(X191,X198,X205,X206),X211)|~p1(X211)|(r1(X208,esk89_6(X191,X198,X205,X206,X207,X208))|~r1(X207,X208)|~r1(X206,X207))|~r1(X205,X206)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191)))&((r1(X206,esk90_4(X191,X198,X205,X206))|(p1(esk89_6(X191,X198,X205,X206,X207,X208))|~r1(X207,X208)|~r1(X206,X207))|~r1(X205,X206)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk90_4(X191,X198,X205,X206),X211)|~p1(X211)|(p1(esk89_6(X191,X198,X205,X206,X207,X208))|~r1(X207,X208)|~r1(X206,X207))|~r1(X205,X206)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))))&(((((r1(X213,esk92_5(X191,X198,X205,X212,X213))|(r1(X215,esk91_7(X191,X198,X205,X212,X213,X214,X215))|~r1(X214,X215)|~r1(X213,X214))|~r1(X212,X213)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk92_5(X191,X198,X205,X212,X213),X218)|~p1(X218)|(r1(X215,esk91_7(X191,X198,X205,X212,X213,X214,X215))|~r1(X214,X215)|~r1(X213,X214))|~r1(X212,X213)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191)))&((r1(X213,esk92_5(X191,X198,X205,X212,X213))|(p1(esk91_7(X191,X198,X205,X212,X213,X214,X215))|~r1(X214,X215)|~r1(X213,X214))|~r1(X212,X213)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~r1(esk92_5(X191,X198,X205,X212,X213),X218)|~p1(X218)|(p1(esk91_7(X191,X198,X205,X212,X213,X214,X215))|~r1(X214,X215)|~r1(X213,X214))|~r1(X212,X213)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))))&(~r1(X212,X219)|epred2_1(X219)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191)))&((r1(X220,esk93_5(X191,X198,X205,X212,X220))|(~r1(X220,X221)|(~r1(X221,X222)|p1(X222)))|~r1(X212,X220)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~p1(esk93_5(X191,X198,X205,X212,X220))|(~r1(X220,X221)|(~r1(X221,X222)|p1(X222)))|~r1(X212,X220)|~r1(X205,X212)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191)))))&((r1(X224,esk94_4(X191,X198,X205,X224))|(~r1(X224,X225)|(~r1(X225,X226)|p1(X226)))|~r1(X205,X224)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191))&(~p1(esk94_4(X191,X198,X205,X224))|(~r1(X224,X225)|(~r1(X225,X226)|p1(X226)))|~r1(X205,X224)|~r1(X198,X205)|~r1(X191,X198)|~epred3_1(X191)))))&((r1(X228,esk95_3(X191,X198,X228))|(~r1(X228,X229)|(~r1(X229,X230)|p1(X230)))|~r1(X198,X228)|~r1(X191,X198)|~epred3_1(X191))&(~p1(esk95_3(X191,X198,X228))|(~r1(X228,X229)|(~r1(X229,X230)|p1(X230)))|~r1(X198,X228)|~r1(X191,X198)|~epred3_1(X191)))))&((r1(X232,esk96_2(X191,X232))|(~r1(X232,X233)|(~r1(X233,X234)|p1(X234)))|~r1(X191,X232)|~epred3_1(X191))&(~p1(esk96_2(X191,X232))|(~r1(X232,X233)|(~r1(X233,X234)|p1(X234)))|~r1(X191,X232)|~epred3_1(X191))))), 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_5])])])])])])).
% 165.87/21.35 cnf(c_0_9, negated_conjecture, (epred3_1(X1)|~r1(esk11_0,X1)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 165.87/21.35 cnf(c_0_10, negated_conjecture, (r1(esk11_0,esk15_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 fof(c_0_11, plain, ![X1]:((epred1_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))), introduced(definition)).
% 165.87/21.35 cnf(c_0_12, plain, (epred2_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred3_1(X5)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 165.87/21.35 cnf(c_0_13, negated_conjecture, (r1(esk15_0,esk19_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_14, negated_conjecture, (epred3_1(esk15_0)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 165.87/21.35 fof(c_0_15, plain, ![X1]:((epred2_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred1_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_3]), c_0_11])).
% 165.87/21.35 cnf(c_0_16, negated_conjecture, (epred2_1(X1)|~r1(esk19_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_14])])).
% 165.87/21.35 cnf(c_0_17, negated_conjecture, (r1(esk19_0,esk23_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 fof(c_0_18, plain, ![X146, X147, X148, X149, X152, X153, X154, X155, X156, X159, X160, X161, X162, X163, X166, X167, X168, X169, X170, X173, X174, X175, X176, X177, X179, X180, X181, X183, X184, X185, X187, X188, X189]:((((((r1(X147,esk74_2(X146,X147))|(r1(X149,esk73_4(X146,X147,X148,X149))|~r1(X148,X149)|~r1(X147,X148))|~r1(X146,X147)|~epred2_1(X146))&(~r1(esk74_2(X146,X147),X152)|~p1(X152)|(r1(X149,esk73_4(X146,X147,X148,X149))|~r1(X148,X149)|~r1(X147,X148))|~r1(X146,X147)|~epred2_1(X146)))&((r1(X147,esk74_2(X146,X147))|(p1(esk73_4(X146,X147,X148,X149))|~r1(X148,X149)|~r1(X147,X148))|~r1(X146,X147)|~epred2_1(X146))&(~r1(esk74_2(X146,X147),X152)|~p1(X152)|(p1(esk73_4(X146,X147,X148,X149))|~r1(X148,X149)|~r1(X147,X148))|~r1(X146,X147)|~epred2_1(X146))))&(((((r1(X154,esk76_3(X146,X153,X154))|(r1(X156,esk75_5(X146,X153,X154,X155,X156))|~r1(X155,X156)|~r1(X154,X155))|~r1(X153,X154)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk76_3(X146,X153,X154),X159)|~p1(X159)|(r1(X156,esk75_5(X146,X153,X154,X155,X156))|~r1(X155,X156)|~r1(X154,X155))|~r1(X153,X154)|~r1(X146,X153)|~epred2_1(X146)))&((r1(X154,esk76_3(X146,X153,X154))|(p1(esk75_5(X146,X153,X154,X155,X156))|~r1(X155,X156)|~r1(X154,X155))|~r1(X153,X154)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk76_3(X146,X153,X154),X159)|~p1(X159)|(p1(esk75_5(X146,X153,X154,X155,X156))|~r1(X155,X156)|~r1(X154,X155))|~r1(X153,X154)|~r1(X146,X153)|~epred2_1(X146))))&(((((r1(X161,esk78_4(X146,X153,X160,X161))|(r1(X163,esk77_6(X146,X153,X160,X161,X162,X163))|~r1(X162,X163)|~r1(X161,X162))|~r1(X160,X161)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk78_4(X146,X153,X160,X161),X166)|~p1(X166)|(r1(X163,esk77_6(X146,X153,X160,X161,X162,X163))|~r1(X162,X163)|~r1(X161,X162))|~r1(X160,X161)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146)))&((r1(X161,esk78_4(X146,X153,X160,X161))|(p1(esk77_6(X146,X153,X160,X161,X162,X163))|~r1(X162,X163)|~r1(X161,X162))|~r1(X160,X161)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk78_4(X146,X153,X160,X161),X166)|~p1(X166)|(p1(esk77_6(X146,X153,X160,X161,X162,X163))|~r1(X162,X163)|~r1(X161,X162))|~r1(X160,X161)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))))&(((((r1(X168,esk80_5(X146,X153,X160,X167,X168))|(r1(X170,esk79_7(X146,X153,X160,X167,X168,X169,X170))|~r1(X169,X170)|~r1(X168,X169))|~r1(X167,X168)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk80_5(X146,X153,X160,X167,X168),X173)|~p1(X173)|(r1(X170,esk79_7(X146,X153,X160,X167,X168,X169,X170))|~r1(X169,X170)|~r1(X168,X169))|~r1(X167,X168)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146)))&((r1(X168,esk80_5(X146,X153,X160,X167,X168))|(p1(esk79_7(X146,X153,X160,X167,X168,X169,X170))|~r1(X169,X170)|~r1(X168,X169))|~r1(X167,X168)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~r1(esk80_5(X146,X153,X160,X167,X168),X173)|~p1(X173)|(p1(esk79_7(X146,X153,X160,X167,X168,X169,X170))|~r1(X169,X170)|~r1(X168,X169))|~r1(X167,X168)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))))&(~r1(X167,X174)|epred1_1(X174)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146)))&((r1(X175,esk81_5(X146,X153,X160,X167,X175))|(~r1(X175,X176)|(~r1(X176,X177)|p1(X177)))|~r1(X167,X175)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~p1(esk81_5(X146,X153,X160,X167,X175))|(~r1(X175,X176)|(~r1(X176,X177)|p1(X177)))|~r1(X167,X175)|~r1(X160,X167)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146)))))&((r1(X179,esk82_4(X146,X153,X160,X179))|(~r1(X179,X180)|(~r1(X180,X181)|p1(X181)))|~r1(X160,X179)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146))&(~p1(esk82_4(X146,X153,X160,X179))|(~r1(X179,X180)|(~r1(X180,X181)|p1(X181)))|~r1(X160,X179)|~r1(X153,X160)|~r1(X146,X153)|~epred2_1(X146)))))&((r1(X183,esk83_3(X146,X153,X183))|(~r1(X183,X184)|(~r1(X184,X185)|p1(X185)))|~r1(X153,X183)|~r1(X146,X153)|~epred2_1(X146))&(~p1(esk83_3(X146,X153,X183))|(~r1(X183,X184)|(~r1(X184,X185)|p1(X185)))|~r1(X153,X183)|~r1(X146,X153)|~epred2_1(X146)))))&((r1(X187,esk84_2(X146,X187))|(~r1(X187,X188)|(~r1(X188,X189)|p1(X189)))|~r1(X146,X187)|~epred2_1(X146))&(~p1(esk84_2(X146,X187))|(~r1(X187,X188)|(~r1(X188,X189)|p1(X189)))|~r1(X146,X187)|~epred2_1(X146))))), 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])])])])])])).
% 165.87/21.35 cnf(c_0_19, negated_conjecture, (epred2_1(X1)|~r1(esk23_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 165.87/21.35 cnf(c_0_20, negated_conjecture, (r1(esk23_0,esk27_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_21, plain, (epred1_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred2_1(X5)), inference(split_conjunct,[status(thm)],[c_0_18])).
% 165.87/21.35 cnf(c_0_22, negated_conjecture, (r1(esk31_0,esk35_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_23, negated_conjecture, (epred2_1(X1)|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 165.87/21.35 cnf(c_0_24, negated_conjecture, (r1(esk27_0,esk31_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_25, negated_conjecture, (epred1_1(X1)|~epred2_1(esk31_0)|~r1(esk35_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 165.87/21.35 cnf(c_0_26, negated_conjecture, (epred2_1(esk31_0)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 165.87/21.35 cnf(c_0_27, negated_conjecture, (epred1_1(X1)|~r1(esk35_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 165.87/21.35 cnf(c_0_28, negated_conjecture, (r1(esk35_0,esk39_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 fof(c_0_29, plain, ![X1]:((epred1_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 165.87/21.35 cnf(c_0_30, negated_conjecture, (epred1_1(X1)|~r1(esk39_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 165.87/21.35 cnf(c_0_31, negated_conjecture, (r1(esk39_0,esk43_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 fof(c_0_32, plain, ![X119, X120, X123, X124, X126, X128, X129, X130, X134, X135, X137, X139, X145]:((((((((r1(X120,esk59_2(X119,X120))|~r1(X119,X120)|~epred1_1(X119))&((r1(esk59_2(X119,X120),esk60_2(X119,X120))|~r1(X119,X120)|~epred1_1(X119))&(~p3(esk60_2(X119,X120))|~r1(X119,X120)|~epred1_1(X119))))&(p2(esk59_2(X119,X120))|~r1(X119,X120)|~epred1_1(X119)))&((((r1(X126,esk62_3(X119,X123,X126))|~r1(X123,X126)|(r1(X124,esk61_3(X119,X123,X124))|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119))&(~r1(esk62_3(X119,X123,X126),X128)|~p2(X128)|~r1(X123,X126)|(r1(X124,esk61_3(X119,X123,X124))|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119)))&((r1(X126,esk62_3(X119,X123,X126))|~r1(X123,X126)|(~p3(esk61_3(X119,X123,X124))|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119))&(~r1(esk62_3(X119,X123,X126),X128)|~p2(X128)|~r1(X123,X126)|(~p3(esk61_3(X119,X123,X124))|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119))))&((r1(X126,esk62_3(X119,X123,X126))|~r1(X123,X126)|(p2(X124)|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119))&(~r1(esk62_3(X119,X123,X126),X128)|~p2(X128)|~r1(X123,X126)|(p2(X124)|~r1(X123,X124)|~p2(X123))|~r1(X119,X123)|~epred1_1(X119)))))&((((r1(X119,esk65_1(X119))|(r1(X130,esk63_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119))&(~r1(esk65_1(X119),X134)|~p2(X134)|(r1(X130,esk63_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119)))&(((r1(X119,esk65_1(X119))|(r1(esk63_3(X119,X129,X130),esk64_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119))&(~r1(esk65_1(X119),X134)|~p2(X134)|(r1(esk63_3(X119,X129,X130),esk64_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119)))&((r1(X119,esk65_1(X119))|(~p3(esk64_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119))&(~r1(esk65_1(X119),X134)|~p2(X134)|(~p3(esk64_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119)))))&((r1(X119,esk65_1(X119))|(p2(esk63_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119))&(~r1(esk65_1(X119),X134)|~p2(X134)|(p2(esk63_3(X119,X129,X130))|~r1(X129,X130)|~r1(X119,X129))|~epred1_1(X119)))))&(((r1(X135,esk67_2(X119,X135))|r1(X135,esk66_2(X119,X135))|~r1(X119,X135)|~epred1_1(X119))&(((r1(X139,esk68_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|r1(X135,esk66_2(X119,X135))|~r1(X119,X135)|~epred1_1(X119))&((r1(esk68_3(X119,X135,X139),esk69_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|r1(X135,esk66_2(X119,X135))|~r1(X119,X135)|~epred1_1(X119))&(~p3(esk69_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|r1(X135,esk66_2(X119,X135))|~r1(X119,X135)|~epred1_1(X119))))&(p2(esk68_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|r1(X135,esk66_2(X119,X135))|~r1(X119,X135)|~epred1_1(X119))))&((r1(X135,esk67_2(X119,X135))|(~r1(esk66_2(X119,X135),X137)|~p2(X137))|~r1(X119,X135)|~epred1_1(X119))&(((r1(X139,esk68_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|(~r1(esk66_2(X119,X135),X137)|~p2(X137))|~r1(X119,X135)|~epred1_1(X119))&((r1(esk68_3(X119,X135,X139),esk69_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|(~r1(esk66_2(X119,X135),X137)|~p2(X137))|~r1(X119,X135)|~epred1_1(X119))&(~p3(esk69_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|(~r1(esk66_2(X119,X135),X137)|~p2(X137))|~r1(X119,X135)|~epred1_1(X119))))&(p2(esk68_3(X119,X135,X139))|~r1(esk67_2(X119,X135),X139)|(~r1(esk66_2(X119,X135),X137)|~p2(X137))|~r1(X119,X135)|~epred1_1(X119))))))&((((r1(X119,esk72_1(X119))|r1(X119,esk70_1(X119))|~epred1_1(X119))&(~r1(esk72_1(X119),X145)|~p2(X145)|r1(X119,esk70_1(X119))|~epred1_1(X119)))&(((r1(X119,esk72_1(X119))|r1(esk70_1(X119),esk71_1(X119))|~epred1_1(X119))&(~r1(esk72_1(X119),X145)|~p2(X145)|r1(esk70_1(X119),esk71_1(X119))|~epred1_1(X119)))&((r1(X119,esk72_1(X119))|~p3(esk71_1(X119))|~epred1_1(X119))&(~r1(esk72_1(X119),X145)|~p2(X145)|~p3(esk71_1(X119))|~epred1_1(X119)))))&((r1(X119,esk72_1(X119))|p2(esk70_1(X119))|~epred1_1(X119))&(~r1(esk72_1(X119),X145)|~p2(X145)|p2(esk70_1(X119))|~epred1_1(X119)))))), 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_29])])])])])])).
% 165.87/21.35 cnf(c_0_33, negated_conjecture, (epred1_1(X1)|~r1(esk43_0,X1)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 165.87/21.35 cnf(c_0_34, negated_conjecture, (r1(esk43_0,esk47_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_35, plain, (r1(X1,esk62_3(X2,X3,X1))|p2(X4)|~r1(X3,X1)|~r1(X3,X4)|~p2(X3)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_36, negated_conjecture, (r1(X1,esk48_1(X1))|~r1(esk47_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_37, negated_conjecture, (~p2(esk48_1(X1))|~r1(esk47_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 165.87/21.35 cnf(c_0_38, plain, (r1(X1,esk72_1(X1))|r1(X1,esk70_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_39, negated_conjecture, (epred1_1(esk47_0)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 165.87/21.35 cnf(c_0_40, plain, (r1(X1,esk72_1(X1))|p2(esk70_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_41, negated_conjecture, (r1(X1,esk62_3(X2,X3,X1))|~epred1_1(X2)|~p2(X3)|~r1(esk47_0,X3)|~r1(X3,X1)|~r1(X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_36]), c_0_37])).
% 165.87/21.35 cnf(c_0_42, plain, (r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 165.87/21.35 cnf(c_0_43, plain, (p2(esk70_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_40, c_0_39])).
% 165.87/21.35 cnf(c_0_44, plain, (r1(X1,esk67_2(X2,X1))|r1(X1,esk66_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_45, plain, (r1(X1,esk62_3(X2,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|~epred1_1(X2)|~r1(esk70_1(esk47_0),X1)|~r1(X2,esk70_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_43])).
% 165.87/21.35 cnf(c_0_46, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_42]), c_0_39])])).
% 165.87/21.35 cnf(c_0_47, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 165.87/21.35 cnf(c_0_48, plain, (r1(X1,esk68_3(X2,X3,X1))|r1(X3,esk66_2(X2,X3))|~r1(esk67_2(X2,X3),X1)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_49, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_42]), c_0_39])])).
% 165.87/21.35 cnf(c_0_50, plain, (p2(esk68_3(X1,X2,X3))|r1(X2,esk66_2(X1,X2))|~r1(esk67_2(X1,X2),X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_51, plain, (p2(X5)|~r1(esk62_3(X1,X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~r1(X2,X5)|~p2(X2)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_52, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_49]), c_0_39])]), c_0_42])).
% 165.87/21.35 cnf(c_0_53, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_49]), c_0_39])]), c_0_42])).
% 165.87/21.35 cnf(c_0_54, plain, (p2(X1)|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_39])]), c_0_42]), c_0_46]), c_0_43]), c_0_53])).
% 165.87/21.35 cnf(c_0_55, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_36]), c_0_42])).
% 165.87/21.35 cnf(c_0_56, plain, (r1(X1,esk65_1(X1))|r1(X2,esk63_3(X1,X3,X2))|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_57, negated_conjecture, (r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_55]), c_0_42])).
% 165.87/21.35 cnf(c_0_58, plain, (r1(X1,esk65_1(X1))|p2(esk63_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_59, plain, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(X1,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))|r1(X1,esk65_1(X1))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 165.87/21.35 cnf(c_0_60, plain, (p2(esk63_3(X1,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))|r1(X1,esk65_1(X1))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_58, c_0_57])).
% 165.87/21.35 cnf(c_0_61, plain, (r1(X1,esk67_2(X2,X1))|~r1(esk66_2(X2,X1),X3)|~p2(X3)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_62, plain, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59, c_0_42]), c_0_39])])).
% 165.87/21.35 cnf(c_0_63, plain, (p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_42]), c_0_39])])).
% 165.87/21.35 cnf(c_0_64, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_39])]), c_0_42]), c_0_63])).
% 165.87/21.35 cnf(c_0_65, plain, (r1(X1,esk68_3(X2,X3,X1))|~r1(esk67_2(X2,X3),X1)|~r1(esk66_2(X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.35 cnf(c_0_66, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_45, c_0_64])).
% 165.87/21.35 cnf(c_0_67, plain, (p2(esk68_3(X1,X2,X3))|~r1(esk67_2(X1,X2),X3)|~r1(esk66_2(X1,X2),X4)|~p2(X4)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_68, plain, (r1(X1,esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_62]), c_0_39])]), c_0_42]), c_0_63])).
% 165.87/21.36 cnf(c_0_69, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_42]), c_0_39])])).
% 165.87/21.36 cnf(c_0_70, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_62]), c_0_39])]), c_0_42]), c_0_63])).
% 165.87/21.36 cnf(c_0_71, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_68, c_0_69])).
% 165.87/21.36 cnf(c_0_72, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_70, c_0_69])).
% 165.87/21.36 cnf(c_0_73, plain, (p2(X1)|r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_71]), c_0_39])]), c_0_42]), c_0_64]), c_0_43]), c_0_72])).
% 165.87/21.36 cnf(c_0_74, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))|r1(esk47_0,esk65_1(esk47_0))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_36]), c_0_42])).
% 165.87/21.36 cnf(c_0_75, plain, (r1(X1,esk59_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_76, negated_conjecture, (r1(esk47_0,esk72_1(esk47_0))|r1(esk47_0,esk65_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_74]), c_0_42])).
% 165.87/21.36 cnf(c_0_77, plain, (r1(X3,esk63_3(X1,X4,X3))|~r1(esk65_1(X1),X2)|~p2(X2)|~r1(X4,X3)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_78, plain, (r1(esk65_1(esk47_0),esk59_2(esk47_0,esk65_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_39])])).
% 165.87/21.36 cnf(c_0_79, plain, (p2(esk63_3(X1,X3,X4))|~r1(esk65_1(X1),X2)|~p2(X2)|~r1(X3,X4)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_80, plain, (r1(X1,esk63_3(esk47_0,X2,X1))|r1(esk47_0,esk72_1(esk47_0))|~p2(esk59_2(esk47_0,esk65_1(esk47_0)))|~r1(esk47_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_78]), c_0_39])])).
% 165.87/21.36 cnf(c_0_81, plain, (p2(esk59_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_82, plain, (p2(esk63_3(esk47_0,X1,X2))|r1(esk47_0,esk72_1(esk47_0))|~p2(esk59_2(esk47_0,esk65_1(esk47_0)))|~r1(esk47_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_78]), c_0_39])])).
% 165.87/21.36 cnf(c_0_83, plain, (r1(X1,esk63_3(esk47_0,X2,X1))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk47_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80, c_0_81]), c_0_39])]), c_0_76])).
% 165.87/21.36 cnf(c_0_84, plain, (p2(esk63_3(esk47_0,X1,X2))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk47_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_81]), c_0_39])]), c_0_76])).
% 165.87/21.36 cnf(c_0_85, plain, (r1(X1,esk63_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(spm,[status(thm)],[c_0_83, c_0_42])).
% 165.87/21.36 cnf(c_0_86, plain, (p2(esk63_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(spm,[status(thm)],[c_0_84, c_0_42])).
% 165.87/21.36 cnf(c_0_87, negated_conjecture, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_85, c_0_57])).
% 165.87/21.36 cnf(c_0_88, negated_conjecture, (p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_86, c_0_57])).
% 165.87/21.36 cnf(c_0_89, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_87]), c_0_39])]), c_0_42]), c_0_88])).
% 165.87/21.36 cnf(c_0_90, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_45, c_0_89])).
% 165.87/21.36 cnf(c_0_91, plain, (r1(X1,esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_87]), c_0_39])]), c_0_42]), c_0_88])).
% 165.87/21.36 cnf(c_0_92, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk72_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90, c_0_42]), c_0_39])])).
% 165.87/21.36 cnf(c_0_93, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk72_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_87]), c_0_39])]), c_0_42]), c_0_88])).
% 165.87/21.36 cnf(c_0_94, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 165.87/21.36 cnf(c_0_95, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk72_1(esk47_0))), inference(spm,[status(thm)],[c_0_93, c_0_92])).
% 165.87/21.36 cnf(c_0_96, plain, (p2(X1)|r1(esk47_0,esk72_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_94]), c_0_39])]), c_0_42]), c_0_89]), c_0_43]), c_0_95])).
% 165.87/21.36 cnf(c_0_97, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))|r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_36]), c_0_42])).
% 165.87/21.36 cnf(c_0_98, negated_conjecture, (r1(esk47_0,esk72_1(esk47_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_97]), c_0_42])).
% 165.87/21.36 cnf(c_0_99, plain, (r1(X1,esk70_1(X1))|~r1(esk72_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_100, plain, (r1(esk72_1(esk47_0),esk59_2(esk47_0,esk72_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_98]), c_0_39])])).
% 165.87/21.36 cnf(c_0_101, plain, (p2(esk70_1(X1))|~r1(esk72_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_32])).
% 165.87/21.36 cnf(c_0_102, plain, (r1(esk47_0,esk70_1(esk47_0))|~p2(esk59_2(esk47_0,esk72_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_100]), c_0_39])])).
% 165.87/21.36 cnf(c_0_103, plain, (p2(esk70_1(esk47_0))|~p2(esk59_2(esk47_0,esk72_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_100]), c_0_39])])).
% 165.87/21.36 cnf(c_0_104, plain, (r1(esk47_0,esk70_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_81]), c_0_39]), c_0_98])])).
% 165.87/21.36 cnf(c_0_105, plain, (p2(esk70_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_81]), c_0_39]), c_0_98])])).
% 165.87/21.36 cnf(c_0_106, negated_conjecture, (r1(X1,esk62_3(X2,esk70_1(esk47_0),X1))|~epred1_1(X2)|~r1(esk70_1(esk47_0),X1)|~r1(X2,esk70_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_104]), c_0_105])])).
% 165.87/21.36 cnf(c_0_107, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_108, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_106, c_0_107])).
% 165.87/21.36 cnf(c_0_109, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_110, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48, c_0_109]), c_0_39]), c_0_104])])).
% 165.87/21.36 cnf(c_0_111, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_109]), c_0_39]), c_0_104])])).
% 165.87/21.36 cnf(c_0_112, plain, (p2(X1)|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))|~r1(esk70_1(esk47_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_110]), c_0_39]), c_0_105]), c_0_104])]), c_0_107]), c_0_111])).
% 165.87/21.36 cnf(c_0_113, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))|r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_36]), c_0_104])])).
% 165.87/21.36 cnf(c_0_114, negated_conjecture, (r1(esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_113]), c_0_104])])).
% 165.87/21.36 cnf(c_0_115, plain, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(X1,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(X1,esk65_1(X1))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_56, c_0_114])).
% 165.87/21.36 cnf(c_0_116, plain, (p2(esk63_3(X1,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(X1,esk65_1(X1))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_58, c_0_114])).
% 165.87/21.36 cnf(c_0_117, plain, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_118, plain, (p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_119, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|r1(esk47_0,esk65_1(esk47_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_117]), c_0_39]), c_0_104])]), c_0_118])).
% 165.87/21.36 cnf(c_0_120, negated_conjecture, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_106, c_0_119])).
% 165.87/21.36 cnf(c_0_121, plain, (r1(X1,esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk65_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_117]), c_0_39]), c_0_104])]), c_0_118])).
% 165.87/21.36 cnf(c_0_122, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_123, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),X1))|r1(esk47_0,esk65_1(esk47_0))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_117]), c_0_39]), c_0_104])]), c_0_118])).
% 165.87/21.36 cnf(c_0_124, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk65_1(esk47_0))), inference(spm,[status(thm)],[c_0_121, c_0_122])).
% 165.87/21.36 cnf(c_0_125, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|r1(esk47_0,esk65_1(esk47_0))), inference(spm,[status(thm)],[c_0_123, c_0_122])).
% 165.87/21.36 cnf(c_0_126, plain, (p2(X1)|r1(esk47_0,esk65_1(esk47_0))|~r1(esk70_1(esk47_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_124]), c_0_39]), c_0_105]), c_0_104])]), c_0_119]), c_0_125])).
% 165.87/21.36 cnf(c_0_127, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))|r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_36]), c_0_104])])).
% 165.87/21.36 cnf(c_0_128, negated_conjecture, (r1(esk47_0,esk65_1(esk47_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_127]), c_0_104])])).
% 165.87/21.36 cnf(c_0_129, plain, (r1(esk65_1(esk47_0),esk59_2(esk47_0,esk65_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_128]), c_0_39])])).
% 165.87/21.36 cnf(c_0_130, plain, (r1(X1,esk63_3(esk47_0,X2,X1))|~p2(esk59_2(esk47_0,esk65_1(esk47_0)))|~r1(esk47_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77, c_0_129]), c_0_39])])).
% 165.87/21.36 cnf(c_0_131, plain, (r1(X1,esk63_3(esk47_0,X2,X1))|~r1(esk47_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_81]), c_0_39]), c_0_128])])).
% 165.87/21.36 cnf(c_0_132, plain, (r1(X1,esk63_3(esk47_0,esk70_1(esk47_0),X1))|~r1(esk70_1(esk47_0),X1)), inference(spm,[status(thm)],[c_0_131, c_0_104])).
% 165.87/21.36 cnf(c_0_133, negated_conjecture, (r1(esk66_2(esk47_0,esk70_1(esk47_0)),esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))), inference(spm,[status(thm)],[c_0_132, c_0_114])).
% 165.87/21.36 cnf(c_0_134, plain, (p2(esk63_3(esk47_0,X1,X2))|~p2(esk59_2(esk47_0,esk65_1(esk47_0)))|~r1(esk47_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_129]), c_0_39])])).
% 165.87/21.36 cnf(c_0_135, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))|~p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_133]), c_0_39]), c_0_104])])).
% 165.87/21.36 cnf(c_0_136, plain, (p2(esk63_3(esk47_0,X1,X2))|~r1(esk47_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134, c_0_81]), c_0_39]), c_0_128])])).
% 165.87/21.36 cnf(c_0_137, plain, (r1(esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_136]), c_0_104]), c_0_114])])).
% 165.87/21.36 cnf(c_0_138, plain, (r1(X1,esk68_3(esk47_0,esk70_1(esk47_0),X1))|~p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_133]), c_0_39]), c_0_104])])).
% 165.87/21.36 cnf(c_0_139, negated_conjecture, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(X1,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))|~epred1_1(X1)|~r1(X1,esk70_1(esk47_0))), inference(spm,[status(thm)],[c_0_106, c_0_137])).
% 165.87/21.36 cnf(c_0_140, plain, (r1(X1,esk68_3(esk47_0,esk70_1(esk47_0),X1))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_138, c_0_136]), c_0_104]), c_0_114])])).
% 165.87/21.36 cnf(c_0_141, plain, (r1(esk67_2(esk47_0,esk70_1(esk47_0)),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_139, c_0_104]), c_0_39])])).
% 165.87/21.36 cnf(c_0_142, plain, (r1(esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0))),esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))), inference(spm,[status(thm)],[c_0_140, c_0_141])).
% 165.87/21.36 cnf(c_0_143, plain, (p2(X1)|~p2(esk68_3(esk47_0,esk70_1(esk47_0),esk62_3(esk47_0,esk70_1(esk47_0),esk67_2(esk47_0,esk70_1(esk47_0)))))|~r1(esk70_1(esk47_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_142]), c_0_39]), c_0_105]), c_0_137]), c_0_104])])).
% 165.87/21.36 cnf(c_0_144, plain, (p2(esk68_3(esk47_0,esk70_1(esk47_0),X1))|~p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|~r1(esk67_2(esk47_0,esk70_1(esk47_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_133]), c_0_39]), c_0_104])])).
% 165.87/21.36 cnf(c_0_145, plain, (p2(X1)|~p2(esk63_3(esk47_0,esk70_1(esk47_0),esk66_2(esk47_0,esk70_1(esk47_0))))|~r1(esk70_1(esk47_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_143, c_0_144]), c_0_141])])).
% 165.87/21.36 cnf(c_0_146, plain, (p2(X1)|~r1(esk70_1(esk47_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_145, c_0_136]), c_0_104]), c_0_114])])).
% 165.87/21.36 cnf(c_0_147, negated_conjecture, (p2(esk48_1(esk70_1(esk47_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_146, c_0_36]), c_0_104])])).
% 165.87/21.36 cnf(c_0_148, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_147]), c_0_104])]), ['proof']).
% 165.87/21.36 % SZS output end Proof
% 165.87/21.36 % User time : 20.839 s
% 165.87/21.36 % System time : 0.109 s
% 165.87/21.36 % Total time : 20.948 s
% 165.87/21.36 % User time : 20.843 s
% 165.87/21.36 % System time : 0.111 s
% 165.87/21.36 % Total time : 20.953 s
% 165.87/21.36
%------------------------------------------------------------------------------