%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW429-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:50 PM UTC 2026
% Result : Unsatisfiable 0.21s 5.89s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 24
% Syntax : Number of formulae : 173 ( 29 unt; 16 def)
% Number of atoms : 638 ( 80 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 887 ( 422 ~; 449 |; 0 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 19 ( 17 usr; 17 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 76 ( 76 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [S,T,Sigma] : sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Sigma] : sep(lseg(X,X),Sigma) = Sigma,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [Y,Sigma] :
( Y = nil
| ~ heap(sep(lseg(nil,Y),Sigma)) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y,Z,W,Sigma] :
( heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma)))
| Z = W
| ~ heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
x4 != x7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
x3 != x8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
heap(sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,plain,
! [X0,X1,X2] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [Y] :
( Y = nil
| ! [Sigma] : ~ heap(sep(lseg(nil,Y),Sigma)) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f23,plain,
! [X0,X1] :
( X0 = nil
| ~ heap(sep(lseg(nil,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f27,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(f28,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| X0 = X1
| ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3))) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f35,plain,
! [X,Z,W,Sigma] :
( heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma)))
| Z = W
| ! [Y] : ~ heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma)))) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f36,plain,
! [X0,X1,X2,X3,X4] :
( heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4)))
| X2 = X3
| ~ heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X2,X3),X4)))) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
x4 != x7,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f39,plain,
x3 != x8,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f42,plain,
heap(sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f53,plain,
! [X0,X1,X2,X3] : sep(X0,sep(X1,sep(X2,X3))) = sep(X2,sep(X0,sep(X1,X3))),
inference(paramodulation,[status(thm)],[f19,f19]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4] :
( heap(sep(lseg(X2,X1),sep(lseg(X1,X3),X4)))
| X1 = X3
| ~ heap(sep(lseg(X0,X1),sep(lseg(X2,X0),sep(lseg(X1,X3),X4)))) ),
inference(paramodulation,[status(thm)],[f19,f36]) ).
fof(f63,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)],[f19,f28]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4] :
( heap(sep(lseg(X3,X1),sep(lseg(X1,X2),X4)))
| X1 = X2
| ~ heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X3,X0),X4)))) ),
inference(paramodulation,[status(thm)],[f19,f59]) ).
fof(f91,plain,
! [X0] :
( nil = nil
| ~ heap(X0) ),
inference(paramodulation,[status(thm)],[f20,f23]) ).
fof(f94,definition,
! [X0] :
( sQ2_spl
<=> ~ heap(X0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f95,plain,
! [X0] :
( ~ sQ2_spl
| ~ heap(X0) ),
inference(component_clause,[status(thm)],[f94]) ).
fof(f97,definition,
( sQ3_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f100,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f91,f94,f97]) ).
fof(f103,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)],[f19,f63]) ).
fof(f186,plain,
heap(sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x5,x1),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f42]) ).
fof(f187,plain,
heap(sep(lseg(x7,x8),sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f186]) ).
fof(f188,plain,
heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f187]) ).
fof(f189,plain,
heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f188]) ).
fof(f190,plain,
heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x4,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f189]) ).
fof(f191,plain,
heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f190]) ).
fof(f192,plain,
heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x4,x7),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f191]) ).
fof(f193,plain,
heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f192]) ).
fof(f194,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f193]) ).
fof(f195,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x8,x11),sep(lseg(x6,x9),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f194]) ).
fof(f196,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f195]) ).
fof(f197,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f196]) ).
fof(f198,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f197]) ).
fof(f199,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f53,f198]) ).
fof(f200,plain,
heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))),
inference(forward_demodulation,[status(thm)],[f19,f199]) ).
fof(f201,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f200,f95]) ).
fof(f202,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f201]) ).
fof(f235,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)],[f53,f103]) ).
fof(f307,plain,
( x4 = x12
| x4 = x7 ),
inference(resolution,[status(thm)],[f200,f28]) ).
fof(f308,definition,
( sQ4_spl
<=> x4 = x7 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f309,plain,
( ~ sQ4_spl
| x4 = x7 ),
inference(component_clause,[status(thm)],[f308]) ).
fof(f311,definition,
( sQ5_spl
<=> x4 = x12 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f312,plain,
( ~ sQ5_spl
| x4 = x12 ),
inference(component_clause,[status(thm)],[f311]) ).
fof(f314,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f307,f308,f311]) ).
fof(f315,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f309,f37]) ).
fof(f316,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f315]) ).
fof(f341,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))) ),
inference(backward_demodulation,[status(thm)],[f312,f200]) ).
fof(f342,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f312,f341]) ).
fof(f343,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x4),sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f342]) ).
fof(f344,plain,
( ~ sQ5_spl
| heap(sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f343]) ).
fof(f345,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f344]) ).
fof(f346,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x7,x12),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f345]) ).
fof(f347,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f346]) ).
fof(f348,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f312,f347]) ).
fof(f349,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f348]) ).
fof(f350,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f349]) ).
fof(f351,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f350]) ).
fof(f352,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f351]) ).
fof(f353,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f352]) ).
fof(f354,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f353]) ).
fof(f355,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f354]) ).
fof(f356,plain,
( ~ sQ5_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f19,f355]) ).
fof(f357,plain,
( ~ sQ5_spl
| x7 = x8
| x7 = x4 ),
inference(resolution,[status(thm)],[f356,f103]) ).
fof(f358,definition,
( sQ6_spl
<=> x7 = x8 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( ~ sQ6_spl
| x7 = x8 ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,plain,
( ~ sQ5_spl
| sQ6_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f357,f308,f358,f311]) ).
fof(f362,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(backward_demodulation,[status(thm)],[f359,f356]) ).
fof(f363,plain,
( ~ sQ6_spl
| x3 != x7 ),
inference(backward_demodulation,[status(thm)],[f359,f39]) ).
fof(f364,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))) ),
inference(forward_demodulation,[status(thm)],[f359,f362]) ).
fof(f365,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f364]) ).
fof(f366,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x11),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f365]) ).
fof(f367,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| x7 = x11
| x7 = x4 ),
inference(resolution,[status(thm)],[f366,f103]) ).
fof(f368,definition,
( sQ7_spl
<=> x7 = x11 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f369,plain,
( ~ sQ7_spl
| x7 = x11 ),
inference(component_clause,[status(thm)],[f368]) ).
fof(f371,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| sQ7_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f367,f308,f368,f358,f311]) ).
fof(f372,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))) ),
inference(backward_demodulation,[status(thm)],[f369,f366]) ).
fof(f373,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f372]) ).
fof(f469,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))
| x7 = x4 ),
inference(resolution,[status(thm)],[f72,f373]) ).
fof(f485,definition,
( sQ9_spl
<=> heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ9_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f469,f308,f485,f368,f358,f311]) ).
fof(f646,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| x3 = x5
| x3 = x4 ),
inference(resolution,[status(thm)],[f235,f373]) ).
fof(f668,definition,
( sQ10_spl
<=> x3 = x4 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f669,plain,
( ~ sQ10_spl
| x3 = x4 ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f671,definition,
( sQ11_spl
<=> x3 = x5 ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( ~ sQ11_spl
| x3 = x5 ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f646,f668,f671,f368,f358,f311]) ).
fof(f699,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(backward_demodulation,[status(thm)],[f669,f373]) ).
fof(f701,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f699]) ).
fof(f702,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x4,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f669,f701]) ).
fof(f703,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f702]) ).
fof(f704,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x4),sep(lseg(x4,x5),sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f703]) ).
fof(f705,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x5),sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f704]) ).
fof(f706,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f705]) ).
fof(f707,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f706]) ).
fof(f708,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f707]) ).
fof(f709,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f708]) ).
fof(f710,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f709]) ).
fof(f711,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f19,f710]) ).
fof(f739,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| x4 = x5
| x4 = x7 ),
inference(resolution,[status(thm)],[f711,f28]) ).
fof(f740,definition,
( sQ12_spl
<=> x4 = x5 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f741,plain,
( ~ sQ12_spl
| x4 = x5 ),
inference(component_clause,[status(thm)],[f740]) ).
fof(f747,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| sQ12_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f739,f308,f740,f668,f368,f358,f311]) ).
fof(f760,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(backward_demodulation,[status(thm)],[f741,f711]) ).
fof(f762,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f741,f760]) ).
fof(f763,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f762]) ).
fof(f764,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f763]) ).
fof(f765,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f764]) ).
fof(f767,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| x4 = x1
| x4 = x7 ),
inference(resolution,[status(thm)],[f765,f28]) ).
fof(f768,definition,
( sQ14_spl
<=> x4 = x1 ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( ~ sQ14_spl
| x4 = x1 ),
inference(component_clause,[status(thm)],[f768]) ).
fof(f775,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| sQ14_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f767,f308,f768,f740,f668,f368,f358,f311]) ).
fof(f776,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x7,x4),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(backward_demodulation,[status(thm)],[f769,f765]) ).
fof(f777,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f769,f776]) ).
fof(f778,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f777]) ).
fof(f779,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f20,f778]) ).
fof(f780,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f53,f779]) ).
fof(f782,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| x4 = x6
| x4 = x7 ),
inference(resolution,[status(thm)],[f780,f28]) ).
fof(f783,definition,
( sQ16_spl
<=> x4 = x6 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f784,plain,
( ~ sQ16_spl
| x4 = x6 ),
inference(component_clause,[status(thm)],[f783]) ).
fof(f790,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| sQ16_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f782,f308,f783,f768,f740,f668,f368,f358,f311]) ).
fof(f839,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x4,x9),emp)))))) ),
inference(backward_demodulation,[status(thm)],[f784,f780]) ).
fof(f840,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x4,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f784,f839]) ).
fof(f841,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x4,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f53,f840]) ).
fof(f842,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x4,x9),emp))))) ),
inference(forward_demodulation,[status(thm)],[f20,f841]) ).
fof(f843,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x7,x4),sep(lseg(x4,x9),emp))))) ),
inference(forward_demodulation,[status(thm)],[f53,f842]) ).
fof(f844,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x4,x9),sep(lseg(x6,x7),emp))))) ),
inference(forward_demodulation,[status(thm)],[f53,f843]) ).
fof(f845,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x6,x7),sep(lseg(x7,x4),emp))))) ),
inference(forward_demodulation,[status(thm)],[f53,f844]) ).
fof(f846,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),sep(lseg(x6,x7),emp))))) ),
inference(forward_demodulation,[status(thm)],[f19,f845]) ).
fof(f847,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),sep(lseg(x4,x7),emp))))) ),
inference(forward_demodulation,[status(thm)],[f784,f846]) ).
fof(f848,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| heap(sep(lseg(x4,x7),sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),emp))))) ),
inference(forward_demodulation,[status(thm)],[f53,f847]) ).
fof(f850,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| x4 = x7
| x4 = x7 ),
inference(resolution,[status(thm)],[f848,f28]) ).
fof(f857,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ12_spl
| ~ sQ14_spl
| ~ sQ16_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f850,f308,f783,f768,f740,f668,f368,f358,f311]) ).
fof(f867,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(backward_demodulation,[status(thm)],[f672,f373]) ).
fof(f868,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))) ),
inference(forward_demodulation,[status(thm)],[f672,f867]) ).
fof(f869,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f868]) ).
fof(f870,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))
| x7 = x4 ),
inference(resolution,[status(thm)],[f869,f72]) ).
fof(f871,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| x3 = x1
| x3 = x4 ),
inference(resolution,[status(thm)],[f869,f235]) ).
fof(f872,definition,
( sQ20_spl
<=> heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f875,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| sQ20_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f870,f308,f872,f671,f368,f358,f311]) ).
fof(f876,definition,
( sQ21_spl
<=> x3 = x1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f877,plain,
( ~ sQ21_spl
| x3 = x1 ),
inference(component_clause,[status(thm)],[f876]) ).
fof(f879,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| sQ21_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f871,f668,f876,f671,f368,f358,f311]) ).
fof(f885,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(backward_demodulation,[status(thm)],[f877,f869]) ).
fof(f886,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))) ),
inference(forward_demodulation,[status(thm)],[f877,f885]) ).
fof(f887,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f20,f886]) ).
fof(f889,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| x3 = x6
| x3 = x4 ),
inference(resolution,[status(thm)],[f887,f235]) ).
fof(f894,definition,
( sQ23_spl
<=> x3 = x6 ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f895,plain,
( ~ sQ23_spl
| x3 = x6 ),
inference(component_clause,[status(thm)],[f894]) ).
fof(f897,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| sQ23_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f889,f668,f894,f876,f671,f368,f358,f311]) ).
fof(f903,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x3,x9),emp))))))) ),
inference(backward_demodulation,[status(thm)],[f895,f887]) ).
fof(f904,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x6),sep(lseg(x6,x7),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f903]) ).
fof(f905,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x3),sep(lseg(x6,x7),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f895,f904]) ).
fof(f906,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x6,x7),sep(lseg(x3,x9),emp))))))) ),
inference(forward_demodulation,[status(thm)],[f53,f905]) ).
fof(f907,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x6,x7),sep(lseg(x3,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f20,f906]) ).
fof(f908,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x6,x7),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f19,f907]) ).
fof(f909,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x7),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f895,f908]) ).
fof(f910,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x7),sep(lseg(x3,x9),emp)))))) ),
inference(forward_demodulation,[status(thm)],[f19,f909]) ).
fof(f912,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| x3 = x7
| x3 = x4 ),
inference(resolution,[status(thm)],[f910,f235]) ).
fof(f917,definition,
( sQ25_spl
<=> x3 = x7 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f918,plain,
( ~ sQ25_spl
| x3 = x7 ),
inference(component_clause,[status(thm)],[f917]) ).
fof(f920,plain,
( ~ sQ5_spl
| ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ11_spl
| ~ sQ21_spl
| ~ sQ23_spl
| sQ25_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f912,f668,f917,f894,f876,f671,f368,f358,f311]) ).
fof(f922,plain,
( ~ sQ25_spl
| ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f918,f363]) ).
fof(f923,plain,
( ~ sQ25_spl
| ~ sQ6_spl ),
inference(contradiction_clause,[status(thm)],[f922]) ).
fof(f924,plain,
$false,
inference(sat_refutation,[status(thm)],[f100,f202,f314,f316,f361,f371,f488,f674,f747,f775,f790,f857,f875,f879,f897,f920,f923]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW429-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n003.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Mon Sep 21 09:53:51 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.21/5.53 % Drodi V4.1.1
% 0.21/5.89 % Refutation found
% 0.21/5.89 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.21/5.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/5.92 % Elapsed time: 0.464184 seconds
% 0.21/5.92 % CPU time: 2.799758 seconds
% 0.21/5.92 % Total memory used: 125.340 MB
% 0.21/5.92 % Net memory used: 123.773 MB
%------------------------------------------------------------------------------