%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL638+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n014.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:15 AM UTC 2026
% Result : Theorem 251.95s 37.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL638+1.010 : 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 : n014.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 : Sun Sep 6 01:48:42 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.14/0.46 start to proof:theBenchmark.p
% 251.95/37.47 % Version : CSI_E---1.1
% 251.95/37.47 % Problem : theBenchmark.p
% 251.95/37.47 % Proof found!
% 251.95/37.47 % SZS status Theorem for theBenchmark.p
% 251.95/37.47 % SZS output start Proof
% 251.95/37.47 fof(main, conjecture, ~(?[X1]:(~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(p1(X1)))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))&p1(X1))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true))))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(p1(X2)))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![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))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true))))))))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(p1(X1)))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))&p1(X1))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true))))))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(p1(X2)))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![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))|![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))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true))))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(p1(X1)))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))&p1(X1))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true))))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(p1(X2)))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(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))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true))))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(p1(X1)))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))&p1(X1))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1))))))&![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true))))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(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))))))))&p1(X2))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))))&![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))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true))))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(p1(X1)))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~(p1(X1))))))))&p1(X1))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))))&![X2]:((~(r1(X1,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))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true))))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))))))))))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(p1(X2)))))))|~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(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))|p1(X2))))))&![X1]:((~(r1(X2,X1))|p1(X1))))))))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true))))))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p1(X1)|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))))))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', main)).
% 251.95/37.47 fof(c_0_1, negated_conjecture, ~(~(?[X1]:(~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~p1(X1))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))&p1(X1))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true)))))))))))))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~p1(X2))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![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)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true)))))))))))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~p1(X1))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))&p1(X1))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true)))))))))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~p1(X2))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![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)|![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)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true)))))))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~p1(X1))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))&p1(X1))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true)))))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~p1(X2))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~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)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true)))))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~p1(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))&p1(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1))))))&![X2]:((~r1(X1,X2)|p1(X2))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true)))))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(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)))))))&p1(X2))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))))&![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))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true)))))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~p1(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~p1(X1)))))))&p1(X1))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))))&![X2]:((~r1(X1,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))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true)))))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~p1(X2))))))|~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(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)|p1(X2))))))&![X1]:((~r1(X2,X1)|p1(X1))))))))|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true)))))))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p1(X1)|~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 251.95/37.47 fof(c_0_2, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, X26, X28, X29, X30, X31, X32, X33, X34, X35, X36, X37, X38, X39, X42, X43, X44, X45, X46, X47, X48, X49, X50, X51, X52, X53, X54, X56, X57, X58, X59, X60, X61, X62, X63, X64, X65, X77, X78, X79, X80, X81, X82, X83, X84, X85, X86, X87, X89, X90, X91, X92, X93, X94, X95, X96, X97, X98, X100, X101, X102, X103, X104, X105, X106, X107, X108, X109, X110, X113, X114, X115, X116, X117, X118, X119, X120, X121, X122, X123, X124, X126, X127, X128, X129, X130, X131, X132, X133, X134, X146, X147, X148, X149, X150, X151, X152, X153, X154, X155, X157, X158, X159, X160, X161, X162, X163, X164, X165, X167, X168, X169, X170, X171, X172, X173, X174, X175, X176, X179, X180, X181, X182, X183, X184, X185, X186, X187, X188, X189, X191, X192, X193, X194, X195, X196, X197, X198, X210, X211, X212, X213, X214, X215, X216, X217, X218, X220, X221, X222, X223, X224, X225, X226, X227, X229, X230, X231, X232, X233, X234, X235, X236, X237, X240, X241, X242, X243, X244, X245, X246, X247, X248, X249, X251, X252, X253, X254, X255, X256, X257, X269, X270, X271, X272, X273, X274, X275, X276, X278, X279, X280, X281, X282, X283, X284, X286, X287, X288, X289, X290, X291, X292, X293, X296, X297, X298, X299, X300, X301, X302, X303, X304, X306, X307, X308, X309, X310, X311, X323, X324, X325, X326, X327, X328, X329, X331, X332, X333, X334, X335, X336, X338, X339, X340, X341, X342, X343, X344, X347, X348, X349, X350, X351, X352, X353, X354, X356, X357, X358, X359, X360, X372, X373, X374, X375, X376, X377, X379, X380, X381, X382, X383, X385, X386, X387, X388, X389, X390, X393, X394, X395, X396, X397, X398, X399, X401, X402, X403, X404, X416, X417, X418, X419, X420, X422, X423, X424, X425, X427, X428, X429, X430, X431, X434, X435, X436, X437, X438, X439, X441, X442, X443, X455, X456, X457, X458, X460, X461, X462, X464, X465, X466, X467, X470, X471, X472, X473, X474, X476, X477, X489, X490, X491, X493, X494, X496, X497, X498, X501, X502, X503, X504, X506, X518]:((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((r1(X14,esk2_11(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14))|~r1(X13,X14)|p1(X13)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))&(~p1(esk2_11(X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14))|~r1(X13,X14)|p1(X13)|~r1(X12,X13)|~r1(X11,X12)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4)))&((r1(X26,esk3_11(X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26))|~r1(X25,X26)|~p1(X25)|~r1(X24,X25)|~r1(X23,X24)|~r1(X22,X23)|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(X17,X18)|~r1(X16,X17)|~r1(esk1_0,X16))&(p1(esk3_11(X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26))|~r1(X25,X26)|~p1(X25)|~r1(X24,X25)|~r1(X23,X24)|~r1(X22,X23)|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(X17,X18)|~r1(X16,X17)|~r1(esk1_0,X16))))&(((r1(X37,esk5_10(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37))|(r1(X39,esk4_12(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|~r1(X38,X39)|~r1(X37,X38))|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28))&(~r1(esk5_10(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37),X42)|~p1(X42)|(r1(X39,esk4_12(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|~r1(X38,X39)|~r1(X37,X38))|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28)))&((r1(X37,esk5_10(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37))|(p1(esk4_12(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|~r1(X38,X39)|~r1(X37,X38))|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28))&(~r1(esk5_10(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37),X42)|~p1(X42)|(p1(esk4_12(X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39))|~r1(X38,X39)|~r1(X37,X38))|~r1(X36,X37)|~r1(X35,X36)|~r1(X34,X35)|~r1(X33,X34)|~r1(X32,X33)|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28)))))&((r1(X52,esk6_10(X43,X44,X45,X46,X47,X48,X49,X50,X51,X52))|(~r1(X52,X53)|(~r1(X53,X54)|p1(X54)))|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(X48,X49)|~r1(X47,X48)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(X43,X44)|~r1(esk1_0,X43))&(~p1(esk6_10(X43,X44,X45,X46,X47,X48,X49,X50,X51,X52))|(~r1(X52,X53)|(~r1(X53,X54)|p1(X54)))|~r1(X51,X52)|~r1(X50,X51)|~r1(X49,X50)|~r1(X48,X49)|~r1(X47,X48)|~r1(X46,X47)|~r1(X45,X46)|~r1(X44,X45)|~r1(X43,X44)|~r1(esk1_0,X43))))&((r1(X65,esk7_10(X56,X57,X58,X59,X60,X61,X62,X63,X64,X65))|~r1(X64,X65)|~r1(X63,X64)|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(esk1_0,X56))&($true|~r1(X64,X65)|~r1(X63,X64)|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(X59,X60)|~r1(X58,X59)|~r1(X57,X58)|~r1(X56,X57)|~r1(esk1_0,X56))))&(r1(esk1_0,esk8_0)&(r1(esk8_0,esk9_0)&(r1(esk9_0,esk10_0)&(r1(esk10_0,esk11_0)&(r1(esk11_0,esk12_0)&(r1(esk12_0,esk13_0)&(r1(esk13_0,esk14_0)&(r1(esk14_0,esk15_0)&(r1(esk15_0,esk16_0)&((r1(esk16_0,esk17_0)&~p1(esk17_0))&(~r1(esk17_0,X77)|p1(X77)))))))))))))&((r1(X87,esk18_10(X78,X79,X80,X81,X82,X83,X84,X85,X86,X87))|~r1(X86,X87)|p1(X86)|~r1(X85,X86)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(X81,X82)|~r1(X80,X81)|~r1(X79,X80)|~r1(X78,X79)|~r1(esk1_0,X78))&(~p1(esk18_10(X78,X79,X80,X81,X82,X83,X84,X85,X86,X87))|~r1(X86,X87)|p1(X86)|~r1(X85,X86)|~r1(X84,X85)|~r1(X83,X84)|~r1(X82,X83)|~r1(X81,X82)|~r1(X80,X81)|~r1(X79,X80)|~r1(X78,X79)|~r1(esk1_0,X78))))&((r1(X98,esk19_10(X89,X90,X91,X92,X93,X94,X95,X96,X97,X98))|~r1(X97,X98)|~p1(X97)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(X89,X90)|~r1(esk1_0,X89))&(p1(esk19_10(X89,X90,X91,X92,X93,X94,X95,X96,X97,X98))|~r1(X97,X98)|~p1(X97)|~r1(X96,X97)|~r1(X95,X96)|~r1(X94,X95)|~r1(X93,X94)|~r1(X92,X93)|~r1(X91,X92)|~r1(X90,X91)|~r1(X89,X90)|~r1(esk1_0,X89))))&(((r1(X108,esk21_9(X100,X101,X102,X103,X104,X105,X106,X107,X108))|(r1(X110,esk20_11(X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110))|~r1(X109,X110)|~r1(X108,X109))|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X103,X104)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))&(~r1(esk21_9(X100,X101,X102,X103,X104,X105,X106,X107,X108),X113)|~p1(X113)|(r1(X110,esk20_11(X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110))|~r1(X109,X110)|~r1(X108,X109))|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X103,X104)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100)))&((r1(X108,esk21_9(X100,X101,X102,X103,X104,X105,X106,X107,X108))|(p1(esk20_11(X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110))|~r1(X109,X110)|~r1(X108,X109))|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X103,X104)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100))&(~r1(esk21_9(X100,X101,X102,X103,X104,X105,X106,X107,X108),X113)|~p1(X113)|(p1(esk20_11(X100,X101,X102,X103,X104,X105,X106,X107,X108,X109,X110))|~r1(X109,X110)|~r1(X108,X109))|~r1(X107,X108)|~r1(X106,X107)|~r1(X105,X106)|~r1(X104,X105)|~r1(X103,X104)|~r1(X102,X103)|~r1(X101,X102)|~r1(X100,X101)|~r1(esk1_0,X100)))))&((r1(X122,esk22_9(X114,X115,X116,X117,X118,X119,X120,X121,X122))|(~r1(X122,X123)|(~r1(X123,X124)|p1(X124)))|~r1(X121,X122)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(X117,X118)|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(esk1_0,X114))&(~p1(esk22_9(X114,X115,X116,X117,X118,X119,X120,X121,X122))|(~r1(X122,X123)|(~r1(X123,X124)|p1(X124)))|~r1(X121,X122)|~r1(X120,X121)|~r1(X119,X120)|~r1(X118,X119)|~r1(X117,X118)|~r1(X116,X117)|~r1(X115,X116)|~r1(X114,X115)|~r1(esk1_0,X114))))&((r1(X134,esk23_9(X126,X127,X128,X129,X130,X131,X132,X133,X134))|~r1(X133,X134)|~r1(X132,X133)|~r1(X131,X132)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(X127,X128)|~r1(X126,X127)|~r1(esk1_0,X126))&($true|~r1(X133,X134)|~r1(X132,X133)|~r1(X131,X132)|~r1(X130,X131)|~r1(X129,X130)|~r1(X128,X129)|~r1(X127,X128)|~r1(X126,X127)|~r1(esk1_0,X126))))&(r1(esk1_0,esk24_0)&(r1(esk24_0,esk25_0)&(r1(esk25_0,esk26_0)&(r1(esk26_0,esk27_0)&(r1(esk27_0,esk28_0)&(r1(esk28_0,esk29_0)&(r1(esk29_0,esk30_0)&(r1(esk30_0,esk31_0)&(r1(esk31_0,esk32_0)&((r1(esk32_0,esk33_0)&~p1(esk33_0))&(~r1(esk33_0,X146)|p1(X146)))))))))))))&((r1(X155,esk34_9(X147,X148,X149,X150,X151,X152,X153,X154,X155))|~r1(X154,X155)|p1(X154)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(X148,X149)|~r1(X147,X148)|~r1(esk1_0,X147))&(~p1(esk34_9(X147,X148,X149,X150,X151,X152,X153,X154,X155))|~r1(X154,X155)|p1(X154)|~r1(X153,X154)|~r1(X152,X153)|~r1(X151,X152)|~r1(X150,X151)|~r1(X149,X150)|~r1(X148,X149)|~r1(X147,X148)|~r1(esk1_0,X147))))&((r1(X165,esk35_9(X157,X158,X159,X160,X161,X162,X163,X164,X165))|~r1(X164,X165)|~p1(X164)|~r1(X163,X164)|~r1(X162,X163)|~r1(X161,X162)|~r1(X160,X161)|~r1(X159,X160)|~r1(X158,X159)|~r1(X157,X158)|~r1(esk1_0,X157))&(p1(esk35_9(X157,X158,X159,X160,X161,X162,X163,X164,X165))|~r1(X164,X165)|~p1(X164)|~r1(X163,X164)|~r1(X162,X163)|~r1(X161,X162)|~r1(X160,X161)|~r1(X159,X160)|~r1(X158,X159)|~r1(X157,X158)|~r1(esk1_0,X157))))&(((r1(X174,esk37_8(X167,X168,X169,X170,X171,X172,X173,X174))|(r1(X176,esk36_10(X167,X168,X169,X170,X171,X172,X173,X174,X175,X176))|~r1(X175,X176)|~r1(X174,X175))|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167))&(~r1(esk37_8(X167,X168,X169,X170,X171,X172,X173,X174),X179)|~p1(X179)|(r1(X176,esk36_10(X167,X168,X169,X170,X171,X172,X173,X174,X175,X176))|~r1(X175,X176)|~r1(X174,X175))|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167)))&((r1(X174,esk37_8(X167,X168,X169,X170,X171,X172,X173,X174))|(p1(esk36_10(X167,X168,X169,X170,X171,X172,X173,X174,X175,X176))|~r1(X175,X176)|~r1(X174,X175))|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167))&(~r1(esk37_8(X167,X168,X169,X170,X171,X172,X173,X174),X179)|~p1(X179)|(p1(esk36_10(X167,X168,X169,X170,X171,X172,X173,X174,X175,X176))|~r1(X175,X176)|~r1(X174,X175))|~r1(X173,X174)|~r1(X172,X173)|~r1(X171,X172)|~r1(X170,X171)|~r1(X169,X170)|~r1(X168,X169)|~r1(X167,X168)|~r1(esk1_0,X167)))))&((r1(X187,esk38_8(X180,X181,X182,X183,X184,X185,X186,X187))|(~r1(X187,X188)|(~r1(X188,X189)|p1(X189)))|~r1(X186,X187)|~r1(X185,X186)|~r1(X184,X185)|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))&(~p1(esk38_8(X180,X181,X182,X183,X184,X185,X186,X187))|(~r1(X187,X188)|(~r1(X188,X189)|p1(X189)))|~r1(X186,X187)|~r1(X185,X186)|~r1(X184,X185)|~r1(X183,X184)|~r1(X182,X183)|~r1(X181,X182)|~r1(X180,X181)|~r1(esk1_0,X180))))&((r1(X198,esk39_8(X191,X192,X193,X194,X195,X196,X197,X198))|~r1(X197,X198)|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(X193,X194)|~r1(X192,X193)|~r1(X191,X192)|~r1(esk1_0,X191))&($true|~r1(X197,X198)|~r1(X196,X197)|~r1(X195,X196)|~r1(X194,X195)|~r1(X193,X194)|~r1(X192,X193)|~r1(X191,X192)|~r1(esk1_0,X191))))&(r1(esk1_0,esk40_0)&(r1(esk40_0,esk41_0)&(r1(esk41_0,esk42_0)&(r1(esk42_0,esk43_0)&(r1(esk43_0,esk44_0)&(r1(esk44_0,esk45_0)&(r1(esk45_0,esk46_0)&(r1(esk46_0,esk47_0)&(r1(esk47_0,esk48_0)&((r1(esk48_0,esk49_0)&~p1(esk49_0))&(~r1(esk49_0,X210)|p1(X210)))))))))))))&((r1(X218,esk50_8(X211,X212,X213,X214,X215,X216,X217,X218))|~r1(X217,X218)|p1(X217)|~r1(X216,X217)|~r1(X215,X216)|~r1(X214,X215)|~r1(X213,X214)|~r1(X212,X213)|~r1(X211,X212)|~r1(esk1_0,X211))&(~p1(esk50_8(X211,X212,X213,X214,X215,X216,X217,X218))|~r1(X217,X218)|p1(X217)|~r1(X216,X217)|~r1(X215,X216)|~r1(X214,X215)|~r1(X213,X214)|~r1(X212,X213)|~r1(X211,X212)|~r1(esk1_0,X211))))&((r1(X227,esk51_8(X220,X221,X222,X223,X224,X225,X226,X227))|~r1(X226,X227)|~p1(X226)|~r1(X225,X226)|~r1(X224,X225)|~r1(X223,X224)|~r1(X222,X223)|~r1(X221,X222)|~r1(X220,X221)|~r1(esk1_0,X220))&(p1(esk51_8(X220,X221,X222,X223,X224,X225,X226,X227))|~r1(X226,X227)|~p1(X226)|~r1(X225,X226)|~r1(X224,X225)|~r1(X223,X224)|~r1(X222,X223)|~r1(X221,X222)|~r1(X220,X221)|~r1(esk1_0,X220))))&(((r1(X235,esk53_7(X229,X230,X231,X232,X233,X234,X235))|(r1(X237,esk52_9(X229,X230,X231,X232,X233,X234,X235,X236,X237))|~r1(X236,X237)|~r1(X235,X236))|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(esk1_0,X229))&(~r1(esk53_7(X229,X230,X231,X232,X233,X234,X235),X240)|~p1(X240)|(r1(X237,esk52_9(X229,X230,X231,X232,X233,X234,X235,X236,X237))|~r1(X236,X237)|~r1(X235,X236))|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(esk1_0,X229)))&((r1(X235,esk53_7(X229,X230,X231,X232,X233,X234,X235))|(p1(esk52_9(X229,X230,X231,X232,X233,X234,X235,X236,X237))|~r1(X236,X237)|~r1(X235,X236))|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(esk1_0,X229))&(~r1(esk53_7(X229,X230,X231,X232,X233,X234,X235),X240)|~p1(X240)|(p1(esk52_9(X229,X230,X231,X232,X233,X234,X235,X236,X237))|~r1(X236,X237)|~r1(X235,X236))|~r1(X234,X235)|~r1(X233,X234)|~r1(X232,X233)|~r1(X231,X232)|~r1(X230,X231)|~r1(X229,X230)|~r1(esk1_0,X229)))))&((r1(X247,esk54_7(X241,X242,X243,X244,X245,X246,X247))|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249)))|~r1(X246,X247)|~r1(X245,X246)|~r1(X244,X245)|~r1(X243,X244)|~r1(X242,X243)|~r1(X241,X242)|~r1(esk1_0,X241))&(~p1(esk54_7(X241,X242,X243,X244,X245,X246,X247))|(~r1(X247,X248)|(~r1(X248,X249)|p1(X249)))|~r1(X246,X247)|~r1(X245,X246)|~r1(X244,X245)|~r1(X243,X244)|~r1(X242,X243)|~r1(X241,X242)|~r1(esk1_0,X241))))&((r1(X257,esk55_7(X251,X252,X253,X254,X255,X256,X257))|~r1(X256,X257)|~r1(X255,X256)|~r1(X254,X255)|~r1(X253,X254)|~r1(X252,X253)|~r1(X251,X252)|~r1(esk1_0,X251))&($true|~r1(X256,X257)|~r1(X255,X256)|~r1(X254,X255)|~r1(X253,X254)|~r1(X252,X253)|~r1(X251,X252)|~r1(esk1_0,X251))))&(r1(esk1_0,esk56_0)&(r1(esk56_0,esk57_0)&(r1(esk57_0,esk58_0)&(r1(esk58_0,esk59_0)&(r1(esk59_0,esk60_0)&(r1(esk60_0,esk61_0)&(r1(esk61_0,esk62_0)&(r1(esk62_0,esk63_0)&(r1(esk63_0,esk64_0)&((r1(esk64_0,esk65_0)&~p1(esk65_0))&(~r1(esk65_0,X269)|p1(X269)))))))))))))&((r1(X276,esk66_7(X270,X271,X272,X273,X274,X275,X276))|~r1(X275,X276)|p1(X275)|~r1(X274,X275)|~r1(X273,X274)|~r1(X272,X273)|~r1(X271,X272)|~r1(X270,X271)|~r1(esk1_0,X270))&(~p1(esk66_7(X270,X271,X272,X273,X274,X275,X276))|~r1(X275,X276)|p1(X275)|~r1(X274,X275)|~r1(X273,X274)|~r1(X272,X273)|~r1(X271,X272)|~r1(X270,X271)|~r1(esk1_0,X270))))&((r1(X284,esk67_7(X278,X279,X280,X281,X282,X283,X284))|~r1(X283,X284)|~p1(X283)|~r1(X282,X283)|~r1(X281,X282)|~r1(X280,X281)|~r1(X279,X280)|~r1(X278,X279)|~r1(esk1_0,X278))&(p1(esk67_7(X278,X279,X280,X281,X282,X283,X284))|~r1(X283,X284)|~p1(X283)|~r1(X282,X283)|~r1(X281,X282)|~r1(X280,X281)|~r1(X279,X280)|~r1(X278,X279)|~r1(esk1_0,X278))))&(((r1(X291,esk69_6(X286,X287,X288,X289,X290,X291))|(r1(X293,esk68_8(X286,X287,X288,X289,X290,X291,X292,X293))|~r1(X292,X293)|~r1(X291,X292))|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X287,X288)|~r1(X286,X287)|~r1(esk1_0,X286))&(~r1(esk69_6(X286,X287,X288,X289,X290,X291),X296)|~p1(X296)|(r1(X293,esk68_8(X286,X287,X288,X289,X290,X291,X292,X293))|~r1(X292,X293)|~r1(X291,X292))|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X287,X288)|~r1(X286,X287)|~r1(esk1_0,X286)))&((r1(X291,esk69_6(X286,X287,X288,X289,X290,X291))|(p1(esk68_8(X286,X287,X288,X289,X290,X291,X292,X293))|~r1(X292,X293)|~r1(X291,X292))|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X287,X288)|~r1(X286,X287)|~r1(esk1_0,X286))&(~r1(esk69_6(X286,X287,X288,X289,X290,X291),X296)|~p1(X296)|(p1(esk68_8(X286,X287,X288,X289,X290,X291,X292,X293))|~r1(X292,X293)|~r1(X291,X292))|~r1(X290,X291)|~r1(X289,X290)|~r1(X288,X289)|~r1(X287,X288)|~r1(X286,X287)|~r1(esk1_0,X286)))))&((r1(X302,esk70_6(X297,X298,X299,X300,X301,X302))|(~r1(X302,X303)|(~r1(X303,X304)|p1(X304)))|~r1(X301,X302)|~r1(X300,X301)|~r1(X299,X300)|~r1(X298,X299)|~r1(X297,X298)|~r1(esk1_0,X297))&(~p1(esk70_6(X297,X298,X299,X300,X301,X302))|(~r1(X302,X303)|(~r1(X303,X304)|p1(X304)))|~r1(X301,X302)|~r1(X300,X301)|~r1(X299,X300)|~r1(X298,X299)|~r1(X297,X298)|~r1(esk1_0,X297))))&((r1(X311,esk71_6(X306,X307,X308,X309,X310,X311))|~r1(X310,X311)|~r1(X309,X310)|~r1(X308,X309)|~r1(X307,X308)|~r1(X306,X307)|~r1(esk1_0,X306))&($true|~r1(X310,X311)|~r1(X309,X310)|~r1(X308,X309)|~r1(X307,X308)|~r1(X306,X307)|~r1(esk1_0,X306))))&(r1(esk1_0,esk72_0)&(r1(esk72_0,esk73_0)&(r1(esk73_0,esk74_0)&(r1(esk74_0,esk75_0)&(r1(esk75_0,esk76_0)&(r1(esk76_0,esk77_0)&(r1(esk77_0,esk78_0)&(r1(esk78_0,esk79_0)&(r1(esk79_0,esk80_0)&((r1(esk80_0,esk81_0)&~p1(esk81_0))&(~r1(esk81_0,X323)|p1(X323)))))))))))))&((r1(X329,esk82_6(X324,X325,X326,X327,X328,X329))|~r1(X328,X329)|p1(X328)|~r1(X327,X328)|~r1(X326,X327)|~r1(X325,X326)|~r1(X324,X325)|~r1(esk1_0,X324))&(~p1(esk82_6(X324,X325,X326,X327,X328,X329))|~r1(X328,X329)|p1(X328)|~r1(X327,X328)|~r1(X326,X327)|~r1(X325,X326)|~r1(X324,X325)|~r1(esk1_0,X324))))&((r1(X336,esk83_6(X331,X332,X333,X334,X335,X336))|~r1(X335,X336)|~p1(X335)|~r1(X334,X335)|~r1(X333,X334)|~r1(X332,X333)|~r1(X331,X332)|~r1(esk1_0,X331))&(p1(esk83_6(X331,X332,X333,X334,X335,X336))|~r1(X335,X336)|~p1(X335)|~r1(X334,X335)|~r1(X333,X334)|~r1(X332,X333)|~r1(X331,X332)|~r1(esk1_0,X331))))&(((r1(X342,esk85_5(X338,X339,X340,X341,X342))|(r1(X344,esk84_7(X338,X339,X340,X341,X342,X343,X344))|~r1(X343,X344)|~r1(X342,X343))|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(esk1_0,X338))&(~r1(esk85_5(X338,X339,X340,X341,X342),X347)|~p1(X347)|(r1(X344,esk84_7(X338,X339,X340,X341,X342,X343,X344))|~r1(X343,X344)|~r1(X342,X343))|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(esk1_0,X338)))&((r1(X342,esk85_5(X338,X339,X340,X341,X342))|(p1(esk84_7(X338,X339,X340,X341,X342,X343,X344))|~r1(X343,X344)|~r1(X342,X343))|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(esk1_0,X338))&(~r1(esk85_5(X338,X339,X340,X341,X342),X347)|~p1(X347)|(p1(esk84_7(X338,X339,X340,X341,X342,X343,X344))|~r1(X343,X344)|~r1(X342,X343))|~r1(X341,X342)|~r1(X340,X341)|~r1(X339,X340)|~r1(X338,X339)|~r1(esk1_0,X338)))))&((r1(X352,esk86_5(X348,X349,X350,X351,X352))|(~r1(X352,X353)|(~r1(X353,X354)|p1(X354)))|~r1(X351,X352)|~r1(X350,X351)|~r1(X349,X350)|~r1(X348,X349)|~r1(esk1_0,X348))&(~p1(esk86_5(X348,X349,X350,X351,X352))|(~r1(X352,X353)|(~r1(X353,X354)|p1(X354)))|~r1(X351,X352)|~r1(X350,X351)|~r1(X349,X350)|~r1(X348,X349)|~r1(esk1_0,X348))))&((r1(X360,esk87_5(X356,X357,X358,X359,X360))|~r1(X359,X360)|~r1(X358,X359)|~r1(X357,X358)|~r1(X356,X357)|~r1(esk1_0,X356))&($true|~r1(X359,X360)|~r1(X358,X359)|~r1(X357,X358)|~r1(X356,X357)|~r1(esk1_0,X356))))&(r1(esk1_0,esk88_0)&(r1(esk88_0,esk89_0)&(r1(esk89_0,esk90_0)&(r1(esk90_0,esk91_0)&(r1(esk91_0,esk92_0)&(r1(esk92_0,esk93_0)&(r1(esk93_0,esk94_0)&(r1(esk94_0,esk95_0)&(r1(esk95_0,esk96_0)&((r1(esk96_0,esk97_0)&~p1(esk97_0))&(~r1(esk97_0,X372)|p1(X372)))))))))))))&((r1(X377,esk98_5(X373,X374,X375,X376,X377))|~r1(X376,X377)|p1(X376)|~r1(X375,X376)|~r1(X374,X375)|~r1(X373,X374)|~r1(esk1_0,X373))&(~p1(esk98_5(X373,X374,X375,X376,X377))|~r1(X376,X377)|p1(X376)|~r1(X375,X376)|~r1(X374,X375)|~r1(X373,X374)|~r1(esk1_0,X373))))&((r1(X383,esk99_5(X379,X380,X381,X382,X383))|~r1(X382,X383)|~p1(X382)|~r1(X381,X382)|~r1(X380,X381)|~r1(X379,X380)|~r1(esk1_0,X379))&(p1(esk99_5(X379,X380,X381,X382,X383))|~r1(X382,X383)|~p1(X382)|~r1(X381,X382)|~r1(X380,X381)|~r1(X379,X380)|~r1(esk1_0,X379))))&(((r1(X388,esk101_4(X385,X386,X387,X388))|(r1(X390,esk100_6(X385,X386,X387,X388,X389,X390))|~r1(X389,X390)|~r1(X388,X389))|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(esk1_0,X385))&(~r1(esk101_4(X385,X386,X387,X388),X393)|~p1(X393)|(r1(X390,esk100_6(X385,X386,X387,X388,X389,X390))|~r1(X389,X390)|~r1(X388,X389))|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(esk1_0,X385)))&((r1(X388,esk101_4(X385,X386,X387,X388))|(p1(esk100_6(X385,X386,X387,X388,X389,X390))|~r1(X389,X390)|~r1(X388,X389))|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(esk1_0,X385))&(~r1(esk101_4(X385,X386,X387,X388),X393)|~p1(X393)|(p1(esk100_6(X385,X386,X387,X388,X389,X390))|~r1(X389,X390)|~r1(X388,X389))|~r1(X387,X388)|~r1(X386,X387)|~r1(X385,X386)|~r1(esk1_0,X385)))))&((r1(X397,esk102_4(X394,X395,X396,X397))|(~r1(X397,X398)|(~r1(X398,X399)|p1(X399)))|~r1(X396,X397)|~r1(X395,X396)|~r1(X394,X395)|~r1(esk1_0,X394))&(~p1(esk102_4(X394,X395,X396,X397))|(~r1(X397,X398)|(~r1(X398,X399)|p1(X399)))|~r1(X396,X397)|~r1(X395,X396)|~r1(X394,X395)|~r1(esk1_0,X394))))&((r1(X404,esk103_4(X401,X402,X403,X404))|~r1(X403,X404)|~r1(X402,X403)|~r1(X401,X402)|~r1(esk1_0,X401))&($true|~r1(X403,X404)|~r1(X402,X403)|~r1(X401,X402)|~r1(esk1_0,X401))))&(r1(esk1_0,esk104_0)&(r1(esk104_0,esk105_0)&(r1(esk105_0,esk106_0)&(r1(esk106_0,esk107_0)&(r1(esk107_0,esk108_0)&(r1(esk108_0,esk109_0)&(r1(esk109_0,esk110_0)&(r1(esk110_0,esk111_0)&(r1(esk111_0,esk112_0)&((r1(esk112_0,esk113_0)&~p1(esk113_0))&(~r1(esk113_0,X416)|p1(X416)))))))))))))&((r1(X420,esk114_4(X417,X418,X419,X420))|~r1(X419,X420)|p1(X419)|~r1(X418,X419)|~r1(X417,X418)|~r1(esk1_0,X417))&(~p1(esk114_4(X417,X418,X419,X420))|~r1(X419,X420)|p1(X419)|~r1(X418,X419)|~r1(X417,X418)|~r1(esk1_0,X417))))&((r1(X425,esk115_4(X422,X423,X424,X425))|~r1(X424,X425)|~p1(X424)|~r1(X423,X424)|~r1(X422,X423)|~r1(esk1_0,X422))&(p1(esk115_4(X422,X423,X424,X425))|~r1(X424,X425)|~p1(X424)|~r1(X423,X424)|~r1(X422,X423)|~r1(esk1_0,X422))))&(((r1(X429,esk117_3(X427,X428,X429))|(r1(X431,esk116_5(X427,X428,X429,X430,X431))|~r1(X430,X431)|~r1(X429,X430))|~r1(X428,X429)|~r1(X427,X428)|~r1(esk1_0,X427))&(~r1(esk117_3(X427,X428,X429),X434)|~p1(X434)|(r1(X431,esk116_5(X427,X428,X429,X430,X431))|~r1(X430,X431)|~r1(X429,X430))|~r1(X428,X429)|~r1(X427,X428)|~r1(esk1_0,X427)))&((r1(X429,esk117_3(X427,X428,X429))|(p1(esk116_5(X427,X428,X429,X430,X431))|~r1(X430,X431)|~r1(X429,X430))|~r1(X428,X429)|~r1(X427,X428)|~r1(esk1_0,X427))&(~r1(esk117_3(X427,X428,X429),X434)|~p1(X434)|(p1(esk116_5(X427,X428,X429,X430,X431))|~r1(X430,X431)|~r1(X429,X430))|~r1(X428,X429)|~r1(X427,X428)|~r1(esk1_0,X427)))))&((r1(X437,esk118_3(X435,X436,X437))|(~r1(X437,X438)|(~r1(X438,X439)|p1(X439)))|~r1(X436,X437)|~r1(X435,X436)|~r1(esk1_0,X435))&(~p1(esk118_3(X435,X436,X437))|(~r1(X437,X438)|(~r1(X438,X439)|p1(X439)))|~r1(X436,X437)|~r1(X435,X436)|~r1(esk1_0,X435))))&((r1(X443,esk119_3(X441,X442,X443))|~r1(X442,X443)|~r1(X441,X442)|~r1(esk1_0,X441))&($true|~r1(X442,X443)|~r1(X441,X442)|~r1(esk1_0,X441))))&(r1(esk1_0,esk120_0)&(r1(esk120_0,esk121_0)&(r1(esk121_0,esk122_0)&(r1(esk122_0,esk123_0)&(r1(esk123_0,esk124_0)&(r1(esk124_0,esk125_0)&(r1(esk125_0,esk126_0)&(r1(esk126_0,esk127_0)&(r1(esk127_0,esk128_0)&((r1(esk128_0,esk129_0)&~p1(esk129_0))&(~r1(esk129_0,X455)|p1(X455)))))))))))))&((r1(X458,esk130_3(X456,X457,X458))|~r1(X457,X458)|p1(X457)|~r1(X456,X457)|~r1(esk1_0,X456))&(~p1(esk130_3(X456,X457,X458))|~r1(X457,X458)|p1(X457)|~r1(X456,X457)|~r1(esk1_0,X456))))&((r1(X462,esk131_3(X460,X461,X462))|~r1(X461,X462)|~p1(X461)|~r1(X460,X461)|~r1(esk1_0,X460))&(p1(esk131_3(X460,X461,X462))|~r1(X461,X462)|~p1(X461)|~r1(X460,X461)|~r1(esk1_0,X460))))&(((r1(X465,esk133_2(X464,X465))|(r1(X467,esk132_4(X464,X465,X466,X467))|~r1(X466,X467)|~r1(X465,X466))|~r1(X464,X465)|~r1(esk1_0,X464))&(~r1(esk133_2(X464,X465),X470)|~p1(X470)|(r1(X467,esk132_4(X464,X465,X466,X467))|~r1(X466,X467)|~r1(X465,X466))|~r1(X464,X465)|~r1(esk1_0,X464)))&((r1(X465,esk133_2(X464,X465))|(p1(esk132_4(X464,X465,X466,X467))|~r1(X466,X467)|~r1(X465,X466))|~r1(X464,X465)|~r1(esk1_0,X464))&(~r1(esk133_2(X464,X465),X470)|~p1(X470)|(p1(esk132_4(X464,X465,X466,X467))|~r1(X466,X467)|~r1(X465,X466))|~r1(X464,X465)|~r1(esk1_0,X464)))))&((r1(X472,esk134_2(X471,X472))|(~r1(X472,X473)|(~r1(X473,X474)|p1(X474)))|~r1(X471,X472)|~r1(esk1_0,X471))&(~p1(esk134_2(X471,X472))|(~r1(X472,X473)|(~r1(X473,X474)|p1(X474)))|~r1(X471,X472)|~r1(esk1_0,X471))))&((r1(X477,esk135_2(X476,X477))|~r1(X476,X477)|~r1(esk1_0,X476))&($true|~r1(X476,X477)|~r1(esk1_0,X476))))&(r1(esk1_0,esk136_0)&(r1(esk136_0,esk137_0)&(r1(esk137_0,esk138_0)&(r1(esk138_0,esk139_0)&(r1(esk139_0,esk140_0)&(r1(esk140_0,esk141_0)&(r1(esk141_0,esk142_0)&(r1(esk142_0,esk143_0)&(r1(esk143_0,esk144_0)&((r1(esk144_0,esk145_0)&~p1(esk145_0))&(~r1(esk145_0,X489)|p1(X489)))))))))))))&((r1(X491,esk146_2(X490,X491))|~r1(X490,X491)|p1(X490)|~r1(esk1_0,X490))&(~p1(esk146_2(X490,X491))|~r1(X490,X491)|p1(X490)|~r1(esk1_0,X490))))&((r1(X494,esk147_2(X493,X494))|~r1(X493,X494)|~p1(X493)|~r1(esk1_0,X493))&(p1(esk147_2(X493,X494))|~r1(X493,X494)|~p1(X493)|~r1(esk1_0,X493))))&(((r1(X496,esk149_1(X496))|(r1(X498,esk148_3(X496,X497,X498))|~r1(X497,X498)|~r1(X496,X497))|~r1(esk1_0,X496))&(~r1(esk149_1(X496),X501)|~p1(X501)|(r1(X498,esk148_3(X496,X497,X498))|~r1(X497,X498)|~r1(X496,X497))|~r1(esk1_0,X496)))&((r1(X496,esk149_1(X496))|(p1(esk148_3(X496,X497,X498))|~r1(X497,X498)|~r1(X496,X497))|~r1(esk1_0,X496))&(~r1(esk149_1(X496),X501)|~p1(X501)|(p1(esk148_3(X496,X497,X498))|~r1(X497,X498)|~r1(X496,X497))|~r1(esk1_0,X496)))))&((r1(X502,esk150_1(X502))|(~r1(X502,X503)|(~r1(X503,X504)|p1(X504)))|~r1(esk1_0,X502))&(~p1(esk150_1(X502))|(~r1(X502,X503)|(~r1(X503,X504)|p1(X504)))|~r1(esk1_0,X502))))&((r1(X506,esk151_1(X506))|~r1(esk1_0,X506))&($true|~r1(esk1_0,X506))))&(r1(esk1_0,esk152_0)&(r1(esk152_0,esk153_0)&(r1(esk153_0,esk154_0)&(r1(esk154_0,esk155_0)&(r1(esk155_0,esk156_0)&(r1(esk156_0,esk157_0)&(r1(esk157_0,esk158_0)&(r1(esk158_0,esk159_0)&(r1(esk159_0,esk160_0)&((r1(esk160_0,esk161_0)&~p1(esk161_0))&(~r1(esk161_0,X518)|p1(X518)))))))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_1])])])])])])).
% 251.95/37.47 cnf(c_0_3, negated_conjecture, (r1(X1,esk18_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1))|p1(X10)|~r1(X10,X1)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_4, negated_conjecture, (r1(esk1_0,esk152_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_5, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,X3,X4,X5,X6,X7,X8,X9,X1,X2))|~r1(esk152_0,X3)|~r1(X1,X2)|~r1(X9,X1)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_3, c_0_4])).
% 251.95/37.47 cnf(c_0_6, negated_conjecture, (r1(esk152_0,esk153_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_7, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,X3,X4,X5,X6,X7,X8,X1,X2))|~r1(esk153_0,X3)|~r1(X1,X2)|~r1(X8,X1)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_5, c_0_6])).
% 251.95/37.47 cnf(c_0_8, negated_conjecture, (r1(esk153_0,esk154_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_9, negated_conjecture, (r1(X1,esk19_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1))|~r1(X10,X1)|~p1(X10)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_10, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,X3,X4,X5,X6,X7,X1,X2))|~r1(esk154_0,X3)|~r1(X1,X2)|~r1(X7,X1)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 251.95/37.47 cnf(c_0_11, negated_conjecture, (r1(esk154_0,esk155_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_12, negated_conjecture, (r1(X1,esk6_10(X2,X3,X4,X5,X6,X7,X8,X9,X10,X1))|p1(X12)|~r1(X1,X11)|~r1(X11,X12)|~r1(X10,X1)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_13, negated_conjecture, (r1(X1,esk19_10(esk152_0,X2,X3,X4,X5,X6,X7,X8,X9,X1))|~p1(X9)|~r1(esk152_0,X2)|~r1(X9,X1)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_9, c_0_4])).
% 251.95/37.47 cnf(c_0_14, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,X3,X4,X5,X6,X1,X2))|~r1(esk155_0,X3)|~r1(X1,X2)|~r1(X6,X1)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 251.95/37.47 cnf(c_0_15, negated_conjecture, (r1(esk155_0,esk156_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_16, negated_conjecture, (r1(X1,esk2_11(X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1))|p1(X11)|~r1(X11,X1)|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_17, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,X3,X4,X5,X6,X7,X8,X9,X10,X2))|~r1(esk152_0,X3)|~r1(X11,X1)|~r1(X10,X2)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X11)), inference(spm,[status(thm)],[c_0_12, c_0_4])).
% 251.95/37.47 cnf(c_0_18, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,X2,X3,X4,X5,X6,X7,X8,X1))|~p1(X8)|~r1(esk153_0,X2)|~r1(X8,X1)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_13, c_0_6])).
% 251.95/37.47 cnf(c_0_19, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,X3,X4,X5,X1,X2))|~r1(esk156_0,X3)|~r1(X1,X2)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 251.95/37.47 cnf(c_0_20, negated_conjecture, (r1(esk156_0,esk157_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_21, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,X3,X4,X5,X6,X7,X8,X9,X10,X1,X2))|~r1(esk152_0,X3)|~r1(X1,X2)|~r1(X10,X1)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_16, c_0_4])).
% 251.95/37.47 cnf(c_0_22, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,X3,X4,X5,X6,X7,X8,X9,X2))|~r1(esk153_0,X3)|~r1(X10,X1)|~r1(X9,X2)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X10)), inference(spm,[status(thm)],[c_0_17, c_0_6])).
% 251.95/37.47 cnf(c_0_23, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,X2,X3,X4,X5,X6,X7,X1))|~p1(X7)|~r1(esk154_0,X2)|~r1(X7,X1)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_18, c_0_8])).
% 251.95/37.47 cnf(c_0_24, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,X3,X4,X1,X2))|~r1(esk157_0,X3)|~r1(X1,X2)|~r1(X4,X1)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 251.95/37.47 cnf(c_0_25, negated_conjecture, (r1(esk157_0,esk158_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_26, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,X3,X4,X5,X6,X7,X8,X9,X1,X2))|~r1(esk153_0,X3)|~r1(X1,X2)|~r1(X9,X1)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_21, c_0_6])).
% 251.95/37.47 cnf(c_0_27, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,X3,X4,X5,X6,X7,X8,X2))|~r1(esk154_0,X3)|~r1(X9,X1)|~r1(X8,X2)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X9)), inference(spm,[status(thm)],[c_0_22, c_0_8])).
% 251.95/37.47 cnf(c_0_28, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,X2,X3,X4,X5,X6,X1))|~p1(X6)|~r1(esk155_0,X2)|~r1(X6,X1)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_23, c_0_11])).
% 251.95/37.47 cnf(c_0_29, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,X3,X1,X2))|~r1(esk158_0,X3)|~r1(X1,X2)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 251.95/37.47 cnf(c_0_30, negated_conjecture, (r1(esk158_0,esk159_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_31, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,X3,X4,X5,X6,X7,X8,X1,X2))|~r1(esk154_0,X3)|~r1(X1,X2)|~r1(X8,X1)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_26, c_0_8])).
% 251.95/37.47 cnf(c_0_32, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,X3,X4,X5,X6,X7,X2))|~r1(esk155_0,X3)|~r1(X8,X1)|~r1(X7,X2)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X8)), inference(spm,[status(thm)],[c_0_27, c_0_11])).
% 251.95/37.47 cnf(c_0_33, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,X2,X3,X4,X5,X1))|~p1(X5)|~r1(esk156_0,X2)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_28, c_0_15])).
% 251.95/37.47 cnf(c_0_34, negated_conjecture, (p1(X1)|r1(X2,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,X1,X2))|~r1(esk159_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 251.95/37.47 cnf(c_0_35, negated_conjecture, (r1(esk159_0,esk160_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_36, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,X3,X4,X5,X6,X7,X1,X2))|~r1(esk155_0,X3)|~r1(X1,X2)|~r1(X7,X1)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_31, c_0_11])).
% 251.95/37.47 cnf(c_0_37, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,X3,X4,X5,X6,X2))|~r1(esk156_0,X3)|~r1(X7,X1)|~r1(X6,X2)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X7)), inference(spm,[status(thm)],[c_0_32, c_0_15])).
% 251.95/37.47 cnf(c_0_38, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,X2,X3,X4,X1))|~p1(X4)|~r1(esk157_0,X2)|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_33, c_0_20])).
% 251.95/37.47 cnf(c_0_39, negated_conjecture, (p1(esk160_0)|r1(X1,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,X1))|~r1(esk160_0,X1)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 251.95/37.47 cnf(c_0_40, negated_conjecture, (r1(esk160_0,esk161_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_41, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,X3,X4,X5,X6,X1,X2))|~r1(esk156_0,X3)|~r1(X1,X2)|~r1(X6,X1)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_36, c_0_15])).
% 251.95/37.47 cnf(c_0_42, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,X3,X4,X5,X2))|~r1(esk157_0,X3)|~r1(X6,X1)|~r1(X5,X2)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X6)), inference(spm,[status(thm)],[c_0_37, c_0_20])).
% 251.95/37.47 cnf(c_0_43, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,X2,X3,X1))|~p1(X3)|~r1(esk158_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_38, c_0_25])).
% 251.95/37.47 cnf(c_0_44, negated_conjecture, (p1(X1)|~r1(esk161_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_45, negated_conjecture, (p1(esk160_0)|r1(esk161_0,esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 251.95/37.47 cnf(c_0_46, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,X3,X4,X5,X1,X2))|~r1(esk157_0,X3)|~r1(X1,X2)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_41, c_0_20])).
% 251.95/37.47 cnf(c_0_47, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,X3,X4,X2))|~r1(esk158_0,X3)|~r1(X5,X1)|~r1(X4,X2)|~r1(X3,X4)|~r1(X2,X5)), inference(spm,[status(thm)],[c_0_42, c_0_25])).
% 251.95/37.47 cnf(c_0_48, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,X2,X1))|~p1(X2)|~r1(esk159_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_43, c_0_30])).
% 251.95/37.47 cnf(c_0_49, negated_conjecture, (p1(X9)|~p1(esk18_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10))|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_50, negated_conjecture, (p1(esk18_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))|p1(esk160_0)), inference(spm,[status(thm)],[c_0_44, c_0_45])).
% 251.95/37.47 cnf(c_0_51, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,X3,X4,X1,X2))|~r1(esk158_0,X3)|~r1(X1,X2)|~r1(X4,X1)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_46, c_0_25])).
% 251.95/37.47 cnf(c_0_52, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,X3,X2))|~r1(esk159_0,X3)|~r1(X4,X1)|~r1(X3,X2)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_47, c_0_30])).
% 251.95/37.47 cnf(c_0_53, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,X1))|~p1(esk160_0)|~r1(esk160_0,X1)), inference(spm,[status(thm)],[c_0_48, c_0_35])).
% 251.95/37.47 cnf(c_0_54, negated_conjecture, (p1(esk160_0)), 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(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_49, c_0_50]), c_0_4]), c_0_40]), c_0_35]), c_0_30]), c_0_25]), c_0_20]), c_0_15]), c_0_11]), c_0_8]), c_0_6])])).
% 251.95/37.47 cnf(c_0_55, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,X3,X1,X2))|~r1(esk159_0,X3)|~r1(X1,X2)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_51, c_0_30])).
% 251.95/37.47 cnf(c_0_56, negated_conjecture, (p1(X1)|r1(X2,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,X2))|~r1(esk160_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_52, c_0_35])).
% 251.95/37.47 cnf(c_0_57, negated_conjecture, (r1(X1,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,X1))|~r1(esk160_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 251.95/37.47 cnf(c_0_58, negated_conjecture, (p1(X1)|r1(X2,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,X1,X2))|~r1(esk160_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_55, c_0_35])).
% 251.95/37.47 cnf(c_0_59, negated_conjecture, (~p1(esk161_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_60, negated_conjecture, (p1(X1)|r1(esk161_0,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))|~r1(esk161_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_56, c_0_40])).
% 251.95/37.47 cnf(c_0_61, negated_conjecture, (r1(esk161_0,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))), inference(spm,[status(thm)],[c_0_57, c_0_40])).
% 251.95/37.47 cnf(c_0_62, negated_conjecture, (r1(X1,esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0,X1))|~r1(esk161_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_40]), c_0_59])).
% 251.95/37.47 cnf(c_0_63, negated_conjecture, (p1(X1)|r1(esk161_0,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))|~r1(esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0),X1)), inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 251.95/37.47 cnf(c_0_64, negated_conjecture, (r1(esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0),esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0)))), inference(spm,[status(thm)],[c_0_62, c_0_61])).
% 251.95/37.47 cnf(c_0_65, negated_conjecture, (p1(X10)|~p1(esk2_11(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11))|~r1(X10,X11)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_66, negated_conjecture, (p1(esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0)))|r1(esk161_0,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))), inference(spm,[status(thm)],[c_0_63, c_0_64])).
% 251.95/37.47 cnf(c_0_67, negated_conjecture, (r1(esk161_0,esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))), inference(sr,[status(thm)],[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(rw,[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_65, c_0_66]), c_0_4]), c_0_61]), c_0_40]), c_0_35]), c_0_30]), c_0_25]), c_0_20]), c_0_15]), c_0_11]), c_0_8]), c_0_6])]), c_0_59])).
% 251.95/37.47 cnf(c_0_68, negated_conjecture, (p1(X12)|~p1(esk6_10(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10))|~r1(X10,X11)|~r1(X11,X12)|~r1(X9,X10)|~r1(X8,X9)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 251.95/37.47 cnf(c_0_69, negated_conjecture, (p1(esk6_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0))), inference(spm,[status(thm)],[c_0_44, c_0_67])).
% 251.95/37.47 cnf(c_0_70, negated_conjecture, (p1(X1)|~r1(esk161_0,X2)|~r1(X2,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(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_68, c_0_69]), c_0_4]), c_0_40]), c_0_35]), c_0_30]), c_0_25]), c_0_20]), c_0_15]), c_0_11]), c_0_8]), c_0_6])])).
% 251.95/37.47 cnf(c_0_71, negated_conjecture, (p1(X1)|~r1(esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0),X1)), inference(spm,[status(thm)],[c_0_70, c_0_61])).
% 251.95/37.47 cnf(c_0_72, negated_conjecture, (p1(esk2_11(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0,esk19_10(esk152_0,esk153_0,esk154_0,esk155_0,esk156_0,esk157_0,esk158_0,esk159_0,esk160_0,esk161_0)))), inference(spm,[status(thm)],[c_0_71, c_0_64])).
% 251.95/37.47 cnf(c_0_73, negated_conjecture, ($false), inference(sr,[status(thm)],[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(rw,[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_65, c_0_72]), c_0_4]), c_0_61]), c_0_40]), c_0_35]), c_0_30]), c_0_25]), c_0_20]), c_0_15]), c_0_11]), c_0_8]), c_0_6])]), c_0_59]), ['proof']).
% 251.95/37.47 % SZS output end Proof
% 251.95/37.47 % User time : 34.768 s
% 251.95/37.47 % System time : 0.179 s
% 251.95/37.47 % Total time : 34.947 s
% 251.95/37.47 % User time : 34.774 s
% 251.95/37.47 % System time : 0.185 s
% 251.95/37.47 % Total time : 34.959 s
% 251.95/37.47
%------------------------------------------------------------------------------