%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT153-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:18 PM UTC 2026
% Result : Unsatisfiable 169.89s 27.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT153-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.43 % Computer : n026.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Sun Sep 20 23:18:58 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.44 % Drodi V4.1.1
% 169.89/27.06 % Refutation found
% 169.89/27.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 169.89/27.06 % SZS output start CNFRefutation for theBenchmark
% 169.89/27.06 fof(f1,axiom,(
% 169.89/27.06 (![X]: (meet(X,X) = X ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f2,axiom,(
% 169.89/27.06 (![X]: (join(X,X) = X ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f3,axiom,(
% 169.89/27.06 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f4,axiom,(
% 169.89/27.06 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f5,axiom,(
% 169.89/27.06 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f6,axiom,(
% 169.89/27.06 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f7,axiom,(
% 169.89/27.06 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f8,axiom,(
% 169.89/27.06 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f9,axiom,(
% 169.89/27.06 (![X,Y,Z,U]: (meet(X,join(Y,meet(Z,join(X,U)))) = meet(X,join(Y,meet(Z,join(U,meet(Z,join(X,Y)))))) ))),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f10,negated_conjecture,(
% 169.89/27.06 meet(a,join(b,meet(a,c))) != meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b)))))) ),
% 169.89/27.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 169.89/27.06 fof(f11,plain,(
% 169.89/27.06 ![X0]: (meet(X0,X0)=X0)),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f1])).
% 169.89/27.06 fof(f12,plain,(
% 169.89/27.06 ![X0]: (join(X0,X0)=X0)),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f2])).
% 169.89/27.06 fof(f13,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f3])).
% 169.89/27.06 fof(f14,plain,(
% 169.89/27.06 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f4])).
% 169.89/27.06 fof(f15,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f5])).
% 169.89/27.06 fof(f16,plain,(
% 169.89/27.06 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f6])).
% 169.89/27.06 fof(f17,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f7])).
% 169.89/27.06 fof(f18,plain,(
% 169.89/27.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f8])).
% 169.89/27.06 fof(f19,plain,(
% 169.89/27.06 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,join(X0,X3))))=meet(X0,join(X1,meet(X2,join(X3,meet(X2,join(X0,X1)))))))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f9])).
% 169.89/27.06 fof(f20,plain,(
% 169.89/27.06 ~meet(a,join(b,meet(a,c)))=meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b))))))),
% 169.89/27.06 inference(cnf_transformation,[status(thm)],[f10])).
% 169.89/27.06 fof(f21,definition,(
% 169.89/27.06 sF2_fnc=meet(a,c)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 169.89/27.06 fof(f22,definition,(
% 169.89/27.06 sF1_fnc=join(b,sF2_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 169.89/27.06 fof(f23,definition,(
% 169.89/27.06 sF0_fnc=meet(a,sF1_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 169.89/27.06 fof(f24,definition,(
% 169.89/27.06 sF7_fnc=meet(a,b)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 169.89/27.06 fof(f25,definition,(
% 169.89/27.06 sF9_fnc=join(a,b)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF9_fnc])],[function_definition])).
% 169.89/27.06 fof(f26,definition,(
% 169.89/27.06 sF8_fnc=meet(c,sF9_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition])).
% 169.89/27.06 fof(f27,definition,(
% 169.89/27.06 sF6_fnc=join(sF7_fnc,sF8_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 169.89/27.06 fof(f28,definition,(
% 169.89/27.06 sF5_fnc=meet(a,sF6_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 169.89/27.06 fof(f29,definition,(
% 169.89/27.06 sF4_fnc=join(b,sF5_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 169.89/27.06 fof(f30,definition,(
% 169.89/27.06 sF3_fnc=meet(a,sF4_fnc)),
% 169.89/27.06 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 169.89/27.06 fof(f31,plain,(
% 169.89/27.06 ~sF0_fnc=sF3_fnc),
% 169.89/27.06 inference(definition_folding,[],[f20,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21])).
% 169.89/27.06 fof(f45,plain,(
% 169.89/27.06 join(a,sF2_fnc)=a),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f21,f14])).
% 169.89/27.06 fof(f53,plain,(
% 169.89/27.06 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f15,f14])).
% 169.89/27.06 fof(f68,plain,(
% 169.89/27.06 join(sF9_fnc,sF8_fnc)=sF9_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f26,f53])).
% 169.89/27.06 fof(f72,plain,(
% 169.89/27.06 join(b,sF7_fnc)=b),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f24,f53])).
% 169.89/27.06 fof(f83,plain,(
% 169.89/27.06 join(sF8_fnc,sF9_fnc)=sF9_fnc),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f16,f68])).
% 169.89/27.06 fof(f91,plain,(
% 169.89/27.06 meet(sF8_fnc,sF9_fnc)=sF8_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f83,f13])).
% 169.89/27.06 fof(f98,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f16,f13])).
% 169.89/27.06 fof(f101,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f15,f17])).
% 169.89/27.06 fof(f108,plain,(
% 169.89/27.06 ![X0]: (meet(sF8_fnc,X0)=meet(c,meet(sF9_fnc,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f26,f17])).
% 169.89/27.06 fof(f111,plain,(
% 169.89/27.06 ![X0]: (meet(sF5_fnc,X0)=meet(a,meet(sF6_fnc,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f28,f17])).
% 169.89/27.06 fof(f112,plain,(
% 169.89/27.06 ![X0]: (meet(sF7_fnc,X0)=meet(a,meet(b,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f24,f17])).
% 169.89/27.06 fof(f114,plain,(
% 169.89/27.06 ![X0]: (meet(sF2_fnc,X0)=meet(a,meet(c,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f21,f17])).
% 169.89/27.06 fof(f118,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f11,f17])).
% 169.89/27.06 fof(f120,plain,(
% 169.89/27.06 ![X0,X1,X2]: (join(X0,meet(X1,meet(X2,X0)))=X0)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f17,f53])).
% 169.89/27.06 fof(f137,plain,(
% 169.89/27.06 ![X0]: (join(sF6_fnc,X0)=join(sF7_fnc,join(sF8_fnc,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f27,f18])).
% 169.89/27.06 fof(f144,plain,(
% 169.89/27.06 ![X0]: (join(sF9_fnc,X0)=join(a,join(b,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f25,f18])).
% 169.89/27.06 fof(f166,plain,(
% 169.89/27.06 ![X0]: (join(b,X0)=join(b,join(sF7_fnc,X0)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f72,f18])).
% 169.89/27.06 fof(f177,plain,(
% 169.89/27.06 ![X0]: (meet(sF8_fnc,X0)=meet(c,meet(X0,sF9_fnc)))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f15,f108])).
% 169.89/27.06 fof(f204,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f18,f98])).
% 169.89/27.06 fof(f217,plain,(
% 169.89/27.06 meet(b,sF9_fnc)=b),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f25,f98])).
% 169.89/27.06 fof(f224,plain,(
% 169.89/27.06 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f14,f98])).
% 169.89/27.06 fof(f248,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f17,f224])).
% 169.89/27.06 fof(f273,plain,(
% 169.89/27.06 ![X0,X1,X2,X3,X4]: (meet(X0,join(X1,meet(meet(X2,X3),join(X0,X4))))=meet(X0,join(X1,meet(X2,meet(X3,join(X4,meet(meet(X2,X3),join(X0,X1))))))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f17,f19])).
% 169.89/27.06 fof(f281,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,join(X0,meet(X2,join(X0,X1))))))=meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f12,f19])).
% 169.89/27.06 fof(f304,plain,(
% 169.89/27.06 ![X0,X1]: (meet(a,join(b,meet(X0,join(a,X1))))=meet(a,join(b,meet(X0,join(X1,meet(X0,sF9_fnc))))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f25,f19])).
% 169.89/27.06 fof(f323,plain,(
% 169.89/27.06 ![X0,X1,X2,X3,X4]: (meet(X0,join(X1,meet(X2,meet(X3,join(X0,X4)))))=meet(X0,join(X1,meet(X2,meet(X3,join(X4,meet(meet(X2,X3),join(X0,X1))))))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f17,f273])).
% 169.89/27.06 fof(f324,plain,(
% 169.89/27.06 ![X0,X1,X2,X3,X4]: (meet(X0,join(X1,meet(X2,meet(X3,join(X0,X4)))))=meet(X0,join(X1,meet(X2,meet(X3,join(X4,meet(X2,meet(X3,join(X0,X1)))))))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f17,f323])).
% 169.89/27.06 fof(f329,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,join(X0,X0))))=meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f19,f281])).
% 169.89/27.06 fof(f330,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,meet(X2,meet(X2,join(X0,X1))))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f12,f329])).
% 169.89/27.06 fof(f331,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,meet(X2,join(X0,X1)))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f118,f330])).
% 169.89/27.06 fof(f800,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,meet(meet(X1,X0),X1))=meet(X1,X0))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f11,f101])).
% 169.89/27.06 fof(f872,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,meet(X1,meet(X0,X1)))=meet(X1,X0))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f17,f800])).
% 169.89/27.06 fof(f873,plain,(
% 169.89/27.06 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f248,f872])).
% 169.89/27.06 fof(f977,plain,(
% 169.89/27.06 ![X0]: (meet(sF5_fnc,join(sF6_fnc,X0))=meet(a,sF6_fnc))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f13,f111])).
% 169.89/27.06 fof(f997,plain,(
% 169.89/27.06 ![X0]: (meet(sF5_fnc,join(sF6_fnc,X0))=sF5_fnc)),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f28,f977])).
% 169.89/27.06 fof(f1075,plain,(
% 169.89/27.06 meet(sF7_fnc,sF9_fnc)=meet(a,b)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f217,f112])).
% 169.89/27.06 fof(f1099,plain,(
% 169.89/27.06 meet(sF7_fnc,sF9_fnc)=sF7_fnc),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f24,f1075])).
% 169.89/27.06 fof(f1126,plain,(
% 169.89/27.06 join(sF9_fnc,sF7_fnc)=sF9_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f1099,f53])).
% 169.89/27.06 fof(f1132,plain,(
% 169.89/27.06 join(sF7_fnc,sF9_fnc)=sF9_fnc),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f16,f1126])).
% 169.89/27.06 fof(f1247,plain,(
% 169.89/27.06 ![X0]: (meet(sF2_fnc,join(X0,a))=sF2_fnc)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f45,f204])).
% 169.89/27.06 fof(f1262,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X0))=meet(X0,X1))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f14,f204])).
% 169.89/27.06 fof(f1290,plain,(
% 169.89/27.06 ![X0,X1,X2]: (meet(X0,meet(X1,join(X2,X0)))=meet(X0,X1))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f17,f1262])).
% 169.89/27.06 fof(f1356,plain,(
% 169.89/27.06 meet(sF2_fnc,sF9_fnc)=meet(a,sF8_fnc)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f26,f114])).
% 169.89/27.06 fof(f3006,plain,(
% 169.89/27.06 join(sF6_fnc,sF9_fnc)=join(sF7_fnc,sF9_fnc)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f83,f137])).
% 169.89/27.06 fof(f3027,plain,(
% 169.89/27.06 join(sF6_fnc,sF9_fnc)=sF9_fnc),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f1132,f3006])).
% 169.89/27.06 fof(f3047,plain,(
% 169.89/27.06 meet(sF5_fnc,sF9_fnc)=sF5_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f3027,f997])).
% 169.89/27.06 fof(f3057,plain,(
% 169.89/27.06 meet(sF6_fnc,sF9_fnc)=sF6_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f3027,f13])).
% 169.89/27.06 fof(f3070,plain,(
% 169.89/27.06 join(sF9_fnc,sF5_fnc)=sF9_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f3047,f53])).
% 169.89/27.06 fof(f3081,plain,(
% 169.89/27.06 join(sF5_fnc,sF9_fnc)=sF9_fnc),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f16,f3070])).
% 169.89/27.06 fof(f3842,plain,(
% 169.89/27.06 ![X0]: (meet(sF2_fnc,join(a,X0))=sF2_fnc)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f16,f1247])).
% 169.89/27.06 fof(f4448,plain,(
% 169.89/27.06 join(sF9_fnc,sF5_fnc)=join(a,sF4_fnc)),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f29,f144])).
% 169.89/27.06 fof(f4487,plain,(
% 169.89/27.06 join(sF5_fnc,sF9_fnc)=join(a,sF4_fnc)),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f16,f4448])).
% 169.89/27.06 fof(f4489,plain,(
% 169.89/27.06 sF9_fnc=join(a,sF4_fnc)),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f3081,f4487])).
% 169.89/27.06 fof(f6938,plain,(
% 169.89/27.06 meet(sF2_fnc,sF9_fnc)=sF2_fnc),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f4489,f3842])).
% 169.89/27.06 fof(f6992,plain,(
% 169.89/27.06 sF2_fnc=meet(a,sF8_fnc)),
% 169.89/27.06 inference(backward_demodulation,[status(thm)],[f6938,f1356])).
% 169.89/27.06 fof(f9306,plain,(
% 169.89/27.06 ![X0]: (meet(a,join(b,meet(sF8_fnc,join(a,X0))))=meet(a,join(b,meet(sF8_fnc,join(X0,sF8_fnc)))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f91,f304])).
% 169.89/27.06 fof(f9310,plain,(
% 169.89/27.06 ![X0]: (meet(a,join(b,meet(sF6_fnc,join(a,X0))))=meet(a,join(b,meet(sF6_fnc,join(X0,sF6_fnc)))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f3057,f304])).
% 169.89/27.06 fof(f9401,plain,(
% 169.89/27.06 ![X0]: (meet(a,join(b,meet(sF8_fnc,join(a,X0))))=meet(a,join(b,sF8_fnc)))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f98,f9306])).
% 169.89/27.06 fof(f9409,plain,(
% 169.89/27.06 ![X0]: (meet(a,join(b,meet(sF6_fnc,join(a,X0))))=meet(a,join(b,sF6_fnc)))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f98,f9310])).
% 169.89/27.06 fof(f9853,plain,(
% 169.89/27.06 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,meet(X3,join(X0,X2)))))=meet(X0,join(X1,meet(X2,meet(X3,X2)))))),
% 169.89/27.06 inference(paramodulation,[status(thm)],[f14,f324])).
% 169.89/27.06 fof(f10119,plain,(
% 169.89/27.06 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,X3)))=meet(X0,join(X1,meet(X2,meet(X3,X2)))))),
% 169.89/27.06 inference(forward_demodulation,[status(thm)],[f1290,f9853])).
% 169.89/27.06 fof(f10120,plain,(
% 169.89/27.06 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,X3)))=meet(X0,join(X1,meet(X3,X2))))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f873,f10119])).
% 33.39/27.33 fof(f12824,plain,(
% 33.39/27.33 ![X0]: (meet(a,join(b,meet(X0,a)))=meet(a,join(b,meet(X0,sF9_fnc))))),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f25,f331])).
% 33.39/27.33 fof(f27648,plain,(
% 33.39/27.33 ![X0]: (join(sF9_fnc,meet(X0,sF6_fnc))=sF9_fnc)),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f3057,f120])).
% 33.39/27.33 fof(f31628,plain,(
% 33.39/27.33 ![X0]: (join(sF9_fnc,meet(sF8_fnc,X0))=sF9_fnc)),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f177,f120])).
% 33.39/27.33 fof(f32157,plain,(
% 33.39/27.33 ![X0]: (join(sF9_fnc,meet(sF6_fnc,X0))=sF9_fnc)),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f15,f27648])).
% 33.39/27.33 fof(f37880,plain,(
% 33.39/27.33 meet(a,join(b,meet(sF8_fnc,join(a,sF9_fnc))))=meet(a,join(b,meet(sF8_fnc,sF9_fnc)))),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f31628,f304])).
% 33.39/27.33 fof(f37961,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=meet(a,join(b,meet(sF8_fnc,sF9_fnc)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f9401,f37880])).
% 33.39/27.33 fof(f37962,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=meet(a,join(b,meet(sF8_fnc,a)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f12824,f37961])).
% 33.39/27.33 fof(f37963,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=meet(a,join(b,meet(a,sF8_fnc)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f10120,f37962])).
% 33.39/27.33 fof(f37964,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=meet(a,join(b,sF2_fnc))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f6992,f37963])).
% 33.39/27.33 fof(f37965,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=meet(a,sF1_fnc)),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f22,f37964])).
% 33.39/27.33 fof(f37967,plain,(
% 33.39/27.33 meet(a,join(b,sF8_fnc))=sF0_fnc),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f23,f37965])).
% 33.39/27.33 fof(f38711,plain,(
% 33.39/27.33 meet(a,join(b,meet(sF6_fnc,join(a,sF9_fnc))))=meet(a,join(b,meet(sF6_fnc,sF9_fnc)))),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f32157,f304])).
% 33.39/27.33 fof(f38794,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=meet(a,join(b,meet(sF6_fnc,sF9_fnc)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f9409,f38711])).
% 33.39/27.33 fof(f38795,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=meet(a,join(b,meet(sF6_fnc,a)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f12824,f38794])).
% 33.39/27.33 fof(f38796,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=meet(a,join(b,meet(a,sF6_fnc)))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f10120,f38795])).
% 33.39/27.33 fof(f38797,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=meet(a,join(b,sF5_fnc))),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f28,f38796])).
% 33.39/27.33 fof(f38798,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=meet(a,sF4_fnc)),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f29,f38797])).
% 33.39/27.33 fof(f38800,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=sF3_fnc),
% 33.39/27.33 inference(forward_demodulation,[status(thm)],[f30,f38798])).
% 33.39/27.33 fof(f45191,plain,(
% 33.39/27.33 join(b,sF8_fnc)=join(b,sF6_fnc)),
% 33.39/27.33 inference(paramodulation,[status(thm)],[f27,f166])).
% 33.39/27.33 fof(f45267,plain,(
% 33.39/27.33 meet(a,join(b,sF6_fnc))=sF0_fnc),
% 33.39/27.33 inference(backward_demodulation,[status(thm)],[f45191,f37967])).
% 33.39/27.33 fof(f45410,plain,(
% 33.39/27.33 sF0_fnc=sF3_fnc),
% 33.39/27.33 inference(backward_demodulation,[status(thm)],[f45267,f38800])).
% 33.39/27.33 fof(f45415,plain,(
% 33.39/27.33 $false),
% 33.39/27.33 inference(forward_subsumption_resolution,[status(thm)],[f45410,f31])).
% 33.39/27.33 % SZS output end CNFRefutation for theBenchmark.p
% 33.39/27.36 % Elapsed time: 21.910356 seconds
% 33.39/27.36 % CPU time: 172.944025 seconds
% 33.39/27.36 % Total memory used: 792.390 MB
% 33.39/27.36 % Net memory used: 779.607 MB
%------------------------------------------------------------------------------