%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW437-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 : n002.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:14 AM UTC 2026
% Result : Unsatisfiable 46.76s 17.41s
% Output : CNFRefutation 46.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 6
% Syntax : Number of formulae : 72 ( 63 unt; 0 def)
% Number of atoms : 83 ( 31 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 23 ( 12 ~; 11 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 21 ( 3 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_6,axiom,
x3 != x8,
file('theBenchmark.p',premise_6) ).
cnf(c_20,plain,
x3 != x8,
inference(clausify,[status(thm)],[premise_6]) ).
cnf(c_21,plain,
x8 != x3,
inference(copy,[status(thm)],[c_20]) ).
fof(premise_10,axiom,
x7 != x16,
file('theBenchmark.p',premise_10) ).
cnf(c_28,plain,
x7 != x16,
inference(clausify,[status(thm)],[premise_10]) ).
fof(premise_27,axiom,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
file('theBenchmark.p',premise_27) ).
cnf(c_55,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(clausify,[status(thm)],[premise_27]) ).
cnf(c_10207,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_55]) ).
cnf(c_10208,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x3,x16),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10207]) ).
cnf(c_10209,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10208]) ).
cnf(c_10210,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x3,x16),sep(lseg(x10,x5),sep(lseg(x3,x12),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10209]) ).
cnf(c_10211,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10210]) ).
cnf(c_10212,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x3,x16),sep(lseg(x10,x15),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10211]) ).
cnf(c_10213,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10212]) ).
cnf(c_10214,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10213]) ).
cnf(c_10215,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10214]) ).
cnf(c_10216,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10215]) ).
cnf(c_10217,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x2,x6),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10216]) ).
cnf(c_10218,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x2,x6),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10217]) ).
cnf(c_10219,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x2,x6),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10218]) ).
cnf(c_10220,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10219]) ).
cnf(c_10221,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x2,x6),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10220]) ).
cnf(c_10222,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10221]) ).
cnf(c_10223,plain,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10222]) ).
cnf(c_10224,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x12,x8),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10223]) ).
cnf(c_10225,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x12,x8),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10224]) ).
cnf(c_10226,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x12,x8),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10225]) ).
cnf(c_10227,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x12,x8),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10226]) ).
cnf(c_10228,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x10,x15),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10227]) ).
cnf(c_10229,plain,
heap(sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10228]) ).
cnf(c_10230,plain,
heap(sep(lseg(x16,x3),sep(lseg(x5,x1),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10229]) ).
cnf(c_10231,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x5,x1),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10230]) ).
cnf(c_10232,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10231]) ).
cnf(c_10233,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10232]) ).
cnf(c_10234,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x5,x1),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10233]) ).
cnf(c_10235,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10234]) ).
cnf(c_56,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10235]) ).
cnf(c_10236,plain,
( x16 = x7
| x16 = x3 ),
inference(resolve,[status(thm)],[c_56,c_8]) ).
cnf(c_10237,plain,
( x16 = x7
| x3 = x16 ),
inference(copy,[status(thm)],[c_10236]) ).
cnf(c_10238,plain,
( x7 = x16
| x3 = x16 ),
inference(copy,[status(thm)],[c_10237]) ).
cnf(c_252,plain,
x3 = x16,
inference(resolve,[status(thm)],[c_28,c_10238]) ).
cnf(c_10239,plain,
heap(sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_56]) ).
cnf(c_10240,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x3,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_252,c_10239]) ).
cnf(c_10241,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x16,x16),sep(lseg(x3,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_252,c_10240]) ).
cnf(c_10242,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x16,x16),sep(lseg(x16,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))))),
inference(paramod,[status(thm)],[c_252,c_10241]) ).
cnf(c_10243,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x16,x16),sep(lseg(x16,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))))),
inference(paramod,[status(thm)],[c_1,c_10242]) ).
cnf(c_10244,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x16,x12),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp))))))))))),
inference(paramod,[status(thm)],[c_2,c_10243]) ).
cnf(c_10245,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp))))))))))),
inference(paramod,[status(thm)],[c_1,c_10244]) ).
cnf(c_253,plain,
heap(sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))),
inference(paramod,[status(thm)],[c_2,c_10245]) ).
cnf(c_280,plain,
x8 != x16,
inference(paramod,[status(thm)],[c_252,c_21]) ).
cnf(c_10246,plain,
x16 != x7,
inference(copy,[status(thm)],[c_28]) ).
cnf(c_10247,plain,
( x16 = A
| ~ heap(sep(lseg(x16,x7),sep(lseg(x16,A),B))) ),
inference(resolve,[status(thm)],[c_8,c_10246]) ).
cnf(c_10248,plain,
x16 != x8,
inference(copy,[status(thm)],[c_280]) ).
cnf(c_332,plain,
~ heap(sep(lseg(x16,x7),sep(lseg(x16,x8),A))),
inference(resolve,[status(thm)],[c_10247,c_10248]) ).
cnf(c_10249,plain,
( x16 = x7
| x16 = x12 ),
inference(resolve,[status(thm)],[c_253,c_8]) ).
cnf(c_10250,plain,
( x16 = x7
| x12 = x16 ),
inference(copy,[status(thm)],[c_10249]) ).
cnf(c_10251,plain,
( x7 = x16
| x12 = x16 ),
inference(copy,[status(thm)],[c_10250]) ).
cnf(c_10205,plain,
x12 = x16,
inference(resolve,[status(thm)],[c_28,c_10251]) ).
cnf(c_10252,plain,
heap(sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))),
inference(paramod,[status(thm)],[c_1,c_253]) ).
cnf(c_10253,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))),
inference(paramod,[status(thm)],[c_10205,c_10252]) ).
cnf(c_10254,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x16,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x2,x6),sep(lseg(x11,x8),emp)))))))))),
inference(paramod,[status(thm)],[c_10205,c_10253]) ).
cnf(c_10255,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x16,x8),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))),
inference(paramod,[status(thm)],[c_1,c_10254]) ).
cnf(c_10256,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x16,x8),sep(lseg(x10,x15),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))),
inference(paramod,[status(thm)],[c_1,c_10255]) ).
cnf(c_10257,plain,
heap(sep(lseg(x16,x16),sep(lseg(x16,x7),sep(lseg(x16,x8),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp)))))))))),
inference(paramod,[status(thm)],[c_1,c_10256]) ).
cnf(c_10258,plain,
heap(sep(lseg(x16,x7),sep(lseg(x16,x8),sep(lseg(x10,x5),sep(lseg(x10,x15),sep(lseg(x5,x1),sep(lseg(x7,x1),sep(lseg(x11,x8),sep(lseg(x2,x6),emp))))))))),
inference(paramod,[status(thm)],[c_2,c_10257]) ).
cnf(c_10206,plain,
$false,
inference(resolve,[status(thm)],[c_332,c_10258]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW437-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/10.53 % Computer : n002.cluster.edu
% 0.09/10.53 % Model : x86_64 x86_64
% 0.09/10.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.53 % Memory : 8046.5625MB
% 0.09/10.53 % OS : Linux 6.8.0-71-generic
% 0.09/10.53 % CPULimit : 300
% 0.09/10.53 % WCLimit : 300
% 0.09/10.53 % DateTime : Sat Sep 26 15:55:02 UTC 2026
% 0.09/10.54 % CPUTime :
% 0.09/10.54 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/10.54 % Process 2113580 was started by sandbox2 on n002,
% 0.09/10.54 % Sat Sep 26 15:55:02 2026
% 0.09/10.54 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/10.54
% 0.09/10.54 % From the command line: assign(max_seconds, 300).
% 46.76/17.41
% 46.76/17.41 % SZS status Unsatisfiable for theBenchmark
% 46.76/17.41
% 46.76/17.41 % Proof 1 at 5.72 (+ 1.12) seconds.
% 46.76/17.41 % Length of proof is 14.
% 46.76/17.41 % Level of proof is 5.
% 46.76/17.41 % Maximum clause weight is 46.000.
% 46.76/17.41 % Given clauses 328.
% 46.76/17.41
% 46.76/17.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------