%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW425-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 : n019.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.18s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW425-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.43 % Computer : n019.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 09:52:37 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 0.18/0.50 % Refutation found
% 0.18/0.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.18/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.18/0.50 fof(f1,axiom,(
% 0.18/0.50 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f2,axiom,(
% 0.18/0.50 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f7,axiom,(
% 0.18/0.50 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f13,hypothesis,(
% 0.18/0.50 x1 != x7 ),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f14,hypothesis,(
% 0.18/0.50 x1 != x10 ),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f19,hypothesis,(
% 0.18/0.50 x7 != x10 ),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f23,hypothesis,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x2,x5),sep(lseg(x2,x10),sep(lseg(x2,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp))))))))) ),
% 0.18/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/0.50 fof(f25,plain,(
% 0.18/0.50 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.18/0.50 fof(f26,plain,(
% 0.18/0.50 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.18/0.50 fof(f33,plain,(
% 0.18/0.50 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 0.18/0.50 inference(miniscoping,[status(thm)],[f7])).
% 0.18/0.50 fof(f34,plain,(
% 0.18/0.50 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f33])).
% 0.18/0.50 fof(f44,plain,(
% 0.18/0.50 ~x1=x7),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f13])).
% 0.18/0.50 fof(f45,plain,(
% 0.18/0.50 ~x1=x10),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f14])).
% 0.18/0.50 fof(f50,plain,(
% 0.18/0.50 ~x7=x10),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f19])).
% 0.18/0.50 fof(f54,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x2,x5),sep(lseg(x2,x10),sep(lseg(x2,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))),
% 0.18/0.50 inference(cnf_transformation,[status(thm)],[f23])).
% 0.18/0.50 fof(f77,plain,(
% 0.18/0.50 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 0.18/0.50 inference(paramodulation,[status(thm)],[f25,f34])).
% 0.18/0.50 fof(f85,plain,(
% 0.18/0.50 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 0.18/0.50 inference(paramodulation,[status(thm)],[f25,f77])).
% 0.18/0.50 fof(f89,plain,(
% 0.18/0.50 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(lseg(X0,X1),sep(X2,sep(X3,sep(lseg(X0,X4),X5)))))|X0=X1|X0=X4)),
% 0.18/0.50 inference(paramodulation,[status(thm)],[f25,f77])).
% 0.18/0.50 fof(f91,plain,(
% 0.18/0.50 x2=x5|x2=x10),
% 0.18/0.50 inference(resolution,[status(thm)],[f85,f54])).
% 0.18/0.50 fof(f98,definition,(
% 0.18/0.50 sQ2_spl <=> (x2=x5)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f99,plain,(
% 0.18/0.50 x2=x5|~sQ2_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f98])).
% 0.18/0.50 fof(f100,plain,(
% 0.18/0.50 ~x2=x5|sQ2_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f98])).
% 0.18/0.50 fof(f101,definition,(
% 0.18/0.50 sQ3_spl <=> (x2=x10)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f102,plain,(
% 0.18/0.50 x2=x10|~sQ3_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f101])).
% 0.18/0.50 fof(f104,plain,(
% 0.18/0.50 sQ2_spl|sQ3_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f91,f98,f101])).
% 0.18/0.50 fof(f105,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x2,x5),sep(lseg(x2,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))|~sQ2_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f99,f54])).
% 0.18/0.50 fof(f106,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x5,x5),sep(lseg(x2,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))|~sQ2_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f99,f105])).
% 0.18/0.50 fof(f107,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x5,x5),sep(lseg(x5,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))|~sQ2_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f99,f106])).
% 0.18/0.50 fof(f117,plain,(
% 0.18/0.50 x5=x7|x5=x10|~sQ2_spl),
% 0.18/0.50 inference(resolution,[status(thm)],[f107,f77])).
% 0.18/0.50 fof(f118,plain,(
% 0.18/0.50 x5=x7|x5=x1|~sQ2_spl),
% 0.18/0.50 inference(resolution,[status(thm)],[f107,f89])).
% 0.18/0.50 fof(f124,definition,(
% 0.18/0.50 sQ4_spl <=> (x5=x7)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f125,plain,(
% 0.18/0.50 x5=x7|~sQ4_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f124])).
% 0.18/0.50 fof(f131,definition,(
% 0.18/0.50 sQ6_spl <=> (x5=x10)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f132,plain,(
% 0.18/0.50 x5=x10|~sQ6_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f131])).
% 0.18/0.50 fof(f134,plain,(
% 0.18/0.50 sQ4_spl|sQ6_spl|~sQ2_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f117,f124,f131,f98])).
% 0.18/0.50 fof(f135,definition,(
% 0.18/0.50 sQ7_spl <=> (x5=x1)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f136,plain,(
% 0.18/0.50 x5=x1|~sQ7_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f135])).
% 0.18/0.50 fof(f138,plain,(
% 0.18/0.50 sQ4_spl|sQ7_spl|~sQ2_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f118,f124,f135,f98])).
% 0.18/0.50 fof(f157,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x5,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp))))))))|~sQ2_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f26,f107])).
% 0.18/0.50 fof(f191,plain,(
% 0.18/0.50 ~x5=x10|~sQ4_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f125,f50])).
% 0.18/0.50 fof(f193,plain,(
% 0.18/0.50 ~x1=x5|~sQ4_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f125,f44])).
% 0.18/0.50 fof(f194,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x5),sep(lseg(x5,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp))))))))|~sQ4_spl|~sQ2_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f125,f157])).
% 0.18/0.50 fof(f195,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))|~sQ4_spl|~sQ2_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f26,f194])).
% 0.18/0.50 fof(f196,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x10),sep(lseg(x5,x1),sep(lseg(x9,x1),sep(lseg(x5,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))|~sQ4_spl|~sQ2_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f125,f195])).
% 0.18/0.50 fof(f197,plain,(
% 0.18/0.50 x5=x10|x5=x1|~sQ4_spl|~sQ2_spl),
% 0.18/0.50 inference(resolution,[status(thm)],[f196,f34])).
% 0.18/0.50 fof(f201,plain,(
% 0.18/0.50 sQ6_spl|sQ7_spl|~sQ4_spl|~sQ2_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f197,f131,f135,f124,f98])).
% 0.18/0.50 fof(f206,plain,(
% 0.18/0.50 ~x1=x5|~sQ6_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f132,f45])).
% 0.18/0.50 fof(f208,plain,(
% 0.18/0.50 ~x5=x5|~sQ7_spl|~sQ6_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f136,f206])).
% 0.18/0.50 fof(f209,plain,(
% 0.18/0.50 $false|~sQ7_spl|~sQ6_spl),
% 0.18/0.50 inference(trivial_equality_resolution,[status(thm)],[f208])).
% 0.18/0.50 fof(f210,plain,(
% 0.18/0.50 ~sQ7_spl|~sQ6_spl),
% 0.18/0.50 inference(contradiction_clause,[status(thm)],[f209])).
% 0.18/0.50 fof(f212,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x10,x5),sep(lseg(x2,x10),sep(lseg(x2,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))|~sQ3_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f102,f54])).
% 0.18/0.50 fof(f213,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x10,x5),sep(lseg(x10,x10),sep(lseg(x2,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp)))))))))|~sQ3_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f102,f212])).
% 0.18/0.50 fof(f214,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x10,x5),sep(lseg(x2,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp))))))))|~sQ3_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f26,f213])).
% 0.18/0.50 fof(f215,plain,(
% 0.18/0.50 heap(sep(lseg(x5,x7),sep(lseg(x10,x5),sep(lseg(x10,x1),sep(lseg(x9,x1),sep(lseg(x7,x6),sep(lseg(x3,x10),sep(lseg(x6,x9),emp))))))))|~sQ3_spl),
% 0.18/0.50 inference(forward_demodulation,[status(thm)],[f102,f214])).
% 0.18/0.50 fof(f216,plain,(
% 0.18/0.50 x10=x5|x10=x1|~sQ3_spl),
% 0.18/0.50 inference(resolution,[status(thm)],[f215,f85])).
% 0.18/0.50 fof(f221,definition,(
% 0.18/0.50 sQ11_spl <=> (x10=x1)),
% 0.18/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.18/0.50 fof(f222,plain,(
% 0.18/0.50 x10=x1|~sQ11_spl),
% 0.18/0.50 inference(component_clause,[status(thm)],[f221])).
% 0.18/0.50 fof(f224,plain,(
% 0.18/0.50 sQ6_spl|sQ11_spl|~sQ3_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f216,f131,f221,f101])).
% 0.18/0.50 fof(f244,plain,(
% 0.18/0.50 ~sQ6_spl|~sQ4_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f191,f131,f124])).
% 0.18/0.50 fof(f259,plain,(
% 0.18/0.50 $false|~sQ11_spl),
% 0.18/0.50 inference(forward_subsumption_resolution,[status(thm)],[f222,f45])).
% 0.18/0.50 fof(f260,plain,(
% 0.18/0.50 ~sQ11_spl),
% 0.18/0.50 inference(contradiction_clause,[status(thm)],[f259])).
% 0.18/0.50 fof(f266,plain,(
% 0.18/0.50 ~x10=x5|~sQ3_spl|sQ2_spl),
% 0.18/0.50 inference(backward_demodulation,[status(thm)],[f102,f100])).
% 0.18/0.50 fof(f273,plain,(
% 0.18/0.50 ~sQ6_spl|~sQ3_spl|sQ2_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f266,f131,f101,f98])).
% 0.18/0.50 fof(f274,plain,(
% 0.18/0.50 ~sQ7_spl|~sQ4_spl),
% 0.18/0.50 inference(split_clause,[status(thm)],[f193,f135,f124])).
% 0.18/0.50 fof(f275,plain,(
% 0.18/0.50 $false),
% 0.18/0.50 inference(sat_refutation,[status(thm)],[f104,f134,f138,f201,f210,f224,f244,f260,f273,f274])).
% 0.18/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.56 % Elapsed time: 0.123056 seconds
% 0.18/0.56 % CPU time: 0.365404 seconds
% 0.18/0.56 % Total memory used: 49.428 MB
% 0.18/0.56 % Net memory used: 49.297 MB
%------------------------------------------------------------------------------