%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW443-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:14:15 AM UTC 2026
% Result : Unsatisfiable 20.55s 8.10s
% Output : CNFRefutation 20.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 7
% Syntax : Number of formulae : 102 ( 83 unt; 0 def)
% Number of atoms : 127 ( 59 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 21 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-2 aty)
% Number of variables : 65 ( 21 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(associative_commutative,axiom,
! [VAR_0,VAR_1,VAR_2] : sep(VAR_0,sep(VAR_1,VAR_2)) = sep(VAR_1,sep(VAR_0,VAR_2)),
file('theBenchmark.p',associative_commutative) ).
cnf(c_1,plain,
sep(A,sep(B,C)) = sep(B,sep(A,C)),
inference(clausify,[status(thm)],[associative_commutative]) ).
fof(normalization,axiom,
! [VAR_0,VAR_1] : sep(lseg(VAR_0,VAR_0),VAR_1) = VAR_1,
file('theBenchmark.p',normalization) ).
cnf(c_2,plain,
sep(lseg(A,A),B) = B,
inference(clausify,[status(thm)],[normalization]) ).
fof(wellformedness_5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_0 = VAR_2
| VAR_0 = VAR_1
| ~ heap(sep(lseg(VAR_0,VAR_1),sep(lseg(VAR_0,VAR_2),VAR_3))) ),
file('theBenchmark.p',wellformedness_5) ).
cnf(c_8,plain,
( A = C
| A = B
| ~ heap(sep(lseg(A,B),sep(lseg(A,C),D))) ),
inference(clausify,[status(thm)],[wellformedness_5]) ).
fof(premise_8,axiom,
x2 != x8,
file('theBenchmark.p',premise_8) ).
cnf(c_24,plain,
x2 != x8,
inference(clausify,[status(thm)],[premise_8]) ).
cnf(c_25,plain,
x8 != x2,
inference(copy,[status(thm)],[c_24]) ).
fof(premise_9,axiom,
x2 != x13,
file('theBenchmark.p',premise_9) ).
cnf(c_26,plain,
x2 != x13,
inference(clausify,[status(thm)],[premise_9]) ).
cnf(c_27,plain,
x13 != x2,
inference(copy,[status(thm)],[c_26]) ).
fof(premise_19,axiom,
x1 != x14,
file('theBenchmark.p',premise_19) ).
cnf(c_42,plain,
x1 != x14,
inference(clausify,[status(thm)],[premise_19]) ).
cnf(c_43,plain,
x14 != x1,
inference(copy,[status(thm)],[c_42]) ).
fof(premise_23,axiom,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp)))))))))))))),
file('theBenchmark.p',premise_23) ).
cnf(c_50,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp)))))))))))))),
inference(clausify,[status(thm)],[premise_23]) ).
cnf(c_6035,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x7),sep(lseg(x11,x9),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_50]) ).
cnf(c_6036,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x11,x7),sep(lseg(x7,x5),sep(lseg(x11,x9),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6035]) ).
cnf(c_6037,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6036]) ).
cnf(c_6038,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x9,x5),sep(lseg(x11,x9),sep(lseg(x7,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6037]) ).
cnf(c_6039,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x9,x5),sep(lseg(x7,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6038]) ).
cnf(c_6040,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6039]) ).
cnf(c_6041,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x12,x13),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6040]) ).
cnf(c_6042,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x12,x13),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6041]) ).
cnf(c_6043,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6042]) ).
cnf(c_6044,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x12,x13),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6043]) ).
cnf(c_6045,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x12,x13),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6044]) ).
cnf(c_6046,plain,
heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6045]) ).
cnf(c_6047,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6046]) ).
cnf(c_6048,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6047]) ).
cnf(c_6049,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6048]) ).
cnf(c_6050,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6049]) ).
cnf(c_6051,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6050]) ).
cnf(c_6052,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x18,x15),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6051]) ).
cnf(c_6053,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6052]) ).
cnf(c_6054,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6053]) ).
cnf(c_6055,plain,
heap(sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6054]) ).
cnf(c_6056,plain,
heap(sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6055]) ).
cnf(c_6057,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6056]) ).
cnf(c_6058,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x10,x1),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6057]) ).
cnf(c_6059,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x10,x1),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6058]) ).
cnf(c_6060,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x10,x1),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6059]) ).
cnf(c_6061,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x10,x1),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6060]) ).
cnf(c_6062,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x10,x1),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6061]) ).
cnf(c_6063,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6062]) ).
cnf(c_6064,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6063]) ).
cnf(c_6065,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x10,x1),sep(lseg(x7,x5),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6064]) ).
cnf(c_6066,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6065]) ).
cnf(c_51,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),sep(lseg(x10,x1),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6066]) ).
cnf(c_53,plain,
sep(A,sep(B,sep(C,D))) = sep(C,sep(A,sep(B,D))),
inference(paramod,[status(thm)],[c_1,c_1]) ).
cnf(c_6067,plain,
x2 != x8,
inference(copy,[status(thm)],[c_25]) ).
cnf(c_6068,plain,
( x2 = A
| ~ heap(sep(lseg(x2,x8),sep(lseg(x2,A),B))) ),
inference(resolve,[status(thm)],[c_8,c_6067]) ).
cnf(c_6069,plain,
x2 != x13,
inference(copy,[status(thm)],[c_27]) ).
cnf(c_6070,plain,
~ heap(sep(lseg(x2,x8),sep(lseg(x2,x13),A))),
inference(resolve,[status(thm)],[c_6068,c_6069]) ).
cnf(c_114,plain,
~ heap(sep(lseg(x2,x13),sep(lseg(x2,x8),A))),
inference(paramod,[status(thm)],[c_1,c_6070]) ).
cnf(c_6071,plain,
( x1 = x3
| x1 = x14 ),
inference(resolve,[status(thm)],[c_51,c_8]) ).
cnf(c_6072,plain,
( x1 = x3
| x14 = x1 ),
inference(copy,[status(thm)],[c_6071]) ).
cnf(c_6073,plain,
( x3 = x1
| x14 = x1 ),
inference(copy,[status(thm)],[c_6072]) ).
cnf(c_207,plain,
x3 = x1,
inference(resolve,[status(thm)],[c_43,c_6073]) ).
cnf(c_6074,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_51]) ).
cnf(c_6075,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x1),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp)))))))))))))),
inference(paramod,[status(thm)],[c_207,c_6074]) ).
cnf(c_6076,plain,
heap(sep(lseg(x1,x14),sep(lseg(x1,x1),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),sep(lseg(x10,x1),emp)))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6075]) ).
cnf(c_208,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x9,x5),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_2,c_6076]) ).
cnf(c_224,plain,
sep(A,sep(B,sep(C,sep(D,E)))) = sep(C,sep(A,sep(D,sep(B,E)))),
inference(paramod,[status(thm)],[c_53,c_1]) ).
cnf(c_235,plain,
( B = D
| B = C
| ~ heap(sep(A,sep(lseg(B,C),sep(lseg(B,D),E)))) ),
inference(paramod,[status(thm)],[c_53,c_8]) ).
cnf(c_262,plain,
sep(A,sep(B,sep(C,sep(D,E)))) = sep(C,sep(D,sep(A,sep(B,E)))),
inference(paramod,[status(thm)],[c_53,c_53]) ).
cnf(c_1135,plain,
( B = F
| B = C
| ~ heap(sep(A,sep(lseg(B,C),sep(D,sep(E,sep(lseg(B,F),V6)))))) ),
inference(paramod,[status(thm)],[c_53,c_235]) ).
cnf(c_1209,plain,
( C = F
| C = D
| ~ heap(sep(A,sep(B,sep(lseg(C,D),sep(E,sep(lseg(C,F),V6)))))) ),
inference(paramod,[status(thm)],[c_224,c_235]) ).
cnf(c_1479,plain,
( D = F
| D = E
| ~ heap(sep(A,sep(B,sep(C,sep(lseg(D,E),sep(lseg(D,F),V6)))))) ),
inference(paramod,[status(thm)],[c_262,c_235]) ).
cnf(c_1795,plain,
~ heap(sep(A,sep(lseg(x2,x13),sep(B,sep(lseg(x2,x8),C))))),
inference(paramod,[status(thm)],[c_224,c_114]) ).
cnf(c_6077,plain,
( x2 = x8
| x2 = x18 ),
inference(resolve,[status(thm)],[c_208,c_1479]) ).
cnf(c_6078,plain,
( x2 = x8
| x18 = x2 ),
inference(copy,[status(thm)],[c_6077]) ).
cnf(c_6079,plain,
( x8 = x2
| x18 = x2 ),
inference(copy,[status(thm)],[c_6078]) ).
cnf(c_6031,plain,
x18 = x2,
inference(resolve,[status(thm)],[c_25,c_6079]) ).
cnf(c_6080,plain,
( x2 = x8
| x2 = x12 ),
inference(resolve,[status(thm)],[c_208,c_1209]) ).
cnf(c_6081,plain,
( x2 = x8
| x12 = x2 ),
inference(copy,[status(thm)],[c_6080]) ).
cnf(c_6082,plain,
( x8 = x2
| x12 = x2 ),
inference(copy,[status(thm)],[c_6081]) ).
cnf(c_6032,plain,
x12 = x2,
inference(resolve,[status(thm)],[c_25,c_6082]) ).
cnf(c_6083,plain,
( x2 = x8
| x2 = x5 ),
inference(resolve,[status(thm)],[c_208,c_1135]) ).
cnf(c_6084,plain,
( x2 = x8
| x5 = x2 ),
inference(copy,[status(thm)],[c_6083]) ).
cnf(c_6085,plain,
( x8 = x2
| x5 = x2 ),
inference(copy,[status(thm)],[c_6084]) ).
cnf(c_6033,plain,
x5 = x2,
inference(resolve,[status(thm)],[c_25,c_6085]) ).
cnf(c_6086,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_208]) ).
cnf(c_6087,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6033,c_6086]) ).
cnf(c_6088,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6032,c_6087]) ).
cnf(c_6089,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6031,c_6088]) ).
cnf(c_6090,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x2,x13),sep(lseg(x18,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6032,c_6089]) ).
cnf(c_6091,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x7,x5),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6031,c_6090]) ).
cnf(c_6092,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x7,x2),sep(lseg(x10,x1),sep(lseg(x9,x5),emp))))))))))))),
inference(paramod,[status(thm)],[c_6033,c_6091]) ).
cnf(c_6093,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x7,x2),sep(lseg(x10,x1),sep(lseg(x9,x2),emp))))))))))))),
inference(paramod,[status(thm)],[c_6033,c_6092]) ).
cnf(c_6094,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6093]) ).
cnf(c_6095,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x2,x13),sep(lseg(x11,x9),sep(lseg(x2,x15),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6094]) ).
cnf(c_6096,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6095]) ).
cnf(c_6097,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x2,x13),sep(lseg(x11,x7),sep(lseg(x2,x15),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6096]) ).
cnf(c_6098,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x8),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6097]) ).
cnf(c_6099,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x13),sep(lseg(x2,x8),sep(lseg(x2,x15),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6098]) ).
cnf(c_6100,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))))),
inference(paramod,[status(thm)],[c_1,c_6099]) ).
cnf(c_6101,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x2),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp)))))))))))),
inference(paramod,[status(thm)],[c_2,c_6100]) ).
cnf(c_6102,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x2),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp))))))))))),
inference(paramod,[status(thm)],[c_2,c_6101]) ).
cnf(c_6103,plain,
heap(sep(lseg(x1,x14),sep(lseg(x2,x13),sep(lseg(x2,x15),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x7,x2),sep(lseg(x9,x2),sep(lseg(x10,x1),emp)))))))))),
inference(paramod,[status(thm)],[c_2,c_6102]) ).
cnf(c_6034,plain,
$false,
inference(resolve,[status(thm)],[c_1795,c_6103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW443-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.36 % Computer : n014.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sat Sep 26 15:53:07 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.37 % Process 3541691 was started by sandbox2 on n014,
% 0.09/5.37 % Sat Sep 26 15:53:07 2026
% 0.09/5.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/5.37
% 0.09/5.37 % From the command line: assign(max_seconds, 300).
% 20.55/8.10
% 20.55/8.10 % SZS status Unsatisfiable for theBenchmark
% 20.55/8.10
% 20.55/8.10 % Proof 1 at 2.21 (+ 0.50) seconds.
% 20.55/8.10 % Length of proof is 26.
% 20.55/8.10 % Level of proof is 5.
% 20.55/8.10 % Maximum clause weight is 54.000.
% 20.55/8.10 % Given clauses 288.
% 20.55/8.10
% 20.55/8.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------