%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT044-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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 01:03:11 PM UTC 2026
% Result : Unsatisfiable 22.25s 3.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT044-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n007.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 : Sun Sep 20 23:06:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 22.25/3.23 % Refutation found
% 22.25/3.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.25/3.23 % SZS output start CNFRefutation for theBenchmark
% 22.25/3.23 fof(f3,axiom,(
% 22.25/3.23 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f4,axiom,(
% 22.25/3.23 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f5,axiom,(
% 22.25/3.23 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f6,axiom,(
% 22.25/3.23 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f7,axiom,(
% 22.25/3.23 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f8,axiom,(
% 22.25/3.23 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f9,axiom,(
% 22.25/3.23 (![X,Y]: (complement(join(X,Y)) = meet(complement(X),complement(Y)) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f11,axiom,(
% 22.25/3.23 (![X]: (join(complement(X),X) = n1 ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f13,axiom,(
% 22.25/3.23 (![X]: (complement(complement(X)) = X ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f14,axiom,(
% 22.25/3.23 (![X,Y]: (join(X,meet(complement(X),join(X,Y))) = join(X,Y) ))),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f15,negated_conjecture,(
% 22.25/3.23 join(meet(complement(a),join(a,b)),join(complement(b),meet(a,b))) != n1 ),
% 22.25/3.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.25/3.23 fof(f18,plain,(
% 22.25/3.23 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f3])).
% 22.25/3.23 fof(f19,plain,(
% 22.25/3.23 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f4])).
% 22.25/3.23 fof(f20,plain,(
% 22.25/3.23 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f5])).
% 22.25/3.23 fof(f21,plain,(
% 22.25/3.23 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f6])).
% 22.25/3.23 fof(f22,plain,(
% 22.25/3.23 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f7])).
% 22.25/3.23 fof(f23,plain,(
% 22.25/3.23 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f8])).
% 22.25/3.23 fof(f24,plain,(
% 22.25/3.23 ![X0,X1]: (complement(join(X0,X1))=meet(complement(X0),complement(X1)))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f9])).
% 22.25/3.23 fof(f26,plain,(
% 22.25/3.23 ![X0]: (join(complement(X0),X0)=n1)),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f11])).
% 22.25/3.23 fof(f28,plain,(
% 22.25/3.23 ![X0]: (complement(complement(X0))=X0)),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f13])).
% 22.25/3.23 fof(f29,plain,(
% 22.25/3.23 ![X0,X1]: (join(X0,meet(complement(X0),join(X0,X1)))=join(X0,X1))),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f14])).
% 22.25/3.23 fof(f30,plain,(
% 22.25/3.23 ~join(meet(complement(a),join(a,b)),join(complement(b),meet(a,b)))=n1),
% 22.25/3.23 inference(cnf_transformation,[status(thm)],[f15])).
% 22.25/3.23 fof(f31,definition,(
% 22.25/3.23 sF2_fnc=complement(a)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 22.25/3.23 fof(f32,definition,(
% 22.25/3.23 sF3_fnc=join(a,b)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 22.25/3.23 fof(f33,definition,(
% 22.25/3.23 sF1_fnc=meet(sF2_fnc,sF3_fnc)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 22.25/3.23 fof(f34,definition,(
% 22.25/3.23 sF5_fnc=complement(b)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 22.25/3.23 fof(f35,definition,(
% 22.25/3.23 sF6_fnc=meet(a,b)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 22.25/3.23 fof(f36,definition,(
% 22.25/3.23 sF4_fnc=join(sF5_fnc,sF6_fnc)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 22.25/3.23 fof(f37,definition,(
% 22.25/3.23 sF0_fnc=join(sF1_fnc,sF4_fnc)),
% 22.25/3.23 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 22.25/3.23 fof(f38,plain,(
% 22.25/3.23 ~sF0_fnc=n1),
% 22.25/3.23 inference(definition_folding,[],[f30,f37,f36,f35,f34,f33,f32,f31])).
% 22.25/3.23 fof(f39,plain,(
% 22.25/3.23 ![X0]: (join(X0,complement(X0))=n1)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f21,f26])).
% 22.25/3.23 fof(f42,plain,(
% 22.25/3.23 complement(sF5_fnc)=b),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f34,f28])).
% 22.25/3.23 fof(f43,plain,(
% 22.25/3.23 complement(sF2_fnc)=a),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f31,f28])).
% 22.25/3.23 fof(f51,plain,(
% 22.25/3.23 join(sF2_fnc,sF1_fnc)=sF2_fnc),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f33,f19])).
% 22.25/3.23 fof(f55,plain,(
% 22.25/3.23 join(sF1_fnc,sF2_fnc)=sF2_fnc),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f21,f51])).
% 22.25/3.23 fof(f72,plain,(
% 22.25/3.23 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f21,f18])).
% 22.25/3.23 fof(f233,plain,(
% 22.25/3.23 ![X0,X1]: (n1=join(X0,join(X1,complement(join(X0,X1)))))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f39,f23])).
% 22.25/3.23 fof(f289,plain,(
% 22.25/3.23 ![X0]: (complement(join(X0,sF5_fnc))=meet(complement(X0),b))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f42,f24])).
% 22.25/3.23 fof(f290,plain,(
% 22.25/3.23 ![X0,X1]: (complement(join(X0,complement(X1)))=meet(complement(X0),X1))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f28,f24])).
% 22.25/3.23 fof(f292,plain,(
% 22.25/3.23 ![X0]: (complement(join(X0,a))=meet(complement(X0),sF2_fnc))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f31,f24])).
% 22.25/3.23 fof(f307,plain,(
% 22.25/3.23 ![X0]: (complement(join(X0,sF5_fnc))=meet(b,complement(X0)))),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f289])).
% 22.25/3.23 fof(f309,plain,(
% 22.25/3.23 ![X0]: (complement(join(X0,a))=meet(sF2_fnc,complement(X0)))),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f292])).
% 22.25/3.23 fof(f412,plain,(
% 22.25/3.23 meet(b,sF3_fnc)=b),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f32,f72])).
% 22.25/3.23 fof(f442,plain,(
% 22.25/3.23 ![X0]: (meet(b,X0)=meet(b,meet(sF3_fnc,X0)))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f412,f22])).
% 22.25/3.23 fof(f524,plain,(
% 22.25/3.23 join(sF1_fnc,meet(complement(sF1_fnc),sF2_fnc))=join(sF1_fnc,sF2_fnc)),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f55,f29])).
% 22.25/3.23 fof(f530,plain,(
% 22.25/3.23 join(a,meet(complement(a),sF3_fnc))=join(a,b)),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f32,f29])).
% 22.25/3.23 fof(f573,plain,(
% 22.25/3.23 join(sF1_fnc,meet(sF2_fnc,complement(sF1_fnc)))=join(sF1_fnc,sF2_fnc)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f524])).
% 22.25/3.23 fof(f574,plain,(
% 22.25/3.23 join(sF1_fnc,complement(join(sF1_fnc,a)))=join(sF1_fnc,sF2_fnc)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f309,f573])).
% 22.25/3.23 fof(f575,plain,(
% 22.25/3.23 join(sF1_fnc,complement(join(a,sF1_fnc)))=join(sF1_fnc,sF2_fnc)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f21,f574])).
% 22.25/3.23 fof(f576,plain,(
% 22.25/3.23 join(sF1_fnc,complement(join(a,sF1_fnc)))=sF2_fnc),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f55,f575])).
% 22.25/3.23 fof(f588,plain,(
% 22.25/3.23 join(a,meet(sF3_fnc,complement(a)))=join(a,b)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f530])).
% 22.25/3.23 fof(f589,plain,(
% 22.25/3.23 join(a,meet(sF3_fnc,sF2_fnc))=join(a,b)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f31,f588])).
% 22.25/3.23 fof(f590,plain,(
% 22.25/3.23 join(a,meet(sF2_fnc,sF3_fnc))=join(a,b)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f589])).
% 22.25/3.23 fof(f591,plain,(
% 22.25/3.23 join(a,sF1_fnc)=join(a,b)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f33,f590])).
% 22.25/3.23 fof(f592,plain,(
% 22.25/3.23 join(sF1_fnc,complement(sF3_fnc))=sF2_fnc),
% 22.25/3.23 inference(backward_demodulation,[status(thm)],[f593,f576])).
% 22.25/3.23 fof(f593,plain,(
% 22.25/3.23 join(a,sF1_fnc)=sF3_fnc),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f32,f591])).
% 22.25/3.23 fof(f13500,plain,(
% 22.25/3.23 complement(sF2_fnc)=meet(complement(sF1_fnc),sF3_fnc)),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f592,f290])).
% 22.25/3.23 fof(f13556,plain,(
% 22.25/3.23 a=meet(complement(sF1_fnc),sF3_fnc)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f43,f13500])).
% 22.25/3.23 fof(f13558,plain,(
% 22.25/3.23 a=meet(sF3_fnc,complement(sF1_fnc))),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f13556])).
% 22.25/3.23 fof(f37277,plain,(
% 22.25/3.23 meet(b,complement(sF1_fnc))=meet(b,a)),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f13558,f442])).
% 22.25/3.23 fof(f37346,plain,(
% 22.25/3.23 complement(join(sF1_fnc,sF5_fnc))=meet(b,a)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f307,f37277])).
% 22.25/3.23 fof(f37347,plain,(
% 22.25/3.23 complement(join(sF1_fnc,sF5_fnc))=meet(a,b)),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f20,f37346])).
% 22.25/3.23 fof(f37348,plain,(
% 22.25/3.23 complement(join(sF1_fnc,sF5_fnc))=sF6_fnc),
% 22.25/3.23 inference(forward_demodulation,[status(thm)],[f35,f37347])).
% 22.25/3.23 fof(f37431,plain,(
% 22.25/3.23 n1=join(sF1_fnc,join(sF5_fnc,sF6_fnc))),
% 22.25/3.23 inference(paramodulation,[status(thm)],[f37348,f233])).
% 22.25/3.29 fof(f37473,plain,(
% 22.25/3.29 sF0_fnc=n1),
% 22.25/3.29 inference(backward_demodulation,[status(thm)],[f37474,f37])).
% 22.25/3.29 fof(f37474,plain,(
% 22.25/3.29 n1=join(sF1_fnc,sF4_fnc)),
% 22.25/3.29 inference(forward_demodulation,[status(thm)],[f36,f37431])).
% 22.25/3.29 fof(f37589,plain,(
% 22.25/3.29 $false),
% 22.25/3.29 inference(forward_subsumption_resolution,[status(thm)],[f37473,f38])).
% 22.25/3.29 % SZS output end CNFRefutation for theBenchmark.p
% 22.25/3.31 % Elapsed time: 2.933323 seconds
% 22.25/3.31 % CPU time: 23.024951 seconds
% 22.25/3.31 % Total memory used: 234.203 MB
% 22.25/3.31 % Net memory used: 226.116 MB
%------------------------------------------------------------------------------