%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : LCL638+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:21:15 AM UTC 2026
% Result : Theorem 1.60s 0.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL638+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : java -jar mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 4 13:47:17 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.23/0.47 start to proof:theBenchmark.p
% 1.60/0.72 % Version : CSI_E---1.1
% 1.60/0.72 % Problem : theBenchmark.p
% 1.60/0.72 % Proof found!
% 1.60/0.72 % SZS status Theorem for theBenchmark.p
% 1.60/0.72 % SZS output start Proof
% 1.60/0.72 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))|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))|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))|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))|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))|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))|p1(X2)|~(![X1]:((~(r1(X2,X1))|p1(X1))))))))))))))|~(![X2]:((~(r1(X1,X2))|![X1]:((~(r1(X2,X1))|~((~(![X2]:((~(r1(X1,X2))|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))&~(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))|p1(X2)|~(![X1]:((~(r1(X2,X1))|p1(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))|~(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))|p1(X2)|~(![X1]:((~(r1(X2,X1))|p1(X1)))))))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', main)).
% 1.60/0.72 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)|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)|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)|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)|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)|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)|p1(X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))))))))))|~(![X2]:((~r1(X1,X2)|![X1]:((~r1(X2,X1)|~((~(![X2]:((~r1(X1,X2)|~(![X1]:((~r1(X2,X1)|p1(X1)))))))&~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)|p1(X2)|~(![X1]:((~r1(X2,X1)|p1(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)|~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)|p1(X2)|~(![X1]:((~r1(X2,X1)|p1(X1))))))))))))))))))), inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])])).
% 1.60/0.72 fof(c_0_2, negated_conjecture, ![X4, X5, X6, X7, X8, X9, X11, X12, X13, X14, X15, X16, X18, X19, X20, X21, X22, X23, X24, X27, X28, X29, X30, X31, X32, X33, X34, X36, X37, X38, X39, X40, X47, X48, X49, X50, X51, X52, X54, X55, X56, X57, X58, X60, X61, X62, X63, X64, X65, X68, X69, X70, X71, X72, X73, X74, X76, X77, X78, X79, X86, X87, X88, X89, X90, X92, X93, X94, X95, X97, X98, X99, X100, X101, X104, X105, X106, X107, X108, X109, X111, X112, X113, X120, X121, X122, X123, X125, X126, X127, X129, X130, X131, X132, X135, X136, X137, X138, X139, X141, X142, X149, X150, X151, X153, X154, X156, X157, X158, X161, X162, X163, X164, X166, X173]:((((((((((((((((((((((((((((((((r1(X9,esk2_6(X4,X5,X6,X7,X8,X9))|~r1(X8,X9)|p1(X8)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4))&(~p1(esk2_6(X4,X5,X6,X7,X8,X9))|~r1(X8,X9)|p1(X8)|~r1(X7,X8)|~r1(X6,X7)|~r1(X5,X6)|~r1(X4,X5)|~r1(esk1_0,X4)))&((r1(X16,esk3_6(X11,X12,X13,X14,X15,X16))|~r1(X15,X16)|~p1(X15)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(esk1_0,X11))&(p1(esk3_6(X11,X12,X13,X14,X15,X16))|~r1(X15,X16)|~p1(X15)|~r1(X14,X15)|~r1(X13,X14)|~r1(X12,X13)|~r1(X11,X12)|~r1(esk1_0,X11))))&(((r1(X22,esk5_5(X18,X19,X20,X21,X22))|(r1(X24,esk4_7(X18,X19,X20,X21,X22,X23,X24))|~r1(X23,X24)|~r1(X22,X23))|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(esk1_0,X18))&(~r1(esk5_5(X18,X19,X20,X21,X22),X27)|~p1(X27)|(r1(X24,esk4_7(X18,X19,X20,X21,X22,X23,X24))|~r1(X23,X24)|~r1(X22,X23))|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(esk1_0,X18)))&((r1(X22,esk5_5(X18,X19,X20,X21,X22))|(p1(esk4_7(X18,X19,X20,X21,X22,X23,X24))|~r1(X23,X24)|~r1(X22,X23))|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(esk1_0,X18))&(~r1(esk5_5(X18,X19,X20,X21,X22),X27)|~p1(X27)|(p1(esk4_7(X18,X19,X20,X21,X22,X23,X24))|~r1(X23,X24)|~r1(X22,X23))|~r1(X21,X22)|~r1(X20,X21)|~r1(X19,X20)|~r1(X18,X19)|~r1(esk1_0,X18)))))&((r1(X32,esk6_5(X28,X29,X30,X31,X32))|(~r1(X32,X33)|(~r1(X33,X34)|p1(X34)))|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28))&(~p1(esk6_5(X28,X29,X30,X31,X32))|(~r1(X32,X33)|(~r1(X33,X34)|p1(X34)))|~r1(X31,X32)|~r1(X30,X31)|~r1(X29,X30)|~r1(X28,X29)|~r1(esk1_0,X28))))&((r1(X40,esk7_5(X36,X37,X38,X39,X40))|~r1(X39,X40)|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(esk1_0,X36))&($true|~r1(X39,X40)|~r1(X38,X39)|~r1(X37,X38)|~r1(X36,X37)|~r1(esk1_0,X36))))&(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)&~p1(esk12_0))&(~r1(esk12_0,X47)|p1(X47))))))))&((r1(X52,esk13_5(X48,X49,X50,X51,X52))|~r1(X51,X52)|p1(X51)|~r1(X50,X51)|~r1(X49,X50)|~r1(X48,X49)|~r1(esk1_0,X48))&(~p1(esk13_5(X48,X49,X50,X51,X52))|~r1(X51,X52)|p1(X51)|~r1(X50,X51)|~r1(X49,X50)|~r1(X48,X49)|~r1(esk1_0,X48))))&((r1(X58,esk14_5(X54,X55,X56,X57,X58))|~r1(X57,X58)|~p1(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))&(p1(esk14_5(X54,X55,X56,X57,X58))|~r1(X57,X58)|~p1(X57)|~r1(X56,X57)|~r1(X55,X56)|~r1(X54,X55)|~r1(esk1_0,X54))))&(((r1(X63,esk16_4(X60,X61,X62,X63))|(r1(X65,esk15_6(X60,X61,X62,X63,X64,X65))|~r1(X64,X65)|~r1(X63,X64))|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(esk1_0,X60))&(~r1(esk16_4(X60,X61,X62,X63),X68)|~p1(X68)|(r1(X65,esk15_6(X60,X61,X62,X63,X64,X65))|~r1(X64,X65)|~r1(X63,X64))|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(esk1_0,X60)))&((r1(X63,esk16_4(X60,X61,X62,X63))|(p1(esk15_6(X60,X61,X62,X63,X64,X65))|~r1(X64,X65)|~r1(X63,X64))|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(esk1_0,X60))&(~r1(esk16_4(X60,X61,X62,X63),X68)|~p1(X68)|(p1(esk15_6(X60,X61,X62,X63,X64,X65))|~r1(X64,X65)|~r1(X63,X64))|~r1(X62,X63)|~r1(X61,X62)|~r1(X60,X61)|~r1(esk1_0,X60)))))&((r1(X72,esk17_4(X69,X70,X71,X72))|(~r1(X72,X73)|(~r1(X73,X74)|p1(X74)))|~r1(X71,X72)|~r1(X70,X71)|~r1(X69,X70)|~r1(esk1_0,X69))&(~p1(esk17_4(X69,X70,X71,X72))|(~r1(X72,X73)|(~r1(X73,X74)|p1(X74)))|~r1(X71,X72)|~r1(X70,X71)|~r1(X69,X70)|~r1(esk1_0,X69))))&((r1(X79,esk18_4(X76,X77,X78,X79))|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(esk1_0,X76))&($true|~r1(X78,X79)|~r1(X77,X78)|~r1(X76,X77)|~r1(esk1_0,X76))))&(r1(esk1_0,esk19_0)&(r1(esk19_0,esk20_0)&(r1(esk20_0,esk21_0)&(r1(esk21_0,esk22_0)&((r1(esk22_0,esk23_0)&~p1(esk23_0))&(~r1(esk23_0,X86)|p1(X86))))))))&((r1(X90,esk24_4(X87,X88,X89,X90))|~r1(X89,X90)|p1(X89)|~r1(X88,X89)|~r1(X87,X88)|~r1(esk1_0,X87))&(~p1(esk24_4(X87,X88,X89,X90))|~r1(X89,X90)|p1(X89)|~r1(X88,X89)|~r1(X87,X88)|~r1(esk1_0,X87))))&((r1(X95,esk25_4(X92,X93,X94,X95))|~r1(X94,X95)|~p1(X94)|~r1(X93,X94)|~r1(X92,X93)|~r1(esk1_0,X92))&(p1(esk25_4(X92,X93,X94,X95))|~r1(X94,X95)|~p1(X94)|~r1(X93,X94)|~r1(X92,X93)|~r1(esk1_0,X92))))&(((r1(X99,esk27_3(X97,X98,X99))|(r1(X101,esk26_5(X97,X98,X99,X100,X101))|~r1(X100,X101)|~r1(X99,X100))|~r1(X98,X99)|~r1(X97,X98)|~r1(esk1_0,X97))&(~r1(esk27_3(X97,X98,X99),X104)|~p1(X104)|(r1(X101,esk26_5(X97,X98,X99,X100,X101))|~r1(X100,X101)|~r1(X99,X100))|~r1(X98,X99)|~r1(X97,X98)|~r1(esk1_0,X97)))&((r1(X99,esk27_3(X97,X98,X99))|(p1(esk26_5(X97,X98,X99,X100,X101))|~r1(X100,X101)|~r1(X99,X100))|~r1(X98,X99)|~r1(X97,X98)|~r1(esk1_0,X97))&(~r1(esk27_3(X97,X98,X99),X104)|~p1(X104)|(p1(esk26_5(X97,X98,X99,X100,X101))|~r1(X100,X101)|~r1(X99,X100))|~r1(X98,X99)|~r1(X97,X98)|~r1(esk1_0,X97)))))&((r1(X107,esk28_3(X105,X106,X107))|(~r1(X107,X108)|(~r1(X108,X109)|p1(X109)))|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))&(~p1(esk28_3(X105,X106,X107))|(~r1(X107,X108)|(~r1(X108,X109)|p1(X109)))|~r1(X106,X107)|~r1(X105,X106)|~r1(esk1_0,X105))))&((r1(X113,esk29_3(X111,X112,X113))|~r1(X112,X113)|~r1(X111,X112)|~r1(esk1_0,X111))&($true|~r1(X112,X113)|~r1(X111,X112)|~r1(esk1_0,X111))))&(r1(esk1_0,esk30_0)&(r1(esk30_0,esk31_0)&(r1(esk31_0,esk32_0)&(r1(esk32_0,esk33_0)&((r1(esk33_0,esk34_0)&~p1(esk34_0))&(~r1(esk34_0,X120)|p1(X120))))))))&((r1(X123,esk35_3(X121,X122,X123))|~r1(X122,X123)|p1(X122)|~r1(X121,X122)|~r1(esk1_0,X121))&(~p1(esk35_3(X121,X122,X123))|~r1(X122,X123)|p1(X122)|~r1(X121,X122)|~r1(esk1_0,X121))))&((r1(X127,esk36_3(X125,X126,X127))|~r1(X126,X127)|~p1(X126)|~r1(X125,X126)|~r1(esk1_0,X125))&(p1(esk36_3(X125,X126,X127))|~r1(X126,X127)|~p1(X126)|~r1(X125,X126)|~r1(esk1_0,X125))))&(((r1(X130,esk38_2(X129,X130))|(r1(X132,esk37_4(X129,X130,X131,X132))|~r1(X131,X132)|~r1(X130,X131))|~r1(X129,X130)|~r1(esk1_0,X129))&(~r1(esk38_2(X129,X130),X135)|~p1(X135)|(r1(X132,esk37_4(X129,X130,X131,X132))|~r1(X131,X132)|~r1(X130,X131))|~r1(X129,X130)|~r1(esk1_0,X129)))&((r1(X130,esk38_2(X129,X130))|(p1(esk37_4(X129,X130,X131,X132))|~r1(X131,X132)|~r1(X130,X131))|~r1(X129,X130)|~r1(esk1_0,X129))&(~r1(esk38_2(X129,X130),X135)|~p1(X135)|(p1(esk37_4(X129,X130,X131,X132))|~r1(X131,X132)|~r1(X130,X131))|~r1(X129,X130)|~r1(esk1_0,X129)))))&((r1(X137,esk39_2(X136,X137))|(~r1(X137,X138)|(~r1(X138,X139)|p1(X139)))|~r1(X136,X137)|~r1(esk1_0,X136))&(~p1(esk39_2(X136,X137))|(~r1(X137,X138)|(~r1(X138,X139)|p1(X139)))|~r1(X136,X137)|~r1(esk1_0,X136))))&((r1(X142,esk40_2(X141,X142))|~r1(X141,X142)|~r1(esk1_0,X141))&($true|~r1(X141,X142)|~r1(esk1_0,X141))))&(r1(esk1_0,esk41_0)&(r1(esk41_0,esk42_0)&(r1(esk42_0,esk43_0)&(r1(esk43_0,esk44_0)&((r1(esk44_0,esk45_0)&~p1(esk45_0))&(~r1(esk45_0,X149)|p1(X149))))))))&((r1(X151,esk46_2(X150,X151))|~r1(X150,X151)|p1(X150)|~r1(esk1_0,X150))&(~p1(esk46_2(X150,X151))|~r1(X150,X151)|p1(X150)|~r1(esk1_0,X150))))&((r1(X154,esk47_2(X153,X154))|~r1(X153,X154)|~p1(X153)|~r1(esk1_0,X153))&(p1(esk47_2(X153,X154))|~r1(X153,X154)|~p1(X153)|~r1(esk1_0,X153))))&(((r1(X156,esk49_1(X156))|(r1(X158,esk48_3(X156,X157,X158))|~r1(X157,X158)|~r1(X156,X157))|~r1(esk1_0,X156))&(~r1(esk49_1(X156),X161)|~p1(X161)|(r1(X158,esk48_3(X156,X157,X158))|~r1(X157,X158)|~r1(X156,X157))|~r1(esk1_0,X156)))&((r1(X156,esk49_1(X156))|(p1(esk48_3(X156,X157,X158))|~r1(X157,X158)|~r1(X156,X157))|~r1(esk1_0,X156))&(~r1(esk49_1(X156),X161)|~p1(X161)|(p1(esk48_3(X156,X157,X158))|~r1(X157,X158)|~r1(X156,X157))|~r1(esk1_0,X156)))))&((r1(X162,esk50_1(X162))|(~r1(X162,X163)|(~r1(X163,X164)|p1(X164)))|~r1(esk1_0,X162))&(~p1(esk50_1(X162))|(~r1(X162,X163)|(~r1(X163,X164)|p1(X164)))|~r1(esk1_0,X162))))&((r1(X166,esk51_1(X166))|~r1(esk1_0,X166))&($true|~r1(esk1_0,X166))))&(r1(esk1_0,esk52_0)&(r1(esk52_0,esk53_0)&(r1(esk53_0,esk54_0)&(r1(esk54_0,esk55_0)&((r1(esk55_0,esk56_0)&~p1(esk56_0))&(~r1(esk56_0,X173)|p1(X173))))))))), 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])])])])])])).
% 1.60/0.72 cnf(c_0_3, negated_conjecture, (r1(X1,esk13_5(X2,X3,X4,X5,X1))|p1(X5)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_4, negated_conjecture, (r1(esk1_0,esk52_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_5, negated_conjecture, (p1(X1)|r1(X2,esk13_5(esk52_0,X3,X4,X1,X2))|~r1(esk52_0,X3)|~r1(X1,X2)|~r1(X4,X1)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_3, c_0_4])).
% 1.60/0.72 cnf(c_0_6, negated_conjecture, (r1(esk52_0,esk53_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_7, negated_conjecture, (p1(X1)|r1(X2,esk13_5(esk52_0,esk53_0,X3,X1,X2))|~r1(esk53_0,X3)|~r1(X1,X2)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_5, c_0_6])).
% 1.60/0.72 cnf(c_0_8, negated_conjecture, (r1(esk53_0,esk54_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_9, negated_conjecture, (r1(X1,esk14_5(X2,X3,X4,X5,X1))|~r1(X5,X1)|~p1(X5)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_10, negated_conjecture, (p1(X1)|r1(X2,esk13_5(esk52_0,esk53_0,esk54_0,X1,X2))|~r1(esk54_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_7, c_0_8])).
% 1.60/0.72 cnf(c_0_11, negated_conjecture, (r1(esk54_0,esk55_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_12, negated_conjecture, (r1(X1,esk6_5(X2,X3,X4,X5,X1))|p1(X7)|~r1(X1,X6)|~r1(X6,X7)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_13, negated_conjecture, (r1(X1,esk14_5(esk52_0,X2,X3,X4,X1))|~p1(X4)|~r1(esk52_0,X2)|~r1(X4,X1)|~r1(X3,X4)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_9, c_0_4])).
% 1.60/0.72 cnf(c_0_14, negated_conjecture, (p1(esk55_0)|r1(X1,esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))|~r1(esk55_0,X1)), inference(spm,[status(thm)],[c_0_10, c_0_11])).
% 1.60/0.72 cnf(c_0_15, negated_conjecture, (r1(esk55_0,esk56_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_16, negated_conjecture, (r1(X1,esk2_6(X2,X3,X4,X5,X6,X1))|p1(X6)|~r1(X6,X1)|~r1(X5,X6)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(esk1_0,X2)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_17, negated_conjecture, (p1(X1)|r1(X2,esk6_5(esk52_0,X3,X4,X5,X2))|~r1(esk52_0,X3)|~r1(X6,X1)|~r1(X5,X2)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X6)), inference(spm,[status(thm)],[c_0_12, c_0_4])).
% 1.60/0.72 cnf(c_0_18, negated_conjecture, (r1(X1,esk14_5(esk52_0,esk53_0,X2,X3,X1))|~p1(X3)|~r1(esk53_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_13, c_0_6])).
% 1.60/0.72 cnf(c_0_19, negated_conjecture, (p1(X1)|~r1(esk56_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_20, negated_conjecture, (p1(esk55_0)|r1(esk56_0,esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))), inference(spm,[status(thm)],[c_0_14, c_0_15])).
% 1.60/0.72 cnf(c_0_21, negated_conjecture, (p1(X1)|r1(X2,esk2_6(esk52_0,X3,X4,X5,X1,X2))|~r1(esk52_0,X3)|~r1(X1,X2)|~r1(X5,X1)|~r1(X4,X5)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_16, c_0_4])).
% 1.60/0.72 cnf(c_0_22, negated_conjecture, (p1(X1)|r1(X2,esk6_5(esk52_0,esk53_0,X3,X4,X2))|~r1(esk53_0,X3)|~r1(X5,X1)|~r1(X4,X2)|~r1(X3,X4)|~r1(X2,X5)), inference(spm,[status(thm)],[c_0_17, c_0_6])).
% 1.60/0.72 cnf(c_0_23, negated_conjecture, (r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,X2,X1))|~p1(X2)|~r1(esk54_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_18, c_0_8])).
% 1.60/0.72 cnf(c_0_24, negated_conjecture, (p1(X4)|~p1(esk13_5(X1,X2,X3,X4,X5))|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_25, negated_conjecture, (p1(esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))|p1(esk55_0)), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 1.60/0.72 cnf(c_0_26, negated_conjecture, (p1(X1)|r1(X2,esk2_6(esk52_0,esk53_0,X3,X4,X1,X2))|~r1(esk53_0,X3)|~r1(X1,X2)|~r1(X4,X1)|~r1(X3,X4)), inference(spm,[status(thm)],[c_0_21, c_0_6])).
% 1.60/0.72 cnf(c_0_27, negated_conjecture, (p1(X1)|r1(X2,esk6_5(esk52_0,esk53_0,esk54_0,X3,X2))|~r1(esk54_0,X3)|~r1(X4,X1)|~r1(X3,X2)|~r1(X2,X4)), inference(spm,[status(thm)],[c_0_22, c_0_8])).
% 1.60/0.72 cnf(c_0_28, negated_conjecture, (r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))|~p1(esk55_0)|~r1(esk55_0,X1)), inference(spm,[status(thm)],[c_0_23, c_0_11])).
% 1.60/0.72 cnf(c_0_29, negated_conjecture, (p1(esk55_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(spm,[status(thm)],[c_0_24, c_0_25]), c_0_4]), c_0_15]), c_0_11]), c_0_8]), c_0_6])])).
% 1.60/0.72 cnf(c_0_30, negated_conjecture, (p1(X1)|r1(X2,esk2_6(esk52_0,esk53_0,esk54_0,X3,X1,X2))|~r1(esk54_0,X3)|~r1(X1,X2)|~r1(X3,X1)), inference(spm,[status(thm)],[c_0_26, c_0_8])).
% 1.60/0.72 cnf(c_0_31, negated_conjecture, (p1(X1)|r1(X2,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,X2))|~r1(esk55_0,X2)|~r1(X3,X1)|~r1(X2,X3)), inference(spm,[status(thm)],[c_0_27, c_0_11])).
% 1.60/0.72 cnf(c_0_32, negated_conjecture, (r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))|~r1(esk55_0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 1.60/0.72 cnf(c_0_33, negated_conjecture, (p1(X1)|r1(X2,esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,X1,X2))|~r1(esk55_0,X1)|~r1(X1,X2)), inference(spm,[status(thm)],[c_0_30, c_0_11])).
% 1.60/0.72 cnf(c_0_34, negated_conjecture, (~p1(esk56_0)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_35, negated_conjecture, (p1(X1)|r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))|~r1(esk56_0,X2)|~r1(X2,X1)), inference(spm,[status(thm)],[c_0_31, c_0_15])).
% 1.60/0.72 cnf(c_0_36, negated_conjecture, (r1(esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))), inference(spm,[status(thm)],[c_0_32, c_0_15])).
% 1.60/0.72 cnf(c_0_37, negated_conjecture, (r1(X1,esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,X1))|~r1(esk56_0,X1)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_33, c_0_15]), c_0_34])).
% 1.60/0.72 cnf(c_0_38, negated_conjecture, (p1(X1)|r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))|~r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),X1)), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 1.60/0.72 cnf(c_0_39, negated_conjecture, (r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)))), inference(spm,[status(thm)],[c_0_37, c_0_36])).
% 1.60/0.72 cnf(c_0_40, negated_conjecture, (p1(X5)|~p1(esk2_6(X1,X2,X3,X4,X5,X6))|~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])).
% 1.60/0.72 cnf(c_0_41, negated_conjecture, (p1(esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)))|r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))), inference(spm,[status(thm)],[c_0_38, c_0_39])).
% 1.60/0.72 cnf(c_0_42, negated_conjecture, (r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_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(spm,[status(thm)],[c_0_40, c_0_41]), c_0_4]), c_0_36]), c_0_15]), c_0_11]), c_0_8]), c_0_6])]), c_0_34])).
% 1.60/0.72 cnf(c_0_43, negated_conjecture, (p1(X7)|~p1(esk6_5(X1,X2,X3,X4,X5))|~r1(X5,X6)|~r1(X6,X7)|~r1(X4,X5)|~r1(X3,X4)|~r1(X2,X3)|~r1(X1,X2)|~r1(esk1_0,X1)), inference(split_conjunct,[status(thm)],[c_0_2])).
% 1.60/0.72 cnf(c_0_44, negated_conjecture, (p1(esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))), inference(spm,[status(thm)],[c_0_19, c_0_42])).
% 1.60/0.72 cnf(c_0_45, negated_conjecture, (p1(X1)|~r1(esk56_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(spm,[status(thm)],[c_0_43, c_0_44]), c_0_4]), c_0_15]), c_0_11]), c_0_8]), c_0_6])])).
% 1.60/0.72 cnf(c_0_46, negated_conjecture, (p1(X1)|~r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),X1)), inference(spm,[status(thm)],[c_0_45, c_0_36])).
% 1.60/0.72 cnf(c_0_47, negated_conjecture, (p1(esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)))), inference(spm,[status(thm)],[c_0_46, c_0_39])).
% 1.60/0.72 cnf(c_0_48, 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(spm,[status(thm)],[c_0_40, c_0_47]), c_0_4]), c_0_36]), c_0_15]), c_0_11]), c_0_8]), c_0_6])]), c_0_34]), ['proof']).
% 1.60/0.72 % SZS output end Proof
% 1.60/0.72 % User time : 0.185 s
% 1.60/0.72 % System time : 0.010 s
% 1.60/0.72 % Total time : 0.195 s
% 1.60/0.72 % User time : 0.187 s
% 1.60/0.72 % System time : 0.012 s
% 1.60/0.72 % Total time : 0.199 s
% 1.60/0.72
%------------------------------------------------------------------------------