%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW434-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:09:07 PM UTC 2026
% Result : Unsatisfiable 20.00s 8.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW434-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n008.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Mon Sep 21 09:53:45 UTC 2026
% 0.19/5.45 % CPUTime :
% 0.19/5.46 % Drodi V4.1.1
% 20.00/8.07 % Refutation found
% 20.00/8.07 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 20.00/8.07 % SZS output start CNFRefutation for theBenchmark
% 20.00/8.07 fof(f1,axiom,(
% 20.00/8.07 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f2,axiom,(
% 20.00/8.07 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f4,axiom,(
% 20.00/8.07 (![Y,Sigma]: (( ~ heap(sep(lseg(nil,Y),Sigma))| Y = nil ) ))),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f7,axiom,(
% 20.00/8.07 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f11,axiom,(
% 20.00/8.07 (![X,Y,Z,W,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma))))| Z = W| heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma))) ) ))),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f17,hypothesis,(
% 20.00/8.07 x9 != x14 ),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f18,hypothesis,(
% 20.00/8.07 x13 != x14 ),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f19,hypothesis,(
% 20.00/8.07 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))))))))))))) ),
% 20.00/8.07 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.00/8.07 fof(f21,plain,(
% 20.00/8.07 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f1])).
% 20.00/8.07 fof(f22,plain,(
% 20.00/8.07 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f2])).
% 20.00/8.07 fof(f24,plain,(
% 20.00/8.07 ![Y]: ((![Sigma]: ~heap(sep(lseg(nil,Y),Sigma)))|Y=nil)),
% 20.00/8.07 inference(miniscoping,[status(thm)],[f4])).
% 20.00/8.07 fof(f25,plain,(
% 20.00/8.07 ![X0,X1]: (~heap(sep(lseg(nil,X0),X1))|X0=nil)),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f24])).
% 20.00/8.07 fof(f29,plain,(
% 20.00/8.07 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 20.00/8.07 inference(miniscoping,[status(thm)],[f7])).
% 20.00/8.07 fof(f30,plain,(
% 20.00/8.07 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f29])).
% 20.00/8.07 fof(f37,plain,(
% 20.00/8.07 ![X,Z,W,Sigma]: (((![Y]: ~heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma)))))|Z=W)|heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma))))),
% 20.00/8.07 inference(miniscoping,[status(thm)],[f11])).
% 20.00/8.07 fof(f38,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X2,X3),X4))))|X2=X3|heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4))))),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f37])).
% 20.00/8.07 fof(f44,plain,(
% 20.00/8.07 ~x9=x14),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f17])).
% 20.00/8.07 fof(f45,plain,(
% 20.00/8.07 ~x13=x14),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f18])).
% 20.00/8.07 fof(f46,plain,(
% 20.00/8.07 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)))))))))))))),
% 20.00/8.07 inference(cnf_transformation,[status(thm)],[f19])).
% 20.00/8.07 fof(f55,plain,(
% 20.00/8.07 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(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(backward_demodulation,[status(thm)],[f21,f46])).
% 20.00/8.07 fof(f64,plain,(
% 20.00/8.07 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(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f55])).
% 20.00/8.07 fof(f65,plain,(
% 20.00/8.07 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(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f64])).
% 20.00/8.07 fof(f66,plain,(
% 20.00/8.07 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(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f65])).
% 20.00/8.07 fof(f67,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x12,x8),sep(lseg(x8,x14),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f66])).
% 20.00/8.07 fof(f68,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x12,x8),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f67])).
% 20.00/8.07 fof(f69,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f68])).
% 20.00/8.07 fof(f70,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x2,x12),sep(lseg(x8,x14),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f69])).
% 20.00/8.07 fof(f71,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f70])).
% 20.00/8.07 fof(f72,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x2,x12),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f71])).
% 20.00/8.07 fof(f73,plain,(
% 20.00/8.07 heap(sep(lseg(x1,x7),sep(lseg(x2,x12),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f72])).
% 20.00/8.07 fof(f74,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x2,x11),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f73])).
% 20.00/8.07 fof(f75,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x2,x11),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f74])).
% 20.00/8.07 fof(f76,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x2,x11),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f75])).
% 20.00/8.07 fof(f77,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x2,x11),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f76])).
% 20.00/8.07 fof(f78,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x2,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f77])).
% 20.00/8.07 fof(f79,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f78])).
% 20.00/8.07 fof(f80,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f79])).
% 20.00/8.07 fof(f81,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x9,x14),sep(lseg(x8,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f80])).
% 20.00/8.07 fof(f82,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f81])).
% 20.00/8.07 fof(f83,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x9,x1),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f82])).
% 20.00/8.07 fof(f84,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x9,x1),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f83])).
% 20.00/8.07 fof(f85,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x11,x13),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f84])).
% 20.00/8.07 fof(f86,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x13),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f85])).
% 20.00/8.07 fof(f87,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x13),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f86])).
% 20.00/8.07 fof(f88,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x11,x13),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f87])).
% 20.00/8.07 fof(f89,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x11,x13),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f88])).
% 20.00/8.07 fof(f90,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x13),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f89])).
% 20.00/8.07 fof(f91,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x11,x13),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f90])).
% 20.00/8.07 fof(f92,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f91])).
% 20.00/8.07 fof(f93,plain,(
% 20.00/8.07 heap(sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f92])).
% 20.00/8.07 fof(f94,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),sep(lseg(x3,x9),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f93])).
% 20.00/8.07 fof(f95,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),sep(lseg(x11,x3),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f94])).
% 20.00/8.07 fof(f96,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x11,x3),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f95])).
% 20.00/8.07 fof(f97,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x3),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f96])).
% 20.00/8.07 fof(f98,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x3),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f97])).
% 20.00/8.07 fof(f99,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x11,x3),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f98])).
% 20.00/8.07 fof(f100,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x11,x3),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f99])).
% 20.00/8.07 fof(f101,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x3),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f100])).
% 20.00/8.07 fof(f102,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x11,x3),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f101])).
% 20.00/8.07 fof(f103,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f102])).
% 20.00/8.07 fof(f104,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x11,x3),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f103])).
% 20.00/8.07 fof(f105,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f104])).
% 20.00/8.07 fof(f114,plain,(
% 20.00/8.07 ![X0]: (~heap(X0)|nil=nil)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f22,f25])).
% 20.00/8.07 fof(f117,definition,(
% 20.00/8.07 ![X0]: (sQ2_spl <=> (~heap(X0)))),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f118,plain,(
% 20.00/8.07 ![X0]: (~heap(X0)|~sQ2_spl)),
% 20.00/8.07 inference(component_clause,[status(thm)],[f117])).
% 20.00/8.07 fof(f120,definition,(
% 20.00/8.07 sQ3_spl <=> (nil=nil)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f123,plain,(
% 20.00/8.07 sQ2_spl|sQ3_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f114,f117,f120])).
% 20.00/8.07 fof(f124,plain,(
% 20.00/8.07 $false|~sQ2_spl),
% 20.00/8.07 inference(backward_subsumption_resolution,[status(thm)],[f105,f118])).
% 20.00/8.07 fof(f125,plain,(
% 20.00/8.07 ~sQ2_spl),
% 20.00/8.07 inference(contradiction_clause,[status(thm)],[f124])).
% 20.00/8.07 fof(f147,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f30])).
% 20.00/8.07 fof(f150,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f147])).
% 20.00/8.07 fof(f165,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5)))))|X1=X2|X1=X4)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f150])).
% 20.00/8.07 fof(f183,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))))|X2=X3|X2=X4)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f165])).
% 20.00/8.07 fof(f195,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X3),sep(lseg(X1,X2),X4))))|X2=X3|heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f38])).
% 20.00/8.07 fof(f198,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(X3,sep(lseg(X2,X4),X5)))))|X2=X4|heap(sep(lseg(X0,X2),sep(lseg(X2,X4),sep(X3,X5)))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f38])).
% 20.00/8.07 fof(f209,plain,(
% 20.00/8.07 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X0),X3)))|X0=X1|heap(sep(lseg(X2,X0),sep(lseg(X0,X1),X3))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f22,f195])).
% 20.00/8.07 fof(f228,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5,X6]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(X4,sep(lseg(X2,X5),X6))))))|X2=X3|X2=X5)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f183])).
% 20.00/8.07 fof(f267,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5,X6]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),sep(lseg(X3,X5),X6))))))|X3=X4|X3=X5)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f228])).
% 20.00/8.07 fof(f288,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),sep(X5,sep(lseg(X3,X6),X7)))))))|X3=X4|X3=X6)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f267])).
% 20.00/8.07 fof(f290,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X1,X3),X4))))|X1=X3|heap(sep(lseg(X0,X1),sep(lseg(X1,X3),sep(X2,X4)))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f22,f198])).
% 20.00/8.07 fof(f329,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X3,X0),X4))))|X0=X1|heap(sep(lseg(X3,X0),sep(lseg(X0,X1),sep(X2,X4)))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f209])).
% 20.00/8.07 fof(f413,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~heap(sep(X0,sep(X1,sep(X2,sep(X3,sep(lseg(X4,X5),sep(lseg(X4,X6),X7)))))))|X4=X5|X4=X6)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f288])).
% 20.00/8.07 fof(f437,plain,(
% 20.00/8.07 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~heap(sep(X0,sep(X1,sep(X2,sep(X3,sep(lseg(X4,X5),sep(X6,sep(lseg(X4,X7),X8))))))))|X4=X5|X4=X7)),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f21,f413])).
% 20.00/8.07 fof(f470,plain,(
% 20.00/8.07 ![X0,X1,X2,X3]: (~heap(sep(X0,sep(lseg(X1,X2),X3)))|X1=X2|heap(sep(lseg(X1,X1),sep(lseg(X1,X2),sep(X0,X3)))))),
% 20.00/8.07 inference(paramodulation,[status(thm)],[f22,f290])).
% 20.00/8.07 fof(f479,plain,(
% 20.00/8.07 ![X0,X1,X2,X3]: (~heap(sep(X0,sep(lseg(X1,X2),X3)))|X1=X2|heap(sep(lseg(X1,X2),sep(X0,X3))))),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f470])).
% 20.00/8.07 fof(f493,plain,(
% 20.00/8.07 x11=x13|x11=x3),
% 20.00/8.07 inference(resolution,[status(thm)],[f105,f30])).
% 20.00/8.07 fof(f494,plain,(
% 20.00/8.07 x2=x11|x2=x12),
% 20.00/8.07 inference(resolution,[status(thm)],[f105,f183])).
% 20.00/8.07 fof(f495,definition,(
% 20.00/8.07 sQ4_spl <=> (x11=x13)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f496,plain,(
% 20.00/8.07 x11=x13|~sQ4_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f495])).
% 20.00/8.07 fof(f498,definition,(
% 20.00/8.07 sQ5_spl <=> (x11=x3)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f499,plain,(
% 20.00/8.07 x11=x3|~sQ5_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f498])).
% 20.00/8.07 fof(f501,plain,(
% 20.00/8.07 sQ4_spl|sQ5_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f493,f495,f498])).
% 20.00/8.07 fof(f502,definition,(
% 20.00/8.07 sQ6_spl <=> (x2=x11)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f503,plain,(
% 20.00/8.07 x2=x11|~sQ6_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f502])).
% 20.00/8.07 fof(f505,definition,(
% 20.00/8.07 sQ7_spl <=> (x2=x12)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f506,plain,(
% 20.00/8.07 x2=x12|~sQ7_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f505])).
% 20.00/8.07 fof(f508,plain,(
% 20.00/8.07 sQ6_spl|sQ7_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f494,f502,f505])).
% 20.00/8.07 fof(f509,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(backward_demodulation,[status(thm)],[f503,f105])).
% 20.00/8.07 fof(f510,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x11,x12),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f509])).
% 20.00/8.07 fof(f511,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f510])).
% 20.00/8.07 fof(f512,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f511])).
% 20.00/8.07 fof(f513,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f503,f512])).
% 20.00/8.07 fof(f514,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f513])).
% 20.00/8.07 fof(f515,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f514])).
% 20.00/8.07 fof(f516,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f515])).
% 20.00/8.07 fof(f517,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f516])).
% 20.00/8.07 fof(f519,plain,(
% 20.00/8.07 x11=x12|x11=x3|~sQ6_spl),
% 20.00/8.07 inference(resolution,[status(thm)],[f517,f147])).
% 20.00/8.07 fof(f521,definition,(
% 20.00/8.07 sQ8_spl <=> (x11=x12)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f522,plain,(
% 20.00/8.07 x11=x12|~sQ8_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f521])).
% 20.00/8.07 fof(f525,plain,(
% 20.00/8.07 sQ8_spl|sQ5_spl|~sQ6_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f519,f521,f498,f502])).
% 20.00/8.07 fof(f527,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(backward_demodulation,[status(thm)],[f496,f517])).
% 20.00/8.07 fof(f528,plain,(
% 20.00/8.07 ~x11=x14|~sQ4_spl),
% 20.00/8.07 inference(backward_demodulation,[status(thm)],[f496,f45])).
% 20.00/8.07 fof(f529,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f496,f527])).
% 20.00/8.07 fof(f530,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f529])).
% 20.00/8.07 fof(f531,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f530])).
% 20.00/8.07 fof(f532,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f531])).
% 20.00/8.07 fof(f533,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f532])).
% 20.00/8.07 fof(f534,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f533])).
% 20.00/8.07 fof(f535,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f534])).
% 20.00/8.07 fof(f536,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f535])).
% 20.00/8.07 fof(f537,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f536])).
% 20.00/8.07 fof(f538,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f537])).
% 20.00/8.07 fof(f539,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x11,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f538])).
% 20.00/8.07 fof(f540,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f539])).
% 20.00/8.07 fof(f542,plain,(
% 20.00/8.07 x9=x1|x9=x14|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(resolution,[status(thm)],[f540,f267])).
% 20.00/8.07 fof(f543,definition,(
% 20.00/8.07 sQ9_spl <=> (x11=x8)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f544,plain,(
% 20.00/8.07 x11=x8|~sQ9_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f543])).
% 20.00/8.07 fof(f547,definition,(
% 20.00/8.07 sQ10_spl <=> (x9=x1)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f548,plain,(
% 20.00/8.07 x9=x1|~sQ10_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f547])).
% 20.00/8.07 fof(f550,definition,(
% 20.00/8.07 sQ11_spl <=> (x9=x14)),
% 20.00/8.07 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 20.00/8.07 fof(f551,plain,(
% 20.00/8.07 x9=x14|~sQ11_spl),
% 20.00/8.07 inference(component_clause,[status(thm)],[f550])).
% 20.00/8.07 fof(f553,plain,(
% 20.00/8.07 sQ10_spl|sQ11_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f542,f547,f550,f521,f495,f502])).
% 20.00/8.07 fof(f554,plain,(
% 20.00/8.07 $false|~sQ11_spl),
% 20.00/8.07 inference(forward_subsumption_resolution,[status(thm)],[f551,f44])).
% 20.00/8.07 fof(f555,plain,(
% 20.00/8.07 ~sQ11_spl),
% 20.00/8.07 inference(contradiction_clause,[status(thm)],[f554])).
% 20.00/8.07 fof(f556,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f517])).
% 20.00/8.07 fof(f557,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f556])).
% 20.00/8.07 fof(f558,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x11,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f557])).
% 20.00/8.07 fof(f559,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f558])).
% 20.00/8.07 fof(f560,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f522,f559])).
% 20.00/8.07 fof(f563,plain,(
% 20.00/8.07 x11=x3|x11=x8|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(resolution,[status(thm)],[f560,f150])).
% 20.00/8.07 fof(f566,plain,(
% 20.00/8.07 sQ5_spl|sQ9_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(split_clause,[status(thm)],[f563,f498,f543,f521,f502])).
% 20.00/8.07 fof(f567,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(backward_demodulation,[status(thm)],[f499,f560])).
% 20.00/8.07 fof(f569,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f499,f567])).
% 20.00/8.07 fof(f570,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f569])).
% 20.00/8.07 fof(f571,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f22,f570])).
% 20.00/8.07 fof(f572,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.07 inference(forward_demodulation,[status(thm)],[f21,f571])).
% 20.00/8.07 fof(f573,plain,(
% 20.00/8.07 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x11,x9),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f572])).
% 20.00/8.08 fof(f574,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x11,x9),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f573])).
% 20.00/8.08 fof(f575,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x11,x9),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f574])).
% 20.00/8.08 fof(f576,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f575])).
% 20.00/8.08 fof(f577,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x9),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f576])).
% 20.00/8.08 fof(f593,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f577])).
% 20.00/8.08 fof(f594,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f593])).
% 20.00/8.08 fof(f595,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f544,f594])).
% 20.00/8.08 fof(f596,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f595])).
% 20.00/8.08 fof(f597,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f596])).
% 20.00/8.08 fof(f598,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f597])).
% 20.00/8.08 fof(f599,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x1,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f598])).
% 20.00/8.08 fof(f600,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x1,x1),sep(lseg(x13,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f599])).
% 20.00/8.08 fof(f601,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x1),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f600])).
% 20.00/8.08 fof(f602,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f601])).
% 20.00/8.08 fof(f603,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f602])).
% 20.00/8.08 fof(f604,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x13,x11),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f603])).
% 20.00/8.08 fof(f605,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x13,x11),sep(lseg(x5,x10),sep(lseg(x11,x14),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f544,f604])).
% 20.00/8.08 fof(f606,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x13,x11),sep(lseg(x11,x14),sep(lseg(x5,x10),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f605])).
% 20.00/8.08 fof(f607,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x11,x14),sep(lseg(x13,x11),sep(lseg(x5,x10),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f606])).
% 20.00/8.08 fof(f608,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x11,x14),sep(lseg(x1,x14),sep(lseg(x13,x11),sep(lseg(x5,x10),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f607])).
% 20.00/8.08 fof(f609,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x13,x11),sep(lseg(x5,x10),emp))))))))|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f608])).
% 20.00/8.08 fof(f611,plain,(
% 20.00/8.08 x11=x1|x11=x14|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f609,f147])).
% 20.00/8.08 fof(f614,definition,(
% 20.00/8.08 sQ12_spl <=> (x11=x1)),
% 20.00/8.08 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 20.00/8.08 fof(f615,plain,(
% 20.00/8.08 x11=x1|~sQ12_spl),
% 20.00/8.08 inference(component_clause,[status(thm)],[f614])).
% 20.00/8.08 fof(f618,definition,(
% 20.00/8.08 sQ13_spl <=> (x11=x14)),
% 20.00/8.08 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 20.00/8.08 fof(f619,plain,(
% 20.00/8.08 x11=x14|~sQ13_spl),
% 20.00/8.08 inference(component_clause,[status(thm)],[f618])).
% 20.00/8.08 fof(f621,plain,(
% 20.00/8.08 sQ12_spl|sQ13_spl|~sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f611,f614,f618,f543,f547,f498,f521,f502])).
% 20.00/8.08 fof(f623,definition,(
% 20.00/8.08 sQ14_spl <=> (x1=x7)),
% 20.00/8.08 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 20.00/8.08 fof(f624,plain,(
% 20.00/8.08 x1=x7|~sQ14_spl),
% 20.00/8.08 inference(component_clause,[status(thm)],[f623])).
% 20.00/8.08 fof(f626,definition,(
% 20.00/8.08 sQ15_spl <=> (x1=x14)),
% 20.00/8.08 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 20.00/8.08 fof(f627,plain,(
% 20.00/8.08 x1=x14|~sQ15_spl),
% 20.00/8.08 inference(component_clause,[status(thm)],[f626])).
% 20.00/8.08 fof(f630,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f544,f540])).
% 20.00/8.08 fof(f631,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f630])).
% 20.00/8.08 fof(f632,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f631])).
% 20.00/8.08 fof(f633,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f632])).
% 20.00/8.08 fof(f634,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x1),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f633])).
% 20.00/8.08 fof(f635,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f634])).
% 20.00/8.08 fof(f636,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f635])).
% 20.00/8.08 fof(f637,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x1),sep(lseg(x8,x14),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f636])).
% 20.00/8.08 fof(f638,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x1),sep(lseg(x11,x14),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f544,f637])).
% 20.00/8.08 fof(f639,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x14),sep(lseg(x3,x1),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f638])).
% 20.00/8.08 fof(f640,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x11,x14),sep(lseg(x5,x10),sep(lseg(x3,x1),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f639])).
% 20.00/8.08 fof(f641,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x11,x14),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x1),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f640])).
% 20.00/8.08 fof(f642,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x1),emp)))))))|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f641])).
% 20.00/8.08 fof(f664,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),X4))))|X2=X3|heap(sep(lseg(X2,X3),sep(X0,sep(X1,X4)))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f479])).
% 20.00/8.08 fof(f667,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),X4))))|X2=X3|heap(sep(lseg(X2,X3),sep(X1,sep(X0,X4)))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f664])).
% 20.00/8.08 fof(f673,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),X5)))))|X3=X4|heap(sep(lseg(X3,X4),sep(X0,sep(X1,sep(X2,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f664])).
% 20.00/8.08 fof(f681,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,X4))))|X1=X2|heap(sep(lseg(X1,X2),sep(X3,sep(X0,X4)))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f667])).
% 20.00/8.08 fof(f689,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(X3,X4))))|X0=X1|heap(sep(lseg(X0,X1),sep(X3,sep(X2,X4)))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f681])).
% 20.00/8.08 fof(f695,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,X5)))))|X1=X2|heap(sep(lseg(X1,X2),sep(X4,sep(X0,sep(X3,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f681])).
% 20.00/8.08 fof(f705,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(lseg(X0,X1),sep(X2,sep(X3,sep(X4,X5)))))|X0=X1|heap(sep(lseg(X0,X1),sep(X4,sep(X2,sep(X3,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f689])).
% 20.00/8.08 fof(f830,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~heap(sep(X0,sep(X1,sep(X2,sep(X3,sep(X4,sep(lseg(X5,X6),sep(lseg(X5,X7),X8))))))))|X5=X6|X5=X7)),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f437])).
% 20.00/8.08 fof(f1031,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X3,X1),X4))))|X1=X2|heap(sep(lseg(X3,X1),sep(lseg(X1,X2),sep(X0,X4)))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f329])).
% 20.00/8.08 fof(f1071,plain,(
% 20.00/8.08 ~x11=x14|~sQ4_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f496,f45])).
% 20.00/8.08 fof(f1072,plain,(
% 20.00/8.08 ~x11=x1|~sQ15_spl|~sQ4_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f627,f528])).
% 20.00/8.08 fof(f1073,plain,(
% 20.00/8.08 $false|~sQ15_spl|~sQ4_spl|~sQ12_spl),
% 20.00/8.08 inference(forward_subsumption_resolution,[status(thm)],[f615,f1072])).
% 20.00/8.08 fof(f1074,plain,(
% 20.00/8.08 ~sQ15_spl|~sQ4_spl|~sQ12_spl),
% 20.00/8.08 inference(contradiction_clause,[status(thm)],[f1073])).
% 20.00/8.08 fof(f1075,plain,(
% 20.00/8.08 x11=x3|x11=x14|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f642,f30])).
% 20.00/8.08 fof(f1079,plain,(
% 20.00/8.08 x1=x7|x1=x14|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f642,f183])).
% 20.00/8.08 fof(f1082,plain,(
% 20.00/8.08 sQ5_spl|sQ13_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1075,f498,f618,f547,f543,f521,f495,f502])).
% 20.00/8.08 fof(f1095,plain,(
% 20.00/8.08 sQ14_spl|sQ15_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1079,f623,f626,f547,f543,f521,f495,f502])).
% 20.00/8.08 fof(f1124,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x1),emp)))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(backward_demodulation,[status(thm)],[f499,f642])).
% 20.00/8.08 fof(f1125,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x1),emp)))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f499,f1124])).
% 20.00/8.08 fof(f1126,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x1),emp))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1125])).
% 20.00/8.08 fof(f1127,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x11,x1),sep(lseg(x5,x10),emp))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1126])).
% 20.00/8.08 fof(f1128,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x11,x1),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1127])).
% 20.00/8.08 fof(f1129,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x11,x1),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1128])).
% 20.00/8.08 fof(f1130,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1129])).
% 20.00/8.08 fof(f1318,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),X5)))))|X3=X4|heap(sep(lseg(X3,X4),sep(X0,sep(X2,sep(X1,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f673])).
% 20.00/8.08 fof(f1440,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(lseg(X0,X1),sep(X2,sep(X3,sep(X4,X5)))))|X0=X1|heap(sep(lseg(X0,X1),sep(X4,sep(X3,sep(X2,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f705])).
% 20.00/8.08 fof(f1600,plain,(
% 20.00/8.08 x11=x7|~sQ12_spl|~sQ14_spl),
% 20.00/8.08 inference(backward_demodulation,[status(thm)],[f615,f624])).
% 20.00/8.08 fof(f1602,plain,(
% 20.00/8.08 x9=x11|~sQ12_spl|~sQ10_spl),
% 20.00/8.08 inference(backward_demodulation,[status(thm)],[f615,f548])).
% 20.00/8.08 fof(f1603,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f615,f1130])).
% 20.00/8.08 fof(f1604,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1603])).
% 20.00/8.08 fof(f1605,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x14),sep(lseg(x11,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f615,f1604])).
% 20.00/8.08 fof(f1606,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x7),sep(lseg(x11,x14),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1605])).
% 20.00/8.08 fof(f1607,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x7),sep(lseg(x11,x14),sep(lseg(x11,x14),sep(lseg(x5,x10),emp)))))|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f615,f1606])).
% 20.00/8.08 fof(f1612,plain,(
% 20.00/8.08 x11=x14|x11=x14|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f1607,f150])).
% 20.00/8.08 fof(f1620,definition,(
% 20.00/8.08 sQ30_spl <=> (x11=x7)),
% 20.00/8.08 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 20.00/8.08 fof(f1621,plain,(
% 20.00/8.08 x11=x7|~sQ30_spl),
% 20.00/8.08 inference(component_clause,[status(thm)],[f1620])).
% 20.00/8.08 fof(f1633,plain,(
% 20.00/8.08 sQ13_spl|~sQ12_spl|~sQ5_spl|~sQ10_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1612,f618,f614,f498,f547,f543,f521,f495,f502])).
% 20.00/8.08 fof(f1659,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f496,f560])).
% 20.00/8.08 fof(f1660,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x3),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1659])).
% 20.00/8.08 fof(f1661,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f499,f1660])).
% 20.00/8.08 fof(f1662,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1661])).
% 20.00/8.08 fof(f1663,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x11,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f496,f1662])).
% 20.00/8.08 fof(f1664,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1663])).
% 20.00/8.08 fof(f1665,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1664])).
% 20.00/8.08 fof(f1666,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1665])).
% 20.00/8.08 fof(f1667,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f499,f1666])).
% 20.00/8.08 fof(f1668,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1667])).
% 20.00/8.08 fof(f1669,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x11,x9),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1668])).
% 20.00/8.08 fof(f1670,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x11,x9),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1669])).
% 20.00/8.08 fof(f1671,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1670])).
% 20.00/8.08 fof(f1672,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x9),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1671])).
% 20.00/8.08 fof(f1681,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f496,f594])).
% 20.00/8.08 fof(f1682,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1681])).
% 20.00/8.08 fof(f1683,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x13,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1682])).
% 20.00/8.08 fof(f1684,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x11,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f496,f1683])).
% 20.00/8.08 fof(f1685,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1684])).
% 20.00/8.08 fof(f1686,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1685])).
% 20.00/8.08 fof(f1687,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x11),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1686])).
% 20.00/8.08 fof(f1688,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1687])).
% 20.00/8.08 fof(f1689,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f1672])).
% 20.00/8.08 fof(f1690,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x1,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f1689])).
% 20.00/8.08 fof(f1691,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x1),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1690])).
% 20.00/8.08 fof(f1692,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f22,f1691])).
% 20.00/8.08 fof(f1693,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f548,f1692])).
% 20.00/8.08 fof(f1694,plain,(
% 20.00/8.08 x11=x1|x11=x8|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f1693,f30])).
% 20.00/8.08 fof(f1702,plain,(
% 20.00/8.08 x1=x7|x1=x14|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f1693,f183])).
% 20.00/8.08 fof(f1707,plain,(
% 20.00/8.08 sQ12_spl|sQ9_spl|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1694,f614,f543,f547,f498,f495,f521,f502])).
% 20.00/8.08 fof(f1730,plain,(
% 20.00/8.08 sQ14_spl|sQ15_spl|~sQ10_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1702,f623,f626,f547,f498,f495,f521,f502])).
% 20.00/8.08 fof(f1770,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f1600,f1688])).
% 20.00/8.08 fof(f1771,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x11),sep(lseg(x11,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f1602,f1770])).
% 20.00/8.08 fof(f1772,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x11,x1),sep(lseg(x1,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1771])).
% 20.00/8.08 fof(f1773,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1772])).
% 20.00/8.08 fof(f1774,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x1,x11),sep(lseg(x11,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f1602,f1773])).
% 20.00/8.08 fof(f1775,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x1),sep(lseg(x11,x1),sep(lseg(x11,x8),sep(lseg(x11,x14),sep(lseg(x1,x11),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f21,f1774])).
% 20.00/8.08 fof(f1787,plain,(
% 20.00/8.08 x11=x8|x11=x14|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(resolution,[status(thm)],[f1775,f183])).
% 20.00/8.08 fof(f1815,plain,(
% 20.00/8.08 sQ9_spl|sQ13_spl|~sQ12_spl|~sQ14_spl|~sQ4_spl|~sQ10_spl|~sQ5_spl|~sQ8_spl|~sQ6_spl),
% 20.00/8.08 inference(split_clause,[status(thm)],[f1787,f543,f618,f614,f623,f495,f547,f498,f521,f502])).
% 20.00/8.08 fof(f1832,plain,(
% 20.00/8.08 $false|~sQ4_spl|~sQ13_spl),
% 20.00/8.08 inference(forward_subsumption_resolution,[status(thm)],[f619,f1071])).
% 20.00/8.08 fof(f1833,plain,(
% 20.00/8.08 ~sQ4_spl|~sQ13_spl),
% 20.00/8.08 inference(contradiction_clause,[status(thm)],[f1832])).
% 20.00/8.08 fof(f1883,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(X4,X5)))))|X2=X3|heap(sep(lseg(X2,X3),sep(X0,sep(X4,sep(X1,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f1318])).
% 20.00/8.08 fof(f1935,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,X5)))))|X1=X2|heap(sep(lseg(X1,X2),sep(X4,sep(X3,sep(X0,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f1440])).
% 20.00/8.08 fof(f1968,plain,(
% 20.00/8.08 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,X5)))))|X1=X2|heap(sep(lseg(X1,X2),sep(X0,sep(X4,sep(X3,X5))))))),
% 20.00/8.08 inference(paramodulation,[status(thm)],[f21,f1883])).
% 20.00/8.08 fof(f2231,plain,(
% 20.00/8.08 heap(sep(lseg(x11,x13),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ30_spl),
% 20.00/8.08 inference(forward_demodulation,[status(thm)],[f1621,f105])).
% 20.00/8.09 fof(f2237,plain,(
% 20.00/8.09 x11=x3|heap(sep(lseg(x2,x11),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ30_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2231,f1031])).
% 20.00/8.09 fof(f2238,plain,(
% 20.00/8.09 x11=x3|heap(sep(lseg(x11,x3),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ30_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2231,f695])).
% 20.00/8.09 fof(f2239,plain,(
% 20.00/8.09 x11=x3|heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ30_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2231,f681])).
% 20.00/8.09 fof(f2240,plain,(
% 20.00/8.09 x11=x3|heap(sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ30_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2231,f479])).
% 20.00/8.09 fof(f2269,definition,(
% 20.00/8.09 sQ58_spl <=> (heap(sep(lseg(x2,x11),sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2272,plain,(
% 20.00/8.09 sQ5_spl|sQ58_spl|~sQ30_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2237,f498,f2269,f1620])).
% 20.00/8.09 fof(f2273,definition,(
% 20.00/8.09 sQ59_spl <=> (heap(sep(lseg(x11,x3),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2276,plain,(
% 20.00/8.09 sQ5_spl|sQ59_spl|~sQ30_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2238,f498,f2273,f1620])).
% 20.00/8.09 fof(f2277,definition,(
% 20.00/8.09 sQ60_spl <=> (heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2280,plain,(
% 20.00/8.09 sQ5_spl|sQ60_spl|~sQ30_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2239,f498,f2277,f1620])).
% 20.00/8.09 fof(f2281,definition,(
% 20.00/8.09 sQ61_spl <=> (heap(sep(lseg(x11,x3),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2284,plain,(
% 20.00/8.09 sQ5_spl|sQ61_spl|~sQ30_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2240,f498,f2281,f1620])).
% 20.00/8.09 fof(f2324,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f517])).
% 20.00/8.09 fof(f2325,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2324])).
% 20.00/8.09 fof(f2326,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2325])).
% 20.00/8.09 fof(f2327,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f2326])).
% 20.00/8.09 fof(f2328,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2327])).
% 20.00/8.09 fof(f2329,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2328])).
% 20.00/8.09 fof(f2330,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f2329])).
% 20.00/8.09 fof(f2331,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x11,x12),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2330])).
% 20.00/8.09 fof(f2332,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2331])).
% 20.00/8.09 fof(f2333,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f2332])).
% 20.00/8.09 fof(f2334,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2333])).
% 20.00/8.09 fof(f2335,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x11,x9),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2334])).
% 20.00/8.09 fof(f2336,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x9),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2335])).
% 20.00/8.09 fof(f2337,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x11,x9),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2336])).
% 20.00/8.09 fof(f2338,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x12),sep(lseg(x11,x9),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2337])).
% 20.00/8.09 fof(f2339,plain,(
% 20.00/8.09 x11=x12|x11=x12|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2338,f30])).
% 20.00/8.09 fof(f2359,plain,(
% 20.00/8.09 sQ8_spl|~sQ5_spl|~sQ4_spl|~sQ6_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2339,f521,f498,f495,f502])).
% 20.00/8.09 fof(f2360,definition,(
% 20.00/8.09 sQ70_spl <=> (x11=x9)),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2361,plain,(
% 20.00/8.09 x11=x9|~sQ70_spl),
% 20.00/8.09 inference(component_clause,[status(thm)],[f2360])).
% 20.00/8.09 fof(f2413,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f105])).
% 20.00/8.09 fof(f2414,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2413])).
% 20.00/8.09 fof(f2415,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x2),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f2414])).
% 20.00/8.09 fof(f2416,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2415])).
% 20.00/8.09 fof(f2417,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x2,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f2416])).
% 20.00/8.09 fof(f2418,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2417])).
% 20.00/8.09 fof(f2419,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f2418])).
% 20.00/8.09 fof(f2420,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x11,x12),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2419])).
% 20.00/8.09 fof(f2421,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x11,x12),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2420])).
% 20.00/8.09 fof(f2422,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x11,x12),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2421])).
% 20.00/8.09 fof(f2423,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2422])).
% 20.00/8.09 fof(f2424,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f2423])).
% 20.00/8.09 fof(f2426,plain,(
% 20.00/8.09 x11=x2|x11=x3|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2424,f30])).
% 20.00/8.09 fof(f2438,plain,(
% 20.00/8.09 x2=x11|x2=x8|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2424,f183])).
% 20.00/8.09 fof(f2449,plain,(
% 20.00/8.09 x9=x1|x9=x14|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f2424,f830])).
% 20.00/8.09 fof(f2454,plain,(
% 20.00/8.09 sQ6_spl|sQ5_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2426,f502,f498,f505,f495])).
% 20.00/8.09 fof(f2455,definition,(
% 20.00/8.09 sQ82_spl <=> (x2=x8)),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f2456,plain,(
% 20.00/8.09 x2=x8|~sQ82_spl),
% 20.00/8.09 inference(component_clause,[status(thm)],[f2455])).
% 20.00/8.09 fof(f2496,plain,(
% 20.00/8.09 sQ6_spl|sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2438,f502,f2455,f505,f495])).
% 20.00/8.09 fof(f2531,plain,(
% 20.00/8.09 sQ10_spl|sQ11_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f2449,f547,f550,f505,f495])).
% 20.00/8.09 fof(f2583,plain,(
% 20.00/8.09 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,X5)))))|X1=X2|heap(sep(lseg(X1,X2),sep(X3,sep(X4,sep(X0,X5))))))),
% 20.00/8.09 inference(paramodulation,[status(thm)],[f21,f1935])).
% 20.00/8.09 fof(f2978,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x2,x14),emp)))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(backward_demodulation,[status(thm)],[f2456,f2424])).
% 20.00/8.09 fof(f2981,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x2),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x2,x14),emp)))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f2456,f2978])).
% 20.00/8.09 fof(f2982,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x2,x14),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2981])).
% 20.00/8.09 fof(f2983,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x2,x14),sep(lseg(x3,x9),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2982])).
% 20.00/8.09 fof(f2984,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x2,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2983])).
% 20.00/8.09 fof(f2985,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x2,x14),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2984])).
% 20.00/8.09 fof(f2986,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x2,x14),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2985])).
% 20.00/8.09 fof(f2987,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2986])).
% 20.00/8.09 fof(f2990,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f2987])).
% 20.00/8.09 fof(f2991,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))))|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2990])).
% 20.00/8.09 fof(f2992,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp)))))))))|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2991])).
% 20.00/8.09 fof(f2993,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp)))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f2992])).
% 20.00/8.09 fof(f2994,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x1),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp)))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2993])).
% 20.00/8.09 fof(f2995,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f2994])).
% 20.00/8.09 fof(f2996,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f2995])).
% 20.00/8.09 fof(f2997,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f2996])).
% 20.00/8.09 fof(f2998,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2997])).
% 20.00/8.09 fof(f2999,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x11,x9),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2998])).
% 20.00/8.09 fof(f3000,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x11,x9),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f2999])).
% 20.00/8.09 fof(f3001,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x11,x9),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3000])).
% 20.00/8.09 fof(f3002,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3001])).
% 20.00/8.09 fof(f3003,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x7),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f3002])).
% 20.00/8.09 fof(f3005,plain,(
% 20.00/8.09 x11=x2|x11=x1|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3003,f30])).
% 20.00/8.09 fof(f3023,plain,(
% 20.00/8.09 x2=x11|x2=x14|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3003,f183])).
% 20.00/8.09 fof(f3036,plain,(
% 20.00/8.09 x1=x7|x1=x14|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3003,f413])).
% 20.00/8.09 fof(f3041,plain,(
% 20.00/8.09 sQ6_spl|sQ12_spl|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3005,f502,f614,f547,f498,f2455,f505,f495])).
% 20.00/8.09 fof(f3042,definition,(
% 20.00/8.09 sQ108_spl <=> (x2=x14)),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3043,plain,(
% 20.00/8.09 x2=x14|~sQ108_spl),
% 20.00/8.09 inference(component_clause,[status(thm)],[f3042])).
% 20.00/8.09 fof(f3104,plain,(
% 20.00/8.09 sQ6_spl|sQ108_spl|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3023,f502,f3042,f547,f498,f2455,f505,f495])).
% 20.00/8.09 fof(f3147,plain,(
% 20.00/8.09 sQ14_spl|sQ15_spl|~sQ10_spl|~sQ5_spl|~sQ82_spl|~sQ7_spl|~sQ4_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3036,f623,f626,f547,f498,f2455,f505,f495])).
% 20.00/8.09 fof(f3178,plain,(
% 20.00/8.09 sQ30_spl|~sQ12_spl|~sQ14_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f1600,f1620,f614,f623])).
% 20.00/8.09 fof(f3298,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f2231])).
% 20.00/8.09 fof(f3299,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x3),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3298])).
% 20.00/8.09 fof(f3300,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f3299])).
% 20.00/8.09 fof(f3301,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3300])).
% 20.00/8.09 fof(f3302,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x2,x2),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f3301])).
% 20.00/8.09 fof(f3303,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3302])).
% 20.00/8.09 fof(f3304,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x2,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f3303])).
% 20.00/8.09 fof(f3305,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x2,x8),sep(lseg(x1,x11),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3304])).
% 20.00/8.09 fof(f3306,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x2,x2),sep(lseg(x1,x11),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f2456,f3305])).
% 20.00/8.09 fof(f3307,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3306])).
% 20.00/8.09 fof(f3308,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x11,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f496,f3307])).
% 20.00/8.09 fof(f3309,plain,(
% 20.00/8.09 heap(sep(lseg(x2,x11),sep(lseg(x11,x12),sep(lseg(x1,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3308])).
% 20.00/8.09 fof(f3310,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x12),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3309])).
% 20.00/8.09 fof(f3311,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f506,f3310])).
% 20.00/8.09 fof(f3312,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f3311])).
% 20.00/8.09 fof(f3313,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3312])).
% 20.00/8.09 fof(f3314,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f3313])).
% 20.00/8.09 fof(f3315,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f3314])).
% 20.00/8.09 fof(f3316,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3315])).
% 20.00/8.09 fof(f3317,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x11,x9),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3316])).
% 20.00/8.09 fof(f3318,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x11,x9),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3317])).
% 20.00/8.09 fof(f3319,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3318])).
% 20.00/8.09 fof(f3320,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f548,f3319])).
% 20.00/8.09 fof(f3321,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),sep(lseg(x2,x14),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f2456,f3320])).
% 20.00/8.09 fof(f3322,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x2,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3321])).
% 20.00/8.09 fof(f3323,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x2,x14),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3322])).
% 20.00/8.09 fof(f3324,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3323])).
% 20.00/8.09 fof(f3332,plain,(
% 20.00/8.09 x2=x11|~sQ8_spl|~sQ7_spl),
% 20.00/8.09 inference(backward_demodulation,[status(thm)],[f522,f506])).
% 20.00/8.09 fof(f3333,plain,(
% 20.00/8.09 sQ6_spl|~sQ8_spl|~sQ7_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3332,f502,f521,f505])).
% 20.00/8.09 fof(f3714,plain,(
% 20.00/8.09 x1=x11|~sQ30_spl|~sQ14_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f1621,f624])).
% 20.00/8.09 fof(f3716,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f3714,f3324])).
% 20.00/8.09 fof(f3717,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))))|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3716])).
% 20.00/8.09 fof(f3718,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x14),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))))|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3717])).
% 20.00/8.09 fof(f3719,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x2,x2),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f3043,f3718])).
% 20.00/8.09 fof(f3720,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3719])).
% 20.00/8.09 fof(f3721,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x11,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f3714,f3720])).
% 20.00/8.09 fof(f3722,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3721])).
% 20.00/8.09 fof(f3723,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp))))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3722])).
% 20.00/8.09 fof(f3724,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x1,x14),sep(lseg(x5,x10),emp)))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3723])).
% 20.00/8.09 fof(f3725,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x11,x14),sep(lseg(x5,x10),emp)))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f3714,f3724])).
% 20.00/8.09 fof(f3726,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x14),sep(lseg(x2,x11),sep(lseg(x5,x10),emp)))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3725])).
% 20.00/8.09 fof(f3727,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x2),sep(lseg(x11,x2),sep(lseg(x2,x11),sep(lseg(x5,x10),emp)))))|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f3043,f3726])).
% 20.00/8.09 fof(f3730,plain,(
% 20.00/8.09 x11=x2|x11=x2|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3727,f30])).
% 20.00/8.09 fof(f3763,plain,(
% 20.00/8.09 sQ6_spl|~sQ108_spl|~sQ14_spl|~sQ10_spl|~sQ82_spl|~sQ7_spl|~sQ5_spl|~sQ4_spl|~sQ30_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3730,f502,f3042,f623,f547,f2455,f505,f498,f495,f1620])).
% 20.00/8.09 fof(f3827,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f105])).
% 20.00/8.09 fof(f3828,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp)))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3827])).
% 20.00/8.09 fof(f3829,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x3,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f22,f3828])).
% 20.00/8.09 fof(f3830,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x11,x9),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f499,f3829])).
% 20.00/8.09 fof(f3831,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x11,x9),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3830])).
% 20.00/8.09 fof(f3832,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x11,x9),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3831])).
% 20.00/8.09 fof(f3833,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x11,x9),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3832])).
% 20.00/8.09 fof(f3834,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x9),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3833])).
% 20.00/8.09 fof(f3835,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x11,x9),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3834])).
% 20.00/8.09 fof(f3836,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x9),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3835])).
% 20.00/8.09 fof(f3837,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3836])).
% 20.00/8.09 fof(f3838,plain,(
% 20.00/8.09 heap(sep(lseg(x11,x13),sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f21,f3837])).
% 20.00/8.09 fof(f3869,plain,(
% 20.00/8.09 x11=x13|x11=x9|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f30])).
% 20.00/8.09 fof(f3876,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x2,x11),sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f1031])).
% 20.00/8.09 fof(f3877,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f2583])).
% 20.00/8.09 fof(f3878,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f1968])).
% 20.00/8.09 fof(f3879,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f1935])).
% 20.00/8.09 fof(f3880,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f695])).
% 20.00/8.09 fof(f3881,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f681])).
% 20.00/8.09 fof(f3882,plain,(
% 20.00/8.09 x11=x9|heap(sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ5_spl),
% 20.00/8.09 inference(resolution,[status(thm)],[f3838,f479])).
% 20.00/8.09 fof(f3896,plain,(
% 20.00/8.09 sQ4_spl|sQ70_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3869,f495,f2360,f498])).
% 20.00/8.09 fof(f3921,definition,(
% 20.00/8.09 sQ152_spl <=> (heap(sep(lseg(x2,x11),sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3924,plain,(
% 20.00/8.09 sQ70_spl|sQ152_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3876,f2360,f3921,f498])).
% 20.00/8.09 fof(f3925,definition,(
% 20.00/8.09 sQ153_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3928,plain,(
% 20.00/8.09 sQ70_spl|sQ153_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3877,f2360,f3925,f498])).
% 20.00/8.09 fof(f3929,definition,(
% 20.00/8.09 sQ154_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3932,plain,(
% 20.00/8.09 sQ70_spl|sQ154_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3878,f2360,f3929,f498])).
% 20.00/8.09 fof(f3933,definition,(
% 20.00/8.09 sQ155_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3936,plain,(
% 20.00/8.09 sQ70_spl|sQ155_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3879,f2360,f3933,f498])).
% 20.00/8.09 fof(f3937,definition,(
% 20.00/8.09 sQ156_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3940,plain,(
% 20.00/8.09 sQ70_spl|sQ156_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3880,f2360,f3937,f498])).
% 20.00/8.09 fof(f3941,definition,(
% 20.00/8.09 sQ157_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x2,x11),sep(lseg(x11,x13),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3944,plain,(
% 20.00/8.09 sQ70_spl|sQ157_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3881,f2360,f3941,f498])).
% 20.00/8.09 fof(f3945,definition,(
% 20.00/8.09 sQ158_spl <=> (heap(sep(lseg(x11,x9),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))))),
% 20.00/8.09 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 20.00/8.09 fof(f3948,plain,(
% 20.00/8.09 sQ70_spl|sQ158_spl|~sQ5_spl),
% 20.00/8.09 inference(split_clause,[status(thm)],[f3882,f2360,f3945,f498])).
% 20.00/8.09 fof(f4323,plain,(
% 20.00/8.09 ~x11=x14|~sQ70_spl),
% 20.00/8.09 inference(forward_demodulation,[status(thm)],[f2361,f44])).
% 20.00/8.10 fof(f4755,plain,(
% 20.00/8.10 $false|~sQ70_spl|~sQ13_spl),
% 20.00/8.10 inference(forward_subsumption_resolution,[status(thm)],[f619,f4323])).
% 20.00/8.10 fof(f4756,plain,(
% 20.00/8.10 ~sQ70_spl|~sQ13_spl),
% 20.00/8.10 inference(contradiction_clause,[status(thm)],[f4755])).
% 20.00/8.10 fof(f4850,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x11,x11),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f2361,f3838])).
% 20.00/8.10 fof(f4851,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x11),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp))))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4850])).
% 20.00/8.10 fof(f4852,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f22,f4851])).
% 20.00/8.10 fof(f4853,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x11,x1),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f2361,f4852])).
% 20.00/8.10 fof(f4854,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x1),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4853])).
% 20.00/8.10 fof(f4855,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x11,x1),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4854])).
% 20.00/8.10 fof(f4856,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x1),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4855])).
% 20.00/8.10 fof(f4857,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x11,x1),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4856])).
% 20.00/8.10 fof(f4858,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x13),sep(lseg(x11,x1),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4857])).
% 20.00/8.10 fof(f4859,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x9,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4858])).
% 20.00/8.10 fof(f4860,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x11,x14),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f2361,f4859])).
% 20.00/8.10 fof(f4861,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x11,x14),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4860])).
% 20.00/8.10 fof(f4862,plain,(
% 20.00/8.10 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x11,x14),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.10 inference(forward_demodulation,[status(thm)],[f21,f4861])).
% 20.00/8.11 fof(f4863,plain,(
% 20.00/8.11 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x11,x14),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(forward_demodulation,[status(thm)],[f21,f4862])).
% 20.00/8.11 fof(f4864,plain,(
% 20.00/8.11 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x2,x11),sep(lseg(x11,x14),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(forward_demodulation,[status(thm)],[f21,f4863])).
% 20.00/8.11 fof(f4865,plain,(
% 20.00/8.11 heap(sep(lseg(x11,x1),sep(lseg(x11,x13),sep(lseg(x11,x14),sep(lseg(x2,x11),sep(lseg(x2,x12),sep(lseg(x1,x7),sep(lseg(x12,x8),sep(lseg(x13,x12),sep(lseg(x5,x10),sep(lseg(x8,x14),emp)))))))))))|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(forward_demodulation,[status(thm)],[f21,f4864])).
% 20.00/8.11 fof(f4867,plain,(
% 20.00/8.11 x11=x1|x11=x14|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(resolution,[status(thm)],[f4865,f147])).
% 20.00/8.11 fof(f4874,plain,(
% 20.00/8.11 x11=x13|x11=x14|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(resolution,[status(thm)],[f4865,f150])).
% 20.00/8.11 fof(f4895,plain,(
% 20.00/8.11 sQ12_spl|sQ13_spl|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(split_clause,[status(thm)],[f4867,f614,f618,f2360,f498])).
% 20.00/8.11 fof(f4920,plain,(
% 20.00/8.11 sQ4_spl|sQ13_spl|~sQ70_spl|~sQ5_spl),
% 20.00/8.11 inference(split_clause,[status(thm)],[f4874,f495,f618,f2360,f498])).
% 20.00/8.11 fof(f4991,plain,(
% 20.00/8.11 $false),
% 20.00/8.11 inference(sat_refutation,[status(thm)],[f123,f125,f501,f508,f525,f553,f555,f566,f621,f1074,f1082,f1095,f1633,f1707,f1730,f1815,f1833,f2272,f2276,f2280,f2284,f2359,f2454,f2496,f2531,f3041,f3104,f3147,f3178,f3333,f3763,f3896,f3924,f3928,f3932,f3936,f3940,f3944,f3948,f4756,f4895,f4920])).
% 20.00/8.11 % SZS output end CNFRefutation for theBenchmark.p
% 3.14/8.12 % Elapsed time: 2.656395 seconds
% 3.14/8.12 % CPU time: 20.648063 seconds
% 3.14/8.12 % Total memory used: 191.670 MB
% 3.14/8.12 % Net memory used: 187.401 MB
%------------------------------------------------------------------------------