%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW443-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:09:08 PM UTC 2026
% Result : Unsatisfiable 2.26s 1.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW443-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:56:17 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 2.26/1.01 % Refutation found
% 2.26/1.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.26/1.01 % SZS output start CNFRefutation for theBenchmark
% 2.26/1.01 fof(f1,axiom,(
% 2.26/1.01 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f2,axiom,(
% 2.26/1.01 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f4,axiom,(
% 2.26/1.01 (![Y,Sigma]: (( ~ heap(sep(lseg(nil,Y),Sigma))| Y = nil ) ))),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f7,axiom,(
% 2.26/1.01 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f15,hypothesis,(
% 2.26/1.01 x11 != x15 ),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f19,hypothesis,(
% 2.26/1.01 x2 != x8 ),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f24,hypothesis,(
% 2.26/1.01 x8 != x9 ),
% 2.26/1.01 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.01 fof(f34,hypothesis,(
% 2.26/1.02 heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp)))))))))))))) ),
% 2.26/1.02 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.26/1.02 fof(f36,plain,(
% 2.26/1.02 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f1])).
% 2.26/1.02 fof(f37,plain,(
% 2.26/1.02 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f2])).
% 2.26/1.02 fof(f39,plain,(
% 2.26/1.02 ![Y]: ((![Sigma]: ~heap(sep(lseg(nil,Y),Sigma)))|Y=nil)),
% 2.26/1.02 inference(miniscoping,[status(thm)],[f4])).
% 2.26/1.02 fof(f40,plain,(
% 2.26/1.02 ![X0,X1]: (~heap(sep(lseg(nil,X0),X1))|X0=nil)),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f39])).
% 2.26/1.02 fof(f44,plain,(
% 2.26/1.02 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 2.26/1.02 inference(miniscoping,[status(thm)],[f7])).
% 2.26/1.02 fof(f45,plain,(
% 2.26/1.02 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f44])).
% 2.26/1.02 fof(f57,plain,(
% 2.26/1.02 ~x11=x15),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f15])).
% 2.26/1.02 fof(f61,plain,(
% 2.26/1.02 ~x2=x8),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f19])).
% 2.26/1.02 fof(f66,plain,(
% 2.26/1.02 ~x8=x9),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f24])).
% 2.26/1.02 fof(f76,plain,(
% 2.26/1.02 heap(sep(lseg(x10,x1),sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(cnf_transformation,[status(thm)],[f34])).
% 2.26/1.02 fof(f87,plain,(
% 2.26/1.02 ![X0,X1,X2,X3]: (sep(X0,sep(X1,sep(X2,X3)))=sep(X2,sep(X0,sep(X1,X3))))),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f36,f36])).
% 2.26/1.02 fof(f97,plain,(
% 2.26/1.02 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f36,f45])).
% 2.26/1.02 fof(f125,plain,(
% 2.26/1.02 ![X0]: (~heap(X0)|nil=nil)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f37,f40])).
% 2.26/1.02 fof(f128,definition,(
% 2.26/1.02 ![X0]: (sQ2_spl <=> (~heap(X0)))),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f129,plain,(
% 2.26/1.02 ![X0]: (~heap(X0)|~sQ2_spl)),
% 2.26/1.02 inference(component_clause,[status(thm)],[f128])).
% 2.26/1.02 fof(f131,definition,(
% 2.26/1.02 sQ3_spl <=> (nil=nil)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f134,plain,(
% 2.26/1.02 sQ2_spl|sQ3_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f125,f128,f131])).
% 2.26/1.02 fof(f136,plain,(
% 2.26/1.02 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f36,f97])).
% 2.26/1.02 fof(f137,plain,(
% 2.26/1.02 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f36,f97])).
% 2.26/1.02 fof(f161,plain,(
% 2.26/1.02 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5)))))|X1=X2|X1=X4)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f36,f136])).
% 2.26/1.02 fof(f175,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f76])).
% 2.26/1.02 fof(f176,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x1,x3),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f175])).
% 2.26/1.02 fof(f177,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f176])).
% 2.26/1.02 fof(f178,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f177])).
% 2.26/1.02 fof(f179,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x2,x5),sep(lseg(x12,x13),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f178])).
% 2.26/1.02 fof(f180,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x2,x5),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f179])).
% 2.26/1.02 fof(f181,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x2,x5),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f180])).
% 2.26/1.02 fof(f182,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f181])).
% 2.26/1.02 fof(f183,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x2,x12),sep(lseg(x12,x13),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f182])).
% 2.26/1.02 fof(f184,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x2,x12),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f183])).
% 2.26/1.02 fof(f185,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x1,x3),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f184])).
% 2.26/1.02 fof(f186,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f185])).
% 2.26/1.02 fof(f187,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x2,x18),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f186])).
% 2.26/1.02 fof(f188,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x2,x18),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f187])).
% 2.26/1.02 fof(f189,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x2,x18),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f188])).
% 2.26/1.02 fof(f190,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x12),sep(lseg(x2,x18),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f189])).
% 2.26/1.02 fof(f191,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x2,x8),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f190])).
% 2.26/1.02 fof(f192,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x2,x8),sep(lseg(x12,x13),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f191])).
% 2.26/1.02 fof(f193,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x2,x8),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f192])).
% 2.26/1.02 fof(f194,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x2,x8),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f193])).
% 2.26/1.02 fof(f195,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f194])).
% 2.26/1.02 fof(f196,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x9,x5),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f195])).
% 2.26/1.02 fof(f197,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x9,x5),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f196])).
% 2.26/1.02 fof(f198,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x9,x5),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f197])).
% 2.26/1.02 fof(f199,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x9,x5),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f198])).
% 2.26/1.02 fof(f200,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x9),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f199])).
% 2.26/1.02 fof(f201,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x11,x9),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f200])).
% 2.26/1.02 fof(f202,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x11,x9),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f201])).
% 2.26/1.02 fof(f203,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x11,x9),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f202])).
% 2.26/1.02 fof(f204,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x11,x9),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f203])).
% 2.26/1.02 fof(f205,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x11,x9),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f204])).
% 2.26/1.02 fof(f206,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x9),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f205])).
% 2.26/1.02 fof(f207,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x9),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f206])).
% 2.26/1.02 fof(f208,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x11,x9),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f207])).
% 2.26/1.02 fof(f209,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x11,x9),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f208])).
% 2.26/1.02 fof(f210,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x11,x9),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f209])).
% 2.26/1.02 fof(f211,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),sep(lseg(x11,x7),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f210])).
% 2.26/1.02 fof(f212,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x11,x7),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f211])).
% 2.26/1.02 fof(f213,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x11,x7),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f212])).
% 2.26/1.02 fof(f214,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x11,x7),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f213])).
% 2.26/1.02 fof(f215,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x11,x7),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f214])).
% 2.26/1.02 fof(f216,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x11,x7),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f215])).
% 2.26/1.02 fof(f217,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x7),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f216])).
% 2.26/1.02 fof(f218,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x7),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f217])).
% 2.26/1.02 fof(f219,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x11,x7),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f218])).
% 2.26/1.02 fof(f220,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x11,x7),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f219])).
% 2.26/1.02 fof(f221,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x11,x7),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f220])).
% 2.26/1.02 fof(f222,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f221])).
% 2.26/1.02 fof(f223,plain,(
% 2.26/1.02 $false|~sQ2_spl),
% 2.26/1.02 inference(forward_subsumption_resolution,[status(thm)],[f222,f129])).
% 2.26/1.02 fof(f224,plain,(
% 2.26/1.02 ~sQ2_spl),
% 2.26/1.02 inference(contradiction_clause,[status(thm)],[f223])).
% 2.26/1.02 fof(f287,plain,(
% 2.26/1.02 x11=x9|x11=x7),
% 2.26/1.02 inference(resolution,[status(thm)],[f222,f45])).
% 2.26/1.02 fof(f288,definition,(
% 2.26/1.02 sQ4_spl <=> (x11=x9)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f289,plain,(
% 2.26/1.02 x11=x9|~sQ4_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f288])).
% 2.26/1.02 fof(f291,definition,(
% 2.26/1.02 sQ5_spl <=> (x11=x7)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f292,plain,(
% 2.26/1.02 x11=x7|~sQ5_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f291])).
% 2.26/1.02 fof(f294,plain,(
% 2.26/1.02 sQ4_spl|sQ5_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f287,f288,f291])).
% 2.26/1.02 fof(f309,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(backward_demodulation,[status(thm)],[f289,f222])).
% 2.26/1.02 fof(f310,plain,(
% 2.26/1.02 ~x8=x11|~sQ4_spl),
% 2.26/1.02 inference(backward_demodulation,[status(thm)],[f289,f66])).
% 2.26/1.02 fof(f311,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f289,f309])).
% 2.26/1.02 fof(f312,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f311])).
% 2.26/1.02 fof(f313,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x5),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f312])).
% 2.26/1.02 fof(f314,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x11,x5),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f313])).
% 2.26/1.02 fof(f315,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x11,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f314])).
% 2.26/1.02 fof(f316,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f315])).
% 2.26/1.02 fof(f317,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f316])).
% 2.26/1.02 fof(f318,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f317])).
% 2.26/1.02 fof(f319,plain,(
% 2.26/1.02 x11=x5|x11=x7|~sQ4_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f318,f45])).
% 2.26/1.02 fof(f320,definition,(
% 2.26/1.02 sQ6_spl <=> (x11=x5)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f321,plain,(
% 2.26/1.02 x11=x5|~sQ6_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f320])).
% 2.26/1.02 fof(f323,plain,(
% 2.26/1.02 sQ6_spl|sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f319,f320,f291,f288])).
% 2.26/1.02 fof(f361,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x11),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f292,f222])).
% 2.26/1.02 fof(f362,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f361])).
% 2.26/1.02 fof(f363,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f362])).
% 2.26/1.02 fof(f364,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x11,x5),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f292,f363])).
% 2.26/1.02 fof(f365,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x11,x5),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f364])).
% 2.26/1.02 fof(f366,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x11,x5),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f365])).
% 2.26/1.02 fof(f367,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x11,x5),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f366])).
% 2.26/1.02 fof(f368,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x11,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f367])).
% 2.26/1.02 fof(f369,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x5),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f368])).
% 2.26/1.02 fof(f370,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x11,x5),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f369])).
% 2.26/1.02 fof(f371,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x11,x5),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f370])).
% 2.26/1.02 fof(f372,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x11,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f371])).
% 2.26/1.02 fof(f373,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f372])).
% 2.26/1.02 fof(f374,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f373])).
% 2.26/1.02 fof(f375,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f374])).
% 2.26/1.02 fof(f376,plain,(
% 2.26/1.02 x11=x5|x11=x9|~sQ5_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f375,f45])).
% 2.26/1.02 fof(f377,plain,(
% 2.26/1.02 sQ6_spl|sQ4_spl|~sQ5_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f376,f320,f288,f291])).
% 2.26/1.02 fof(f380,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(backward_demodulation,[status(thm)],[f321,f318])).
% 2.26/1.02 fof(f384,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f380])).
% 2.26/1.02 fof(f385,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f384])).
% 2.26/1.02 fof(f386,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f385])).
% 2.26/1.02 fof(f459,plain,(
% 2.26/1.02 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))))|X2=X3|X2=X4)),
% 2.26/1.02 inference(paramodulation,[status(thm)],[f87,f137])).
% 2.26/1.02 fof(f759,plain,(
% 2.26/1.02 x2=x11|x2=x18|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f459,f386])).
% 2.26/1.02 fof(f780,definition,(
% 2.26/1.02 sQ8_spl <=> (x2=x11)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f781,plain,(
% 2.26/1.02 x2=x11|~sQ8_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f780])).
% 2.26/1.02 fof(f783,definition,(
% 2.26/1.02 sQ9_spl <=> (x2=x18)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f784,plain,(
% 2.26/1.02 x2=x18|~sQ9_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f783])).
% 2.26/1.02 fof(f786,plain,(
% 2.26/1.02 sQ8_spl|sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f759,f780,f783,f320,f288])).
% 2.26/1.02 fof(f787,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))))|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f375])).
% 2.26/1.02 fof(f788,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f787])).
% 2.26/1.02 fof(f789,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f788])).
% 2.26/1.02 fof(f790,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f789])).
% 2.26/1.02 fof(f791,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f222])).
% 2.26/1.02 fof(f792,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))))|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f791])).
% 2.26/1.02 fof(f793,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))))|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f321,f792])).
% 2.26/1.02 fof(f794,plain,(
% 2.26/1.02 x2=x11|x2=x18|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f790,f459])).
% 2.26/1.02 fof(f795,plain,(
% 2.26/1.02 sQ8_spl|sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f794,f780,f783,f320,f291])).
% 2.26/1.02 fof(f799,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f781,f793])).
% 2.26/1.02 fof(f800,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x11),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f799])).
% 2.26/1.02 fof(f801,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f800])).
% 2.26/1.02 fof(f802,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f801])).
% 2.26/1.02 fof(f803,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x11,x7),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f802])).
% 2.26/1.02 fof(f804,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x2,x18),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f803])).
% 2.26/1.02 fof(f805,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f804])).
% 2.26/1.02 fof(f806,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f805])).
% 2.26/1.02 fof(f807,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f781,f806])).
% 2.26/1.02 fof(f808,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x11,x18),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f807])).
% 2.26/1.02 fof(f809,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f808])).
% 2.26/1.02 fof(f810,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x11,x7),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f809])).
% 2.26/1.02 fof(f811,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x2,x12),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f810])).
% 2.26/1.02 fof(f812,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f811])).
% 2.26/1.02 fof(f813,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f781,f812])).
% 2.26/1.02 fof(f814,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x9),sep(lseg(x11,x8),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f813])).
% 2.26/1.02 fof(f815,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x7),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f814])).
% 2.26/1.02 fof(f816,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x11,x7),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f815])).
% 2.26/1.02 fof(f817,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x2,x12),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f816])).
% 2.26/1.02 fof(f818,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f817])).
% 2.26/1.02 fof(f819,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f818])).
% 2.26/1.02 fof(f820,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x11,x12),sep(lseg(x1,x3),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f781,f819])).
% 2.26/1.02 fof(f821,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x1,x3),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f820])).
% 2.26/1.02 fof(f822,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f821])).
% 2.26/1.02 fof(f823,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f822])).
% 2.26/1.02 fof(f824,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x10,x1),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f823])).
% 2.26/1.02 fof(f825,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x7,x11),sep(lseg(x12,x13),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f824])).
% 2.26/1.02 fof(f826,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f825])).
% 2.26/1.02 fof(f827,plain,(
% 2.26/1.02 x11=x18|x11=x8|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f826,f45])).
% 2.26/1.02 fof(f828,plain,(
% 2.26/1.02 x11=x18|x11=x9|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f826,f97])).
% 2.26/1.02 fof(f833,definition,(
% 2.26/1.02 sQ10_spl <=> (x11=x18)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f834,plain,(
% 2.26/1.02 x11=x18|~sQ10_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f833])).
% 2.26/1.02 fof(f836,definition,(
% 2.26/1.02 sQ11_spl <=> (x11=x8)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f837,plain,(
% 2.26/1.02 x11=x8|~sQ11_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f836])).
% 2.26/1.02 fof(f839,plain,(
% 2.26/1.02 sQ10_spl|sQ11_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f827,f833,f836,f780,f320])).
% 2.26/1.02 fof(f840,plain,(
% 2.26/1.02 sQ10_spl|sQ4_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f828,f833,f288,f780,f320])).
% 2.26/1.02 fof(f848,plain,(
% 2.26/1.02 $false|~sQ4_spl|~sQ11_spl),
% 2.26/1.02 inference(forward_subsumption_resolution,[status(thm)],[f837,f310])).
% 2.26/1.02 fof(f849,plain,(
% 2.26/1.02 ~sQ4_spl|~sQ11_spl),
% 2.26/1.02 inference(contradiction_clause,[status(thm)],[f848])).
% 2.26/1.02 fof(f864,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x18),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(backward_demodulation,[status(thm)],[f834,f826])).
% 2.26/1.02 fof(f868,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))))|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f834,f864])).
% 2.26/1.02 fof(f869,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x15),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f868])).
% 2.26/1.02 fof(f870,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x15),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f869])).
% 2.26/1.02 fof(f871,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x15),sep(lseg(x11,x8),sep(lseg(x11,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f870])).
% 2.26/1.02 fof(f890,definition,(
% 2.26/1.02 sQ13_spl <=> (x11=x15)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f891,plain,(
% 2.26/1.02 x11=x15|~sQ13_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f890])).
% 2.26/1.02 fof(f899,plain,(
% 2.26/1.02 $false|~sQ13_spl),
% 2.26/1.02 inference(forward_subsumption_resolution,[status(thm)],[f891,f57])).
% 2.26/1.02 fof(f900,plain,(
% 2.26/1.02 ~sQ13_spl),
% 2.26/1.02 inference(contradiction_clause,[status(thm)],[f899])).
% 2.26/1.02 fof(f926,plain,(
% 2.26/1.02 x11=x15|x11=x8|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f871,f45])).
% 2.26/1.02 fof(f927,plain,(
% 2.26/1.02 x11=x15|x11=x9|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f871,f97])).
% 2.26/1.02 fof(f932,plain,(
% 2.26/1.02 sQ13_spl|sQ11_spl|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f926,f890,f836,f833,f780,f320])).
% 2.26/1.02 fof(f933,plain,(
% 2.26/1.02 sQ13_spl|sQ4_spl|~sQ10_spl|~sQ8_spl|~sQ6_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f927,f890,f288,f833,f780,f320])).
% 2.26/1.02 fof(f966,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x15),sep(lseg(x18,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f386])).
% 2.26/1.02 fof(f967,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x2,x18),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f966])).
% 2.26/1.02 fof(f968,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f967])).
% 2.26/1.02 fof(f969,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f968])).
% 2.26/1.02 fof(f970,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f969])).
% 2.26/1.02 fof(f971,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f970])).
% 2.26/1.02 fof(f972,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f971])).
% 2.26/1.02 fof(f973,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x1,x3),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f972])).
% 2.26/1.02 fof(f974,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f973])).
% 2.26/1.02 fof(f975,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f974])).
% 2.26/1.02 fof(f976,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f975])).
% 2.26/1.02 fof(f977,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x10,x1),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f976])).
% 2.26/1.02 fof(f978,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x7,x11),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f977])).
% 2.26/1.02 fof(f979,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x7),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x11),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f978])).
% 2.26/1.02 fof(f981,plain,(
% 2.26/1.02 x18=x11|x18=x8|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f979,f161])).
% 2.26/1.02 fof(f982,plain,(
% 2.26/1.02 x18=x15|x18=x8|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f979,f459])).
% 2.26/1.02 fof(f983,definition,(
% 2.26/1.02 sQ14_spl <=> (x18=x15)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f984,plain,(
% 2.26/1.02 x18=x15|~sQ14_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f983])).
% 2.26/1.02 fof(f987,definition,(
% 2.26/1.02 sQ15_spl <=> (x18=x8)),
% 2.26/1.02 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 2.26/1.02 fof(f988,plain,(
% 2.26/1.02 x18=x8|~sQ15_spl),
% 2.26/1.02 inference(component_clause,[status(thm)],[f987])).
% 2.26/1.02 fof(f990,plain,(
% 2.26/1.02 sQ10_spl|sQ15_spl|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f981,f833,f987,f783,f320,f288])).
% 2.26/1.02 fof(f991,plain,(
% 2.26/1.02 sQ14_spl|sQ15_spl|~sQ9_spl|~sQ6_spl|~sQ4_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f982,f983,f987,f783,f320,f288])).
% 2.26/1.02 fof(f992,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x15),sep(lseg(x18,x11),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f790])).
% 2.26/1.02 fof(f993,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x2,x18),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f992])).
% 2.26/1.02 fof(f994,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f993])).
% 2.26/1.02 fof(f995,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f994])).
% 2.26/1.02 fof(f996,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f995])).
% 2.26/1.02 fof(f997,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f996])).
% 2.26/1.02 fof(f998,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x2,x8),sep(lseg(x9,x11),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f997])).
% 2.26/1.02 fof(f999,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x9,x11),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f998])).
% 2.26/1.02 fof(f1000,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f999])).
% 2.26/1.02 fof(f1001,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x1,x3),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f1000])).
% 2.26/1.02 fof(f1002,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x9,x11),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1001])).
% 2.26/1.02 fof(f1003,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1002])).
% 2.26/1.02 fof(f1004,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x10,x1),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1003])).
% 2.26/1.02 fof(f1005,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x9),sep(lseg(x18,x11),sep(lseg(x18,x15),sep(lseg(x18,x8),sep(lseg(x18,x12),sep(lseg(x9,x11),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp)))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f1004])).
% 2.26/1.02 fof(f1022,plain,(
% 2.26/1.02 x18=x11|x18=x8|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f1005,f161])).
% 2.26/1.02 fof(f1023,plain,(
% 2.26/1.02 x18=x15|x18=x8|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(resolution,[status(thm)],[f1005,f459])).
% 2.26/1.02 fof(f1025,plain,(
% 2.26/1.02 sQ10_spl|sQ15_spl|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f1022,f833,f987,f783,f320,f291])).
% 2.26/1.02 fof(f1026,plain,(
% 2.26/1.02 sQ14_spl|sQ15_spl|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 2.26/1.02 inference(split_clause,[status(thm)],[f1023,f983,f987,f783,f320,f291])).
% 2.26/1.02 fof(f1029,plain,(
% 2.26/1.02 ~x18=x8|~sQ9_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f784,f61])).
% 2.26/1.02 fof(f1035,plain,(
% 2.26/1.02 $false|~sQ9_spl|~sQ15_spl),
% 2.26/1.02 inference(forward_subsumption_resolution,[status(thm)],[f988,f1029])).
% 2.26/1.02 fof(f1036,plain,(
% 2.26/1.02 ~sQ9_spl|~sQ15_spl),
% 2.26/1.02 inference(contradiction_clause,[status(thm)],[f1035])).
% 2.26/1.02 fof(f1083,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x11,x11),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f292,f318])).
% 2.26/1.02 fof(f1084,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x11),sep(lseg(x18,x15),sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp)))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1083])).
% 2.26/1.02 fof(f1085,plain,(
% 2.26/1.02 heap(sep(lseg(x18,x15),sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f37,f1084])).
% 2.26/1.02 fof(f1086,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1085])).
% 2.26/1.02 fof(f1087,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x18),sep(lseg(x2,x5),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1086])).
% 2.26/1.02 fof(f1088,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x8),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1087])).
% 2.26/1.02 fof(f1089,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x12),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1088])).
% 2.26/1.02 fof(f1090,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x1,x3),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1089])).
% 2.26/1.02 fof(f1091,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x14),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1090])).
% 2.26/1.02 fof(f1092,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x10,x1),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1091])).
% 2.26/1.02 fof(f1093,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x12,x13),sep(lseg(x10,x1),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1092])).
% 2.26/1.02 fof(f1094,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x7,x5),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1093])).
% 2.26/1.02 fof(f1095,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x7,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f36,f1094])).
% 2.26/1.02 fof(f1096,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),sep(lseg(x11,x5),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f292,f1095])).
% 2.26/1.02 fof(f1097,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x11,x5),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.02 inference(forward_demodulation,[status(thm)],[f87,f1096])).
% 2.26/1.02 fof(f1098,plain,(
% 2.26/1.02 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x11,x5),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(forward_demodulation,[status(thm)],[f87,f1097])).
% 2.26/1.04 fof(f1099,plain,(
% 2.26/1.04 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x11,x5),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(forward_demodulation,[status(thm)],[f87,f1098])).
% 2.26/1.04 fof(f1100,plain,(
% 2.26/1.04 heap(sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x11,x5),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(forward_demodulation,[status(thm)],[f87,f1099])).
% 2.26/1.04 fof(f1101,plain,(
% 2.26/1.04 heap(sep(lseg(x11,x5),sep(lseg(x11,x5),sep(lseg(x18,x15),sep(lseg(x2,x5),sep(lseg(x2,x18),sep(lseg(x2,x8),sep(lseg(x2,x12),sep(lseg(x1,x3),sep(lseg(x1,x14),sep(lseg(x10,x1),sep(lseg(x12,x13),emp))))))))))))|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(forward_demodulation,[status(thm)],[f87,f1100])).
% 2.26/1.04 fof(f1102,plain,(
% 2.26/1.04 x11=x5|x11=x5|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(resolution,[status(thm)],[f1101,f45])).
% 2.26/1.04 fof(f1103,plain,(
% 2.26/1.04 sQ6_spl|~sQ5_spl|~sQ4_spl),
% 2.26/1.04 inference(split_clause,[status(thm)],[f1102,f320,f291,f288])).
% 2.26/1.04 fof(f1206,definition,(
% 2.26/1.04 sQ20_spl <=> (x2=x8)),
% 2.26/1.04 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 2.26/1.04 fof(f1207,plain,(
% 2.26/1.04 x2=x8|~sQ20_spl),
% 2.26/1.04 inference(component_clause,[status(thm)],[f1206])).
% 2.26/1.04 fof(f1211,plain,(
% 2.26/1.04 $false|~sQ20_spl),
% 2.26/1.04 inference(forward_subsumption_resolution,[status(thm)],[f1207,f61])).
% 2.26/1.04 fof(f1212,plain,(
% 2.26/1.04 ~sQ20_spl),
% 2.26/1.04 inference(contradiction_clause,[status(thm)],[f1211])).
% 2.26/1.04 fof(f1273,plain,(
% 2.26/1.04 x11=x15|~sQ10_spl|~sQ14_spl),
% 2.26/1.04 inference(backward_demodulation,[status(thm)],[f834,f984])).
% 2.26/1.04 fof(f1274,plain,(
% 2.26/1.04 sQ13_spl|~sQ10_spl|~sQ14_spl),
% 2.26/1.04 inference(split_clause,[status(thm)],[f1273,f890,f833,f983])).
% 2.26/1.04 fof(f1275,plain,(
% 2.26/1.04 $false),
% 2.26/1.04 inference(sat_refutation,[status(thm)],[f134,f224,f294,f323,f377,f786,f795,f839,f840,f849,f900,f932,f933,f990,f991,f1025,f1026,f1036,f1103,f1212,f1274])).
% 2.26/1.04 % SZS output end CNFRefutation for theBenchmark.p
% 2.26/1.05 % Elapsed time: 0.673336 seconds
% 2.26/1.05 % CPU time: 4.846972 seconds
% 2.26/1.05 % Total memory used: 136.724 MB
% 2.26/1.05 % Net memory used: 135.064 MB
%------------------------------------------------------------------------------