%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW431-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 : n011.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.22s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW431-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n011.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 09:53:11 UTC 2026
% 0.18/0.46 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 0.22/0.65 % Refutation found
% 0.22/0.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.65 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.65 fof(f1,axiom,(
% 0.22/0.65 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 0.22/0.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.65 fof(f2,axiom,(
% 0.22/0.65 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 0.22/0.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.65 fof(f7,axiom,(
% 0.22/0.65 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 0.22/0.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.65 fof(f18,hypothesis,(
% 0.22/0.65 x7 != x11 ),
% 0.22/0.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.65 fof(f24,hypothesis,(
% 0.22/0.65 heap(sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x1,x11),sep(lseg(x4,x9),sep(lseg(x2,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp))))))))))))) ),
% 0.22/0.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.22/0.65 fof(f26,plain,(
% 0.22/0.65 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 0.22/0.65 inference(cnf_transformation,[status(thm)],[f1])).
% 0.22/0.65 fof(f27,plain,(
% 0.22/0.65 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 0.22/0.65 inference(cnf_transformation,[status(thm)],[f2])).
% 0.22/0.65 fof(f34,plain,(
% 0.22/0.65 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 0.22/0.65 inference(miniscoping,[status(thm)],[f7])).
% 0.22/0.65 fof(f35,plain,(
% 0.22/0.65 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 0.22/0.65 inference(cnf_transformation,[status(thm)],[f34])).
% 0.22/0.65 fof(f50,plain,(
% 0.22/0.65 ~x7=x11),
% 0.22/0.65 inference(cnf_transformation,[status(thm)],[f18])).
% 0.22/0.65 fof(f56,plain,(
% 0.22/0.65 heap(sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x1,x11),sep(lseg(x4,x9),sep(lseg(x2,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(cnf_transformation,[status(thm)],[f24])).
% 0.22/0.65 fof(f77,plain,(
% 0.22/0.65 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 0.22/0.65 inference(paramodulation,[status(thm)],[f26,f35])).
% 0.22/0.65 fof(f83,plain,(
% 0.22/0.65 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 0.22/0.65 inference(paramodulation,[status(thm)],[f26,f77])).
% 0.22/0.65 fof(f178,plain,(
% 0.22/0.65 heap(sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x1,x11),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x2,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f56])).
% 0.22/0.65 fof(f179,plain,(
% 0.22/0.65 heap(sep(lseg(x5,x3),sep(lseg(x1,x11),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x2,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f178])).
% 0.22/0.65 fof(f180,plain,(
% 0.22/0.65 heap(sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x2,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f179])).
% 0.22/0.65 fof(f181,plain,(
% 0.22/0.65 heap(sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x2,x9),sep(lseg(x4,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f180])).
% 0.22/0.65 fof(f182,plain,(
% 0.22/0.65 heap(sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x2,x9),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f181])).
% 0.22/0.65 fof(f183,plain,(
% 0.22/0.65 heap(sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x2,x9),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f182])).
% 0.22/0.65 fof(f184,plain,(
% 0.22/0.65 heap(sep(lseg(x1,x11),sep(lseg(x2,x9),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f183])).
% 0.22/0.65 fof(f185,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f184])).
% 0.22/0.65 fof(f186,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x12,x7),sep(lseg(x4,x9),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f185])).
% 0.22/0.65 fof(f187,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x12,x7),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f186])).
% 0.22/0.65 fof(f188,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x5,x3),sep(lseg(x12,x7),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f187])).
% 0.22/0.65 fof(f189,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f188])).
% 0.22/0.65 fof(f190,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x9,x2),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f189])).
% 0.22/0.65 fof(f191,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x9,x2),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f190])).
% 0.22/0.65 fof(f192,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x9,x2),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f191])).
% 0.22/0.65 fof(f193,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x9,x2),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f192])).
% 0.22/0.65 fof(f194,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x1,x11),sep(lseg(x9,x2),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f193])).
% 0.22/0.65 fof(f195,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f194])).
% 0.22/0.65 fof(f196,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x7,x10),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f195])).
% 0.22/0.65 fof(f197,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x7,x10),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f196])).
% 0.22/0.65 fof(f198,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x7,x10),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f197])).
% 0.22/0.65 fof(f199,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x7,x10),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f198])).
% 0.22/0.65 fof(f200,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x7,x10),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f199])).
% 0.22/0.65 fof(f201,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x7,x10),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f200])).
% 0.22/0.65 fof(f202,plain,(
% 0.22/0.65 heap(sep(lseg(x2,x9),sep(lseg(x7,x10),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f201])).
% 0.22/0.65 fof(f203,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f202])).
% 0.22/0.65 fof(f204,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x11,x12),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f203])).
% 0.22/0.65 fof(f205,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x11,x12),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f204])).
% 0.22/0.65 fof(f206,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x11,x12),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f205])).
% 0.22/0.65 fof(f207,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x11,x12),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f206])).
% 0.22/0.65 fof(f208,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x11,x12),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f207])).
% 0.22/0.65 fof(f209,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x12),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f208])).
% 0.22/0.65 fof(f210,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x2,x9),sep(lseg(x11,x12),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f209])).
% 0.22/0.65 fof(f211,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x7),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f210])).
% 0.22/0.65 fof(f212,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x11,x7),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f211])).
% 0.22/0.65 fof(f213,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x11,x7),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f212])).
% 0.22/0.65 fof(f214,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x11,x7),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f213])).
% 0.22/0.65 fof(f215,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x11,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f214])).
% 0.22/0.65 fof(f216,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x11,x7),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f215])).
% 0.22/0.65 fof(f217,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x7),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f216])).
% 0.22/0.65 fof(f218,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x11,x7),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f217])).
% 0.22/0.65 fof(f219,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x12),sep(lseg(x11,x7),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f218])).
% 0.22/0.65 fof(f220,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),sep(lseg(x11,x1),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f219])).
% 0.22/0.65 fof(f221,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x11,x1),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f220])).
% 0.22/0.65 fof(f222,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x11,x1),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f221])).
% 0.22/0.65 fof(f223,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x11,x1),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f222])).
% 0.22/0.65 fof(f224,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x11,x1),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f223])).
% 0.22/0.65 fof(f225,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x11,x1),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f224])).
% 0.22/0.65 fof(f226,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x1),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f225])).
% 0.22/0.65 fof(f227,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x11,x1),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f226])).
% 0.22/0.65 fof(f228,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x11,x1),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f227])).
% 0.22/0.65 fof(f229,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x1),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x1,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f228])).
% 0.22/0.65 fof(f320,plain,(
% 0.22/0.65 x11=x7|x11=x1),
% 0.22/0.65 inference(resolution,[status(thm)],[f83,f229])).
% 0.22/0.65 fof(f330,definition,(
% 0.22/0.65 sQ5_spl <=> (x11=x7)),
% 0.22/0.65 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.22/0.65 fof(f331,plain,(
% 0.22/0.65 x11=x7|~sQ5_spl),
% 0.22/0.65 inference(component_clause,[status(thm)],[f330])).
% 0.22/0.65 fof(f333,definition,(
% 0.22/0.65 sQ6_spl <=> (x11=x1)),
% 0.22/0.65 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.22/0.65 fof(f334,plain,(
% 0.22/0.65 x11=x1|~sQ6_spl),
% 0.22/0.65 inference(component_clause,[status(thm)],[f333])).
% 0.22/0.65 fof(f336,plain,(
% 0.22/0.65 sQ5_spl|sQ6_spl),
% 0.22/0.65 inference(split_clause,[status(thm)],[f320,f330,f333])).
% 0.22/0.65 fof(f337,plain,(
% 0.22/0.65 $false|~sQ5_spl),
% 0.22/0.65 inference(forward_subsumption_resolution,[status(thm)],[f331,f50])).
% 0.22/0.65 fof(f338,plain,(
% 0.22/0.65 ~sQ5_spl),
% 0.22/0.65 inference(contradiction_clause,[status(thm)],[f337])).
% 0.22/0.65 fof(f339,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x1),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))|~sQ6_spl),
% 0.22/0.65 inference(backward_demodulation,[status(thm)],[f334,f229])).
% 0.22/0.65 fof(f340,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))))|~sQ6_spl),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f334,f339])).
% 0.22/0.65 fof(f341,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x11),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))))|~sQ6_spl),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f27,f340])).
% 0.22/0.65 fof(f342,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x11,x11),sep(lseg(x9,x2),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))))|~sQ6_spl),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f341])).
% 0.22/0.65 fof(f343,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x11,x11),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))))|~sQ6_spl),
% 0.22/0.65 inference(forward_demodulation,[status(thm)],[f26,f342])).
% 0.22/0.65 fof(f344,plain,(
% 0.22/0.65 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x11),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))))|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f26,f343])).
% 0.22/0.66 fof(f345,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x12,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f27,f344])).
% 0.22/0.66 fof(f346,plain,(
% 0.22/0.66 x11=x7|x11=x12|~sQ6_spl),
% 0.22/0.66 inference(resolution,[status(thm)],[f345,f83])).
% 0.22/0.66 fof(f347,definition,(
% 0.22/0.66 sQ7_spl <=> (x11=x12)),
% 0.22/0.66 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.22/0.66 fof(f348,plain,(
% 0.22/0.66 x11=x12|~sQ7_spl),
% 0.22/0.66 inference(component_clause,[status(thm)],[f347])).
% 0.22/0.66 fof(f350,plain,(
% 0.22/0.66 sQ5_spl|sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(split_clause,[status(thm)],[f346,f330,f347,f333])).
% 0.22/0.66 fof(f351,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x12),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(backward_demodulation,[status(thm)],[f348,f345])).
% 0.22/0.66 fof(f353,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x11),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp)))))))))))|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f348,f351])).
% 0.22/0.66 fof(f354,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x11,x7),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f27,f353])).
% 0.22/0.66 fof(f355,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x2,x9),sep(lseg(x11,x7),sep(lseg(x9,x2),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f26,f354])).
% 0.22/0.66 fof(f356,plain,(
% 0.22/0.66 heap(sep(lseg(x7,x10),sep(lseg(x11,x7),sep(lseg(x11,x7),sep(lseg(x2,x9),sep(lseg(x9,x2),sep(lseg(x5,x3),sep(lseg(x10,x8),sep(lseg(x13,x8),sep(lseg(x4,x9),emp))))))))))|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(forward_demodulation,[status(thm)],[f26,f355])).
% 0.22/0.66 fof(f393,plain,(
% 0.22/0.66 x11=x7|x11=x7|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(resolution,[status(thm)],[f356,f83])).
% 0.22/0.66 fof(f394,plain,(
% 0.22/0.66 sQ5_spl|~sQ7_spl|~sQ6_spl),
% 0.22/0.66 inference(split_clause,[status(thm)],[f393,f330,f347,f333])).
% 0.22/0.66 fof(f395,plain,(
% 0.22/0.66 $false),
% 0.22/0.66 inference(sat_refutation,[status(thm)],[f336,f338,f350,f394])).
% 0.22/0.66 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.68 % Elapsed time: 0.197460 seconds
% 0.22/0.68 % CPU time: 1.290247 seconds
% 0.22/0.68 % Total memory used: 116.063 MB
% 0.22/0.68 % Net memory used: 115.505 MB
%------------------------------------------------------------------------------