%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT007-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 : n008.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:07 PM UTC 2026
% Result : Unsatisfiable 22.34s 13.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT007-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/10.38 % Computer : n008.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sun Sep 20 23:05:51 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.39 % Drodi V4.1.1
% 22.34/13.27 % Refutation found
% 22.34/13.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.34/13.27 % SZS output start CNFRefutation for theBenchmark
% 22.34/13.27 fof(f1,axiom,(
% 22.34/13.27 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 22.34/13.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.34/13.27 fof(f2,axiom,(
% 22.34/13.27 (![X,Y,Z]: (meet(X,join(Y,Z)) = join(meet(Z,X),meet(Y,X)) ))),
% 22.34/13.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.34/13.27 fof(f3,negated_conjecture,(
% 22.34/13.27 join(join(a,b),c) != join(a,join(b,c)) ),
% 22.34/13.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.34/13.27 fof(f4,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 22.34/13.27 inference(cnf_transformation,[status(thm)],[f1])).
% 22.34/13.27 fof(f5,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(X1,X2))=join(meet(X2,X0),meet(X1,X0)))),
% 22.34/13.27 inference(cnf_transformation,[status(thm)],[f2])).
% 22.34/13.27 fof(f6,plain,(
% 22.34/13.27 ~join(join(a,b),c)=join(a,join(b,c))),
% 22.34/13.27 inference(cnf_transformation,[status(thm)],[f3])).
% 22.34/13.27 fof(f12,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,X0))=join(X0,meet(X2,join(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f5])).
% 22.34/13.27 fof(f13,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f5])).
% 22.34/13.27 fof(f14,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,join(X2,X0)))=meet(X0,X1))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f5,f4])).
% 22.34/13.27 fof(f15,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X0,meet(join(X0,X1),join(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f12])).
% 22.34/13.27 fof(f19,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=join(meet(X3,join(X0,X1)),join(X1,meet(X0,join(X1,X2)))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f12,f5])).
% 22.34/13.27 fof(f20,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(join(X1,meet(X0,join(X1,X3))),meet(X2,join(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f12,f5])).
% 22.34/13.27 fof(f21,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X0,join(meet(X1,join(X0,X1)),X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f13,f15])).
% 22.34/13.27 fof(f28,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X0,X2),X3))=join(meet(X3,join(X0,X1)),join(meet(X1,join(X0,X2)),X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f13,f5])).
% 22.34/13.27 fof(f35,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X0),join(X1,join(X0,X2)))=join(join(X0,X0),meet(X1,join(X0,X0))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f20])).
% 22.34/13.27 fof(f63,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(X0,X1))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f14])).
% 22.34/13.27 fof(f86,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=join(meet(X2,X0),meet(X1,X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f63,f5])).
% 22.34/13.27 fof(f87,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=join(meet(X2,X0),meet(X1,X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f63,f5])).
% 22.34/13.27 fof(f94,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(X0,join(X1,X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f5,f86])).
% 22.34/13.27 fof(f96,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f5,f87])).
% 22.34/13.27 fof(f99,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),meet(join(X0,X1),join(X2,join(X1,X3))))=meet(join(X0,X1),join(join(X1,meet(X0,join(X1,X3))),X2)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f20,f96])).
% 22.34/13.27 fof(f100,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,meet(X0,join(X1,X2)))=meet(X0,join(meet(X2,X0),X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f5,f96])).
% 22.34/13.27 fof(f117,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=meet(join(X0,X1),join(join(X1,meet(X0,join(X1,X2))),X3)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f118,f99])).
% 22.34/13.27 fof(f118,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,meet(X0,join(X1,X2)))=meet(X0,join(X2,X1)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f94,f100])).
% 22.34/13.27 fof(f128,plain,(
% 22.34/13.27 ![X0]: (join(X0,X0)=join(join(X0,X0),meet(join(X0,X0),join(X0,X0))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f4,f35])).
% 22.34/13.27 fof(f151,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,join(X1,X1)))=join(join(join(X1,X1),meet(X0,join(X1,X1))),meet(X3,join(X0,join(X1,X2)))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f35,f5])).
% 22.34/13.27 fof(f152,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X0),meet(join(X0,X0),join(X1,join(X0,X2))))=meet(join(X0,X0),join(join(X0,X0),X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f35,f96])).
% 22.34/13.27 fof(f163,plain,(
% 22.34/13.27 ![X0]: (join(X0,X0)=join(join(X0,X0),join(meet(X0,join(X0,X0)),X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f13,f128])).
% 22.34/13.27 fof(f164,plain,(
% 22.34/13.27 ![X0]: (join(X0,X0)=join(join(X0,X0),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f163])).
% 22.34/13.27 fof(f203,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X0),join(join(X0,X1),X2))=meet(join(X0,X0),join(join(X0,X0),X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f118,f152])).
% 22.34/13.27 fof(f205,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X0),join(join(X0,X1),X2))=join(X0,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f203])).
% 22.34/13.27 fof(f210,plain,(
% 22.34/13.27 ![X0,X1]: (join(meet(X0,X1),meet(X0,X1))=join(meet(X1,join(X0,X0)),join(meet(X0,X1),meet(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f5,f164])).
% 22.34/13.27 fof(f222,plain,(
% 22.34/13.27 ![X0,X1]: (meet(join(X0,X0),join(join(X0,X0),X1))=join(meet(X1,join(join(X0,X0),join(X0,X0))),join(X0,X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f164,f13])).
% 22.34/13.27 fof(f228,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X1))=join(meet(X0,join(X1,X1)),join(meet(X1,X0),meet(X1,X0))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f5,f210])).
% 22.34/13.27 fof(f229,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X1))=join(meet(X0,join(X1,X1)),meet(X0,join(X1,X1))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f5,f228])).
% 22.34/13.27 fof(f231,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X1))=meet(join(X1,X1),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f5,f229])).
% 22.34/13.27 fof(f256,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X0)=join(meet(X1,join(join(X0,X0),join(X0,X0))),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f222])).
% 22.34/13.27 fof(f257,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X0)=join(meet(X1,join(X0,X0)),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f164,f256])).
% 22.34/13.27 fof(f379,plain,(
% 22.34/13.27 ![X0]: (meet(X0,join(X0,X0))=join(meet(X0,join(X0,X0)),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f13,f231])).
% 22.34/13.27 fof(f381,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,join(X1,X1)),join(X1,X1))=meet(join(X1,X1),join(meet(X0,join(X1,X1)),X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f96,f231])).
% 22.34/13.27 fof(f398,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,join(X1,X1)),join(X0,X0))=meet(join(X1,X1),join(X0,X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f231,f63])).
% 22.34/13.27 fof(f407,plain,(
% 22.34/13.27 ![X0]: (X0=join(meet(X0,join(X0,X0)),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f379])).
% 22.34/13.27 fof(f412,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X0),join(join(X0,X1),X2))=X0)),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f452,f205])).
% 22.34/13.27 fof(f431,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X0)=join(meet(X1,join(X0,X0)),X0))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f452,f257])).
% 22.34/13.27 fof(f441,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,join(X1,X1)))=join(join(join(X1,X1),meet(X0,X1)),meet(X3,join(X0,join(X1,X2)))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f452,f151])).
% 22.34/13.27 fof(f452,plain,(
% 22.34/13.27 ![X0]: (X0=join(X0,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f407])).
% 22.34/13.27 fof(f455,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X1))=meet(join(X1,X1),join(meet(X0,join(X1,X1)),X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f63,f381])).
% 22.34/13.27 fof(f456,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,X1)=meet(join(X1,X1),join(meet(X0,join(X1,X1)),X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f455])).
% 22.34/13.27 fof(f457,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,X1)=meet(join(X1,X1),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f94,f456])).
% 22.34/13.27 fof(f458,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,X1)=meet(X1,join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f457])).
% 22.34/13.27 fof(f459,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f458])).
% 22.34/13.27 fof(f516,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,X1),join(X0,X0))=meet(join(X1,X1),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f398])).
% 22.34/13.27 fof(f517,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(join(X1,X1),join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f516])).
% 22.34/13.27 fof(f518,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X1,join(X0,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f517])).
% 22.34/13.27 fof(f519,plain,(
% 22.34/13.27 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X1,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f518])).
% 22.34/13.27 fof(f536,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(join(X0,X1),X2))=X0)),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f412])).
% 22.34/13.27 fof(f567,plain,(
% 22.34/13.27 ![X0,X1]: (X0=join(meet(X1,join(X0,X0)),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f431])).
% 22.34/13.27 fof(f571,plain,(
% 22.34/13.27 ![X0,X1]: (X0=join(meet(X1,X0),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f567])).
% 22.34/13.27 fof(f615,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,X1))=join(join(join(X1,X1),meet(X0,X1)),meet(X3,join(X0,join(X1,X2)))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f441])).
% 22.34/13.27 fof(f616,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,X1))=join(join(X1,meet(X0,X1)),meet(X3,join(X0,join(X1,X2)))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f615])).
% 22.34/13.27 fof(f649,plain,(
% 22.34/13.27 ![X0,X1]: (meet(join(X0,X1),X0)=join(meet(X0,join(X0,X1)),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f452,f13])).
% 22.34/13.27 fof(f652,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X1,join(X0,X0))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f452,f12])).
% 22.34/13.27 fof(f653,plain,(
% 22.34/13.27 ![X0]: (meet(X0,X0)=X0)),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f452,f4])).
% 22.34/13.27 fof(f663,plain,(
% 22.34/13.27 ![X0,X1]: (meet(join(X0,X1),X0)=join(X0,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f4,f649])).
% 22.34/13.27 fof(f664,plain,(
% 22.34/13.27 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f663])).
% 22.34/13.27 fof(f669,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X0,join(join(X1,meet(X0,X1)),X0)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f670,f21])).
% 22.34/13.27 fof(f670,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X1,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f452,f652])).
% 22.34/13.27 fof(f672,plain,(
% 22.34/13.27 ![X0,X1]: (join(meet(X0,join(X1,X0)),X1)=join(X1,X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f13,f653])).
% 22.34/13.27 fof(f684,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f685,f669])).
% 22.34/13.27 fof(f685,plain,(
% 22.34/13.27 ![X0,X1]: (join(join(X0,meet(X1,X0)),X1)=join(X1,X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f670,f672])).
% 22.34/13.27 fof(f699,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f63,f459])).
% 22.34/13.27 fof(f701,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=meet(join(X1,X0),join(X0,X2)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f12,f459])).
% 22.34/13.27 fof(f747,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),X0)=join(X0,meet(meet(X2,X0),join(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f571,f12])).
% 22.34/13.27 fof(f760,plain,(
% 22.34/13.27 ![X0,X1,X2]: (X0=join(X0,meet(meet(X1,X0),join(X0,X2))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f664,f747])).
% 22.34/13.27 fof(f994,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,join(X1,X0))=meet(X0,join(X1,join(X0,X2))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f664,f96])).
% 22.34/13.27 fof(f1018,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,X0))=meet(X0,join(X1,join(X0,X2))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f670,f994])).
% 22.34/13.27 fof(f1083,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X1,X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f459,f519])).
% 22.34/13.27 fof(f1089,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(meet(X0,join(X1,X2)),X1),join(X1,X2))=meet(join(X1,X0),join(X1,X2)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f13,f519])).
% 22.34/13.27 fof(f1120,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(meet(X1,join(X0,X2)),join(X0,X2)))=meet(join(X0,X1),join(X0,X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f701,f1089])).
% 22.34/13.27 fof(f1121,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1123,f13])).
% 22.34/13.27 fof(f1123,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=meet(join(X0,X1),join(X0,X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f63,f1120])).
% 22.34/13.27 fof(f1172,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X0,X2),X3))=join(meet(X3,join(X0,X1)),join(X0,meet(X2,join(X0,X1)))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1121,f28])).
% 22.34/13.27 fof(f1276,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(join(X0,X1),X2),join(X0,X1))=join(join(X0,X1),meet(X0,join(join(X0,X1),X2))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f684,f12])).
% 22.34/13.27 fof(f1289,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(join(X0,X1),meet(X0,join(join(X0,X1),X2))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f664,f1276])).
% 22.34/13.27 fof(f1294,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(join(X0,X1),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f536,f1289])).
% 22.34/13.27 fof(f1316,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,meet(X0,X1)))=meet(meet(X0,X1),join(X2,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f699,f96])).
% 22.34/13.27 fof(f1319,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(meet(X0,X1),join(X1,X2))=join(meet(X2,meet(X0,X1)),meet(X0,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f699,f5])).
% 22.34/13.27 fof(f1345,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,meet(X0,X1)))=meet(meet(X0,X1),join(X2,X1)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f670,f1316])).
% 22.34/13.27 fof(f1350,plain,(
% 22.34/13.27 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1351,f760])).
% 22.34/13.27 fof(f1351,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(meet(X0,X1),join(X1,X2))=meet(X0,X1))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f571,f1319])).
% 22.34/13.27 fof(f1354,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X2,X1)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1350,f1345])).
% 22.34/13.27 fof(f1357,plain,(
% 22.34/13.27 ![X0,X1,X2]: (X0=meet(X0,join(X1,join(X0,X2))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1350,f1018])).
% 22.34/13.27 fof(f1358,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1350,f685])).
% 22.34/13.27 fof(f1359,plain,(
% 22.34/13.27 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1350,f670])).
% 22.34/13.27 fof(f1368,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,X1))=join(X1,meet(X3,join(X0,join(X1,X2)))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f1350,f616])).
% 22.34/13.27 fof(f1459,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1358,f684])).
% 22.34/13.27 fof(f1460,plain,(
% 22.34/13.27 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1358,f664])).
% 22.34/13.27 fof(f1501,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(join(X0,X1),X1))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1359,f1350])).
% 22.34/13.27 fof(f1867,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (join(join(X0,meet(X1,join(X0,X2))),meet(X3,join(X1,X0)))=join(meet(join(X1,X0),join(X3,join(X0,X2))),join(X0,meet(X1,join(X0,X2)))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f20,f1294])).
% 22.34/13.27 fof(f1875,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(join(X1,X0),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1358,f1294])).
% 22.34/13.27 fof(f1893,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(meet(join(X0,X1),join(X2,join(X1,X3))),join(X1,meet(X0,join(X1,X3)))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f20,f1867])).
% 22.34/13.27 fof(f1983,plain,(
% 22.34/13.27 ![X0,X1]: (join(X0,X1)=join(join(X1,X0),X1))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1358,f1501])).
% 22.34/13.27 fof(f2100,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,join(X1,X2))))=join(join(X1,meet(X0,join(X1,X2))),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f12,f1121])).
% 22.34/13.27 fof(f2103,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(meet(X1,X2),join(X0,X2)))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f96,f1121])).
% 22.34/13.27 fof(f2119,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(join(X1,X0),join(X0,X2)))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1459,f1121])).
% 22.34/13.27 fof(f2148,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(join(X1,meet(X0,join(X1,X2))),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1357,f2100])).
% 22.34/13.27 fof(f2152,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1354,f2103])).
% 22.34/13.27 fof(f2176,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,join(X0,meet(X1,join(X0,X2))))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f701,f2119])).
% 22.34/13.27 fof(f2177,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=join(meet(X2,join(X0,X1)),X0))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f684,f2176])).
% 22.34/13.27 fof(f2178,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(join(X1,meet(X0,X3)),meet(X2,join(X0,X1))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f20])).
% 22.34/13.27 fof(f2179,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,X0))=join(X0,meet(X2,X1)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f12])).
% 22.34/13.27 fof(f2199,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(join(X1,meet(X0,X2)),X0))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f2148])).
% 22.34/13.27 fof(f2200,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(meet(join(X0,X1),join(X2,join(X1,X3))),join(X1,meet(X0,X3))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f1893])).
% 22.34/13.27 fof(f2211,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X0,X2),X3))=join(meet(X3,join(X0,X1)),join(X0,meet(X2,X1))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f1172])).
% 22.34/13.27 fof(f2221,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,X2))=meet(join(X0,X1),join(X0,X2)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f1123])).
% 22.34/13.27 fof(f2228,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=meet(join(X0,X1),join(join(X1,meet(X0,X2)),X3)))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f117])).
% 22.34/13.27 fof(f2236,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=join(meet(X3,join(X0,X1)),join(X1,meet(X0,X2))))),
% 22.34/13.27 inference(backward_demodulation,[status(thm)],[f2237,f19])).
% 22.34/13.27 fof(f2237,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=join(X0,meet(X1,X2)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f2152,f2177])).
% 22.34/13.27 fof(f2394,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,join(X0,X1)))=join(join(X0,X1),meet(X2,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1501,f2179])).
% 22.34/13.27 fof(f2408,plain,(
% 22.34/13.27 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(join(X0,X2),X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1294,f2179])).
% 22.34/13.27 fof(f2445,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(join(X0,X1),meet(X2,X1)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1359,f2394])).
% 22.34/13.27 fof(f2458,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(join(X0,X2),X1)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f2221,f2408])).
% 22.34/13.27 fof(f3722,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(X0,X2))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1358,f2199])).
% 22.34/13.27 fof(f3744,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(join(X2,X1),join(X0,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1460,f2199])).
% 22.34/13.27 fof(f3840,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(join(X0,X1),X1)=join(join(X0,X1),meet(X2,X1)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1501,f2445])).
% 22.34/13.27 fof(f3905,plain,(
% 22.34/13.27 ![X0,X1,X2]: (join(X0,X1)=join(join(X1,X0),meet(X2,X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1875,f3840])).
% 22.34/13.27 fof(f5565,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(join(X0,X1),X0),join(X2,join(X0,X3)))=join(join(X0,meet(join(X0,X1),X3)),meet(X2,join(X0,X1))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f1294,f2178])).
% 22.34/13.27 fof(f5592,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),meet(join(X0,X1),join(X2,join(X1,X3))))=meet(join(X0,X1),join(join(X1,meet(X0,X3)),X2)))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f2178,f96])).
% 22.34/13.27 fof(f5605,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (join(meet(X0,join(X1,X2)),join(X2,meet(X1,X3)))=join(meet(join(X1,X2),join(X0,join(X2,X3))),join(X2,meet(X1,X3))))),
% 22.34/13.27 inference(paramodulation,[status(thm)],[f2178,f1983])).
% 22.34/13.27 fof(f5722,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(join(X1,meet(join(X1,X0),X3)),meet(X2,join(X1,X0))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1983,f5565])).
% 22.34/13.27 fof(f5723,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(join(X1,meet(X3,X0)),meet(X2,join(X1,X0))))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f2458,f5722])).
% 22.34/13.27 fof(f5769,plain,(
% 22.34/13.27 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X3,X1))=meet(join(X3,X1),join(join(X1,meet(X3,X2)),X0)))),
% 22.34/13.27 inference(forward_demodulation,[status(thm)],[f1083,f5592])).
% 22.34/13.27 fof(f5770,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=join(X1,meet(X0,join(X3,join(X1,X2)))))),
% 22.34/13.30 inference(backward_demodulation,[status(thm)],[f5771,f2228])).
% 22.34/13.30 fof(f5771,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,join(X0,X3))))=meet(join(X1,X0),join(join(X0,meet(X1,X3)),X2)))),
% 22.34/13.30 inference(forward_demodulation,[status(thm)],[f1368,f5769])).
% 22.34/13.30 fof(f5786,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X1,X2),X3))=join(meet(join(X0,X1),join(X3,join(X1,X2))),join(X1,meet(X0,X2))))),
% 22.34/13.30 inference(forward_demodulation,[status(thm)],[f2236,f5605])).
% 22.34/13.30 fof(f5804,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,join(X0,X3))))=join(meet(join(X1,X0),join(X2,join(X0,X3))),join(X0,meet(X1,X3))))),
% 22.34/13.30 inference(backward_demodulation,[status(thm)],[f5770,f5786])).
% 22.34/13.30 fof(f5811,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X2,join(X1,X3)))=join(X1,meet(X0,join(X2,join(X1,X3)))))),
% 22.34/13.30 inference(backward_demodulation,[status(thm)],[f5804,f2200])).
% 22.34/13.30 fof(f5848,plain,(
% 22.34/13.30 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,join(X0,X3))))=join(join(X0,meet(X3,X1)),meet(X2,join(X0,X1))))),
% 22.34/13.31 inference(backward_demodulation,[status(thm)],[f5811,f5723])).
% 22.34/13.31 fof(f6134,plain,(
% 22.34/13.31 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 22.34/13.31 inference(paramodulation,[status(thm)],[f3905,f3722])).
% 22.34/13.31 fof(f10885,plain,(
% 22.34/13.31 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X0,X2),X3))=join(join(X0,meet(X2,X1)),meet(X3,join(X0,X1))))),
% 22.34/13.31 inference(paramodulation,[status(thm)],[f1358,f2211])).
% 22.34/13.31 fof(f10905,plain,(
% 22.34/13.31 ![X0,X1,X2]: (meet(join(X0,X1),join(join(X0,X2),X1))=join(X1,join(X0,meet(X2,X1))))),
% 22.34/13.31 inference(paramodulation,[status(thm)],[f1359,f2211])).
% 22.34/13.31 fof(f11089,plain,(
% 22.34/13.31 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(join(X0,X2),X3))=join(X0,meet(X1,join(X3,join(X0,X2)))))),
% 22.34/13.31 inference(forward_demodulation,[status(thm)],[f5848,f10885])).
% 22.34/13.31 fof(f11130,plain,(
% 22.34/13.31 ![X0,X1,X2]: (join(X0,meet(X1,join(X1,join(X0,X2))))=join(X1,join(X0,meet(X2,X1))))),
% 22.34/13.31 inference(forward_demodulation,[status(thm)],[f11089,f10905])).
% 22.34/13.31 fof(f11131,plain,(
% 22.34/13.31 ![X0,X1,X2]: (join(X0,X1)=join(X1,join(X0,meet(X2,X1))))),
% 22.34/13.31 inference(forward_demodulation,[status(thm)],[f4,f11130])).
% 22.34/13.31 fof(f11564,plain,(
% 22.34/13.31 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X2),join(X0,X2)))),
% 22.34/13.31 inference(paramodulation,[status(thm)],[f1359,f11131])).
% 22.34/13.31 fof(f11653,plain,(
% 22.34/13.31 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X2,X1)))),
% 22.34/13.31 inference(backward_demodulation,[status(thm)],[f11564,f3744])).
% 22.34/13.31 fof(f11693,plain,(
% 22.34/13.31 ~join(a,join(c,b))=join(a,join(b,c))),
% 22.34/13.31 inference(backward_demodulation,[status(thm)],[f11653,f6])).
% 22.34/13.31 fof(f12081,plain,(
% 22.34/13.31 $false),
% 22.34/13.31 inference(forward_subsumption_resolution,[status(thm)],[f11693,f6134])).
% 22.34/13.31 % SZS output end CNFRefutation for theBenchmark.p
% 23.32/14.54 % Elapsed time: 3.930521 seconds
% 23.32/14.54 % CPU time: 10.046083 seconds
% 23.32/14.54 % Total memory used: 97.733 MB
% 23.32/14.54 % Net memory used: 93.326 MB
%------------------------------------------------------------------------------