%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT021-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:08 PM UTC 2026
% Result : Unsatisfiable 32.64s 4.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT021-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n019.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 23:07:04 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.36 % Drodi V4.1.1
% 32.64/4.56 % Refutation found
% 32.64/4.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 32.64/4.56 % SZS output start CNFRefutation for theBenchmark
% 32.64/4.56 fof(f1,axiom,(
% 32.64/4.56 (![X]: (meet(X,X) = X ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f2,axiom,(
% 32.64/4.56 (![X]: (join(X,X) = X ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f3,axiom,(
% 32.64/4.56 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f4,axiom,(
% 32.64/4.56 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f5,axiom,(
% 32.64/4.56 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f6,axiom,(
% 32.64/4.56 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f7,axiom,(
% 32.64/4.56 (![X,Y,Z]: (join(meet(X,join(Y,Z)),meet(X,Y)) = meet(X,join(Y,Z)) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f8,axiom,(
% 32.64/4.56 (![X,Y,Z]: (meet(join(X,meet(Y,Z)),join(X,Y)) = join(X,meet(Y,Z)) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f9,hypothesis,(
% 32.64/4.56 (![X,Y,Z]: (join(join(X,meet(Y,Z)),meet(join(X,Y),Z)) = join(X,meet(Y,Z)) ))),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f10,negated_conjecture,(
% 32.64/4.56 meet(a,join(b,c)) != join(meet(a,b),meet(a,c)) ),
% 32.64/4.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 32.64/4.56 fof(f11,plain,(
% 32.64/4.56 ![X0]: (meet(X0,X0)=X0)),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f1])).
% 32.64/4.56 fof(f12,plain,(
% 32.64/4.56 ![X0]: (join(X0,X0)=X0)),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f2])).
% 32.64/4.56 fof(f13,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f3])).
% 32.64/4.56 fof(f14,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f4])).
% 32.64/4.56 fof(f15,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f5])).
% 32.64/4.56 fof(f16,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f6])).
% 32.64/4.56 fof(f17,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),meet(X0,X1))=meet(X0,join(X1,X2)))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f7])).
% 32.64/4.56 fof(f18,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,meet(X1,X2)),join(X0,X1))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f8])).
% 32.64/4.56 fof(f19,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(join(X0,meet(X1,X2)),meet(join(X0,X1),X2))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f9])).
% 32.64/4.56 fof(f20,plain,(
% 32.64/4.56 ~meet(a,join(b,c))=join(meet(a,b),meet(a,c))),
% 32.64/4.56 inference(cnf_transformation,[status(thm)],[f10])).
% 32.64/4.56 fof(f27,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X1,X2)))=meet(X0,join(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f14,f17])).
% 32.64/4.56 fof(f28,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X1,X2)))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f13,f18])).
% 32.64/4.56 fof(f29,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(join(X0,X1),X2)))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f16,f19])).
% 32.64/4.56 fof(f38,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f15])).
% 32.64/4.56 fof(f42,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f15])).
% 32.64/4.56 fof(f44,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f11,f15])).
% 32.64/4.56 fof(f50,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f16])).
% 32.64/4.56 fof(f54,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f16])).
% 32.64/4.56 fof(f56,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f12,f16])).
% 32.64/4.56 fof(f65,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f44])).
% 32.64/4.56 fof(f82,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f56])).
% 32.64/4.56 fof(f152,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f15,f42])).
% 32.64/4.56 fof(f160,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(meet(X1,X0),meet(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f65,f42])).
% 32.64/4.56 fof(f186,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X0,X1),meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f160])).
% 32.64/4.56 fof(f187,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X0,meet(X1,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f186])).
% 32.64/4.56 fof(f203,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f16,f54])).
% 32.64/4.56 fof(f211,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(join(X1,X0),join(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f82,f54])).
% 32.64/4.56 fof(f237,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),join(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f54,f211])).
% 32.64/4.56 fof(f238,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,join(X1,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f54,f237])).
% 32.64/4.56 fof(f262,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X1,meet(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f11,f38])).
% 32.64/4.56 fof(f271,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f11,f38])).
% 32.64/4.56 fof(f278,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X2,X0),X1))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f38])).
% 32.64/4.56 fof(f307,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,meet(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f38,f44])).
% 32.64/4.56 fof(f313,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f187,f262])).
% 32.64/4.56 fof(f358,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X0,meet(X1,X2)))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f42,f313])).
% 32.64/4.56 fof(f386,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X2,X0))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f307,f358])).
% 32.64/4.56 fof(f420,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(meet(X1,X2),X0))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f42,f271])).
% 32.64/4.56 fof(f428,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X2),meet(X1,meet(X2,X0))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f15,f271])).
% 32.64/4.56 fof(f452,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X2,meet(X1,X0)))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f420])).
% 32.64/4.56 fof(f453,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X0),meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f386,f452])).
% 32.64/4.56 fof(f454,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X1,meet(X1,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f453])).
% 32.64/4.56 fof(f455,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f271,f454])).
% 32.64/4.56 fof(f463,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,meet(X1,meet(X2,X0)))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f428])).
% 32.64/4.56 fof(f464,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(meet(X2,X0),X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f271,f463])).
% 32.64/4.56 fof(f465,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X0,meet(X2,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f464])).
% 32.64/4.56 fof(f504,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,join(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f12,f50])).
% 32.64/4.56 fof(f513,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f12,f50])).
% 32.64/4.56 fof(f549,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,join(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f50,f56])).
% 32.64/4.56 fof(f555,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f238,f504])).
% 32.64/4.56 fof(f600,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X0,join(X1,X2)))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f54,f555])).
% 32.64/4.56 fof(f628,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X2,X0))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f549,f600])).
% 32.64/4.56 fof(f662,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(join(X1,X2),X0))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f54,f513])).
% 32.64/4.56 fof(f694,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X2,join(X1,X0)))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f54,f662])).
% 32.64/4.56 fof(f695,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X0),join(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f628,f694])).
% 32.64/4.56 fof(f696,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X1,join(X1,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f54,f695])).
% 32.64/4.56 fof(f697,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f513,f696])).
% 32.64/4.56 fof(f739,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(meet(X0,X1),join(X2,X3)))=meet(meet(X0,X1),join(X2,X3)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f15,f27])).
% 32.64/4.56 fof(f745,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(meet(X0,X1),X2)))=meet(X0,join(meet(X0,X1),X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f44,f27])).
% 32.64/4.56 fof(f746,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,join(X0,X2)))=meet(X1,join(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f27])).
% 32.64/4.56 fof(f748,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X0,join(X0,X1)))=meet(X0,join(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f11,f27])).
% 32.64/4.56 fof(f753,plain,(
% 32.64/4.56 ![X0,X1]: (join(meet(join(X0,X1),X0),join(X0,X1))=meet(join(X0,X1),join(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f11,f27])).
% 32.64/4.56 fof(f757,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,X1)))=meet(X0,join(X1,join(X1,X2))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f513,f27])).
% 32.64/4.56 fof(f761,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X1,X2)))=meet(X0,join(X1,join(X2,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f82,f27])).
% 32.64/4.56 fof(f763,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,X1)))=meet(X0,join(X1,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f27])).
% 32.64/4.56 fof(f776,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(X1,meet(X0,join(X2,X3))))=meet(meet(X0,X1),join(X2,X3)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f739])).
% 32.64/4.56 fof(f777,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (join(meet(X0,meet(X1,X2)),meet(X1,meet(X0,join(X2,X3))))=meet(X1,meet(X0,join(X2,X3))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f42,f776])).
% 32.64/4.56 fof(f783,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,join(meet(join(X1,X0),X1),X1))=meet(join(X1,X0),join(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f50,f753])).
% 32.64/4.56 fof(f784,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,join(X1,meet(join(X1,X0),X1)))=meet(join(X1,X0),join(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f697,f783])).
% 32.64/4.56 fof(f785,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,join(X1,meet(X1,join(X1,X0))))=meet(join(X1,X0),join(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f13,f784])).
% 32.64/4.56 fof(f786,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X1,join(X1,X0)))=meet(join(X1,X0),join(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f748,f785])).
% 32.64/4.56 fof(f787,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X1,join(X1,X0)))=join(X1,X0))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f11,f786])).
% 32.64/4.56 fof(f791,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,X1)))=meet(X0,join(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f513,f757])).
% 32.64/4.56 fof(f793,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X1,join(X2,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f27,f761])).
% 32.64/4.56 fof(f794,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f555,f793])).
% 32.64/4.56 fof(f812,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),join(X1,meet(X0,X2)))=join(X1,meet(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f28])).
% 32.64/4.56 fof(f814,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,join(X0,meet(X0,X1)))=join(X0,meet(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f12,f28])).
% 32.64/4.56 fof(f820,plain,(
% 32.64/4.56 ![X0,X1]: (meet(join(meet(X0,X1),X0),meet(X0,X1))=join(meet(X0,X1),meet(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f12,f28])).
% 32.64/4.56 fof(f828,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(X1,X2)))=join(X0,meet(X1,meet(X2,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f65,f28])).
% 32.64/4.56 fof(f858,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,meet(join(meet(X1,X0),X1),X1))=join(meet(X1,X0),meet(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f38,f820])).
% 32.64/4.56 fof(f859,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,meet(X1,join(meet(X1,X0),X1)))=join(meet(X1,X0),meet(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f455,f858])).
% 32.64/4.56 fof(f860,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,meet(X1,join(X1,meet(X1,X0))))=join(meet(X1,X0),meet(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f794,f859])).
% 32.64/4.56 fof(f861,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,join(X1,meet(X1,X0)))=join(meet(X1,X0),meet(X1,X0)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f814,f860])).
% 32.64/4.56 fof(f862,plain,(
% 32.64/4.56 ![X0,X1]: (meet(X0,join(X1,meet(X1,X0)))=meet(X1,X0))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f12,f861])).
% 32.64/4.56 fof(f868,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X1,meet(X2,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f28,f828])).
% 32.64/4.56 fof(f869,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f313,f868])).
% 32.64/4.56 fof(f890,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(meet(X1,meet(X2,X0)),X2))=meet(meet(X2,X0),X1))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f65,f278])).
% 32.64/4.56 fof(f940,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X2,meet(X1,X0))))=meet(meet(X1,X0),X2))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f455,f890])).
% 32.64/4.56 fof(f941,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X0,X2)))=meet(meet(X2,X0),X1))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f465,f940])).
% 32.64/4.56 fof(f942,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X0,X2),X1))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f386,f941])).
% 32.64/4.56 fof(f1042,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X2,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f203])).
% 32.64/4.56 fof(f1374,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,X3)))=meet(join(X1,X2),meet(X0,join(X1,meet(X2,X3)))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f28,f152])).
% 32.64/4.56 fof(f1576,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X1,join(X0,X1)))=join(X1,X0))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f787])).
% 32.64/4.56 fof(f1668,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),X2)=meet(X2,join(X1,X0)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f794])).
% 32.64/4.56 fof(f1672,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (meet(X0,join(X1,join(X2,X3)))=meet(X0,join(X3,join(X2,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f54,f794])).
% 32.64/4.56 fof(f1807,plain,(
% 32.64/4.56 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X0,join(X1,meet(X1,X0))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f862,f27])).
% 32.64/4.56 fof(f1877,plain,(
% 32.64/4.56 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f862,f1807])).
% 32.64/4.56 fof(f2051,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(meet(X0,join(X3,X2)),X1))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f794,f942])).
% 32.64/4.56 fof(f2138,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (meet(X0,meet(X1,join(X2,X3)))=meet(X0,meet(X1,join(X3,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f942,f2051])).
% 32.64/4.56 fof(f3367,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X2,X1),X0))=meet(X0,join(X1,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f1668,f27])).
% 32.64/4.56 fof(f3758,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (meet(join(X0,X1),join(X0,meet(X1,meet(X2,X3))))=join(X0,meet(X1,meet(X3,X2))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f455,f28])).
% 32.64/4.56 fof(f3873,plain,(
% 32.64/4.56 ![X0,X1,X2,X3]: (join(X0,meet(X1,meet(X2,X3)))=join(X0,meet(X1,meet(X3,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f28,f3758])).
% 32.64/4.56 fof(f4119,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),join(X2,meet(join(X2,X0),X1)))=join(X2,meet(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f203,f29])).
% 32.64/4.56 fof(f4135,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(join(X0,X2),join(X1,meet(X1,X2)))))=join(X0,meet(X2,join(X1,meet(X1,X2)))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f862,f29])).
% 32.64/4.56 fof(f4151,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(join(X0,X2),X1)))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f13,f29])).
% 32.64/4.56 fof(f4196,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(join(X1,X0),X2),meet(join(X0,X1),X2)))=join(X0,meet(join(X1,X0),X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f82,f29])).
% 32.64/4.56 fof(f4198,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(join(X1,X0),X2)))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f14,f29])).
% 32.64/4.56 fof(f4216,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(meet(X1,X2),meet(join(X0,X1),X2)),join(X0,meet(X1,X2))))=join(join(meet(X1,X2),meet(join(X0,X1),X2)),X0))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f29,f1576])).
% 32.64/4.56 fof(f4270,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(join(X0,X2),join(X1,meet(X1,X2)))))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f862,f4135])).
% 32.64/4.56 fof(f4281,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(X1,join(X0,X2))))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f4283,f4270])).
% 32.64/4.56 fof(f4283,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f3367,f4151])).
% 32.64/4.56 fof(f4390,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X0,meet(X1,X2)),join(meet(X1,X2),meet(join(X0,X1),X2))))=join(join(meet(X1,X2),meet(join(X0,X1),X2)),X0))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f869,f4216])).
% 32.64/4.56 fof(f4391,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X0,meet(X1,X2)),join(meet(X1,X2),meet(join(X0,X1),X2))))=join(meet(X1,X2),join(X0,meet(join(X0,X1),X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f1042,f4390])).
% 32.64/4.56 fof(f4392,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X0,meet(X1,X2)),join(meet(X1,X2),meet(join(X0,X1),X2))))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f4119,f4391])).
% 32.64/4.56 fof(f4437,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f763,f4281])).
% 32.64/4.56 fof(f4451,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X1,join(X0,X2))))=meet(X1,meet(X1,join(X0,X2))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f271,f777])).
% 32.64/4.56 fof(f4503,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,meet(join(X1,X2),X1)),meet(join(X1,X2),X0))=meet(join(X1,X2),meet(X0,join(X1,X2))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f65,f777])).
% 32.64/4.56 fof(f4587,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X0,X2),X1))=meet(X1,meet(X1,join(X0,X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f271,f4451])).
% 32.64/4.56 fof(f4588,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X1,X0),X2))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f4589,f4198])).
% 32.64/4.56 fof(f4589,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X0,X2),X1))=meet(join(X0,X2),X1))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f271,f4587])).
% 32.64/4.56 fof(f4656,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(X2,meet(join(X0,X1),X0)))=meet(join(X0,X1),meet(X2,join(X0,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f14,f4503])).
% 32.64/4.56 fof(f4657,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(X2,meet(X0,join(X0,X1))))=meet(join(X0,X1),meet(X2,join(X0,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f3873,f4656])).
% 32.64/4.56 fof(f4659,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(X2,meet(X0,join(X0,X1))))=meet(X2,join(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f313,f4657])).
% 32.64/4.56 fof(f4805,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,join(meet(join(X1,X0),X2),meet(join(X0,X1),X2)))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f4588,f4196])).
% 32.64/4.56 fof(f4855,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X2,X0),X1))=meet(X1,join(X0,X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f1668,f746])).
% 32.64/4.56 fof(f4989,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X0,meet(X1,X2)),meet(X2,join(X1,X0))))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f4855,f4392])).
% 32.64/4.56 fof(f5086,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(meet(X1,join(X2,X0)),join(X0,meet(X2,X1))))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f869,f4989])).
% 32.64/4.56 fof(f5087,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,meet(join(X0,meet(X2,X1)),join(X2,X0))))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f942,f5086])).
% 32.64/4.56 fof(f5088,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,meet(join(X2,X0),join(X0,meet(X2,X1)))))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f3873,f5087])).
% 32.64/4.56 fof(f5089,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,meet(X2,X1))))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f812,f5088])).
% 32.64/4.56 fof(f5111,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(join(X1,X0),X2))=meet(join(X1,X0),X2))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f1668,f1877])).
% 32.64/4.56 fof(f5219,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=join(X0,meet(X1,X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f5111,f4805])).
% 32.64/4.56 fof(f6939,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X0,join(X1,X0)))=meet(X0,join(X0,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f794,f748])).
% 32.64/4.56 fof(f7065,plain,(
% 32.64/4.56 ![X0,X1]: (join(X0,meet(X0,X1))=meet(X0,join(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f4437,f6939])).
% 32.64/4.56 fof(f7314,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(meet(X0,X1),join(meet(X0,X1),X2)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f278,f7065])).
% 32.64/4.56 fof(f7453,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(X0,meet(join(meet(X0,X1),X2),X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f942,f7314])).
% 32.64/4.56 fof(f7454,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),meet(X2,join(meet(join(X0,X1),X2),X0)))=meet(X2,join(X0,X1)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f7461,f4659])).
% 32.64/4.56 fof(f7461,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(X0,meet(X1,join(meet(X0,X1),X2))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f455,f7453])).
% 32.64/4.56 fof(f7669,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),meet(X2,join(X0,meet(join(X0,X1),X2))))=meet(X2,join(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f2138,f7454])).
% 32.64/4.56 fof(f7670,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(join(X0,X1),meet(X2,join(X0,meet(X1,X2))))=meet(X2,join(X0,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f5219,f7669])).
% 32.64/4.56 fof(f7674,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(X0,meet(X1,join(X0,X2)))=join(X0,meet(X2,X1)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f7676,f5089])).
% 32.64/4.56 fof(f7676,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,X2)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f1374,f7670])).
% 32.64/4.56 fof(f7735,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X0))=meet(X0,join(meet(X0,X1),X2)))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f7674,f745])).
% 32.64/4.56 fof(f9665,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(join(X2,X1),X0))=meet(X0,join(X2,X1)))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f869,f791])).
% 32.64/4.56 fof(f9688,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,join(X2,meet(X1,X0))))=meet(X1,join(X2,meet(X1,X0))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f271,f791])).
% 32.64/4.56 fof(f9689,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X1))))=meet(X1,join(X2,meet(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f313,f791])).
% 32.64/4.56 fof(f9693,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,join(X2,meet(X0,X1))))=meet(X0,join(X2,meet(X0,X1))))),
% 32.64/4.56 inference(paramodulation,[status(thm)],[f44,f791])).
% 32.64/4.56 fof(f9777,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(meet(X0,X1),join(X2,X1)))=meet(X0,join(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f7735,f9665])).
% 32.64/4.56 fof(f9778,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,meet(X0,X1))))=meet(X0,join(X2,X1)))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f1672,f9777])).
% 32.64/4.56 fof(f9816,plain,(
% 32.64/4.56 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(X1,join(X2,meet(X0,X1))))),
% 32.64/4.56 inference(forward_demodulation,[status(thm)],[f4437,f9689])).
% 32.64/4.56 fof(f9832,plain,(
% 32.64/4.56 ![X0,X1,X2]: (meet(X0,join(join(X1,meet(X0,X2)),X2))=meet(X0,join(X1,meet(X0,X2))))),
% 32.64/4.56 inference(backward_demodulation,[status(thm)],[f9838,f9688])).
% 32.64/4.56 fof(f9838,plain,(
% 32.64/4.58 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(X1,join(X2,X0)))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f7676,f9816])).
% 32.64/4.58 fof(f9841,plain,(
% 32.64/4.58 ~meet(a,join(b,c))=meet(a,join(c,meet(a,b)))),
% 32.64/4.58 inference(backward_demodulation,[status(thm)],[f9878,f20])).
% 32.64/4.58 fof(f9878,plain,(
% 32.64/4.58 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(X0,join(X2,meet(X0,X1))))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f4437,f9693])).
% 32.64/4.58 fof(f10230,plain,(
% 32.64/4.58 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,meet(X0,X1))))=meet(X0,join(X2,meet(X0,X1))))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f794,f9832])).
% 32.64/4.58 fof(f10241,plain,(
% 32.64/4.58 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(X0,join(X1,meet(X0,X2))))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f9778,f10230])).
% 32.64/4.58 fof(f10252,plain,(
% 32.64/4.58 ~meet(a,join(b,c))=meet(a,join(c,b))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f10241,f9841])).
% 32.64/4.58 fof(f10253,plain,(
% 32.64/4.58 ~meet(a,join(b,c))=meet(a,join(b,c))),
% 32.64/4.58 inference(forward_demodulation,[status(thm)],[f794,f10252])).
% 32.64/4.58 fof(f10254,plain,(
% 32.64/4.58 $false),
% 32.64/4.58 inference(trivial_equality_resolution,[status(thm)],[f10253])).
% 32.64/4.58 % SZS output end CNFRefutation for theBenchmark.p
% 13.02/15.77 % Elapsed time: 15.411960 seconds
% 13.02/15.77 % CPU time: 119.584166 seconds
% 13.02/15.77 % Total memory used: 65.456 GB
% 13.02/15.77 % Net memory used: 65.454 GB
%------------------------------------------------------------------------------