%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW445-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 0.64s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW445-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 09:56:07 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 0.64/0.51 % Refutation found
% 0.64/0.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.64/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.64/0.51 fof(f1,axiom,(
% 0.64/0.51 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f2,axiom,(
% 0.64/0.51 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f7,axiom,(
% 0.64/0.51 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f12,hypothesis,(
% 0.64/0.51 x6 != x19 ),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f14,hypothesis,(
% 0.64/0.51 x3 != x20 ),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f30,hypothesis,(
% 0.64/0.51 heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp))))))))))))))) ),
% 0.64/0.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.64/0.51 fof(f32,plain,(
% 0.64/0.51 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f1])).
% 0.64/0.51 fof(f33,plain,(
% 0.64/0.51 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f2])).
% 0.64/0.51 fof(f40,plain,(
% 0.64/0.51 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 0.64/0.51 inference(miniscoping,[status(thm)],[f7])).
% 0.64/0.51 fof(f41,plain,(
% 0.64/0.51 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f40])).
% 0.64/0.51 fof(f50,plain,(
% 0.64/0.51 ~x6=x19),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f12])).
% 0.64/0.51 fof(f52,plain,(
% 0.64/0.51 ~x3=x20),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f14])).
% 0.64/0.51 fof(f68,plain,(
% 0.64/0.51 heap(sep(lseg(x5,x17),sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(cnf_transformation,[status(thm)],[f30])).
% 0.64/0.51 fof(f79,plain,(
% 0.64/0.51 ![X0,X1,X2,X3]: (sep(X0,sep(X1,sep(X2,X3)))=sep(X2,sep(X0,sep(X1,X3))))),
% 0.64/0.51 inference(paramodulation,[status(thm)],[f32,f32])).
% 0.64/0.51 fof(f89,plain,(
% 0.64/0.51 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 0.64/0.51 inference(paramodulation,[status(thm)],[f32,f41])).
% 0.64/0.51 fof(f129,plain,(
% 0.64/0.51 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 0.64/0.51 inference(paramodulation,[status(thm)],[f32,f89])).
% 0.64/0.51 fof(f167,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x5,x17),sep(lseg(x4,x12),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f68])).
% 0.64/0.51 fof(f168,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x15),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f167])).
% 0.64/0.51 fof(f169,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f168])).
% 0.64/0.51 fof(f170,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x2,x18),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f169])).
% 0.64/0.51 fof(f171,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x2,x18),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f170])).
% 0.64/0.51 fof(f172,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x2,x18),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f171])).
% 0.64/0.51 fof(f173,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f172])).
% 0.64/0.51 fof(f174,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f173])).
% 0.64/0.51 fof(f175,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x17,x14),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f174])).
% 0.64/0.51 fof(f176,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x17,x14),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f175])).
% 0.64/0.51 fof(f177,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x17,x14),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f176])).
% 0.64/0.51 fof(f178,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x17,x14),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f177])).
% 0.64/0.51 fof(f179,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f178])).
% 0.64/0.51 fof(f180,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x7,x16),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f179])).
% 0.64/0.51 fof(f181,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x7,x16),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f180])).
% 0.64/0.51 fof(f182,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x7,x16),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f181])).
% 0.64/0.51 fof(f183,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x7,x16),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f182])).
% 0.64/0.51 fof(f184,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f183])).
% 0.64/0.51 fof(f185,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x2,x18),sep(lseg(x7,x16),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f184])).
% 0.64/0.51 fof(f186,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f185])).
% 0.64/0.51 fof(f187,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x20),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f186])).
% 0.64/0.51 fof(f188,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x3,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f187])).
% 0.64/0.51 fof(f189,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x3,x20),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f188])).
% 0.64/0.51 fof(f190,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x3,x20),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f189])).
% 0.64/0.51 fof(f191,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x3,x20),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f190])).
% 0.64/0.51 fof(f192,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x20),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f191])).
% 0.64/0.51 fof(f193,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f192])).
% 0.64/0.51 fof(f194,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x3,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f193])).
% 0.64/0.51 fof(f195,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x12),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f194])).
% 0.64/0.51 fof(f196,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x3,x12),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f195])).
% 0.64/0.51 fof(f197,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x3,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f196])).
% 0.64/0.51 fof(f198,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x3,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f197])).
% 0.64/0.51 fof(f199,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f198])).
% 0.64/0.51 fof(f200,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x12),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f199])).
% 0.64/0.51 fof(f201,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x3,x12),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f200])).
% 0.64/0.51 fof(f202,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f201])).
% 0.64/0.51 fof(f203,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x11,x12),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f202])).
% 0.64/0.51 fof(f204,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x11,x12),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f203])).
% 0.64/0.51 fof(f205,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x5,x17),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f204])).
% 0.64/0.51 fof(f206,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x17),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f205])).
% 0.64/0.51 fof(f207,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x6,x17),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f206])).
% 0.64/0.51 fof(f208,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x6,x17),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f207])).
% 0.64/0.51 fof(f209,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x6,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f208])).
% 0.64/0.51 fof(f210,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x6,x17),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f209])).
% 0.64/0.51 fof(f211,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x6,x17),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f210])).
% 0.64/0.51 fof(f212,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x6,x17),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f211])).
% 0.64/0.51 fof(f213,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x17),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f212])).
% 0.64/0.51 fof(f214,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x17),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f213])).
% 0.64/0.51 fof(f215,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x17),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f214])).
% 0.64/0.51 fof(f216,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x17),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f215])).
% 0.64/0.51 fof(f217,plain,(
% 0.64/0.51 heap(sep(lseg(x19,x1),sep(lseg(x6,x17),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f216])).
% 0.64/0.51 fof(f218,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),sep(lseg(x6,x19),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f217])).
% 0.64/0.51 fof(f219,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x6,x19),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f218])).
% 0.64/0.51 fof(f220,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x6,x19),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f219])).
% 0.64/0.51 fof(f221,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x6,x19),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f220])).
% 0.64/0.51 fof(f222,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x6,x19),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f221])).
% 0.64/0.51 fof(f223,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x6,x19),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f222])).
% 0.64/0.51 fof(f224,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x6,x19),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f223])).
% 0.64/0.51 fof(f225,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x19),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f224])).
% 0.64/0.51 fof(f226,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x19),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f225])).
% 0.64/0.51 fof(f227,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x19),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f226])).
% 0.64/0.51 fof(f228,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x19),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f227])).
% 0.64/0.51 fof(f229,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x6,x19),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f228])).
% 0.64/0.51 fof(f230,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x17),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f229])).
% 0.64/0.51 fof(f231,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x17),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f230])).
% 0.64/0.51 fof(f242,plain,(
% 0.64/0.51 x6=x19|x6=x17),
% 0.64/0.51 inference(resolution,[status(thm)],[f41,f231])).
% 0.64/0.51 fof(f249,definition,(
% 0.64/0.51 sQ4_spl <=> (x6=x19)),
% 0.64/0.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.64/0.51 fof(f250,plain,(
% 0.64/0.51 x6=x19|~sQ4_spl),
% 0.64/0.51 inference(component_clause,[status(thm)],[f249])).
% 0.64/0.51 fof(f252,definition,(
% 0.64/0.51 sQ5_spl <=> (x6=x17)),
% 0.64/0.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.64/0.51 fof(f253,plain,(
% 0.64/0.51 x6=x17|~sQ5_spl),
% 0.64/0.51 inference(component_clause,[status(thm)],[f252])).
% 0.64/0.51 fof(f255,plain,(
% 0.64/0.51 sQ4_spl|sQ5_spl),
% 0.64/0.51 inference(split_clause,[status(thm)],[f242,f249,f252])).
% 0.64/0.51 fof(f256,plain,(
% 0.64/0.51 $false|~sQ4_spl),
% 0.64/0.51 inference(forward_subsumption_resolution,[status(thm)],[f250,f50])).
% 0.64/0.51 fof(f257,plain,(
% 0.64/0.51 ~sQ4_spl),
% 0.64/0.51 inference(contradiction_clause,[status(thm)],[f256])).
% 0.64/0.51 fof(f267,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x6,x17),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(backward_demodulation,[status(thm)],[f253,f231])).
% 0.64/0.51 fof(f270,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f253,f267])).
% 0.64/0.51 fof(f271,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x6),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f270])).
% 0.64/0.51 fof(f272,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x17,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f33,f271])).
% 0.64/0.51 fof(f273,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x6,x14),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f253,f272])).
% 0.64/0.51 fof(f274,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x6,x14),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f273])).
% 0.64/0.51 fof(f275,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x6,x14),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f274])).
% 0.64/0.51 fof(f276,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x6,x14),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f275])).
% 0.64/0.51 fof(f277,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x6,x14),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f276])).
% 0.64/0.51 fof(f278,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x6,x14),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f277])).
% 0.64/0.51 fof(f279,plain,(
% 0.64/0.51 x6=x19|x6=x14|~sQ5_spl),
% 0.64/0.51 inference(resolution,[status(thm)],[f278,f41])).
% 0.64/0.51 fof(f280,definition,(
% 0.64/0.51 sQ6_spl <=> (x6=x14)),
% 0.64/0.51 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.64/0.51 fof(f281,plain,(
% 0.64/0.51 x6=x14|~sQ6_spl),
% 0.64/0.51 inference(component_clause,[status(thm)],[f280])).
% 0.64/0.51 fof(f283,plain,(
% 0.64/0.51 sQ4_spl|sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(split_clause,[status(thm)],[f279,f249,f280,f252])).
% 0.64/0.51 fof(f284,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x6,x6),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(backward_demodulation,[status(thm)],[f281,f278])).
% 0.64/0.51 fof(f285,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x6),sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp))))))))))))))|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f32,f284])).
% 0.64/0.51 fof(f286,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x12,x15),emp)))))))))))))|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f33,f285])).
% 0.64/0.51 fof(f404,plain,(
% 0.64/0.51 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))))|X2=X3|X2=X4)),
% 0.64/0.51 inference(paramodulation,[status(thm)],[f79,f129])).
% 0.64/0.51 fof(f690,plain,(
% 0.64/0.51 x3=x20|x3=x12|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(resolution,[status(thm)],[f404,f286])).
% 0.64/0.51 fof(f711,definition,(
% 0.64/0.51 sQ8_spl <=> (x3=x20)),
% 0.64/0.51 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.64/0.51 fof(f712,plain,(
% 0.64/0.51 x3=x20|~sQ8_spl),
% 0.64/0.51 inference(component_clause,[status(thm)],[f711])).
% 0.64/0.51 fof(f714,definition,(
% 0.64/0.51 sQ9_spl <=> (x3=x12)),
% 0.64/0.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.64/0.51 fof(f715,plain,(
% 0.64/0.51 x3=x12|~sQ9_spl),
% 0.64/0.51 inference(component_clause,[status(thm)],[f714])).
% 0.64/0.51 fof(f717,plain,(
% 0.64/0.51 sQ8_spl|sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(split_clause,[status(thm)],[f690,f711,f714,f280,f252])).
% 0.64/0.51 fof(f718,plain,(
% 0.64/0.51 $false|~sQ8_spl),
% 0.64/0.51 inference(forward_subsumption_resolution,[status(thm)],[f712,f52])).
% 0.64/0.51 fof(f719,plain,(
% 0.64/0.51 ~sQ8_spl),
% 0.64/0.51 inference(contradiction_clause,[status(thm)],[f718])).
% 0.64/0.51 fof(f720,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x12),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(backward_demodulation,[status(thm)],[f715,f286])).
% 0.64/0.51 fof(f721,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x3),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f715,f720])).
% 0.64/0.51 fof(f722,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x3),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp)))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f721])).
% 0.64/0.51 fof(f723,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f33,f722])).
% 0.64/0.51 fof(f724,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f723])).
% 0.64/0.51 fof(f725,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x4,x12),sep(lseg(x2,x18),sep(lseg(x11,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f724])).
% 0.64/0.51 fof(f726,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x11,x12),sep(lseg(x4,x12),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f725])).
% 0.64/0.51 fof(f727,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x12),sep(lseg(x5,x6),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f726])).
% 0.64/0.51 fof(f728,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x5,x6),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f715,f727])).
% 0.64/0.51 fof(f729,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x12),sep(lseg(x12,x20),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f728])).
% 0.64/0.51 fof(f730,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x12,x20),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f715,f729])).
% 0.64/0.51 fof(f731,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),sep(lseg(x12,x20),sep(lseg(x3,x15),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f730])).
% 0.64/0.51 fof(f732,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x3,x15),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f731])).
% 0.64/0.51 fof(f733,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x3,x15),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f732])).
% 0.64/0.51 fof(f734,plain,(
% 0.64/0.51 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x3,x15),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.51 inference(forward_demodulation,[status(thm)],[f79,f733])).
% 0.64/0.52 fof(f735,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x20),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f734])).
% 0.64/0.52 fof(f736,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x3,x20),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f715,f735])).
% 0.64/0.52 fof(f737,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x3,x20),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f736])).
% 0.64/0.52 fof(f738,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x3,x20),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f737])).
% 0.64/0.52 fof(f739,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x12,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f738])).
% 0.64/0.52 fof(f740,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),sep(lseg(x3,x11),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f715,f739])).
% 0.64/0.52 fof(f741,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x3,x11),sep(lseg(x11,x3),sep(lseg(x5,x6),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f740])).
% 0.64/0.52 fof(f742,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x3,x11),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f741])).
% 0.64/0.52 fof(f743,plain,(
% 0.64/0.52 heap(sep(lseg(x6,x19),sep(lseg(x19,x1),sep(lseg(x3,x20),sep(lseg(x3,x20),sep(lseg(x3,x11),sep(lseg(x3,x15),sep(lseg(x7,x16),sep(lseg(x2,x18),sep(lseg(x4,x3),sep(lseg(x11,x3),sep(lseg(x5,x6),emp))))))))))))|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(forward_demodulation,[status(thm)],[f79,f742])).
% 0.64/0.52 fof(f744,plain,(
% 0.64/0.52 x3=x20|x3=x20|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(resolution,[status(thm)],[f743,f404])).
% 0.64/0.52 fof(f745,plain,(
% 0.64/0.52 sQ8_spl|~sQ9_spl|~sQ6_spl|~sQ5_spl),
% 0.64/0.52 inference(split_clause,[status(thm)],[f744,f711,f714,f280,f252])).
% 0.64/0.52 fof(f746,plain,(
% 0.64/0.52 $false),
% 0.64/0.52 inference(sat_refutation,[status(thm)],[f255,f257,f283,f717,f719,f745])).
% 0.64/0.52 % SZS output end CNFRefutation for theBenchmark.p
% 0.64/0.52 % Elapsed time: 0.148887 seconds
% 0.64/0.52 % CPU time: 0.884637 seconds
% 0.64/0.52 % Total memory used: 116.909 MB
% 0.64/0.52 % Net memory used: 116.388 MB
%------------------------------------------------------------------------------