%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT170-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:19 PM UTC 2026
% Result : Unsatisfiable 42.49s 5.91s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT170-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41 % Computer : n020.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Sun Sep 20 23:18:18 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.42 % Drodi V4.1.1
% 42.49/5.91 % Refutation found
% 42.49/5.91 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 42.49/5.91 % SZS output start CNFRefutation for theBenchmark
% 42.49/5.91 fof(f1,axiom,(
% 42.49/5.91 (![X]: (meet(X,X) = X ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f2,axiom,(
% 42.49/5.91 (![X]: (join(X,X) = X ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f3,axiom,(
% 42.49/5.91 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f4,axiom,(
% 42.49/5.91 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f5,axiom,(
% 42.49/5.91 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f6,axiom,(
% 42.49/5.91 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f7,axiom,(
% 42.49/5.91 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f8,axiom,(
% 42.49/5.91 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f9,axiom,(
% 42.49/5.91 (![X,Y,Z,U]: (join(X,meet(Y,join(Z,meet(X,U)))) = join(X,meet(Y,meet(join(X,Z),join(Z,meet(Y,U))))) ))),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f10,negated_conjecture,(
% 42.49/5.91 meet(a,join(b,c)) != meet(a,join(b,meet(join(a,b),join(c,meet(a,b))))) ),
% 42.49/5.91 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.49/5.91 fof(f11,plain,(
% 42.49/5.91 ![X0]: (meet(X0,X0)=X0)),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f1])).
% 42.49/5.91 fof(f12,plain,(
% 42.49/5.91 ![X0]: (join(X0,X0)=X0)),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f2])).
% 42.49/5.91 fof(f13,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f3])).
% 42.49/5.91 fof(f14,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f4])).
% 42.49/5.91 fof(f15,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f5])).
% 42.49/5.91 fof(f16,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f6])).
% 42.49/5.91 fof(f17,plain,(
% 42.49/5.91 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f7])).
% 42.49/5.91 fof(f18,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f8])).
% 42.49/5.91 fof(f19,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,X3))))=join(X0,meet(X1,meet(join(X0,X2),join(X2,meet(X1,X3))))))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f9])).
% 42.49/5.91 fof(f20,plain,(
% 42.49/5.91 ~meet(a,join(b,c))=meet(a,join(b,meet(join(a,b),join(c,meet(a,b)))))),
% 42.49/5.91 inference(cnf_transformation,[status(thm)],[f10])).
% 42.49/5.91 fof(f21,definition,(
% 42.49/5.91 sF1_fnc=join(b,c)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 42.49/5.91 fof(f22,definition,(
% 42.49/5.91 sF0_fnc=meet(a,sF1_fnc)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 42.49/5.91 fof(f23,definition,(
% 42.49/5.91 sF5_fnc=join(a,b)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 42.49/5.91 fof(f24,definition,(
% 42.49/5.91 sF7_fnc=meet(a,b)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 42.49/5.91 fof(f25,definition,(
% 42.49/5.91 sF6_fnc=join(c,sF7_fnc)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 42.49/5.91 fof(f26,definition,(
% 42.49/5.91 sF4_fnc=meet(sF5_fnc,sF6_fnc)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 42.49/5.91 fof(f27,definition,(
% 42.49/5.91 sF3_fnc=join(b,sF4_fnc)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 42.49/5.91 fof(f28,definition,(
% 42.49/5.91 sF2_fnc=meet(a,sF3_fnc)),
% 42.49/5.91 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 42.49/5.91 fof(f29,plain,(
% 42.49/5.91 ~sF0_fnc=sF2_fnc),
% 42.49/5.91 inference(definition_folding,[],[f20,f28,f27,f26,f25,f24,f23,f22,f21])).
% 42.49/5.91 fof(f38,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f14])).
% 42.49/5.91 fof(f44,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f13])).
% 42.49/5.91 fof(f46,plain,(
% 42.49/5.91 meet(b,sF1_fnc)=b),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f21,f13])).
% 42.49/5.91 fof(f47,plain,(
% 42.49/5.91 join(a,sF0_fnc)=a),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f22,f14])).
% 42.49/5.91 fof(f50,plain,(
% 42.49/5.91 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(X1,join(meet(X0,X1),X2))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f13,f17])).
% 42.49/5.91 fof(f51,plain,(
% 42.49/5.91 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f17])).
% 42.49/5.91 fof(f55,plain,(
% 42.49/5.91 ![X0]: (meet(sF7_fnc,X0)=meet(a,meet(b,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f24,f17])).
% 42.49/5.91 fof(f56,plain,(
% 42.49/5.91 ![X0]: (meet(sF0_fnc,X0)=meet(a,meet(sF1_fnc,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f22,f17])).
% 42.49/5.91 fof(f60,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f11,f17])).
% 42.49/5.91 fof(f68,plain,(
% 42.49/5.91 meet(c,sF6_fnc)=c),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f25,f13])).
% 42.49/5.91 fof(f69,plain,(
% 42.49/5.91 ![X0]: (meet(sF4_fnc,X0)=meet(sF5_fnc,meet(sF6_fnc,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f26,f17])).
% 42.49/5.91 fof(f70,plain,(
% 42.49/5.91 join(sF5_fnc,sF4_fnc)=sF5_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f26,f14])).
% 42.49/5.91 fof(f71,plain,(
% 42.49/5.91 meet(b,sF3_fnc)=b),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f27,f13])).
% 42.49/5.91 fof(f75,plain,(
% 42.49/5.91 join(sF6_fnc,sF4_fnc)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f26,f38])).
% 42.49/5.91 fof(f76,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,meet(X2,X0)))=X0)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f17,f38])).
% 42.49/5.91 fof(f77,plain,(
% 42.49/5.91 join(sF3_fnc,sF2_fnc)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f28,f38])).
% 42.49/5.91 fof(f80,plain,(
% 42.49/5.91 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f13,f38])).
% 42.49/5.91 fof(f86,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f18,f80])).
% 42.49/5.91 fof(f88,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(join(X0,X1),X2))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f14,f18])).
% 42.49/5.91 fof(f89,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f18])).
% 42.49/5.91 fof(f93,plain,(
% 42.49/5.91 ![X0]: (join(sF6_fnc,X0)=join(c,join(sF7_fnc,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f25,f18])).
% 42.49/5.91 fof(f94,plain,(
% 42.49/5.91 ![X0]: (join(sF5_fnc,X0)=join(a,join(b,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f23,f18])).
% 42.49/5.91 fof(f95,plain,(
% 42.49/5.91 ![X0]: (join(sF3_fnc,X0)=join(b,join(sF4_fnc,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f27,f18])).
% 42.49/5.91 fof(f96,plain,(
% 42.49/5.91 ![X0]: (join(sF1_fnc,X0)=join(b,join(c,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f21,f18])).
% 42.49/5.91 fof(f114,plain,(
% 42.49/5.91 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f18,f44])).
% 42.49/5.91 fof(f115,plain,(
% 42.49/5.91 meet(sF7_fnc,sF6_fnc)=sF7_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f25,f44])).
% 42.49/5.91 fof(f116,plain,(
% 42.49/5.91 meet(b,sF5_fnc)=b),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f23,f44])).
% 42.49/5.91 fof(f117,plain,(
% 42.49/5.91 meet(sF4_fnc,sF3_fnc)=sF4_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f27,f44])).
% 42.49/5.91 fof(f118,plain,(
% 42.49/5.91 meet(c,sF1_fnc)=c),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f21,f44])).
% 42.49/5.91 fof(f120,plain,(
% 42.49/5.91 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f14,f44])).
% 42.49/5.91 fof(f131,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f17,f120])).
% 42.49/5.91 fof(f136,plain,(
% 42.49/5.91 meet(sF0_fnc,a)=sF0_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f47,f44])).
% 42.49/5.91 fof(f148,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,X3))))=join(X0,meet(X1,meet(join(X2,meet(X1,X3)),join(X0,X2)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f19])).
% 42.49/5.91 fof(f166,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,meet(X0,X2))))=join(X0,meet(X1,meet(join(X0,X2),X2))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f38,f19])).
% 42.49/5.91 fof(f168,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,X3))))=join(X0,meet(X1,meet(join(X0,X2),join(meet(X1,X3),X2)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f19])).
% 42.49/5.91 fof(f170,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,join(meet(X1,X2),meet(X0,X2))))=join(X0,meet(X1,meet(join(X0,meet(X1,X2)),meet(X1,X2)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f12,f19])).
% 42.49/5.91 fof(f176,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,meet(a,join(X1,meet(X0,b))))=join(X0,meet(a,meet(join(X0,X1),join(X1,sF7_fnc)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f24,f19])).
% 42.49/5.91 fof(f202,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X1,meet(join(X0,X2),X2))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f38,f166])).
% 42.49/5.91 fof(f205,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,join(meet(X1,X2),meet(X0,X2))))=join(X0,meet(X1,meet(X1,X2))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f202,f170])).
% 42.49/5.91 fof(f206,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,join(meet(X1,X2),meet(X0,X2))))=join(X0,meet(X1,X2)))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f60,f205])).
% 42.49/5.91 fof(f219,plain,(
% 42.49/5.91 join(sF6_fnc,c)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f68,f38])).
% 42.49/5.91 fof(f232,plain,(
% 42.49/5.91 join(sF3_fnc,b)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f71,f38])).
% 42.49/5.91 fof(f240,plain,(
% 42.49/5.91 join(sF4_fnc,sF6_fnc)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f75])).
% 42.49/5.91 fof(f314,plain,(
% 42.49/5.91 join(sF2_fnc,sF3_fnc)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f77])).
% 42.49/5.91 fof(f334,plain,(
% 42.49/5.91 meet(sF6_fnc,sF7_fnc)=sF7_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f115])).
% 42.49/5.91 fof(f379,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f11,f51])).
% 42.49/5.91 fof(f385,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,meet(meet(X1,X0),X1))=meet(X1,X0))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f11,f51])).
% 42.49/5.91 fof(f431,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,meet(X1,meet(X0,X1)))=meet(X1,X0))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f17,f385])).
% 42.49/5.91 fof(f432,plain,(
% 42.49/5.91 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f131,f431])).
% 42.49/5.91 fof(f476,plain,(
% 42.49/5.91 join(sF1_fnc,c)=sF1_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f118,f38])).
% 42.49/5.91 fof(f498,plain,(
% 42.49/5.91 ![X0]: (meet(sF0_fnc,X0)=meet(sF0_fnc,meet(a,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f136,f17])).
% 42.49/5.91 fof(f516,plain,(
% 42.49/5.91 meet(sF7_fnc,sF5_fnc)=meet(a,b)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f116,f55])).
% 42.49/5.91 fof(f518,plain,(
% 42.49/5.91 meet(sF7_fnc,sF1_fnc)=meet(a,b)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f46,f55])).
% 42.49/5.91 fof(f539,plain,(
% 42.49/5.91 meet(sF7_fnc,sF5_fnc)=sF7_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f24,f516])).
% 42.49/5.91 fof(f541,plain,(
% 42.49/5.91 meet(sF7_fnc,sF1_fnc)=sF7_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f24,f518])).
% 42.49/5.91 fof(f572,plain,(
% 42.49/5.91 join(c,sF6_fnc)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f219])).
% 42.49/5.91 fof(f597,plain,(
% 42.49/5.91 join(b,sF3_fnc)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f232])).
% 42.49/5.91 fof(f958,plain,(
% 42.49/5.91 join(c,sF1_fnc)=sF1_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f476])).
% 42.49/5.91 fof(f1116,plain,(
% 42.49/5.91 meet(sF5_fnc,sF7_fnc)=sF7_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f539])).
% 42.49/5.91 fof(f1152,plain,(
% 42.49/5.91 meet(sF1_fnc,sF7_fnc)=sF7_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f541])).
% 42.49/5.91 fof(f1420,plain,(
% 42.49/5.91 meet(sF4_fnc,sF7_fnc)=meet(sF5_fnc,sF7_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f334,f69])).
% 42.49/5.91 fof(f1448,plain,(
% 42.49/5.91 meet(sF4_fnc,sF7_fnc)=sF7_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f1116,f1420])).
% 42.49/5.91 fof(f2100,plain,(
% 42.49/5.91 ![X0]: (join(sF3_fnc,meet(X0,sF4_fnc))=sF3_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f117,f76])).
% 42.49/5.91 fof(f2150,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,X1)=join(X1,join(meet(X2,meet(X3,X1)),X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f76,f89])).
% 42.49/5.91 fof(f2151,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,meet(X2,X0)))=join(X0,join(meet(X1,meet(X2,X0)),meet(X0,X3))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f76,f88])).
% 42.49/5.91 fof(f2167,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (X0=join(X0,join(meet(X1,meet(X2,X0)),meet(X0,X3))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f76,f2151])).
% 42.49/5.91 fof(f2168,plain,(
% 42.49/5.91 ![X0,X1]: (X0=join(meet(X0,X1),X0))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f2150,f2167])).
% 42.49/5.91 fof(f2176,plain,(
% 42.49/5.91 sF1_fnc=join(sF7_fnc,sF1_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f1152,f2168])).
% 42.49/5.91 fof(f2186,plain,(
% 42.49/5.91 sF4_fnc=join(sF7_fnc,sF4_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f1448,f2168])).
% 42.49/5.91 fof(f2302,plain,(
% 42.49/5.91 join(sF6_fnc,sF1_fnc)=join(c,sF1_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2176,f93])).
% 42.49/5.91 fof(f2313,plain,(
% 42.49/5.91 join(sF6_fnc,sF1_fnc)=sF1_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f958,f2302])).
% 42.49/5.91 fof(f2387,plain,(
% 42.49/5.91 join(sF5_fnc,sF4_fnc)=join(a,sF3_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f27,f94])).
% 42.49/5.91 fof(f2415,plain,(
% 42.49/5.91 sF5_fnc=join(a,sF3_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f70,f2387])).
% 42.49/5.91 fof(f2454,plain,(
% 42.49/5.91 join(sF6_fnc,sF4_fnc)=join(c,sF4_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2186,f93])).
% 42.49/5.91 fof(f2465,plain,(
% 42.49/5.91 sF6_fnc=join(c,sF4_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f75,f2454])).
% 42.49/5.91 fof(f2520,plain,(
% 42.49/5.91 join(sF3_fnc,sF6_fnc)=join(b,sF6_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f240,f95])).
% 42.49/5.91 fof(f2684,plain,(
% 42.49/5.91 join(sF1_fnc,sF6_fnc)=sF1_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f2313])).
% 42.49/5.91 fof(f2695,plain,(
% 42.49/5.91 meet(sF6_fnc,sF1_fnc)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2313,f13])).
% 42.49/5.91 fof(f2713,plain,(
% 42.49/5.91 join(sF1_fnc,sF6_fnc)=join(b,sF6_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f572,f96])).
% 42.49/5.91 fof(f2741,plain,(
% 42.49/5.91 join(sF3_fnc,sF6_fnc)=sF1_fnc),
% 42.49/5.91 inference(backward_demodulation,[status(thm)],[f2742,f2520])).
% 42.49/5.91 fof(f2742,plain,(
% 42.49/5.91 sF1_fnc=join(b,sF6_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f2684,f2713])).
% 42.49/5.91 fof(f2813,plain,(
% 42.49/5.91 meet(sF1_fnc,sF6_fnc)=sF6_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f2695])).
% 42.49/5.91 fof(f2815,plain,(
% 42.49/5.91 meet(sF4_fnc,sF1_fnc)=meet(sF5_fnc,sF6_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2695,f69])).
% 42.49/5.91 fof(f2832,plain,(
% 42.49/5.91 meet(sF4_fnc,sF1_fnc)=sF4_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f26,f2815])).
% 42.49/5.91 fof(f3023,plain,(
% 42.49/5.91 meet(sF3_fnc,sF1_fnc)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2741,f13])).
% 42.49/5.91 fof(f3037,plain,(
% 42.49/5.91 meet(sF0_fnc,sF6_fnc)=meet(a,sF6_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2813,f56])).
% 42.49/5.91 fof(f3218,plain,(
% 42.49/5.91 meet(sF1_fnc,sF4_fnc)=sF4_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f2832])).
% 42.49/5.91 fof(f3268,plain,(
% 42.49/5.91 meet(sF1_fnc,sF3_fnc)=sF3_fnc),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f3023])).
% 42.49/5.91 fof(f3296,plain,(
% 42.49/5.91 meet(sF0_fnc,sF4_fnc)=meet(a,sF4_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f3218,f56])).
% 42.49/5.91 fof(f3555,plain,(
% 42.49/5.91 meet(sF0_fnc,sF3_fnc)=meet(a,sF3_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f3268,f56])).
% 42.49/5.91 fof(f3571,plain,(
% 42.49/5.91 meet(sF0_fnc,sF3_fnc)=sF2_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f28,f3555])).
% 42.49/5.91 fof(f4703,plain,(
% 42.49/5.91 join(sF4_fnc,sF6_fnc)=join(sF4_fnc,c)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2465,f86])).
% 42.49/5.91 fof(f4723,plain,(
% 42.49/5.91 join(c,sF1_fnc)=join(c,b)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f21,f86])).
% 42.49/5.91 fof(f4806,plain,(
% 42.49/5.91 sF6_fnc=join(sF4_fnc,c)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f240,f4703])).
% 42.49/5.91 fof(f4839,plain,(
% 42.49/5.91 sF1_fnc=join(c,b)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f958,f4723])).
% 42.49/5.91 fof(f5425,plain,(
% 42.49/5.91 join(sF3_fnc,c)=join(b,sF6_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f4806,f95])).
% 42.49/5.91 fof(f5443,plain,(
% 42.49/5.91 join(sF3_fnc,c)=sF1_fnc),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f2742,f5425])).
% 42.49/5.91 fof(f6691,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (meet(X0,X1)=meet(X1,meet(join(X2,join(X3,X1)),X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f114,f51])).
% 42.49/5.91 fof(f6692,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (meet(X0,join(X1,join(X2,X0)))=meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f114,f50])).
% 42.49/5.91 fof(f6739,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (X0=meet(X0,meet(join(X1,join(X2,X0)),join(X0,X3))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f114,f6692])).
% 42.49/5.91 fof(f6768,plain,(
% 42.49/5.91 ![X0,X1]: (X0=meet(join(X0,X1),X0))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f6691,f6739])).
% 42.49/5.91 fof(f6831,plain,(
% 42.49/5.91 sF2_fnc=meet(sF3_fnc,sF2_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f314,f6768])).
% 42.49/5.91 fof(f6878,plain,(
% 42.49/5.91 a=meet(sF5_fnc,a)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f2415,f6768])).
% 42.49/5.91 fof(f6890,plain,(
% 42.49/5.91 b=meet(sF3_fnc,b)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f597,f6768])).
% 42.49/5.91 fof(f6908,plain,(
% 42.49/5.91 ![X0,X1]: (X0=meet(join(X1,X0),X0))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16,f6768])).
% 42.49/5.91 fof(f7515,plain,(
% 42.49/5.91 ![X0]: (meet(X0,a)=meet(sF5_fnc,meet(a,X0)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f6878,f51])).
% 42.49/5.91 fof(f8946,plain,(
% 42.49/5.91 meet(sF3_fnc,sF2_fnc)=meet(sF3_fnc,sF0_fnc)),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f3571,f131])).
% 42.49/5.91 fof(f9028,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,meet(X3,X1)))))=join(X0,meet(X1,meet(join(X2,meet(X1,X3)),join(X0,X2)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f131,f148])).
% 42.49/5.91 fof(f9078,plain,(
% 42.49/5.91 sF2_fnc=meet(sF3_fnc,sF0_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f6831,f8946])).
% 42.49/5.91 fof(f9169,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,meet(X3,X1)))))=join(X0,meet(X1,join(X2,meet(X0,X3)))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f148,f9028])).
% 42.49/5.91 fof(f16315,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,meet(X3,X1)))))=join(X0,meet(X1,meet(join(X0,X2),join(meet(X3,X1),X2)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f432,f168])).
% 42.49/5.91 fof(f16602,plain,(
% 42.49/5.91 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,X3))))=join(X0,meet(X1,meet(join(X0,X2),join(meet(X3,X1),X2)))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f9169,f16315])).
% 42.49/5.91 fof(f16726,plain,(
% 42.49/5.91 meet(sF6_fnc,sF0_fnc)=meet(sF0_fnc,meet(a,sF6_fnc))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f3037,f379])).
% 42.49/5.91 fof(f16754,plain,(
% 42.49/5.91 meet(sF6_fnc,sF0_fnc)=meet(sF0_fnc,sF6_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f498,f16726])).
% 42.49/5.91 fof(f16757,plain,(
% 42.49/5.91 meet(sF6_fnc,sF0_fnc)=meet(a,sF6_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f3037,f16754])).
% 42.49/5.91 fof(f16782,plain,(
% 42.49/5.91 meet(sF4_fnc,sF0_fnc)=meet(sF0_fnc,meet(a,sF4_fnc))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f3296,f379])).
% 42.49/5.91 fof(f16810,plain,(
% 42.49/5.91 meet(sF4_fnc,sF0_fnc)=meet(sF0_fnc,sF4_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f498,f16782])).
% 42.49/5.91 fof(f16811,plain,(
% 42.49/5.91 meet(sF4_fnc,sF0_fnc)=meet(a,sF4_fnc)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f3296,f16810])).
% 42.49/5.91 fof(f17113,plain,(
% 42.49/5.91 ![X0,X1,X2]: (join(X0,meet(X1,join(meet(X2,X1),meet(X0,X2))))=join(X0,meet(X1,X2)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f15,f206])).
% 42.49/5.91 fof(f17827,plain,(
% 42.49/5.91 join(sF3_fnc,meet(a,join(c,meet(sF3_fnc,b))))=join(sF3_fnc,meet(a,meet(sF1_fnc,join(c,sF7_fnc))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f5443,f176])).
% 42.49/5.91 fof(f18111,plain,(
% 42.49/5.91 join(sF3_fnc,meet(a,join(c,b)))=join(sF3_fnc,meet(a,meet(sF1_fnc,join(c,sF7_fnc))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f6890,f17827])).
% 42.49/5.91 fof(f18112,plain,(
% 42.49/5.91 join(sF3_fnc,meet(a,sF1_fnc))=join(sF3_fnc,meet(a,meet(sF1_fnc,join(c,sF7_fnc))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f4839,f18111])).
% 42.49/5.91 fof(f18113,plain,(
% 42.49/5.91 join(sF3_fnc,sF0_fnc)=join(sF3_fnc,meet(a,meet(sF1_fnc,join(c,sF7_fnc))))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f22,f18112])).
% 42.49/5.91 fof(f18114,plain,(
% 42.49/5.91 join(sF3_fnc,sF0_fnc)=join(sF3_fnc,meet(sF0_fnc,join(c,sF7_fnc)))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f56,f18113])).
% 42.49/5.91 fof(f18115,plain,(
% 42.49/5.91 join(sF3_fnc,sF0_fnc)=join(sF3_fnc,meet(sF0_fnc,sF6_fnc))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f25,f18114])).
% 42.49/5.91 fof(f18116,plain,(
% 42.49/5.91 join(sF3_fnc,sF0_fnc)=join(sF3_fnc,meet(a,sF6_fnc))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f3037,f18115])).
% 42.49/5.91 fof(f18528,plain,(
% 42.49/5.91 meet(sF4_fnc,sF0_fnc)=meet(sF5_fnc,meet(a,sF6_fnc))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16757,f69])).
% 42.49/5.91 fof(f18530,plain,(
% 42.49/5.91 ![X0]: (join(X0,meet(sF6_fnc,join(meet(a,sF6_fnc),meet(X0,sF0_fnc))))=join(X0,meet(sF6_fnc,sF0_fnc)))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16757,f206])).
% 42.49/5.91 fof(f18531,plain,(
% 42.49/5.91 ![X0,X1]: (join(X0,meet(sF6_fnc,join(X1,meet(X0,sF0_fnc))))=join(X0,meet(sF6_fnc,meet(join(X0,X1),join(meet(a,sF6_fnc),X1)))))),
% 42.49/5.91 inference(paramodulation,[status(thm)],[f16757,f168])).
% 42.49/5.91 fof(f18568,plain,(
% 42.49/5.91 meet(a,sF4_fnc)=meet(sF5_fnc,meet(a,sF6_fnc))),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f16811,f18528])).
% 42.49/5.91 fof(f18569,plain,(
% 42.49/5.91 meet(a,sF4_fnc)=meet(sF6_fnc,a)),
% 42.49/5.91 inference(forward_demodulation,[status(thm)],[f7515,f18568])).
% 42.49/5.91 fof(f18570,plain,(
% 42.49/5.91 ![X0]: (join(X0,meet(sF6_fnc,join(meet(a,sF6_fnc),meet(X0,sF0_fnc))))=join(X0,meet(a,sF6_fnc)))),
% 43.36/6.00 inference(forward_demodulation,[status(thm)],[f16757,f18530])).
% 43.36/6.00 fof(f18571,plain,(
% 43.36/6.00 ![X0]: (join(X0,meet(sF6_fnc,join(meet(a,sF6_fnc),meet(X0,a))))=join(X0,meet(a,sF6_fnc)))),
% 43.36/6.00 inference(backward_demodulation,[status(thm)],[f18572,f18570])).
% 43.36/6.00 fof(f18572,plain,(
% 43.36/6.00 ![X0,X1]: (join(X0,meet(sF6_fnc,join(X1,meet(X0,sF0_fnc))))=join(X0,meet(sF6_fnc,join(X1,meet(X0,a)))))),
% 43.36/6.00 inference(forward_demodulation,[status(thm)],[f16602,f18531])).
% 43.36/6.00 fof(f18619,plain,(
% 43.36/6.00 ![X0]: (join(X0,meet(sF6_fnc,a))=join(X0,meet(a,sF6_fnc)))),
% 43.36/6.00 inference(forward_demodulation,[status(thm)],[f17113,f18571])).
% 43.36/6.00 fof(f18627,plain,(
% 43.36/6.00 join(sF3_fnc,sF0_fnc)=join(sF3_fnc,meet(a,sF4_fnc))),
% 43.36/6.00 inference(backward_demodulation,[status(thm)],[f18643,f18116])).
% 43.36/6.00 fof(f18643,plain,(
% 43.36/6.00 ![X0]: (join(X0,meet(a,sF4_fnc))=join(X0,meet(a,sF6_fnc)))),
% 43.36/6.00 inference(forward_demodulation,[status(thm)],[f18569,f18619])).
% 43.36/6.00 fof(f18648,plain,(
% 43.36/6.00 join(sF3_fnc,sF0_fnc)=sF3_fnc),
% 43.36/6.00 inference(forward_demodulation,[status(thm)],[f2100,f18627])).
% 43.36/6.00 fof(f18690,plain,(
% 43.36/6.00 sF0_fnc=meet(sF3_fnc,sF0_fnc)),
% 43.36/6.00 inference(paramodulation,[status(thm)],[f18648,f6908])).
% 43.36/6.00 fof(f18721,plain,(
% 43.36/6.00 sF2_fnc=sF0_fnc),
% 43.36/6.00 inference(backward_demodulation,[status(thm)],[f18690,f9078])).
% 43.36/6.00 fof(f18733,plain,(
% 43.36/6.00 $false),
% 43.36/6.00 inference(forward_subsumption_resolution,[status(thm)],[f18721,f29])).
% 43.36/6.00 % SZS output end CNFRefutation for theBenchmark.p
% 8.42/6.03 % Elapsed time: 5.593697 seconds
% 8.42/6.03 % CPU time: 43.940500 seconds
% 8.42/6.03 % Total memory used: 283.202 MB
% 8.42/6.03 % Net memory used: 278.956 MB
%------------------------------------------------------------------------------