%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL002+1 : TPTP v9.3.1. Released v4.0.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 02:03:30 PM UTC 2026
% Result : Theorem 0.10s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL002+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 03:57:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.10/0.38 % Refutation found
% 0.10/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.38 fof(f1,axiom,(
% 0.10/0.38 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f2,axiom,(
% 0.10/0.38 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f3,axiom,(
% 0.10/0.38 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f4,axiom,(
% 0.10/0.38 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f11,axiom,(
% 0.10/0.38 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f12,axiom,(
% 0.10/0.38 (! [X0] : top = join(X0,complement(X0)) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f13,axiom,(
% 0.10/0.38 (! [X0] : zero = meet(X0,complement(X0)) )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f14,conjecture,(
% 0.10/0.38 (! [X0] : join(X0,top) = top )),
% 0.10/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.38 fof(f15,negated_conjecture,(
% 0.10/0.38 ~((! [X0] : join(X0,top) = top ))),
% 0.10/0.38 inference(negated_conjecture,[status(cth)],[f14])).
% 0.10/0.38 fof(f16,plain,(
% 0.10/0.38 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.38 fof(f17,plain,(
% 0.10/0.38 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.38 fof(f18,plain,(
% 0.10/0.38 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.38 fof(f19,plain,(
% 0.10/0.38 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.38 fof(f26,plain,(
% 0.10/0.38 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.38 fof(f27,plain,(
% 0.10/0.38 ![X0]: (top=join(X0,complement(X0)))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.38 fof(f28,plain,(
% 0.10/0.38 ![X0]: (zero=meet(X0,complement(X0)))),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f13])).
% 0.10/0.38 fof(f29,plain,(
% 0.10/0.38 (?[X0]: ~join(X0,top)=top)),
% 0.10/0.38 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.10/0.38 fof(f30,plain,(
% 0.10/0.38 ~join(sK0_skl,top)=top),
% 0.10/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X0,sK0_skl)],[f29])).
% 0.10/0.38 fof(f31,plain,(
% 0.10/0.38 ~join(sK0_skl,top)=top),
% 0.10/0.38 inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.38 fof(f32,definition,(
% 0.10/0.38 sF0_fnc=join(sK0_skl,top)),
% 0.10/0.38 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.10/0.38 fof(f33,plain,(
% 0.10/0.38 ~sF0_fnc=top),
% 0.10/0.38 inference(definition_folding,[],[f31,f32])).
% 0.10/0.38 fof(f34,plain,(
% 0.10/0.38 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 0.10/0.38 fof(f35,plain,(
% 0.10/0.38 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f19,f34])).
% 0.10/0.38 fof(f36,plain,(
% 0.10/0.38 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 0.10/0.38 fof(f37,plain,(
% 0.10/0.38 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f35])).
% 0.10/0.38 fof(f43,plain,(
% 0.10/0.38 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f16,f17])).
% 0.10/0.38 fof(f46,plain,(
% 0.10/0.38 ![X0]: (join(sK0_skl,join(top,X0))=join(sF0_fnc,X0))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f32,f17])).
% 0.10/0.38 fof(f47,plain,(
% 0.10/0.38 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f27,f17])).
% 0.10/0.38 fof(f55,plain,(
% 0.10/0.38 join(sK0_skl,top)=join(sF0_fnc,complement(top))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f27,f46])).
% 0.10/0.38 fof(f56,plain,(
% 0.10/0.38 ![X0]: (join(sK0_skl,join(X0,top))=join(sF0_fnc,X0))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f16,f46])).
% 0.10/0.38 fof(f59,plain,(
% 0.10/0.38 sF0_fnc=join(sF0_fnc,complement(top))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f32,f55])).
% 0.10/0.38 fof(f65,plain,(
% 0.10/0.38 ![X0]: (join(X0,top)=join(top,complement(complement(X0))))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f27,f47])).
% 0.10/0.38 fof(f66,plain,(
% 0.10/0.38 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f16,f47])).
% 0.10/0.38 fof(f74,plain,(
% 0.10/0.38 ![X0]: (join(sK0_skl,join(X0,top))=join(sF0_fnc,complement(complement(X0))))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f65,f46])).
% 0.10/0.38 fof(f76,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,X0)=join(sF0_fnc,complement(complement(X0))))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f56,f74])).
% 0.10/0.38 fof(f79,plain,(
% 0.10/0.38 join(top,top)=join(sF0_fnc,complement(sK0_skl))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f47,f56])).
% 0.10/0.38 fof(f91,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,join(complement(sK0_skl),X0))=join(join(top,top),X0))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f79,f17])).
% 0.10/0.38 fof(f92,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,join(complement(sK0_skl),X0))=join(top,join(top,X0)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f17,f91])).
% 0.10/0.38 fof(f94,plain,(
% 0.10/0.38 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f27,f37])).
% 0.10/0.38 fof(f99,plain,(
% 0.10/0.38 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f94])).
% 0.10/0.38 fof(f101,plain,(
% 0.10/0.38 ![X0]: (join(top,X0)=join(top,meet(X0,complement(complement(X0)))))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f99,f47])).
% 0.10/0.38 fof(f107,plain,(
% 0.10/0.38 ![X0,X1]: (join(join(complement(X0),X1),X0)=join(top,meet(X0,X1)))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f37,f66])).
% 0.10/0.38 fof(f123,plain,(
% 0.10/0.38 ![X0,X1]: (join(complement(X0),join(X1,X0))=join(top,meet(X0,X1)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f17,f107])).
% 0.10/0.38 fof(f124,plain,(
% 0.10/0.38 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,meet(X0,X1)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f43,f123])).
% 0.10/0.38 fof(f125,plain,(
% 0.10/0.38 ![X0]: (join(top,X0)=join(top,complement(complement(X0))))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f126,f101])).
% 0.10/0.38 fof(f126,plain,(
% 0.10/0.38 ![X0,X1]: (join(top,X0)=join(top,meet(X1,X0)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f47,f124])).
% 0.10/0.38 fof(f135,plain,(
% 0.10/0.38 ![X0,X1]: (join(sK0_skl,join(top,X0))=join(sF0_fnc,meet(X1,X0)))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f126,f46])).
% 0.10/0.38 fof(f136,plain,(
% 0.10/0.38 ![X0,X1,X2]: (join(top,join(meet(X0,X1),X2))=join(join(top,X1),X2))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f126,f17])).
% 0.10/0.38 fof(f137,plain,(
% 0.10/0.38 ![X0,X1]: (join(sF0_fnc,X0)=join(sF0_fnc,meet(X1,X0)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f46,f135])).
% 0.10/0.38 fof(f138,plain,(
% 0.10/0.38 ![X0,X1,X2]: (join(top,join(meet(X0,X1),X2))=join(top,join(X1,X2)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f17,f136])).
% 0.10/0.38 fof(f173,plain,(
% 0.10/0.38 ![X0,X1]: (join(X0,complement(X0))=join(top,composition(converse(X1),complement(composition(X1,X0)))))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f36,f47])).
% 0.10/0.38 fof(f176,plain,(
% 0.10/0.38 ![X0,X1]: (top=join(top,composition(converse(X0),complement(composition(X0,X1)))))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f27,f173])).
% 0.10/0.38 fof(f247,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,complement(X0))=join(sF0_fnc,zero))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f28,f137])).
% 0.10/0.38 fof(f248,plain,(
% 0.10/0.38 ![X0]: (join(top,complement(X0))=join(top,zero))),
% 0.10/0.38 inference(paramodulation,[status(thm)],[f28,f126])).
% 0.10/0.38 fof(f252,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,X0)=join(zero,sF0_fnc))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f254,f76])).
% 0.10/0.38 fof(f253,plain,(
% 0.10/0.38 sF0_fnc=join(zero,sF0_fnc)),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f254,f59])).
% 0.10/0.38 fof(f254,plain,(
% 0.10/0.38 ![X0]: (join(sF0_fnc,complement(X0))=join(zero,sF0_fnc))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f247])).
% 0.10/0.38 fof(f255,plain,(
% 0.10/0.38 ![X0]: (join(top,X0)=join(zero,top))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f257,f125])).
% 0.10/0.38 fof(f257,plain,(
% 0.10/0.38 ![X0]: (join(top,complement(X0))=join(zero,top))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f16,f248])).
% 0.10/0.38 fof(f265,plain,(
% 0.10/0.38 ![X0]: (join(zero,sF0_fnc)=join(top,join(top,X0)))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f252,f92])).
% 0.10/0.38 fof(f275,plain,(
% 0.10/0.38 ![X0]: (join(top,X0)=join(zero,top))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f255,f126])).
% 0.10/0.38 fof(f279,plain,(
% 0.10/0.38 top=join(zero,top)),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f255,f176])).
% 0.10/0.38 fof(f281,plain,(
% 0.10/0.38 ![X0,X1]: (join(zero,top)=join(top,join(X0,X1)))),
% 0.10/0.38 inference(backward_demodulation,[status(thm)],[f255,f138])).
% 0.10/0.38 fof(f300,plain,(
% 0.10/0.38 ![X0]: (sF0_fnc=join(top,join(top,X0)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f253,f265])).
% 0.10/0.38 fof(f303,plain,(
% 0.10/0.38 sF0_fnc=join(zero,top)),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f255,f300])).
% 0.10/0.38 fof(f314,plain,(
% 0.10/0.38 ![X0]: (join(top,X0)=sF0_fnc)),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f303,f275])).
% 0.10/0.38 fof(f324,plain,(
% 0.10/0.38 ![X0,X1]: (top=join(top,join(X0,X1)))),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f279,f281])).
% 0.10/0.38 fof(f325,plain,(
% 0.10/0.38 top=sF0_fnc),
% 0.10/0.38 inference(forward_demodulation,[status(thm)],[f314,f324])).
% 0.10/0.38 fof(f326,plain,(
% 0.10/0.38 $false),
% 0.10/0.38 inference(forward_subsumption_resolution,[status(thm)],[f325,f33])).
% 0.10/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.40 % Elapsed time: 0.027956 seconds
% 0.13/0.40 % CPU time: 0.052774 seconds
% 0.13/0.40 % Total memory used: 2.034 MB
% 0.13/0.40 % Net memory used: 2.025 MB
%------------------------------------------------------------------------------