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