%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL652+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:20 AM UTC 2026
% Result : Theorem 65.91s 10.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL652+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n010.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 5 05:55:23 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.24/0.46 start to proof:theBenchmark.p
% 65.91/10.24 % Version : CSI_E---1.1
% 65.91/10.24 % Problem : theBenchmark.p
% 65.91/10.24 % Proof found!
% 65.91/10.24 % SZS status Theorem for theBenchmark.p
% 65.91/10.24 % SZS output start Proof
% 65.91/10.24 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))|p3(X1)))|~(p2(X2))))))))|~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2)))))))&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))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(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)))))))))))))))|(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p2(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))|p2(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/sandbox2/benchmark/theBenchmark.p', main)).
% 65.91/10.24 fof(c_0_1, plain, ![X2]:((epred2_1(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)|p3(X1)))|~p2(X2)))))))|~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2))))))&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)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~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))))))))))))))|(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(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)))))))))))), introduced(definition)).
% 65.91/10.24 fof(c_0_2, plain, ![X2]:((epred1_1(X2)<=>~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))|~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2))))))&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)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~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))))))))))))))|(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))))))), introduced(definition)).
% 65.91/10.24 fof(c_0_3, 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)|epred2_1(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)|p2(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])).
% 65.91/10.24 fof(c_0_4, plain, ![X2]:((epred2_1(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)|epred1_1(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)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1]), c_0_2])).
% 65.91/10.24 fof(c_0_5, negated_conjecture, ![X4, X5, X6, X7, X10, X11, X12, X13, X14, X18, X23, X28, X33, X38, X41, X43, X44, X45, X47, X48, X49, X51, X52, X53, X55, X56, X57, X59, X60, X61]:((((((((~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(esk1_0,X11)|epred2_1(X11)))&((r1(X12,esk4_1(X12))|(~r1(X12,X13)|(~r1(X13,X14)|p1(X14)))|~r1(esk1_0,X12))&(~p1(esk4_1(X12))|(~r1(X12,X13)|(~r1(X13,X14)|p1(X14)))|~r1(esk1_0,X12))))&((r1(esk1_0,esk5_0)&(r1(esk5_0,esk6_0)&(~r1(esk6_0,X18)|p1(X18))))&(r1(esk5_0,esk7_0)&~p1(esk7_0))))&(((r1(esk1_0,esk8_0)&((r1(esk8_0,esk9_0)&(r1(esk9_0,esk10_0)&(~r1(esk10_0,X23)|p1(X23))))&(r1(esk9_0,esk11_0)&~p1(esk11_0))))&(((r1(esk8_0,esk12_0)&((r1(esk12_0,esk13_0)&(r1(esk13_0,esk14_0)&(~r1(esk14_0,X28)|p1(X28))))&(r1(esk13_0,esk15_0)&~p1(esk15_0))))&(((r1(esk12_0,esk16_0)&((r1(esk16_0,esk17_0)&(r1(esk17_0,esk18_0)&(~r1(esk18_0,X33)|p1(X33))))&(r1(esk17_0,esk19_0)&~p1(esk19_0))))&(((r1(esk16_0,esk20_0)&((r1(esk20_0,esk21_0)&(r1(esk21_0,esk22_0)&(~r1(esk22_0,X38)|p1(X38))))&(r1(esk21_0,esk23_0)&~p1(esk23_0))))&(r1(esk20_0,esk24_0)&((r1(X41,esk25_1(X41))|~r1(esk24_0,X41))&(~p2(esk25_1(X41))|~r1(esk24_0,X41)))))&((r1(X43,esk26_1(X43))|(~r1(esk20_0,X43)|(~r1(X43,X44)|(~r1(X44,X45)|~p1(X45)))))&(p1(esk26_1(X43))|(~r1(esk20_0,X43)|(~r1(X43,X44)|(~r1(X44,X45)|~p1(X45))))))))&((r1(X47,esk27_1(X47))|(~r1(esk16_0,X47)|(~r1(X47,X48)|(~r1(X48,X49)|~p1(X49)))))&(p1(esk27_1(X47))|(~r1(esk16_0,X47)|(~r1(X47,X48)|(~r1(X48,X49)|~p1(X49))))))))&((r1(X51,esk28_1(X51))|(~r1(esk12_0,X51)|(~r1(X51,X52)|(~r1(X52,X53)|~p1(X53)))))&(p1(esk28_1(X51))|(~r1(esk12_0,X51)|(~r1(X51,X52)|(~r1(X52,X53)|~p1(X53))))))))&((r1(X55,esk29_1(X55))|(~r1(esk8_0,X55)|(~r1(X55,X56)|(~r1(X56,X57)|~p1(X57)))))&(p1(esk29_1(X55))|(~r1(esk8_0,X55)|(~r1(X55,X56)|(~r1(X56,X57)|~p1(X57))))))))&((r1(X59,esk30_1(X59))|(~r1(esk1_0,X59)|(~r1(X59,X60)|(~r1(X60,X61)|~p1(X61)))))&(p1(esk30_1(X59))|(~r1(esk1_0,X59)|(~r1(X59,X60)|(~r1(X60,X61)|~p1(X61)))))))), 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])])])])])])).
% 65.91/10.24 fof(c_0_6, plain, ![X90, X91, X92, X93, X96, X97, X98, X99, X100, X103, X104, X105, X106, X107, X110, X111, X112, X113, X114, X117, X118, X119, X120, X121, X123, X124, X125, X127, X128, X129, X131, X132, X133]:((((((r1(X91,esk46_2(X90,X91))|(r1(X93,esk45_4(X90,X91,X92,X93))|~r1(X92,X93)|~r1(X91,X92))|~r1(X90,X91)|~epred2_1(X90))&(~r1(esk46_2(X90,X91),X96)|~p1(X96)|(r1(X93,esk45_4(X90,X91,X92,X93))|~r1(X92,X93)|~r1(X91,X92))|~r1(X90,X91)|~epred2_1(X90)))&((r1(X91,esk46_2(X90,X91))|(p1(esk45_4(X90,X91,X92,X93))|~r1(X92,X93)|~r1(X91,X92))|~r1(X90,X91)|~epred2_1(X90))&(~r1(esk46_2(X90,X91),X96)|~p1(X96)|(p1(esk45_4(X90,X91,X92,X93))|~r1(X92,X93)|~r1(X91,X92))|~r1(X90,X91)|~epred2_1(X90))))&(((((r1(X98,esk48_3(X90,X97,X98))|(r1(X100,esk47_5(X90,X97,X98,X99,X100))|~r1(X99,X100)|~r1(X98,X99))|~r1(X97,X98)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk48_3(X90,X97,X98),X103)|~p1(X103)|(r1(X100,esk47_5(X90,X97,X98,X99,X100))|~r1(X99,X100)|~r1(X98,X99))|~r1(X97,X98)|~r1(X90,X97)|~epred2_1(X90)))&((r1(X98,esk48_3(X90,X97,X98))|(p1(esk47_5(X90,X97,X98,X99,X100))|~r1(X99,X100)|~r1(X98,X99))|~r1(X97,X98)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk48_3(X90,X97,X98),X103)|~p1(X103)|(p1(esk47_5(X90,X97,X98,X99,X100))|~r1(X99,X100)|~r1(X98,X99))|~r1(X97,X98)|~r1(X90,X97)|~epred2_1(X90))))&(((((r1(X105,esk50_4(X90,X97,X104,X105))|(r1(X107,esk49_6(X90,X97,X104,X105,X106,X107))|~r1(X106,X107)|~r1(X105,X106))|~r1(X104,X105)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk50_4(X90,X97,X104,X105),X110)|~p1(X110)|(r1(X107,esk49_6(X90,X97,X104,X105,X106,X107))|~r1(X106,X107)|~r1(X105,X106))|~r1(X104,X105)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90)))&((r1(X105,esk50_4(X90,X97,X104,X105))|(p1(esk49_6(X90,X97,X104,X105,X106,X107))|~r1(X106,X107)|~r1(X105,X106))|~r1(X104,X105)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk50_4(X90,X97,X104,X105),X110)|~p1(X110)|(p1(esk49_6(X90,X97,X104,X105,X106,X107))|~r1(X106,X107)|~r1(X105,X106))|~r1(X104,X105)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))))&(((((r1(X112,esk52_5(X90,X97,X104,X111,X112))|(r1(X114,esk51_7(X90,X97,X104,X111,X112,X113,X114))|~r1(X113,X114)|~r1(X112,X113))|~r1(X111,X112)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk52_5(X90,X97,X104,X111,X112),X117)|~p1(X117)|(r1(X114,esk51_7(X90,X97,X104,X111,X112,X113,X114))|~r1(X113,X114)|~r1(X112,X113))|~r1(X111,X112)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90)))&((r1(X112,esk52_5(X90,X97,X104,X111,X112))|(p1(esk51_7(X90,X97,X104,X111,X112,X113,X114))|~r1(X113,X114)|~r1(X112,X113))|~r1(X111,X112)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~r1(esk52_5(X90,X97,X104,X111,X112),X117)|~p1(X117)|(p1(esk51_7(X90,X97,X104,X111,X112,X113,X114))|~r1(X113,X114)|~r1(X112,X113))|~r1(X111,X112)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))))&(~r1(X111,X118)|epred1_1(X118)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90)))&((r1(X119,esk53_5(X90,X97,X104,X111,X119))|(~r1(X119,X120)|(~r1(X120,X121)|p1(X121)))|~r1(X111,X119)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~p1(esk53_5(X90,X97,X104,X111,X119))|(~r1(X119,X120)|(~r1(X120,X121)|p1(X121)))|~r1(X111,X119)|~r1(X104,X111)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90)))))&((r1(X123,esk54_4(X90,X97,X104,X123))|(~r1(X123,X124)|(~r1(X124,X125)|p1(X125)))|~r1(X104,X123)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90))&(~p1(esk54_4(X90,X97,X104,X123))|(~r1(X123,X124)|(~r1(X124,X125)|p1(X125)))|~r1(X104,X123)|~r1(X97,X104)|~r1(X90,X97)|~epred2_1(X90)))))&((r1(X127,esk55_3(X90,X97,X127))|(~r1(X127,X128)|(~r1(X128,X129)|p1(X129)))|~r1(X97,X127)|~r1(X90,X97)|~epred2_1(X90))&(~p1(esk55_3(X90,X97,X127))|(~r1(X127,X128)|(~r1(X128,X129)|p1(X129)))|~r1(X97,X127)|~r1(X90,X97)|~epred2_1(X90)))))&((r1(X131,esk56_2(X90,X131))|(~r1(X131,X132)|(~r1(X132,X133)|p1(X133)))|~r1(X90,X131)|~epred2_1(X90))&(~p1(esk56_2(X90,X131))|(~r1(X131,X132)|(~r1(X132,X133)|p1(X133)))|~r1(X90,X131)|~epred2_1(X90))))), 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_4])])])])])])).
% 65.91/10.24 cnf(c_0_7, negated_conjecture, (epred2_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_8, negated_conjecture, (r1(esk1_0,esk8_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_9, 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_6])).
% 65.91/10.24 cnf(c_0_10, negated_conjecture, (r1(esk8_0,esk12_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_11, negated_conjecture, (epred2_1(esk8_0)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 65.91/10.24 cnf(c_0_12, negated_conjecture, (epred1_1(X1)|~r1(esk12_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_9, c_0_10]), c_0_11])])).
% 65.91/10.24 cnf(c_0_13, negated_conjecture, (r1(esk12_0,esk16_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 fof(c_0_14, plain, ![X2]:((epred1_1(X2)=>~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))|~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2))))))&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)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~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))))))))))))))|(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))))))), inference(split_equiv,[status(thm)],[c_0_2])).
% 65.91/10.24 cnf(c_0_15, negated_conjecture, (epred1_1(X1)|~r1(esk16_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 65.91/10.24 cnf(c_0_16, negated_conjecture, (r1(esk16_0,esk20_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 fof(c_0_17, plain, ![X63, X64, X67, X68, X70, X72, X73, X74, X78, X79, X81, X83, X89]:((((((((r1(X64,esk31_2(X63,X64))|~r1(X63,X64)|~epred1_1(X63))&((r1(esk31_2(X63,X64),esk32_2(X63,X64))|~r1(X63,X64)|~epred1_1(X63))&(~p3(esk32_2(X63,X64))|~r1(X63,X64)|~epred1_1(X63))))&(p2(esk31_2(X63,X64))|~r1(X63,X64)|~epred1_1(X63)))&((((r1(X70,esk34_3(X63,X67,X70))|~r1(X67,X70)|(r1(X68,esk33_3(X63,X67,X68))|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63))&(~r1(esk34_3(X63,X67,X70),X72)|~p2(X72)|~r1(X67,X70)|(r1(X68,esk33_3(X63,X67,X68))|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63)))&((r1(X70,esk34_3(X63,X67,X70))|~r1(X67,X70)|(~p3(esk33_3(X63,X67,X68))|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63))&(~r1(esk34_3(X63,X67,X70),X72)|~p2(X72)|~r1(X67,X70)|(~p3(esk33_3(X63,X67,X68))|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63))))&((r1(X70,esk34_3(X63,X67,X70))|~r1(X67,X70)|(p2(X68)|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63))&(~r1(esk34_3(X63,X67,X70),X72)|~p2(X72)|~r1(X67,X70)|(p2(X68)|~r1(X67,X68)|~p2(X67))|~r1(X63,X67)|~epred1_1(X63)))))&((((r1(X63,esk37_1(X63))|(r1(X74,esk35_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63))&(~r1(esk37_1(X63),X78)|~p2(X78)|(r1(X74,esk35_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63)))&(((r1(X63,esk37_1(X63))|(r1(esk35_3(X63,X73,X74),esk36_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63))&(~r1(esk37_1(X63),X78)|~p2(X78)|(r1(esk35_3(X63,X73,X74),esk36_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63)))&((r1(X63,esk37_1(X63))|(~p3(esk36_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63))&(~r1(esk37_1(X63),X78)|~p2(X78)|(~p3(esk36_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63)))))&((r1(X63,esk37_1(X63))|(p2(esk35_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63))&(~r1(esk37_1(X63),X78)|~p2(X78)|(p2(esk35_3(X63,X73,X74))|~r1(X73,X74)|~r1(X63,X73))|~epred1_1(X63)))))&(((r1(X79,esk39_2(X63,X79))|r1(X79,esk38_2(X63,X79))|~r1(X63,X79)|~epred1_1(X63))&(((r1(X83,esk40_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|r1(X79,esk38_2(X63,X79))|~r1(X63,X79)|~epred1_1(X63))&((r1(esk40_3(X63,X79,X83),esk41_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|r1(X79,esk38_2(X63,X79))|~r1(X63,X79)|~epred1_1(X63))&(~p3(esk41_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|r1(X79,esk38_2(X63,X79))|~r1(X63,X79)|~epred1_1(X63))))&(p2(esk40_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|r1(X79,esk38_2(X63,X79))|~r1(X63,X79)|~epred1_1(X63))))&((r1(X79,esk39_2(X63,X79))|(~r1(esk38_2(X63,X79),X81)|~p2(X81))|~r1(X63,X79)|~epred1_1(X63))&(((r1(X83,esk40_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|(~r1(esk38_2(X63,X79),X81)|~p2(X81))|~r1(X63,X79)|~epred1_1(X63))&((r1(esk40_3(X63,X79,X83),esk41_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|(~r1(esk38_2(X63,X79),X81)|~p2(X81))|~r1(X63,X79)|~epred1_1(X63))&(~p3(esk41_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|(~r1(esk38_2(X63,X79),X81)|~p2(X81))|~r1(X63,X79)|~epred1_1(X63))))&(p2(esk40_3(X63,X79,X83))|~r1(esk39_2(X63,X79),X83)|(~r1(esk38_2(X63,X79),X81)|~p2(X81))|~r1(X63,X79)|~epred1_1(X63))))))&((((r1(X63,esk44_1(X63))|r1(X63,esk42_1(X63))|~epred1_1(X63))&(~r1(esk44_1(X63),X89)|~p2(X89)|r1(X63,esk42_1(X63))|~epred1_1(X63)))&(((r1(X63,esk44_1(X63))|r1(esk42_1(X63),esk43_1(X63))|~epred1_1(X63))&(~r1(esk44_1(X63),X89)|~p2(X89)|r1(esk42_1(X63),esk43_1(X63))|~epred1_1(X63)))&((r1(X63,esk44_1(X63))|~p3(esk43_1(X63))|~epred1_1(X63))&(~r1(esk44_1(X63),X89)|~p2(X89)|~p3(esk43_1(X63))|~epred1_1(X63)))))&((r1(X63,esk44_1(X63))|p2(esk42_1(X63))|~epred1_1(X63))&(~r1(esk44_1(X63),X89)|~p2(X89)|p2(esk42_1(X63))|~epred1_1(X63)))))), 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_14])])])])])])).
% 65.91/10.24 cnf(c_0_18, negated_conjecture, (epred1_1(X1)|~r1(esk20_0,X1)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 65.91/10.24 cnf(c_0_19, negated_conjecture, (r1(esk20_0,esk24_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_20, plain, (r1(X1,esk34_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_17])).
% 65.91/10.24 cnf(c_0_21, negated_conjecture, (r1(X1,esk25_1(X1))|~r1(esk24_0,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_22, negated_conjecture, (~p2(esk25_1(X1))|~r1(esk24_0,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 65.91/10.24 cnf(c_0_23, plain, (r1(X1,esk44_1(X1))|r1(X1,esk42_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_24, negated_conjecture, (epred1_1(esk24_0)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 65.91/10.24 cnf(c_0_25, plain, (r1(X1,esk44_1(X1))|p2(esk42_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_26, negated_conjecture, (r1(X1,esk34_3(X2,X3,X1))|~epred1_1(X2)|~p2(X3)|~r1(esk24_0,X3)|~r1(X3,X1)|~r1(X2,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_20, c_0_21]), c_0_22])).
% 65.91/10.24 cnf(c_0_27, plain, (r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 65.91/10.24 cnf(c_0_28, plain, (p2(esk42_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_25, c_0_24])).
% 65.91/10.24 cnf(c_0_29, plain, (r1(X1,esk39_2(X2,X1))|r1(X1,esk38_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_30, plain, (r1(X1,esk34_3(X2,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|~epred1_1(X2)|~r1(esk42_1(esk24_0),X1)|~r1(X2,esk42_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_28])).
% 65.91/10.24 cnf(c_0_31, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_32, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 65.91/10.24 cnf(c_0_33, plain, (r1(X1,esk40_3(X2,X3,X1))|r1(X3,esk38_2(X2,X3))|~r1(esk39_2(X2,X3),X1)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_34, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_35, plain, (p2(esk40_3(X1,X2,X3))|r1(X2,esk38_2(X1,X2))|~r1(esk39_2(X1,X2),X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_36, plain, (p2(X5)|~r1(esk34_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_17])).
% 65.91/10.24 cnf(c_0_37, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_24])]), c_0_27])).
% 65.91/10.24 cnf(c_0_38, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_34]), c_0_24])]), c_0_27])).
% 65.91/10.24 cnf(c_0_39, plain, (p2(X1)|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk42_1(esk24_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_36, c_0_37]), c_0_24])]), c_0_27]), c_0_31]), c_0_28]), c_0_38])).
% 65.91/10.24 cnf(c_0_40, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_21]), c_0_27])).
% 65.91/10.24 cnf(c_0_41, plain, (r1(X1,esk37_1(X1))|r1(X2,esk35_3(X1,X3,X2))|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_42, negated_conjecture, (r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_40]), c_0_27])).
% 65.91/10.24 cnf(c_0_43, plain, (r1(X1,esk37_1(X1))|p2(esk35_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_44, plain, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))|r1(X1,esk37_1(X1))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_41, c_0_42])).
% 65.91/10.24 cnf(c_0_45, plain, (p2(esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))|r1(X1,esk37_1(X1))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_43, c_0_42])).
% 65.91/10.24 cnf(c_0_46, plain, (r1(X1,esk39_2(X2,X1))|~r1(esk38_2(X2,X1),X3)|~p2(X3)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_47, plain, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_48, plain, (p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_49, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_47]), c_0_24])]), c_0_27]), c_0_48])).
% 65.91/10.24 cnf(c_0_50, plain, (r1(X1,esk40_3(X2,X3,X1))|~r1(esk39_2(X2,X3),X1)|~r1(esk38_2(X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_51, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_30, c_0_49])).
% 65.91/10.24 cnf(c_0_52, plain, (p2(esk40_3(X1,X2,X3))|~r1(esk39_2(X1,X2),X3)|~r1(esk38_2(X1,X2),X4)|~p2(X4)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_53, plain, (r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_47]), c_0_24])]), c_0_27]), c_0_48])).
% 65.91/10.24 cnf(c_0_54, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_55, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_47]), c_0_24])]), c_0_27]), c_0_48])).
% 65.91/10.24 cnf(c_0_56, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 65.91/10.24 cnf(c_0_57, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_55, c_0_54])).
% 65.91/10.24 cnf(c_0_58, plain, (p2(X1)|r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))|~r1(esk42_1(esk24_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_36, c_0_56]), c_0_24])]), c_0_27]), c_0_49]), c_0_28]), c_0_57])).
% 65.91/10.24 cnf(c_0_59, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))|r1(esk24_0,esk37_1(esk24_0))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_21]), c_0_27])).
% 65.91/10.24 cnf(c_0_60, plain, (r1(X1,esk31_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_61, negated_conjecture, (r1(esk24_0,esk44_1(esk24_0))|r1(esk24_0,esk37_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_59]), c_0_27])).
% 65.91/10.24 cnf(c_0_62, plain, (r1(X3,esk35_3(X1,X4,X3))|~r1(esk37_1(X1),X2)|~p2(X2)|~r1(X4,X3)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_63, plain, (r1(esk37_1(esk24_0),esk31_2(esk24_0,esk37_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_61]), c_0_24])])).
% 65.91/10.24 cnf(c_0_64, plain, (p2(esk35_3(X1,X3,X4))|~r1(esk37_1(X1),X2)|~p2(X2)|~r1(X3,X4)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_65, plain, (r1(X1,esk35_3(esk24_0,X2,X1))|r1(esk24_0,esk44_1(esk24_0))|~p2(esk31_2(esk24_0,esk37_1(esk24_0)))|~r1(esk24_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_24])])).
% 65.91/10.24 cnf(c_0_66, plain, (p2(esk31_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_67, plain, (p2(esk35_3(esk24_0,X1,X2))|r1(esk24_0,esk44_1(esk24_0))|~p2(esk31_2(esk24_0,esk37_1(esk24_0)))|~r1(esk24_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_63]), c_0_24])])).
% 65.91/10.24 cnf(c_0_68, plain, (r1(X1,esk35_3(esk24_0,X2,X1))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk24_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_24])]), c_0_61])).
% 65.91/10.24 cnf(c_0_69, plain, (p2(esk35_3(esk24_0,X1,X2))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk24_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_66]), c_0_24])]), c_0_61])).
% 65.91/10.24 cnf(c_0_70, plain, (r1(X1,esk35_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk42_1(esk24_0),X1)), inference(spm,[status(thm)],[c_0_68, c_0_27])).
% 65.91/10.24 cnf(c_0_71, plain, (p2(esk35_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk42_1(esk24_0),X1)), inference(spm,[status(thm)],[c_0_69, c_0_27])).
% 65.91/10.24 cnf(c_0_72, negated_conjecture, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_70, c_0_42])).
% 65.91/10.24 cnf(c_0_73, negated_conjecture, (p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_71, c_0_42])).
% 65.91/10.24 cnf(c_0_74, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_72]), c_0_24])]), c_0_27]), c_0_73])).
% 65.91/10.24 cnf(c_0_75, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_30, c_0_74])).
% 65.91/10.24 cnf(c_0_76, plain, (r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_72]), c_0_24])]), c_0_27]), c_0_73])).
% 65.91/10.24 cnf(c_0_77, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk44_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_27]), c_0_24])])).
% 65.91/10.24 cnf(c_0_78, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk44_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_72]), c_0_24])]), c_0_27]), c_0_73])).
% 65.91/10.24 cnf(c_0_79, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_76, c_0_77])).
% 65.91/10.24 cnf(c_0_80, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk44_1(esk24_0))), inference(spm,[status(thm)],[c_0_78, c_0_77])).
% 65.91/10.24 cnf(c_0_81, plain, (p2(X1)|r1(esk24_0,esk44_1(esk24_0))|~r1(esk42_1(esk24_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_36, c_0_79]), c_0_24])]), c_0_27]), c_0_74]), c_0_28]), c_0_80])).
% 65.91/10.24 cnf(c_0_82, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))|r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_21]), c_0_27])).
% 65.91/10.24 cnf(c_0_83, negated_conjecture, (r1(esk24_0,esk44_1(esk24_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_82]), c_0_27])).
% 65.91/10.24 cnf(c_0_84, plain, (r1(X1,esk42_1(X1))|~r1(esk44_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_85, plain, (r1(esk44_1(esk24_0),esk31_2(esk24_0,esk44_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_83]), c_0_24])])).
% 65.91/10.24 cnf(c_0_86, plain, (p2(esk42_1(X1))|~r1(esk44_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 65.91/10.24 cnf(c_0_87, plain, (r1(esk24_0,esk42_1(esk24_0))|~p2(esk31_2(esk24_0,esk44_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_85]), c_0_24])])).
% 65.91/10.24 cnf(c_0_88, plain, (p2(esk42_1(esk24_0))|~p2(esk31_2(esk24_0,esk44_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_85]), c_0_24])])).
% 65.91/10.24 cnf(c_0_89, plain, (r1(esk24_0,esk42_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_66]), c_0_24]), c_0_83])])).
% 65.91/10.24 cnf(c_0_90, plain, (p2(esk42_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_66]), c_0_24]), c_0_83])])).
% 65.91/10.24 cnf(c_0_91, negated_conjecture, (r1(X1,esk34_3(X2,esk42_1(esk24_0),X1))|~epred1_1(X2)|~r1(esk42_1(esk24_0),X1)|~r1(X2,esk42_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_89]), c_0_90])])).
% 65.91/10.24 cnf(c_0_92, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_93, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_91, c_0_92])).
% 65.91/10.24 cnf(c_0_94, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_95, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_94]), c_0_24]), c_0_89])])).
% 65.91/10.24 cnf(c_0_96, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35, c_0_94]), c_0_24]), c_0_89])])).
% 65.91/10.24 cnf(c_0_97, plain, (p2(X1)|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))|~r1(esk42_1(esk24_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_36, c_0_95]), c_0_24]), c_0_90]), c_0_89])]), c_0_92]), c_0_96])).
% 65.91/10.24 cnf(c_0_98, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))|r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_21]), c_0_89])])).
% 65.91/10.24 cnf(c_0_99, negated_conjecture, (r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_98]), c_0_89])])).
% 65.91/10.24 cnf(c_0_100, plain, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(X1,esk37_1(X1))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_41, c_0_99])).
% 65.91/10.24 cnf(c_0_101, plain, (p2(esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(X1,esk37_1(X1))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_43, c_0_99])).
% 65.91/10.24 cnf(c_0_102, plain, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_100, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_103, plain, (p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_104, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|r1(esk24_0,esk37_1(esk24_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_102]), c_0_24]), c_0_89])]), c_0_103])).
% 65.91/10.24 cnf(c_0_105, negated_conjecture, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_91, c_0_104])).
% 65.91/10.24 cnf(c_0_106, plain, (r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk37_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_102]), c_0_24]), c_0_89])]), c_0_103])).
% 65.91/10.24 cnf(c_0_107, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_108, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))|r1(esk24_0,esk37_1(esk24_0))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_102]), c_0_24]), c_0_89])]), c_0_103])).
% 65.91/10.24 cnf(c_0_109, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk37_1(esk24_0))), inference(spm,[status(thm)],[c_0_106, c_0_107])).
% 65.91/10.24 cnf(c_0_110, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|r1(esk24_0,esk37_1(esk24_0))), inference(spm,[status(thm)],[c_0_108, c_0_107])).
% 65.91/10.24 cnf(c_0_111, plain, (p2(X1)|r1(esk24_0,esk37_1(esk24_0))|~r1(esk42_1(esk24_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_36, c_0_109]), c_0_24]), c_0_90]), c_0_89])]), c_0_104]), c_0_110])).
% 65.91/10.24 cnf(c_0_112, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))|r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111, c_0_21]), c_0_89])])).
% 65.91/10.24 cnf(c_0_113, negated_conjecture, (r1(esk24_0,esk37_1(esk24_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_112]), c_0_89])])).
% 65.91/10.24 cnf(c_0_114, plain, (r1(esk37_1(esk24_0),esk31_2(esk24_0,esk37_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60, c_0_113]), c_0_24])])).
% 65.91/10.24 cnf(c_0_115, plain, (r1(X1,esk35_3(esk24_0,X2,X1))|~p2(esk31_2(esk24_0,esk37_1(esk24_0)))|~r1(esk24_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_114]), c_0_24])])).
% 65.91/10.24 cnf(c_0_116, plain, (r1(X1,esk35_3(esk24_0,X2,X1))|~r1(esk24_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_115, c_0_66]), c_0_24]), c_0_113])])).
% 65.91/10.24 cnf(c_0_117, plain, (r1(X1,esk35_3(esk24_0,esk42_1(esk24_0),X1))|~r1(esk42_1(esk24_0),X1)), inference(spm,[status(thm)],[c_0_116, c_0_89])).
% 65.91/10.24 cnf(c_0_118, negated_conjecture, (r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))), inference(spm,[status(thm)],[c_0_117, c_0_99])).
% 65.91/10.24 cnf(c_0_119, plain, (p2(esk35_3(esk24_0,X1,X2))|~p2(esk31_2(esk24_0,esk37_1(esk24_0)))|~r1(esk24_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_114]), c_0_24])])).
% 65.91/10.24 cnf(c_0_120, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))|~p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_118]), c_0_24]), c_0_89])])).
% 65.91/10.24 cnf(c_0_121, plain, (p2(esk35_3(esk24_0,X1,X2))|~r1(esk24_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119, c_0_66]), c_0_24]), c_0_113])])).
% 65.91/10.24 cnf(c_0_122, plain, (r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_121]), c_0_89]), c_0_99])])).
% 65.91/10.24 cnf(c_0_123, plain, (r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))|~p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_118]), c_0_24]), c_0_89])])).
% 65.91/10.24 cnf(c_0_124, negated_conjecture, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))|~epred1_1(X1)|~r1(X1,esk42_1(esk24_0))), inference(spm,[status(thm)],[c_0_91, c_0_122])).
% 65.91/10.24 cnf(c_0_125, plain, (r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_121]), c_0_89]), c_0_99])])).
% 65.91/10.24 cnf(c_0_126, plain, (r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_89]), c_0_24])])).
% 65.91/10.24 cnf(c_0_127, plain, (r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))), inference(spm,[status(thm)],[c_0_125, c_0_126])).
% 65.91/10.24 cnf(c_0_128, plain, (p2(X1)|~p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))|~r1(esk42_1(esk24_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_36, c_0_127]), c_0_24]), c_0_90]), c_0_122]), c_0_89])])).
% 65.91/10.24 cnf(c_0_129, plain, (p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))|~p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|~r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_52, c_0_118]), c_0_24]), c_0_89])])).
% 65.91/10.24 cnf(c_0_130, plain, (p2(X1)|~p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))|~r1(esk42_1(esk24_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128, c_0_129]), c_0_126])])).
% 65.91/10.24 cnf(c_0_131, plain, (p2(X1)|~r1(esk42_1(esk24_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_121]), c_0_89]), c_0_99])])).
% 65.91/10.24 cnf(c_0_132, negated_conjecture, (p2(esk25_1(esk42_1(esk24_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131, c_0_21]), c_0_89])])).
% 65.91/10.24 cnf(c_0_133, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_132]), c_0_89])]), ['proof']).
% 65.91/10.24 % SZS output end Proof
% 65.91/10.24 % User time : 9.626 s
% 65.91/10.24 % System time : 0.075 s
% 65.91/10.24 % Total time : 9.701 s
% 65.91/10.24 % User time : 46.613 s
% 65.91/10.24 % System time : 0.128 s
% 65.91/10.24 % Total time : 46.741 s
% 65.91/10.24
%------------------------------------------------------------------------------