%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW407-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 : n018.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:05 PM UTC 2026
% Result : Unsatisfiable 40.34s 5.72s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW407-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.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:53:30 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 40.34/5.72 % Refutation found
% 40.34/5.72 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 40.34/5.72 % SZS output start CNFRefutation for theBenchmark
% 40.34/5.72 fof(f1,axiom,(
% 40.34/5.72 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f2,axiom,(
% 40.34/5.72 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f8,axiom,(
% 40.34/5.72 (![X,Y,Z,Sigma]: (( ~ heap(sep(next(X,Y),sep(lseg(Y,Z),Sigma)))| X = Y| heap(sep(lseg(X,Z),Sigma)) ) ))),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f10,axiom,(
% 40.34/5.72 (![X,Y,Z,W,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(next(Z,W),Sigma))))| heap(sep(lseg(X,Z),sep(next(Z,W),Sigma))) ) ))),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f16,hypothesis,(
% 40.34/5.72 x1 != x2 ),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f20,hypothesis,(
% 40.34/5.72 heap(sep(next(x1,x2),sep(lseg(x3,x1),sep(lseg(x4,nil),sep(next(x2,x4),emp))))) ),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f21,negated_conjecture,(
% 40.34/5.72 ~ heap(sep(lseg(x4,nil),sep(next(x2,x4),sep(lseg(x3,x2),emp)))) ),
% 40.34/5.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 40.34/5.72 fof(f22,plain,(
% 40.34/5.72 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f1])).
% 40.34/5.72 fof(f23,plain,(
% 40.34/5.72 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f2])).
% 40.34/5.72 fof(f32,plain,(
% 40.34/5.72 ![X,Z,Sigma]: ((![Y]: (~heap(sep(next(X,Y),sep(lseg(Y,Z),Sigma)))|X=Y))|heap(sep(lseg(X,Z),Sigma)))),
% 40.34/5.72 inference(miniscoping,[status(thm)],[f8])).
% 40.34/5.72 fof(f33,plain,(
% 40.34/5.72 ![X0,X1,X2,X3]: (~heap(sep(next(X0,X1),sep(lseg(X1,X2),X3)))|X0=X1|heap(sep(lseg(X0,X2),X3)))),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f32])).
% 40.34/5.72 fof(f36,plain,(
% 40.34/5.72 ![X,Z,W,Sigma]: ((![Y]: ~heap(sep(lseg(X,Y),sep(lseg(Y,Z),sep(next(Z,W),Sigma)))))|heap(sep(lseg(X,Z),sep(next(Z,W),Sigma))))),
% 40.34/5.72 inference(miniscoping,[status(thm)],[f10])).
% 40.34/5.72 fof(f37,plain,(
% 40.34/5.72 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(next(X2,X3),X4))))|heap(sep(lseg(X0,X2),sep(next(X2,X3),X4))))),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f36])).
% 40.34/5.72 fof(f44,plain,(
% 40.34/5.72 ~x1=x2),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f16])).
% 40.34/5.72 fof(f48,plain,(
% 40.34/5.72 heap(sep(next(x1,x2),sep(lseg(x3,x1),sep(lseg(x4,nil),sep(next(x2,x4),emp)))))),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f20])).
% 40.34/5.72 fof(f49,plain,(
% 40.34/5.72 ~heap(sep(lseg(x4,nil),sep(next(x2,x4),sep(lseg(x3,x2),emp))))),
% 40.34/5.72 inference(cnf_transformation,[status(thm)],[f21])).
% 40.34/5.72 fof(f52,plain,(
% 40.34/5.72 ![X0,X1,X2,X3]: (sep(X0,sep(X1,sep(X2,X3)))=sep(X2,sep(X0,sep(X1,X3))))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f22,f22])).
% 40.34/5.72 fof(f58,plain,(
% 40.34/5.72 ~heap(sep(lseg(x4,nil),sep(lseg(x3,x2),sep(next(x2,x4),emp))))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f22,f49])).
% 40.34/5.72 fof(f90,plain,(
% 40.34/5.72 ![X0,X1,X2]: (~heap(sep(next(X0,X1),X2))|X0=X1|heap(sep(lseg(X0,X1),X2)))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f23,f33])).
% 40.34/5.72 fof(f100,plain,(
% 40.34/5.72 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X0),sep(next(X1,X3),X4))))|heap(sep(lseg(X2,X1),sep(next(X1,X3),X4))))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f22,f37])).
% 40.34/5.72 fof(f181,plain,(
% 40.34/5.72 ~heap(sep(lseg(x3,x2),sep(next(x2,x4),sep(lseg(x4,nil),emp))))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f52,f58])).
% 40.34/5.72 fof(f298,plain,(
% 40.34/5.72 x1=x2|heap(sep(lseg(x1,x2),sep(lseg(x3,x1),sep(lseg(x4,nil),sep(next(x2,x4),emp)))))),
% 40.34/5.72 inference(resolution,[status(thm)],[f90,f48])).
% 40.34/5.72 fof(f303,plain,(
% 40.34/5.72 heap(sep(lseg(x1,x2),sep(lseg(x3,x1),sep(lseg(x4,nil),sep(next(x2,x4),emp)))))),
% 40.34/5.72 inference(forward_subsumption_resolution,[status(thm)],[f298,f44])).
% 40.34/5.72 fof(f370,plain,(
% 40.34/5.72 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(lseg(X0,X1),sep(lseg(X2,X0),sep(X3,sep(next(X1,X4),X5)))))|heap(sep(lseg(X2,X1),sep(next(X1,X4),sep(X3,X5)))))),
% 40.34/5.72 inference(paramodulation,[status(thm)],[f22,f100])).
% 40.34/5.72 fof(f12067,plain,(
% 40.34/5.72 heap(sep(lseg(x3,x2),sep(next(x2,x4),sep(lseg(x4,nil),emp))))),
% 40.34/5.72 inference(resolution,[status(thm)],[f370,f303])).
% 40.34/5.72 fof(f12183,plain,(
% 40.34/5.72 $false),
% 40.34/5.72 inference(forward_subsumption_resolution,[status(thm)],[f12067,f181])).
% 40.34/5.73 % SZS output end CNFRefutation for theBenchmark.p
% 2.78/5.75 % Elapsed time: 5.369645 seconds
% 2.78/5.75 % CPU time: 42.186040 seconds
% 2.78/5.75 % Total memory used: 246.228 MB
% 2.78/5.75 % Net memory used: 237.841 MB
%------------------------------------------------------------------------------