%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL646+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n020.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:18 AM UTC 2026
% Result : Theorem 26.97s 4.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL646+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : java -jar mcs_scs.jar %d %s
% 0.15/0.42 % Computer : n020.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Fri Sep 4 19:45:42 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.28/0.59 start to proof:theBenchmark.p
% 26.97/4.01 % Version : CSI_E---1.1
% 26.97/4.01 % Problem : theBenchmark.p
% 26.97/4.01 % Proof found!
% 26.97/4.01 % SZS status Theorem for theBenchmark.p
% 26.97/4.01 % SZS output start Proof
% 26.97/4.01 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p6(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p4(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p4(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p6(X2)))&~(p6(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p6(X2)))&~(p4(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p6(X2)))&~(p2(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p6(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p4(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p2(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p6(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p4(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p2(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p6(X1)))&~(p6(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p6(X1)))&~(p2(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p5(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))&~(p5(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p1(X2)))&~(p5(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p4(X1)))&~(p6(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p4(X1)))&~(p2(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p3(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))&~(p3(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p1(X2)))&~(p3(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p2(X1)))&~(p6(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p2(X1)))&~(p2(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p1(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p1(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))&~(p1(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))|p6(X2)))&~(p6(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p6(X2)))&~(p4(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p6(X2)))&~(p2(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p5(X1)))&~(p5(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p5(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p6(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p4(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p2(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p1(X1)))&~(p4(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p5(X1)))&~(p3(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p3(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p6(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p4(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p2(X2)))&~(p2(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p5(X1)))&~(p1(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p1(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p6(X1)))&~(p6(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p6(X1)))&~(p4(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p5(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))&~(p5(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p1(X2)))&~(p5(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p4(X1)))&~(p6(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p4(X1)))&~(p4(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p3(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))&~(p3(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p1(X2)))&~(p3(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p2(X1)))&~(p6(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p2(X1)))&~(p4(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p5(X2)))&~(p1(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p4(X2)))&~(p1(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(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))|p5(X1)))&~(p5(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p5(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p5(X1)))&~(p3(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p3(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p1(X1)))&~(p2(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p5(X1)))&~(p1(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p3(X1)))&~(p1(X2)))))))|![X2]:((~(r1(X1,X2))|p5(X2)))|![X2]:((~(r1(X1,X2))|p3(X2)))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|p1(X2))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 26.97/4.01 fof(c_0_1, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p6(X2))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p4(X2))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p4(X2))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p6(X2)))&~p6(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p6(X2)))&~p4(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p6(X2)))&~p2(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p6(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p4(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p2(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p6(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p4(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p2(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p6(X1)))&~p6(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p6(X1)))&~p2(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p5(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))&~p5(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p1(X2)))&~p5(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p4(X1)))&~p6(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p4(X1)))&~p2(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p3(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))&~p3(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p1(X2)))&~p3(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p2(X1)))&~p6(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p2(X1)))&~p2(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p1(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p1(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))&~p1(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)|p6(X2)))&~p6(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p6(X2)))&~p4(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p6(X2)))&~p2(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&~p5(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p5(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p6(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p4(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p2(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p1(X1)))&~p4(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&~p3(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p3(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p6(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p4(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p2(X2)))&~p2(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&~p1(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p1(X2))))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p6(X1)))&~p6(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p6(X1)))&~p4(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p5(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))&~p5(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p1(X2)))&~p5(X1))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p4(X1)))&~p6(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p4(X1)))&~p4(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p3(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))&~p3(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p1(X2)))&~p3(X1))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p2(X1)))&~p6(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p2(X1)))&~p4(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p5(X2)))&~p1(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p4(X2)))&~p1(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(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)|p5(X1)))&~p5(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p5(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&~p3(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p3(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p1(X1)))&~p2(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p5(X1)))&~p1(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p3(X1)))&~p1(X2))))))|![X2]:((~r1(X1,X2)|p5(X2)))|![X2]:((~r1(X1,X2)|p3(X2)))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|p1(X2)))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 26.97/4.02 fof(c_0_2, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X27, X29, X30, X31, X32, X34, X35, X36, X37, X39, X40, X41, X42, X44, X45, X46, X47, X49, X50, X51, X52, X54, X55, X56, X57, X59, X60, X61, X62, X64, X65, X66, X67, X69, X70, X71, X73, X74, X75, X77, X78, X79, X80, X82, X83, X84, X85, X87, X88, X89, X90, X92, X93, X94, X96, X97, X98, X100, X101, X102, X103, X105, X106, X107, X108, X110, X111, X112, X113, X115, X116, X117, X119, X120, X121, X123, X124, X125, X126, X128, X129, X130, X131, X133, X134, X135, X136, X138, X139, X140, X141, X143, X144, X146, X147, X149, X150, X152, X153, X154, X156, X157, X158, X160, X161, X163, X164, X166, X167, X169, X170, X171, X173, X174, X175, X177, X178, X179, X181, X182, X184, X185, X187, X188, X190, X191, X192, X194, X195, X196, X198, X200, X202, X203, X205, X206, X208, X209, X211, X213, X215, X216, X218, X219, X221, X222, X224, X226, X228, X229, X231, X232, X234, X235, X237, X238, X240, X242, X244, X246, X248, X250, X252]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(esk1_0,X4)|(~r1(X4,X5)|(~r1(X5,X6)|(~r1(X6,X7)|(~r1(X7,X8)|p6(X8))))))&(~r1(esk1_0,X9)|(~r1(X9,X10)|(~r1(X10,X11)|(~r1(X11,X12)|(~r1(X12,X13)|p4(X13)))))))&(~r1(esk1_0,X14)|(~r1(X14,X15)|(~r1(X15,X16)|(~r1(X16,X17)|(~r1(X17,X18)|p4(X18)))))))&(~r1(esk1_0,X19)|(~r1(X19,X20)|(~r1(X20,X21)|(~r1(X21,X22)|(~r1(X22,X23)|p2(X23)))))))&((r1(X27,esk2_4(X24,X25,X26,X27))|p6(X27)|~r1(X26,X27)|~r1(X25,X26)|~r1(X24,X25)|~r1(esk1_0,X24))&(~p6(esk2_4(X24,X25,X26,X27))|p6(X27)|~r1(X26,X27)|~r1(X25,X26)|~r1(X24,X25)|~r1(esk1_0,X24))))&((r1(X32,esk3_4(X29,X30,X31,X32))|p4(X32)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(esk1_0,X29))&(~p6(esk3_4(X29,X30,X31,X32))|p4(X32)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(esk1_0,X29))))&((r1(X37,esk4_4(X34,X35,X36,X37))|p2(X37)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(esk1_0,X34))&(~p6(esk4_4(X34,X35,X36,X37))|p2(X37)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(esk1_0,X34))))&((r1(X42,esk5_4(X39,X40,X41,X42))|p6(X42)|~r1(X41,X42)|~r1(X40,X41)|~r1(X39,X40)|~r1(esk1_0,X39))&(~p4(esk5_4(X39,X40,X41,X42))|p6(X42)|~r1(X41,X42)|~r1(X40,X41)|~r1(X39,X40)|~r1(esk1_0,X39))))&((r1(X47,esk6_4(X44,X45,X46,X47))|p4(X47)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(esk1_0,X44))&(~p4(esk6_4(X44,X45,X46,X47))|p4(X47)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(esk1_0,X44))))&((r1(X52,esk7_4(X49,X50,X51,X52))|p2(X52)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))&(~p4(esk7_4(X49,X50,X51,X52))|p2(X52)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))))&((r1(X57,esk8_4(X54,X55,X56,X57))|p6(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))&(~p2(esk8_4(X54,X55,X56,X57))|p6(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))))&((r1(X62,esk9_4(X59,X60,X61,X62))|p4(X62)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~r1(esk1_0,X59))&(~p2(esk9_4(X59,X60,X61,X62))|p4(X62)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~r1(esk1_0,X59))))&((r1(X67,esk10_4(X64,X65,X66,X67))|p2(X67)|~r1(X66,X67)|~r1(X65,X66)|~r1(X64,X65)|~r1(esk1_0,X64))&(~p2(esk10_4(X64,X65,X66,X67))|p2(X67)|~r1(X66,X67)|~r1(X65,X66)|~r1(X64,X65)|~r1(esk1_0,X64))))&((r1(X71,esk11_3(X69,X70,X71))|p6(X71)|~r1(X70,X71)|~r1(X69,X70)|~r1(esk1_0,X69))&(~p6(esk11_3(X69,X70,X71))|p6(X71)|~r1(X70,X71)|~r1(X69,X70)|~r1(esk1_0,X69))))&((r1(X75,esk12_3(X73,X74,X75))|p2(X75)|~r1(X74,X75)|~r1(X73,X74)|~r1(esk1_0,X73))&(~p6(esk12_3(X73,X74,X75))|p2(X75)|~r1(X74,X75)|~r1(X73,X74)|~r1(esk1_0,X73))))&((r1(X80,esk13_4(X77,X78,X79,X80))|p5(X80)|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(esk1_0,X77))&(~p5(esk13_4(X77,X78,X79,X80))|p5(X80)|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(esk1_0,X77))))&((r1(X85,esk14_4(X82,X83,X84,X85))|p5(X85)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(esk1_0,X82))&(~p3(esk14_4(X82,X83,X84,X85))|p5(X85)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(esk1_0,X82))))&((r1(X90,esk15_4(X87,X88,X89,X90))|p5(X90)|~r1(X89,X90)|~r1(X88,X89)|~r1(X87,X88)|~r1(esk1_0,X87))&(~p1(esk15_4(X87,X88,X89,X90))|p5(X90)|~r1(X89,X90)|~r1(X88,X89)|~r1(X87,X88)|~r1(esk1_0,X87))))&((r1(X94,esk16_3(X92,X93,X94))|p6(X94)|~r1(X93,X94)|~r1(X92,X93)|~r1(esk1_0,X92))&(~p4(esk16_3(X92,X93,X94))|p6(X94)|~r1(X93,X94)|~r1(X92,X93)|~r1(esk1_0,X92))))&((r1(X98,esk17_3(X96,X97,X98))|p2(X98)|~r1(X97,X98)|~r1(X96,X97)|~r1(esk1_0,X96))&(~p4(esk17_3(X96,X97,X98))|p2(X98)|~r1(X97,X98)|~r1(X96,X97)|~r1(esk1_0,X96))))&((r1(X103,esk18_4(X100,X101,X102,X103))|p3(X103)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))&(~p5(esk18_4(X100,X101,X102,X103))|p3(X103)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))))&((r1(X108,esk19_4(X105,X106,X107,X108))|p3(X108)|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))&(~p3(esk19_4(X105,X106,X107,X108))|p3(X108)|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))))&((r1(X113,esk20_4(X110,X111,X112,X113))|p3(X113)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(esk1_0,X110))&(~p1(esk20_4(X110,X111,X112,X113))|p3(X113)|~r1(X112,X113)|~r1(X111,X112)|~r1(X110,X111)|~r1(esk1_0,X110))))&((r1(X117,esk21_3(X115,X116,X117))|p6(X117)|~r1(X116,X117)|~r1(X115,X116)|~r1(esk1_0,X115))&(~p2(esk21_3(X115,X116,X117))|p6(X117)|~r1(X116,X117)|~r1(X115,X116)|~r1(esk1_0,X115))))&((r1(X121,esk22_3(X119,X120,X121))|p2(X121)|~r1(X120,X121)|~r1(X119,X120)|~r1(esk1_0,X119))&(~p2(esk22_3(X119,X120,X121))|p2(X121)|~r1(X120,X121)|~r1(X119,X120)|~r1(esk1_0,X119))))&((r1(X126,esk23_4(X123,X124,X125,X126))|p1(X126)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(esk1_0,X123))&(~p5(esk23_4(X123,X124,X125,X126))|p1(X126)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(esk1_0,X123))))&((r1(X131,esk24_4(X128,X129,X130,X131))|p1(X131)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(esk1_0,X128))&(~p4(esk24_4(X128,X129,X130,X131))|p1(X131)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(esk1_0,X128))))&((r1(X136,esk25_4(X133,X134,X135,X136))|p1(X136)|~r1(X135,X136)|~r1(X134,X135)|~r1(X133,X134)|~r1(esk1_0,X133))&(~p3(esk25_4(X133,X134,X135,X136))|p1(X136)|~r1(X135,X136)|~r1(X134,X135)|~r1(X133,X134)|~r1(esk1_0,X133))))&((r1(X141,esk26_4(X138,X139,X140,X141))|p1(X141)|~r1(X140,X141)|~r1(X139,X140)|~r1(X138,X139)|~r1(esk1_0,X138))&(~p1(esk26_4(X138,X139,X140,X141))|p1(X141)|~r1(X140,X141)|~r1(X139,X140)|~r1(X138,X139)|~r1(esk1_0,X138))))&((r1(X144,esk27_2(X143,X144))|p6(X144)|~r1(X143,X144)|~r1(esk1_0,X143))&(~p6(esk27_2(X143,X144))|p6(X144)|~r1(X143,X144)|~r1(esk1_0,X143))))&((r1(X147,esk28_2(X146,X147))|p4(X147)|~r1(X146,X147)|~r1(esk1_0,X146))&(~p6(esk28_2(X146,X147))|p4(X147)|~r1(X146,X147)|~r1(esk1_0,X146))))&((r1(X150,esk29_2(X149,X150))|p2(X150)|~r1(X149,X150)|~r1(esk1_0,X149))&(~p6(esk29_2(X149,X150))|p2(X150)|~r1(X149,X150)|~r1(esk1_0,X149))))&((r1(X154,esk30_3(X152,X153,X154))|p5(X154)|~r1(X153,X154)|~r1(X152,X153)|~r1(esk1_0,X152))&(~p5(esk30_3(X152,X153,X154))|p5(X154)|~r1(X153,X154)|~r1(X152,X153)|~r1(esk1_0,X152))))&((r1(X158,esk31_3(X156,X157,X158))|p5(X158)|~r1(X157,X158)|~r1(X156,X157)|~r1(esk1_0,X156))&(~p3(esk31_3(X156,X157,X158))|p5(X158)|~r1(X157,X158)|~r1(X156,X157)|~r1(esk1_0,X156))))&((r1(X161,esk32_2(X160,X161))|p6(X161)|~r1(X160,X161)|~r1(esk1_0,X160))&(~p4(esk32_2(X160,X161))|p6(X161)|~r1(X160,X161)|~r1(esk1_0,X160))))&((r1(X164,esk33_2(X163,X164))|p4(X164)|~r1(X163,X164)|~r1(esk1_0,X163))&(~p4(esk33_2(X163,X164))|p4(X164)|~r1(X163,X164)|~r1(esk1_0,X163))))&((r1(X167,esk34_2(X166,X167))|p2(X167)|~r1(X166,X167)|~r1(esk1_0,X166))&(~p4(esk34_2(X166,X167))|p2(X167)|~r1(X166,X167)|~r1(esk1_0,X166))))&((r1(X171,esk35_3(X169,X170,X171))|p4(X171)|~r1(X170,X171)|~r1(X169,X170)|~r1(esk1_0,X169))&(~p1(esk35_3(X169,X170,X171))|p4(X171)|~r1(X170,X171)|~r1(X169,X170)|~r1(esk1_0,X169))))&((r1(X175,esk36_3(X173,X174,X175))|p3(X175)|~r1(X174,X175)|~r1(X173,X174)|~r1(esk1_0,X173))&(~p5(esk36_3(X173,X174,X175))|p3(X175)|~r1(X174,X175)|~r1(X173,X174)|~r1(esk1_0,X173))))&((r1(X179,esk37_3(X177,X178,X179))|p3(X179)|~r1(X178,X179)|~r1(X177,X178)|~r1(esk1_0,X177))&(~p3(esk37_3(X177,X178,X179))|p3(X179)|~r1(X178,X179)|~r1(X177,X178)|~r1(esk1_0,X177))))&((r1(X182,esk38_2(X181,X182))|p6(X182)|~r1(X181,X182)|~r1(esk1_0,X181))&(~p2(esk38_2(X181,X182))|p6(X182)|~r1(X181,X182)|~r1(esk1_0,X181))))&((r1(X185,esk39_2(X184,X185))|p4(X185)|~r1(X184,X185)|~r1(esk1_0,X184))&(~p2(esk39_2(X184,X185))|p4(X185)|~r1(X184,X185)|~r1(esk1_0,X184))))&((r1(X188,esk40_2(X187,X188))|p2(X188)|~r1(X187,X188)|~r1(esk1_0,X187))&(~p2(esk40_2(X187,X188))|p2(X188)|~r1(X187,X188)|~r1(esk1_0,X187))))&((r1(X192,esk41_3(X190,X191,X192))|p1(X192)|~r1(X191,X192)|~r1(X190,X191)|~r1(esk1_0,X190))&(~p5(esk41_3(X190,X191,X192))|p1(X192)|~r1(X191,X192)|~r1(X190,X191)|~r1(esk1_0,X190))))&((r1(X196,esk42_3(X194,X195,X196))|p1(X196)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))&(~p3(esk42_3(X194,X195,X196))|p1(X196)|~r1(X195,X196)|~r1(X194,X195)|~r1(esk1_0,X194))))&((r1(X198,esk43_1(X198))|p6(X198)|~r1(esk1_0,X198))&(~p6(esk43_1(X198))|p6(X198)|~r1(esk1_0,X198))))&((r1(X200,esk44_1(X200))|p4(X200)|~r1(esk1_0,X200))&(~p6(esk44_1(X200))|p4(X200)|~r1(esk1_0,X200))))&((r1(X203,esk45_2(X202,X203))|p5(X203)|~r1(X202,X203)|~r1(esk1_0,X202))&(~p5(esk45_2(X202,X203))|p5(X203)|~r1(X202,X203)|~r1(esk1_0,X202))))&((r1(X206,esk46_2(X205,X206))|p5(X206)|~r1(X205,X206)|~r1(esk1_0,X205))&(~p3(esk46_2(X205,X206))|p5(X206)|~r1(X205,X206)|~r1(esk1_0,X205))))&((r1(X209,esk47_2(X208,X209))|p5(X209)|~r1(X208,X209)|~r1(esk1_0,X208))&(~p1(esk47_2(X208,X209))|p5(X209)|~r1(X208,X209)|~r1(esk1_0,X208))))&((r1(X211,esk48_1(X211))|p6(X211)|~r1(esk1_0,X211))&(~p4(esk48_1(X211))|p6(X211)|~r1(esk1_0,X211))))&((r1(X213,esk49_1(X213))|p4(X213)|~r1(esk1_0,X213))&(~p4(esk49_1(X213))|p4(X213)|~r1(esk1_0,X213))))&((r1(X216,esk50_2(X215,X216))|p3(X216)|~r1(X215,X216)|~r1(esk1_0,X215))&(~p5(esk50_2(X215,X216))|p3(X216)|~r1(X215,X216)|~r1(esk1_0,X215))))&((r1(X219,esk51_2(X218,X219))|p3(X219)|~r1(X218,X219)|~r1(esk1_0,X218))&(~p3(esk51_2(X218,X219))|p3(X219)|~r1(X218,X219)|~r1(esk1_0,X218))))&((r1(X222,esk52_2(X221,X222))|p3(X222)|~r1(X221,X222)|~r1(esk1_0,X221))&(~p1(esk52_2(X221,X222))|p3(X222)|~r1(X221,X222)|~r1(esk1_0,X221))))&((r1(X224,esk53_1(X224))|p6(X224)|~r1(esk1_0,X224))&(~p2(esk53_1(X224))|p6(X224)|~r1(esk1_0,X224))))&((r1(X226,esk54_1(X226))|p4(X226)|~r1(esk1_0,X226))&(~p2(esk54_1(X226))|p4(X226)|~r1(esk1_0,X226))))&((r1(X229,esk55_2(X228,X229))|p1(X229)|~r1(X228,X229)|~r1(esk1_0,X228))&(~p5(esk55_2(X228,X229))|p1(X229)|~r1(X228,X229)|~r1(esk1_0,X228))))&((r1(X232,esk56_2(X231,X232))|p1(X232)|~r1(X231,X232)|~r1(esk1_0,X231))&(~p4(esk56_2(X231,X232))|p1(X232)|~r1(X231,X232)|~r1(esk1_0,X231))))&((r1(X235,esk57_2(X234,X235))|p1(X235)|~r1(X234,X235)|~r1(esk1_0,X234))&(~p3(esk57_2(X234,X235))|p1(X235)|~r1(X234,X235)|~r1(esk1_0,X234))))&((r1(X238,esk58_2(X237,X238))|p1(X238)|~r1(X237,X238)|~r1(esk1_0,X237))&(~p1(esk58_2(X237,X238))|p1(X238)|~r1(X237,X238)|~r1(esk1_0,X237))))&((r1(X240,esk59_1(X240))|p5(X240)|~r1(esk1_0,X240))&(~p5(esk59_1(X240))|p5(X240)|~r1(esk1_0,X240))))&((r1(X242,esk60_1(X242))|p5(X242)|~r1(esk1_0,X242))&(~p3(esk60_1(X242))|p5(X242)|~r1(esk1_0,X242))))&((r1(X244,esk61_1(X244))|p3(X244)|~r1(esk1_0,X244))&(~p5(esk61_1(X244))|p3(X244)|~r1(esk1_0,X244))))&((r1(X246,esk62_1(X246))|p3(X246)|~r1(esk1_0,X246))&(~p3(esk62_1(X246))|p3(X246)|~r1(esk1_0,X246))))&((r1(X248,esk63_1(X248))|p2(X248)|~r1(esk1_0,X248))&(~p1(esk63_1(X248))|p2(X248)|~r1(esk1_0,X248))))&((r1(X250,esk64_1(X250))|p1(X250)|~r1(esk1_0,X250))&(~p5(esk64_1(X250))|p1(X250)|~r1(esk1_0,X250))))&((r1(X252,esk65_1(X252))|p1(X252)|~r1(esk1_0,X252))&(~p3(esk65_1(X252))|p1(X252)|~r1(esk1_0,X252))))&(r1(esk1_0,esk66_0)&~p5(esk66_0)))&(r1(esk1_0,esk67_0)&~p3(esk67_0)))&(r1(esk1_0,esk68_0)&~p2(esk68_0)))&(r1(esk1_0,esk69_0)&~p1(esk69_0)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])])])])).
% 26.97/4.02 cnf(c_0_3, negated_conjecture, (r1(X1,esk56_2(X2,X1))|p1(X1)|~r1(X2,X1)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_4, negated_conjecture, (r1(esk1_0,esk68_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_5, negated_conjecture, (r1(X1,esk63_1(X1))|p2(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_6, negated_conjecture, (~p2(esk68_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_7, negated_conjecture, (r1(X1,esk35_3(X2,X3,X1))|p4(X1)|~r1(X3,X1)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_8, negated_conjecture, (p1(X1)|r1(X1,esk56_2(esk68_0,X1))|~r1(esk68_0,X1)), inference(spm,[status(thm)],[c_0_3, c_0_4])).
% 26.97/4.02 cnf(c_0_9, negated_conjecture, (r1(esk68_0,esk63_1(esk68_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5, c_0_4]), c_0_6])).
% 26.97/4.02 cnf(c_0_10, negated_conjecture, (p1(X2)|~p4(esk56_2(X1,X2))|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_11, negated_conjecture, (p4(X1)|r1(X1,esk35_3(esk68_0,X2,X1))|~r1(esk68_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_7, c_0_4])).
% 26.97/4.02 cnf(c_0_12, negated_conjecture, (p2(X1)|~p1(esk63_1(X1))|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_13, negated_conjecture, (p1(esk63_1(esk68_0))|r1(esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))), inference(spm,[status(thm)],[c_0_8, c_0_9])).
% 26.97/4.02 cnf(c_0_14, negated_conjecture, (r1(X1,esk24_4(X2,X3,X4,X1))|p1(X1)|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_15, negated_conjecture, (p1(X1)|~p4(esk56_2(esk68_0,X1))|~r1(esk68_0,X1)), inference(spm,[status(thm)],[c_0_10, c_0_4])).
% 26.97/4.02 cnf(c_0_16, negated_conjecture, (p4(X1)|r1(X1,esk35_3(esk68_0,esk63_1(esk68_0),X1))|~r1(esk63_1(esk68_0),X1)), inference(spm,[status(thm)],[c_0_11, c_0_9])).
% 26.97/4.02 cnf(c_0_17, negated_conjecture, (r1(esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_13]), c_0_4])]), c_0_6])).
% 26.97/4.02 cnf(c_0_18, negated_conjecture, (p4(X3)|~p1(esk35_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_19, negated_conjecture, (p1(X1)|r1(X1,esk24_4(esk68_0,X2,X3,X1))|~r1(esk68_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_14, c_0_4])).
% 26.97/4.02 cnf(c_0_20, negated_conjecture, (p1(esk63_1(esk68_0))|~p4(esk56_2(esk68_0,esk63_1(esk68_0)))), inference(spm,[status(thm)],[c_0_15, c_0_9])).
% 26.97/4.02 cnf(c_0_21, negated_conjecture, (p4(esk56_2(esk68_0,esk63_1(esk68_0)))|r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))), inference(spm,[status(thm)],[c_0_16, c_0_17])).
% 26.97/4.02 cnf(c_0_22, negated_conjecture, (p4(X1)|~p1(esk35_3(esk68_0,X2,X1))|~r1(esk68_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_18, c_0_4])).
% 26.97/4.02 cnf(c_0_23, negated_conjecture, (p1(X1)|r1(X1,esk24_4(esk68_0,esk63_1(esk68_0),X2,X1))|~r1(esk63_1(esk68_0),X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_19, c_0_9])).
% 26.97/4.02 cnf(c_0_24, negated_conjecture, (p1(esk63_1(esk68_0))|r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 26.97/4.02 cnf(c_0_25, negated_conjecture, (p4(X5)|~r1(esk1_0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|~r1(X4,X5)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_26, negated_conjecture, (p4(X1)|~p1(esk35_3(esk68_0,esk63_1(esk68_0),X1))|~r1(esk63_1(esk68_0),X1)), inference(spm,[status(thm)],[c_0_22, c_0_9])).
% 26.97/4.02 cnf(c_0_27, negated_conjecture, (p1(X1)|r1(X1,esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),X1))|~r1(esk56_2(esk68_0,esk63_1(esk68_0)),X1)), inference(spm,[status(thm)],[c_0_23, c_0_17])).
% 26.97/4.02 cnf(c_0_28, negated_conjecture, (r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_24]), c_0_4])]), c_0_6])).
% 26.97/4.02 cnf(c_0_29, negated_conjecture, (p1(X4)|~p4(esk24_4(X1,X2,X3,X4))|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 26.97/4.02 cnf(c_0_30, negated_conjecture, (p4(X1)|~r1(esk68_0,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_25, c_0_4])).
% 26.97/4.02 cnf(c_0_31, negated_conjecture, (p4(esk56_2(esk68_0,esk63_1(esk68_0)))|~p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))), inference(spm,[status(thm)],[c_0_26, c_0_17])).
% 26.97/4.02 cnf(c_0_32, negated_conjecture, (p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))|r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 26.97/4.02 cnf(c_0_33, negated_conjecture, (p1(X1)|~p4(esk24_4(esk68_0,X2,X3,X1))|~r1(esk68_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_29, c_0_4])).
% 26.97/4.02 cnf(c_0_34, negated_conjecture, (p4(X1)|~r1(esk63_1(esk68_0),X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_30, c_0_9])).
% 26.97/4.02 cnf(c_0_35, negated_conjecture, (p4(esk56_2(esk68_0,esk63_1(esk68_0)))|r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 26.97/4.02 cnf(c_0_36, negated_conjecture, (p1(X1)|~p4(esk24_4(esk68_0,esk63_1(esk68_0),X2,X1))|~r1(esk63_1(esk68_0),X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_33, c_0_9])).
% 26.97/4.02 cnf(c_0_37, negated_conjecture, (p4(X1)|~r1(esk56_2(esk68_0,esk63_1(esk68_0)),X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_34, c_0_17])).
% 26.97/4.02 cnf(c_0_38, negated_conjecture, (p1(esk63_1(esk68_0))|r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(spm,[status(thm)],[c_0_20, c_0_35])).
% 26.97/4.02 cnf(c_0_39, negated_conjecture, (p1(X1)|~p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),X1))|~r1(esk56_2(esk68_0,esk63_1(esk68_0)),X1)), inference(spm,[status(thm)],[c_0_36, c_0_17])).
% 26.97/4.02 cnf(c_0_40, negated_conjecture, (p4(X1)|~r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),X1)), inference(spm,[status(thm)],[c_0_37, c_0_28])).
% 26.97/4.02 cnf(c_0_41, negated_conjecture, (r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_38]), c_0_4])]), c_0_6])).
% 26.97/4.02 cnf(c_0_42, negated_conjecture, (p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))|~p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(spm,[status(thm)],[c_0_39, c_0_28])).
% 26.97/4.02 cnf(c_0_43, negated_conjecture, (p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))))), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 26.97/4.02 cnf(c_0_44, negated_conjecture, (p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 26.97/4.02 cnf(c_0_45, negated_conjecture, (p4(esk56_2(esk68_0,esk63_1(esk68_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_44])])).
% 26.97/4.02 cnf(c_0_46, negated_conjecture, (p1(esk63_1(esk68_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_45])])).
% 26.97/4.02 cnf(c_0_47, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12, c_0_46]), c_0_4])]), c_0_6]), ['proof']).
% 26.97/4.02 % SZS output end Proof
% 26.97/4.02 % User time : 3.248 s
% 26.97/4.02 % System time : 0.094 s
% 26.97/4.02 % Total time : 3.342 s
% 26.97/4.02 % User time : 3.254 s
% 26.97/4.02 % System time : 0.100 s
% 26.97/4.02 % Total time : 3.354 s
% 26.97/4.02
%------------------------------------------------------------------------------