%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW445-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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 : Fri Sep 25 03:27:07 PM UTC 2026
% Result : Unsatisfiable 123.56s 16.27s
% Output : Proof 123.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 117
% Number of leaves : 28
% Syntax : Number of formulae : 246 ( 242 unt; 0 def)
% Number of atoms : 254 ( 238 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 94 ( 86 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 24 con; 0-4 aty)
% Number of variables : 178 ( 60 sgn 30 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f6,axiom,
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_5) ).
fof(f6_nnf,plain,
! [X,Y,Z,Sigma] :
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z,Sigma] :
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( X0 = X2
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3))) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t52,plain,
ifeq(heap(sep(lseg(X1,X2),sep(lseg(X1,X3),X4))),true,or(eq(X1,X2),eq(X1,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t78,plain,
ifeq(heap(sep(lseg(X1,X2),sep(lseg(X1,X3),X4))),true,or(eq(X1,X2),eq(X1,X3)),true) = true,
inference(orient,[status(thm)],[t52]) ).
cnf(f0,axiom,
sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_commutative) ).
fof(f0_nnf,plain,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t45,plain,
sep(X1,sep(X2,X3)) = sep(X2,sep(X1,X3)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t113,plain,
sep(X1,sep(X2,X3)) = sep(X2,sep(X1,X3)),
inference(orient,[status(thm)],[t45]) ).
cnf(t121,plain,
true = ifeq(heap(sep(lseg(X1,X2),sep(lseg(X1,X3),X4))),true,or(eq(X1,X3),eq(X1,X2)),true),
inference(cp,[status(thm)],[t78,t113]) ).
cnf(t1270,plain,
ifeq(heap(sep(lseg(X1,X2),sep(lseg(X1,X3),X4))),true,or(eq(X1,X3),eq(X1,X2)),true) = true,
inference(orient,[status(thm)],[t121]) ).
cnf(t1271,plain,
true = ifeq(heap(sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5)))),true,or(eq(X1,X4),eq(X1,X2)),true),
inference(cp,[status(thm)],[t1270,t113]) ).
cnf(t18336,plain,
true = ifeq(heap(sep(X3,sep(lseg(X1,X2),sep(lseg(X1,X4),X5)))),true,or(eq(X1,X4),eq(X1,X2)),true),
inference(step,[status(thm)],[t1271,t113]) ).
cnf(t1726,plain,
ifeq(heap(sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))),true,or(eq(X2,X4),eq(X2,X3)),true) = true,
inference(orient,[status(thm)],[t18336]) ).
cnf(t1728,plain,
true = ifeq(heap(sep(X1,sep(lseg(X2,X3),sep(X4,sep(lseg(X2,X5),Y5))))),true,or(eq(X2,X5),eq(X2,X3)),true),
inference(cp,[status(thm)],[t1726,t113]) ).
cnf(t18502,plain,
true = ifeq(heap(sep(X1,sep(X4,sep(lseg(X2,X3),sep(lseg(X2,X5),Y5))))),true,or(eq(X2,X5),eq(X2,X3)),true),
inference(step,[status(thm)],[t1728,t113]) ).
cnf(t2753,plain,
ifeq(heap(sep(X1,sep(X2,sep(lseg(X3,X4),sep(lseg(X3,X5),Y5))))),true,or(eq(X3,X5),eq(X3,X4)),true) = true,
inference(orient,[status(thm)],[t18502]) ).
cnf(t2755,plain,
true = ifeq(heap(sep(X1,sep(X2,sep(lseg(X3,X4),sep(X5,sep(lseg(X3,Y5),Y6)))))),true,or(eq(X3,Y5),eq(X3,X4)),true),
inference(cp,[status(thm)],[t2753,t113]) ).
cnf(t18554,plain,
true = ifeq(heap(sep(X1,sep(X2,sep(X5,sep(lseg(X3,X4),sep(lseg(X3,Y5),Y6)))))),true,or(eq(X3,Y5),eq(X3,X4)),true),
inference(step,[status(thm)],[t2755,t113]) ).
cnf(t3244,plain,
ifeq(heap(sep(X1,sep(X2,sep(X3,sep(lseg(X4,X5),sep(lseg(X4,Y5),Y6)))))),true,or(eq(X4,Y5),eq(X4,X5)),true) = true,
inference(orient,[status(thm)],[t18554]) ).
cnf(t3246,plain,
true = ifeq(heap(sep(X1,sep(X2,sep(X3,sep(lseg(X4,X5),sep(Y5,sep(lseg(X4,Y6),Y7))))))),true,or(eq(X4,Y6),eq(X4,X5)),true),
inference(cp,[status(thm)],[t3244,t113]) ).
cnf(t18985,plain,
true = ifeq(heap(sep(X1,sep(X2,sep(X3,sep(Y5,sep(lseg(X4,X5),sep(lseg(X4,Y6),Y7))))))),true,or(eq(X4,Y6),eq(X4,X5)),true),
inference(step,[status(thm)],[t3246,t113]) ).
cnf(t5408,plain,
ifeq(heap(sep(X1,sep(X2,sep(X3,sep(X4,sep(lseg(X5,Y5),sep(lseg(X5,Y6),Y7))))))),true,or(eq(X5,Y6),eq(X5,Y5)),true) = true,
inference(orient,[status(thm)],[t18985]) ).
cnf(f29,hypothesis,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_19) ).
fof(f29_nnf,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(t56,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t109,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(orient,[status(thm)],[t56]) ).
cnf(t133,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(rw,[status(thm)],[t109]) ).
cnf(t18612,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t133,t113]) ).
cnf(t18613,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x2,x18),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18612,t113]) ).
cnf(t18614,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x2,x18),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18613,t113]) ).
cnf(t18615,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18614,t113]) ).
cnf(t18616,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18615,t113]) ).
cnf(t18617,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x12,x11),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18616,t113]) ).
cnf(t18618,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x17,x14),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18617,t113]) ).
cnf(t18619,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18618,t113]) ).
cnf(t18620,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18619,t113]) ).
cnf(t18621,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x7,x16),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18620,t113]) ).
cnf(t18622,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18621,t113]) ).
cnf(t18623,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18622,t113]) ).
cnf(t18624,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x7,x16),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18623,t113]) ).
cnf(t18625,plain,
heap(sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18624,t113]) ).
cnf(t18626,plain,
heap(sep(lseg(x5,x17),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18625,t113]) ).
cnf(t18627,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18626,t113]) ).
cnf(t18628,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18627,t113]) ).
cnf(t18629,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x3,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18628,t113]) ).
cnf(t18630,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x3,x20),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18629,t113]) ).
cnf(t18631,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18630,t113]) ).
cnf(t18632,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x3,x20),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18631,t113]) ).
cnf(t18633,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18632,t113]) ).
cnf(t18634,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18633,t113]) ).
cnf(t18635,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x3,x12),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18634,t113]) ).
cnf(t18636,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x3,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18635,t113]) ).
cnf(t18637,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x3,x12),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18636,t113]) ).
cnf(t18638,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x3,x12),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18637,t113]) ).
cnf(t18639,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18638,t113]) ).
cnf(t18640,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x6,x17),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18639,t113]) ).
cnf(t18641,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18640,t113]) ).
cnf(t18642,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x6,x17),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18641,t113]) ).
cnf(t18643,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x6,x17),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18642,t113]) ).
cnf(t18644,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x6,x17),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18643,t113]) ).
cnf(t18645,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18644,t113]) ).
cnf(t18646,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x17),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18645,t113]) ).
cnf(t18647,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x6,x17),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18646,t113]) ).
cnf(t18648,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x6,x17),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18647,t113]) ).
cnf(t18649,plain,
heap(sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x6,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18648,t113]) ).
cnf(t18650,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x6,x19),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18649,t113]) ).
cnf(t18651,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x6,x19),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18650,t113]) ).
cnf(t18652,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x6,x19),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18651,t113]) ).
cnf(t18653,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x6,x19),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18652,t113]) ).
cnf(t18654,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x6,x19),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18653,t113]) ).
cnf(t18655,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x6,x19),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18654,t113]) ).
cnf(t18656,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18655,t113]) ).
cnf(t18657,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x19),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18656,t113]) ).
cnf(t18658,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x6,x19),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18657,t113]) ).
cnf(t18659,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x6,x19),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18658,t113]) ).
cnf(t18660,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x6,x19),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18659,t113]) ).
cnf(t18661,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x6,x19),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18660,t113]) ).
cnf(t18662,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t18661,t113]) ).
cnf(t3777,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(orient,[status(thm)],[t18662]) ).
cnf(t3919,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(rw,[status(thm)],[t3777]) ).
cnf(t44,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t59,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t44]) ).
cnf(t3811,plain,
true = ifeq(true,true,or(eq(x6,x17),eq(x6,x19)),true),
inference(cp,[status(thm)],[t1726,t3777]) ).
cnf(t23,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t58,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t23]) ).
cnf(t18663,plain,
true = or(eq(x6,x17),eq(x6,x19)),
inference(step,[status(thm)],[t3811,t58]) ).
cnf(f11,hypothesis,
x6 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_1) ).
fof(f11_nnf,plain,
x6 != x19,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
x6 != x19,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
x6 != x19,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t14,plain,
eq(x6,x19) = false,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t200,plain,
eq(x6,x19) = false,
inference(orient,[status(thm)],[t14]) ).
cnf(t18664,plain,
true = or(eq(x6,x17),false),
inference(step,[status(thm)],[t18663,t200]) ).
cnf(t19,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t62,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t19]) ).
cnf(t18665,plain,
true = eq(x6,x17),
inference(step,[status(thm)],[t18664,t62]) ).
cnf(t3853,plain,
eq(x6,x17) = true,
inference(orient,[status(thm)],[t18665]) ).
cnf(t3854,plain,
x17 = ifeq(true,true,x6,x17),
inference(cp,[status(thm)],[t59,t3853]) ).
cnf(t18666,plain,
x17 = x6,
inference(step,[status(thm)],[t3854,t58]) ).
cnf(t3855,plain,
x17 = x6,
inference(orient,[status(thm)],[t18666]) ).
cnf(t19267,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))))) = true,
inference(step,[status(thm)],[t3919,t3855]) ).
cnf(f1,axiom,
sep(lseg(X,X),Sigma) = Sigma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',normalization) ).
fof(f1_nnf,plain,
! [X,Sigma] : sep(lseg(X,X),Sigma) = Sigma,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Sigma] : sep(lseg(X,X),Sigma) = Sigma,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
sep(lseg(X0,X0),X1) = X1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t42,plain,
sep(lseg(X1,X1),X2) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t57,plain,
sep(lseg(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t42]) ).
cnf(t19268,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19267,t57]) ).
cnf(t19269,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19268,t3855]) ).
cnf(t19270,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x6,x14),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19269,t3855]) ).
cnf(t19271,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x6,x14),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19270,t113]) ).
cnf(t19272,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x14),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19271,t113]) ).
cnf(t19273,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x6,x14),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19272,t113]) ).
cnf(t19274,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x6,x14),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19273,t113]) ).
cnf(t19275,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x6,x14),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19274,t113]) ).
cnf(t19276,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x14),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t19275,t113]) ).
cnf(t7642,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x14),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(orient,[status(thm)],[t19276]) ).
cnf(t7757,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x14),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(rw,[status(thm)],[t7642]) ).
cnf(t7680,plain,
true = ifeq(true,true,or(eq(x6,x14),eq(x6,x19)),true),
inference(cp,[status(thm)],[t1726,t7642]) ).
cnf(t19277,plain,
true = or(eq(x6,x14),eq(x6,x19)),
inference(step,[status(thm)],[t7680,t58]) ).
cnf(t19278,plain,
true = or(eq(x6,x14),false),
inference(step,[status(thm)],[t19277,t200]) ).
cnf(t19279,plain,
true = eq(x6,x14),
inference(step,[status(thm)],[t19278,t62]) ).
cnf(t7754,plain,
eq(x6,x14) = true,
inference(orient,[status(thm)],[t19279]) ).
cnf(t7755,plain,
x14 = ifeq(true,true,x6,x14),
inference(cp,[status(thm)],[t59,t7754]) ).
cnf(t19280,plain,
x14 = x6,
inference(step,[status(thm)],[t7755,t58]) ).
cnf(t7756,plain,
x14 = x6,
inference(orient,[status(thm)],[t19280]) ).
cnf(t19782,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))))) = true,
inference(step,[status(thm)],[t7757,t7756]) ).
cnf(t19783,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))) = true,
inference(step,[status(thm)],[t19782,t57]) ).
cnf(t12914,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))) = true,
inference(orient,[status(thm)],[t19783]) ).
cnf(t13084,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))) = true,
inference(rw,[status(thm)],[t12914]) ).
cnf(t13058,plain,
true = ifeq(true,true,or(eq(x3,x12),eq(x3,x20)),true),
inference(cp,[status(thm)],[t5408,t12914]) ).
cnf(t19784,plain,
true = or(eq(x3,x12),eq(x3,x20)),
inference(step,[status(thm)],[t13058,t58]) ).
cnf(f13,hypothesis,
x3 != x20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_3) ).
fof(f13_nnf,plain,
x3 != x20,
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
x3 != x20,
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
x3 != x20,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t9,plain,
eq(x3,x20) = false,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t164,plain,
eq(x3,x20) = false,
inference(orient,[status(thm)],[t9]) ).
cnf(t19785,plain,
true = or(eq(x3,x12),false),
inference(step,[status(thm)],[t19784,t164]) ).
cnf(t19786,plain,
true = eq(x3,x12),
inference(step,[status(thm)],[t19785,t62]) ).
cnf(t13081,plain,
eq(x3,x12) = true,
inference(orient,[status(thm)],[t19786]) ).
cnf(t13082,plain,
x12 = ifeq(true,true,x3,x12),
inference(cp,[status(thm)],[t59,t13081]) ).
cnf(t19787,plain,
x12 = x3,
inference(step,[status(thm)],[t13082,t58]) ).
cnf(t13083,plain,
x12 = x3,
inference(orient,[status(thm)],[t19787]) ).
cnf(t20225,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))) = true,
inference(step,[status(thm)],[t13084,t13083]) ).
cnf(t20226,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x3),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp))))))))))))) = true,
inference(step,[status(thm)],[t20225,t13083]) ).
cnf(t20227,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20226,t57]) ).
cnf(t20228,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20227,t13083]) ).
cnf(t20229,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x3,x20),sep(lseg(x19,x1),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20228,t113]) ).
cnf(t20230,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20229,t113]) ).
cnf(t20231,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x3,x15),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20230,t13083]) ).
cnf(t20232,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x3,x15),sep(lseg(x19,x1),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20231,t113]) ).
cnf(t20233,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x12,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20232,t113]) ).
cnf(t20234,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x3,x11),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20233,t13083]) ).
cnf(t20235,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x2,x18),sep(lseg(x3,x11),sep(lseg(x19,x1),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20234,t113]) ).
cnf(t20236,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x3,x11),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x11,x12),emp)))))))))))) = true,
inference(step,[status(thm)],[t20235,t113]) ).
cnf(t20237,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x3,x11),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x11,x3),emp)))))))))))) = true,
inference(step,[status(thm)],[t20236,t13083]) ).
cnf(t17740,plain,
heap(sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x5,x6),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x3,x11),sep(lseg(x2,x18),sep(lseg(x19,x1),sep(lseg(x11,x3),emp)))))))))))) = true,
inference(orient,[status(thm)],[t20237]) ).
cnf(t17892,plain,
true = ifeq(true,true,or(eq(x3,x20),eq(x3,x20)),true),
inference(cp,[status(thm)],[t5408,t17740]) ).
cnf(t20238,plain,
true = or(eq(x3,x20),eq(x3,x20)),
inference(step,[status(thm)],[t17892,t58]) ).
cnf(t20239,plain,
true = or(false,eq(x3,x20)),
inference(step,[status(thm)],[t20238,t164]) ).
cnf(t21,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t63,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t20240,plain,
true = eq(x3,x20),
inference(step,[status(thm)],[t20239,t63]) ).
cnf(t20241,plain,
true = false,
inference(step,[status(thm)],[t20240,t164]) ).
cnf(t17945,plain,
false = true,
inference(orient,[status(thm)],[t20241]) ).
cnf(f2,axiom,
~ heap(sep(next(nil,Y),Sigma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_1) ).
fof(f2_nnf,plain,
! [Y,Sigma] : ~ heap(sep(next(nil,Y),Sigma)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Y,Sigma] : ~ heap(sep(next(nil,Y),Sigma)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
~ heap(sep(next(nil,X0),X1)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f4,axiom,
~ heap(sep(next(X,Y),sep(next(X,Z),Sigma))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_3) ).
fof(f4_nnf,plain,
! [X,Y,Z,Sigma] : ~ heap(sep(next(X,Y),sep(next(X,Z),Sigma))),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y,Z,Sigma] : ~ heap(sep(next(X,Y),sep(next(X,Z),Sigma))),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ heap(sep(next(X0,X1),sep(next(X0,X2),X3))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(f12,hypothesis,
x3 != x7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_2) ).
fof(f12_nnf,plain,
x3 != x7,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
x3 != x7,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
x3 != x7,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(f14,hypothesis,
x7 != x20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_4) ).
fof(f14_nnf,plain,
x7 != x20,
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
x7 != x20,
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
x7 != x20,
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,hypothesis,
x9 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_5) ).
fof(f15_nnf,plain,
x9 != x19,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
x9 != x19,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
x9 != x19,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f16,hypothesis,
x2 != x20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_6) ).
fof(f16_nnf,plain,
x2 != x20,
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
x2 != x20,
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
x2 != x20,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f17,hypothesis,
x8 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_7) ).
fof(f17_nnf,plain,
x8 != x19,
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
x8 != x19,
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
x8 != x19,
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(f18,hypothesis,
x8 != x17,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_8) ).
fof(f18_nnf,plain,
x8 != x17,
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
x8 != x17,
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
x8 != x17,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(f19,hypothesis,
x4 != x11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_9) ).
fof(f19_nnf,plain,
x4 != x11,
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
x4 != x11,
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
x4 != x11,
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(f20,hypothesis,
x4 != x13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_10) ).
fof(f20_nnf,plain,
x4 != x13,
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
x4 != x13,
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
x4 != x13,
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(f21,hypothesis,
x4 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_11) ).
fof(f21_nnf,plain,
x4 != x19,
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
x4 != x19,
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
x4 != x19,
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(f22,hypothesis,
x1 != x16,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_12) ).
fof(f22_nnf,plain,
x1 != x16,
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
x1 != x16,
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
x1 != x16,
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(f23,hypothesis,
x1 != x20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_13) ).
fof(f23_nnf,plain,
x1 != x20,
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
x1 != x20,
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
x1 != x20,
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(f24,hypothesis,
x13 != x18,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_14) ).
fof(f24_nnf,plain,
x13 != x18,
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
x13 != x18,
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
x13 != x18,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(f25,hypothesis,
x13 != x17,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_15) ).
fof(f25_nnf,plain,
x13 != x17,
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
x13 != x17,
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
x13 != x17,
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(f26,hypothesis,
x10 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_16) ).
fof(f26_nnf,plain,
x10 != x19,
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
x10 != x19,
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
x10 != x19,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(f27,hypothesis,
x10 != x20,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_17) ).
fof(f27_nnf,plain,
x10 != x20,
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
x10 != x20,
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
x10 != x20,
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(f28,hypothesis,
x16 != x19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_18) ).
fof(f28_nnf,plain,
x16 != x19,
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
x16 != x19,
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
x16 != x19,
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c4,c11,c12,c13,c14,c15,c16,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,c27,c28]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t17945]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW445-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.56 % Computer : n020.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.57 % CPULimit : 300
% 0.08/0.57 % WCLimit : 300
% 0.08/0.57 % DateTime : Thu Sep 24 22:25:04 UTC 2026
% 0.08/0.57 % CPUTime :
% 0.08/0.57 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 123.56/16.27 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 123.56/16.27 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------