%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL640+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n003.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:16 AM UTC 2026
% Result : Theorem 11.89s 2.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL640+1.015 : 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 : n003.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 18:06:06 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.46 start to proof:theBenchmark.p
% 11.89/2.28 % Version : CSI_E---1.1
% 11.89/2.28 % Problem : theBenchmark.p
% 11.89/2.28 % Proof found!
% 11.89/2.28 % SZS status Theorem for theBenchmark.p
% 11.89/2.28 % SZS output start Proof
% 11.89/2.28 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((p1(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))|p1(X2)))|~(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))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((p1(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))|p1(X2)))|~(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))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((p1(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))|p1(X2)))|~(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))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((((![X2]:((~(r1(X1,X2))|p1(X2)))|~(p1(X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2)))|~(p1(X1)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)))|~(p1(X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)))|~(p1(X2))))|~((![X2]:((~(r1(X1,X2))|p1(X2)))|~(p1(X1)))))))))))&(p1(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))|p1(X2)))|~(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))|p1(X1)|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)))|~(p1(X2)))))))))|~(![X2]:((~(r1(X1,X2))|p1(X2)|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2)))|~(p1(X1)))))))))))))))))))))))))))|~((((((((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2)))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|~(![X2]:((~(r1(X1,X2))|p1(X2)|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2)))|~(p1(X1)))))))))))))))))))))))))&![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|((p1(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))|p1(X2)))|~(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))|![X2]:((~(r1(X1,X2))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|![X1]:((~(r1(X2,X1))|((p1(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))|p1(X2)))|~(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))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![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))|((p1(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))|p1(X2)))|~(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))|((p1(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))|p1(X1)))|~(p1(X2)))))))))&![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)))))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 11.89/2.28 fof(c_0_1, plain, ![X1]:((epred1_1(X1)<=>((((![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2)))|~((![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))))))&(p1(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)|p1(X2)))|~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)|p1(X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2))))))))|~(![X2]:((~r1(X1,X2)|p1(X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))))))), introduced(definition)).
% 11.89/2.28 fof(c_0_2, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|((p1(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)|p1(X2)))|~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)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|((p1(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)|p1(X2)))|~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)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|((p1(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)|p1(X2)))|~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)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|epred1_1(X1))))))))))))))))))|~((((((((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![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))))))|~(![X2]:((~r1(X1,X2)|p1(X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))))))))))))))))))))&![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|((p1(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)|p1(X2)))|~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)|![X2]:((~r1(X1,X2)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|![X1]:((~r1(X2,X1)|((p1(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)|p1(X2)))|~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)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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)|((p1(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)|p1(X2)))|~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)|((p1(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)|p1(X1)))|~p1(X2))))))))&![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(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1])).
% 11.89/2.28 fof(c_0_3, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X21, X22, X23, X24, X25, X27, X28, X29, X30, X31, X32, X33, X34, X35, X36, X37, X38, X39, X40, X43, X44, X45, X46, X47, X49, X50, X51, X52, X53, X54, X55, X56, X57, X58, X59, X60, X61, X64, X65, X66, X67, X68, X70, X71, X72, X73, X74, X75, X76, X77, X78, X79, X80, X81, X84, X85, X86, X87, X88, X90, X91, X92, X93, X94, X95, X96, X97, X98, X99, X100, X103, X104, X105, X106, X107, X109, X110, X111, X112, X113, X114, X115, X116, X117, X118, X121, X122, X123, X124, X125, X127, X128, X129, X130, X131, X132, X133, X134, X145, X146, X149, X150, X151, X152, X153, X154, X155, X156, X159, X160, X161, X162, X163, X165, X166, X167, X168, X169, X170, X171, X174, X175, X176, X177, X178, X180, X181, X182, X183, X184, X185, X188, X189, X190, X191, X192, X194, X195, X196, X197, X198, X201, X202, X203, X204, X205, X207, X208, X209, X210, X213, X214, X215, X216, X217, X219, X220, X221, X224, X225, X226, X227, X228, X230, X231, X234, X235, X236, X237, X238]:(((((((((((((r1(X17,esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17))|(r1(X18,esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))&(~p1(esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17))|(r1(X18,esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4)))&(~r1(esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),X21)|(~r1(X21,X22)|p1(X22))|~p1(X21)|(r1(X18,esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4)))&(((r1(X17,esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17))|(~p1(esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))&(~p1(esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17))|(~p1(esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4)))&(~r1(esk3_14(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17),X21)|(~r1(X21,X22)|p1(X22))|~p1(X21)|(~p1(esk2_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18))|~r1(X17,X18)|p1(X17))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))))&((r1(X23,esk4_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X23))|(~r1(X17,X23)|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25))))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))&(~p1(esk4_15(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X23))|(~r1(X17,X23)|(~r1(X23,X24)|(~r1(X24,X25)|p1(X25))))|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))))&(((((r1(X39,esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|(r1(X40,esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27))&(~p1(esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|(r1(X40,esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27)))&(~r1(esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39),X43)|(~r1(X43,X44)|p1(X44))|~p1(X43)|(r1(X40,esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27)))&(((r1(X39,esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|(~p1(esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27))&(~p1(esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|(~p1(esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27)))&(~r1(esk6_13(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39),X43)|(~r1(X43,X44)|p1(X44))|~p1(X43)|(~p1(esk5_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40))|~r1(X39,X40)|p1(X39))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27))))&((r1(X45,esk7_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X45))|(~r1(X39,X45)|(~r1(X45,X46)|(~r1(X46,X47)|p1(X47))))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27))&(~p1(esk7_14(X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X45))|(~r1(X39,X45)|(~r1(X45,X46)|(~r1(X46,X47)|p1(X47))))|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(X27,X28)|~r1(esk1_0,X27)))))&(((((r1(X60,esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60))|(r1(X61,esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))&(~p1(esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60))|(r1(X61,esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49)))&(~r1(esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60),X64)|(~r1(X64,X65)|p1(X65))|~p1(X64)|(r1(X61,esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49)))&(((r1(X60,esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60))|(~p1(esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))&(~p1(esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60))|(~p1(esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49)))&(~r1(esk9_12(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60),X64)|(~r1(X64,X65)|p1(X65))|~p1(X64)|(~p1(esk8_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X61))|~r1(X60,X61)|p1(X60))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))))&((r1(X66,esk10_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X66))|(~r1(X60,X66)|(~r1(X66,X67)|(~r1(X67,X68)|p1(X68))))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))&(~p1(esk10_13(X49,X50,X51,X52,X53,X54,X55,X56,X57,X58,X59,X60,X66))|(~r1(X60,X66)|(~r1(X66,X67)|(~r1(X67,X68)|p1(X68))))|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(X53,X54)|~r1(X52,X53)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49)))))&(((((r1(X80,esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80))|(r1(X81,esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70))&(~p1(esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80))|(r1(X81,esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70)))&(~r1(esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80),X84)|(~r1(X84,X85)|p1(X85))|~p1(X84)|(r1(X81,esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70)))&(((r1(X80,esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80))|(~p1(esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70))&(~p1(esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80))|(~p1(esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70)))&(~r1(esk12_11(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80),X84)|(~r1(X84,X85)|p1(X85))|~p1(X84)|(~p1(esk11_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X81))|~r1(X80,X81)|p1(X80))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70))))&((r1(X86,esk13_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X86))|(~r1(X80,X86)|(~r1(X86,X87)|(~r1(X87,X88)|p1(X88))))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70))&(~p1(esk13_12(X70,X71,X72,X73,X74,X75,X76,X77,X78,X79,X80,X86))|(~r1(X80,X86)|(~r1(X86,X87)|(~r1(X87,X88)|p1(X88))))|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(X75,X76)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(X71,X72)|~r1(X70,X71)|~r1(esk1_0,X70)))))&(((((r1(X99,esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99))|(r1(X100,esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))&(~p1(esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99))|(r1(X100,esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90)))&(~r1(esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99),X103)|(~r1(X103,X104)|p1(X104))|~p1(X103)|(r1(X100,esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90)))&(((r1(X99,esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99))|(~p1(esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))&(~p1(esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99))|(~p1(esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90)))&(~r1(esk15_10(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99),X103)|(~r1(X103,X104)|p1(X104))|~p1(X103)|(~p1(esk14_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X100))|~r1(X99,X100)|p1(X99))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))))&((r1(X105,esk16_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X105))|(~r1(X99,X105)|(~r1(X105,X106)|(~r1(X106,X107)|p1(X107))))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))&(~p1(esk16_11(X90,X91,X92,X93,X94,X95,X96,X97,X98,X99,X105))|(~r1(X99,X105)|(~r1(X105,X106)|(~r1(X106,X107)|p1(X107))))|~r1(X98,X99)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90)))))&(((((r1(X117,esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117))|(r1(X118,esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))&(~p1(esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117))|(r1(X118,esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109)))&(~r1(esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117),X121)|(~r1(X121,X122)|p1(X122))|~p1(X121)|(r1(X118,esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109)))&(((r1(X117,esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117))|(~p1(esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))&(~p1(esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117))|(~p1(esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109)))&(~r1(esk18_9(X109,X110,X111,X112,X113,X114,X115,X116,X117),X121)|(~r1(X121,X122)|p1(X122))|~p1(X121)|(~p1(esk17_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X118))|~r1(X117,X118)|p1(X117))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))))&((r1(X123,esk19_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X123))|(~r1(X117,X123)|(~r1(X123,X124)|(~r1(X124,X125)|p1(X125))))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))&(~p1(esk19_10(X109,X110,X111,X112,X113,X114,X115,X116,X117,X123))|(~r1(X117,X123)|(~r1(X123,X124)|(~r1(X124,X125)|p1(X125))))|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109)))))&(~r1(esk1_0,X127)|(~r1(X127,X128)|(~r1(X128,X129)|(~r1(X129,X130)|(~r1(X130,X131)|(~r1(X131,X132)|(~r1(X132,X133)|(~r1(X133,X134)|epred1_1(X134))))))))))&((((((((r1(esk1_0,esk20_0)&(r1(esk20_0,esk21_0)&(r1(esk21_0,esk22_0)&(r1(esk22_0,esk23_0)&(r1(esk23_0,esk24_0)&(r1(esk24_0,esk25_0)&(r1(esk25_0,esk26_0)&(((r1(esk26_0,esk27_0)&(r1(esk27_0,esk28_0)&~p1(esk28_0)))&(r1(esk27_0,esk29_0)&(~r1(esk29_0,X145)|p1(X145))))&(((r1(X146,esk30_1(X146))|(~r1(esk27_0,X146)|p1(X146)))&((r1(esk30_1(X146),esk31_1(X146))|(~r1(esk27_0,X146)|p1(X146)))&(~p1(esk31_1(X146))|(~r1(esk27_0,X146)|p1(X146)))))&(p1(esk30_1(X146))|(~r1(esk27_0,X146)|p1(X146))))))))))))&(((((r1(X155,esk33_7(X149,X150,X151,X152,X153,X154,X155))|(r1(X156,esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149))&(~p1(esk33_7(X149,X150,X151,X152,X153,X154,X155))|(r1(X156,esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149)))&(~r1(esk33_7(X149,X150,X151,X152,X153,X154,X155),X159)|(~r1(X159,X160)|p1(X160))|~p1(X159)|(r1(X156,esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149)))&(((r1(X155,esk33_7(X149,X150,X151,X152,X153,X154,X155))|(~p1(esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149))&(~p1(esk33_7(X149,X150,X151,X152,X153,X154,X155))|(~p1(esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149)))&(~r1(esk33_7(X149,X150,X151,X152,X153,X154,X155),X159)|(~r1(X159,X160)|p1(X160))|~p1(X159)|(~p1(esk32_8(X149,X150,X151,X152,X153,X154,X155,X156))|~r1(X155,X156)|p1(X155))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149))))&((r1(X161,esk34_8(X149,X150,X151,X152,X153,X154,X155,X161))|(~r1(X155,X161)|(~r1(X161,X162)|(~r1(X162,X163)|p1(X163))))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149))&(~p1(esk34_8(X149,X150,X151,X152,X153,X154,X155,X161))|(~r1(X155,X161)|(~r1(X161,X162)|(~r1(X162,X163)|p1(X163))))|~r1(X154,X155)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(esk1_0,X149)))))&(((((r1(X170,esk36_6(X165,X166,X167,X168,X169,X170))|(r1(X171,esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165))&(~p1(esk36_6(X165,X166,X167,X168,X169,X170))|(r1(X171,esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165)))&(~r1(esk36_6(X165,X166,X167,X168,X169,X170),X174)|(~r1(X174,X175)|p1(X175))|~p1(X174)|(r1(X171,esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165)))&(((r1(X170,esk36_6(X165,X166,X167,X168,X169,X170))|(~p1(esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165))&(~p1(esk36_6(X165,X166,X167,X168,X169,X170))|(~p1(esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165)))&(~r1(esk36_6(X165,X166,X167,X168,X169,X170),X174)|(~r1(X174,X175)|p1(X175))|~p1(X174)|(~p1(esk35_7(X165,X166,X167,X168,X169,X170,X171))|~r1(X170,X171)|p1(X170))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165))))&((r1(X176,esk37_7(X165,X166,X167,X168,X169,X170,X176))|(~r1(X170,X176)|(~r1(X176,X177)|(~r1(X177,X178)|p1(X178))))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165))&(~p1(esk37_7(X165,X166,X167,X168,X169,X170,X176))|(~r1(X170,X176)|(~r1(X176,X177)|(~r1(X177,X178)|p1(X178))))|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(X166,X167)|~r1(X165,X166)|~r1(esk1_0,X165)))))&(((((r1(X184,esk39_5(X180,X181,X182,X183,X184))|(r1(X185,esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))&(~p1(esk39_5(X180,X181,X182,X183,X184))|(r1(X185,esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180)))&(~r1(esk39_5(X180,X181,X182,X183,X184),X188)|(~r1(X188,X189)|p1(X189))|~p1(X188)|(r1(X185,esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180)))&(((r1(X184,esk39_5(X180,X181,X182,X183,X184))|(~p1(esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))&(~p1(esk39_5(X180,X181,X182,X183,X184))|(~p1(esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180)))&(~r1(esk39_5(X180,X181,X182,X183,X184),X188)|(~r1(X188,X189)|p1(X189))|~p1(X188)|(~p1(esk38_6(X180,X181,X182,X183,X184,X185))|~r1(X184,X185)|p1(X184))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))))&((r1(X190,esk40_6(X180,X181,X182,X183,X184,X190))|(~r1(X184,X190)|(~r1(X190,X191)|(~r1(X191,X192)|p1(X192))))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))&(~p1(esk40_6(X180,X181,X182,X183,X184,X190))|(~r1(X184,X190)|(~r1(X190,X191)|(~r1(X191,X192)|p1(X192))))|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180)))))&(((((r1(X197,esk42_4(X194,X195,X196,X197))|(r1(X198,esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))&(~p1(esk42_4(X194,X195,X196,X197))|(r1(X198,esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194)))&(~r1(esk42_4(X194,X195,X196,X197),X201)|(~r1(X201,X202)|p1(X202))|~p1(X201)|(r1(X198,esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194)))&(((r1(X197,esk42_4(X194,X195,X196,X197))|(~p1(esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))&(~p1(esk42_4(X194,X195,X196,X197))|(~p1(esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194)))&(~r1(esk42_4(X194,X195,X196,X197),X201)|(~r1(X201,X202)|p1(X202))|~p1(X201)|(~p1(esk41_5(X194,X195,X196,X197,X198))|~r1(X197,X198)|p1(X197))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))))&((r1(X203,esk43_5(X194,X195,X196,X197,X203))|(~r1(X197,X203)|(~r1(X203,X204)|(~r1(X204,X205)|p1(X205))))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))&(~p1(esk43_5(X194,X195,X196,X197,X203))|(~r1(X197,X203)|(~r1(X203,X204)|(~r1(X204,X205)|p1(X205))))|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194)))))&(((((r1(X209,esk45_3(X207,X208,X209))|(r1(X210,esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207))&(~p1(esk45_3(X207,X208,X209))|(r1(X210,esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207)))&(~r1(esk45_3(X207,X208,X209),X213)|(~r1(X213,X214)|p1(X214))|~p1(X213)|(r1(X210,esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207)))&(((r1(X209,esk45_3(X207,X208,X209))|(~p1(esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207))&(~p1(esk45_3(X207,X208,X209))|(~p1(esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207)))&(~r1(esk45_3(X207,X208,X209),X213)|(~r1(X213,X214)|p1(X214))|~p1(X213)|(~p1(esk44_4(X207,X208,X209,X210))|~r1(X209,X210)|p1(X209))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207))))&((r1(X215,esk46_4(X207,X208,X209,X215))|(~r1(X209,X215)|(~r1(X215,X216)|(~r1(X216,X217)|p1(X217))))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207))&(~p1(esk46_4(X207,X208,X209,X215))|(~r1(X209,X215)|(~r1(X215,X216)|(~r1(X216,X217)|p1(X217))))|~r1(X208,X209)|~r1(X207,X208)|~r1(esk1_0,X207)))))&(((((r1(X220,esk48_2(X219,X220))|(r1(X221,esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219))&(~p1(esk48_2(X219,X220))|(r1(X221,esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219)))&(~r1(esk48_2(X219,X220),X224)|(~r1(X224,X225)|p1(X225))|~p1(X224)|(r1(X221,esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219)))&(((r1(X220,esk48_2(X219,X220))|(~p1(esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219))&(~p1(esk48_2(X219,X220))|(~p1(esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219)))&(~r1(esk48_2(X219,X220),X224)|(~r1(X224,X225)|p1(X225))|~p1(X224)|(~p1(esk47_3(X219,X220,X221))|~r1(X220,X221)|p1(X220))|~r1(X219,X220)|~r1(esk1_0,X219))))&((r1(X226,esk49_3(X219,X220,X226))|(~r1(X220,X226)|(~r1(X226,X227)|(~r1(X227,X228)|p1(X228))))|~r1(X219,X220)|~r1(esk1_0,X219))&(~p1(esk49_3(X219,X220,X226))|(~r1(X220,X226)|(~r1(X226,X227)|(~r1(X227,X228)|p1(X228))))|~r1(X219,X220)|~r1(esk1_0,X219)))))&(((((r1(X230,esk51_1(X230))|(r1(X231,esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230))&(~p1(esk51_1(X230))|(r1(X231,esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230)))&(~r1(esk51_1(X230),X234)|(~r1(X234,X235)|p1(X235))|~p1(X234)|(r1(X231,esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230)))&(((r1(X230,esk51_1(X230))|(~p1(esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230))&(~p1(esk51_1(X230))|(~p1(esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230)))&(~r1(esk51_1(X230),X234)|(~r1(X234,X235)|p1(X235))|~p1(X234)|(~p1(esk50_2(X230,X231))|~r1(X230,X231)|p1(X230))|~r1(esk1_0,X230))))&((r1(X236,esk52_2(X230,X236))|(~r1(X230,X236)|(~r1(X236,X237)|(~r1(X237,X238)|p1(X238))))|~r1(esk1_0,X230))&(~p1(esk52_2(X230,X236))|(~r1(X230,X236)|(~r1(X236,X237)|(~r1(X237,X238)|p1(X238))))|~r1(esk1_0,X230))))))), 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])])])])])])).
% 11.89/2.28 cnf(c_0_4, negated_conjecture, (epred1_1(X8)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)|~r1(X5,X6)|~r1(X6,X7)|~r1(X7,X8)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_5, negated_conjecture, (r1(esk1_0,esk20_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_6, negated_conjecture, (epred1_1(X1)|~r1(esk20_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X7,X6)|~r1(X2,X7)), inference(spm,[status(thm)],[c_0_4, c_0_5])).
% 11.89/2.28 cnf(c_0_7, negated_conjecture, (r1(esk20_0,esk21_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_8, negated_conjecture, (epred1_1(X1)|~r1(esk21_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X6,X5)|~r1(X2,X6)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 11.89/2.28 cnf(c_0_9, negated_conjecture, (r1(esk21_0,esk22_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_10, negated_conjecture, (epred1_1(X1)|~r1(esk22_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~r1(X2,X5)), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 11.89/2.28 cnf(c_0_11, negated_conjecture, (r1(esk22_0,esk23_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_12, negated_conjecture, (epred1_1(X1)|~r1(esk23_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 11.89/2.28 cnf(c_0_13, negated_conjecture, (r1(esk23_0,esk24_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 fof(c_0_14, plain, ![X1]:((epred1_1(X1)=>((((![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2)))|~((![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))))))&(p1(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)|p1(X2)))|~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)|p1(X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)))|~p1(X2))))))))|~(![X2]:((~r1(X1,X2)|p1(X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2)))|~p1(X1))))))))))), inference(split_equiv,[status(thm)],[c_0_1])).
% 11.89/2.28 cnf(c_0_15, negated_conjecture, (epred1_1(X1)|~r1(esk24_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 11.89/2.28 cnf(c_0_16, negated_conjecture, (r1(esk24_0,esk25_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 fof(c_0_17, plain, ![X240, X241, X242, X247, X248, X249, X251, X254, X255, X256, X257, X258, X260, X261, X265, X266]:((((((((((r1(X240,esk55_1(X240))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&((r1(esk55_1(X240),esk56_1(X240))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk56_1(X240))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&(p1(esk55_1(X240))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(((r1(X247,esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(p1(X247)|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(X242,esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&(((((r1(X240,esk55_1(X240))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&((r1(esk55_1(X240),esk56_1(X240))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk56_1(X240))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&(p1(esk55_1(X240))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(((r1(X247,esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(p1(X247)|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(r1(esk53_2(X240,X242),esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&((((r1(X240,esk55_1(X240))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&((r1(esk55_1(X240),esk56_1(X240))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk56_1(X240))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&(p1(esk55_1(X240))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(((r1(X247,esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(p1(X247)|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(~p1(esk54_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))))&((((r1(X240,esk55_1(X240))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&((r1(esk55_1(X240),esk56_1(X240))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk56_1(X240))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))))&(p1(esk55_1(X240))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(((r1(X247,esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240))&(~p1(esk57_2(X240,X247))|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))&(p1(X247)|(~r1(esk55_1(X240),X247)|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249))|~p1(X248)))|(p1(esk53_2(X240,X242))|~r1(X240,X242)|(~r1(X240,X241)|p1(X241)|~p1(X240)))|~epred1_1(X240)))))&((((r1(X240,esk59_1(X240))|(r1(X251,esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240))&(~p1(esk59_1(X240))|(r1(X251,esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240)))&(~r1(esk59_1(X240),X254)|(~r1(X254,X255)|p1(X255))|~p1(X254)|(r1(X251,esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240)))&(((r1(X240,esk59_1(X240))|(~p1(esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240))&(~p1(esk59_1(X240))|(~p1(esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240)))&(~r1(esk59_1(X240),X254)|(~r1(X254,X255)|p1(X255))|~p1(X254)|(~p1(esk58_2(X240,X251))|~r1(X240,X251)|p1(X240))|~epred1_1(X240)))))&((r1(X256,esk60_2(X240,X256))|(~r1(X240,X256)|(~r1(X256,X257)|(~r1(X257,X258)|p1(X258))))|~epred1_1(X240))&(~p1(esk60_2(X240,X256))|(~r1(X240,X256)|(~r1(X256,X257)|(~r1(X257,X258)|p1(X258))))|~epred1_1(X240))))&(((((r1(X240,esk63_1(X240))|(r1(X261,esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240))&(~p1(esk63_1(X240))|(r1(X261,esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&(~r1(esk63_1(X240),X265)|(~r1(X265,X266)|p1(X266))|~p1(X265)|(r1(X261,esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&((((r1(X240,esk63_1(X240))|(r1(esk61_3(X240,X260,X261),esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240))&(~p1(esk63_1(X240))|(r1(esk61_3(X240,X260,X261),esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&(~r1(esk63_1(X240),X265)|(~r1(X265,X266)|p1(X266))|~p1(X265)|(r1(esk61_3(X240,X260,X261),esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&(((r1(X240,esk63_1(X240))|(~p1(esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240))&(~p1(esk63_1(X240))|(~p1(esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&(~r1(esk63_1(X240),X265)|(~r1(X265,X266)|p1(X266))|~p1(X265)|(~p1(esk62_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))))&(((r1(X240,esk63_1(X240))|(p1(esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240))&(~p1(esk63_1(X240))|(p1(esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))&(~r1(esk63_1(X240),X265)|(~r1(X265,X266)|p1(X266))|~p1(X265)|(p1(esk61_3(X240,X260,X261))|(~r1(X260,X261)|p1(X261))|~r1(X240,X260))|~epred1_1(X240)))))), 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])])])])])])).
% 11.89/2.28 cnf(c_0_18, negated_conjecture, (epred1_1(X1)|~r1(esk25_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 11.89/2.28 cnf(c_0_19, negated_conjecture, (r1(esk25_0,esk26_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_20, plain, (r1(X1,esk59_1(X1))|r1(X2,esk58_2(X1,X2))|p1(X1)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_21, negated_conjecture, (r1(esk27_0,esk29_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_22, negated_conjecture, (epred1_1(X1)|~r1(esk26_0,X1)), inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 11.89/2.28 cnf(c_0_23, negated_conjecture, (r1(esk26_0,esk27_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_24, negated_conjecture, (p1(esk27_0)|r1(esk29_0,esk58_2(esk27_0,esk29_0))|r1(esk27_0,esk59_1(esk27_0))|~epred1_1(esk27_0)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 11.89/2.28 cnf(c_0_25, negated_conjecture, (epred1_1(esk27_0)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 11.89/2.28 cnf(c_0_26, negated_conjecture, (p1(X1)|~r1(esk29_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_27, negated_conjecture, (p1(esk27_0)|r1(esk29_0,esk58_2(esk27_0,esk29_0))|r1(esk27_0,esk59_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 11.89/2.28 cnf(c_0_28, plain, (r1(X1,esk59_1(X1))|p1(X1)|~p1(esk58_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_29, negated_conjecture, (p1(esk58_2(esk27_0,esk29_0))|p1(esk27_0)|r1(esk27_0,esk59_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 11.89/2.28 cnf(c_0_30, negated_conjecture, (r1(X1,esk30_1(X1))|p1(X1)|~r1(esk27_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_31, plain, (p1(esk27_0)|r1(esk27_0,esk59_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28, c_0_29]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_32, negated_conjecture, (p1(esk30_1(X1))|p1(X1)|~r1(esk27_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_33, plain, (p1(X3)|r1(X4,esk58_2(X1,X4))|p1(X1)|~r1(esk59_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_34, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|r1(esk59_1(esk27_0),esk30_1(esk59_1(esk27_0)))), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 11.89/2.28 cnf(c_0_35, negated_conjecture, (p1(esk30_1(esk59_1(esk27_0)))|p1(esk59_1(esk27_0))|p1(esk27_0)), inference(spm,[status(thm)],[c_0_32, c_0_31])).
% 11.89/2.28 cnf(c_0_36, negated_conjecture, (r1(esk30_1(X1),esk31_1(X1))|p1(X1)|~r1(esk27_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_37, negated_conjecture, (p1(X1)|~p1(esk31_1(X1))|~r1(esk27_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_38, plain, (p1(esk59_1(esk27_0))|p1(esk27_0)|p1(X1)|r1(X2,esk58_2(esk27_0,X2))|~r1(esk30_1(esk59_1(esk27_0)),X1)|~r1(esk27_0,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_34]), c_0_25])]), c_0_35])).
% 11.89/2.28 cnf(c_0_39, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|r1(esk30_1(esk59_1(esk27_0)),esk31_1(esk59_1(esk27_0)))), inference(spm,[status(thm)],[c_0_36, c_0_31])).
% 11.89/2.28 cnf(c_0_40, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|~p1(esk31_1(esk59_1(esk27_0)))), inference(spm,[status(thm)],[c_0_37, c_0_31])).
% 11.89/2.28 cnf(c_0_41, plain, (p1(X3)|p1(X1)|~r1(esk59_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~p1(esk58_2(X1,X4))|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_42, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|r1(X1,esk58_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])).
% 11.89/2.28 cnf(c_0_43, plain, (p1(esk59_1(esk27_0))|p1(esk27_0)|p1(X1)|~p1(esk58_2(esk27_0,X2))|~r1(esk30_1(esk59_1(esk27_0)),X1)|~r1(esk27_0,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_34]), c_0_25])]), c_0_35])).
% 11.89/2.28 cnf(c_0_44, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|r1(esk29_0,esk58_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_42, c_0_21])).
% 11.89/2.28 cnf(c_0_45, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)|~p1(esk58_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_39]), c_0_40])).
% 11.89/2.28 cnf(c_0_46, negated_conjecture, (p1(esk58_2(esk27_0,esk29_0))|p1(esk59_1(esk27_0))|p1(esk27_0)), inference(spm,[status(thm)],[c_0_26, c_0_44])).
% 11.89/2.28 cnf(c_0_47, plain, (r1(X2,esk58_2(X1,X2))|p1(X1)|~p1(esk59_1(X1))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_48, negated_conjecture, (p1(esk59_1(esk27_0))|p1(esk27_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_21])])).
% 11.89/2.28 cnf(c_0_49, plain, (p1(esk27_0)|r1(X1,esk58_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_25])])).
% 11.89/2.28 cnf(c_0_50, negated_conjecture, (p1(esk27_0)|r1(esk29_0,esk58_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_49, c_0_21])).
% 11.89/2.28 cnf(c_0_51, plain, (r1(X1,esk55_1(X1))|r1(esk53_2(X1,X2),esk54_2(X1,X2))|p1(X3)|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_52, negated_conjecture, (r1(esk27_0,esk28_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_53, negated_conjecture, (~p1(esk28_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 11.89/2.28 cnf(c_0_54, plain, (p1(X1)|~p1(esk59_1(X1))|~p1(esk58_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_55, negated_conjecture, (p1(esk58_2(esk27_0,esk29_0))|p1(esk27_0)), inference(spm,[status(thm)],[c_0_26, c_0_50])).
% 11.89/2.28 cnf(c_0_56, negated_conjecture, (r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk27_0,esk55_1(esk27_0))|~p1(esk27_0)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_53]), c_0_25])])).
% 11.89/2.28 cnf(c_0_57, plain, (p1(esk27_0)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55]), c_0_25]), c_0_21])]), c_0_48])).
% 11.89/2.28 cnf(c_0_58, plain, (r1(X1,esk55_1(X1))|r1(X2,esk53_2(X1,X2))|p1(X3)|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_59, negated_conjecture, (r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk27_0,esk55_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 11.89/2.28 cnf(c_0_60, negated_conjecture, (r1(esk27_0,esk55_1(esk27_0))|r1(X1,esk53_2(esk27_0,X1))|~p1(esk27_0)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_52]), c_0_53]), c_0_25])])).
% 11.89/2.28 cnf(c_0_61, plain, (r1(X1,esk60_2(X2,X1))|p1(X4)|~r1(X2,X1)|~r1(X1,X3)|~r1(X3,X4)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_62, negated_conjecture, (r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_59, c_0_21])).
% 11.89/2.28 cnf(c_0_63, negated_conjecture, (r1(X1,esk53_2(esk27_0,X1))|r1(esk27_0,esk55_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_57])])).
% 11.89/2.28 cnf(c_0_64, plain, (p1(esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_62])).
% 11.89/2.28 cnf(c_0_65, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_63, c_0_21])).
% 11.89/2.28 cnf(c_0_66, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|r1(esk27_0,esk55_1(esk27_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_64, c_0_65])).
% 11.89/2.28 cnf(c_0_67, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_68, plain, (p1(X4)|~p1(esk60_2(X1,X2))|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_69, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_67])).
% 11.89/2.28 cnf(c_0_70, plain, (r1(esk55_1(X1),esk56_1(X1))|r1(X2,esk53_2(X1,X2))|p1(X3)|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_71, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk27_0,esk55_1(esk27_0))|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_69]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_72, negated_conjecture, (r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(X1,esk53_2(esk27_0,X1))|~p1(esk27_0)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_52]), c_0_53]), c_0_25])])).
% 11.89/2.28 cnf(c_0_73, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk27_0,esk55_1(esk27_0))|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_71, c_0_65])).
% 11.89/2.28 cnf(c_0_74, negated_conjecture, (r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_57])])).
% 11.89/2.28 cnf(c_0_75, plain, (r1(X1,esk55_1(X1))|p1(X3)|~p1(esk54_2(X1,X2))|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_76, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_73, c_0_62])).
% 11.89/2.28 cnf(c_0_77, plain, (r1(X1,esk63_1(X1))|r1(X2,esk61_3(X1,X3,X2))|p1(X2)|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_78, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_74, c_0_21])).
% 11.89/2.28 cnf(c_0_79, plain, (p1(X1)|r1(esk27_0,esk55_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_25]), c_0_57]), c_0_21])])).
% 11.89/2.28 cnf(c_0_80, plain, (r1(X1,esk63_1(X1))|p1(esk61_3(X1,X2,X3))|p1(X3)|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_81, plain, (p1(X1)|p1(X4)|r1(X5,esk53_2(X2,X5))|p1(X6)|~r1(esk55_1(X2),X1)|~r1(X1,X3)|~r1(X3,X4)|~p1(X3)|~r1(X2,X5)|~r1(X2,X6)|~p1(X2)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_82, plain, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_77, c_0_78])).
% 11.89/2.28 cnf(c_0_83, negated_conjecture, (r1(esk27_0,esk55_1(esk27_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_84, plain, (p1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_80, c_0_78])).
% 11.89/2.28 cnf(c_0_85, plain, (r1(X1,esk63_1(X1))|r1(esk61_3(X1,X2,X3),esk62_3(X1,X2,X3))|p1(X3)|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_86, plain, (p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X3,esk53_2(esk27_0,X3))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_78]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_87, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_88, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_89, plain, (p1(esk56_1(esk27_0))|r1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_85, c_0_78])).
% 11.89/2.28 cnf(c_0_90, plain, (p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X3,esk53_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_87]), c_0_88])).
% 11.89/2.28 cnf(c_0_91, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_92, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X2,esk53_2(esk27_0,X2))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_90, c_0_91])).
% 11.89/2.28 cnf(c_0_93, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_94, plain, (r1(X1,esk63_1(X1))|p1(X3)|~p1(esk62_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_95, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_93, c_0_21])).
% 11.89/2.28 cnf(c_0_96, plain, (r1(X2,esk53_2(X1,X2))|p1(X3)|~p1(esk56_1(X1))|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_97, plain, (p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_95]), c_0_25]), c_0_83])]), c_0_78])).
% 11.89/2.28 cnf(c_0_98, plain, (p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X2,esk53_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_97]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_99, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk53_2(esk27_0,X1))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_98, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_100, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_99, c_0_21])).
% 11.89/2.28 cnf(c_0_101, plain, (p1(X3)|r1(X4,esk61_3(X1,X5,X4))|p1(X4)|~r1(esk63_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~r1(X5,X4)|~r1(X1,X5)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_102, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk63_1(esk27_0),esk30_1(esk63_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_30, c_0_100])).
% 11.89/2.28 cnf(c_0_103, negated_conjecture, (p1(esk30_1(esk63_1(esk27_0)))|p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_32, c_0_100])).
% 11.89/2.28 cnf(c_0_104, plain, (p1(X3)|p1(esk61_3(X1,X4,X5))|p1(X5)|~r1(esk63_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~r1(X4,X5)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_105, plain, (p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk61_3(esk27_0,X3,X1))|~r1(esk30_1(esk63_1(esk27_0)),X2)|~r1(esk27_0,X3)|~r1(X3,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_102]), c_0_25])]), c_0_103])).
% 11.89/2.28 cnf(c_0_106, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk30_1(esk63_1(esk27_0)),esk31_1(esk63_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_36, c_0_100])).
% 11.89/2.28 cnf(c_0_107, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~p1(esk31_1(esk63_1(esk27_0)))), inference(spm,[status(thm)],[c_0_37, c_0_100])).
% 11.89/2.28 cnf(c_0_108, plain, (p1(esk61_3(esk27_0,X1,X2))|p1(esk63_1(esk27_0))|p1(X2)|p1(X3)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk30_1(esk63_1(esk27_0)),X3)|~r1(esk27_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_102]), c_0_25])]), c_0_103])).
% 11.89/2.28 cnf(c_0_109, plain, (p1(X3)|r1(esk61_3(X1,X4,X5),esk62_3(X1,X4,X5))|p1(X5)|~r1(esk63_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~r1(X4,X5)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_110, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk61_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_106]), c_0_107])).
% 11.89/2.28 cnf(c_0_111, negated_conjecture, (p1(esk61_3(esk27_0,X1,X2))|p1(esk63_1(esk27_0))|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk27_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_106]), c_0_107])).
% 11.89/2.28 cnf(c_0_112, plain, (p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|r1(esk61_3(esk27_0,X3,X1),esk62_3(esk27_0,X3,X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk30_1(esk63_1(esk27_0)),X2)|~r1(esk27_0,X3)|~r1(X3,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109, c_0_102]), c_0_25])]), c_0_103])).
% 11.89/2.28 cnf(c_0_113, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(X1,esk61_3(esk27_0,esk55_1(esk27_0),X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_110, c_0_83])).
% 11.89/2.28 cnf(c_0_114, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),X1))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_111, c_0_83])).
% 11.89/2.28 cnf(c_0_115, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk61_3(esk27_0,X2,X1),esk62_3(esk27_0,X2,X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_106]), c_0_107])).
% 11.89/2.28 cnf(c_0_116, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_113, c_0_78])).
% 11.89/2.28 cnf(c_0_117, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_114, c_0_78])).
% 11.89/2.28 cnf(c_0_118, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk61_3(esk27_0,esk55_1(esk27_0),X1),esk62_3(esk27_0,esk55_1(esk27_0),X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_115, c_0_83])).
% 11.89/2.28 cnf(c_0_119, plain, (p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X3,esk53_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_116]), c_0_117])).
% 11.89/2.28 cnf(c_0_120, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_118, c_0_78])).
% 11.89/2.28 cnf(c_0_121, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X2,esk53_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_119, c_0_120])).
% 11.89/2.28 cnf(c_0_122, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_121, c_0_100])).
% 11.89/2.28 cnf(c_0_123, plain, (p1(X3)|p1(X5)|~r1(esk63_1(X1),X2)|~r1(X2,X3)|~p1(X2)|~p1(esk62_3(X1,X4,X5))|~r1(X4,X5)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_124, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_122, c_0_21])).
% 11.89/2.28 cnf(c_0_125, plain, (p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~p1(X2)|~r1(esk63_1(esk27_0),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_124]), c_0_25]), c_0_83])]), c_0_78])).
% 11.89/2.28 cnf(c_0_126, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk30_1(esk63_1(esk27_0)),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_125, c_0_102]), c_0_103])).
% 11.89/2.28 cnf(c_0_127, negated_conjecture, (p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_126, c_0_106]), c_0_107])).
% 11.89/2.28 cnf(c_0_128, plain, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X2,esk53_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_127]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_129, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_128, c_0_100])).
% 11.89/2.28 cnf(c_0_130, plain, (r1(X2,esk61_3(X1,X3,X2))|p1(X2)|~p1(esk63_1(X1))|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_131, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_129, c_0_21])).
% 11.89/2.28 cnf(c_0_132, plain, (p1(esk61_3(X1,X2,X3))|p1(X3)|~p1(esk63_1(X1))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_133, plain, (p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk61_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_131]), c_0_25])])).
% 11.89/2.28 cnf(c_0_134, plain, (p1(esk61_3(esk27_0,X1,X2))|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk27_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_131]), c_0_25])])).
% 11.89/2.28 cnf(c_0_135, plain, (r1(esk61_3(X1,X2,X3),esk62_3(X1,X2,X3))|p1(X3)|~p1(esk63_1(X1))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_136, negated_conjecture, (p1(X1)|r1(X1,esk61_3(esk27_0,esk55_1(esk27_0),X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_133, c_0_83])).
% 11.89/2.28 cnf(c_0_137, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),X1))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_134, c_0_83])).
% 11.89/2.28 cnf(c_0_138, plain, (p1(X1)|r1(esk61_3(esk27_0,X2,X1),esk62_3(esk27_0,X2,X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_131]), c_0_25])])).
% 11.89/2.28 cnf(c_0_139, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_136, c_0_78])).
% 11.89/2.28 cnf(c_0_140, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_137, c_0_78])).
% 11.89/2.28 cnf(c_0_141, negated_conjecture, (p1(X1)|r1(esk61_3(esk27_0,esk55_1(esk27_0),X1),esk62_3(esk27_0,esk55_1(esk27_0),X1))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_138, c_0_83])).
% 11.89/2.28 cnf(c_0_142, plain, (p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X3,esk53_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86, c_0_139]), c_0_140])).
% 11.89/2.28 cnf(c_0_143, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_141, c_0_78])).
% 11.89/2.28 cnf(c_0_144, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X2,esk53_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_142, c_0_143])).
% 11.89/2.28 cnf(c_0_145, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_144, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_146, plain, (r1(esk55_1(X1),esk56_1(X1))|r1(esk53_2(X1,X2),esk54_2(X1,X2))|p1(X3)|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_147, plain, (p1(X3)|~p1(esk63_1(X1))|~p1(esk62_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_148, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_145, c_0_21])).
% 11.89/2.28 cnf(c_0_149, negated_conjecture, (r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk55_1(esk27_0),esk56_1(esk27_0))|~p1(esk27_0)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_146, c_0_52]), c_0_53]), c_0_25])])).
% 11.89/2.28 cnf(c_0_150, plain, (p1(esk56_1(esk27_0))|r1(esk29_0,esk53_2(esk27_0,esk29_0))), 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_147, c_0_148]), c_0_25]), c_0_83])]), c_0_78]), c_0_131])).
% 11.89/2.28 cnf(c_0_151, negated_conjecture, (r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk55_1(esk27_0),esk56_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149, c_0_57])])).
% 11.89/2.28 cnf(c_0_152, plain, (p1(X1)|r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X2,esk53_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_150]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_153, negated_conjecture, (r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_151, c_0_21])).
% 11.89/2.28 cnf(c_0_154, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))|r1(X1,esk53_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_152, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_155, plain, (p1(esk54_2(esk27_0,esk29_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_153])).
% 11.89/2.28 cnf(c_0_156, negated_conjecture, (r1(esk29_0,esk53_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_154, c_0_21])).
% 11.89/2.28 cnf(c_0_157, plain, (p1(esk54_2(esk27_0,esk29_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(esk29_0,esk60_2(X1,esk29_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_155, c_0_156])).
% 11.89/2.28 cnf(c_0_158, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_157, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_159, plain, (p1(X1)|p1(X4)|r1(esk53_2(X2,X5),esk54_2(X2,X5))|p1(X6)|~r1(esk55_1(X2),X1)|~r1(X1,X3)|~r1(X3,X4)|~p1(X3)|~r1(X2,X5)|~r1(X2,X6)|~p1(X2)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_160, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_77, c_0_158])).
% 11.89/2.28 cnf(c_0_161, plain, (p1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_80, c_0_158])).
% 11.89/2.28 cnf(c_0_162, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_158]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_163, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_160, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_164, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_161, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_165, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_85, c_0_158])).
% 11.89/2.28 cnf(c_0_166, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_163]), c_0_164])).
% 11.89/2.28 cnf(c_0_167, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_165, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_168, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_166, c_0_167])).
% 11.89/2.28 cnf(c_0_169, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_168, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_170, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_169, c_0_21])).
% 11.89/2.28 cnf(c_0_171, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_170]), c_0_25]), c_0_83])]), c_0_158])).
% 11.89/2.28 cnf(c_0_172, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_171])).
% 11.89/2.28 cnf(c_0_173, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_172, c_0_156])).
% 11.89/2.28 cnf(c_0_174, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_173, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_175, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_174])).
% 11.89/2.28 cnf(c_0_176, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_175]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_177, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_176, c_0_156])).
% 11.89/2.28 cnf(c_0_178, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_177, c_0_153])).
% 11.89/2.28 cnf(c_0_179, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_77, c_0_178])).
% 11.89/2.28 cnf(c_0_180, plain, (p1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_80, c_0_178])).
% 11.89/2.28 cnf(c_0_181, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk27_0,esk63_1(esk27_0))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_178]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_182, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_179, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_183, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_180, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_184, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_85, c_0_178])).
% 11.89/2.28 cnf(c_0_185, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_181, c_0_182]), c_0_183])).
% 11.89/2.28 cnf(c_0_186, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_184, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_187, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_185, c_0_186])).
% 11.89/2.28 cnf(c_0_188, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_187, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_189, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_188, c_0_21])).
% 11.89/2.28 cnf(c_0_190, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_189]), c_0_25]), c_0_83])]), c_0_153])).
% 11.89/2.28 cnf(c_0_191, plain, (r1(esk53_2(X1,X2),esk54_2(X1,X2))|p1(X3)|~p1(esk56_1(X1))|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_192, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_177, c_0_190])).
% 11.89/2.28 cnf(c_0_193, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191, c_0_192]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_194, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_193, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_195, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_194, c_0_21])).
% 11.89/2.28 cnf(c_0_196, plain, (p1(esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_195])).
% 11.89/2.28 cnf(c_0_197, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|r1(esk27_0,esk63_1(esk27_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_196, c_0_156])).
% 11.89/2.28 cnf(c_0_198, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_197, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_199, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_198])).
% 11.89/2.28 cnf(c_0_200, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_199]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_201, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_200, c_0_156])).
% 11.89/2.28 cnf(c_0_202, plain, (r1(esk55_1(X1),esk56_1(X1))|p1(X3)|~p1(esk54_2(X1,X2))|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_203, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk27_0,esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_201, c_0_195])).
% 11.89/2.28 cnf(c_0_204, plain, (p1(X1)|r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_202, c_0_203]), c_0_25]), c_0_57]), c_0_21])])).
% 11.89/2.28 cnf(c_0_205, plain, (p1(X3)|~p1(esk56_1(X1))|~p1(esk54_2(X1,X2))|~r1(X1,X2)|~r1(X1,X3)|~p1(X1)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_206, negated_conjecture, (r1(esk55_1(esk27_0),esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_204, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_207, plain, (p1(X1)|p1(X4)|p1(X6)|~r1(esk55_1(X2),X1)|~r1(X1,X3)|~r1(X3,X4)|~p1(X3)|~p1(esk54_2(X2,X5))|~r1(X2,X5)|~r1(X2,X6)|~p1(X2)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 11.89/2.28 cnf(c_0_208, plain, (p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~p1(esk56_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205, c_0_203]), c_0_25]), c_0_57]), c_0_21])])).
% 11.89/2.28 cnf(c_0_209, plain, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_77, c_0_206])).
% 11.89/2.28 cnf(c_0_210, plain, (p1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_80, c_0_206])).
% 11.89/2.28 cnf(c_0_211, plain, (p1(X1)|p1(X2)|r1(esk27_0,esk63_1(esk27_0))|~p1(esk54_2(esk27_0,X3))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_207, c_0_206]), c_0_25]), c_0_57])]), c_0_208])).
% 11.89/2.28 cnf(c_0_212, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_209, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_213, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_210, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_214, plain, (p1(esk56_1(esk27_0))|r1(esk61_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(X1,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))|r1(X1,esk63_1(X1))|~epred1_1(X1)|~r1(X1,esk55_1(esk27_0))), inference(spm,[status(thm)],[c_0_85, c_0_206])).
% 11.89/2.28 cnf(c_0_215, plain, (p1(X1)|p1(X2)|r1(esk27_0,esk63_1(esk27_0))|~p1(esk54_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_211, c_0_212]), c_0_213]), c_0_208])).
% 11.89/2.28 cnf(c_0_216, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_214, c_0_83]), c_0_25])])).
% 11.89/2.28 cnf(c_0_217, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~p1(esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_215, c_0_216]), c_0_208])).
% 11.89/2.28 cnf(c_0_218, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_217, c_0_203]), c_0_21])])).
% 11.89/2.28 cnf(c_0_219, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk27_0,esk63_1(esk27_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_218, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_220, plain, (p1(esk56_1(esk27_0))|r1(esk27_0,esk63_1(esk27_0))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94, c_0_219]), c_0_25]), c_0_83])]), c_0_206])).
% 11.89/2.28 cnf(c_0_221, plain, (p1(X1)|r1(esk27_0,esk63_1(esk27_0))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_208, c_0_220])).
% 11.89/2.28 cnf(c_0_222, negated_conjecture, (r1(esk27_0,esk63_1(esk27_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_221, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_223, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk63_1(esk27_0),esk30_1(esk63_1(esk27_0)))), inference(spm,[status(thm)],[c_0_30, c_0_222])).
% 11.89/2.28 cnf(c_0_224, negated_conjecture, (p1(esk30_1(esk63_1(esk27_0)))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_32, c_0_222])).
% 11.89/2.28 cnf(c_0_225, plain, (p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|r1(X1,esk61_3(esk27_0,X3,X1))|~r1(esk30_1(esk63_1(esk27_0)),X2)|~r1(esk27_0,X3)|~r1(X3,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101, c_0_223]), c_0_25])]), c_0_224])).
% 11.89/2.28 cnf(c_0_226, negated_conjecture, (p1(esk63_1(esk27_0))|r1(esk30_1(esk63_1(esk27_0)),esk31_1(esk63_1(esk27_0)))), inference(spm,[status(thm)],[c_0_36, c_0_222])).
% 11.89/2.28 cnf(c_0_227, negated_conjecture, (p1(esk63_1(esk27_0))|~p1(esk31_1(esk63_1(esk27_0)))), inference(spm,[status(thm)],[c_0_37, c_0_222])).
% 11.89/2.28 cnf(c_0_228, plain, (p1(esk61_3(esk27_0,X1,X2))|p1(esk63_1(esk27_0))|p1(X2)|p1(X3)|~r1(esk30_1(esk63_1(esk27_0)),X3)|~r1(esk27_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_223]), c_0_25])]), c_0_224])).
% 11.89/2.28 cnf(c_0_229, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(X1,esk61_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_225, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_230, negated_conjecture, (p1(esk61_3(esk27_0,X1,X2))|p1(esk63_1(esk27_0))|p1(X2)|~r1(esk27_0,X1)|~r1(X1,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_228, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_231, plain, (p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|r1(esk61_3(esk27_0,X3,X1),esk62_3(esk27_0,X3,X1))|~r1(esk30_1(esk63_1(esk27_0)),X2)|~r1(esk27_0,X3)|~r1(X3,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109, c_0_223]), c_0_25])]), c_0_224])).
% 11.89/2.28 cnf(c_0_232, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(X1,esk61_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_229, c_0_83])).
% 11.89/2.28 cnf(c_0_233, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),X1))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_230, c_0_83])).
% 11.89/2.28 cnf(c_0_234, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk61_3(esk27_0,X2,X1),esk62_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_231, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_235, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_232, c_0_158])).
% 11.89/2.28 cnf(c_0_236, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_233, c_0_158])).
% 11.89/2.28 cnf(c_0_237, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|r1(esk61_3(esk27_0,esk55_1(esk27_0),X1),esk62_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_234, c_0_83])).
% 11.89/2.28 cnf(c_0_238, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_235]), c_0_236])).
% 11.89/2.28 cnf(c_0_239, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_237, c_0_158])).
% 11.89/2.28 cnf(c_0_240, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_238, c_0_239])).
% 11.89/2.28 cnf(c_0_241, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_240, c_0_222])).
% 11.89/2.28 cnf(c_0_242, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_241, c_0_21])).
% 11.89/2.28 cnf(c_0_243, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~p1(X2)|~r1(esk63_1(esk27_0),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_242]), c_0_25]), c_0_83])]), c_0_158])).
% 11.89/2.28 cnf(c_0_244, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk30_1(esk63_1(esk27_0)),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_243, c_0_223]), c_0_224])).
% 11.89/2.28 cnf(c_0_245, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_244, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_246, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_245])).
% 11.89/2.28 cnf(c_0_247, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_246, c_0_156])).
% 11.89/2.28 cnf(c_0_248, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_247, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_249, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_248])).
% 11.89/2.28 cnf(c_0_250, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_249]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_251, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_250, c_0_156])).
% 11.89/2.28 cnf(c_0_252, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_251, c_0_153])).
% 11.89/2.28 cnf(c_0_253, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_252]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_254, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_232, c_0_252])).
% 11.89/2.28 cnf(c_0_255, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_233, c_0_252])).
% 11.89/2.28 cnf(c_0_256, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_253, c_0_254]), c_0_255])).
% 11.89/2.28 cnf(c_0_257, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_237, c_0_252])).
% 11.89/2.28 cnf(c_0_258, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_256, c_0_257])).
% 11.89/2.28 cnf(c_0_259, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_258, c_0_222])).
% 11.89/2.28 cnf(c_0_260, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_259, c_0_21])).
% 11.89/2.28 cnf(c_0_261, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|~p1(X2)|~r1(esk63_1(esk27_0),X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_260]), c_0_25]), c_0_83])]), c_0_153])).
% 11.89/2.28 cnf(c_0_262, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|~r1(esk30_1(esk63_1(esk27_0)),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_261, c_0_223]), c_0_224])).
% 11.89/2.28 cnf(c_0_263, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_262, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_264, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_251, c_0_263])).
% 11.89/2.28 cnf(c_0_265, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191, c_0_264]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_266, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_265, c_0_222])).
% 11.89/2.28 cnf(c_0_267, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_266, c_0_21])).
% 11.89/2.28 cnf(c_0_268, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_267])).
% 11.89/2.28 cnf(c_0_269, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk60_2(X1,esk29_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_268, c_0_156])).
% 11.89/2.28 cnf(c_0_270, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_269, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_271, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_270])).
% 11.89/2.28 cnf(c_0_272, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_271]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_273, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_272, c_0_156])).
% 11.89/2.28 cnf(c_0_274, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_273, c_0_267])).
% 11.89/2.28 cnf(c_0_275, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(X1,esk61_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_274]), c_0_25])])).
% 11.89/2.28 cnf(c_0_276, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk61_3(esk27_0,X1,X2))|p1(X2)|~r1(esk27_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_274]), c_0_25])])).
% 11.89/2.28 cnf(c_0_277, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(X1,esk61_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_275, c_0_83])).
% 11.89/2.28 cnf(c_0_278, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),X1))|p1(esk54_2(esk27_0,esk29_0))|p1(X1)|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_276, c_0_83])).
% 11.89/2.28 cnf(c_0_279, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk61_3(esk27_0,X2,X1),esk62_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_274]), c_0_25])])).
% 11.89/2.28 cnf(c_0_280, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_277, c_0_158])).
% 11.89/2.28 cnf(c_0_281, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_278, c_0_158])).
% 11.89/2.28 cnf(c_0_282, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk61_3(esk27_0,esk55_1(esk27_0),X1),esk62_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_279, c_0_83])).
% 11.89/2.28 cnf(c_0_283, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_280]), c_0_281])).
% 11.89/2.28 cnf(c_0_284, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_282, c_0_158])).
% 11.89/2.28 cnf(c_0_285, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_283, c_0_284])).
% 11.89/2.28 cnf(c_0_286, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_285, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_287, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_286, c_0_21])).
% 11.89/2.28 cnf(c_0_288, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), 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_147, c_0_287]), c_0_25]), c_0_83])]), c_0_158]), c_0_274])).
% 11.89/2.28 cnf(c_0_289, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_288])).
% 11.89/2.28 cnf(c_0_290, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_289, c_0_156])).
% 11.89/2.28 cnf(c_0_291, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_290, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_292, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_26, c_0_291])).
% 11.89/2.28 cnf(c_0_293, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_292]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_294, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_293, c_0_156])).
% 11.89/2.28 cnf(c_0_295, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_294, c_0_153])).
% 11.89/2.28 cnf(c_0_296, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_159, c_0_295]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_297, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_277, c_0_295])).
% 11.89/2.28 cnf(c_0_298, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_278, c_0_295])).
% 11.89/2.28 cnf(c_0_299, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|p1(X2)|r1(esk53_2(esk27_0,X3),esk54_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_296, c_0_297]), c_0_298])).
% 11.89/2.28 cnf(c_0_300, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_282, c_0_295])).
% 11.89/2.28 cnf(c_0_301, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(spm,[status(thm)],[c_0_299, c_0_300])).
% 11.89/2.28 cnf(c_0_302, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_301, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_303, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_302, c_0_21])).
% 11.89/2.28 cnf(c_0_304, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), 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_147, c_0_303]), c_0_25]), c_0_83])]), c_0_153]), c_0_274])).
% 11.89/2.28 cnf(c_0_305, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_294, c_0_304])).
% 11.89/2.28 cnf(c_0_306, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|r1(esk53_2(esk27_0,X2),esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191, c_0_305]), c_0_25]), c_0_57])])).
% 11.89/2.28 cnf(c_0_307, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk53_2(esk27_0,X1),esk54_2(esk27_0,X1))|~r1(esk27_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_306, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_308, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk53_2(esk27_0,esk29_0),esk54_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_307, c_0_21])).
% 11.89/2.28 cnf(c_0_309, plain, (p1(esk54_2(esk27_0,esk29_0))|r1(X1,esk60_2(X2,X1))|~epred1_1(X2)|~r1(X1,esk53_2(esk27_0,esk29_0))|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_61, c_0_308])).
% 11.89/2.28 cnf(c_0_310, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(X1,esk29_0))|~epred1_1(X1)|~r1(X1,esk29_0)), inference(spm,[status(thm)],[c_0_309, c_0_156])).
% 11.89/2.28 cnf(c_0_311, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|r1(esk29_0,esk60_2(esk27_0,esk29_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_310, c_0_21]), c_0_25])])).
% 11.89/2.28 cnf(c_0_312, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(esk60_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_26, c_0_311])).
% 11.89/2.28 cnf(c_0_313, plain, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|~r1(esk29_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68, c_0_312]), c_0_25]), c_0_21])])).
% 11.89/2.28 cnf(c_0_314, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))|p1(X1)|~r1(esk53_2(esk27_0,esk29_0),X1)), inference(spm,[status(thm)],[c_0_313, c_0_156])).
% 11.89/2.28 cnf(c_0_315, negated_conjecture, (p1(esk54_2(esk27_0,esk29_0))), inference(spm,[status(thm)],[c_0_314, c_0_308])).
% 11.89/2.28 cnf(c_0_316, plain, (p1(X1)|r1(esk55_1(esk27_0),esk56_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_202, c_0_315]), c_0_25]), c_0_57]), c_0_21])])).
% 11.89/2.28 cnf(c_0_317, negated_conjecture, (r1(esk55_1(esk27_0),esk56_1(esk27_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_316, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_318, plain, (p1(X1)|~p1(esk56_1(esk27_0))|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_205, c_0_315]), c_0_25]), c_0_57]), c_0_21])])).
% 11.89/2.28 cnf(c_0_319, plain, (p1(X1)|p1(X2)|~p1(esk54_2(esk27_0,X3))|~p1(X4)|~r1(esk56_1(esk27_0),X4)|~r1(esk27_0,X1)|~r1(esk27_0,X3)|~r1(X4,X2)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_207, c_0_317]), c_0_25]), c_0_57])]), c_0_318])).
% 11.89/2.28 cnf(c_0_320, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_232, c_0_317])).
% 11.89/2.28 cnf(c_0_321, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_233, c_0_317])).
% 11.89/2.28 cnf(c_0_322, negated_conjecture, (p1(esk63_1(esk27_0))|p1(X1)|p1(X2)|~p1(esk54_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_319, c_0_320]), c_0_321]), c_0_318])).
% 11.89/2.28 cnf(c_0_323, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_237, c_0_317])).
% 11.89/2.28 cnf(c_0_324, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk63_1(esk27_0))|p1(X1)|~p1(esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_322, c_0_323]), c_0_318])).
% 11.89/2.28 cnf(c_0_325, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_324, c_0_315]), c_0_21])])).
% 11.89/2.28 cnf(c_0_326, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_325, c_0_222])).
% 11.89/2.28 cnf(c_0_327, plain, (p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))|p1(X1)|~p1(X2)|~r1(esk63_1(esk27_0),X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_326]), c_0_25]), c_0_317]), c_0_83])])).
% 11.89/2.28 cnf(c_0_328, negated_conjecture, (p1(esk56_1(esk27_0))|p1(esk63_1(esk27_0))|p1(X1)|~r1(esk30_1(esk63_1(esk27_0)),X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_327, c_0_223]), c_0_224])).
% 11.89/2.28 cnf(c_0_329, negated_conjecture, (p1(esk63_1(esk27_0))|p1(esk56_1(esk27_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_328, c_0_226]), c_0_227])).
% 11.89/2.28 cnf(c_0_330, plain, (p1(esk63_1(esk27_0))|p1(X1)|~r1(esk27_0,X1)), inference(spm,[status(thm)],[c_0_318, c_0_329])).
% 11.89/2.28 cnf(c_0_331, negated_conjecture, (p1(esk63_1(esk27_0))), inference(spm,[status(thm)],[c_0_330, c_0_222])).
% 11.89/2.28 cnf(c_0_332, plain, (p1(X1)|r1(X1,esk61_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_331]), c_0_25])])).
% 11.89/2.28 cnf(c_0_333, plain, (p1(esk61_3(esk27_0,X1,X2))|p1(X2)|~r1(esk27_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132, c_0_331]), c_0_25])])).
% 11.89/2.28 cnf(c_0_334, negated_conjecture, (p1(X1)|r1(X1,esk61_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_332, c_0_83])).
% 11.89/2.28 cnf(c_0_335, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),X1))|p1(X1)|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_333, c_0_83])).
% 11.89/2.28 cnf(c_0_336, plain, (p1(X1)|r1(esk61_3(esk27_0,X2,X1),esk62_3(esk27_0,X2,X1))|~r1(esk27_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_331]), c_0_25])])).
% 11.89/2.28 cnf(c_0_337, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk56_1(esk27_0),esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_334, c_0_317])).
% 11.89/2.28 cnf(c_0_338, negated_conjecture, (p1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(esk56_1(esk27_0))), inference(spm,[status(thm)],[c_0_335, c_0_317])).
% 11.89/2.28 cnf(c_0_339, negated_conjecture, (p1(X1)|r1(esk61_3(esk27_0,esk55_1(esk27_0),X1),esk62_3(esk27_0,esk55_1(esk27_0),X1))|~r1(esk55_1(esk27_0),X1)), inference(spm,[status(thm)],[c_0_336, c_0_83])).
% 11.89/2.28 cnf(c_0_340, plain, (p1(X1)|p1(X2)|~p1(esk54_2(esk27_0,X3))|~r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),X1)|~r1(esk27_0,X2)|~r1(esk27_0,X3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_319, c_0_337]), c_0_338]), c_0_318])).
% 11.89/2.28 cnf(c_0_341, negated_conjecture, (p1(esk56_1(esk27_0))|r1(esk61_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)),esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(spm,[status(thm)],[c_0_339, c_0_317])).
% 11.89/2.28 cnf(c_0_342, plain, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(X1)|~p1(esk54_2(esk27_0,X2))|~r1(esk27_0,X1)|~r1(esk27_0,X2)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_340, c_0_341]), c_0_318])).
% 11.89/2.28 cnf(c_0_343, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))|p1(X1)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_342, c_0_315]), c_0_21])])).
% 11.89/2.28 cnf(c_0_344, negated_conjecture, (p1(esk62_3(esk27_0,esk55_1(esk27_0),esk56_1(esk27_0)))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_343, c_0_52]), c_0_53])).
% 11.89/2.28 cnf(c_0_345, plain, (p1(esk56_1(esk27_0))), 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_147, c_0_344]), c_0_25]), c_0_331]), c_0_317]), c_0_83])])).
% 11.89/2.28 cnf(c_0_346, plain, (p1(X1)|~r1(esk27_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_318, c_0_345])])).
% 11.89/2.28 cnf(c_0_347, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_346, c_0_52]), c_0_53]), ['proof']).
% 11.89/2.28 % SZS output end Proof
% 11.89/2.28 % User time : 1.566 s
% 11.89/2.28 % System time : 0.009 s
% 11.89/2.28 % Total time : 1.575 s
% 11.89/2.28 % User time : 1.571 s
% 11.89/2.28 % System time : 0.011 s
% 11.89/2.28 % Total time : 1.582 s
% 11.89/2.28
%------------------------------------------------------------------------------