%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW434-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : Thu Sep 24 03:07:51 PM UTC 2026
% Result : Unsatisfiable 79.01s 10.63s
% Output : CNFRefutation 79.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 19
% Syntax : Number of formulae : 230 ( 57 unt; 13 def)
% Number of atoms : 834 ( 94 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 1166 ( 562 ~; 591 |; 0 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 16 ( 14 usr; 14 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 64 ( 64 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Sigma] : sep(lseg(X,X),Sigma) = Sigma,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X,Y,Z,Sigma] :
( X = Z
| X = Y
| ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
x9 != x14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
x13 != x14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
heap(sep(lseg(x5,x10),sep(lseg(x13,x12),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x13),sep(lseg(x11,x3),emp))))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,plain,
! [X0,X1,X2] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f29,plain,
! [X,Z] :
( X = Z
| ! [Y] :
( X = Y
| ! [Sigma] : ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( X1 = X0
| X2 = X0
| ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3))) ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f44,plain,
x9 != x14,
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f45,plain,
x13 != x14,
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f46,plain,
heap(sep(lseg(x5,x10),sep(lseg(x13,x12),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x13),sep(lseg(x11,x3),emp))))))))))))),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f55,plain,
heap(sep(lseg(x5,x10),sep(lseg(x13,x12),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(backward_demodulation,[status(thm)],[f21,f46]) ).
fof(f56,plain,
heap(sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f55]) ).
fof(f57,plain,
heap(sep(lseg(x13,x12),sep(lseg(x1,x7),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f56]) ).
fof(f58,plain,
heap(sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f57]) ).
fof(f59,plain,
heap(sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x8,x14),sep(lseg(x5,x10),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f58]) ).
fof(f60,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f59]) ).
fof(f61,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x13,x12),sep(lseg(x12,x8),sep(lseg(x5,x10),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f60]) ).
fof(f62,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f61]) ).
fof(f63,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f62]) ).
fof(f64,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x5,x10),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f63]) ).
fof(f65,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f64]) ).
fof(f66,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f65]) ).
fof(f67,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f66]) ).
fof(f68,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f67]) ).
fof(f69,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x9,x14),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f68]) ).
fof(f70,plain,
heap(sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f69]) ).
fof(f71,plain,
heap(sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f70]) ).
fof(f72,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f71]) ).
fof(f73,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x9,x1),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f72]) ).
fof(f74,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x9,x1),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f73]) ).
fof(f75,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f74]) ).
fof(f76,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f75]) ).
fof(f77,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x9,x1),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f76]) ).
fof(f78,plain,
heap(sep(lseg(x9,x14),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f77]) ).
fof(f79,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f78]) ).
fof(f80,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x3,x9),sep(lseg(x5,x10),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f79]) ).
fof(f81,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x3,x9),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f80]) ).
fof(f82,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f81]) ).
fof(f83,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x3),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f82]) ).
fof(f84,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x3),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f83]) ).
fof(f85,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x11,x3),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f84]) ).
fof(f86,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f85]) ).
fof(f87,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f86]) ).
fof(f88,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f87]) ).
fof(f89,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x11,x13),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f88]) ).
fof(f90,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f89]) ).
fof(f91,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f90]) ).
fof(f92,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f91]) ).
fof(f93,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x11,x13),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f92]) ).
fof(f94,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f93]) ).
fof(f95,plain,
heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x1,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))),
inference(forward_demodulation,[status(thm)],[f21,f94]) ).
fof(f104,plain,
( x1 = x9
| x14 = x9 ),
inference(resolution,[status(thm)],[f95,f30]) ).
fof(f105,definition,
( sQ2_spl
<=> x14 = x9 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f106,plain,
( ~ sQ2_spl
| x14 = x9 ),
inference(component_clause,[status(thm)],[f105]) ).
fof(f108,definition,
( sQ3_spl
<=> x1 = x9 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f109,plain,
( ~ sQ3_spl
| x9 = x1 ),
inference(component_clause,[status(thm)],[f108]) ).
fof(f111,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f104,f105,f108]) ).
fof(f112,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f106,f44]) ).
fof(f113,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f112]) ).
fof(f114,plain,
( ~ sQ3_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x9,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))) ),
inference(backward_demodulation,[status(thm)],[f109,f95]) ).
fof(f115,plain,
( ~ sQ3_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x9,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f109,f114]) ).
fof(f116,plain,
( ~ sQ3_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x7),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f115]) ).
fof(f117,plain,
( ~ sQ3_spl
| x7 = x9
| x14 = x9 ),
inference(resolution,[status(thm)],[f116,f30]) ).
fof(f118,definition,
( sQ4_spl
<=> x7 = x9 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f119,plain,
( ~ sQ4_spl
| x7 = x9 ),
inference(component_clause,[status(thm)],[f118]) ).
fof(f121,plain,
( ~ sQ3_spl
| sQ4_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f117,f105,f118,f108]) ).
fof(f122,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))))) ),
inference(backward_demodulation,[status(thm)],[f119,f116]) ).
fof(f124,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f122]) ).
fof(f203,plain,
! [X0,X1,X2,X3] : sep(X0,sep(X1,sep(X2,X3))) = sep(X1,sep(X2,sep(X0,X3))),
inference(paramodulation,[status(thm)],[f21,f21]) ).
fof(f273,plain,
! [X0,X1,X2,X3,X4] :
( X0 = X3
| ~ heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f21,f30]) ).
fof(f282,plain,
! [X0,X1,X2,X3,X4] :
( ~ heap(sep(X3,sep(lseg(X0,X1),sep(lseg(X0,X2),X4))))
| X0 = X2
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f21,f273]) ).
fof(f314,plain,
! [X0,X1,X2,X3,X4,X5] :
( X4 = X1
| X2 = X1
| ~ heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5))))) ),
inference(paramodulation,[status(thm)],[f21,f282]) ).
fof(f548,plain,
! [X0,X1,X2,X3,X4,X5] :
( X4 = X1
| ~ heap(sep(X2,sep(X3,sep(lseg(X1,X0),sep(lseg(X1,X4),X5)))))
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f21,f314]) ).
fof(f582,plain,
! [X0,X1,X2,X3,X4,X5] : sep(X0,sep(X1,sep(X2,sep(X3,sep(X4,X5))))) = sep(X1,sep(X2,sep(X4,sep(X0,sep(X3,X5))))),
inference(paramodulation,[status(thm)],[f203,f203]) ).
fof(f583,plain,
! [X0,X1,X2,X3,X4,X5] : sep(X0,sep(X1,sep(X2,sep(X3,sep(X4,X5))))) = sep(X4,sep(X0,sep(X1,sep(X2,sep(X3,X5))))),
inference(paramodulation,[status(thm)],[f203,f203]) ).
fof(f660,plain,
! [X0,X1,X2,X3] : sep(X0,sep(X1,sep(X2,X3))) = sep(X0,sep(X2,sep(X1,X3))),
inference(paramodulation,[status(thm)],[f203,f21]) ).
fof(f775,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| x3 = x11
| x11 = x13 ),
inference(resolution,[status(thm)],[f548,f124]) ).
fof(f804,definition,
( sQ15_spl
<=> x11 = x13 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f805,plain,
( ~ sQ15_spl
| x13 = x11 ),
inference(component_clause,[status(thm)],[f804]) ).
fof(f806,plain,
( sQ15_spl
| x11 != x13 ),
inference(component_clause,[status(thm)],[f804]) ).
fof(f807,definition,
( sQ16_spl
<=> x3 = x11 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f808,plain,
( ~ sQ16_spl
| x3 = x11 ),
inference(component_clause,[status(thm)],[f807]) ).
fof(f810,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f775,f804,f807,f118,f108]) ).
fof(f811,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x11,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(backward_demodulation,[status(thm)],[f805,f124]) ).
fof(f812,plain,
( ~ sQ15_spl
| x14 != x11 ),
inference(backward_demodulation,[status(thm)],[f805,f45]) ).
fof(f813,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f583,f811]) ).
fof(f814,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f805,f813]) ).
fof(f815,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f203,f814]) ).
fof(f816,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f815]) ).
fof(f817,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| x12 = x11
| x11 = x3 ),
inference(resolution,[status(thm)],[f816,f548]) ).
fof(f818,definition,
( sQ17_spl
<=> x12 = x11 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f819,plain,
( ~ sQ17_spl
| x12 = x11 ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f820,plain,
( sQ17_spl
| x11 != x12 ),
inference(component_clause,[status(thm)],[f818]) ).
fof(f821,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f817,f807,f818,f804,f118,f108]) ).
fof(f823,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f808,f124]) ).
fof(f824,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f823]) ).
fof(f825,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x11,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f808,f824]) ).
fof(f826,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f203,f825]) ).
fof(f827,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| x9 = x11
| x11 = x13 ),
inference(resolution,[status(thm)],[f826,f548]) ).
fof(f828,definition,
( sQ18_spl
<=> x9 = x11 ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f829,plain,
( ~ sQ18_spl
| x9 = x11 ),
inference(component_clause,[status(thm)],[f828]) ).
fof(f831,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| sQ18_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f827,f804,f828,f807,f118,f108]) ).
fof(f834,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f808,f816]) ).
fof(f835,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f834]) ).
fof(f836,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f835]) ).
fof(f837,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f808,f836]) ).
fof(f838,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f203,f837]) ).
fof(f843,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| x9 = x11
| x11 = x12 ),
inference(resolution,[status(thm)],[f838,f548]) ).
fof(f844,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f843,f818,f828,f807,f804,f118,f108]) ).
fof(f845,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f805,f124]) ).
fof(f846,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f845]) ).
fof(f847,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f846]) ).
fof(f848,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f847]) ).
fof(f849,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f848]) ).
fof(f850,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x11,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f805,f849]) ).
fof(f851,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f203,f850]) ).
fof(f852,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f851]) ).
fof(f853,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f852]) ).
fof(f854,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x11),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f853]) ).
fof(f860,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| x8 = x11
| x11 = x3 ),
inference(resolution,[status(thm)],[f854,f548]) ).
fof(f861,definition,
( sQ19_spl
<=> x8 = x11 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f862,plain,
( ~ sQ19_spl
| x11 = x8 ),
inference(component_clause,[status(thm)],[f861]) ).
fof(f863,plain,
( sQ19_spl
| x8 != x11 ),
inference(component_clause,[status(thm)],[f861]) ).
fof(f864,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| sQ19_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f860,f807,f861,f818,f804,f118,f108]) ).
fof(f868,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(backward_demodulation,[status(thm)],[f808,f816]) ).
fof(f877,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f582,f868]) ).
fof(f878,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x9),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f877]) ).
fof(f879,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f878]) ).
fof(f880,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f879]) ).
fof(f881,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f880]) ).
fof(f882,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f881]) ).
fof(f883,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f882]) ).
fof(f884,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x9,x3),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f883]) ).
fof(f885,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x9,x3),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f884]) ).
fof(f886,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x9,x11),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f808,f885]) ).
fof(f887,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x11),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f886]) ).
fof(f888,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f887]) ).
fof(f889,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f888]) ).
fof(f890,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x2,x9),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f889]) ).
fof(f897,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| x12 = x9
| x14 = x9 ),
inference(resolution,[status(thm)],[f890,f30]) ).
fof(f898,definition,
( sQ20_spl
<=> x12 = x9 ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f899,plain,
( ~ sQ20_spl
| x9 = x12 ),
inference(component_clause,[status(thm)],[f898]) ).
fof(f900,plain,
( sQ20_spl
| x12 != x9 ),
inference(component_clause,[status(thm)],[f898]) ).
fof(f901,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ18_spl
| sQ20_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f897,f105,f898,f828,f807,f804,f118,f108]) ).
fof(f902,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x5,x10),emp))))))))) ),
inference(backward_demodulation,[status(thm)],[f862,f854]) ).
fof(f903,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(backward_demodulation,[status(thm)],[f862,f816]) ).
fof(f904,plain,
( ~ sQ15_spl
| ~ sQ19_spl
| x8 != x14 ),
inference(backward_demodulation,[status(thm)],[f862,f812]) ).
fof(f905,plain,
( ~ sQ17_spl
| ~ sQ19_spl
| x8 = x12 ),
inference(forward_demodulation,[status(thm)],[f862,f819]) ).
fof(f910,plain,
( ~ sQ20_spl
| ~ sQ17_spl
| ~ sQ19_spl
| x8 = x9 ),
inference(forward_demodulation,[status(thm)],[f905,f899]) ).
fof(f913,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f903]) ).
fof(f914,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x8,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f862,f913]) ).
fof(f915,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x12),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f914]) ).
fof(f916,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f905,f915]) ).
fof(f917,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f916]) ).
fof(f918,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f917]) ).
fof(f919,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x8,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f862,f918]) ).
fof(f920,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f919]) ).
fof(f921,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x8,x8),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f905,f920]) ).
fof(f922,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f921]) ).
fof(f923,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x3,x9),sep(lseg(x2,x9),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f922]) ).
fof(f924,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x3,x9),sep(lseg(x2,x9),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f905,f923]) ).
fof(f925,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x3,x9),sep(lseg(x2,x9),sep(lseg(x2,x9),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f910,f924]) ).
fof(f938,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| x14 = x9
| x14 = x9 ),
inference(resolution,[status(thm)],[f925,f30]) ).
fof(f941,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f938,f105,f818,f898,f861,f804,f118,f108]) ).
fof(f951,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x8),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f862,f902]) ).
fof(f952,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f951]) ).
fof(f953,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x3),sep(lseg(x3,x9),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f862,f952]) ).
fof(f954,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x3),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x11),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f953]) ).
fof(f955,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x3),sep(lseg(x3,x9),sep(lseg(x2,x8),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f862,f954]) ).
fof(f961,plain,
( sQ20_spl
| ~ sQ17_spl
| ~ sQ19_spl
| x9 != x8 ),
inference(forward_demodulation,[status(thm)],[f905,f900]) ).
fof(f962,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| x3 = x8
| x14 = x8 ),
inference(resolution,[status(thm)],[f955,f282]) ).
fof(f963,definition,
( sQ22_spl
<=> x14 = x8 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f964,plain,
( ~ sQ22_spl
| x14 = x8 ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,definition,
( sQ23_spl
<=> x3 = x8 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f967,plain,
( ~ sQ23_spl
| x8 = x3 ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f962,f963,f966,f861,f818,f804,f118,f108]) ).
fof(f970,plain,
( ~ sQ22_spl
| ~ sQ15_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f964,f904]) ).
fof(f971,plain,
( ~ sQ22_spl
| ~ sQ15_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f970]) ).
fof(f972,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x3),sep(lseg(x8,x9),sep(lseg(x2,x8),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(backward_demodulation,[status(thm)],[f967,f955]) ).
fof(f974,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x9),sep(lseg(x8,x3),sep(lseg(x2,x8),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f972]) ).
fof(f975,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x9),sep(lseg(x8,x8),sep(lseg(x2,x8),sep(lseg(x2,x8),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f967,f974]) ).
fof(f976,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x8,x9),sep(lseg(x2,x8),sep(lseg(x2,x8),sep(lseg(x5,x10),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f975]) ).
fof(f977,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| x9 = x8
| x14 = x8 ),
inference(resolution,[status(thm)],[f976,f282]) ).
fof(f978,definition,
( sQ24_spl
<=> x9 = x8 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f979,plain,
( ~ sQ24_spl
| x9 = x8 ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ17_spl
| ~ sQ19_spl
| ~ sQ23_spl
| sQ24_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f977,f963,f978,f966,f861,f818,f804,f118,f108]) ).
fof(f982,plain,
( ~ sQ24_spl
| sQ20_spl
| ~ sQ17_spl
| ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f979,f961]) ).
fof(f983,plain,
( ~ sQ24_spl
| sQ20_spl
| ~ sQ17_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f982]) ).
fof(f984,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x11),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f838]) ).
fof(f985,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f984]) ).
fof(f986,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x8),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f985]) ).
fof(f987,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x9),sep(lseg(x11,x8),sep(lseg(x2,x11),sep(lseg(x2,x11),sep(lseg(x5,x10),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f819,f986]) ).
fof(f1009,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| x9 = x11
| x11 = x8 ),
inference(resolution,[status(thm)],[f987,f548]) ).
fof(f1010,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ15_spl
| ~ sQ16_spl
| ~ sQ17_spl
| sQ18_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f1009,f861,f828,f818,f807,f804,f118,f108]) ).
fof(f1015,plain,
( sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| x8 != x9 ),
inference(backward_demodulation,[status(thm)],[f1018,f863]) ).
fof(f1018,plain,
( ~ sQ20_spl
| ~ sQ17_spl
| x11 = x9 ),
inference(forward_demodulation,[status(thm)],[f819,f899]) ).
fof(f1132,plain,
( ~ sQ24_spl
| sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f979,f1015]) ).
fof(f1133,plain,
( ~ sQ24_spl
| sQ19_spl
| ~ sQ20_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f1132]) ).
fof(f1143,plain,
( sQ17_spl
| ~ sQ20_spl
| x11 != x9 ),
inference(backward_demodulation,[status(thm)],[f899,f820]) ).
fof(f1166,plain,
( sQ17_spl
| ~ sQ20_spl
| ~ sQ18_spl ),
inference(split_clause,[status(thm)],[f1143,f828,f898,f818]) ).
fof(f1169,plain,
( ~ sQ17_spl
| ~ sQ18_spl
| x12 = x9 ),
inference(forward_demodulation,[status(thm)],[f829,f819]) ).
fof(f1170,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x9),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f826]) ).
fof(f1171,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x9),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f1170]) ).
fof(f1172,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f22,f1171]) ).
fof(f1173,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f1172]) ).
fof(f1174,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f1173]) ).
fof(f1180,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x3),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f124]) ).
fof(f1181,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f1180]) ).
fof(f1213,plain,
( sQ15_spl
| ~ sQ18_spl
| x9 != x13 ),
inference(forward_demodulation,[status(thm)],[f829,f806]) ).
fof(f1237,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x8,x14),sep(lseg(x9,x13),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f1181]) ).
fof(f1238,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f1237]) ).
fof(f1239,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x9,x8),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f1169,f1238]) ).
fof(f1240,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x3,x9),sep(lseg(x8,x14),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f582,f1239]) ).
fof(f1241,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f660,f1240]) ).
fof(f1242,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x13,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f1169,f1241]) ).
fof(f1243,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x13,x9),sep(lseg(x2,x9),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f1242]) ).
fof(f1244,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x8),sep(lseg(x9,x3),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x13,x9),sep(lseg(x2,x9),sep(lseg(x2,x9),sep(lseg(x5,x10),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f1169,f1243]) ).
fof(f1279,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| x14 = x9
| x8 = x9 ),
inference(resolution,[status(thm)],[f1244,f30]) ).
fof(f1280,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ18_spl
| ~ sQ17_spl
| sQ2_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f1279,f978,f105,f818,f828,f118,f108]) ).
fof(f1283,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| heap(sep(lseg(x9,x14),sep(lseg(x9,x13),sep(lseg(x8,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x9),sep(lseg(x2,x12),sep(lseg(x5,x10),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f829,f1174]) ).
fof(f1358,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| x14 = x9
| x13 = x9 ),
inference(resolution,[status(thm)],[f1283,f30]) ).
fof(f1359,definition,
( sQ25_spl
<=> x13 = x9 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f1360,plain,
( ~ sQ25_spl
| x13 = x9 ),
inference(component_clause,[status(thm)],[f1359]) ).
fof(f1362,plain,
( ~ sQ3_spl
| ~ sQ4_spl
| ~ sQ16_spl
| ~ sQ18_spl
| sQ2_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f1358,f1359,f105,f828,f807,f118,f108]) ).
fof(f1363,plain,
( ~ sQ25_spl
| sQ15_spl
| ~ sQ18_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1360,f1213]) ).
fof(f1364,plain,
( ~ sQ25_spl
| sQ15_spl
| ~ sQ18_spl ),
inference(contradiction_clause,[status(thm)],[f1363]) ).
fof(f1365,plain,
$false,
inference(sat_refutation,[status(thm)],[f111,f113,f121,f810,f821,f831,f844,f864,f901,f941,f969,f971,f981,f983,f1010,f1133,f1166,f1280,f1362,f1364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW434-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.47 % Computer : n026.cluster.edu
% 0.19/0.47 % Model : x86_64 x86_64
% 0.19/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.47 % Memory : 8046.5625MB
% 0.19/0.47 % OS : Linux 6.8.0-71-generic
% 0.19/0.47 % CPULimit : 300
% 0.19/0.47 % WCLimit : 300
% 0.19/0.47 % DateTime : Mon Sep 21 09:55:37 UTC 2026
% 0.19/0.48 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 79.01/10.63 % Refutation found
% 79.01/10.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 79.01/10.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 57.44/10.70 % Elapsed time: 10.201128 seconds
% 57.44/10.70 % CPU time: 80.136390 seconds
% 57.44/10.70 % Total memory used: 265.750 MB
% 57.44/10.70 % Net memory used: 255.024 MB
%------------------------------------------------------------------------------