%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n007.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:30 AM UTC 2026
% Result : Theorem 93.27s 14.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL682+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.36 % Computer : n007.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 13:44:24 UTC 2026
% 0.01/0.36 % CPUTime :
% 0.25/0.48 start to proof:theBenchmark.p
% 93.27/14.56 % Version : CSI_E---1.1
% 93.27/14.56 % Problem : theBenchmark.p
% 93.27/14.56 % Proof found!
% 93.27/14.56 % SZS status Theorem for theBenchmark.p
% 93.27/14.56 % SZS output start Proof
% 93.27/14.56 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|p56(X1))))|~(![X1]:((~(r1(X2,X1))|p54(X1))))|~(![X1]:((~(r1(X2,X1))|p54(X1))))|~(![X1]:((~(r1(X2,X1))|p52(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p56(X2)))&~(p46(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p56(X2)))&~(p44(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p56(X2)))&~(p42(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p54(X2)))&~(p46(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p54(X2)))&~(p44(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p54(X2)))&~(p42(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p52(X2)))&~(p46(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p52(X2)))&~(p44(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p52(X2)))&~(p42(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p46(X1)))&~(p36(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p46(X1)))&~(p32(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p55(X2)))&~(p45(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p53(X2)))&~(p45(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p51(X2)))&~(p45(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p44(X1)))&~(p36(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p44(X1)))&~(p32(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p55(X2)))&~(p43(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p53(X2)))&~(p43(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p51(X2)))&~(p43(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p42(X1)))&~(p36(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p42(X1)))&~(p32(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p55(X2)))&~(p41(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p54(X2)))&~(p41(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p53(X2)))&~(p41(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p51(X2)))&~(p41(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p36(X2)))&~(p26(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p36(X2)))&~(p24(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p36(X2)))&~(p22(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p45(X1)))&~(p35(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p43(X1)))&~(p35(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p34(X2)))&~(p26(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p34(X2)))&~(p24(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p34(X2)))&~(p22(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p41(X1)))&~(p34(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p45(X1)))&~(p33(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p43(X1)))&~(p33(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p32(X2)))&~(p26(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p32(X2)))&~(p24(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p32(X2)))&~(p22(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p45(X1)))&~(p31(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p43(X1)))&~(p31(X2)))))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p26(X1)))&~(p16(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p26(X1)))&~(p14(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p35(X2)))&~(p25(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p33(X2)))&~(p25(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p31(X2)))&~(p25(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p24(X1)))&~(p16(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p24(X1)))&~(p14(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p35(X2)))&~(p23(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p33(X2)))&~(p23(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p31(X2)))&~(p23(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p22(X1)))&~(p16(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p22(X1)))&~(p14(X2)))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p35(X2)))&~(p21(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p34(X2)))&~(p21(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p33(X2)))&~(p21(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p31(X2)))&~(p21(X1)))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p25(X1)))&~(p15(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p23(X1)))&~(p15(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p25(X1)))&~(p13(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p23(X1)))&~(p13(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p21(X1)))&~(p12(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p25(X1)))&~(p11(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|p23(X1)))&~(p11(X2)))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p15(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p13(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p12(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p11(X1))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 93.27/14.56 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', reflexivity)).
% 93.27/14.56 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', transitivity)).
% 93.27/14.56 fof(c_0_3, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|p56(X1))))|~(![X1]:((~r1(X2,X1)|p54(X1))))|~(![X1]:((~r1(X2,X1)|p54(X1))))|~(![X1]:((~r1(X2,X1)|p52(X1)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p56(X2)))&~p46(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p56(X2)))&~p44(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p56(X2)))&~p42(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p54(X2)))&~p46(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p54(X2)))&~p44(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p54(X2)))&~p42(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p52(X2)))&~p46(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p52(X2)))&~p44(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p52(X2)))&~p42(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p46(X1)))&~p36(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p46(X1)))&~p32(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p55(X2)))&~p45(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p53(X2)))&~p45(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p51(X2)))&~p45(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p44(X1)))&~p36(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p44(X1)))&~p32(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p55(X2)))&~p43(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p53(X2)))&~p43(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p51(X2)))&~p43(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p42(X1)))&~p36(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p42(X1)))&~p32(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p55(X2)))&~p41(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p54(X2)))&~p41(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p53(X2)))&~p41(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p51(X2)))&~p41(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p36(X2)))&~p26(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p36(X2)))&~p24(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p36(X2)))&~p22(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p45(X1)))&~p35(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p43(X1)))&~p35(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p34(X2)))&~p26(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p34(X2)))&~p24(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p34(X2)))&~p22(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p41(X1)))&~p34(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p45(X1)))&~p33(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p43(X1)))&~p33(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p32(X2)))&~p26(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p32(X2)))&~p24(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p32(X2)))&~p22(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p45(X1)))&~p31(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p43(X1)))&~p31(X2))))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p26(X1)))&~p16(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p26(X1)))&~p14(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p35(X2)))&~p25(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p33(X2)))&~p25(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p31(X2)))&~p25(X1))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p24(X1)))&~p16(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p24(X1)))&~p14(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p35(X2)))&~p23(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p33(X2)))&~p23(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p31(X2)))&~p23(X1))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p22(X1)))&~p16(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p22(X1)))&~p14(X2))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p35(X2)))&~p21(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p34(X2)))&~p21(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p33(X2)))&~p21(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p31(X2)))&~p21(X1))))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p25(X1)))&~p15(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p23(X1)))&~p15(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p25(X1)))&~p13(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p23(X1)))&~p13(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p21(X1)))&~p12(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p25(X1)))&~p11(X2))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|p23(X1)))&~p11(X2))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p15(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p13(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p12(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p11(X1)))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 93.27/14.56 fof(c_0_4, negated_conjecture, ![X9, X10, X11, X12, X13, X14, X15, X16, X17, X19, X20, X21, X22, 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, X63, X64, X65, X67, X68, X69, X70, X72, X73, X74, X75, X77, X78, X79, X80, X82, X83, X84, X86, X87, X88, X90, X91, X92, X93, X95, X96, X97, X98, X100, X101, X102, X103, X105, X106, X107, X109, X110, X111, X113, X114, X115, X116, X118, X119, X120, X121, X123, X124, X125, X126, X128, X129, X130, X131, X133, X134, X136, X137, X139, X140, X142, X143, X144, X146, X147, X148, X150, X151, X153, X154, X156, X157, X159, X160, X161, X163, X164, X165, X167, X168, X169, X171, X172, X174, X175, X177, X178, X180, X181, X182, X184, X185, X186, X188, X190, X192, X193, X195, X196, X198, X199, X201, X203, X205, X206, X208, X209, X211, X212, X214, X216, X218, X219, X221, X222, X224, X225, X227, X228, X230, X232, X234, X236, X238, X240, X242]:(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~r1(X9,X10)|p56(X10)|~r1(esk1_0,X9))&(~r1(X9,X11)|p54(X11)|~r1(esk1_0,X9)))&(~r1(X9,X12)|p54(X12)|~r1(esk1_0,X9)))&(~r1(X9,X13)|p52(X13)|~r1(esk1_0,X9)))&((r1(X17,esk2_4(X14,X15,X16,X17))|p46(X17)|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(esk1_0,X14))&(~p56(esk2_4(X14,X15,X16,X17))|p46(X17)|~r1(X16,X17)|~r1(X15,X16)|~r1(X14,X15)|~r1(esk1_0,X14))))&((r1(X22,esk3_4(X19,X20,X21,X22))|p44(X22)|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(esk1_0,X19))&(~p56(esk3_4(X19,X20,X21,X22))|p44(X22)|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(esk1_0,X19))))&((r1(X27,esk4_4(X24,X25,X26,X27))|p42(X27)|~r1(X26,X27)|~r1(X25,X26)|~r1(X24,X25)|~r1(esk1_0,X24))&(~p56(esk4_4(X24,X25,X26,X27))|p42(X27)|~r1(X26,X27)|~r1(X25,X26)|~r1(X24,X25)|~r1(esk1_0,X24))))&((r1(X32,esk5_4(X29,X30,X31,X32))|p46(X32)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(esk1_0,X29))&(~p54(esk5_4(X29,X30,X31,X32))|p46(X32)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(esk1_0,X29))))&((r1(X37,esk6_4(X34,X35,X36,X37))|p44(X37)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(esk1_0,X34))&(~p54(esk6_4(X34,X35,X36,X37))|p44(X37)|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(esk1_0,X34))))&((r1(X42,esk7_4(X39,X40,X41,X42))|p42(X42)|~r1(X41,X42)|~r1(X40,X41)|~r1(X39,X40)|~r1(esk1_0,X39))&(~p54(esk7_4(X39,X40,X41,X42))|p42(X42)|~r1(X41,X42)|~r1(X40,X41)|~r1(X39,X40)|~r1(esk1_0,X39))))&((r1(X47,esk8_4(X44,X45,X46,X47))|p46(X47)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(esk1_0,X44))&(~p52(esk8_4(X44,X45,X46,X47))|p46(X47)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(esk1_0,X44))))&((r1(X52,esk9_4(X49,X50,X51,X52))|p44(X52)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))&(~p52(esk9_4(X49,X50,X51,X52))|p44(X52)|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(esk1_0,X49))))&((r1(X57,esk10_4(X54,X55,X56,X57))|p42(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))&(~p52(esk10_4(X54,X55,X56,X57))|p42(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))))&((r1(X61,esk11_3(X59,X60,X61))|p36(X61)|~r1(X60,X61)|~r1(X59,X60)|~r1(esk1_0,X59))&(~p46(esk11_3(X59,X60,X61))|p36(X61)|~r1(X60,X61)|~r1(X59,X60)|~r1(esk1_0,X59))))&((r1(X65,esk12_3(X63,X64,X65))|p32(X65)|~r1(X64,X65)|~r1(X63,X64)|~r1(esk1_0,X63))&(~p46(esk12_3(X63,X64,X65))|p32(X65)|~r1(X64,X65)|~r1(X63,X64)|~r1(esk1_0,X63))))&((r1(X70,esk13_4(X67,X68,X69,X70))|p45(X70)|~r1(X69,X70)|~r1(X68,X69)|~r1(X67,X68)|~r1(esk1_0,X67))&(~p55(esk13_4(X67,X68,X69,X70))|p45(X70)|~r1(X69,X70)|~r1(X68,X69)|~r1(X67,X68)|~r1(esk1_0,X67))))&((r1(X75,esk14_4(X72,X73,X74,X75))|p45(X75)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(esk1_0,X72))&(~p53(esk14_4(X72,X73,X74,X75))|p45(X75)|~r1(X74,X75)|~r1(X73,X74)|~r1(X72,X73)|~r1(esk1_0,X72))))&((r1(X80,esk15_4(X77,X78,X79,X80))|p45(X80)|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(esk1_0,X77))&(~p51(esk15_4(X77,X78,X79,X80))|p45(X80)|~r1(X79,X80)|~r1(X78,X79)|~r1(X77,X78)|~r1(esk1_0,X77))))&((r1(X84,esk16_3(X82,X83,X84))|p36(X84)|~r1(X83,X84)|~r1(X82,X83)|~r1(esk1_0,X82))&(~p44(esk16_3(X82,X83,X84))|p36(X84)|~r1(X83,X84)|~r1(X82,X83)|~r1(esk1_0,X82))))&((r1(X88,esk17_3(X86,X87,X88))|p32(X88)|~r1(X87,X88)|~r1(X86,X87)|~r1(esk1_0,X86))&(~p44(esk17_3(X86,X87,X88))|p32(X88)|~r1(X87,X88)|~r1(X86,X87)|~r1(esk1_0,X86))))&((r1(X93,esk18_4(X90,X91,X92,X93))|p43(X93)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))&(~p55(esk18_4(X90,X91,X92,X93))|p43(X93)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(esk1_0,X90))))&((r1(X98,esk19_4(X95,X96,X97,X98))|p43(X98)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(esk1_0,X95))&(~p53(esk19_4(X95,X96,X97,X98))|p43(X98)|~r1(X97,X98)|~r1(X96,X97)|~r1(X95,X96)|~r1(esk1_0,X95))))&((r1(X103,esk20_4(X100,X101,X102,X103))|p43(X103)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))&(~p51(esk20_4(X100,X101,X102,X103))|p43(X103)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))))&((r1(X107,esk21_3(X105,X106,X107))|p36(X107)|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))&(~p42(esk21_3(X105,X106,X107))|p36(X107)|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))))&((r1(X111,esk22_3(X109,X110,X111))|p32(X111)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))&(~p42(esk22_3(X109,X110,X111))|p32(X111)|~r1(X110,X111)|~r1(X109,X110)|~r1(esk1_0,X109))))&((r1(X116,esk23_4(X113,X114,X115,X116))|p41(X116)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(esk1_0,X113))&(~p55(esk23_4(X113,X114,X115,X116))|p41(X116)|~r1(X115,X116)|~r1(X114,X115)|~r1(X113,X114)|~r1(esk1_0,X113))))&((r1(X121,esk24_4(X118,X119,X120,X121))|p41(X121)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(esk1_0,X118))&(~p54(esk24_4(X118,X119,X120,X121))|p41(X121)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(esk1_0,X118))))&((r1(X126,esk25_4(X123,X124,X125,X126))|p41(X126)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(esk1_0,X123))&(~p53(esk25_4(X123,X124,X125,X126))|p41(X126)|~r1(X125,X126)|~r1(X124,X125)|~r1(X123,X124)|~r1(esk1_0,X123))))&((r1(X131,esk26_4(X128,X129,X130,X131))|p41(X131)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(esk1_0,X128))&(~p51(esk26_4(X128,X129,X130,X131))|p41(X131)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(esk1_0,X128))))&((r1(X134,esk27_2(X133,X134))|p26(X134)|~r1(X133,X134)|~r1(esk1_0,X133))&(~p36(esk27_2(X133,X134))|p26(X134)|~r1(X133,X134)|~r1(esk1_0,X133))))&((r1(X137,esk28_2(X136,X137))|p24(X137)|~r1(X136,X137)|~r1(esk1_0,X136))&(~p36(esk28_2(X136,X137))|p24(X137)|~r1(X136,X137)|~r1(esk1_0,X136))))&((r1(X140,esk29_2(X139,X140))|p22(X140)|~r1(X139,X140)|~r1(esk1_0,X139))&(~p36(esk29_2(X139,X140))|p22(X140)|~r1(X139,X140)|~r1(esk1_0,X139))))&((r1(X144,esk30_3(X142,X143,X144))|p35(X144)|~r1(X143,X144)|~r1(X142,X143)|~r1(esk1_0,X142))&(~p45(esk30_3(X142,X143,X144))|p35(X144)|~r1(X143,X144)|~r1(X142,X143)|~r1(esk1_0,X142))))&((r1(X148,esk31_3(X146,X147,X148))|p35(X148)|~r1(X147,X148)|~r1(X146,X147)|~r1(esk1_0,X146))&(~p43(esk31_3(X146,X147,X148))|p35(X148)|~r1(X147,X148)|~r1(X146,X147)|~r1(esk1_0,X146))))&((r1(X151,esk32_2(X150,X151))|p26(X151)|~r1(X150,X151)|~r1(esk1_0,X150))&(~p34(esk32_2(X150,X151))|p26(X151)|~r1(X150,X151)|~r1(esk1_0,X150))))&((r1(X154,esk33_2(X153,X154))|p24(X154)|~r1(X153,X154)|~r1(esk1_0,X153))&(~p34(esk33_2(X153,X154))|p24(X154)|~r1(X153,X154)|~r1(esk1_0,X153))))&((r1(X157,esk34_2(X156,X157))|p22(X157)|~r1(X156,X157)|~r1(esk1_0,X156))&(~p34(esk34_2(X156,X157))|p22(X157)|~r1(X156,X157)|~r1(esk1_0,X156))))&((r1(X161,esk35_3(X159,X160,X161))|p34(X161)|~r1(X160,X161)|~r1(X159,X160)|~r1(esk1_0,X159))&(~p41(esk35_3(X159,X160,X161))|p34(X161)|~r1(X160,X161)|~r1(X159,X160)|~r1(esk1_0,X159))))&((r1(X165,esk36_3(X163,X164,X165))|p33(X165)|~r1(X164,X165)|~r1(X163,X164)|~r1(esk1_0,X163))&(~p45(esk36_3(X163,X164,X165))|p33(X165)|~r1(X164,X165)|~r1(X163,X164)|~r1(esk1_0,X163))))&((r1(X169,esk37_3(X167,X168,X169))|p33(X169)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167))&(~p43(esk37_3(X167,X168,X169))|p33(X169)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167))))&((r1(X172,esk38_2(X171,X172))|p26(X172)|~r1(X171,X172)|~r1(esk1_0,X171))&(~p32(esk38_2(X171,X172))|p26(X172)|~r1(X171,X172)|~r1(esk1_0,X171))))&((r1(X175,esk39_2(X174,X175))|p24(X175)|~r1(X174,X175)|~r1(esk1_0,X174))&(~p32(esk39_2(X174,X175))|p24(X175)|~r1(X174,X175)|~r1(esk1_0,X174))))&((r1(X178,esk40_2(X177,X178))|p22(X178)|~r1(X177,X178)|~r1(esk1_0,X177))&(~p32(esk40_2(X177,X178))|p22(X178)|~r1(X177,X178)|~r1(esk1_0,X177))))&((r1(X182,esk41_3(X180,X181,X182))|p31(X182)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))&(~p45(esk41_3(X180,X181,X182))|p31(X182)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))))&((r1(X186,esk42_3(X184,X185,X186))|p31(X186)|~r1(X185,X186)|~r1(X184,X185)|~r1(esk1_0,X184))&(~p43(esk42_3(X184,X185,X186))|p31(X186)|~r1(X185,X186)|~r1(X184,X185)|~r1(esk1_0,X184))))&((r1(X188,esk43_1(X188))|p16(X188)|~r1(esk1_0,X188))&(~p26(esk43_1(X188))|p16(X188)|~r1(esk1_0,X188))))&((r1(X190,esk44_1(X190))|p14(X190)|~r1(esk1_0,X190))&(~p26(esk44_1(X190))|p14(X190)|~r1(esk1_0,X190))))&((r1(X193,esk45_2(X192,X193))|p25(X193)|~r1(X192,X193)|~r1(esk1_0,X192))&(~p35(esk45_2(X192,X193))|p25(X193)|~r1(X192,X193)|~r1(esk1_0,X192))))&((r1(X196,esk46_2(X195,X196))|p25(X196)|~r1(X195,X196)|~r1(esk1_0,X195))&(~p33(esk46_2(X195,X196))|p25(X196)|~r1(X195,X196)|~r1(esk1_0,X195))))&((r1(X199,esk47_2(X198,X199))|p25(X199)|~r1(X198,X199)|~r1(esk1_0,X198))&(~p31(esk47_2(X198,X199))|p25(X199)|~r1(X198,X199)|~r1(esk1_0,X198))))&((r1(X201,esk48_1(X201))|p16(X201)|~r1(esk1_0,X201))&(~p24(esk48_1(X201))|p16(X201)|~r1(esk1_0,X201))))&((r1(X203,esk49_1(X203))|p14(X203)|~r1(esk1_0,X203))&(~p24(esk49_1(X203))|p14(X203)|~r1(esk1_0,X203))))&((r1(X206,esk50_2(X205,X206))|p23(X206)|~r1(X205,X206)|~r1(esk1_0,X205))&(~p35(esk50_2(X205,X206))|p23(X206)|~r1(X205,X206)|~r1(esk1_0,X205))))&((r1(X209,esk51_2(X208,X209))|p23(X209)|~r1(X208,X209)|~r1(esk1_0,X208))&(~p33(esk51_2(X208,X209))|p23(X209)|~r1(X208,X209)|~r1(esk1_0,X208))))&((r1(X212,esk52_2(X211,X212))|p23(X212)|~r1(X211,X212)|~r1(esk1_0,X211))&(~p31(esk52_2(X211,X212))|p23(X212)|~r1(X211,X212)|~r1(esk1_0,X211))))&((r1(X214,esk53_1(X214))|p16(X214)|~r1(esk1_0,X214))&(~p22(esk53_1(X214))|p16(X214)|~r1(esk1_0,X214))))&((r1(X216,esk54_1(X216))|p14(X216)|~r1(esk1_0,X216))&(~p22(esk54_1(X216))|p14(X216)|~r1(esk1_0,X216))))&((r1(X219,esk55_2(X218,X219))|p21(X219)|~r1(X218,X219)|~r1(esk1_0,X218))&(~p35(esk55_2(X218,X219))|p21(X219)|~r1(X218,X219)|~r1(esk1_0,X218))))&((r1(X222,esk56_2(X221,X222))|p21(X222)|~r1(X221,X222)|~r1(esk1_0,X221))&(~p34(esk56_2(X221,X222))|p21(X222)|~r1(X221,X222)|~r1(esk1_0,X221))))&((r1(X225,esk57_2(X224,X225))|p21(X225)|~r1(X224,X225)|~r1(esk1_0,X224))&(~p33(esk57_2(X224,X225))|p21(X225)|~r1(X224,X225)|~r1(esk1_0,X224))))&((r1(X228,esk58_2(X227,X228))|p21(X228)|~r1(X227,X228)|~r1(esk1_0,X227))&(~p31(esk58_2(X227,X228))|p21(X228)|~r1(X227,X228)|~r1(esk1_0,X227))))&((r1(X230,esk59_1(X230))|p15(X230)|~r1(esk1_0,X230))&(~p25(esk59_1(X230))|p15(X230)|~r1(esk1_0,X230))))&((r1(X232,esk60_1(X232))|p15(X232)|~r1(esk1_0,X232))&(~p23(esk60_1(X232))|p15(X232)|~r1(esk1_0,X232))))&((r1(X234,esk61_1(X234))|p13(X234)|~r1(esk1_0,X234))&(~p25(esk61_1(X234))|p13(X234)|~r1(esk1_0,X234))))&((r1(X236,esk62_1(X236))|p13(X236)|~r1(esk1_0,X236))&(~p23(esk62_1(X236))|p13(X236)|~r1(esk1_0,X236))))&((r1(X238,esk63_1(X238))|p12(X238)|~r1(esk1_0,X238))&(~p21(esk63_1(X238))|p12(X238)|~r1(esk1_0,X238))))&((r1(X240,esk64_1(X240))|p11(X240)|~r1(esk1_0,X240))&(~p25(esk64_1(X240))|p11(X240)|~r1(esk1_0,X240))))&((r1(X242,esk65_1(X242))|p11(X242)|~r1(esk1_0,X242))&(~p23(esk65_1(X242))|p11(X242)|~r1(esk1_0,X242))))&(r1(esk1_0,esk66_0)&(r1(esk66_0,esk67_0)&~p15(esk67_0))))&(r1(esk1_0,esk68_0)&(r1(esk68_0,esk69_0)&~p13(esk69_0))))&(r1(esk1_0,esk70_0)&(r1(esk70_0,esk71_0)&~p12(esk71_0))))&(r1(esk1_0,esk72_0)&(r1(esk72_0,esk73_0)&~p11(esk73_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_3])])])])])])).
% 93.27/14.56 fof(c_0_5, plain, ![X4]:(r1(X4,X4)), inference(variable_rename,[status(thm)],[reflexivity])).
% 93.27/14.56 cnf(c_0_6, negated_conjecture, (p54(X2)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_7, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 93.27/14.56 fof(c_0_8, plain, ![X5, X6, X7]:((~r1(X5,X6)|~r1(X6,X7)|r1(X5,X7))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])])).
% 93.27/14.56 cnf(c_0_9, negated_conjecture, (p41(X4)|~p54(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_4])).
% 93.27/14.56 cnf(c_0_10, negated_conjecture, (p54(X1)|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 93.27/14.56 cnf(c_0_11, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 93.27/14.56 cnf(c_0_12, negated_conjecture, (r1(X1,esk24_4(X2,X3,X4,X1))|p41(X1)|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_13, negated_conjecture, (p41(X1)|~r1(esk1_0,esk24_4(X2,X3,X4,X1))|~r1(esk1_0,X2)|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 93.27/14.56 cnf(c_0_14, negated_conjecture, (p41(X1)|r1(X2,esk24_4(X3,X4,X5,X1))|~r1(esk1_0,X3)|~r1(X2,X1)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_11, c_0_12])).
% 93.27/14.56 cnf(c_0_15, negated_conjecture, (p41(X1)|~r1(esk1_0,X2)|~r1(esk1_0,X1)|~r1(X3,X1)|~r1(X4,X3)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 93.27/14.56 cnf(c_0_16, negated_conjecture, (p41(X1)|~r1(esk1_0,X1)|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_15, c_0_7])).
% 93.27/14.56 cnf(c_0_17, negated_conjecture, (r1(esk1_0,esk70_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_18, negated_conjecture, (p41(X1)|~r1(esk1_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_7]), c_0_11])).
% 93.27/14.56 cnf(c_0_19, negated_conjecture, (r1(X1,esk70_0)|~r1(X1,esk1_0)), inference(spm,[status(thm)],[c_0_11, c_0_17])).
% 93.27/14.56 cnf(c_0_20, negated_conjecture, (p34(X3)|~p41(esk35_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_21, negated_conjecture, (p41(X1)|~r1(esk70_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_18, c_0_19]), c_0_7])])).
% 93.27/14.56 cnf(c_0_22, negated_conjecture, (r1(X1,esk35_3(X2,X3,X1))|p34(X1)|~r1(X3,X1)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_23, negated_conjecture, (p34(X1)|~r1(esk70_0,esk35_3(X2,X3,X1))|~r1(esk1_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 93.27/14.56 cnf(c_0_24, negated_conjecture, (p34(X1)|r1(X2,esk35_3(X3,X4,X1))|~r1(esk1_0,X3)|~r1(X2,X1)|~r1(X4,X1)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_11, c_0_22])).
% 93.27/14.56 cnf(c_0_25, negated_conjecture, (p34(X1)|~r1(esk1_0,X2)|~r1(esk70_0,X1)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 93.27/14.56 cnf(c_0_26, negated_conjecture, (p34(X1)|~r1(esk70_0,X2)|~r1(X2,X1)), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_19]), c_0_7])]), c_0_11])).
% 93.27/14.56 cnf(c_0_27, negated_conjecture, (p21(X2)|~p34(esk56_2(X1,X2))|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_28, negated_conjecture, (p34(X1)|~r1(esk70_0,X1)), inference(spm,[status(thm)],[c_0_26, c_0_7])).
% 93.27/14.56 cnf(c_0_29, negated_conjecture, (r1(X1,esk56_2(X2,X1))|p21(X1)|~r1(X2,X1)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_30, negated_conjecture, (p21(X1)|~r1(esk70_0,esk56_2(X2,X1))|~r1(esk1_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 93.27/14.56 cnf(c_0_31, negated_conjecture, (p21(X1)|r1(X2,esk56_2(X3,X1))|~r1(esk1_0,X3)|~r1(X2,X1)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_11, c_0_29])).
% 93.27/14.56 cnf(c_0_32, negated_conjecture, (p21(X1)|~r1(esk1_0,X2)|~r1(esk70_0,X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 93.27/14.56 cnf(c_0_33, negated_conjecture, (p12(X1)|~p21(esk63_1(X1))|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_34, negated_conjecture, (p21(X1)|~r1(esk70_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32, c_0_19]), c_0_7])])).
% 93.27/14.56 cnf(c_0_35, negated_conjecture, (r1(X1,esk63_1(X1))|p12(X1)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_36, negated_conjecture, (p12(X1)|~r1(esk70_0,esk63_1(X1))|~r1(esk1_0,X1)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 93.27/14.56 cnf(c_0_37, negated_conjecture, (p12(X1)|r1(X2,esk63_1(X1))|~r1(esk1_0,X1)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_11, c_0_35])).
% 93.27/14.56 cnf(c_0_38, negated_conjecture, (~p12(esk71_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_39, negated_conjecture, (p12(X1)|~r1(esk1_0,X1)|~r1(esk70_0,X1)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 93.27/14.56 cnf(c_0_40, negated_conjecture, (r1(esk70_0,esk71_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 93.27/14.56 cnf(c_0_41, negated_conjecture, (~r1(esk1_0,esk71_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_38, c_0_39]), c_0_40])])).
% 93.27/14.56 cnf(c_0_42, negated_conjecture, (r1(X1,esk71_0)|~r1(X1,esk70_0)), inference(spm,[status(thm)],[c_0_11, c_0_40])).
% 93.27/14.56 cnf(c_0_43, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_42]), c_0_17])]), ['proof']).
% 93.27/14.56 % SZS output end Proof
% 93.27/14.56 % User time : 12.753 s
% 93.27/14.56 % System time : 0.191 s
% 93.27/14.56 % Total time : 12.944 s
% 93.27/14.56 % User time : 64.910 s
% 93.27/14.56 % System time : 0.768 s
% 93.27/14.56 % Total time : 65.678 s
% 93.27/14.56
%------------------------------------------------------------------------------