%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW429-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 : n014.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 0.19s 5.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW429-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.42 % Computer : n014.cluster.edu
% 0.15/5.42 % Model : x86_64 x86_64
% 0.15/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.42 % Memory : 8046.5625MB
% 0.15/5.42 % OS : Linux 6.8.0-71-generic
% 0.15/5.42 % CPULimit : 300
% 0.15/5.42 % WCLimit : 300
% 0.15/5.42 % DateTime : Mon Sep 21 09:52:10 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.44 % Drodi V4.1.1
% 0.19/5.80 % Refutation found
% 0.19/5.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.19/5.80 % SZS output start CNFRefutation for theBenchmark
% 0.19/5.80 fof(f1,axiom,(
% 0.19/5.80 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f2,axiom,(
% 0.19/5.80 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f4,axiom,(
% 0.19/5.80 (![Y,Sigma]: (( ~ heap(sep(lseg(nil,Y),Sigma))| Y = nil ) ))),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f7,axiom,(
% 0.19/5.80 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f11,axiom,(
% 0.19/5.80 (![X,Y,Z,W,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma))))| Z = W| heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma))) ) ))),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f12,hypothesis,(
% 0.19/5.80 x4 != x7 ),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f14,hypothesis,(
% 0.19/5.80 x3 != x8 ),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f17,hypothesis,(
% 0.19/5.80 heap(sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp)))))))))))) ),
% 0.19/5.80 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/5.80 fof(f19,plain,(
% 0.19/5.80 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f1])).
% 0.19/5.80 fof(f20,plain,(
% 0.19/5.80 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f2])).
% 0.19/5.80 fof(f22,plain,(
% 0.19/5.80 ![Y]: ((![Sigma]: ~heap(sep(lseg(nil,Y),Sigma)))|Y=nil)),
% 0.19/5.80 inference(miniscoping,[status(thm)],[f4])).
% 0.19/5.80 fof(f23,plain,(
% 0.19/5.80 ![X0,X1]: (~heap(sep(lseg(nil,X0),X1))|X0=nil)),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f22])).
% 0.19/5.80 fof(f27,plain,(
% 0.19/5.80 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 0.19/5.80 inference(miniscoping,[status(thm)],[f7])).
% 0.19/5.80 fof(f28,plain,(
% 0.19/5.80 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f27])).
% 0.19/5.80 fof(f35,plain,(
% 0.19/5.80 ![X,Z,W,Sigma]: (((![Y]: ~heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(lseg(Z,W),Sigma)))))|Z=W)|heap(sep(lseg(X,Z),sep(lseg(Z,W),Sigma))))),
% 0.19/5.80 inference(miniscoping,[status(thm)],[f11])).
% 0.19/5.80 fof(f36,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X2,X3),X4))))|X2=X3|heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4))))),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f35])).
% 0.19/5.80 fof(f37,plain,(
% 0.19/5.80 ~x4=x7),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f12])).
% 0.19/5.80 fof(f39,plain,(
% 0.19/5.80 ~x3=x8),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f14])).
% 0.19/5.80 fof(f42,plain,(
% 0.19/5.80 heap(sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(cnf_transformation,[status(thm)],[f17])).
% 0.19/5.80 fof(f53,plain,(
% 0.19/5.80 ![X0,X1,X2,X3]: (sep(X0,sep(X1,sep(X2,X3)))=sep(X2,sep(X0,sep(X1,X3))))),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f19])).
% 0.19/5.80 fof(f59,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X0),sep(lseg(X1,X3),X4))))|X1=X3|heap(sep(lseg(X2,X1),sep(lseg(X1,X3),X4))))),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f36])).
% 0.19/5.80 fof(f60,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X3),sep(lseg(X1,X2),X4))))|X2=X3|heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4))))),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f36])).
% 0.19/5.80 fof(f63,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f28])).
% 0.19/5.80 fof(f72,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X3,X0),X4))))|X1=X2|heap(sep(lseg(X3,X1),sep(lseg(X1,X2),X4))))),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f59])).
% 0.19/5.80 fof(f91,plain,(
% 0.19/5.80 ![X0]: (~heap(X0)|nil=nil)),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f20,f23])).
% 0.19/5.80 fof(f94,definition,(
% 0.19/5.80 ![X0]: (sQ2_spl <=> (~heap(X0)))),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f95,plain,(
% 0.19/5.80 ![X0]: (~heap(X0)|~sQ2_spl)),
% 0.19/5.80 inference(component_clause,[status(thm)],[f94])).
% 0.19/5.80 fof(f97,definition,(
% 0.19/5.80 sQ3_spl <=> (nil=nil)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f100,plain,(
% 0.19/5.80 sQ2_spl|sQ3_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f91,f94,f97])).
% 0.19/5.80 fof(f103,plain,(
% 0.19/5.80 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f19,f63])).
% 0.19/5.80 fof(f110,plain,(
% 0.19/5.80 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X0),X3)))|X0=X1|heap(sep(lseg(X2,X0),sep(lseg(X0,X1),X3))))),
% 0.19/5.80 inference(paramodulation,[status(thm)],[f20,f60])).
% 0.19/5.80 fof(f186,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x5,x1),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f42])).
% 0.19/5.80 fof(f187,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x8),sep(lseg(x5,x1),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f186])).
% 0.19/5.80 fof(f188,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f187])).
% 0.19/5.80 fof(f189,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x4,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f188])).
% 0.19/5.80 fof(f190,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x4,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f189])).
% 0.19/5.80 fof(f191,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x4,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f190])).
% 0.19/5.80 fof(f192,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x4,x7),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f191])).
% 0.19/5.80 fof(f193,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f192])).
% 0.19/5.80 fof(f194,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),sep(lseg(x8,x11),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f193])).
% 0.19/5.80 fof(f195,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x8,x11),sep(lseg(x6,x9),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f194])).
% 0.19/5.80 fof(f196,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x5,x1),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f195])).
% 0.19/5.80 fof(f197,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f196])).
% 0.19/5.80 fof(f198,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f197])).
% 0.19/5.80 fof(f199,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f198])).
% 0.19/5.80 fof(f200,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x12),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f19,f199])).
% 0.19/5.80 fof(f201,plain,(
% 0.19/5.80 $false|~sQ2_spl),
% 0.19/5.80 inference(forward_subsumption_resolution,[status(thm)],[f200,f95])).
% 0.19/5.80 fof(f202,plain,(
% 0.19/5.80 ~sQ2_spl),
% 0.19/5.80 inference(contradiction_clause,[status(thm)],[f201])).
% 0.19/5.80 fof(f235,plain,(
% 0.19/5.80 ![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.19/5.80 inference(paramodulation,[status(thm)],[f53,f103])).
% 0.19/5.80 fof(f307,plain,(
% 0.19/5.80 x4=x7|x4=x12),
% 0.19/5.80 inference(resolution,[status(thm)],[f200,f28])).
% 0.19/5.80 fof(f308,definition,(
% 0.19/5.80 sQ4_spl <=> (x4=x7)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f309,plain,(
% 0.19/5.80 x4=x7|~sQ4_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f308])).
% 0.19/5.80 fof(f311,definition,(
% 0.19/5.80 sQ5_spl <=> (x4=x12)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f312,plain,(
% 0.19/5.80 x4=x12|~sQ5_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f311])).
% 0.19/5.80 fof(f314,plain,(
% 0.19/5.80 sQ4_spl|sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f307,f308,f311])).
% 0.19/5.80 fof(f315,plain,(
% 0.19/5.80 $false|~sQ4_spl),
% 0.19/5.80 inference(forward_subsumption_resolution,[status(thm)],[f309,f37])).
% 0.19/5.80 fof(f316,plain,(
% 0.19/5.80 ~sQ4_spl),
% 0.19/5.80 inference(contradiction_clause,[status(thm)],[f315])).
% 0.19/5.80 fof(f341,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x12),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f312,f200])).
% 0.19/5.80 fof(f342,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f312,f341])).
% 0.19/5.80 fof(f343,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x4),sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f342])).
% 0.19/5.80 fof(f344,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x8),sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f343])).
% 0.19/5.80 fof(f345,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x12),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f344])).
% 0.19/5.80 fof(f346,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x7,x12),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f345])).
% 0.19/5.80 fof(f347,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x7,x12),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f346])).
% 0.19/5.80 fof(f348,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x8),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f312,f347])).
% 0.19/5.80 fof(f349,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f348])).
% 0.19/5.80 fof(f350,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x5),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f349])).
% 0.19/5.80 fof(f351,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x8,x11),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f350])).
% 0.19/5.80 fof(f352,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f351])).
% 0.19/5.80 fof(f353,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f352])).
% 0.19/5.80 fof(f354,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f353])).
% 0.19/5.80 fof(f355,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f354])).
% 0.19/5.80 fof(f356,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x8,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f19,f355])).
% 0.19/5.80 fof(f357,plain,(
% 0.19/5.80 x7=x4|x7=x8|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f356,f103])).
% 0.19/5.80 fof(f358,definition,(
% 0.19/5.80 sQ6_spl <=> (x7=x8)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f359,plain,(
% 0.19/5.80 x7=x8|~sQ6_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f358])).
% 0.19/5.80 fof(f361,plain,(
% 0.19/5.80 sQ4_spl|sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f357,f308,f358,f311])).
% 0.19/5.80 fof(f362,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x8),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f359,f356])).
% 0.19/5.80 fof(f363,plain,(
% 0.19/5.80 ~x3=x7|~sQ6_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f359,f39])).
% 0.19/5.80 fof(f364,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))))|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f359,f362])).
% 0.19/5.80 fof(f365,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x7,x11),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f364])).
% 0.19/5.80 fof(f366,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x11),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f365])).
% 0.19/5.80 fof(f367,plain,(
% 0.19/5.80 x7=x4|x7=x11|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f366,f103])).
% 0.19/5.80 fof(f368,definition,(
% 0.19/5.80 sQ7_spl <=> (x7=x11)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f369,plain,(
% 0.19/5.80 x7=x11|~sQ7_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f368])).
% 0.19/5.80 fof(f371,plain,(
% 0.19/5.80 sQ4_spl|sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f367,f308,f368,f358,f311])).
% 0.19/5.80 fof(f372,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x7,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f369,f366])).
% 0.19/5.80 fof(f373,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f372])).
% 0.19/5.80 fof(f469,plain,(
% 0.19/5.80 x7=x4|heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f72,f373])).
% 0.19/5.80 fof(f485,definition,(
% 0.19/5.80 sQ9_spl <=> (heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f488,plain,(
% 0.19/5.80 sQ4_spl|sQ9_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f469,f308,f485,f368,f358,f311])).
% 0.19/5.80 fof(f564,plain,(
% 0.19/5.80 x4=x7|heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f110,f373])).
% 0.19/5.80 fof(f575,definition,(
% 0.19/5.80 sQ10_spl <=> (heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))))),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f578,plain,(
% 0.19/5.80 sQ4_spl|sQ10_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f564,f308,f575,f368,f358,f311])).
% 0.19/5.80 fof(f630,plain,(
% 0.19/5.80 x3=x4|x3=x5|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f235,f373])).
% 0.19/5.80 fof(f651,definition,(
% 0.19/5.80 sQ11_spl <=> (x3=x4)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f652,plain,(
% 0.19/5.80 x3=x4|~sQ11_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f651])).
% 0.19/5.80 fof(f654,definition,(
% 0.19/5.80 sQ12_spl <=> (x3=x5)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f655,plain,(
% 0.19/5.80 x3=x5|~sQ12_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f654])).
% 0.19/5.80 fof(f657,plain,(
% 0.19/5.80 sQ11_spl|sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f630,f651,f654,f368,f358,f311])).
% 0.19/5.80 fof(f679,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f652,f373])).
% 0.19/5.80 fof(f681,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f679])).
% 0.19/5.80 fof(f682,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x4,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f652,f681])).
% 0.19/5.80 fof(f683,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f682])).
% 0.19/5.80 fof(f684,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x4),sep(lseg(x4,x5),sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f683])).
% 0.19/5.80 fof(f685,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x5),sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f684])).
% 0.19/5.80 fof(f686,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f685])).
% 0.19/5.80 fof(f687,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x5,x1),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f686])).
% 0.19/5.80 fof(f688,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f687])).
% 0.19/5.80 fof(f689,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x6,x7),sep(lseg(x1,x6),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f688])).
% 0.19/5.80 fof(f690,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x9),sep(lseg(x6,x7),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f689])).
% 0.19/5.80 fof(f691,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x5,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f19,f690])).
% 0.19/5.80 fof(f719,plain,(
% 0.19/5.80 x4=x7|x4=x5|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f691,f28])).
% 0.19/5.80 fof(f720,definition,(
% 0.19/5.80 sQ13_spl <=> (x4=x5)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f721,plain,(
% 0.19/5.80 x4=x5|~sQ13_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f720])).
% 0.19/5.80 fof(f727,plain,(
% 0.19/5.80 sQ4_spl|sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f719,f308,f720,f651,f368,f358,f311])).
% 0.19/5.80 fof(f738,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x5),sep(lseg(x7,x4),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f721,f691])).
% 0.19/5.80 fof(f740,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f721,f738])).
% 0.19/5.80 fof(f741,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f740])).
% 0.19/5.80 fof(f742,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f741])).
% 0.19/5.80 fof(f743,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x7,x4),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f742])).
% 0.19/5.80 fof(f745,plain,(
% 0.19/5.80 x4=x7|x4=x1|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f743,f28])).
% 0.19/5.80 fof(f746,definition,(
% 0.19/5.80 sQ15_spl <=> (x4=x1)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f747,plain,(
% 0.19/5.80 x4=x1|~sQ15_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f746])).
% 0.19/5.80 fof(f753,plain,(
% 0.19/5.80 sQ4_spl|sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f745,f308,f746,f720,f651,f368,f358,f311])).
% 0.19/5.80 fof(f754,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x1),sep(lseg(x7,x4),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f747,f743])).
% 0.19/5.80 fof(f755,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f747,f754])).
% 0.19/5.80 fof(f756,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f755])).
% 0.19/5.80 fof(f757,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f756])).
% 0.19/5.80 fof(f758,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f757])).
% 0.19/5.80 fof(f760,plain,(
% 0.19/5.80 x4=x7|x4=x6|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(resolution,[status(thm)],[f758,f28])).
% 0.19/5.80 fof(f761,definition,(
% 0.19/5.80 sQ17_spl <=> (x4=x6)),
% 0.19/5.80 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.19/5.80 fof(f762,plain,(
% 0.19/5.80 x4=x6|~sQ17_spl),
% 0.19/5.80 inference(component_clause,[status(thm)],[f761])).
% 0.19/5.80 fof(f768,plain,(
% 0.19/5.80 sQ4_spl|sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(split_clause,[status(thm)],[f760,f308,f761,f746,f720,f651,f368,f358,f311])).
% 0.19/5.80 fof(f793,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x6),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x4,x9),emp))))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(backward_demodulation,[status(thm)],[f762,f758])).
% 0.19/5.80 fof(f794,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x6,x7),sep(lseg(x4,x9),emp))))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f762,f793])).
% 0.19/5.80 fof(f795,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x4),sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x4,x9),emp))))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f794])).
% 0.19/5.80 fof(f796,plain,(
% 0.19/5.80 heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x4,x9),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f20,f795])).
% 0.19/5.80 fof(f797,plain,(
% 0.19/5.80 heap(sep(lseg(x4,x7),sep(lseg(x6,x7),sep(lseg(x7,x4),sep(lseg(x4,x9),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.80 inference(forward_demodulation,[status(thm)],[f53,f796])).
% 0.19/5.81 fof(f798,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x4,x9),sep(lseg(x6,x7),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f53,f797])).
% 0.19/5.81 fof(f799,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x6,x7),sep(lseg(x7,x4),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f53,f798])).
% 0.19/5.81 fof(f800,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),sep(lseg(x6,x7),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f19,f799])).
% 0.19/5.81 fof(f801,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),sep(lseg(x4,x7),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f762,f800])).
% 0.19/5.81 fof(f802,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x4,x7),sep(lseg(x4,x9),sep(lseg(x7,x4),emp)))))|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f53,f801])).
% 0.19/5.81 fof(f804,plain,(
% 0.19/5.81 x4=x7|x4=x7|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f802,f28])).
% 0.19/5.81 fof(f811,plain,(
% 0.19/5.81 sQ4_spl|~sQ17_spl|~sQ15_spl|~sQ13_spl|~sQ11_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f804,f308,f761,f746,f720,f651,f368,f358,f311])).
% 0.19/5.81 fof(f823,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x5),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(backward_demodulation,[status(thm)],[f655,f373])).
% 0.19/5.81 fof(f824,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f655,f823])).
% 0.19/5.81 fof(f825,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f20,f824])).
% 0.19/5.81 fof(f826,plain,(
% 0.19/5.81 x7=x4|heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f825,f72])).
% 0.19/5.81 fof(f827,plain,(
% 0.19/5.81 x4=x7|heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f825,f110])).
% 0.19/5.81 fof(f828,plain,(
% 0.19/5.81 x3=x4|x3=x1|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f825,f235])).
% 0.19/5.81 fof(f829,definition,(
% 0.19/5.81 sQ22_spl <=> (heap(sep(lseg(x3,x7),sep(lseg(x7,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))),
% 0.19/5.81 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.19/5.81 fof(f832,plain,(
% 0.19/5.81 sQ4_spl|sQ22_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f826,f308,f829,f654,f368,f358,f311])).
% 0.19/5.81 fof(f833,definition,(
% 0.19/5.81 sQ23_spl <=> (heap(sep(lseg(x7,x4),sep(lseg(x4,x7),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x1,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))))),
% 0.19/5.81 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.19/5.81 fof(f836,plain,(
% 0.19/5.81 sQ4_spl|sQ23_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f827,f308,f833,f654,f368,f358,f311])).
% 0.19/5.81 fof(f837,definition,(
% 0.19/5.81 sQ24_spl <=> (x3=x1)),
% 0.19/5.81 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.19/5.81 fof(f838,plain,(
% 0.19/5.81 x3=x1|~sQ24_spl),
% 0.19/5.81 inference(component_clause,[status(thm)],[f837])).
% 0.19/5.81 fof(f840,plain,(
% 0.19/5.81 sQ11_spl|sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f828,f651,f837,f654,f368,f358,f311])).
% 0.19/5.81 fof(f852,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x1),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(backward_demodulation,[status(thm)],[f838,f825])).
% 0.19/5.81 fof(f853,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp))))))))|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f838,f852])).
% 0.19/5.81 fof(f854,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x6,x9),emp)))))))|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f20,f853])).
% 0.19/5.81 fof(f857,plain,(
% 0.19/5.81 x3=x4|x3=x6|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f854,f235])).
% 0.19/5.81 fof(f866,definition,(
% 0.19/5.81 sQ27_spl <=> (x3=x6)),
% 0.19/5.81 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.19/5.81 fof(f867,plain,(
% 0.19/5.81 x3=x6|~sQ27_spl),
% 0.19/5.81 inference(component_clause,[status(thm)],[f866])).
% 0.19/5.81 fof(f869,plain,(
% 0.19/5.81 sQ11_spl|sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f857,f651,f866,f837,f654,f368,f358,f311])).
% 0.19/5.81 fof(f880,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x6),sep(lseg(x6,x7),sep(lseg(x3,x9),emp)))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(backward_demodulation,[status(thm)],[f867,f854])).
% 0.19/5.81 fof(f881,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x6),sep(lseg(x6,x7),emp)))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f53,f880])).
% 0.19/5.81 fof(f882,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x3),sep(lseg(x6,x7),emp)))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f867,f881])).
% 0.19/5.81 fof(f883,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x3),sep(lseg(x6,x7),sep(lseg(x3,x9),emp)))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f53,f882])).
% 0.19/5.81 fof(f884,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x6,x7),sep(lseg(x3,x9),emp))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f20,f883])).
% 0.19/5.81 fof(f885,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x6,x7),emp))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f19,f884])).
% 0.19/5.81 fof(f886,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x9),sep(lseg(x3,x7),emp))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f867,f885])).
% 0.19/5.81 fof(f887,plain,(
% 0.19/5.81 heap(sep(lseg(x4,x7),sep(lseg(x7,x4),sep(lseg(x3,x4),sep(lseg(x3,x7),sep(lseg(x3,x9),emp))))))|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(forward_demodulation,[status(thm)],[f19,f886])).
% 0.19/5.81 fof(f890,plain,(
% 0.19/5.81 x3=x4|x3=x7|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(resolution,[status(thm)],[f887,f235])).
% 0.19/5.81 fof(f899,definition,(
% 0.19/5.81 sQ30_spl <=> (x3=x7)),
% 0.19/5.81 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.19/5.81 fof(f900,plain,(
% 0.19/5.81 x3=x7|~sQ30_spl),
% 0.19/5.81 inference(component_clause,[status(thm)],[f899])).
% 0.19/5.81 fof(f902,plain,(
% 0.19/5.81 sQ11_spl|sQ30_spl|~sQ27_spl|~sQ24_spl|~sQ12_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl),
% 0.19/5.81 inference(split_clause,[status(thm)],[f890,f651,f899,f866,f837,f654,f368,f358,f311])).
% 0.19/5.81 fof(f908,plain,(
% 0.19/5.81 $false|~sQ6_spl|~sQ30_spl),
% 0.19/5.81 inference(forward_subsumption_resolution,[status(thm)],[f900,f363])).
% 0.19/5.81 fof(f909,plain,(
% 0.19/5.81 ~sQ6_spl|~sQ30_spl),
% 0.19/5.81 inference(contradiction_clause,[status(thm)],[f908])).
% 0.19/5.81 fof(f910,plain,(
% 0.19/5.81 $false),
% 0.19/5.81 inference(sat_refutation,[status(thm)],[f100,f202,f314,f316,f361,f371,f488,f578,f657,f727,f753,f768,f811,f832,f836,f840,f869,f902,f909])).
% 0.19/5.81 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/5.81 % Elapsed time: 0.376584 seconds
% 0.19/5.81 % CPU time: 2.732279 seconds
% 0.19/5.81 % Total memory used: 123.816 MB
% 0.19/5.81 % Net memory used: 122.574 MB
%------------------------------------------------------------------------------