%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW436-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 : n007.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 5.49s 1.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW436-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 09:50:36 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 5.49/1.14 % Refutation found
% 5.49/1.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.49/1.14 % SZS output start CNFRefutation for theBenchmark
% 5.49/1.14 fof(f1,axiom,(
% 5.49/1.14 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f2,axiom,(
% 5.49/1.14 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f4,axiom,(
% 5.49/1.14 (![Y,Sigma]: (( ~ heap(sep(lseg(nil,Y),Sigma))| Y = nil ) ))),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f7,axiom,(
% 5.49/1.14 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f15,hypothesis,(
% 5.49/1.14 x4 != x6 ),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f16,hypothesis,(
% 5.49/1.14 x4 != x7 ),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f20,hypothesis,(
% 5.49/1.14 heap(sep(lseg(x13,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp))))))))))))))))) ),
% 5.49/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.49/1.14 fof(f22,plain,(
% 5.49/1.14 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f1])).
% 5.49/1.14 fof(f23,plain,(
% 5.49/1.14 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f2])).
% 5.49/1.14 fof(f25,plain,(
% 5.49/1.14 ![Y]: ((![Sigma]: ~heap(sep(lseg(nil,Y),Sigma)))|Y=nil)),
% 5.49/1.14 inference(miniscoping,[status(thm)],[f4])).
% 5.49/1.14 fof(f26,plain,(
% 5.49/1.14 ![X0,X1]: (~heap(sep(lseg(nil,X0),X1))|X0=nil)),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f25])).
% 5.49/1.14 fof(f30,plain,(
% 5.49/1.14 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 5.49/1.14 inference(miniscoping,[status(thm)],[f7])).
% 5.49/1.14 fof(f31,plain,(
% 5.49/1.14 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f30])).
% 5.49/1.14 fof(f43,plain,(
% 5.49/1.14 ~x4=x6),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f15])).
% 5.49/1.14 fof(f44,plain,(
% 5.49/1.14 ~x4=x7),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f16])).
% 5.49/1.14 fof(f48,plain,(
% 5.49/1.14 heap(sep(lseg(x13,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(cnf_transformation,[status(thm)],[f20])).
% 5.49/1.14 fof(f59,plain,(
% 5.49/1.14 ![X0,X1,X2,X3]: (sep(X0,sep(X1,sep(X2,X3)))=sep(X2,sep(X0,sep(X1,X3))))),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f22,f22])).
% 5.49/1.14 fof(f69,plain,(
% 5.49/1.14 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f22,f31])).
% 5.49/1.14 fof(f75,plain,(
% 5.49/1.14 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f22,f69])).
% 5.49/1.14 fof(f85,plain,(
% 5.49/1.14 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5)))))|X1=X2|X1=X4)),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f22,f75])).
% 5.49/1.14 fof(f97,plain,(
% 5.49/1.14 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))))|X2=X3|X2=X4)),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f22,f85])).
% 5.49/1.14 fof(f160,plain,(
% 5.49/1.14 ![X0]: (~heap(X0)|nil=nil)),
% 5.49/1.14 inference(paramodulation,[status(thm)],[f23,f26])).
% 5.49/1.14 fof(f163,definition,(
% 5.49/1.14 ![X0]: (sQ2_spl <=> (~heap(X0)))),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f164,plain,(
% 5.49/1.14 ![X0]: (~heap(X0)|~sQ2_spl)),
% 5.49/1.14 inference(component_clause,[status(thm)],[f163])).
% 5.49/1.14 fof(f166,definition,(
% 5.49/1.14 sQ3_spl <=> (nil=nil)),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f169,plain,(
% 5.49/1.14 sQ2_spl|sQ3_spl),
% 5.49/1.14 inference(split_clause,[status(thm)],[f160,f163,f166])).
% 5.49/1.14 fof(f215,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x13,x2),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f48])).
% 5.49/1.14 fof(f216,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x13,x2),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f215])).
% 5.49/1.14 fof(f217,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x13,x2),sep(lseg(x1,x5),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f216])).
% 5.49/1.14 fof(f218,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f217])).
% 5.49/1.14 fof(f219,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x8,x1),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f218])).
% 5.49/1.14 fof(f220,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f219])).
% 5.49/1.14 fof(f221,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x13,x2),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f220])).
% 5.49/1.14 fof(f222,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x13,x2),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f221])).
% 5.49/1.14 fof(f223,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f222])).
% 5.49/1.14 fof(f224,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x15,x4),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f223])).
% 5.49/1.14 fof(f225,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x8,x1),sep(lseg(x15,x4),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f224])).
% 5.49/1.14 fof(f226,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f225])).
% 5.49/1.14 fof(f227,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f226])).
% 5.49/1.14 fof(f228,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f227])).
% 5.49/1.14 fof(f229,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x14,x8),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f228])).
% 5.49/1.14 fof(f230,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x2,x15),sep(lseg(x13,x2),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f229])).
% 5.49/1.14 fof(f231,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x2,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f230])).
% 5.49/1.14 fof(f232,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f231])).
% 5.49/1.14 fof(f233,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x2,x9),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f232])).
% 5.49/1.14 fof(f234,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x2,x9),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f233])).
% 5.49/1.14 fof(f235,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f234])).
% 5.49/1.14 fof(f236,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f235])).
% 5.49/1.14 fof(f237,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f236])).
% 5.49/1.14 fof(f238,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x14,x8),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f237])).
% 5.49/1.14 fof(f239,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x9,x7),sep(lseg(x13,x2),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f238])).
% 5.49/1.14 fof(f240,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x9,x7),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f239])).
% 5.49/1.14 fof(f241,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f240])).
% 5.49/1.14 fof(f242,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x9,x6),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f241])).
% 5.49/1.14 fof(f243,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x9,x6),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f242])).
% 5.49/1.14 fof(f244,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x3,x10),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f243])).
% 5.49/1.14 fof(f245,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x3,x10),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f244])).
% 5.49/1.14 fof(f246,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x3,x10),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f245])).
% 5.49/1.14 fof(f247,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x3,x10),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f246])).
% 5.49/1.14 fof(f248,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x3,x10),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f247])).
% 5.49/1.14 fof(f249,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),sep(lseg(x6,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f248])).
% 5.49/1.14 fof(f250,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x6,x2),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f249])).
% 5.49/1.14 fof(f251,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x6,x2),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f250])).
% 5.49/1.14 fof(f252,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x6,x2),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f251])).
% 5.49/1.14 fof(f253,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x6,x2),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f252])).
% 5.49/1.14 fof(f254,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x6,x2),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f253])).
% 5.49/1.14 fof(f255,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x6,x2),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f254])).
% 5.49/1.14 fof(f256,plain,(
% 5.49/1.14 heap(sep(lseg(x4,x9),sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f255])).
% 5.49/1.14 fof(f257,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f256])).
% 5.49/1.14 fof(f258,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x4,x13),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f257])).
% 5.49/1.14 fof(f259,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f258])).
% 5.49/1.14 fof(f260,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f259])).
% 5.49/1.14 fof(f261,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f260])).
% 5.49/1.14 fof(f262,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f261])).
% 5.49/1.14 fof(f263,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f262])).
% 5.49/1.14 fof(f264,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f263])).
% 5.49/1.14 fof(f265,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f264])).
% 5.49/1.14 fof(f266,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f265])).
% 5.49/1.14 fof(f267,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f266])).
% 5.49/1.14 fof(f268,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f267])).
% 5.49/1.14 fof(f269,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f268])).
% 5.49/1.14 fof(f270,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x14,x8),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f269])).
% 5.49/1.14 fof(f271,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f22,f270])).
% 5.49/1.14 fof(f272,plain,(
% 5.49/1.14 $false|~sQ2_spl),
% 5.49/1.14 inference(forward_subsumption_resolution,[status(thm)],[f271,f164])).
% 5.49/1.14 fof(f273,plain,(
% 5.49/1.14 ~sQ2_spl),
% 5.49/1.14 inference(contradiction_clause,[status(thm)],[f272])).
% 5.49/1.14 fof(f411,plain,(
% 5.49/1.14 x4=x9|x4=x13),
% 5.49/1.14 inference(resolution,[status(thm)],[f75,f271])).
% 5.49/1.14 fof(f427,definition,(
% 5.49/1.14 sQ5_spl <=> (x4=x9)),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f428,plain,(
% 5.49/1.14 x4=x9|~sQ5_spl),
% 5.49/1.14 inference(component_clause,[status(thm)],[f427])).
% 5.49/1.14 fof(f430,definition,(
% 5.49/1.14 sQ6_spl <=> (x4=x13)),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f431,plain,(
% 5.49/1.14 x4=x13|~sQ6_spl),
% 5.49/1.14 inference(component_clause,[status(thm)],[f430])).
% 5.49/1.14 fof(f433,plain,(
% 5.49/1.14 sQ5_spl|sQ6_spl),
% 5.49/1.14 inference(split_clause,[status(thm)],[f411,f427,f430])).
% 5.49/1.14 fof(f434,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x4,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(backward_demodulation,[status(thm)],[f428,f271])).
% 5.49/1.14 fof(f435,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x4),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x4,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f428,f434])).
% 5.49/1.14 fof(f436,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x4,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f23,f435])).
% 5.49/1.14 fof(f437,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x4,x7),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f436])).
% 5.49/1.14 fof(f438,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x4,x7),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f437])).
% 5.49/1.14 fof(f439,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x1,x6),sep(lseg(x4,x7),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f438])).
% 5.49/1.14 fof(f440,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f439])).
% 5.49/1.14 fof(f441,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f440])).
% 5.49/1.14 fof(f442,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f441])).
% 5.49/1.14 fof(f443,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f442])).
% 5.49/1.14 fof(f444,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f443])).
% 5.49/1.14 fof(f445,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f444])).
% 5.49/1.14 fof(f446,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x8,x1),sep(lseg(x9,x6),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f445])).
% 5.49/1.14 fof(f447,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x4),sep(lseg(x8,x1),sep(lseg(x9,x6),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f428,f446])).
% 5.49/1.14 fof(f448,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x8,x1),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f447])).
% 5.49/1.14 fof(f449,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f448])).
% 5.49/1.14 fof(f450,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x4,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f428,f449])).
% 5.49/1.14 fof(f451,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x4,x6),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f450])).
% 5.49/1.14 fof(f452,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x4,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f451])).
% 5.49/1.14 fof(f453,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f452])).
% 5.49/1.14 fof(f454,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x13),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ5_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f453])).
% 5.49/1.14 fof(f455,plain,(
% 5.49/1.14 x4=x6|x4=x13|~sQ5_spl),
% 5.49/1.14 inference(resolution,[status(thm)],[f454,f75])).
% 5.49/1.14 fof(f456,definition,(
% 5.49/1.14 sQ7_spl <=> (x4=x6)),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f457,plain,(
% 5.49/1.14 x4=x6|~sQ7_spl),
% 5.49/1.14 inference(component_clause,[status(thm)],[f456])).
% 5.49/1.14 fof(f459,plain,(
% 5.49/1.14 sQ7_spl|sQ6_spl|~sQ5_spl),
% 5.49/1.14 inference(split_clause,[status(thm)],[f455,f456,f430,f427])).
% 5.49/1.14 fof(f630,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x4),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f431,f271])).
% 5.49/1.14 fof(f631,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x4),sep(lseg(x1,x6),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f630])).
% 5.49/1.14 fof(f632,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x1,x6),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f23,f631])).
% 5.49/1.14 fof(f633,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f632])).
% 5.49/1.14 fof(f634,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f633])).
% 5.49/1.14 fof(f635,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f634])).
% 5.49/1.14 fof(f636,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f635])).
% 5.49/1.14 fof(f637,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f636])).
% 5.49/1.14 fof(f638,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f637])).
% 5.49/1.14 fof(f639,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f638])).
% 5.49/1.14 fof(f640,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f639])).
% 5.49/1.14 fof(f641,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f640])).
% 5.49/1.14 fof(f642,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f641])).
% 5.49/1.14 fof(f643,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f642])).
% 5.49/1.14 fof(f644,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x13,x2),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f643])).
% 5.49/1.14 fof(f645,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f22,f644])).
% 5.49/1.14 fof(f646,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x4,x2),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f431,f645])).
% 5.49/1.14 fof(f647,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x4,x2),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f646])).
% 5.49/1.14 fof(f648,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x4,x2),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f647])).
% 5.49/1.14 fof(f649,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x4,x2),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f648])).
% 5.49/1.14 fof(f650,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x4,x2),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f649])).
% 5.49/1.14 fof(f651,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x4,x2),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f650])).
% 5.49/1.14 fof(f652,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x9),sep(lseg(x4,x2),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f651])).
% 5.49/1.14 fof(f653,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x1,x6),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f652])).
% 5.49/1.14 fof(f654,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f653])).
% 5.49/1.14 fof(f655,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f654])).
% 5.49/1.14 fof(f656,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f655])).
% 5.49/1.14 fof(f657,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x15),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f656])).
% 5.49/1.14 fof(f658,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f657])).
% 5.49/1.14 fof(f659,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x9,x6),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f658])).
% 5.49/1.14 fof(f660,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f659])).
% 5.49/1.14 fof(f661,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f660])).
% 5.49/1.14 fof(f662,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f661])).
% 5.49/1.14 fof(f663,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f662])).
% 5.49/1.14 fof(f664,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f59,f663])).
% 5.49/1.14 fof(f665,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x2),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ6_spl),
% 5.49/1.14 inference(forward_demodulation,[status(thm)],[f22,f664])).
% 5.49/1.14 fof(f666,plain,(
% 5.49/1.14 x4=x2|x4=x9|~sQ6_spl),
% 5.49/1.14 inference(resolution,[status(thm)],[f665,f75])).
% 5.49/1.14 fof(f667,definition,(
% 5.49/1.14 sQ9_spl <=> (x4=x2)),
% 5.49/1.14 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 5.49/1.14 fof(f668,plain,(
% 5.49/1.14 x4=x2|~sQ9_spl),
% 5.49/1.14 inference(component_clause,[status(thm)],[f667])).
% 5.49/1.14 fof(f670,plain,(
% 5.49/1.14 sQ9_spl|sQ5_spl|~sQ6_spl),
% 5.49/1.14 inference(split_clause,[status(thm)],[f666,f667,f427,f430])).
% 5.49/1.14 fof(f671,plain,(
% 5.49/1.14 $false|~sQ7_spl),
% 5.49/1.14 inference(forward_subsumption_resolution,[status(thm)],[f457,f43])).
% 5.49/1.14 fof(f672,plain,(
% 5.49/1.14 ~sQ7_spl),
% 5.49/1.14 inference(contradiction_clause,[status(thm)],[f671])).
% 5.49/1.14 fof(f685,plain,(
% 5.49/1.14 heap(sep(lseg(x6,x4),sep(lseg(x4,x2),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f668,f665])).
% 5.49/1.15 fof(f686,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x4),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp))))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f668,f685])).
% 5.49/1.15 fof(f687,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f23,f686])).
% 5.49/1.15 fof(f688,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x4,x15),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f668,f687])).
% 5.49/1.15 fof(f689,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x4,x15),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f688])).
% 5.49/1.15 fof(f690,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x9),sep(lseg(x4,x15),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f689])).
% 5.49/1.15 fof(f691,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x1,x6),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f690])).
% 5.49/1.15 fof(f692,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f691])).
% 5.49/1.15 fof(f693,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f692])).
% 5.49/1.15 fof(f694,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x9),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f693])).
% 5.49/1.15 fof(f695,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x9),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f694])).
% 5.49/1.15 fof(f696,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f695])).
% 5.49/1.15 fof(f697,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f696])).
% 5.49/1.15 fof(f698,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x4,x9),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f668,f697])).
% 5.49/1.15 fof(f699,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x4,x9),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f698])).
% 5.49/1.15 fof(f700,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x7),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f699])).
% 5.49/1.15 fof(f701,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x8,x1),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f700])).
% 5.49/1.15 fof(f702,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f701])).
% 5.49/1.15 fof(f703,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f702])).
% 5.49/1.15 fof(f704,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f703])).
% 5.49/1.15 fof(f705,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x4),sep(lseg(x4,x15),sep(lseg(x4,x9),sep(lseg(x4,x9),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x9,x6),sep(lseg(x9,x7),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f22,f704])).
% 5.49/1.15 fof(f708,plain,(
% 5.49/1.15 x4=x9|x4=x9|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(resolution,[status(thm)],[f705,f97])).
% 5.49/1.15 fof(f714,plain,(
% 5.49/1.15 sQ5_spl|~sQ9_spl|~sQ6_spl),
% 5.49/1.15 inference(split_clause,[status(thm)],[f708,f427,f667,f430])).
% 5.49/1.15 fof(f715,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x4),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp))))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f431,f454])).
% 5.49/1.15 fof(f716,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x13,x2),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f23,f715])).
% 5.49/1.15 fof(f717,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),sep(lseg(x4,x2),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f431,f716])).
% 5.49/1.15 fof(f718,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x4,x2),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f717])).
% 5.49/1.15 fof(f719,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x4,x2),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f718])).
% 5.49/1.15 fof(f720,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x4,x2),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f719])).
% 5.49/1.15 fof(f721,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x4,x2),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f720])).
% 5.49/1.15 fof(f722,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x7),sep(lseg(x4,x2),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f721])).
% 5.49/1.15 fof(f723,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x1,x6),sep(lseg(x4,x7),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f722])).
% 5.49/1.15 fof(f724,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x5),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f723])).
% 5.49/1.15 fof(f725,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x3,x10),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f724])).
% 5.49/1.15 fof(f726,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x15,x4),sep(lseg(x3,x10),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f725])).
% 5.49/1.15 fof(f727,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x2,x4),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f726])).
% 5.49/1.15 fof(f728,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x15),sep(lseg(x2,x4),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f727])).
% 5.49/1.15 fof(f729,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x8,x1),sep(lseg(x2,x15),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f728])).
% 5.49/1.15 fof(f730,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f729])).
% 5.49/1.15 fof(f731,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x14),sep(lseg(x8,x15),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f730])).
% 5.49/1.15 fof(f732,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x14,x8),sep(lseg(x8,x14),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f59,f731])).
% 5.49/1.15 fof(f733,plain,(
% 5.49/1.15 heap(sep(lseg(x6,x2),sep(lseg(x4,x6),sep(lseg(x4,x2),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x1,x5),sep(lseg(x3,x10),sep(lseg(x15,x4),sep(lseg(x2,x4),sep(lseg(x2,x15),sep(lseg(x8,x1),sep(lseg(x8,x15),sep(lseg(x8,x14),sep(lseg(x14,x8),emp)))))))))))))))|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(forward_demodulation,[status(thm)],[f22,f732])).
% 5.49/1.15 fof(f771,plain,(
% 5.49/1.15 x4=x6|x4=x7|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(resolution,[status(thm)],[f733,f85])).
% 5.49/1.15 fof(f774,definition,(
% 5.49/1.15 sQ11_spl <=> (x4=x7)),
% 5.49/1.15 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 5.49/1.15 fof(f775,plain,(
% 5.49/1.15 x4=x7|~sQ11_spl),
% 5.49/1.15 inference(component_clause,[status(thm)],[f774])).
% 5.49/1.15 fof(f777,plain,(
% 5.49/1.15 sQ7_spl|sQ11_spl|~sQ6_spl|~sQ5_spl),
% 5.49/1.15 inference(split_clause,[status(thm)],[f771,f456,f774,f430,f427])).
% 5.49/1.15 fof(f779,plain,(
% 5.49/1.15 $false|~sQ11_spl),
% 5.49/1.15 inference(forward_subsumption_resolution,[status(thm)],[f775,f44])).
% 5.49/1.15 fof(f780,plain,(
% 5.49/1.15 ~sQ11_spl),
% 5.49/1.15 inference(contradiction_clause,[status(thm)],[f779])).
% 5.49/1.15 fof(f781,plain,(
% 5.49/1.15 $false),
% 5.49/1.15 inference(sat_refutation,[status(thm)],[f169,f273,f433,f459,f670,f672,f714,f777,f780])).
% 5.49/1.15 % SZS output end CNFRefutation for theBenchmark.p
% 5.49/1.16 % Elapsed time: 0.785916 seconds
% 5.49/1.16 % CPU time: 5.806506 seconds
% 5.49/1.16 % Total memory used: 139.499 MB
% 5.49/1.16 % Net memory used: 137.145 MB
%------------------------------------------------------------------------------