%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL652+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:20 AM UTC 2026
% Result : Theorem 149.51s 22.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL652+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 14:37:58 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.23/0.46 start to proof:theBenchmark.p
% 149.51/22.12 % Version : CSI_E---1.1
% 149.51/22.12 % Problem : theBenchmark.p
% 149.51/22.12 % Proof found!
% 149.51/22.12 % SZS status Theorem for theBenchmark.p
% 149.51/22.12 % SZS output start Proof
% 149.51/22.12 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|~(p4(X2)))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1))))))))|~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|~((![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1)))))))&p2(X2))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1))))))))))))))))|(~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1))))))))|~(![X2]:((~(r1(X1,X2))|~((![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p2(X2)))))))&![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p3(X2)))|~(p2(X1)))))))))))))))|(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p3(X1)))|~(p2(X2))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p2(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))|~(![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2))))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p2(X1)))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))|~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(p1(X1))))))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(p1(X2))))))|~(![X1]:((~(r1(X2,X1))|~(p1(X1)))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 149.51/22.12 fof(c_0_1, plain, ![X1]:((epred5_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 149.51/22.12 fof(c_0_2, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|~p4(X2))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred5_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p2(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~p1(X1)))))|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~p1(X2)))))|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]), c_0_1])).
% 149.51/22.12 fof(c_0_3, negated_conjecture, ![X4, X5, X6, X7, X10, X11, X12, X13, X14, X17, X18, X19, X20, X21, X24, X25, X26, X27, X28, X31, X32, X33, X34, X35, X37, X38, X39, X41, X42, X43, X45, X46, X47, X51, X56, X61, X66, X71, X76, X81, X86, X91, X96, X101, X106, X111, X116, X121, X126, X131, X136, X141, X146, X149, X151, X152, X153, X155, X156, X157, X159, X160, X161, X163, X164, X165, X167, X168, X169, X171, X172, X173, X175, X176, X177, X179, X180, X181, X183, X184, X185, X187, X188, X189, X191, X192, X193, X195, X196, X197, X199, X200, X201, X203, X204, X205, X207, X208, X209, X211, X212, X213, X215, X216, X217, X219, X220, X221, X223, X224, X225, X227, X228, X229]:((((((((~r1(esk1_0,X4)|~p4(X4))&(((r1(X5,esk3_1(X5))|(r1(X7,esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5))&(~r1(esk3_1(X5),X10)|~p1(X10)|(r1(X7,esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5)))&((r1(X5,esk3_1(X5))|(p1(esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5))&(~r1(esk3_1(X5),X10)|~p1(X10)|(p1(esk2_3(X5,X6,X7))|~r1(X6,X7)|~r1(X5,X6))|~r1(esk1_0,X5)))))&(((((r1(X12,esk5_2(X11,X12))|(r1(X14,esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))&(~r1(esk5_2(X11,X12),X17)|~p1(X17)|(r1(X14,esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11)))&((r1(X12,esk5_2(X11,X12))|(p1(esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))&(~r1(esk5_2(X11,X12),X17)|~p1(X17)|(p1(esk4_4(X11,X12,X13,X14))|~r1(X13,X14)|~r1(X12,X13))|~r1(X11,X12)|~r1(esk1_0,X11))))&(((((r1(X19,esk7_3(X11,X18,X19))|(r1(X21,esk6_5(X11,X18,X19,X20,X21))|~r1(X20,X21)|~r1(X19,X20))|~r1(X18,X19)|~r1(X11,X18)|~r1(esk1_0,X11))&(~r1(esk7_3(X11,X18,X19),X24)|~p1(X24)|(r1(X21,esk6_5(X11,X18,X19,X20,X21))|~r1(X20,X21)|~r1(X19,X20))|~r1(X18,X19)|~r1(X11,X18)|~r1(esk1_0,X11)))&((r1(X19,esk7_3(X11,X18,X19))|(p1(esk6_5(X11,X18,X19,X20,X21))|~r1(X20,X21)|~r1(X19,X20))|~r1(X18,X19)|~r1(X11,X18)|~r1(esk1_0,X11))&(~r1(esk7_3(X11,X18,X19),X24)|~p1(X24)|(p1(esk6_5(X11,X18,X19,X20,X21))|~r1(X20,X21)|~r1(X19,X20))|~r1(X18,X19)|~r1(X11,X18)|~r1(esk1_0,X11))))&(((((r1(X26,esk9_4(X11,X18,X25,X26))|(r1(X28,esk8_6(X11,X18,X25,X26,X27,X28))|~r1(X27,X28)|~r1(X26,X27))|~r1(X25,X26)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11))&(~r1(esk9_4(X11,X18,X25,X26),X31)|~p1(X31)|(r1(X28,esk8_6(X11,X18,X25,X26,X27,X28))|~r1(X27,X28)|~r1(X26,X27))|~r1(X25,X26)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11)))&((r1(X26,esk9_4(X11,X18,X25,X26))|(p1(esk8_6(X11,X18,X25,X26,X27,X28))|~r1(X27,X28)|~r1(X26,X27))|~r1(X25,X26)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11))&(~r1(esk9_4(X11,X18,X25,X26),X31)|~p1(X31)|(p1(esk8_6(X11,X18,X25,X26,X27,X28))|~r1(X27,X28)|~r1(X26,X27))|~r1(X25,X26)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11))))&(~r1(X25,X32)|epred5_1(X32)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11)))&((r1(X33,esk10_4(X11,X18,X25,X33))|(~r1(X33,X34)|(~r1(X34,X35)|p1(X35)))|~r1(X25,X33)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11))&(~p1(esk10_4(X11,X18,X25,X33))|(~r1(X33,X34)|(~r1(X34,X35)|p1(X35)))|~r1(X25,X33)|~r1(X18,X25)|~r1(X11,X18)|~r1(esk1_0,X11)))))&((r1(X37,esk11_3(X11,X18,X37))|(~r1(X37,X38)|(~r1(X38,X39)|p1(X39)))|~r1(X18,X37)|~r1(X11,X18)|~r1(esk1_0,X11))&(~p1(esk11_3(X11,X18,X37))|(~r1(X37,X38)|(~r1(X38,X39)|p1(X39)))|~r1(X18,X37)|~r1(X11,X18)|~r1(esk1_0,X11)))))&((r1(X41,esk12_2(X11,X41))|(~r1(X41,X42)|(~r1(X42,X43)|p1(X43)))|~r1(X11,X41)|~r1(esk1_0,X11))&(~p1(esk12_2(X11,X41))|(~r1(X41,X42)|(~r1(X42,X43)|p1(X43)))|~r1(X11,X41)|~r1(esk1_0,X11)))))&((r1(X45,esk13_1(X45))|(~r1(X45,X46)|(~r1(X46,X47)|p1(X47)))|~r1(esk1_0,X45))&(~p1(esk13_1(X45))|(~r1(X45,X46)|(~r1(X46,X47)|p1(X47)))|~r1(esk1_0,X45))))&((r1(esk1_0,esk14_0)&(r1(esk14_0,esk15_0)&(~r1(esk15_0,X51)|p1(X51))))&(r1(esk14_0,esk16_0)&~p1(esk16_0))))&(((r1(esk1_0,esk17_0)&((r1(esk17_0,esk18_0)&(r1(esk18_0,esk19_0)&(~r1(esk19_0,X56)|p1(X56))))&(r1(esk18_0,esk20_0)&~p1(esk20_0))))&(((r1(esk17_0,esk21_0)&((r1(esk21_0,esk22_0)&(r1(esk22_0,esk23_0)&(~r1(esk23_0,X61)|p1(X61))))&(r1(esk22_0,esk24_0)&~p1(esk24_0))))&(((r1(esk21_0,esk25_0)&((r1(esk25_0,esk26_0)&(r1(esk26_0,esk27_0)&(~r1(esk27_0,X66)|p1(X66))))&(r1(esk26_0,esk28_0)&~p1(esk28_0))))&(((r1(esk25_0,esk29_0)&((r1(esk29_0,esk30_0)&(r1(esk30_0,esk31_0)&(~r1(esk31_0,X71)|p1(X71))))&(r1(esk30_0,esk32_0)&~p1(esk32_0))))&(((r1(esk29_0,esk33_0)&((r1(esk33_0,esk34_0)&(r1(esk34_0,esk35_0)&(~r1(esk35_0,X76)|p1(X76))))&(r1(esk34_0,esk36_0)&~p1(esk36_0))))&(((r1(esk33_0,esk37_0)&((r1(esk37_0,esk38_0)&(r1(esk38_0,esk39_0)&(~r1(esk39_0,X81)|p1(X81))))&(r1(esk38_0,esk40_0)&~p1(esk40_0))))&(((r1(esk37_0,esk41_0)&((r1(esk41_0,esk42_0)&(r1(esk42_0,esk43_0)&(~r1(esk43_0,X86)|p1(X86))))&(r1(esk42_0,esk44_0)&~p1(esk44_0))))&(((r1(esk41_0,esk45_0)&((r1(esk45_0,esk46_0)&(r1(esk46_0,esk47_0)&(~r1(esk47_0,X91)|p1(X91))))&(r1(esk46_0,esk48_0)&~p1(esk48_0))))&(((r1(esk45_0,esk49_0)&((r1(esk49_0,esk50_0)&(r1(esk50_0,esk51_0)&(~r1(esk51_0,X96)|p1(X96))))&(r1(esk50_0,esk52_0)&~p1(esk52_0))))&(((r1(esk49_0,esk53_0)&((r1(esk53_0,esk54_0)&(r1(esk54_0,esk55_0)&(~r1(esk55_0,X101)|p1(X101))))&(r1(esk54_0,esk56_0)&~p1(esk56_0))))&(((r1(esk53_0,esk57_0)&((r1(esk57_0,esk58_0)&(r1(esk58_0,esk59_0)&(~r1(esk59_0,X106)|p1(X106))))&(r1(esk58_0,esk60_0)&~p1(esk60_0))))&(((r1(esk57_0,esk61_0)&((r1(esk61_0,esk62_0)&(r1(esk62_0,esk63_0)&(~r1(esk63_0,X111)|p1(X111))))&(r1(esk62_0,esk64_0)&~p1(esk64_0))))&(((r1(esk61_0,esk65_0)&((r1(esk65_0,esk66_0)&(r1(esk66_0,esk67_0)&(~r1(esk67_0,X116)|p1(X116))))&(r1(esk66_0,esk68_0)&~p1(esk68_0))))&(((r1(esk65_0,esk69_0)&((r1(esk69_0,esk70_0)&(r1(esk70_0,esk71_0)&(~r1(esk71_0,X121)|p1(X121))))&(r1(esk70_0,esk72_0)&~p1(esk72_0))))&(((r1(esk69_0,esk73_0)&((r1(esk73_0,esk74_0)&(r1(esk74_0,esk75_0)&(~r1(esk75_0,X126)|p1(X126))))&(r1(esk74_0,esk76_0)&~p1(esk76_0))))&(((r1(esk73_0,esk77_0)&((r1(esk77_0,esk78_0)&(r1(esk78_0,esk79_0)&(~r1(esk79_0,X131)|p1(X131))))&(r1(esk78_0,esk80_0)&~p1(esk80_0))))&(((r1(esk77_0,esk81_0)&((r1(esk81_0,esk82_0)&(r1(esk82_0,esk83_0)&(~r1(esk83_0,X136)|p1(X136))))&(r1(esk82_0,esk84_0)&~p1(esk84_0))))&(((r1(esk81_0,esk85_0)&((r1(esk85_0,esk86_0)&(r1(esk86_0,esk87_0)&(~r1(esk87_0,X141)|p1(X141))))&(r1(esk86_0,esk88_0)&~p1(esk88_0))))&(((r1(esk85_0,esk89_0)&((r1(esk89_0,esk90_0)&(r1(esk90_0,esk91_0)&(~r1(esk91_0,X146)|p1(X146))))&(r1(esk90_0,esk92_0)&~p1(esk92_0))))&(r1(esk89_0,esk93_0)&((r1(X149,esk94_1(X149))|~r1(esk93_0,X149))&(~p2(esk94_1(X149))|~r1(esk93_0,X149)))))&((r1(X151,esk95_1(X151))|(~r1(esk89_0,X151)|(~r1(X151,X152)|(~r1(X152,X153)|~p1(X153)))))&(p1(esk95_1(X151))|(~r1(esk89_0,X151)|(~r1(X151,X152)|(~r1(X152,X153)|~p1(X153))))))))&((r1(X155,esk96_1(X155))|(~r1(esk85_0,X155)|(~r1(X155,X156)|(~r1(X156,X157)|~p1(X157)))))&(p1(esk96_1(X155))|(~r1(esk85_0,X155)|(~r1(X155,X156)|(~r1(X156,X157)|~p1(X157))))))))&((r1(X159,esk97_1(X159))|(~r1(esk81_0,X159)|(~r1(X159,X160)|(~r1(X160,X161)|~p1(X161)))))&(p1(esk97_1(X159))|(~r1(esk81_0,X159)|(~r1(X159,X160)|(~r1(X160,X161)|~p1(X161))))))))&((r1(X163,esk98_1(X163))|(~r1(esk77_0,X163)|(~r1(X163,X164)|(~r1(X164,X165)|~p1(X165)))))&(p1(esk98_1(X163))|(~r1(esk77_0,X163)|(~r1(X163,X164)|(~r1(X164,X165)|~p1(X165))))))))&((r1(X167,esk99_1(X167))|(~r1(esk73_0,X167)|(~r1(X167,X168)|(~r1(X168,X169)|~p1(X169)))))&(p1(esk99_1(X167))|(~r1(esk73_0,X167)|(~r1(X167,X168)|(~r1(X168,X169)|~p1(X169))))))))&((r1(X171,esk100_1(X171))|(~r1(esk69_0,X171)|(~r1(X171,X172)|(~r1(X172,X173)|~p1(X173)))))&(p1(esk100_1(X171))|(~r1(esk69_0,X171)|(~r1(X171,X172)|(~r1(X172,X173)|~p1(X173))))))))&((r1(X175,esk101_1(X175))|(~r1(esk65_0,X175)|(~r1(X175,X176)|(~r1(X176,X177)|~p1(X177)))))&(p1(esk101_1(X175))|(~r1(esk65_0,X175)|(~r1(X175,X176)|(~r1(X176,X177)|~p1(X177))))))))&((r1(X179,esk102_1(X179))|(~r1(esk61_0,X179)|(~r1(X179,X180)|(~r1(X180,X181)|~p1(X181)))))&(p1(esk102_1(X179))|(~r1(esk61_0,X179)|(~r1(X179,X180)|(~r1(X180,X181)|~p1(X181))))))))&((r1(X183,esk103_1(X183))|(~r1(esk57_0,X183)|(~r1(X183,X184)|(~r1(X184,X185)|~p1(X185)))))&(p1(esk103_1(X183))|(~r1(esk57_0,X183)|(~r1(X183,X184)|(~r1(X184,X185)|~p1(X185))))))))&((r1(X187,esk104_1(X187))|(~r1(esk53_0,X187)|(~r1(X187,X188)|(~r1(X188,X189)|~p1(X189)))))&(p1(esk104_1(X187))|(~r1(esk53_0,X187)|(~r1(X187,X188)|(~r1(X188,X189)|~p1(X189))))))))&((r1(X191,esk105_1(X191))|(~r1(esk49_0,X191)|(~r1(X191,X192)|(~r1(X192,X193)|~p1(X193)))))&(p1(esk105_1(X191))|(~r1(esk49_0,X191)|(~r1(X191,X192)|(~r1(X192,X193)|~p1(X193))))))))&((r1(X195,esk106_1(X195))|(~r1(esk45_0,X195)|(~r1(X195,X196)|(~r1(X196,X197)|~p1(X197)))))&(p1(esk106_1(X195))|(~r1(esk45_0,X195)|(~r1(X195,X196)|(~r1(X196,X197)|~p1(X197))))))))&((r1(X199,esk107_1(X199))|(~r1(esk41_0,X199)|(~r1(X199,X200)|(~r1(X200,X201)|~p1(X201)))))&(p1(esk107_1(X199))|(~r1(esk41_0,X199)|(~r1(X199,X200)|(~r1(X200,X201)|~p1(X201))))))))&((r1(X203,esk108_1(X203))|(~r1(esk37_0,X203)|(~r1(X203,X204)|(~r1(X204,X205)|~p1(X205)))))&(p1(esk108_1(X203))|(~r1(esk37_0,X203)|(~r1(X203,X204)|(~r1(X204,X205)|~p1(X205))))))))&((r1(X207,esk109_1(X207))|(~r1(esk33_0,X207)|(~r1(X207,X208)|(~r1(X208,X209)|~p1(X209)))))&(p1(esk109_1(X207))|(~r1(esk33_0,X207)|(~r1(X207,X208)|(~r1(X208,X209)|~p1(X209))))))))&((r1(X211,esk110_1(X211))|(~r1(esk29_0,X211)|(~r1(X211,X212)|(~r1(X212,X213)|~p1(X213)))))&(p1(esk110_1(X211))|(~r1(esk29_0,X211)|(~r1(X211,X212)|(~r1(X212,X213)|~p1(X213))))))))&((r1(X215,esk111_1(X215))|(~r1(esk25_0,X215)|(~r1(X215,X216)|(~r1(X216,X217)|~p1(X217)))))&(p1(esk111_1(X215))|(~r1(esk25_0,X215)|(~r1(X215,X216)|(~r1(X216,X217)|~p1(X217))))))))&((r1(X219,esk112_1(X219))|(~r1(esk21_0,X219)|(~r1(X219,X220)|(~r1(X220,X221)|~p1(X221)))))&(p1(esk112_1(X219))|(~r1(esk21_0,X219)|(~r1(X219,X220)|(~r1(X220,X221)|~p1(X221))))))))&((r1(X223,esk113_1(X223))|(~r1(esk17_0,X223)|(~r1(X223,X224)|(~r1(X224,X225)|~p1(X225)))))&(p1(esk113_1(X223))|(~r1(esk17_0,X223)|(~r1(X223,X224)|(~r1(X224,X225)|~p1(X225))))))))&((r1(X227,esk114_1(X227))|(~r1(esk1_0,X227)|(~r1(X227,X228)|(~r1(X228,X229)|~p1(X229)))))&(p1(esk114_1(X227))|(~r1(esk1_0,X227)|(~r1(X227,X228)|(~r1(X228,X229)|~p1(X229)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])])).
% 149.51/22.12 cnf(c_0_4, negated_conjecture, (epred5_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(esk1_0,X4)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_5, negated_conjecture, (r1(esk1_0,esk17_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_6, plain, ![X1]:((epred4_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 149.51/22.12 cnf(c_0_7, negated_conjecture, (epred5_1(X1)|~r1(esk17_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_4, c_0_5])).
% 149.51/22.12 cnf(c_0_8, negated_conjecture, (r1(esk17_0,esk21_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_9, plain, ![X1]:((epred5_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred4_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1]), c_0_6])).
% 149.51/22.12 cnf(c_0_10, negated_conjecture, (epred5_1(X1)|~r1(esk21_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 149.51/22.12 cnf(c_0_11, negated_conjecture, (r1(esk21_0,esk25_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_12, plain, ![X393, X394, X395, X396, X399, X400, X401, X402, X403, X406, X407, X408, X409, X410, X413, X414, X415, X416, X417, X420, X421, X422, X423, X424, X426, X427, X428, X430, X431, X432, X434, X435, X436]:((((((r1(X394,esk166_2(X393,X394))|(r1(X396,esk165_4(X393,X394,X395,X396))|~r1(X395,X396)|~r1(X394,X395))|~r1(X393,X394)|~epred5_1(X393))&(~r1(esk166_2(X393,X394),X399)|~p1(X399)|(r1(X396,esk165_4(X393,X394,X395,X396))|~r1(X395,X396)|~r1(X394,X395))|~r1(X393,X394)|~epred5_1(X393)))&((r1(X394,esk166_2(X393,X394))|(p1(esk165_4(X393,X394,X395,X396))|~r1(X395,X396)|~r1(X394,X395))|~r1(X393,X394)|~epred5_1(X393))&(~r1(esk166_2(X393,X394),X399)|~p1(X399)|(p1(esk165_4(X393,X394,X395,X396))|~r1(X395,X396)|~r1(X394,X395))|~r1(X393,X394)|~epred5_1(X393))))&(((((r1(X401,esk168_3(X393,X400,X401))|(r1(X403,esk167_5(X393,X400,X401,X402,X403))|~r1(X402,X403)|~r1(X401,X402))|~r1(X400,X401)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk168_3(X393,X400,X401),X406)|~p1(X406)|(r1(X403,esk167_5(X393,X400,X401,X402,X403))|~r1(X402,X403)|~r1(X401,X402))|~r1(X400,X401)|~r1(X393,X400)|~epred5_1(X393)))&((r1(X401,esk168_3(X393,X400,X401))|(p1(esk167_5(X393,X400,X401,X402,X403))|~r1(X402,X403)|~r1(X401,X402))|~r1(X400,X401)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk168_3(X393,X400,X401),X406)|~p1(X406)|(p1(esk167_5(X393,X400,X401,X402,X403))|~r1(X402,X403)|~r1(X401,X402))|~r1(X400,X401)|~r1(X393,X400)|~epred5_1(X393))))&(((((r1(X408,esk170_4(X393,X400,X407,X408))|(r1(X410,esk169_6(X393,X400,X407,X408,X409,X410))|~r1(X409,X410)|~r1(X408,X409))|~r1(X407,X408)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk170_4(X393,X400,X407,X408),X413)|~p1(X413)|(r1(X410,esk169_6(X393,X400,X407,X408,X409,X410))|~r1(X409,X410)|~r1(X408,X409))|~r1(X407,X408)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393)))&((r1(X408,esk170_4(X393,X400,X407,X408))|(p1(esk169_6(X393,X400,X407,X408,X409,X410))|~r1(X409,X410)|~r1(X408,X409))|~r1(X407,X408)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk170_4(X393,X400,X407,X408),X413)|~p1(X413)|(p1(esk169_6(X393,X400,X407,X408,X409,X410))|~r1(X409,X410)|~r1(X408,X409))|~r1(X407,X408)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))))&(((((r1(X415,esk172_5(X393,X400,X407,X414,X415))|(r1(X417,esk171_7(X393,X400,X407,X414,X415,X416,X417))|~r1(X416,X417)|~r1(X415,X416))|~r1(X414,X415)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk172_5(X393,X400,X407,X414,X415),X420)|~p1(X420)|(r1(X417,esk171_7(X393,X400,X407,X414,X415,X416,X417))|~r1(X416,X417)|~r1(X415,X416))|~r1(X414,X415)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393)))&((r1(X415,esk172_5(X393,X400,X407,X414,X415))|(p1(esk171_7(X393,X400,X407,X414,X415,X416,X417))|~r1(X416,X417)|~r1(X415,X416))|~r1(X414,X415)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~r1(esk172_5(X393,X400,X407,X414,X415),X420)|~p1(X420)|(p1(esk171_7(X393,X400,X407,X414,X415,X416,X417))|~r1(X416,X417)|~r1(X415,X416))|~r1(X414,X415)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))))&(~r1(X414,X421)|epred4_1(X421)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393)))&((r1(X422,esk173_5(X393,X400,X407,X414,X422))|(~r1(X422,X423)|(~r1(X423,X424)|p1(X424)))|~r1(X414,X422)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~p1(esk173_5(X393,X400,X407,X414,X422))|(~r1(X422,X423)|(~r1(X423,X424)|p1(X424)))|~r1(X414,X422)|~r1(X407,X414)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393)))))&((r1(X426,esk174_4(X393,X400,X407,X426))|(~r1(X426,X427)|(~r1(X427,X428)|p1(X428)))|~r1(X407,X426)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393))&(~p1(esk174_4(X393,X400,X407,X426))|(~r1(X426,X427)|(~r1(X427,X428)|p1(X428)))|~r1(X407,X426)|~r1(X400,X407)|~r1(X393,X400)|~epred5_1(X393)))))&((r1(X430,esk175_3(X393,X400,X430))|(~r1(X430,X431)|(~r1(X431,X432)|p1(X432)))|~r1(X400,X430)|~r1(X393,X400)|~epred5_1(X393))&(~p1(esk175_3(X393,X400,X430))|(~r1(X430,X431)|(~r1(X431,X432)|p1(X432)))|~r1(X400,X430)|~r1(X393,X400)|~epred5_1(X393)))))&((r1(X434,esk176_2(X393,X434))|(~r1(X434,X435)|(~r1(X435,X436)|p1(X436)))|~r1(X393,X434)|~epred5_1(X393))&(~p1(esk176_2(X393,X434))|(~r1(X434,X435)|(~r1(X435,X436)|p1(X436)))|~r1(X393,X434)|~epred5_1(X393))))), 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_9])])])])])])).
% 149.51/22.12 cnf(c_0_13, negated_conjecture, (epred5_1(X1)|~r1(esk25_0,X1)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 149.51/22.12 cnf(c_0_14, negated_conjecture, (r1(esk25_0,esk29_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_15, plain, ![X1]:((epred3_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 149.51/22.12 cnf(c_0_16, plain, (epred4_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred5_1(X5)), inference(split_conjunct,[status(thm)],[c_0_12])).
% 149.51/22.12 cnf(c_0_17, negated_conjecture, (r1(esk29_0,esk33_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_18, negated_conjecture, (epred5_1(esk29_0)), inference(spm,[status(thm)],[c_0_13, c_0_14])).
% 149.51/22.12 fof(c_0_19, plain, ![X1]:((epred4_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred3_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_6]), c_0_15])).
% 149.51/22.12 cnf(c_0_20, negated_conjecture, (epred4_1(X1)|~r1(esk33_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18])])).
% 149.51/22.12 cnf(c_0_21, negated_conjecture, (r1(esk33_0,esk37_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_22, plain, ![X348, X349, X350, X351, X354, X355, X356, X357, X358, X361, X362, X363, X364, X365, X368, X369, X370, X371, X372, X375, X376, X377, X378, X379, X381, X382, X383, X385, X386, X387, X389, X390, X391]:((((((r1(X349,esk154_2(X348,X349))|(r1(X351,esk153_4(X348,X349,X350,X351))|~r1(X350,X351)|~r1(X349,X350))|~r1(X348,X349)|~epred4_1(X348))&(~r1(esk154_2(X348,X349),X354)|~p1(X354)|(r1(X351,esk153_4(X348,X349,X350,X351))|~r1(X350,X351)|~r1(X349,X350))|~r1(X348,X349)|~epred4_1(X348)))&((r1(X349,esk154_2(X348,X349))|(p1(esk153_4(X348,X349,X350,X351))|~r1(X350,X351)|~r1(X349,X350))|~r1(X348,X349)|~epred4_1(X348))&(~r1(esk154_2(X348,X349),X354)|~p1(X354)|(p1(esk153_4(X348,X349,X350,X351))|~r1(X350,X351)|~r1(X349,X350))|~r1(X348,X349)|~epred4_1(X348))))&(((((r1(X356,esk156_3(X348,X355,X356))|(r1(X358,esk155_5(X348,X355,X356,X357,X358))|~r1(X357,X358)|~r1(X356,X357))|~r1(X355,X356)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk156_3(X348,X355,X356),X361)|~p1(X361)|(r1(X358,esk155_5(X348,X355,X356,X357,X358))|~r1(X357,X358)|~r1(X356,X357))|~r1(X355,X356)|~r1(X348,X355)|~epred4_1(X348)))&((r1(X356,esk156_3(X348,X355,X356))|(p1(esk155_5(X348,X355,X356,X357,X358))|~r1(X357,X358)|~r1(X356,X357))|~r1(X355,X356)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk156_3(X348,X355,X356),X361)|~p1(X361)|(p1(esk155_5(X348,X355,X356,X357,X358))|~r1(X357,X358)|~r1(X356,X357))|~r1(X355,X356)|~r1(X348,X355)|~epred4_1(X348))))&(((((r1(X363,esk158_4(X348,X355,X362,X363))|(r1(X365,esk157_6(X348,X355,X362,X363,X364,X365))|~r1(X364,X365)|~r1(X363,X364))|~r1(X362,X363)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk158_4(X348,X355,X362,X363),X368)|~p1(X368)|(r1(X365,esk157_6(X348,X355,X362,X363,X364,X365))|~r1(X364,X365)|~r1(X363,X364))|~r1(X362,X363)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348)))&((r1(X363,esk158_4(X348,X355,X362,X363))|(p1(esk157_6(X348,X355,X362,X363,X364,X365))|~r1(X364,X365)|~r1(X363,X364))|~r1(X362,X363)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk158_4(X348,X355,X362,X363),X368)|~p1(X368)|(p1(esk157_6(X348,X355,X362,X363,X364,X365))|~r1(X364,X365)|~r1(X363,X364))|~r1(X362,X363)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))))&(((((r1(X370,esk160_5(X348,X355,X362,X369,X370))|(r1(X372,esk159_7(X348,X355,X362,X369,X370,X371,X372))|~r1(X371,X372)|~r1(X370,X371))|~r1(X369,X370)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk160_5(X348,X355,X362,X369,X370),X375)|~p1(X375)|(r1(X372,esk159_7(X348,X355,X362,X369,X370,X371,X372))|~r1(X371,X372)|~r1(X370,X371))|~r1(X369,X370)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348)))&((r1(X370,esk160_5(X348,X355,X362,X369,X370))|(p1(esk159_7(X348,X355,X362,X369,X370,X371,X372))|~r1(X371,X372)|~r1(X370,X371))|~r1(X369,X370)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~r1(esk160_5(X348,X355,X362,X369,X370),X375)|~p1(X375)|(p1(esk159_7(X348,X355,X362,X369,X370,X371,X372))|~r1(X371,X372)|~r1(X370,X371))|~r1(X369,X370)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))))&(~r1(X369,X376)|epred3_1(X376)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348)))&((r1(X377,esk161_5(X348,X355,X362,X369,X377))|(~r1(X377,X378)|(~r1(X378,X379)|p1(X379)))|~r1(X369,X377)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~p1(esk161_5(X348,X355,X362,X369,X377))|(~r1(X377,X378)|(~r1(X378,X379)|p1(X379)))|~r1(X369,X377)|~r1(X362,X369)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348)))))&((r1(X381,esk162_4(X348,X355,X362,X381))|(~r1(X381,X382)|(~r1(X382,X383)|p1(X383)))|~r1(X362,X381)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348))&(~p1(esk162_4(X348,X355,X362,X381))|(~r1(X381,X382)|(~r1(X382,X383)|p1(X383)))|~r1(X362,X381)|~r1(X355,X362)|~r1(X348,X355)|~epred4_1(X348)))))&((r1(X385,esk163_3(X348,X355,X385))|(~r1(X385,X386)|(~r1(X386,X387)|p1(X387)))|~r1(X355,X385)|~r1(X348,X355)|~epred4_1(X348))&(~p1(esk163_3(X348,X355,X385))|(~r1(X385,X386)|(~r1(X386,X387)|p1(X387)))|~r1(X355,X385)|~r1(X348,X355)|~epred4_1(X348)))))&((r1(X389,esk164_2(X348,X389))|(~r1(X389,X390)|(~r1(X390,X391)|p1(X391)))|~r1(X348,X389)|~epred4_1(X348))&(~p1(esk164_2(X348,X389))|(~r1(X389,X390)|(~r1(X390,X391)|p1(X391)))|~r1(X348,X389)|~epred4_1(X348))))), 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_19])])])])])])).
% 149.51/22.12 cnf(c_0_23, negated_conjecture, (epred4_1(X1)|~r1(esk37_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 149.51/22.12 cnf(c_0_24, negated_conjecture, (r1(esk37_0,esk41_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_25, plain, (epred3_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred4_1(X5)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 149.51/22.12 cnf(c_0_26, negated_conjecture, (r1(esk45_0,esk49_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_27, negated_conjecture, (epred4_1(X1)|~r1(esk41_0,X1)), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 149.51/22.12 cnf(c_0_28, negated_conjecture, (r1(esk41_0,esk45_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_29, plain, ![X1]:((epred2_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), introduced(definition)).
% 149.51/22.12 cnf(c_0_30, negated_conjecture, (epred3_1(X1)|~epred4_1(esk45_0)|~r1(esk49_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_25, c_0_26])).
% 149.51/22.12 cnf(c_0_31, negated_conjecture, (epred4_1(esk45_0)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 149.51/22.12 fof(c_0_32, plain, ![X1]:((epred3_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred2_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_15]), c_0_29])).
% 149.51/22.12 cnf(c_0_33, negated_conjecture, (epred3_1(X1)|~r1(esk49_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 149.51/22.12 cnf(c_0_34, negated_conjecture, (r1(esk49_0,esk53_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_35, plain, ![X303, X304, X305, X306, X309, X310, X311, X312, X313, X316, X317, X318, X319, X320, X323, X324, X325, X326, X327, X330, X331, X332, X333, X334, X336, X337, X338, X340, X341, X342, X344, X345, X346]:((((((r1(X304,esk142_2(X303,X304))|(r1(X306,esk141_4(X303,X304,X305,X306))|~r1(X305,X306)|~r1(X304,X305))|~r1(X303,X304)|~epred3_1(X303))&(~r1(esk142_2(X303,X304),X309)|~p1(X309)|(r1(X306,esk141_4(X303,X304,X305,X306))|~r1(X305,X306)|~r1(X304,X305))|~r1(X303,X304)|~epred3_1(X303)))&((r1(X304,esk142_2(X303,X304))|(p1(esk141_4(X303,X304,X305,X306))|~r1(X305,X306)|~r1(X304,X305))|~r1(X303,X304)|~epred3_1(X303))&(~r1(esk142_2(X303,X304),X309)|~p1(X309)|(p1(esk141_4(X303,X304,X305,X306))|~r1(X305,X306)|~r1(X304,X305))|~r1(X303,X304)|~epred3_1(X303))))&(((((r1(X311,esk144_3(X303,X310,X311))|(r1(X313,esk143_5(X303,X310,X311,X312,X313))|~r1(X312,X313)|~r1(X311,X312))|~r1(X310,X311)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk144_3(X303,X310,X311),X316)|~p1(X316)|(r1(X313,esk143_5(X303,X310,X311,X312,X313))|~r1(X312,X313)|~r1(X311,X312))|~r1(X310,X311)|~r1(X303,X310)|~epred3_1(X303)))&((r1(X311,esk144_3(X303,X310,X311))|(p1(esk143_5(X303,X310,X311,X312,X313))|~r1(X312,X313)|~r1(X311,X312))|~r1(X310,X311)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk144_3(X303,X310,X311),X316)|~p1(X316)|(p1(esk143_5(X303,X310,X311,X312,X313))|~r1(X312,X313)|~r1(X311,X312))|~r1(X310,X311)|~r1(X303,X310)|~epred3_1(X303))))&(((((r1(X318,esk146_4(X303,X310,X317,X318))|(r1(X320,esk145_6(X303,X310,X317,X318,X319,X320))|~r1(X319,X320)|~r1(X318,X319))|~r1(X317,X318)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk146_4(X303,X310,X317,X318),X323)|~p1(X323)|(r1(X320,esk145_6(X303,X310,X317,X318,X319,X320))|~r1(X319,X320)|~r1(X318,X319))|~r1(X317,X318)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303)))&((r1(X318,esk146_4(X303,X310,X317,X318))|(p1(esk145_6(X303,X310,X317,X318,X319,X320))|~r1(X319,X320)|~r1(X318,X319))|~r1(X317,X318)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk146_4(X303,X310,X317,X318),X323)|~p1(X323)|(p1(esk145_6(X303,X310,X317,X318,X319,X320))|~r1(X319,X320)|~r1(X318,X319))|~r1(X317,X318)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))))&(((((r1(X325,esk148_5(X303,X310,X317,X324,X325))|(r1(X327,esk147_7(X303,X310,X317,X324,X325,X326,X327))|~r1(X326,X327)|~r1(X325,X326))|~r1(X324,X325)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk148_5(X303,X310,X317,X324,X325),X330)|~p1(X330)|(r1(X327,esk147_7(X303,X310,X317,X324,X325,X326,X327))|~r1(X326,X327)|~r1(X325,X326))|~r1(X324,X325)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303)))&((r1(X325,esk148_5(X303,X310,X317,X324,X325))|(p1(esk147_7(X303,X310,X317,X324,X325,X326,X327))|~r1(X326,X327)|~r1(X325,X326))|~r1(X324,X325)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~r1(esk148_5(X303,X310,X317,X324,X325),X330)|~p1(X330)|(p1(esk147_7(X303,X310,X317,X324,X325,X326,X327))|~r1(X326,X327)|~r1(X325,X326))|~r1(X324,X325)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))))&(~r1(X324,X331)|epred2_1(X331)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303)))&((r1(X332,esk149_5(X303,X310,X317,X324,X332))|(~r1(X332,X333)|(~r1(X333,X334)|p1(X334)))|~r1(X324,X332)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~p1(esk149_5(X303,X310,X317,X324,X332))|(~r1(X332,X333)|(~r1(X333,X334)|p1(X334)))|~r1(X324,X332)|~r1(X317,X324)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303)))))&((r1(X336,esk150_4(X303,X310,X317,X336))|(~r1(X336,X337)|(~r1(X337,X338)|p1(X338)))|~r1(X317,X336)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303))&(~p1(esk150_4(X303,X310,X317,X336))|(~r1(X336,X337)|(~r1(X337,X338)|p1(X338)))|~r1(X317,X336)|~r1(X310,X317)|~r1(X303,X310)|~epred3_1(X303)))))&((r1(X340,esk151_3(X303,X310,X340))|(~r1(X340,X341)|(~r1(X341,X342)|p1(X342)))|~r1(X310,X340)|~r1(X303,X310)|~epred3_1(X303))&(~p1(esk151_3(X303,X310,X340))|(~r1(X340,X341)|(~r1(X341,X342)|p1(X342)))|~r1(X310,X340)|~r1(X303,X310)|~epred3_1(X303)))))&((r1(X344,esk152_2(X303,X344))|(~r1(X344,X345)|(~r1(X345,X346)|p1(X346)))|~r1(X303,X344)|~epred3_1(X303))&(~p1(esk152_2(X303,X344))|(~r1(X344,X345)|(~r1(X345,X346)|p1(X346)))|~r1(X303,X344)|~epred3_1(X303))))), 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_32])])])])])])).
% 149.51/22.12 cnf(c_0_36, negated_conjecture, (epred3_1(X1)|~r1(esk53_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 149.51/22.12 cnf(c_0_37, negated_conjecture, (r1(esk53_0,esk57_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_38, plain, (epred2_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred3_1(X5)), inference(split_conjunct,[status(thm)],[c_0_35])).
% 149.51/22.12 cnf(c_0_39, negated_conjecture, (r1(esk61_0,esk65_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_40, negated_conjecture, (epred3_1(X1)|~r1(esk57_0,X1)), inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 149.51/22.12 cnf(c_0_41, negated_conjecture, (r1(esk57_0,esk61_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_42, plain, ![X1]:((epred1_1(X1)<=>~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))), introduced(definition)).
% 149.51/22.12 cnf(c_0_43, negated_conjecture, (epred2_1(X1)|~epred3_1(esk61_0)|~r1(esk65_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 149.51/22.12 cnf(c_0_44, negated_conjecture, (epred3_1(esk61_0)), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 149.51/22.12 fof(c_0_45, plain, ![X1]:((epred2_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))|~(![X1]:((~r1(X2,X1)|epred1_1(X1))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))))|~(![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2)))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1)))))))))))), inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_29]), c_0_42])).
% 149.51/22.12 cnf(c_0_46, negated_conjecture, (epred2_1(X1)|~r1(esk65_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 149.51/22.12 cnf(c_0_47, negated_conjecture, (r1(esk65_0,esk69_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_48, plain, ![X258, X259, X260, X261, X264, X265, X266, X267, X268, X271, X272, X273, X274, X275, X278, X279, X280, X281, X282, X285, X286, X287, X288, X289, X291, X292, X293, X295, X296, X297, X299, X300, X301]:((((((r1(X259,esk130_2(X258,X259))|(r1(X261,esk129_4(X258,X259,X260,X261))|~r1(X260,X261)|~r1(X259,X260))|~r1(X258,X259)|~epred2_1(X258))&(~r1(esk130_2(X258,X259),X264)|~p1(X264)|(r1(X261,esk129_4(X258,X259,X260,X261))|~r1(X260,X261)|~r1(X259,X260))|~r1(X258,X259)|~epred2_1(X258)))&((r1(X259,esk130_2(X258,X259))|(p1(esk129_4(X258,X259,X260,X261))|~r1(X260,X261)|~r1(X259,X260))|~r1(X258,X259)|~epred2_1(X258))&(~r1(esk130_2(X258,X259),X264)|~p1(X264)|(p1(esk129_4(X258,X259,X260,X261))|~r1(X260,X261)|~r1(X259,X260))|~r1(X258,X259)|~epred2_1(X258))))&(((((r1(X266,esk132_3(X258,X265,X266))|(r1(X268,esk131_5(X258,X265,X266,X267,X268))|~r1(X267,X268)|~r1(X266,X267))|~r1(X265,X266)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk132_3(X258,X265,X266),X271)|~p1(X271)|(r1(X268,esk131_5(X258,X265,X266,X267,X268))|~r1(X267,X268)|~r1(X266,X267))|~r1(X265,X266)|~r1(X258,X265)|~epred2_1(X258)))&((r1(X266,esk132_3(X258,X265,X266))|(p1(esk131_5(X258,X265,X266,X267,X268))|~r1(X267,X268)|~r1(X266,X267))|~r1(X265,X266)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk132_3(X258,X265,X266),X271)|~p1(X271)|(p1(esk131_5(X258,X265,X266,X267,X268))|~r1(X267,X268)|~r1(X266,X267))|~r1(X265,X266)|~r1(X258,X265)|~epred2_1(X258))))&(((((r1(X273,esk134_4(X258,X265,X272,X273))|(r1(X275,esk133_6(X258,X265,X272,X273,X274,X275))|~r1(X274,X275)|~r1(X273,X274))|~r1(X272,X273)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk134_4(X258,X265,X272,X273),X278)|~p1(X278)|(r1(X275,esk133_6(X258,X265,X272,X273,X274,X275))|~r1(X274,X275)|~r1(X273,X274))|~r1(X272,X273)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258)))&((r1(X273,esk134_4(X258,X265,X272,X273))|(p1(esk133_6(X258,X265,X272,X273,X274,X275))|~r1(X274,X275)|~r1(X273,X274))|~r1(X272,X273)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk134_4(X258,X265,X272,X273),X278)|~p1(X278)|(p1(esk133_6(X258,X265,X272,X273,X274,X275))|~r1(X274,X275)|~r1(X273,X274))|~r1(X272,X273)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))))&(((((r1(X280,esk136_5(X258,X265,X272,X279,X280))|(r1(X282,esk135_7(X258,X265,X272,X279,X280,X281,X282))|~r1(X281,X282)|~r1(X280,X281))|~r1(X279,X280)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk136_5(X258,X265,X272,X279,X280),X285)|~p1(X285)|(r1(X282,esk135_7(X258,X265,X272,X279,X280,X281,X282))|~r1(X281,X282)|~r1(X280,X281))|~r1(X279,X280)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258)))&((r1(X280,esk136_5(X258,X265,X272,X279,X280))|(p1(esk135_7(X258,X265,X272,X279,X280,X281,X282))|~r1(X281,X282)|~r1(X280,X281))|~r1(X279,X280)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~r1(esk136_5(X258,X265,X272,X279,X280),X285)|~p1(X285)|(p1(esk135_7(X258,X265,X272,X279,X280,X281,X282))|~r1(X281,X282)|~r1(X280,X281))|~r1(X279,X280)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))))&(~r1(X279,X286)|epred1_1(X286)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258)))&((r1(X287,esk137_5(X258,X265,X272,X279,X287))|(~r1(X287,X288)|(~r1(X288,X289)|p1(X289)))|~r1(X279,X287)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~p1(esk137_5(X258,X265,X272,X279,X287))|(~r1(X287,X288)|(~r1(X288,X289)|p1(X289)))|~r1(X279,X287)|~r1(X272,X279)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258)))))&((r1(X291,esk138_4(X258,X265,X272,X291))|(~r1(X291,X292)|(~r1(X292,X293)|p1(X293)))|~r1(X272,X291)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258))&(~p1(esk138_4(X258,X265,X272,X291))|(~r1(X291,X292)|(~r1(X292,X293)|p1(X293)))|~r1(X272,X291)|~r1(X265,X272)|~r1(X258,X265)|~epred2_1(X258)))))&((r1(X295,esk139_3(X258,X265,X295))|(~r1(X295,X296)|(~r1(X296,X297)|p1(X297)))|~r1(X265,X295)|~r1(X258,X265)|~epred2_1(X258))&(~p1(esk139_3(X258,X265,X295))|(~r1(X295,X296)|(~r1(X296,X297)|p1(X297)))|~r1(X265,X295)|~r1(X258,X265)|~epred2_1(X258)))))&((r1(X299,esk140_2(X258,X299))|(~r1(X299,X300)|(~r1(X300,X301)|p1(X301)))|~r1(X258,X299)|~epred2_1(X258))&(~p1(esk140_2(X258,X299))|(~r1(X299,X300)|(~r1(X300,X301)|p1(X301)))|~r1(X258,X299)|~epred2_1(X258))))), 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_45])])])])])])).
% 149.51/22.12 cnf(c_0_49, negated_conjecture, (epred2_1(X1)|~r1(esk69_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_46, c_0_47])).
% 149.51/22.12 cnf(c_0_50, negated_conjecture, (r1(esk69_0,esk73_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_51, plain, (epred1_1(X2)|~r1(X1,X2)|~r1(X3,X1)|~r1(X4,X3)|~r1(X5,X4)|~epred2_1(X5)), inference(split_conjunct,[status(thm)],[c_0_48])).
% 149.51/22.12 cnf(c_0_52, negated_conjecture, (r1(esk77_0,esk81_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_53, negated_conjecture, (epred2_1(X1)|~r1(esk73_0,X1)), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 149.51/22.12 cnf(c_0_54, negated_conjecture, (r1(esk73_0,esk77_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_55, negated_conjecture, (epred1_1(X1)|~epred2_1(esk77_0)|~r1(esk81_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 149.51/22.12 cnf(c_0_56, negated_conjecture, (epred2_1(esk77_0)), inference(spm,[status(thm)],[c_0_53, c_0_54])).
% 149.51/22.12 cnf(c_0_57, negated_conjecture, (epred1_1(X1)|~r1(esk81_0,X2)|~r1(X2,X3)|~r1(X3,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_55, c_0_56])])).
% 149.51/22.12 cnf(c_0_58, negated_conjecture, (r1(esk81_0,esk85_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_59, plain, ![X1]:((epred1_1(X1)=>~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|~((![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))&p2(X2))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))))))))))|(~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1)))))))|~(![X2]:((~r1(X1,X2)|~((![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p2(X2))))))&![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p3(X2)))|~p2(X1))))))))))))))|(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p3(X1)))|~p2(X2)))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p2(X1))))))))))), inference(split_equiv,[status(thm)],[c_0_42])).
% 149.51/22.12 cnf(c_0_60, negated_conjecture, (epred1_1(X1)|~r1(esk85_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_57, c_0_58])).
% 149.51/22.12 cnf(c_0_61, negated_conjecture, (r1(esk85_0,esk89_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 fof(c_0_62, plain, ![X231, X232, X235, X236, X238, X240, X241, X242, X246, X247, X249, X251, X257]:((((((((r1(X232,esk115_2(X231,X232))|~r1(X231,X232)|~epred1_1(X231))&((r1(esk115_2(X231,X232),esk116_2(X231,X232))|~r1(X231,X232)|~epred1_1(X231))&(~p3(esk116_2(X231,X232))|~r1(X231,X232)|~epred1_1(X231))))&(p2(esk115_2(X231,X232))|~r1(X231,X232)|~epred1_1(X231)))&((((r1(X238,esk118_3(X231,X235,X238))|~r1(X235,X238)|(r1(X236,esk117_3(X231,X235,X236))|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231))&(~r1(esk118_3(X231,X235,X238),X240)|~p2(X240)|~r1(X235,X238)|(r1(X236,esk117_3(X231,X235,X236))|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231)))&((r1(X238,esk118_3(X231,X235,X238))|~r1(X235,X238)|(~p3(esk117_3(X231,X235,X236))|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231))&(~r1(esk118_3(X231,X235,X238),X240)|~p2(X240)|~r1(X235,X238)|(~p3(esk117_3(X231,X235,X236))|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231))))&((r1(X238,esk118_3(X231,X235,X238))|~r1(X235,X238)|(p2(X236)|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231))&(~r1(esk118_3(X231,X235,X238),X240)|~p2(X240)|~r1(X235,X238)|(p2(X236)|~r1(X235,X236)|~p2(X235))|~r1(X231,X235)|~epred1_1(X231)))))&((((r1(X231,esk121_1(X231))|(r1(X242,esk119_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231))&(~r1(esk121_1(X231),X246)|~p2(X246)|(r1(X242,esk119_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231)))&(((r1(X231,esk121_1(X231))|(r1(esk119_3(X231,X241,X242),esk120_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231))&(~r1(esk121_1(X231),X246)|~p2(X246)|(r1(esk119_3(X231,X241,X242),esk120_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231)))&((r1(X231,esk121_1(X231))|(~p3(esk120_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231))&(~r1(esk121_1(X231),X246)|~p2(X246)|(~p3(esk120_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231)))))&((r1(X231,esk121_1(X231))|(p2(esk119_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231))&(~r1(esk121_1(X231),X246)|~p2(X246)|(p2(esk119_3(X231,X241,X242))|~r1(X241,X242)|~r1(X231,X241))|~epred1_1(X231)))))&(((r1(X247,esk123_2(X231,X247))|r1(X247,esk122_2(X231,X247))|~r1(X231,X247)|~epred1_1(X231))&(((r1(X251,esk124_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|r1(X247,esk122_2(X231,X247))|~r1(X231,X247)|~epred1_1(X231))&((r1(esk124_3(X231,X247,X251),esk125_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|r1(X247,esk122_2(X231,X247))|~r1(X231,X247)|~epred1_1(X231))&(~p3(esk125_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|r1(X247,esk122_2(X231,X247))|~r1(X231,X247)|~epred1_1(X231))))&(p2(esk124_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|r1(X247,esk122_2(X231,X247))|~r1(X231,X247)|~epred1_1(X231))))&((r1(X247,esk123_2(X231,X247))|(~r1(esk122_2(X231,X247),X249)|~p2(X249))|~r1(X231,X247)|~epred1_1(X231))&(((r1(X251,esk124_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|(~r1(esk122_2(X231,X247),X249)|~p2(X249))|~r1(X231,X247)|~epred1_1(X231))&((r1(esk124_3(X231,X247,X251),esk125_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|(~r1(esk122_2(X231,X247),X249)|~p2(X249))|~r1(X231,X247)|~epred1_1(X231))&(~p3(esk125_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|(~r1(esk122_2(X231,X247),X249)|~p2(X249))|~r1(X231,X247)|~epred1_1(X231))))&(p2(esk124_3(X231,X247,X251))|~r1(esk123_2(X231,X247),X251)|(~r1(esk122_2(X231,X247),X249)|~p2(X249))|~r1(X231,X247)|~epred1_1(X231))))))&((((r1(X231,esk128_1(X231))|r1(X231,esk126_1(X231))|~epred1_1(X231))&(~r1(esk128_1(X231),X257)|~p2(X257)|r1(X231,esk126_1(X231))|~epred1_1(X231)))&(((r1(X231,esk128_1(X231))|r1(esk126_1(X231),esk127_1(X231))|~epred1_1(X231))&(~r1(esk128_1(X231),X257)|~p2(X257)|r1(esk126_1(X231),esk127_1(X231))|~epred1_1(X231)))&((r1(X231,esk128_1(X231))|~p3(esk127_1(X231))|~epred1_1(X231))&(~r1(esk128_1(X231),X257)|~p2(X257)|~p3(esk127_1(X231))|~epred1_1(X231)))))&((r1(X231,esk128_1(X231))|p2(esk126_1(X231))|~epred1_1(X231))&(~r1(esk128_1(X231),X257)|~p2(X257)|p2(esk126_1(X231))|~epred1_1(X231)))))), 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_59])])])])])])).
% 149.51/22.12 cnf(c_0_63, negated_conjecture, (epred1_1(X1)|~r1(esk89_0,X1)), inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 149.51/22.12 cnf(c_0_64, negated_conjecture, (r1(esk89_0,esk93_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_65, plain, (r1(X1,esk128_1(X1))|r1(X1,esk126_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_66, negated_conjecture, (epred1_1(esk93_0)), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 149.51/22.12 cnf(c_0_67, plain, (r1(X1,esk115_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_68, plain, (r1(esk93_0,esk126_1(esk93_0))|r1(esk93_0,esk128_1(esk93_0))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 149.51/22.12 cnf(c_0_69, plain, (r1(X1,esk128_1(X1))|p2(esk126_1(X1))|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_70, plain, (r1(X1,esk126_1(X1))|~r1(esk128_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_71, plain, (r1(esk128_1(esk93_0),esk115_2(esk93_0,esk128_1(esk93_0)))|r1(esk93_0,esk126_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_66])])).
% 149.51/22.12 cnf(c_0_72, plain, (p2(esk115_2(X1,X2))|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_73, plain, (p2(esk126_1(esk93_0))|r1(esk93_0,esk128_1(esk93_0))), inference(spm,[status(thm)],[c_0_69, c_0_66])).
% 149.51/22.12 cnf(c_0_74, plain, (r1(esk93_0,esk126_1(esk93_0))|~p2(esk115_2(esk93_0,esk128_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_70, c_0_71]), c_0_66])])).
% 149.51/22.12 cnf(c_0_75, plain, (p2(esk115_2(esk93_0,esk128_1(esk93_0)))|r1(esk93_0,esk126_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_68]), c_0_66])])).
% 149.51/22.12 cnf(c_0_76, plain, (p2(esk126_1(X1))|~r1(esk128_1(X1),X2)|~p2(X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_77, plain, (p2(esk126_1(esk93_0))|r1(esk128_1(esk93_0),esk115_2(esk93_0,esk128_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_73]), c_0_66])])).
% 149.51/22.12 cnf(c_0_78, negated_conjecture, (r1(X1,esk94_1(X1))|~r1(esk93_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_79, plain, (r1(esk93_0,esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_74, c_0_75])).
% 149.51/22.12 cnf(c_0_80, plain, (p2(esk126_1(esk93_0))|~p2(esk115_2(esk93_0,esk128_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_77]), c_0_66])])).
% 149.51/22.12 cnf(c_0_81, plain, (p2(esk115_2(esk93_0,esk128_1(esk93_0)))|p2(esk126_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_73]), c_0_66])])).
% 149.51/22.12 cnf(c_0_82, plain, (r1(X1,esk118_3(X2,X3,X1))|p2(X4)|~r1(X3,X1)|~r1(X3,X4)|~p2(X3)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_83, negated_conjecture, (r1(esk126_1(esk93_0),esk94_1(esk126_1(esk93_0)))), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 149.51/22.12 cnf(c_0_84, plain, (p2(esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 149.51/22.12 cnf(c_0_85, plain, (r1(X1,esk123_2(X2,X1))|r1(X1,esk122_2(X2,X1))|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_86, negated_conjecture, (p2(esk94_1(esk126_1(esk93_0)))|r1(X1,esk118_3(X2,esk126_1(esk93_0),X1))|~epred1_1(X2)|~r1(esk126_1(esk93_0),X1)|~r1(X2,esk126_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_83]), c_0_84])])).
% 149.51/22.12 cnf(c_0_87, plain, (r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))|r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_79]), c_0_66])])).
% 149.51/22.12 cnf(c_0_88, plain, (p2(esk94_1(esk126_1(esk93_0)))|r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(X1,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))|~epred1_1(X1)|~r1(X1,esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_86, c_0_87])).
% 149.51/22.12 cnf(c_0_89, negated_conjecture, (~p2(esk94_1(X1))|~r1(esk93_0,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 149.51/22.12 cnf(c_0_90, plain, (p2(esk94_1(esk126_1(esk93_0)))|r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_88, c_0_79]), c_0_66])])).
% 149.51/22.12 cnf(c_0_91, plain, (r1(X1,esk124_3(X2,X3,X1))|r1(X3,esk122_2(X2,X3))|~r1(esk123_2(X2,X3),X1)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_92, negated_conjecture, (r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_90]), c_0_79])])).
% 149.51/22.12 cnf(c_0_93, plain, (p2(X5)|~r1(esk118_3(X1,X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~r1(X2,X5)|~p2(X2)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_94, plain, (r1(esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))),esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_92]), c_0_66]), c_0_79])])).
% 149.51/22.12 cnf(c_0_95, plain, (p2(X1)|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))|~p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))|~r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))|~r1(esk126_1(esk93_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_94]), c_0_66]), c_0_84]), c_0_79])])).
% 149.51/22.12 cnf(c_0_96, plain, (p2(esk124_3(X1,X2,X3))|r1(X2,esk122_2(X1,X2))|~r1(esk123_2(X1,X2),X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_97, plain, (p2(X1)|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))|~p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))|~r1(esk126_1(esk93_0),X1)), inference(spm,[status(thm)],[c_0_95, c_0_87])).
% 149.51/22.12 cnf(c_0_98, plain, (p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_96, c_0_92]), c_0_66]), c_0_79])])).
% 149.51/22.12 cnf(c_0_99, plain, (p2(X1)|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))|~r1(esk126_1(esk93_0),X1)), inference(spm,[status(thm)],[c_0_97, c_0_98])).
% 149.51/22.12 cnf(c_0_100, negated_conjecture, (p2(esk94_1(esk126_1(esk93_0)))|r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(spm,[status(thm)],[c_0_99, c_0_83])).
% 149.51/22.12 cnf(c_0_101, plain, (r1(X1,esk121_1(X1))|r1(X2,esk119_3(X1,X3,X2))|~r1(X3,X2)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_102, negated_conjecture, (r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_100]), c_0_79])])).
% 149.51/22.12 cnf(c_0_103, plain, (r1(X1,esk121_1(X1))|p2(esk119_3(X1,X2,X3))|~r1(X2,X3)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_104, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(X1,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(X1,esk121_1(X1))|~epred1_1(X1)|~r1(X1,esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_101, c_0_102])).
% 149.51/22.12 cnf(c_0_105, plain, (p2(esk119_3(X1,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(X1,esk121_1(X1))|~epred1_1(X1)|~r1(X1,esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_103, c_0_102])).
% 149.51/22.12 cnf(c_0_106, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(esk93_0,esk121_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104, c_0_79]), c_0_66])])).
% 149.51/22.12 cnf(c_0_107, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(esk93_0,esk121_1(esk93_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105, c_0_79]), c_0_66])])).
% 149.51/22.12 cnf(c_0_108, plain, (r1(X3,esk119_3(X1,X4,X3))|~r1(esk121_1(X1),X2)|~p2(X2)|~r1(X4,X3)|~r1(X1,X4)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_109, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(esk121_1(esk93_0),esk115_2(esk93_0,esk121_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_106]), c_0_66])])).
% 149.51/22.12 cnf(c_0_110, plain, (p2(esk119_3(X1,X3,X4))|~r1(esk121_1(X1),X2)|~p2(X2)|~r1(X3,X4)|~r1(X1,X3)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_111, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(esk121_1(esk93_0),esk115_2(esk93_0,esk121_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_107]), c_0_66])])).
% 149.51/22.12 cnf(c_0_112, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(X1,esk119_3(esk93_0,X2,X1))|~p2(esk115_2(esk93_0,esk121_1(esk93_0)))|~r1(esk93_0,X2)|~r1(X2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_108, c_0_109]), c_0_66])])).
% 149.51/22.12 cnf(c_0_113, plain, (p2(esk115_2(esk93_0,esk121_1(esk93_0)))|r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_106]), c_0_66])])).
% 149.51/22.12 cnf(c_0_114, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|p2(esk119_3(esk93_0,X1,X2))|~p2(esk115_2(esk93_0,esk121_1(esk93_0)))|~r1(esk93_0,X1)|~r1(X1,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_110, c_0_111]), c_0_66])])).
% 149.51/22.12 cnf(c_0_115, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|p2(esk115_2(esk93_0,esk121_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_107]), c_0_66])])).
% 149.51/22.12 cnf(c_0_116, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(X1,esk119_3(esk93_0,X2,X1))|~r1(esk93_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_112, c_0_113])).
% 149.51/22.12 cnf(c_0_117, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|p2(esk119_3(esk93_0,X1,X2))|~r1(esk93_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_114, c_0_115])).
% 149.51/22.12 cnf(c_0_118, plain, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|r1(X1,esk119_3(esk93_0,esk126_1(esk93_0),X1))|~r1(esk126_1(esk93_0),X1)), inference(spm,[status(thm)],[c_0_116, c_0_79])).
% 149.51/22.12 cnf(c_0_119, plain, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))|p2(esk119_3(esk93_0,esk126_1(esk93_0),X1))|~r1(esk126_1(esk93_0),X1)), inference(spm,[status(thm)],[c_0_117, c_0_79])).
% 149.51/22.12 cnf(c_0_120, plain, (r1(X1,esk123_2(X2,X1))|~r1(esk122_2(X2,X1),X3)|~p2(X3)|~r1(X2,X1)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_121, negated_conjecture, (r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))), inference(spm,[status(thm)],[c_0_118, c_0_102])).
% 149.51/22.12 cnf(c_0_122, negated_conjecture, (p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))), inference(spm,[status(thm)],[c_0_119, c_0_102])).
% 149.51/22.12 cnf(c_0_123, plain, (r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120, c_0_121]), c_0_66]), c_0_122]), c_0_79])])).
% 149.51/22.12 cnf(c_0_124, negated_conjecture, (p2(esk94_1(esk126_1(esk93_0)))|r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(X1,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))|~epred1_1(X1)|~r1(X1,esk126_1(esk93_0))), inference(spm,[status(thm)],[c_0_86, c_0_123])).
% 149.51/22.12 cnf(c_0_125, plain, (r1(X1,esk124_3(X2,X3,X1))|~r1(esk123_2(X2,X3),X1)|~r1(esk122_2(X2,X3),X4)|~p2(X4)|~r1(X2,X3)|~epred1_1(X2)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_126, plain, (p2(esk94_1(esk126_1(esk93_0)))|r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_124, c_0_79]), c_0_66])])).
% 149.51/22.12 cnf(c_0_127, plain, (p2(esk124_3(X1,X2,X3))|~r1(esk123_2(X1,X2),X3)|~r1(esk122_2(X1,X2),X4)|~p2(X4)|~r1(X1,X2)|~epred1_1(X1)), inference(split_conjunct,[status(thm)],[c_0_62])).
% 149.51/22.12 cnf(c_0_128, plain, (r1(X1,esk124_3(esk93_0,esk126_1(esk93_0),X1))|~r1(esk123_2(esk93_0,esk126_1(esk93_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125, c_0_121]), c_0_66]), c_0_122]), c_0_79])])).
% 149.51/22.12 cnf(c_0_129, negated_conjecture, (r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_126]), c_0_79])])).
% 149.51/22.12 cnf(c_0_130, plain, (p2(esk124_3(esk93_0,esk126_1(esk93_0),X1))|~r1(esk123_2(esk93_0,esk126_1(esk93_0)),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_127, c_0_121]), c_0_66]), c_0_122]), c_0_79])])).
% 149.51/22.12 cnf(c_0_131, plain, (r1(esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))),esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))), inference(spm,[status(thm)],[c_0_128, c_0_129])).
% 149.51/22.12 cnf(c_0_132, plain, (p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))), inference(spm,[status(thm)],[c_0_130, c_0_129])).
% 149.51/22.12 cnf(c_0_133, plain, (p2(X1)|~r1(esk126_1(esk93_0),X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93, c_0_131]), c_0_66]), c_0_132]), c_0_84]), c_0_123]), c_0_79])])).
% 149.51/22.12 cnf(c_0_134, negated_conjecture, (p2(esk94_1(esk126_1(esk93_0)))), inference(spm,[status(thm)],[c_0_133, c_0_83])).
% 149.51/22.12 cnf(c_0_135, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89, c_0_134]), c_0_79])]), ['proof']).
% 149.51/22.12 % SZS output end Proof
% 149.51/22.12 % User time : 21.046 s
% 149.51/22.12 % System time : 0.170 s
% 149.51/22.12 % Total time : 21.216 s
% 149.51/22.12 % User time : 104.519 s
% 149.51/22.12 % System time : 1.372 s
% 149.51/22.12 % Total time : 105.891 s
% 149.51/22.12
%------------------------------------------------------------------------------