%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT089-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:14 PM UTC 2026
% Result : Unsatisfiable 0.02s 0.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT089-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Sun Sep 20 23:12:00 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.37 % Drodi V4.1.1
% 0.02/0.50 % Refutation found
% 0.02/0.50 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.50 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.50 fof(f1,axiom,(
% 0.02/0.50 (![A,B]: (join(meet(A,B),meet(A,join(A,B))) = A ))),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f2,axiom,(
% 0.02/0.50 (![A,B]: (join(meet(A,A),meet(B,join(A,A))) = A ))),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f3,axiom,(
% 0.02/0.50 (![A,B]: (join(meet(A,B),meet(B,join(A,B))) = B ))),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f4,axiom,(
% 0.02/0.50 (![A,B,C]: (meet(meet(join(A,B),join(C,A)),A) = A ))),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f5,axiom,(
% 0.02/0.50 (![A,B,C]: (join(join(meet(A,B),meet(C,A)),A) = A ))),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f6,negated_conjecture,(
% 0.02/0.50 meet(b,a) != meet(a,b) ),
% 0.02/0.50 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.02/0.50 fof(f7,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,X1),meet(X0,join(X0,X1)))=X0)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.50 fof(f8,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,X0),meet(X1,join(X0,X0)))=X0)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.50 fof(f9,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,X1),meet(X1,join(X0,X1)))=X1)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.50 fof(f10,plain,(
% 0.02/0.50 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X0)),X0)=X0)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f4])).
% 0.02/0.50 fof(f11,plain,(
% 0.02/0.50 ![X0,X1,X2]: (join(join(meet(X0,X1),meet(X2,X0)),X0)=X0)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f5])).
% 0.02/0.50 fof(f12,plain,(
% 0.02/0.50 ~meet(b,a)=meet(a,b)),
% 0.02/0.50 inference(cnf_transformation,[status(thm)],[f6])).
% 0.02/0.50 fof(f13,definition,(
% 0.02/0.50 sF0_fnc=meet(b,a)),
% 0.02/0.50 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.02/0.50 fof(f14,definition,(
% 0.02/0.50 sF1_fnc=meet(a,b)),
% 0.02/0.50 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.02/0.50 fof(f15,plain,(
% 0.02/0.50 ~sF0_fnc=sF1_fnc),
% 0.02/0.50 inference(definition_folding,[],[f12,f14,f13])).
% 0.02/0.50 fof(f17,plain,(
% 0.02/0.50 ![X0,X1,X2]: (meet(meet(join(meet(X0,join(X1,X1)),X2),X1),meet(X0,join(X1,X1)))=meet(X0,join(X1,X1)))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f8,f10])).
% 0.02/0.50 fof(f18,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,X0),join(X0,X0))=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f10,f8])).
% 0.02/0.50 fof(f22,plain,(
% 0.02/0.50 ![X0,X1,X2]: (join(X0,meet(meet(join(X0,X1),join(X2,X0)),join(meet(join(X0,X1),join(X2,X0)),X0)))=meet(join(X0,X1),join(X2,X0)))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f10,f7])).
% 0.02/0.50 fof(f25,plain,(
% 0.02/0.50 ![X0]: (join(meet(meet(X0,X0),join(X0,X0)),meet(meet(X0,X0),X0))=meet(X0,X0))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f18,f7])).
% 0.02/0.50 fof(f26,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(meet(X0,X1),meet(X0,join(X0,X1))),meet(meet(X0,X1),X0))=meet(X0,X1))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f7,f7])).
% 0.02/0.50 fof(f27,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(meet(X0,X0),meet(X1,join(X0,X0))),meet(meet(X0,X0),X0))=meet(X0,X0))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f8,f7])).
% 0.02/0.50 fof(f73,plain,(
% 0.02/0.50 join(sF1_fnc,meet(b,join(a,b)))=b),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f14,f9])).
% 0.02/0.50 fof(f74,plain,(
% 0.02/0.50 join(sF0_fnc,meet(a,join(b,a)))=a),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f13,f9])).
% 0.02/0.50 fof(f82,plain,(
% 0.02/0.50 ![X0]: (join(meet(meet(X0,X0),join(X0,X0)),meet(join(X0,X0),X0))=join(X0,X0))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f18,f9])).
% 0.02/0.50 fof(f96,plain,(
% 0.02/0.50 ![X0]: (meet(meet(b,join(X0,sF1_fnc)),sF1_fnc)=sF1_fnc)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f73,f10])).
% 0.02/0.50 fof(f102,plain,(
% 0.02/0.50 ![X0]: (meet(meet(a,join(X0,sF0_fnc)),sF0_fnc)=sF0_fnc)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f74,f10])).
% 0.02/0.50 fof(f126,plain,(
% 0.02/0.50 ![X0,X1]: (join(join(meet(X0,X1),X0),X0)=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f10,f11])).
% 0.02/0.50 fof(f127,plain,(
% 0.02/0.50 ![X0]: (join(join(meet(b,X0),sF1_fnc),b)=b)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f14,f11])).
% 0.02/0.50 fof(f128,plain,(
% 0.02/0.50 ![X0]: (join(join(meet(a,X0),sF0_fnc),a)=a)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f13,f11])).
% 0.02/0.50 fof(f139,plain,(
% 0.02/0.50 ![X0,X1]: (meet(meet(join(X0,X1),X0),X0)=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f11,f10])).
% 0.02/0.50 fof(f280,plain,(
% 0.02/0.50 join(join(sF0_fnc,b),b)=b),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f13,f126])).
% 0.02/0.50 fof(f309,plain,(
% 0.02/0.50 join(meet(join(sF0_fnc,b),b),meet(join(sF0_fnc,b),b))=join(sF0_fnc,b)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f280,f7])).
% 0.02/0.50 fof(f313,plain,(
% 0.02/0.50 ![X0,X1]: (meet(meet(join(X0,X0),X0),meet(X1,join(X0,X0)))=meet(X1,join(X0,X0)))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f9,f17])).
% 0.02/0.50 fof(f367,plain,(
% 0.02/0.50 ![X0,X1]: (join(join(X0,X0),meet(meet(join(join(X0,X0),X1),X0),join(meet(join(join(X0,X0),X1),join(meet(X0,X0),join(X0,X0))),join(X0,X0))))=meet(join(join(X0,X0),X1),join(meet(X0,X0),join(X0,X0))))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f18,f22])).
% 0.02/0.50 fof(f413,plain,(
% 0.02/0.50 ![X0,X1,X2]: (meet(meet(meet(join(X0,X1),join(X2,X0)),X0),X0)=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f22,f139])).
% 0.02/0.50 fof(f487,plain,(
% 0.02/0.50 ![X0,X1]: (join(join(X0,X0),meet(meet(join(join(X0,X0),X1),X0),join(meet(join(join(X0,X0),X1),X0),join(X0,X0))))=meet(join(join(X0,X0),X1),join(meet(X0,X0),join(X0,X0))))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f18,f367])).
% 0.02/0.50 fof(f490,plain,(
% 0.02/0.50 ![X0,X1]: (join(join(X0,X0),meet(meet(join(join(X0,X0),X1),X0),join(meet(join(join(X0,X0),X1),X0),join(X0,X0))))=meet(join(join(X0,X0),X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f18,f487])).
% 0.02/0.50 fof(f584,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(X1,join(X0,X0)))=X0)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f594,f8])).
% 0.02/0.50 fof(f591,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,join(X0,X0)),meet(join(X0,X0),X0))=join(X0,X0))),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f594,f82])).
% 0.02/0.50 fof(f592,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(meet(X0,X0),meet(X1,join(X0,X0))),meet(meet(X0,X0),X0))=X0)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f594,f27])).
% 0.02/0.50 fof(f593,plain,(
% 0.02/0.50 ![X0]: (join(meet(meet(X0,X0),join(X0,X0)),meet(meet(X0,X0),X0))=X0)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f594,f25])).
% 0.02/0.50 fof(f594,plain,(
% 0.02/0.50 ![X0]: (meet(X0,X0)=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f10,f413])).
% 0.02/0.50 fof(f601,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,meet(X1,join(X0,X0))),meet(meet(X0,X0),X0))=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f592])).
% 0.02/0.50 fof(f602,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,meet(X1,join(X0,X0))),meet(X0,X0))=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f601])).
% 0.02/0.50 fof(f603,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,meet(X1,join(X0,X0))),X0)=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f602])).
% 0.02/0.50 fof(f604,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,join(X0,X0)),meet(meet(X0,X0),X0))=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f593])).
% 0.02/0.50 fof(f605,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,join(X0,X0)),meet(X0,X0))=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f604])).
% 0.02/0.50 fof(f608,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,join(X0,X0)),X0)=X0)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f605])).
% 0.02/0.50 fof(f622,plain,(
% 0.02/0.50 ![X0,X1]: (meet(meet(X0,join(X1,X0)),X0)=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f584,f10])).
% 0.02/0.50 fof(f692,plain,(
% 0.02/0.50 join(join(sF0_fnc,sF1_fnc),b)=b),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f13,f127])).
% 0.02/0.50 fof(f729,plain,(
% 0.02/0.50 join(join(sF1_fnc,sF0_fnc),a)=a),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f14,f128])).
% 0.02/0.50 fof(f754,plain,(
% 0.02/0.50 join(meet(join(sF1_fnc,sF0_fnc),a),meet(join(sF1_fnc,sF0_fnc),a))=join(sF1_fnc,sF0_fnc)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f729,f7])).
% 0.02/0.50 fof(f1121,plain,(
% 0.02/0.50 ![X0]: (meet(join(X0,X0),X0)=X0)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f594,f10])).
% 0.02/0.50 fof(f1141,plain,(
% 0.02/0.50 ![X0]: (join(meet(X0,join(X0,X0)),X0)=join(X0,X0))),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1121,f591])).
% 0.02/0.50 fof(f1142,plain,(
% 0.02/0.50 ![X0,X1]: (meet(X0,meet(X1,join(X0,X0)))=meet(X1,join(X0,X0)))),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1121,f313])).
% 0.02/0.50 fof(f1155,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1188,f584])).
% 0.02/0.50 fof(f1165,plain,(
% 0.02/0.50 meet(join(sF0_fnc,b),b)=join(sF0_fnc,b)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1188,f309])).
% 0.02/0.50 fof(f1167,plain,(
% 0.02/0.50 meet(join(sF1_fnc,sF0_fnc),a)=join(sF1_fnc,sF0_fnc)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1188,f754])).
% 0.02/0.50 fof(f1177,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,meet(X1,X0)),X0)=X0)),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1188,f603])).
% 0.02/0.50 fof(f1181,plain,(
% 0.02/0.50 ![X0,X1]: (join(join(X0,X0),meet(meet(join(join(X0,X0),X1),X0),join(meet(join(join(X0,X0),X1),X0),join(X0,X0))))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(backward_demodulation,[status(thm)],[f1188,f490])).
% 0.02/0.50 fof(f1188,plain,(
% 0.02/0.50 ![X0]: (X0=join(X0,X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f608,f1141])).
% 0.02/0.50 fof(f1189,plain,(
% 0.02/0.50 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,join(X0,X0)))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1142])).
% 0.02/0.50 fof(f1191,plain,(
% 0.02/0.50 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1189])).
% 0.02/0.50 fof(f1242,plain,(
% 0.02/0.50 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1191,f1177])).
% 0.02/0.50 fof(f1249,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(meet(join(join(X0,X0),X1),X0),join(meet(join(join(X0,X0),X1),X0),join(X0,X0))))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1181])).
% 0.02/0.50 fof(f1250,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(meet(join(X0,X1),X0),join(meet(join(join(X0,X0),X1),X0),join(X0,X0))))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1249])).
% 0.02/0.50 fof(f1251,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(meet(join(X0,X1),X0),join(meet(join(X0,X1),X0),join(X0,X0))))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1250])).
% 0.02/0.50 fof(f1252,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(meet(join(X0,X1),X0),join(meet(join(X0,X1),X0),X0)))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f1251])).
% 0.02/0.50 fof(f1253,plain,(
% 0.02/0.50 ![X0,X1]: (join(X0,meet(meet(join(X0,X1),X0),X0))=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1242,f1252])).
% 0.02/0.50 fof(f1256,plain,(
% 0.02/0.50 ![X0,X1]: (X0=meet(join(X0,X1),X0))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1155,f1253])).
% 0.02/0.50 fof(f1575,plain,(
% 0.02/0.50 join(sF0_fnc,sF1_fnc)=meet(b,join(sF0_fnc,sF1_fnc))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f692,f1256])).
% 0.02/0.50 fof(f1576,plain,(
% 0.02/0.50 join(sF0_fnc,b)=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f280,f1256])).
% 0.02/0.50 fof(f3343,plain,(
% 0.02/0.50 meet(join(sF0_fnc,sF1_fnc),sF1_fnc)=sF1_fnc),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f1575,f96])).
% 0.02/0.50 fof(f3385,plain,(
% 0.02/0.50 join(sF1_fnc,meet(join(sF0_fnc,sF1_fnc),join(join(sF0_fnc,sF1_fnc),sF1_fnc)))=join(sF0_fnc,sF1_fnc)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f3343,f7])).
% 0.02/0.50 fof(f3783,plain,(
% 0.02/0.50 join(b,join(sF0_fnc,b))=b),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f1165,f1155])).
% 0.02/0.50 fof(f3812,plain,(
% 0.02/0.50 join(meet(meet(b,join(sF0_fnc,b)),meet(b,b)),meet(meet(b,join(sF0_fnc,b)),b))=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f3783,f26])).
% 0.02/0.50 fof(f3819,plain,(
% 0.02/0.50 join(meet(b,join(sF0_fnc,b)),meet(join(sF0_fnc,b),b))=join(sF0_fnc,b)),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f3783,f9])).
% 0.02/0.50 fof(f3829,plain,(
% 0.02/0.50 join(meet(join(sF0_fnc,b),meet(b,b)),meet(meet(b,join(sF0_fnc,b)),b))=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1576,f3812])).
% 0.02/0.50 fof(f3830,plain,(
% 0.02/0.50 join(meet(join(sF0_fnc,b),b),meet(meet(b,join(sF0_fnc,b)),b))=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f594,f3829])).
% 0.02/0.50 fof(f3831,plain,(
% 0.02/0.50 join(join(sF0_fnc,b),meet(meet(b,join(sF0_fnc,b)),b))=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1165,f3830])).
% 0.02/0.50 fof(f3832,plain,(
% 0.02/0.50 join(join(sF0_fnc,b),b)=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f622,f3831])).
% 0.02/0.50 fof(f3834,plain,(
% 0.02/0.50 b=meet(b,join(sF0_fnc,b))),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f280,f3832])).
% 0.02/0.50 fof(f3844,plain,(
% 0.02/0.50 join(b,meet(join(sF0_fnc,b),b))=join(sF0_fnc,b)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f3834,f3819])).
% 0.02/0.50 fof(f3856,plain,(
% 0.02/0.50 b=join(sF0_fnc,b)),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1155,f3844])).
% 0.02/0.50 fof(f3889,plain,(
% 0.02/0.50 join(meet(sF0_fnc,b),meet(sF0_fnc,b))=sF0_fnc),
% 0.02/0.50 inference(paramodulation,[status(thm)],[f3856,f7])).
% 0.02/0.50 fof(f3928,plain,(
% 0.02/0.50 meet(sF0_fnc,b)=sF0_fnc),
% 0.02/0.50 inference(forward_demodulation,[status(thm)],[f1188,f3889])).
% 0.02/0.51 fof(f3998,plain,(
% 0.02/0.51 join(b,sF0_fnc)=b),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f3928,f1155])).
% 0.02/0.51 fof(f4058,plain,(
% 0.02/0.51 meet(meet(a,b),sF0_fnc)=sF0_fnc),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f3998,f102])).
% 0.02/0.51 fof(f4075,plain,(
% 0.02/0.51 meet(sF1_fnc,sF0_fnc)=sF0_fnc),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f14,f4058])).
% 0.02/0.51 fof(f4125,plain,(
% 0.02/0.51 join(join(sF0_fnc,sF1_fnc),sF1_fnc)=sF1_fnc),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f4075,f126])).
% 0.02/0.51 fof(f4141,plain,(
% 0.02/0.51 join(sF1_fnc,meet(join(sF0_fnc,sF1_fnc),sF1_fnc))=join(sF0_fnc,sF1_fnc)),
% 0.02/0.51 inference(backward_demodulation,[status(thm)],[f4125,f3385])).
% 0.02/0.51 fof(f4166,plain,(
% 0.02/0.51 sF1_fnc=join(sF0_fnc,sF1_fnc)),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f1155,f4141])).
% 0.02/0.51 fof(f4207,plain,(
% 0.02/0.51 join(meet(sF0_fnc,sF1_fnc),meet(sF0_fnc,sF1_fnc))=sF0_fnc),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f4166,f7])).
% 0.02/0.51 fof(f4242,plain,(
% 0.02/0.51 meet(sF0_fnc,sF1_fnc)=sF0_fnc),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f1188,f4207])).
% 0.02/0.51 fof(f4256,plain,(
% 0.02/0.51 join(sF1_fnc,sF0_fnc)=sF1_fnc),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f4242,f1155])).
% 0.02/0.51 fof(f4283,plain,(
% 0.02/0.51 meet(join(sF1_fnc,sF0_fnc),a)=sF1_fnc),
% 0.02/0.51 inference(backward_demodulation,[status(thm)],[f4256,f1167])).
% 0.02/0.51 fof(f4319,plain,(
% 0.02/0.51 meet(sF1_fnc,a)=sF1_fnc),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f4256,f4283])).
% 0.02/0.51 fof(f4451,plain,(
% 0.02/0.51 join(a,sF1_fnc)=a),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f4319,f1155])).
% 0.02/0.51 fof(f4513,plain,(
% 0.02/0.51 meet(meet(b,a),sF1_fnc)=sF1_fnc),
% 0.02/0.51 inference(paramodulation,[status(thm)],[f4451,f96])).
% 0.02/0.51 fof(f4530,plain,(
% 0.02/0.51 meet(sF0_fnc,sF1_fnc)=sF1_fnc),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f13,f4513])).
% 0.02/0.51 fof(f4531,plain,(
% 0.02/0.51 sF0_fnc=sF1_fnc),
% 0.02/0.51 inference(forward_demodulation,[status(thm)],[f4242,f4530])).
% 0.02/0.51 fof(f4532,plain,(
% 0.02/0.51 $false),
% 0.02/0.51 inference(forward_subsumption_resolution,[status(thm)],[f4531,f15])).
% 0.02/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.53 % Elapsed time: 0.164395 seconds
% 0.02/0.53 % CPU time: 1.124859 seconds
% 0.02/0.53 % Total memory used: 48.938 MB
% 0.02/0.53 % Net memory used: 46.328 MB
%------------------------------------------------------------------------------