%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL652+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n005.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 2.32s 0.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL652+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 12:49:05 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.23/0.48 start to proof:theBenchmark.p
% 2.32/0.89 % Version : CSI_E---1.1
% 2.32/0.89 % Problem : theBenchmark.p
% 2.32/0.89 % Proof found!
% 2.32/0.89 % SZS status Theorem for theBenchmark.p
% 2.32/0.89 % SZS output start Proof
% 2.32/0.89 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))|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))))))))|![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)))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 2.32/0.89 fof(c_0_1, 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)).
% 2.32/0.89 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)|epred1_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)|p2(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])).
% 2.32/0.89 fof(c_0_3, 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_1])).
% 2.32/0.89 fof(c_0_4, negated_conjecture, ![X4, X5, X6, X7, X10, X11, X12, X13, X14, X18, X21, X23, X24, X25]:((((((((~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)|epred1_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(X21,esk9_1(X21))|~r1(esk8_0,X21))&(~p2(esk9_1(X21))|~r1(esk8_0,X21)))))&((r1(X23,esk10_1(X23))|(~r1(esk1_0,X23)|(~r1(X23,X24)|(~r1(X24,X25)|~p1(X25)))))&(p1(esk10_1(X23))|(~r1(esk1_0,X23)|(~r1(X23,X24)|(~r1(X24,X25)|~p1(X25)))))))), 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])])])])])])).
% 2.32/0.89 fof(c_0_5, plain, ![X27, X28, X31, X32, X34, X36, X37, X38, X42, X43, X45, X47, X53]:((((((((r1(X28,esk11_2(X27,X28))|~r1(X27,X28)|~epred1_1(X27))&((r1(esk11_2(X27,X28),esk12_2(X27,X28))|~r1(X27,X28)|~epred1_1(X27))&(~p3(esk12_2(X27,X28))|~r1(X27,X28)|~epred1_1(X27))))&(p2(esk11_2(X27,X28))|~r1(X27,X28)|~epred1_1(X27)))&((((r1(X34,esk14_3(X27,X31,X34))|~r1(X31,X34)|(r1(X32,esk13_3(X27,X31,X32))|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27))&(~r1(esk14_3(X27,X31,X34),X36)|~p2(X36)|~r1(X31,X34)|(r1(X32,esk13_3(X27,X31,X32))|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27)))&((r1(X34,esk14_3(X27,X31,X34))|~r1(X31,X34)|(~p3(esk13_3(X27,X31,X32))|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27))&(~r1(esk14_3(X27,X31,X34),X36)|~p2(X36)|~r1(X31,X34)|(~p3(esk13_3(X27,X31,X32))|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27))))&((r1(X34,esk14_3(X27,X31,X34))|~r1(X31,X34)|(p2(X32)|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27))&(~r1(esk14_3(X27,X31,X34),X36)|~p2(X36)|~r1(X31,X34)|(p2(X32)|~r1(X31,X32)|~p2(X31))|~r1(X27,X31)|~epred1_1(X27)))))&((((r1(X27,esk17_1(X27))|(r1(X38,esk15_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27))&(~r1(esk17_1(X27),X42)|~p2(X42)|(r1(X38,esk15_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27)))&(((r1(X27,esk17_1(X27))|(r1(esk15_3(X27,X37,X38),esk16_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27))&(~r1(esk17_1(X27),X42)|~p2(X42)|(r1(esk15_3(X27,X37,X38),esk16_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27)))&((r1(X27,esk17_1(X27))|(~p3(esk16_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27))&(~r1(esk17_1(X27),X42)|~p2(X42)|(~p3(esk16_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27)))))&((r1(X27,esk17_1(X27))|(p2(esk15_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27))&(~r1(esk17_1(X27),X42)|~p2(X42)|(p2(esk15_3(X27,X37,X38))|~r1(X37,X38)|~r1(X27,X37))|~epred1_1(X27)))))&(((r1(X43,esk19_2(X27,X43))|r1(X43,esk18_2(X27,X43))|~r1(X27,X43)|~epred1_1(X27))&(((r1(X47,esk20_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|r1(X43,esk18_2(X27,X43))|~r1(X27,X43)|~epred1_1(X27))&((r1(esk20_3(X27,X43,X47),esk21_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|r1(X43,esk18_2(X27,X43))|~r1(X27,X43)|~epred1_1(X27))&(~p3(esk21_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|r1(X43,esk18_2(X27,X43))|~r1(X27,X43)|~epred1_1(X27))))&(p2(esk20_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|r1(X43,esk18_2(X27,X43))|~r1(X27,X43)|~epred1_1(X27))))&((r1(X43,esk19_2(X27,X43))|(~r1(esk18_2(X27,X43),X45)|~p2(X45))|~r1(X27,X43)|~epred1_1(X27))&(((r1(X47,esk20_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|(~r1(esk18_2(X27,X43),X45)|~p2(X45))|~r1(X27,X43)|~epred1_1(X27))&((r1(esk20_3(X27,X43,X47),esk21_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|(~r1(esk18_2(X27,X43),X45)|~p2(X45))|~r1(X27,X43)|~epred1_1(X27))&(~p3(esk21_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|(~r1(esk18_2(X27,X43),X45)|~p2(X45))|~r1(X27,X43)|~epred1_1(X27))))&(p2(esk20_3(X27,X43,X47))|~r1(esk19_2(X27,X43),X47)|(~r1(esk18_2(X27,X43),X45)|~p2(X45))|~r1(X27,X43)|~epred1_1(X27))))))&((((r1(X27,esk24_1(X27))|r1(X27,esk22_1(X27))|~epred1_1(X27))&(~r1(esk24_1(X27),X53)|~p2(X53)|r1(X27,esk22_1(X27))|~epred1_1(X27)))&(((r1(X27,esk24_1(X27))|r1(esk22_1(X27),esk23_1(X27))|~epred1_1(X27))&(~r1(esk24_1(X27),X53)|~p2(X53)|r1(esk22_1(X27),esk23_1(X27))|~epred1_1(X27)))&((r1(X27,esk24_1(X27))|~p3(esk23_1(X27))|~epred1_1(X27))&(~r1(esk24_1(X27),X53)|~p2(X53)|~p3(esk23_1(X27))|~epred1_1(X27)))))&((r1(X27,esk24_1(X27))|p2(esk22_1(X27))|~epred1_1(X27))&(~r1(esk24_1(X27),X53)|~p2(X53)|p2(esk22_1(X27))|~epred1_1(X27)))))), 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])])])])])])).
% 2.32/0.89 cnf(c_0_6, negated_conjecture, (epred1_1(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 2.32/0.89 cnf(c_0_7, negated_conjecture, (r1(esk1_0,esk8_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 2.32/0.89 cnf(c_0_8, plain, (r1(X1,esk24_1(X1))|r1(X1,esk22_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_9, negated_conjecture, (epred1_1(esk8_0)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 2.32/0.89 cnf(c_0_10, plain, (r1(X1,esk11_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_11, plain, (r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 2.32/0.89 cnf(c_0_12, plain, (p2(esk11_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_13, plain, (r1(X1,esk22_1(X1))|~r1(esk24_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_14, plain, (r1(esk24_1(esk8_0),esk11_2(esk8_0,esk24_1(esk8_0)))|r1(esk8_0,esk22_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_9])])).
% 2.32/0.89 cnf(c_0_15, plain, (p2(esk11_2(esk8_0,esk24_1(esk8_0)))|r1(esk8_0,esk22_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_11]), c_0_9])])).
% 2.32/0.89 cnf(c_0_16, negated_conjecture, (r1(X1,esk9_1(X1))|~r1(esk8_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 2.32/0.89 cnf(c_0_17, plain, (r1(esk8_0,esk22_1(esk8_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_14]), c_0_9])]), c_0_15])).
% 2.32/0.89 cnf(c_0_18, plain, (r1(X1,esk14_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_5])).
% 2.32/0.89 cnf(c_0_19, negated_conjecture, (r1(esk22_1(esk8_0),esk9_1(esk22_1(esk8_0)))), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 2.32/0.89 cnf(c_0_20, plain, (r1(X1,esk24_1(X1))|p2(esk22_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_21, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(X1,esk14_3(X2,esk22_1(esk8_0),X1))|~epred1_1(X2)|~p2(esk22_1(esk8_0))|~r1(esk22_1(esk8_0),X1)|~r1(X2,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 2.32/0.89 cnf(c_0_22, plain, (p2(esk22_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_20, c_0_9])).
% 2.32/0.89 cnf(c_0_23, plain, (r1(X1,esk19_2(X2,X1))|r1(X1,esk18_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_24, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(X1,esk14_3(X2,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|~epred1_1(X2)|~r1(esk22_1(esk8_0),X1)|~r1(X2,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 2.32/0.89 cnf(c_0_25, plain, (r1(esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_26, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 2.32/0.89 cnf(c_0_27, negated_conjecture, (~p2(esk9_1(X1))|~r1(esk8_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 2.32/0.89 cnf(c_0_28, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_29, plain, (r1(X1,esk20_3(X2,X3,X1))|r1(X3,esk18_2(X2,X3))|~r1(esk19_2(X2,X3),X1)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_30, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_28]), c_0_17])])).
% 2.32/0.89 cnf(c_0_31, plain, (p2(esk20_3(X1,X2,X3))|r1(X2,esk18_2(X1,X2))|~r1(esk19_2(X1,X2),X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_32, plain, (p2(X5)|~r1(esk14_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_5])).
% 2.32/0.89 cnf(c_0_33, plain, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_30]), c_0_9]), c_0_17])])).
% 2.32/0.89 cnf(c_0_34, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_30]), c_0_9]), c_0_17])])).
% 2.32/0.89 cnf(c_0_35, plain, (p2(X1)|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk22_1(esk8_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_33]), c_0_9]), c_0_17])]), c_0_25]), c_0_22]), c_0_34])).
% 2.32/0.89 cnf(c_0_36, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_35, c_0_19])).
% 2.32/0.89 cnf(c_0_37, plain, (r1(X1,esk17_1(X1))|r1(X2,esk15_3(X1,X3,X2))|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_38, negated_conjecture, (r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_36]), c_0_17])])).
% 2.32/0.89 cnf(c_0_39, plain, (r1(X1,esk17_1(X1))|p2(esk15_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_40, plain, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(X1,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))|r1(X1,esk17_1(X1))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 2.32/0.89 cnf(c_0_41, plain, (p2(esk15_3(X1,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))|r1(X1,esk17_1(X1))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_39, c_0_38])).
% 2.32/0.89 cnf(c_0_42, plain, (r1(X1,esk19_2(X2,X1))|~r1(esk18_2(X2,X1),X3)|~p2(X3)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_43, plain, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_44, plain, (p2(esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_45, plain, (r1(esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_9]), c_0_17])]), c_0_44])).
% 2.32/0.89 cnf(c_0_46, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_24, c_0_45])).
% 2.32/0.89 cnf(c_0_47, plain, (r1(X1,esk20_3(X2,X3,X1))|~r1(esk19_2(X2,X3),X1)|~r1(esk18_2(X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_48, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_46, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_49, plain, (p2(esk20_3(X1,X2,X3))|~r1(esk19_2(X1,X2),X3)|~r1(esk18_2(X1,X2),X4)|~p2(X4)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_50, plain, (r1(X1,esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_43]), c_0_9]), c_0_17])]), c_0_44])).
% 2.32/0.89 cnf(c_0_51, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_48]), c_0_17])])).
% 2.32/0.89 cnf(c_0_52, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_43]), c_0_9]), c_0_17])]), c_0_44])).
% 2.32/0.89 cnf(c_0_53, negated_conjecture, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_50, c_0_51])).
% 2.32/0.89 cnf(c_0_54, negated_conjecture, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_52, c_0_51])).
% 2.32/0.89 cnf(c_0_55, plain, (p2(X1)|r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))|~r1(esk22_1(esk8_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_53]), c_0_9]), c_0_17])]), c_0_45]), c_0_22]), c_0_54])).
% 2.32/0.89 cnf(c_0_56, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk8_0,esk17_1(esk8_0))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_55, c_0_19])).
% 2.32/0.89 cnf(c_0_57, negated_conjecture, (r1(esk8_0,esk24_1(esk8_0))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_56]), c_0_17])])).
% 2.32/0.89 cnf(c_0_58, plain, (r1(X3,esk15_3(X1,X4,X3))|~r1(esk17_1(X1),X2)|~p2(X2)|~r1(X4,X3)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_59, plain, (r1(esk17_1(esk8_0),esk11_2(esk8_0,esk17_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_57]), c_0_9])])).
% 2.32/0.89 cnf(c_0_60, plain, (p2(esk11_2(esk8_0,esk17_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_57]), c_0_9])])).
% 2.32/0.89 cnf(c_0_61, plain, (p2(esk15_3(X1,X3,X4))|~r1(esk17_1(X1),X2)|~p2(X2)|~r1(X3,X4)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_62, plain, (r1(X1,esk15_3(esk8_0,X2,X1))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk8_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_9])]), c_0_60])).
% 2.32/0.89 cnf(c_0_63, plain, (p2(esk15_3(esk8_0,X1,X2))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk8_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_59]), c_0_9])]), c_0_60])).
% 2.32/0.89 cnf(c_0_64, plain, (r1(X1,esk15_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk22_1(esk8_0),X1)), inference(spm,[status(thm)],[c_0_62, c_0_17])).
% 2.32/0.89 cnf(c_0_65, plain, (p2(esk15_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk22_1(esk8_0),X1)), inference(spm,[status(thm)],[c_0_63, c_0_17])).
% 2.32/0.89 cnf(c_0_66, negated_conjecture, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_64, c_0_38])).
% 2.32/0.89 cnf(c_0_67, negated_conjecture, (p2(esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_65, c_0_38])).
% 2.32/0.89 cnf(c_0_68, plain, (r1(esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_66]), c_0_9]), c_0_17])]), c_0_67])).
% 2.32/0.89 cnf(c_0_69, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_24, c_0_68])).
% 2.32/0.89 cnf(c_0_70, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_71, plain, (r1(X1,esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_66]), c_0_9]), c_0_17])]), c_0_67])).
% 2.32/0.89 cnf(c_0_72, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_70]), c_0_17])])).
% 2.32/0.89 cnf(c_0_73, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk24_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_66]), c_0_9]), c_0_17])]), c_0_67])).
% 2.32/0.89 cnf(c_0_74, negated_conjecture, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_71, c_0_72])).
% 2.32/0.89 cnf(c_0_75, negated_conjecture, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_73, c_0_72])).
% 2.32/0.89 cnf(c_0_76, plain, (p2(X1)|r1(esk8_0,esk24_1(esk8_0))|~r1(esk22_1(esk8_0),X1)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_74]), c_0_9]), c_0_17])]), c_0_68]), c_0_22]), c_0_75])).
% 2.32/0.89 cnf(c_0_77, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk8_0,esk24_1(esk8_0))), inference(spm,[status(thm)],[c_0_76, c_0_19])).
% 2.32/0.89 cnf(c_0_78, negated_conjecture, (r1(esk8_0,esk24_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_77]), c_0_17])])).
% 2.32/0.89 cnf(c_0_79, plain, (p2(esk22_1(X1))|~r1(esk24_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 2.32/0.89 cnf(c_0_80, plain, (r1(esk24_1(esk8_0),esk11_2(esk8_0,esk24_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_78]), c_0_9])])).
% 2.32/0.89 cnf(c_0_81, plain, (p2(esk11_2(esk8_0,esk24_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_78]), c_0_9])])).
% 2.32/0.89 cnf(c_0_82, plain, (p2(esk22_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_80]), c_0_9]), c_0_81])])).
% 2.32/0.89 cnf(c_0_83, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(X1,esk14_3(X2,esk22_1(esk8_0),X1))|~epred1_1(X2)|~r1(esk22_1(esk8_0),X1)|~r1(X2,esk22_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_82])])).
% 2.32/0.89 cnf(c_0_84, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_83, c_0_25])).
% 2.32/0.89 cnf(c_0_85, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_86, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_85]), c_0_17])])).
% 2.32/0.89 cnf(c_0_87, plain, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_29, c_0_86]), c_0_9]), c_0_17])])).
% 2.32/0.89 cnf(c_0_88, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_86]), c_0_9]), c_0_17])])).
% 2.32/0.89 cnf(c_0_89, plain, (p2(X1)|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))|~r1(esk22_1(esk8_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_32, c_0_87]), c_0_9]), c_0_82]), c_0_17])]), c_0_25]), c_0_88])).
% 2.32/0.89 cnf(c_0_90, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(spm,[status(thm)],[c_0_89, c_0_19])).
% 2.32/0.89 cnf(c_0_91, negated_conjecture, (r1(esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_90]), c_0_17])])).
% 2.32/0.89 cnf(c_0_92, plain, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(X1,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(X1,esk17_1(X1))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_37, c_0_91])).
% 2.32/0.89 cnf(c_0_93, plain, (p2(esk15_3(X1,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(X1,esk17_1(X1))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_39, c_0_91])).
% 2.32/0.89 cnf(c_0_94, plain, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_95, plain, (p2(esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_96, plain, (r1(esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))|r1(esk8_0,esk17_1(esk8_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_94]), c_0_9]), c_0_17])]), c_0_95])).
% 2.32/0.89 cnf(c_0_97, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_83, c_0_96])).
% 2.32/0.89 cnf(c_0_98, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_99, plain, (r1(X1,esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk17_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_94]), c_0_9]), c_0_17])]), c_0_95])).
% 2.32/0.89 cnf(c_0_100, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_98]), c_0_17])])).
% 2.32/0.89 cnf(c_0_101, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),X1))|r1(esk8_0,esk17_1(esk8_0))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_94]), c_0_9]), c_0_17])]), c_0_95])).
% 2.32/0.89 cnf(c_0_102, negated_conjecture, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk17_1(esk8_0))), inference(spm,[status(thm)],[c_0_99, c_0_100])).
% 2.32/0.89 cnf(c_0_103, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))|r1(esk8_0,esk17_1(esk8_0))), inference(spm,[status(thm)],[c_0_101, c_0_100])).
% 2.32/0.89 cnf(c_0_104, plain, (p2(X1)|r1(esk8_0,esk17_1(esk8_0))|~r1(esk22_1(esk8_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_32, c_0_102]), c_0_9]), c_0_82]), c_0_17])]), c_0_96]), c_0_103])).
% 2.32/0.89 cnf(c_0_105, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk8_0,esk17_1(esk8_0))), inference(spm,[status(thm)],[c_0_104, c_0_19])).
% 2.32/0.89 cnf(c_0_106, negated_conjecture, (r1(esk8_0,esk17_1(esk8_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_105]), c_0_17])])).
% 2.32/0.89 cnf(c_0_107, plain, (r1(esk17_1(esk8_0),esk11_2(esk8_0,esk17_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_106]), c_0_9])])).
% 2.32/0.89 cnf(c_0_108, plain, (p2(esk11_2(esk8_0,esk17_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_106]), c_0_9])])).
% 2.32/0.89 cnf(c_0_109, plain, (r1(X1,esk15_3(esk8_0,X2,X1))|~r1(esk8_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_107]), c_0_9]), c_0_108])])).
% 2.32/0.89 cnf(c_0_110, plain, (p2(esk15_3(esk8_0,X1,X2))|~r1(esk8_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_107]), c_0_9]), c_0_108])])).
% 2.32/0.89 cnf(c_0_111, plain, (r1(X1,esk15_3(esk8_0,esk22_1(esk8_0),X1))|~r1(esk22_1(esk8_0),X1)), inference(spm,[status(thm)],[c_0_109, c_0_17])).
% 2.32/0.89 cnf(c_0_112, plain, (p2(esk15_3(esk8_0,esk22_1(esk8_0),X1))|~r1(esk22_1(esk8_0),X1)), inference(spm,[status(thm)],[c_0_110, c_0_17])).
% 2.32/0.89 cnf(c_0_113, negated_conjecture, (r1(esk18_2(esk8_0,esk22_1(esk8_0)),esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))), inference(spm,[status(thm)],[c_0_111, c_0_91])).
% 2.32/0.89 cnf(c_0_114, negated_conjecture, (p2(esk15_3(esk8_0,esk22_1(esk8_0),esk18_2(esk8_0,esk22_1(esk8_0))))), inference(spm,[status(thm)],[c_0_112, c_0_91])).
% 2.32/0.89 cnf(c_0_115, plain, (r1(esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_113]), c_0_9]), c_0_114]), c_0_17])])).
% 2.32/0.89 cnf(c_0_116, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(X1,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))|~epred1_1(X1)|~r1(X1,esk22_1(esk8_0))), inference(spm,[status(thm)],[c_0_83, c_0_115])).
% 2.32/0.89 cnf(c_0_117, plain, (p2(esk9_1(esk22_1(esk8_0)))|r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_17]), c_0_9])])).
% 2.32/0.89 cnf(c_0_118, plain, (r1(X1,esk20_3(esk8_0,esk22_1(esk8_0),X1))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_113]), c_0_9]), c_0_114]), c_0_17])])).
% 2.32/0.89 cnf(c_0_119, negated_conjecture, (r1(esk19_2(esk8_0,esk22_1(esk8_0)),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_117]), c_0_17])])).
% 2.32/0.89 cnf(c_0_120, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),X1))|~r1(esk19_2(esk8_0,esk22_1(esk8_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_113]), c_0_9]), c_0_114]), c_0_17])])).
% 2.32/0.89 cnf(c_0_121, plain, (r1(esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0))),esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))), inference(spm,[status(thm)],[c_0_118, c_0_119])).
% 2.32/0.89 cnf(c_0_122, plain, (p2(esk20_3(esk8_0,esk22_1(esk8_0),esk14_3(esk8_0,esk22_1(esk8_0),esk19_2(esk8_0,esk22_1(esk8_0)))))), inference(spm,[status(thm)],[c_0_120, c_0_119])).
% 2.32/0.89 cnf(c_0_123, plain, (p2(X1)|~r1(esk22_1(esk8_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_121]), c_0_9]), c_0_122]), c_0_82]), c_0_115]), c_0_17])])).
% 2.32/0.89 cnf(c_0_124, negated_conjecture, (p2(esk9_1(esk22_1(esk8_0)))), inference(spm,[status(thm)],[c_0_123, c_0_19])).
% 2.32/0.89 cnf(c_0_125, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_27, c_0_124]), c_0_17])]), ['proof']).
% 2.32/0.89 % SZS output end Proof
% 2.32/0.89 % User time : 0.352 s
% 2.32/0.89 % System time : 0.010 s
% 2.32/0.89 % Total time : 0.362 s
% 2.32/0.89 % User time : 0.353 s
% 2.32/0.89 % System time : 0.014 s
% 2.32/0.89 % Total time : 0.367 s
% 2.32/0.89
%------------------------------------------------------------------------------