%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW445-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:07:52 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.56s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 106
% Number of leaves : 11
% Syntax : Number of formulae : 142 ( 79 unt; 5 def)
% Number of atoms : 273 ( 39 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 250 ( 119 ~; 126 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-2 aty)
% Number of variables : 42 ( 42 !; 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(f12,hypothesis,
x6 != x19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
x3 != x20,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,plain,
! [X0,X1,X2] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f33,plain,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f40,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(f41,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3))) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f50,plain,
x6 != x19,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f52,plain,
x3 != x20,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f68,plain,
heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f79,plain,
! [X0,X1,X2,X3] : sep(X0,sep(X1,sep(X2,X3))) = sep(X2,sep(X0,sep(X1,X3))),
inference(paramodulation,[status(thm)],[f32,f32]) ).
fof(f89,plain,
! [X0,X1,X2,X3,X4] :
( X0 = X3
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4)))) ),
inference(paramodulation,[status(thm)],[f32,f41]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X3
| X1 = X2
| ~ heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))) ),
inference(paramodulation,[status(thm)],[f32,f89]) ).
fof(f167,plain,
heap(sep(lseg(x19,x1),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f68]) ).
fof(f168,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f167]) ).
fof(f169,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f168]) ).
fof(f170,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f169]) ).
fof(f171,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x2,x18),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f170]) ).
fof(f172,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x2,x18),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f171]) ).
fof(f173,plain,
heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f172]) ).
fof(f174,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f173]) ).
fof(f175,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f174]) ).
fof(f176,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x17,x14),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f175]) ).
fof(f177,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f176]) ).
fof(f178,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x17,x14),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f177]) ).
fof(f179,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f178]) ).
fof(f180,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x7,x16),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f179]) ).
fof(f181,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x7,x16),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f180]) ).
fof(f182,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x7,x16),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f181]) ).
fof(f183,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f182]) ).
fof(f184,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f183]) ).
fof(f185,plain,
heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x7,x16),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f184]) ).
fof(f186,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f185]) ).
fof(f187,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f186]) ).
fof(f188,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x3,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f187]) ).
fof(f189,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x3,x20),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f188]) ).
fof(f190,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f189]) ).
fof(f191,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x3,x20),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f190]) ).
fof(f192,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x20),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f191]) ).
fof(f193,plain,
heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f192]) ).
fof(f194,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f193]) ).
fof(f195,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f194]) ).
fof(f196,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x3,x12),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f195]) ).
fof(f197,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x3,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f196]) ).
fof(f198,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x3,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f197]) ).
fof(f199,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f198]) ).
fof(f200,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x12),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f199]) ).
fof(f201,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f200]) ).
fof(f202,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f201]) ).
fof(f203,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f202]) ).
fof(f204,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x11,x12),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f203]) ).
fof(f205,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f204]) ).
fof(f206,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f205]) ).
fof(f207,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x6,x17),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f206]) ).
fof(f208,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x6,x17),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f207]) ).
fof(f209,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x6,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f208]) ).
fof(f210,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f209]) ).
fof(f211,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x6,x17),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f210]) ).
fof(f212,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x6,x17),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f211]) ).
fof(f213,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x17),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f212]) ).
fof(f214,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f213]) ).
fof(f215,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x17),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f214]) ).
fof(f216,plain,
heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x17),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f215]) ).
fof(f217,plain,
heap(sep(lseg(x19,x1),sep(lseg(x6,x17),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f216]) ).
fof(f218,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f217]) ).
fof(f219,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x6,x19),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f218]) ).
fof(f220,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x6,x19),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f219]) ).
fof(f221,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x6,x19),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f220]) ).
fof(f222,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x6,x19),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f221]) ).
fof(f223,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x6,x19),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f222]) ).
fof(f224,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x6,x19),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f223]) ).
fof(f225,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x19),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f224]) ).
fof(f226,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f225]) ).
fof(f227,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x19),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f226]) ).
fof(f228,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x19),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f227]) ).
fof(f229,plain,
heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x6,x19),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f228]) ).
fof(f230,plain,
heap(sep(lseg(x6,x17),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f229]) ).
fof(f231,plain,
heap(sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))),
inference(forward_demodulation,[status(thm)],[f32,f230]) ).
fof(f242,plain,
( x6 = x17
| x6 = x19 ),
inference(resolution,[status(thm)],[f41,f231]) ).
fof(f249,definition,
( sQ4_spl
<=> x6 = x19 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f250,plain,
( ~ sQ4_spl
| x6 = x19 ),
inference(component_clause,[status(thm)],[f249]) ).
fof(f252,definition,
( sQ5_spl
<=> x6 = x17 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f253,plain,
( ~ sQ5_spl
| x6 = x17 ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f255,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f242,f249,f252]) ).
fof(f256,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f250,f50]) ).
fof(f257,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f256]) ).
fof(f267,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))) ),
inference(backward_demodulation,[status(thm)],[f253,f231]) ).
fof(f270,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f253,f267]) ).
fof(f271,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x6),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f270]) ).
fof(f272,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f33,f271]) ).
fof(f273,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f253,f272]) ).
fof(f274,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x14),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f273]) ).
fof(f275,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x14),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f274]) ).
fof(f276,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x14),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f275]) ).
fof(f277,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x6,x14),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f276]) ).
fof(f278,plain,
( ~ sQ5_spl
| heap(sep(lseg(x6,x19),sep(lseg(x6,x14),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f277]) ).
fof(f279,plain,
( ~ sQ5_spl
| x6 = x14
| x6 = x19 ),
inference(resolution,[status(thm)],[f278,f41]) ).
fof(f280,definition,
( sQ6_spl
<=> x6 = x14 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f281,plain,
( ~ sQ6_spl
| x6 = x14 ),
inference(component_clause,[status(thm)],[f280]) ).
fof(f283,plain,
( ~ sQ5_spl
| sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f279,f249,f280,f252]) ).
fof(f284,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(backward_demodulation,[status(thm)],[f281,f278]) ).
fof(f285,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x6,x6),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f32,f284]) ).
fof(f286,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f33,f285]) ).
fof(f404,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X4
| X2 = X3
| ~ heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5))))) ),
inference(paramodulation,[status(thm)],[f79,f129]) ).
fof(f690,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| x3 = x12
| x3 = x20 ),
inference(resolution,[status(thm)],[f404,f286]) ).
fof(f711,definition,
( sQ8_spl
<=> x3 = x20 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f712,plain,
( ~ sQ8_spl
| x3 = x20 ),
inference(component_clause,[status(thm)],[f711]) ).
fof(f714,definition,
( sQ9_spl
<=> x3 = x12 ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f715,plain,
( ~ sQ9_spl
| x3 = x12 ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f717,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f690,f711,f714,f280,f252]) ).
fof(f718,plain,
( ~ sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f52]) ).
fof(f719,plain,
~ sQ8_spl,
inference(contradiction_clause,[status(thm)],[f718]) ).
fof(f720,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))) ),
inference(backward_demodulation,[status(thm)],[f715,f286]) ).
fof(f721,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x3),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f715,f720]) ).
fof(f722,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x3),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f721]) ).
fof(f723,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f33,f722]) ).
fof(f724,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f723]) ).
fof(f725,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f724]) ).
fof(f726,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x11,x12),sep(lseg(x4,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f725]) ).
fof(f727,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x6),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f726]) ).
fof(f728,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x5,x6),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f715,f727]) ).
fof(f729,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f728]) ).
fof(f730,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x12,x20),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f715,f729]) ).
fof(f731,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x12,x20),sep(lseg(x3,x15),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f730]) ).
fof(f732,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x3,x15),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f731]) ).
fof(f733,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x3,x15),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f732]) ).
fof(f734,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x15),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f733]) ).
fof(f735,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f734]) ).
fof(f736,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x3,x20),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f715,f735]) ).
fof(f737,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f736]) ).
fof(f738,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f737]) ).
fof(f739,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f738]) ).
fof(f740,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x3,x11),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f715,f739]) ).
fof(f741,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x3,x11),sep(lseg(x11,x3),sep(lseg(x5,x6),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f740]) ).
fof(f742,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x3,x11),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f741]) ).
fof(f743,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x11),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f79,f742]) ).
fof(f744,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| x3 = x20
| x3 = x20 ),
inference(resolution,[status(thm)],[f743,f404]) ).
fof(f745,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f744,f711,f714,f280,f252]) ).
fof(f746,plain,
$false,
inference(sat_refutation,[status(thm)],[f255,f257,f283,f717,f719,f745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW445-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n018.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 09:55:30 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.36 % Drodi V4.1.1
% 0.13/0.56 % Refutation found
% 0.13/0.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.61 % Elapsed time: 0.236401 seconds
% 0.27/0.61 % CPU time: 1.497745 seconds
% 0.27/0.61 % Total memory used: 118.913 MB
% 0.27/0.61 % Net memory used: 117.825 MB
%------------------------------------------------------------------------------