%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT029-1 : TPTP v9.3.1. Released v2.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 01:03:09 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT029-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.53 % Computer : n019.cluster.edu
% 0.09/0.53 % Model : x86_64 x86_64
% 0.09/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.53 % Memory : 8046.5625MB
% 0.09/0.53 % OS : Linux 6.8.0-71-generic
% 0.09/0.53 % CPULimit : 300
% 0.09/0.53 % WCLimit : 300
% 0.09/0.53 % DateTime : Sun Sep 20 23:07:38 UTC 2026
% 0.09/0.53 % CPUTime :
% 0.09/0.54 % Drodi V4.1.1
% 0.14/0.84 % Refutation found
% 0.14/0.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.84 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.84 fof(f1,axiom,(
% 0.14/0.84 (![X,Y]: (join(meet(X,Y),meet(X,join(X,Y))) = X ))),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f2,axiom,(
% 0.14/0.84 (![X,Y]: (join(meet(X,X),meet(Y,join(X,X))) = X ))),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f3,axiom,(
% 0.14/0.84 (![X,Y]: (join(meet(X,Y),meet(Y,join(X,Y))) = Y ))),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f4,axiom,(
% 0.14/0.84 (![X,Y,Z]: (meet(meet(join(X,Y),join(Z,X)),X) = X ))),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f5,axiom,(
% 0.14/0.84 (![X,Y,Z]: (join(join(meet(X,Y),meet(Z,X)),X) = X ))),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f6,negated_conjecture,(
% 0.14/0.84 ( meet(a,a) != a| meet(b,a) != meet(a,b)| join(a,a) != a| join(b,a) != join(a,b) ) ),
% 0.14/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.84 fof(f7,plain,(
% 0.14/0.84 ![X0,X1]: (join(meet(X0,X1),meet(X0,join(X0,X1)))=X0)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/0.84 fof(f8,plain,(
% 0.14/0.84 ![X0,X1]: (join(meet(X0,X0),meet(X1,join(X0,X0)))=X0)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/0.84 fof(f9,plain,(
% 0.14/0.84 ![X0,X1]: (join(meet(X0,X1),meet(X1,join(X0,X1)))=X1)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.84 fof(f10,plain,(
% 0.14/0.84 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X0)),X0)=X0)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.84 fof(f11,plain,(
% 0.14/0.84 ![X0,X1,X2]: (join(join(meet(X0,X1),meet(X2,X0)),X0)=X0)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.84 fof(f12,plain,(
% 0.14/0.84 ~meet(a,a)=a|~meet(b,a)=meet(a,b)|~join(a,a)=a|~join(b,a)=join(a,b)),
% 0.14/0.84 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.84 fof(f25,plain,(
% 0.14/0.84 ![X0,X1,X2]: (meet(meet(X0,join(X1,meet(X2,X0))),meet(X2,X0))=meet(X2,X0))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f9,f10])).
% 0.14/0.84 fof(f38,plain,(
% 0.14/0.84 ![X0,X1,X2,X3]: (join(join(X0,meet(X1,meet(join(X0,X2),join(X3,X0)))),meet(join(X0,X2),join(X3,X0)))=meet(join(X0,X2),join(X3,X0)))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f10,f11])).
% 0.14/0.84 fof(f39,plain,(
% 0.14/0.84 ![X0,X1]: (join(join(meet(X0,X1),X0),X0)=X0)),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f10,f11])).
% 0.14/0.84 fof(f40,plain,(
% 0.14/0.84 ![X0,X1]: (meet(meet(join(X0,X1),X0),X0)=X0)),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f11,f10])).
% 0.14/0.84 fof(f48,plain,(
% 0.14/0.84 ![X0,X1]: (join(meet(join(meet(X0,X1),X0),X0),meet(join(meet(X0,X1),X0),X0))=join(meet(X0,X1),X0))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f39,f7])).
% 0.14/0.84 fof(f52,plain,(
% 0.14/0.84 ![X0,X1]: (meet(meet(X0,meet(X1,X0)),meet(X1,X0))=meet(X1,X0))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f9,f40])).
% 0.14/0.84 fof(f54,plain,(
% 0.14/0.84 ![X0,X1]: (meet(meet(X0,meet(X0,X1)),meet(X0,X1))=meet(X0,X1))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f7,f40])).
% 0.14/0.84 fof(f56,plain,(
% 0.14/0.84 ![X0,X1]: (join(join(X0,meet(join(X0,X1),X0)),meet(join(X0,X1),X0))=meet(join(X0,X1),X0))),
% 0.14/0.84 inference(paramodulation,[status(thm)],[f40,f39])).
% 0.14/0.84 fof(f69,plain,(
% 0.14/0.84 ![X0,X1,X2]: (meet(meet(X0,X0),meet(meet(join(X0,X1),join(X2,X0)),X0))=meet(meet(join(X0,X1),join(X2,X0)),X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f10,f52])).
% 0.14/0.85 fof(f76,plain,(
% 0.14/0.85 ![X0,X1]: (join(join(meet(X0,X1),meet(X1,meet(X0,X1))),meet(X1,meet(X0,X1)))=meet(X1,meet(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f52,f39])).
% 0.14/0.85 fof(f81,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(X0,X0),X0)=meet(meet(join(X0,X1),join(X2,X0)),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f10,f69])).
% 0.14/0.85 fof(f85,plain,(
% 0.14/0.85 ![X0]: (meet(meet(X0,X0),X0)=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f10,f81])).
% 0.14/0.85 fof(f103,plain,(
% 0.14/0.85 ![X0]: (join(X0,meet(X0,join(meet(X0,X0),X0)))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f85,f9])).
% 0.14/0.85 fof(f107,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(X0,join(X1,X0)),X0)=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f103,f10])).
% 0.14/0.85 fof(f108,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(meet(X0,join(meet(X0,X0),X0)),X0))=meet(X0,join(meet(X0,X0),X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f103,f9])).
% 0.14/0.85 fof(f109,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,meet(X0,join(meet(X0,X0),X0))),meet(X0,X0))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f103,f7])).
% 0.14/0.85 fof(f111,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,meet(X0,join(meet(X0,X0),X0))),X0)=meet(X0,join(meet(X0,X0),X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f107,f108])).
% 0.14/0.85 fof(f116,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(X1,X0)))=meet(X0,join(X1,X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f9,f107])).
% 0.14/0.85 fof(f128,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(meet(X0,join(X1,X0)),join(meet(X0,join(X1,X0)),X0)))=meet(X0,join(X1,X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f107,f7])).
% 0.14/0.85 fof(f130,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(meet(X0,X0),X0)),meet(X0,X0))=X0)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f132,f109])).
% 0.14/0.85 fof(f131,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(meet(X0,X0),X0)),X0)=meet(X0,join(meet(X0,X0),X0)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f132,f111])).
% 0.14/0.85 fof(f132,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,meet(X0,join(X1,X0)))=meet(X0,join(X1,X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f107,f116])).
% 0.14/0.85 fof(f176,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(meet(join(X0,X1),join(X2,X0)),X0),meet(meet(join(X0,X1),join(X2,X0)),X0))=meet(meet(join(X0,X1),join(X2,X0)),X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f10,f54])).
% 0.14/0.85 fof(f196,plain,(
% 0.14/0.85 ![X0,X1]: (join(join(meet(X0,X1),meet(X0,meet(X0,X1))),meet(X0,meet(X0,X1)))=meet(X0,meet(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f54,f39])).
% 0.14/0.85 fof(f201,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(X0,meet(meet(join(X0,X1),join(X2,X0)),X0))=meet(meet(join(X0,X1),join(X2,X0)),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f10,f176])).
% 0.14/0.85 fof(f202,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(X0,X0)=meet(meet(join(X0,X1),join(X2,X0)),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f10,f201])).
% 0.14/0.85 fof(f204,plain,(
% 0.14/0.85 ~a=a|~meet(b,a)=meet(a,b)|~join(a,a)=a|~join(b,a)=join(a,b)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f237,f12])).
% 0.14/0.85 fof(f210,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(X1,join(X0,X0)))=X0)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f237,f8])).
% 0.14/0.85 fof(f224,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(meet(X0,X0),X0)),X0)=meet(X0,join(X0,X0)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f237,f131])).
% 0.14/0.85 fof(f225,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(meet(X0,X0),X0)),X0)=X0)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f237,f130])).
% 0.14/0.85 fof(f237,plain,(
% 0.14/0.85 ![X0]: (meet(X0,X0)=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f10,f202])).
% 0.14/0.85 fof(f268,plain,(
% 0.14/0.85 ~meet(b,a)=meet(a,b)|~join(a,a)=a|~join(b,a)=join(a,b)),
% 0.14/0.85 inference(trivial_equality_resolution,[status(thm)],[f204])).
% 0.14/0.85 fof(f290,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(X0,X0)),X0)=meet(X0,join(X0,X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f237,f224])).
% 0.14/0.85 fof(f291,plain,(
% 0.14/0.85 ![X0]: (X0=meet(X0,join(X0,X0)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f292,f290])).
% 0.14/0.85 fof(f292,plain,(
% 0.14/0.85 ![X0]: (join(meet(X0,join(X0,X0)),X0)=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f237,f225])).
% 0.14/0.85 fof(f305,plain,(
% 0.14/0.85 ![X0]: (join(X0,X0)=X0)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f291,f292])).
% 0.14/0.85 fof(f306,plain,(
% 0.14/0.85 ~meet(b,a)=meet(a,b)|~a=a|~join(b,a)=join(a,b)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f305,f268])).
% 0.14/0.85 fof(f308,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(meet(X0,X1),X0),X0)=join(meet(X0,X1),X0))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f305,f48])).
% 0.14/0.85 fof(f316,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f305,f210])).
% 0.14/0.85 fof(f322,plain,(
% 0.14/0.85 ~meet(b,a)=meet(a,b)|~join(b,a)=join(a,b)),
% 0.14/0.85 inference(trivial_equality_resolution,[status(thm)],[f306])).
% 0.14/0.85 fof(f332,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,X1),meet(X0,meet(X0,X1)))=meet(X0,meet(X0,X1)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f316,f196])).
% 0.14/0.85 fof(f334,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,X1),meet(X1,meet(X0,X1)))=meet(X1,meet(X0,X1)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f316,f76])).
% 0.14/0.85 fof(f336,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(join(X0,X1),X0))=meet(join(X0,X1),X0))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f316,f56])).
% 0.14/0.85 fof(f353,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f316,f332])).
% 0.14/0.85 fof(f364,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f316,f334])).
% 0.14/0.85 fof(f370,plain,(
% 0.14/0.85 ![X0,X1]: (X0=meet(join(X0,X1),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f316,f336])).
% 0.14/0.85 fof(f417,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,X1),X0)=meet(X0,join(meet(X0,X1),X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f39,f370])).
% 0.14/0.85 fof(f426,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(X0,join(join(X0,X1),X0)))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f370,f9])).
% 0.14/0.85 fof(f529,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,meet(X0,join(join(X0,X1),X0))),meet(meet(X0,join(join(X0,X1),X0)),X0))=meet(X0,join(join(X0,X1),X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f426,f9])).
% 0.14/0.85 fof(f530,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,meet(X0,join(join(X0,X1),X0))),meet(X0,X0))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f426,f7])).
% 0.14/0.85 fof(f539,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,join(join(X0,X1),X0)),meet(meet(X0,join(join(X0,X1),X0)),X0))=meet(X0,join(join(X0,X1),X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f353,f529])).
% 0.14/0.85 fof(f540,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,join(join(X0,X1),X0)),X0)=meet(X0,join(join(X0,X1),X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f107,f539])).
% 0.14/0.85 fof(f541,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,join(join(X0,X1),X0)),meet(X0,X0))=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f353,f530])).
% 0.14/0.85 fof(f542,plain,(
% 0.14/0.85 ![X0,X1]: (X0=meet(X0,join(join(X0,X1),X0)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f543,f540])).
% 0.14/0.85 fof(f543,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,join(join(X0,X1),X0)),X0)=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f237,f541])).
% 0.14/0.85 fof(f556,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,join(join(X0,X1),X0))=meet(join(join(X0,X1),X0),X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f542,f364])).
% 0.14/0.85 fof(f572,plain,(
% 0.14/0.85 ![X0,X1]: (X0=meet(join(join(X0,X1),X0),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f542,f556])).
% 0.14/0.85 fof(f583,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=meet(join(X0,meet(X0,X1)),meet(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f7,f572])).
% 0.14/0.85 fof(f693,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(X0,meet(X0,join(X1,X0))),meet(X0,join(X1,X0)))=join(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(X1,X0))))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f107,f308])).
% 0.14/0.85 fof(f705,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,join(meet(X0,X1),X0))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f308,f316])).
% 0.14/0.85 fof(f719,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,join(X1,X0))=join(meet(meet(X0,join(X1,X0)),X0),meet(X0,join(X1,X0))))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f583,f693])).
% 0.14/0.85 fof(f723,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X0,join(X1,X0))))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f107,f719])).
% 0.14/0.85 fof(f781,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(join(X0,X1),X0),join(X0,X1))=meet(join(X0,X1),join(X0,join(X0,X1))))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f370,f417])).
% 0.14/0.85 fof(f790,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(meet(X0,X1),X0),X0)=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f417,f107])).
% 0.14/0.85 fof(f804,plain,(
% 0.14/0.85 ![X0,X1]: (join(join(meet(X0,X1),X0),meet(join(meet(X0,X1),X0),join(X0,join(meet(X0,X1),X0))))=join(meet(X0,X1),X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f417,f9])).
% 0.14/0.85 fof(f813,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,join(X0,X1))=meet(join(X0,X1),join(X0,join(X0,X1))))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f370,f781])).
% 0.14/0.85 fof(f842,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(meet(X0,X1),X0),join(X0,join(meet(X0,X1),X0)))=join(meet(X0,X1),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f723,f804])).
% 0.14/0.85 fof(f843,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(meet(X0,X1),X0),X0)=join(meet(X0,X1),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f705,f842])).
% 0.14/0.85 fof(f848,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(meet(X0,join(X1,X0)),X0))=meet(X0,join(X1,X0)))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f856,f128])).
% 0.14/0.85 fof(f856,plain,(
% 0.14/0.85 ![X0,X1]: (X0=join(meet(X0,X1),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f790,f843])).
% 0.14/0.85 fof(f865,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 0.14/0.85 inference(backward_demodulation,[status(thm)],[f873,f813])).
% 0.14/0.85 fof(f873,plain,(
% 0.14/0.85 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f316,f848])).
% 0.14/0.85 fof(f912,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(meet(X0,X1),X0),meet(meet(X0,X1),X0))=meet(X0,X1))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f856,f7])).
% 0.14/0.85 fof(f917,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f305,f912])).
% 0.14/0.85 fof(f992,plain,(
% 0.14/0.85 ![X0,X1]: (join(meet(X0,join(X0,X1)),meet(X0,join(X0,X1)))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f865,f7])).
% 0.14/0.85 fof(f1001,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f305,f992])).
% 0.14/0.85 fof(f1022,plain,(
% 0.14/0.85 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1001,f316])).
% 0.14/0.85 fof(f1041,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X1)),meet(X1,join(X0,X1)))=meet(X1,join(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f873,f25])).
% 0.14/0.85 fof(f1079,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X1)),X1)=meet(X1,join(X0,X1)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f873,f1041])).
% 0.14/0.85 fof(f1080,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X1)),X1)=X1)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f873,f1079])).
% 0.14/0.85 fof(f1417,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f917,f316])).
% 0.14/0.85 fof(f1459,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1417,f25])).
% 0.14/0.85 fof(f1649,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X1,X2)),X1)=X1)),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1022,f1080])).
% 0.14/0.85 fof(f2284,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(meet(X0,X1),meet(X1,X0)),meet(X0,X1))=meet(meet(X1,X0),meet(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1459,f1459])).
% 0.14/0.85 fof(f2308,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=join(meet(X1,X0),meet(X0,X1)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1459,f856])).
% 0.14/0.85 fof(f2333,plain,(
% 0.14/0.85 ![X0,X1]: (meet(meet(X0,X1),meet(X1,X0))=meet(meet(X1,X0),meet(X0,X1)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f917,f2284])).
% 0.14/0.85 fof(f2334,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),meet(X1,X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f1459,f2333])).
% 0.14/0.85 fof(f2723,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(meet(X0,meet(join(X1,X0),join(X0,X2))),X0)=meet(meet(join(X1,X0),join(X0,X2)),X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1649,f1459])).
% 0.14/0.85 fof(f2770,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X0,X2)))=meet(meet(join(X1,X0),join(X0,X2)),X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f917,f2723])).
% 0.14/0.85 fof(f2771,plain,(
% 0.14/0.85 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X0,X2)))=X0)),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f1649,f2770])).
% 0.14/0.85 fof(f3674,plain,(
% 0.14/0.85 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f1459,f2334])).
% 0.14/0.85 fof(f3763,plain,(
% 0.14/0.85 ~join(b,a)=join(a,b)),
% 0.14/0.85 inference(backward_subsumption_resolution,[status(thm)],[f322,f3674])).
% 0.14/0.85 fof(f5049,plain,(
% 0.14/0.85 ![X0,X1]: (join(join(X0,X1),meet(join(X0,X1),join(X1,X0)))=meet(join(X0,X1),join(X1,X0)))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f2771,f38])).
% 0.14/0.85 fof(f5119,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,X1)=meet(join(X0,X1),join(X1,X0)))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f1417,f5049])).
% 0.14/0.85 fof(f5226,plain,(
% 0.14/0.85 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=join(join(X1,X0),meet(join(X0,X1),join(X1,X0))))),
% 0.14/0.85 inference(paramodulation,[status(thm)],[f5119,f2308])).
% 0.14/0.85 fof(f5323,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,X1)=join(join(X1,X0),meet(join(X0,X1),join(X1,X0))))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f5119,f5226])).
% 0.14/0.85 fof(f5325,plain,(
% 0.14/0.85 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 0.14/0.85 inference(forward_demodulation,[status(thm)],[f316,f5323])).
% 0.14/0.85 fof(f5326,plain,(
% 0.14/0.85 $false),
% 0.14/0.85 inference(backward_subsumption_resolution,[status(thm)],[f3763,f5325])).
% 0.14/0.85 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.87 % Elapsed time: 0.322927 seconds
% 0.14/0.87 % CPU time: 2.362677 seconds
% 0.14/0.87 % Total memory used: 112.161 MB
% 0.14/0.87 % Net memory used: 110.710 MB
%------------------------------------------------------------------------------