%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL672+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n008.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:26 AM UTC 2026
% Result : Theorem 47.60s 7.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL672+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.33 % Computer : n008.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Fri Sep 4 20:28:23 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.12/0.46 start to proof:theBenchmark.p
% 47.60/7.53 % Version : CSI_E---1.1
% 47.60/7.53 % Problem : theBenchmark.p
% 47.60/7.53 % Proof found!
% 47.60/7.53 % SZS status Theorem for theBenchmark.p
% 47.60/7.53 % SZS output start Proof
% 47.60/7.53 fof(main, conjecture, ~(?[X1]:(~((((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|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))))))))&p1(X1)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![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))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))|((~(![X2]:((~(r1(X1,X2))|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))))))))&p1(X1)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|p1(X2)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![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))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(((~(![X1]:((~(r1(X2,X1))|p2(X1))))&~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~$true)))))))&~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~((~(![X1]:((~(r1(X2,X1))|~(![X2]:((~(r1(X1,X2))|~(p1(X2))))))))&p1(X2)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![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))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|((~(![X2]:((~(r1(X1,X2))|p2(X2))))&~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|~$true)))))))&~(![X2]:((~(r1(X1,X2))|p1(X2)))))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(X2)))|![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|p2(X1)))|![X1]:((~(r1(X2,X1))|![X2]:((~(r1(X1,X2))|p2(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))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2)))))|![X1]:((~(r1(X2,X1))|p1(X1)))))|![X2]:((~(r1(X1,X2))|p1(X2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 47.60/7.53 fof(transitivity, axiom, ![X1, X2, X3]:(((r1(X1,X2)&r1(X2,X3))=>r1(X1,X3))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', transitivity)).
% 47.60/7.53 fof(reflexivity, axiom, ![X1]:(r1(X1,X1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity)).
% 47.60/7.53 fof(c_0_3, negated_conjecture, ~(~(?[X1]:(~((((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2)))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|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)))))))&p1(X1)))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![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)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2)))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true))))))))&~(![X2]:((~r1(X1,X2)|p1(X2))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))|((~(![X2]:((~r1(X1,X2)|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)))))))&p1(X1)))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|p1(X2)))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![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)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(((~(![X1]:((~r1(X2,X1)|p2(X1))))&~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~($true))))))))&~(![X1]:((~r1(X2,X1)|p1(X1))))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~((~(![X1]:((~r1(X2,X1)|~(![X2]:((~r1(X1,X2)|~p1(X2)))))))&p1(X2)))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![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)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|((~(![X2]:((~r1(X1,X2)|p2(X2))))&~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|~($true))))))))&~(![X2]:((~r1(X1,X2)|p1(X2)))))|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(X2)))|![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|p2(X1)))|![X1]:((~r1(X2,X1)|![X2]:((~r1(X1,X2)|p2(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)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))|![X1]:((~r1(X2,X1)|p1(X1)))))|![X2]:((~r1(X1,X2)|p1(X2)))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 47.60/7.53 fof(c_0_4, plain, ![X5, X6, X7]:((~r1(X5,X6)|~r1(X6,X7)|r1(X5,X7))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity])])])).
% 47.60/7.53 fof(c_0_5, negated_conjecture, ![X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X21, X22, X23, X24, X25, X26, X27, X28, X29, X30, X31, X32, X33, X34, X35, X36, X37, X39, X40, X41, X42, X43, X44, X45, X46, X47, X48, X49, X50, X51, X52, X53, X54, X55, X57, X58, X60, X61, X62, X63, X64, X65, X66, X67, X68, X69, X70, X71, X72, X73, X74, X76, X77, X78, X79, X80, X92, X99, X100, X101, X102, X103, X104, X105, X106, X107, X109, X110, X111, X112, X113, X114, X115, X116, X117, X118, X119, X120, X121, X122, X124, X125, X126, X127, X128, X129, X130, X131, X132, X133, X134, X135, X136, X137, X139, X140, X142, X143, X144, X145, X146, X147, X148, X149, X150, X151, X152, X153, X155, X156, X157, X158, X170, X177, X178, X179, X180, X181, X182, X183, X185, X186, X187, X188, X189, X190, X191, X192, X193, X194, X195, X197, X198, X199, X200, X201, X202, X203, X204, X205, X206, X207, X209, X210, X212, X213, X214, X215, X216, X217, X218, X219, X220, X222, X223, X224, X236, X243, X244, X245, X246, X247, X249, X250, X251, X252, X253, X254, X255, X256, X258, X259, X260, X261, X262, X263, X264, X265, X267, X268, X270, X271, X272, X273, X274, X275, X277, X278, X290, X297, X298, X299, X301, X302, X303, X304, X305, X307, X308, X309, X310, X311, X313, X314, X316, X317, X318, X320, X332]:(((((((((((((((((((((((((((((((((((((r1(X19,esk2_6(X10,X12,X14,X16,X18,X19))|~r1(X18,X19)|~p1(X18)|~r1(X16,X18)|(~r1(X16,X17)|p2(X17))|(~r1(X16,X21)|p1(X21))|~r1(X14,X16)|(~r1(X14,X15)|p2(X15))|(~r1(X14,X22)|p1(X22))|~r1(X12,X14)|(~r1(X12,X13)|p2(X13))|(~r1(X12,X23)|p1(X23))|~r1(X10,X12)|(~r1(X10,X11)|p2(X11))|(~r1(X10,X24)|p1(X24))|~r1(esk1_0,X10)|(~r1(esk1_0,X9)|p2(X9))|(~r1(esk1_0,X25)|p1(X25)))&(p1(esk2_6(X10,X12,X14,X16,X18,X19))|~r1(X18,X19)|~p1(X18)|~r1(X16,X18)|(~r1(X16,X17)|p2(X17))|(~r1(X16,X21)|p1(X21))|~r1(X14,X16)|(~r1(X14,X15)|p2(X15))|(~r1(X14,X22)|p1(X22))|~r1(X12,X14)|(~r1(X12,X13)|p2(X13))|(~r1(X12,X23)|p1(X23))|~r1(X10,X12)|(~r1(X10,X11)|p2(X11))|(~r1(X10,X24)|p1(X24))|~r1(esk1_0,X10)|(~r1(esk1_0,X9)|p2(X9))|(~r1(esk1_0,X25)|p1(X25))))&((r1(X37,esk3_7(X27,X29,X31,X33,X35,X36,X37))|~r1(X36,X37)|(~r1(X36,X39)|p1(X39))|~r1(X35,X36)|~r1(X33,X35)|(~r1(X33,X34)|p2(X34))|(~r1(X33,X40)|p1(X40))|~r1(X31,X33)|(~r1(X31,X32)|p2(X32))|(~r1(X31,X41)|p1(X41))|~r1(X29,X31)|(~r1(X29,X30)|p2(X30))|(~r1(X29,X42)|p1(X42))|~r1(X27,X29)|(~r1(X27,X28)|p2(X28))|(~r1(X27,X43)|p1(X43))|~r1(esk1_0,X27)|(~r1(esk1_0,X26)|p2(X26))|(~r1(esk1_0,X44)|p1(X44)))&(~p1(esk3_7(X27,X29,X31,X33,X35,X36,X37))|~r1(X36,X37)|(~r1(X36,X39)|p1(X39))|~r1(X35,X36)|~r1(X33,X35)|(~r1(X33,X34)|p2(X34))|(~r1(X33,X40)|p1(X40))|~r1(X31,X33)|(~r1(X31,X32)|p2(X32))|(~r1(X31,X41)|p1(X41))|~r1(X29,X31)|(~r1(X29,X30)|p2(X30))|(~r1(X29,X42)|p1(X42))|~r1(X27,X29)|(~r1(X27,X28)|p2(X28))|(~r1(X27,X43)|p1(X43))|~r1(esk1_0,X27)|(~r1(esk1_0,X26)|p2(X26))|(~r1(esk1_0,X44)|p1(X44)))))&(((r1(X58,esk5_6(X46,X48,X50,X52,X54,X58))|~r1(X54,X58)|(r1(X55,esk4_6(X46,X48,X50,X52,X54,X55))|~r1(X54,X55))|~r1(X52,X54)|(~r1(X52,X53)|p2(X53))|(~r1(X52,X60)|p1(X60))|~r1(X50,X52)|(~r1(X50,X51)|p2(X51))|(~r1(X50,X61)|p1(X61))|~r1(X48,X50)|(~r1(X48,X49)|p2(X49))|(~r1(X48,X62)|p1(X62))|~r1(X46,X48)|(~r1(X46,X47)|p2(X47))|(~r1(X46,X63)|p1(X63))|~r1(esk1_0,X46)|(~r1(esk1_0,X45)|p2(X45))|(~r1(esk1_0,X64)|p1(X64)))&(~p1(esk5_6(X46,X48,X50,X52,X54,X58))|~r1(X54,X58)|(r1(X55,esk4_6(X46,X48,X50,X52,X54,X55))|~r1(X54,X55))|~r1(X52,X54)|(~r1(X52,X53)|p2(X53))|(~r1(X52,X60)|p1(X60))|~r1(X50,X52)|(~r1(X50,X51)|p2(X51))|(~r1(X50,X61)|p1(X61))|~r1(X48,X50)|(~r1(X48,X49)|p2(X49))|(~r1(X48,X62)|p1(X62))|~r1(X46,X48)|(~r1(X46,X47)|p2(X47))|(~r1(X46,X63)|p1(X63))|~r1(esk1_0,X46)|(~r1(esk1_0,X45)|p2(X45))|(~r1(esk1_0,X64)|p1(X64))))&((r1(X58,esk5_6(X46,X48,X50,X52,X54,X58))|~r1(X54,X58)|(~r1(esk4_6(X46,X48,X50,X52,X54,X55),X57)|p1(X57)|~r1(X54,X55))|~r1(X52,X54)|(~r1(X52,X53)|p2(X53))|(~r1(X52,X60)|p1(X60))|~r1(X50,X52)|(~r1(X50,X51)|p2(X51))|(~r1(X50,X61)|p1(X61))|~r1(X48,X50)|(~r1(X48,X49)|p2(X49))|(~r1(X48,X62)|p1(X62))|~r1(X46,X48)|(~r1(X46,X47)|p2(X47))|(~r1(X46,X63)|p1(X63))|~r1(esk1_0,X46)|(~r1(esk1_0,X45)|p2(X45))|(~r1(esk1_0,X64)|p1(X64)))&(~p1(esk5_6(X46,X48,X50,X52,X54,X58))|~r1(X54,X58)|(~r1(esk4_6(X46,X48,X50,X52,X54,X55),X57)|p1(X57)|~r1(X54,X55))|~r1(X52,X54)|(~r1(X52,X53)|p2(X53))|(~r1(X52,X60)|p1(X60))|~r1(X50,X52)|(~r1(X50,X51)|p2(X51))|(~r1(X50,X61)|p1(X61))|~r1(X48,X50)|(~r1(X48,X49)|p2(X49))|(~r1(X48,X62)|p1(X62))|~r1(X46,X48)|(~r1(X46,X47)|p2(X47))|(~r1(X46,X63)|p1(X63))|~r1(esk1_0,X46)|(~r1(esk1_0,X45)|p2(X45))|(~r1(esk1_0,X64)|p1(X64))))))&((r1(X74,esk6_5(X66,X68,X70,X72,X74))|~r1(X72,X74)|(~r1(X72,X73)|p2(X73))|(~r1(X72,X76)|p1(X76))|~r1(X70,X72)|(~r1(X70,X71)|p2(X71))|(~r1(X70,X77)|p1(X77))|~r1(X68,X70)|(~r1(X68,X69)|p2(X69))|(~r1(X68,X78)|p1(X78))|~r1(X66,X68)|(~r1(X66,X67)|p2(X67))|(~r1(X66,X79)|p1(X79))|~r1(esk1_0,X66)|(~r1(esk1_0,X65)|p2(X65))|(~r1(esk1_0,X80)|p1(X80)))&($true|~r1(X72,X74)|(~r1(X72,X73)|p2(X73))|(~r1(X72,X76)|p1(X76))|~r1(X70,X72)|(~r1(X70,X71)|p2(X71))|(~r1(X70,X77)|p1(X77))|~r1(X68,X70)|(~r1(X68,X69)|p2(X69))|(~r1(X68,X78)|p1(X78))|~r1(X66,X68)|(~r1(X66,X67)|p2(X67))|(~r1(X66,X79)|p1(X79))|~r1(esk1_0,X66)|(~r1(esk1_0,X65)|p2(X65))|(~r1(esk1_0,X80)|p1(X80)))))&(r1(esk1_0,esk7_0)&~p2(esk7_0)))&(((r1(esk1_0,esk8_0)&(r1(esk8_0,esk9_0)&~p2(esk9_0)))&(((r1(esk8_0,esk10_0)&(r1(esk10_0,esk11_0)&~p2(esk11_0)))&(((r1(esk10_0,esk12_0)&(r1(esk12_0,esk13_0)&~p2(esk13_0)))&(((r1(esk12_0,esk14_0)&(r1(esk14_0,esk15_0)&~p2(esk15_0)))&((r1(esk14_0,esk16_0)&(r1(esk16_0,esk17_0)&(~r1(esk17_0,X92)|p1(X92))))&(r1(esk16_0,esk18_0)&~p1(esk18_0))))&(r1(esk14_0,esk19_0)&~p1(esk19_0))))&(r1(esk12_0,esk20_0)&~p1(esk20_0))))&(r1(esk10_0,esk21_0)&~p1(esk21_0))))&(r1(esk8_0,esk22_0)&~p1(esk22_0))))&(r1(esk1_0,esk23_0)&~p1(esk23_0)))&((r1(X107,esk24_5(X100,X102,X104,X106,X107))|~r1(X106,X107)|~p1(X106)|~r1(X104,X106)|(~r1(X104,X105)|p2(X105))|(~r1(X104,X109)|p1(X109))|~r1(X102,X104)|(~r1(X102,X103)|p2(X103))|(~r1(X102,X110)|p1(X110))|~r1(X100,X102)|(~r1(X100,X101)|p2(X101))|(~r1(X100,X111)|p1(X111))|~r1(esk1_0,X100)|(~r1(esk1_0,X99)|p2(X99))|(~r1(esk1_0,X112)|p1(X112)))&(p1(esk24_5(X100,X102,X104,X106,X107))|~r1(X106,X107)|~p1(X106)|~r1(X104,X106)|(~r1(X104,X105)|p2(X105))|(~r1(X104,X109)|p1(X109))|~r1(X102,X104)|(~r1(X102,X103)|p2(X103))|(~r1(X102,X110)|p1(X110))|~r1(X100,X102)|(~r1(X100,X101)|p2(X101))|(~r1(X100,X111)|p1(X111))|~r1(esk1_0,X100)|(~r1(esk1_0,X99)|p2(X99))|(~r1(esk1_0,X112)|p1(X112)))))&((r1(X122,esk25_6(X114,X116,X118,X120,X121,X122))|~r1(X121,X122)|(~r1(X121,X124)|p1(X124))|~r1(X120,X121)|~r1(X118,X120)|(~r1(X118,X119)|p2(X119))|(~r1(X118,X125)|p1(X125))|~r1(X116,X118)|(~r1(X116,X117)|p2(X117))|(~r1(X116,X126)|p1(X126))|~r1(X114,X116)|(~r1(X114,X115)|p2(X115))|(~r1(X114,X127)|p1(X127))|~r1(esk1_0,X114)|(~r1(esk1_0,X113)|p2(X113))|(~r1(esk1_0,X128)|p1(X128)))&(~p1(esk25_6(X114,X116,X118,X120,X121,X122))|~r1(X121,X122)|(~r1(X121,X124)|p1(X124))|~r1(X120,X121)|~r1(X118,X120)|(~r1(X118,X119)|p2(X119))|(~r1(X118,X125)|p1(X125))|~r1(X116,X118)|(~r1(X116,X117)|p2(X117))|(~r1(X116,X126)|p1(X126))|~r1(X114,X116)|(~r1(X114,X115)|p2(X115))|(~r1(X114,X127)|p1(X127))|~r1(esk1_0,X114)|(~r1(esk1_0,X113)|p2(X113))|(~r1(esk1_0,X128)|p1(X128)))))&(((r1(X140,esk27_5(X130,X132,X134,X136,X140))|~r1(X136,X140)|(r1(X137,esk26_5(X130,X132,X134,X136,X137))|~r1(X136,X137))|~r1(X134,X136)|(~r1(X134,X135)|p2(X135))|(~r1(X134,X142)|p1(X142))|~r1(X132,X134)|(~r1(X132,X133)|p2(X133))|(~r1(X132,X143)|p1(X143))|~r1(X130,X132)|(~r1(X130,X131)|p2(X131))|(~r1(X130,X144)|p1(X144))|~r1(esk1_0,X130)|(~r1(esk1_0,X129)|p2(X129))|(~r1(esk1_0,X145)|p1(X145)))&(~p1(esk27_5(X130,X132,X134,X136,X140))|~r1(X136,X140)|(r1(X137,esk26_5(X130,X132,X134,X136,X137))|~r1(X136,X137))|~r1(X134,X136)|(~r1(X134,X135)|p2(X135))|(~r1(X134,X142)|p1(X142))|~r1(X132,X134)|(~r1(X132,X133)|p2(X133))|(~r1(X132,X143)|p1(X143))|~r1(X130,X132)|(~r1(X130,X131)|p2(X131))|(~r1(X130,X144)|p1(X144))|~r1(esk1_0,X130)|(~r1(esk1_0,X129)|p2(X129))|(~r1(esk1_0,X145)|p1(X145))))&((r1(X140,esk27_5(X130,X132,X134,X136,X140))|~r1(X136,X140)|(~r1(esk26_5(X130,X132,X134,X136,X137),X139)|p1(X139)|~r1(X136,X137))|~r1(X134,X136)|(~r1(X134,X135)|p2(X135))|(~r1(X134,X142)|p1(X142))|~r1(X132,X134)|(~r1(X132,X133)|p2(X133))|(~r1(X132,X143)|p1(X143))|~r1(X130,X132)|(~r1(X130,X131)|p2(X131))|(~r1(X130,X144)|p1(X144))|~r1(esk1_0,X130)|(~r1(esk1_0,X129)|p2(X129))|(~r1(esk1_0,X145)|p1(X145)))&(~p1(esk27_5(X130,X132,X134,X136,X140))|~r1(X136,X140)|(~r1(esk26_5(X130,X132,X134,X136,X137),X139)|p1(X139)|~r1(X136,X137))|~r1(X134,X136)|(~r1(X134,X135)|p2(X135))|(~r1(X134,X142)|p1(X142))|~r1(X132,X134)|(~r1(X132,X133)|p2(X133))|(~r1(X132,X143)|p1(X143))|~r1(X130,X132)|(~r1(X130,X131)|p2(X131))|(~r1(X130,X144)|p1(X144))|~r1(esk1_0,X130)|(~r1(esk1_0,X129)|p2(X129))|(~r1(esk1_0,X145)|p1(X145))))))&((r1(X153,esk28_4(X147,X149,X151,X153))|~r1(X151,X153)|(~r1(X151,X152)|p2(X152))|(~r1(X151,X155)|p1(X155))|~r1(X149,X151)|(~r1(X149,X150)|p2(X150))|(~r1(X149,X156)|p1(X156))|~r1(X147,X149)|(~r1(X147,X148)|p2(X148))|(~r1(X147,X157)|p1(X157))|~r1(esk1_0,X147)|(~r1(esk1_0,X146)|p2(X146))|(~r1(esk1_0,X158)|p1(X158)))&($true|~r1(X151,X153)|(~r1(X151,X152)|p2(X152))|(~r1(X151,X155)|p1(X155))|~r1(X149,X151)|(~r1(X149,X150)|p2(X150))|(~r1(X149,X156)|p1(X156))|~r1(X147,X149)|(~r1(X147,X148)|p2(X148))|(~r1(X147,X157)|p1(X157))|~r1(esk1_0,X147)|(~r1(esk1_0,X146)|p2(X146))|(~r1(esk1_0,X158)|p1(X158)))))&(r1(esk1_0,esk29_0)&~p2(esk29_0)))&(((r1(esk1_0,esk30_0)&(r1(esk30_0,esk31_0)&~p2(esk31_0)))&(((r1(esk30_0,esk32_0)&(r1(esk32_0,esk33_0)&~p2(esk33_0)))&(((r1(esk32_0,esk34_0)&(r1(esk34_0,esk35_0)&~p2(esk35_0)))&(((r1(esk34_0,esk36_0)&(r1(esk36_0,esk37_0)&~p2(esk37_0)))&((r1(esk36_0,esk38_0)&(r1(esk38_0,esk39_0)&(~r1(esk39_0,X170)|p1(X170))))&(r1(esk38_0,esk40_0)&~p1(esk40_0))))&(r1(esk36_0,esk41_0)&~p1(esk41_0))))&(r1(esk34_0,esk42_0)&~p1(esk42_0))))&(r1(esk32_0,esk43_0)&~p1(esk43_0))))&(r1(esk30_0,esk44_0)&~p1(esk44_0))))&(r1(esk1_0,esk45_0)&~p1(esk45_0)))&((r1(X183,esk46_4(X178,X180,X182,X183))|~r1(X182,X183)|~p1(X182)|~r1(X180,X182)|(~r1(X180,X181)|p2(X181))|(~r1(X180,X185)|p1(X185))|~r1(X178,X180)|(~r1(X178,X179)|p2(X179))|(~r1(X178,X186)|p1(X186))|~r1(esk1_0,X178)|(~r1(esk1_0,X177)|p2(X177))|(~r1(esk1_0,X187)|p1(X187)))&(p1(esk46_4(X178,X180,X182,X183))|~r1(X182,X183)|~p1(X182)|~r1(X180,X182)|(~r1(X180,X181)|p2(X181))|(~r1(X180,X185)|p1(X185))|~r1(X178,X180)|(~r1(X178,X179)|p2(X179))|(~r1(X178,X186)|p1(X186))|~r1(esk1_0,X178)|(~r1(esk1_0,X177)|p2(X177))|(~r1(esk1_0,X187)|p1(X187)))))&((r1(X195,esk47_5(X189,X191,X193,X194,X195))|~r1(X194,X195)|(~r1(X194,X197)|p1(X197))|~r1(X193,X194)|~r1(X191,X193)|(~r1(X191,X192)|p2(X192))|(~r1(X191,X198)|p1(X198))|~r1(X189,X191)|(~r1(X189,X190)|p2(X190))|(~r1(X189,X199)|p1(X199))|~r1(esk1_0,X189)|(~r1(esk1_0,X188)|p2(X188))|(~r1(esk1_0,X200)|p1(X200)))&(~p1(esk47_5(X189,X191,X193,X194,X195))|~r1(X194,X195)|(~r1(X194,X197)|p1(X197))|~r1(X193,X194)|~r1(X191,X193)|(~r1(X191,X192)|p2(X192))|(~r1(X191,X198)|p1(X198))|~r1(X189,X191)|(~r1(X189,X190)|p2(X190))|(~r1(X189,X199)|p1(X199))|~r1(esk1_0,X189)|(~r1(esk1_0,X188)|p2(X188))|(~r1(esk1_0,X200)|p1(X200)))))&(((r1(X210,esk49_4(X202,X204,X206,X210))|~r1(X206,X210)|(r1(X207,esk48_4(X202,X204,X206,X207))|~r1(X206,X207))|~r1(X204,X206)|(~r1(X204,X205)|p2(X205))|(~r1(X204,X212)|p1(X212))|~r1(X202,X204)|(~r1(X202,X203)|p2(X203))|(~r1(X202,X213)|p1(X213))|~r1(esk1_0,X202)|(~r1(esk1_0,X201)|p2(X201))|(~r1(esk1_0,X214)|p1(X214)))&(~p1(esk49_4(X202,X204,X206,X210))|~r1(X206,X210)|(r1(X207,esk48_4(X202,X204,X206,X207))|~r1(X206,X207))|~r1(X204,X206)|(~r1(X204,X205)|p2(X205))|(~r1(X204,X212)|p1(X212))|~r1(X202,X204)|(~r1(X202,X203)|p2(X203))|(~r1(X202,X213)|p1(X213))|~r1(esk1_0,X202)|(~r1(esk1_0,X201)|p2(X201))|(~r1(esk1_0,X214)|p1(X214))))&((r1(X210,esk49_4(X202,X204,X206,X210))|~r1(X206,X210)|(~r1(esk48_4(X202,X204,X206,X207),X209)|p1(X209)|~r1(X206,X207))|~r1(X204,X206)|(~r1(X204,X205)|p2(X205))|(~r1(X204,X212)|p1(X212))|~r1(X202,X204)|(~r1(X202,X203)|p2(X203))|(~r1(X202,X213)|p1(X213))|~r1(esk1_0,X202)|(~r1(esk1_0,X201)|p2(X201))|(~r1(esk1_0,X214)|p1(X214)))&(~p1(esk49_4(X202,X204,X206,X210))|~r1(X206,X210)|(~r1(esk48_4(X202,X204,X206,X207),X209)|p1(X209)|~r1(X206,X207))|~r1(X204,X206)|(~r1(X204,X205)|p2(X205))|(~r1(X204,X212)|p1(X212))|~r1(X202,X204)|(~r1(X202,X203)|p2(X203))|(~r1(X202,X213)|p1(X213))|~r1(esk1_0,X202)|(~r1(esk1_0,X201)|p2(X201))|(~r1(esk1_0,X214)|p1(X214))))))&((r1(X220,esk50_3(X216,X218,X220))|~r1(X218,X220)|(~r1(X218,X219)|p2(X219))|(~r1(X218,X222)|p1(X222))|~r1(X216,X218)|(~r1(X216,X217)|p2(X217))|(~r1(X216,X223)|p1(X223))|~r1(esk1_0,X216)|(~r1(esk1_0,X215)|p2(X215))|(~r1(esk1_0,X224)|p1(X224)))&($true|~r1(X218,X220)|(~r1(X218,X219)|p2(X219))|(~r1(X218,X222)|p1(X222))|~r1(X216,X218)|(~r1(X216,X217)|p2(X217))|(~r1(X216,X223)|p1(X223))|~r1(esk1_0,X216)|(~r1(esk1_0,X215)|p2(X215))|(~r1(esk1_0,X224)|p1(X224)))))&(r1(esk1_0,esk51_0)&~p2(esk51_0)))&(((r1(esk1_0,esk52_0)&(r1(esk52_0,esk53_0)&~p2(esk53_0)))&(((r1(esk52_0,esk54_0)&(r1(esk54_0,esk55_0)&~p2(esk55_0)))&(((r1(esk54_0,esk56_0)&(r1(esk56_0,esk57_0)&~p2(esk57_0)))&(((r1(esk56_0,esk58_0)&(r1(esk58_0,esk59_0)&~p2(esk59_0)))&((r1(esk58_0,esk60_0)&(r1(esk60_0,esk61_0)&(~r1(esk61_0,X236)|p1(X236))))&(r1(esk60_0,esk62_0)&~p1(esk62_0))))&(r1(esk58_0,esk63_0)&~p1(esk63_0))))&(r1(esk56_0,esk64_0)&~p1(esk64_0))))&(r1(esk54_0,esk65_0)&~p1(esk65_0))))&(r1(esk52_0,esk66_0)&~p1(esk66_0))))&(r1(esk1_0,esk67_0)&~p1(esk67_0)))&((r1(X247,esk68_3(X244,X246,X247))|~r1(X246,X247)|~p1(X246)|~r1(X244,X246)|(~r1(X244,X245)|p2(X245))|(~r1(X244,X249)|p1(X249))|~r1(esk1_0,X244)|(~r1(esk1_0,X243)|p2(X243))|(~r1(esk1_0,X250)|p1(X250)))&(p1(esk68_3(X244,X246,X247))|~r1(X246,X247)|~p1(X246)|~r1(X244,X246)|(~r1(X244,X245)|p2(X245))|(~r1(X244,X249)|p1(X249))|~r1(esk1_0,X244)|(~r1(esk1_0,X243)|p2(X243))|(~r1(esk1_0,X250)|p1(X250)))))&((r1(X256,esk69_4(X252,X254,X255,X256))|~r1(X255,X256)|(~r1(X255,X258)|p1(X258))|~r1(X254,X255)|~r1(X252,X254)|(~r1(X252,X253)|p2(X253))|(~r1(X252,X259)|p1(X259))|~r1(esk1_0,X252)|(~r1(esk1_0,X251)|p2(X251))|(~r1(esk1_0,X260)|p1(X260)))&(~p1(esk69_4(X252,X254,X255,X256))|~r1(X255,X256)|(~r1(X255,X258)|p1(X258))|~r1(X254,X255)|~r1(X252,X254)|(~r1(X252,X253)|p2(X253))|(~r1(X252,X259)|p1(X259))|~r1(esk1_0,X252)|(~r1(esk1_0,X251)|p2(X251))|(~r1(esk1_0,X260)|p1(X260)))))&(((r1(X268,esk71_3(X262,X264,X268))|~r1(X264,X268)|(r1(X265,esk70_3(X262,X264,X265))|~r1(X264,X265))|~r1(X262,X264)|(~r1(X262,X263)|p2(X263))|(~r1(X262,X270)|p1(X270))|~r1(esk1_0,X262)|(~r1(esk1_0,X261)|p2(X261))|(~r1(esk1_0,X271)|p1(X271)))&(~p1(esk71_3(X262,X264,X268))|~r1(X264,X268)|(r1(X265,esk70_3(X262,X264,X265))|~r1(X264,X265))|~r1(X262,X264)|(~r1(X262,X263)|p2(X263))|(~r1(X262,X270)|p1(X270))|~r1(esk1_0,X262)|(~r1(esk1_0,X261)|p2(X261))|(~r1(esk1_0,X271)|p1(X271))))&((r1(X268,esk71_3(X262,X264,X268))|~r1(X264,X268)|(~r1(esk70_3(X262,X264,X265),X267)|p1(X267)|~r1(X264,X265))|~r1(X262,X264)|(~r1(X262,X263)|p2(X263))|(~r1(X262,X270)|p1(X270))|~r1(esk1_0,X262)|(~r1(esk1_0,X261)|p2(X261))|(~r1(esk1_0,X271)|p1(X271)))&(~p1(esk71_3(X262,X264,X268))|~r1(X264,X268)|(~r1(esk70_3(X262,X264,X265),X267)|p1(X267)|~r1(X264,X265))|~r1(X262,X264)|(~r1(X262,X263)|p2(X263))|(~r1(X262,X270)|p1(X270))|~r1(esk1_0,X262)|(~r1(esk1_0,X261)|p2(X261))|(~r1(esk1_0,X271)|p1(X271))))))&((r1(X275,esk72_2(X273,X275))|~r1(X273,X275)|(~r1(X273,X274)|p2(X274))|(~r1(X273,X277)|p1(X277))|~r1(esk1_0,X273)|(~r1(esk1_0,X272)|p2(X272))|(~r1(esk1_0,X278)|p1(X278)))&($true|~r1(X273,X275)|(~r1(X273,X274)|p2(X274))|(~r1(X273,X277)|p1(X277))|~r1(esk1_0,X273)|(~r1(esk1_0,X272)|p2(X272))|(~r1(esk1_0,X278)|p1(X278)))))&(r1(esk1_0,esk73_0)&~p2(esk73_0)))&(((r1(esk1_0,esk74_0)&(r1(esk74_0,esk75_0)&~p2(esk75_0)))&(((r1(esk74_0,esk76_0)&(r1(esk76_0,esk77_0)&~p2(esk77_0)))&(((r1(esk76_0,esk78_0)&(r1(esk78_0,esk79_0)&~p2(esk79_0)))&(((r1(esk78_0,esk80_0)&(r1(esk80_0,esk81_0)&~p2(esk81_0)))&((r1(esk80_0,esk82_0)&(r1(esk82_0,esk83_0)&(~r1(esk83_0,X290)|p1(X290))))&(r1(esk82_0,esk84_0)&~p1(esk84_0))))&(r1(esk80_0,esk85_0)&~p1(esk85_0))))&(r1(esk78_0,esk86_0)&~p1(esk86_0))))&(r1(esk76_0,esk87_0)&~p1(esk87_0))))&(r1(esk74_0,esk88_0)&~p1(esk88_0))))&(r1(esk1_0,esk89_0)&~p1(esk89_0)))&((r1(X299,esk90_2(X298,X299))|~r1(X298,X299)|~p1(X298)|~r1(esk1_0,X298)|(~r1(esk1_0,X297)|p2(X297))|(~r1(esk1_0,X301)|p1(X301)))&(p1(esk90_2(X298,X299))|~r1(X298,X299)|~p1(X298)|~r1(esk1_0,X298)|(~r1(esk1_0,X297)|p2(X297))|(~r1(esk1_0,X301)|p1(X301)))))&((r1(X305,esk91_3(X303,X304,X305))|~r1(X304,X305)|(~r1(X304,X307)|p1(X307))|~r1(X303,X304)|~r1(esk1_0,X303)|(~r1(esk1_0,X302)|p2(X302))|(~r1(esk1_0,X308)|p1(X308)))&(~p1(esk91_3(X303,X304,X305))|~r1(X304,X305)|(~r1(X304,X307)|p1(X307))|~r1(X303,X304)|~r1(esk1_0,X303)|(~r1(esk1_0,X302)|p2(X302))|(~r1(esk1_0,X308)|p1(X308)))))&(((r1(X314,esk93_2(X310,X314))|~r1(X310,X314)|(r1(X311,esk92_2(X310,X311))|~r1(X310,X311))|~r1(esk1_0,X310)|(~r1(esk1_0,X309)|p2(X309))|(~r1(esk1_0,X316)|p1(X316)))&(~p1(esk93_2(X310,X314))|~r1(X310,X314)|(r1(X311,esk92_2(X310,X311))|~r1(X310,X311))|~r1(esk1_0,X310)|(~r1(esk1_0,X309)|p2(X309))|(~r1(esk1_0,X316)|p1(X316))))&((r1(X314,esk93_2(X310,X314))|~r1(X310,X314)|(~r1(esk92_2(X310,X311),X313)|p1(X313)|~r1(X310,X311))|~r1(esk1_0,X310)|(~r1(esk1_0,X309)|p2(X309))|(~r1(esk1_0,X316)|p1(X316)))&(~p1(esk93_2(X310,X314))|~r1(X310,X314)|(~r1(esk92_2(X310,X311),X313)|p1(X313)|~r1(X310,X311))|~r1(esk1_0,X310)|(~r1(esk1_0,X309)|p2(X309))|(~r1(esk1_0,X316)|p1(X316))))))&((r1(X318,esk94_1(X318))|~r1(esk1_0,X318)|(~r1(esk1_0,X317)|p2(X317))|(~r1(esk1_0,X320)|p1(X320)))&($true|~r1(esk1_0,X318)|(~r1(esk1_0,X317)|p2(X317))|(~r1(esk1_0,X320)|p1(X320)))))&(r1(esk1_0,esk95_0)&~p2(esk95_0)))&(((r1(esk1_0,esk96_0)&(r1(esk96_0,esk97_0)&~p2(esk97_0)))&(((r1(esk96_0,esk98_0)&(r1(esk98_0,esk99_0)&~p2(esk99_0)))&(((r1(esk98_0,esk100_0)&(r1(esk100_0,esk101_0)&~p2(esk101_0)))&(((r1(esk100_0,esk102_0)&(r1(esk102_0,esk103_0)&~p2(esk103_0)))&((r1(esk102_0,esk104_0)&(r1(esk104_0,esk105_0)&(~r1(esk105_0,X332)|p1(X332))))&(r1(esk104_0,esk106_0)&~p1(esk106_0))))&(r1(esk102_0,esk107_0)&~p1(esk107_0))))&(r1(esk100_0,esk108_0)&~p1(esk108_0))))&(r1(esk98_0,esk109_0)&~p1(esk109_0))))&(r1(esk96_0,esk110_0)&~p1(esk110_0))))&(r1(esk1_0,esk111_0)&~p1(esk111_0)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])])).
% 47.60/7.53 cnf(c_0_6, plain, (r1(X1,X3)|~r1(X1,X2)|~r1(X2,X3)), inference(split_conjunct,[status(thm)],[c_0_4])).
% 47.60/7.53 cnf(c_0_7, negated_conjecture, (r1(esk96_0,esk98_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_8, negated_conjecture, (r1(esk98_0,esk100_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_9, negated_conjecture, (r1(X1,esk98_0)|~r1(X1,esk96_0)), inference(spm,[status(thm)],[c_0_6, c_0_7])).
% 47.60/7.53 cnf(c_0_10, negated_conjecture, (r1(esk1_0,esk96_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_11, negated_conjecture, (r1(esk100_0,esk102_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_12, negated_conjecture, (r1(X1,esk100_0)|~r1(X1,esk98_0)), inference(spm,[status(thm)],[c_0_6, c_0_8])).
% 47.60/7.53 cnf(c_0_13, negated_conjecture, (r1(esk1_0,esk98_0)), inference(spm,[status(thm)],[c_0_9, c_0_10])).
% 47.60/7.53 cnf(c_0_14, negated_conjecture, (r1(esk102_0,esk103_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_15, negated_conjecture, (r1(X1,esk102_0)|~r1(X1,esk100_0)), inference(spm,[status(thm)],[c_0_6, c_0_11])).
% 47.60/7.53 cnf(c_0_16, negated_conjecture, (r1(esk1_0,esk100_0)), inference(spm,[status(thm)],[c_0_12, c_0_13])).
% 47.60/7.53 cnf(c_0_17, negated_conjecture, (r1(X1,esk91_3(X2,X3,X1))|p1(X4)|p2(X5)|p1(X6)|~r1(X3,X1)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)|~r1(esk1_0,X5)|~r1(esk1_0,X6)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_18, negated_conjecture, (r1(esk1_0,esk111_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_19, negated_conjecture, (~p1(esk111_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_20, negated_conjecture, (r1(X1,esk103_0)|~r1(X1,esk102_0)), inference(spm,[status(thm)],[c_0_6, c_0_14])).
% 47.60/7.53 cnf(c_0_21, negated_conjecture, (r1(esk1_0,esk102_0)), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 47.60/7.53 cnf(c_0_22, negated_conjecture, (p1(X1)|p2(X2)|r1(X3,esk91_3(X4,X5,X3))|~r1(esk1_0,X2)|~r1(esk1_0,X4)|~r1(X5,X1)|~r1(X5,X3)|~r1(X4,X5)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_19])).
% 47.60/7.53 cnf(c_0_23, negated_conjecture, (r1(esk1_0,esk103_0)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 47.60/7.53 cnf(c_0_24, negated_conjecture, (~p2(esk103_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 fof(c_0_25, plain, ![X4]:(r1(X4,X4)), inference(variable_rename,[status(thm)],[reflexivity])).
% 47.60/7.53 cnf(c_0_26, negated_conjecture, (r1(esk104_0,esk105_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_27, negated_conjecture, (p1(X1)|r1(X2,esk91_3(X3,X4,X2))|~r1(esk1_0,X3)|~r1(X4,X1)|~r1(X4,X2)|~r1(X3,X4)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_23]), c_0_24])).
% 47.60/7.53 cnf(c_0_28, plain, (r1(X1,X1)), inference(split_conjunct,[status(thm)],[c_0_25])).
% 47.60/7.53 cnf(c_0_29, negated_conjecture, (r1(X1,esk105_0)|~r1(X1,esk104_0)), inference(spm,[status(thm)],[c_0_6, c_0_26])).
% 47.60/7.53 cnf(c_0_30, negated_conjecture, (r1(esk102_0,esk104_0)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_31, negated_conjecture, (p1(X1)|r1(X2,esk91_3(esk1_0,X3,X2))|~r1(esk1_0,X3)|~r1(X3,X1)|~r1(X3,X2)), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 47.60/7.53 cnf(c_0_32, negated_conjecture, (r1(esk102_0,esk105_0)), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 47.60/7.53 cnf(c_0_33, negated_conjecture, (p1(X1)|r1(X2,esk91_3(esk1_0,esk1_0,X2))|~r1(esk1_0,X1)|~r1(esk1_0,X2)), inference(spm,[status(thm)],[c_0_31, c_0_28])).
% 47.60/7.53 cnf(c_0_34, negated_conjecture, (r1(X1,esk105_0)|~r1(X1,esk102_0)), inference(spm,[status(thm)],[c_0_6, c_0_32])).
% 47.60/7.53 cnf(c_0_35, negated_conjecture, (r1(X1,esk91_3(esk1_0,esk1_0,X1))|~r1(esk1_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_18]), c_0_19])).
% 47.60/7.53 cnf(c_0_36, negated_conjecture, (r1(esk1_0,esk105_0)), inference(spm,[status(thm)],[c_0_34, c_0_21])).
% 47.60/7.53 cnf(c_0_37, negated_conjecture, (p1(X1)|~r1(esk105_0,X1)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_38, negated_conjecture, (r1(esk105_0,esk91_3(esk1_0,esk1_0,esk105_0))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 47.60/7.53 cnf(c_0_39, negated_conjecture, (p1(X4)|p2(X5)|p1(X6)|~p1(esk91_3(X1,X2,X3))|~r1(X2,X3)|~r1(X2,X4)|~r1(X1,X2)|~r1(esk1_0,X1)|~r1(esk1_0,X5)|~r1(esk1_0,X6)), inference(split_conjunct,[status(thm)],[c_0_5])).
% 47.60/7.53 cnf(c_0_40, negated_conjecture, (p1(esk91_3(esk1_0,esk1_0,esk105_0))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 47.60/7.53 cnf(c_0_41, negated_conjecture, (p1(X1)|p1(X2)|p2(X3)|~r1(esk1_0,X1)|~r1(esk1_0,X3)|~r1(esk1_0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_28]), c_0_36])])).
% 47.60/7.53 cnf(c_0_42, negated_conjecture, (p1(X1)|p2(X2)|~r1(esk1_0,X2)|~r1(esk1_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_41, c_0_18]), c_0_19])).
% 47.60/7.53 cnf(c_0_43, negated_conjecture, (p1(X1)|~r1(esk1_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_23]), c_0_24])).
% 47.60/7.53 cnf(c_0_44, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_18]), c_0_19]), ['proof']).
% 47.60/7.54 % SZS output end Proof
% 47.60/7.54 % User time : 6.868 s
% 47.60/7.54 % System time : 0.097 s
% 47.60/7.54 % Total time : 6.965 s
% 47.60/7.54 % User time : 33.575 s
% 47.60/7.54 % System time : 0.459 s
% 47.60/7.54 % Total time : 34.034 s
% 47.60/7.54
%------------------------------------------------------------------------------