%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT010-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 4.95s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT010-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.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 23:06:55 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 4.95/1.12 % Refutation found
% 4.95/1.12 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.95/1.12 % SZS output start CNFRefutation for theBenchmark
% 4.95/1.12 fof(f1,axiom,(
% 4.95/1.12 (![X]: (meet(X,X) = X ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f2,axiom,(
% 4.95/1.12 (![X]: (join(X,X) = X ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f3,axiom,(
% 4.95/1.12 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f4,axiom,(
% 4.95/1.12 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f5,axiom,(
% 4.95/1.12 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f6,axiom,(
% 4.95/1.12 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f7,axiom,(
% 4.95/1.12 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f8,axiom,(
% 4.95/1.12 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f9,hypothesis,(
% 4.95/1.12 (![X,Y,Z,U]: (meet(X,join(Y,meet(Z,join(X,U)))) = join(meet(X,join(Y,meet(X,Z))),meet(X,join(meet(X,Y),meet(Z,U)))) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f10,hypothesis,(
% 4.95/1.12 (![X,Y,Z,U]: (join(X,meet(Y,join(Z,meet(X,U)))) = meet(join(X,meet(Y,join(X,Z))),join(X,meet(join(X,Y),join(Z,U)))) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f11,hypothesis,(
% 4.95/1.12 (![X,Y,Z]: (meet(join(X,meet(Y,Z)),join(Z,meet(X,Y))) = join(meet(Z,join(X,meet(Y,Z))),meet(X,join(Y,Z))) ))),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f12,negated_conjecture,(
% 4.95/1.12 meet(a,meet(join(b,c),join(b,d))) != meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))) ),
% 4.95/1.12 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.95/1.12 fof(f13,plain,(
% 4.95/1.12 ![X0]: (meet(X0,X0)=X0)),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f1])).
% 4.95/1.12 fof(f14,plain,(
% 4.95/1.12 ![X0]: (join(X0,X0)=X0)),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f2])).
% 4.95/1.12 fof(f15,plain,(
% 4.95/1.12 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f3])).
% 4.95/1.12 fof(f16,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f4])).
% 4.95/1.12 fof(f17,plain,(
% 4.95/1.12 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f5])).
% 4.95/1.12 fof(f18,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f6])).
% 4.95/1.12 fof(f19,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f7])).
% 4.95/1.12 fof(f20,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f8])).
% 4.95/1.12 fof(f21,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,join(X0,X3))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(X2,X3)))))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f9])).
% 4.95/1.12 fof(f22,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (join(X0,meet(X1,join(X2,meet(X0,X3))))=meet(join(X0,meet(X1,join(X0,X2))),join(X0,meet(join(X0,X1),join(X2,X3)))))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f10])).
% 4.95/1.12 fof(f23,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(join(X0,meet(X1,X2)),join(X2,meet(X0,X1)))=join(meet(X2,join(X0,meet(X1,X2))),meet(X0,join(X1,X2))))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f11])).
% 4.95/1.12 fof(f24,plain,(
% 4.95/1.12 ~meet(a,meet(join(b,c),join(b,d)))=meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d))))),
% 4.95/1.12 inference(cnf_transformation,[status(thm)],[f12])).
% 4.95/1.12 fof(f40,plain,(
% 4.95/1.12 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(meet(join(b,c),join(b,d)),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f24])).
% 4.95/1.12 fof(f41,plain,(
% 4.95/1.12 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d))))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f40])).
% 4.95/1.12 fof(f53,plain,(
% 4.95/1.12 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f15])).
% 4.95/1.12 fof(f113,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f20])).
% 4.95/1.12 fof(f115,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f14,f20])).
% 4.95/1.12 fof(f117,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f20,f53])).
% 4.95/1.12 fof(f128,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f115])).
% 4.95/1.12 fof(f148,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(join(X1,X0),X2))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f117])).
% 4.95/1.12 fof(f153,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X0))=meet(X0,X1))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f16,f117])).
% 4.95/1.12 fof(f161,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,join(X0,X2)))=X0)),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f20,f148])).
% 4.95/1.12 fof(f163,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,meet(X1,join(X2,X0)))=meet(X0,X1))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f153])).
% 4.95/1.12 fof(f166,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,join(X2,join(X0,X3))))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f20,f161])).
% 4.95/1.12 fof(f201,plain,(
% 4.95/1.12 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=join(X0,X1))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f128,f53])).
% 4.95/1.12 fof(f233,plain,(
% 4.95/1.12 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f13,f19])).
% 4.95/1.12 fof(f318,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,meet(X1,join(X0,X2)))=meet(X0,X1))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f163])).
% 4.95/1.12 fof(f381,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,X1)=meet(join(X1,X0),join(X0,X1)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f201,f17])).
% 4.95/1.12 fof(f394,plain,(
% 4.95/1.12 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),join(meet(c,a),meet(a,d))))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f17,f41])).
% 4.95/1.12 fof(f397,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f17,f19])).
% 4.95/1.12 fof(f399,plain,(
% 4.95/1.12 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f17,f16])).
% 4.95/1.12 fof(f422,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(meet(X0,X2),join(X0,X3))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(meet(X0,X2),X3)))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f233,f21])).
% 4.95/1.12 fof(f435,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,join(X0,X3))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X2,X3),meet(X0,X1)))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f18,f21])).
% 4.95/1.12 fof(f455,plain,(
% 4.95/1.12 ![X0,X1,X2,X3,X4]: (meet(X0,join(X1,meet(X2,join(X0,join(X3,join(X2,X4))))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),X2))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f161,f21])).
% 4.95/1.12 fof(f495,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X0,meet(X2,join(X0,X3)))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(meet(X0,X2),X3)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f422])).
% 4.95/1.12 fof(f496,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(meet(X0,X2),X3)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f318,f495])).
% 4.95/1.12 fof(f497,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(X0,meet(X2,X3))))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f496])).
% 4.95/1.12 fof(f574,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,X2))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),X2))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f166,f455])).
% 4.95/1.12 fof(f593,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(X0,meet(X1,meet(X2,X0)))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f19,f399])).
% 4.95/1.12 fof(f605,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,join(X0,meet(X0,X1)))))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,meet(X0,X1))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f399,f21])).
% 4.95/1.12 fof(f626,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,meet(X0,X1))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f16,f605])).
% 4.95/1.12 fof(f627,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,X1)))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f233,f626])).
% 4.95/1.12 fof(f642,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(X0,meet(meet(X1,X0),X2))=X0)),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f17,f593])).
% 4.95/1.12 fof(f672,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(X0,meet(X1,meet(X0,X2)))=X0)),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f19,f642])).
% 4.95/1.12 fof(f887,plain,(
% 4.95/1.12 ![X0,X1]: (join(meet(X0,X1),X1)=meet(X1,join(meet(X0,X1),X1)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f399,f381])).
% 4.95/1.12 fof(f942,plain,(
% 4.95/1.12 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f53,f887])).
% 4.95/1.12 fof(f1011,plain,(
% 4.95/1.12 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,join(X2,X0)))=meet(X1,join(X2,X0)))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f163,f942])).
% 4.95/1.12 fof(f1569,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,meet(X2,join(X3,meet(X0,X1))))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f163,f397])).
% 4.95/1.12 fof(f1630,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=meet(X0,meet(X1,meet(X2,join(X3,meet(X1,X0))))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f397,f1569])).
% 4.95/1.12 fof(f2092,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(meet(X0,X1),X3))))=meet(join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),join(meet(X0,X1),meet(X1,join(X2,X3)))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f942,f22])).
% 4.95/1.12 fof(f2293,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X1,meet(X0,X3)))))=meet(join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),join(meet(X0,X1),meet(X1,join(X2,X3)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f397,f2092])).
% 4.95/1.12 fof(f2389,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(join(X0,meet(X1,meet(X0,X2))),join(meet(X0,X2),meet(X0,X1)))=join(meet(meet(X0,X2),X0),meet(X0,join(X1,meet(X0,X2)))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f672,f23])).
% 4.95/1.12 fof(f2390,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(join(X0,meet(X1,meet(X2,X0))),join(meet(X2,X0),meet(X0,X1)))=join(meet(meet(X2,X0),X0),meet(X0,join(X1,meet(X2,X0)))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f593,f23])).
% 4.95/1.12 fof(f2534,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(meet(X0,X1),meet(X0,X2)))=join(meet(meet(X0,X1),X0),meet(X0,join(X2,meet(X0,X1)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f672,f2389])).
% 4.95/1.12 fof(f2536,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X2,X3),meet(X0,X1)))))),
% 4.95/1.12 inference(backward_demodulation,[status(thm)],[f2538,f497])).
% 4.95/1.12 fof(f2538,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(meet(X0,X1),meet(X0,X2)))=meet(X0,join(X2,meet(X0,X1))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f1011,f2534])).
% 4.95/1.12 fof(f2539,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),meet(X0,X2)))=join(meet(meet(X1,X0),X0),meet(X0,join(X2,meet(X1,X0)))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f593,f2390])).
% 4.95/1.12 fof(f2542,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),meet(X0,X2)))=meet(X0,join(X2,meet(X1,X0))))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f1011,f2539])).
% 4.95/1.12 fof(f2810,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X2,join(X0,X3))))=meet(X0,join(X1,meet(X0,X2))))),
% 4.95/1.12 inference(backward_demodulation,[status(thm)],[f2536,f435])).
% 4.95/1.12 fof(f2811,plain,(
% 4.95/1.12 ![X0,X1,X2,X3]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),meet(X2,X3)))))),
% 4.95/1.12 inference(backward_demodulation,[status(thm)],[f2810,f21])).
% 4.95/1.12 fof(f2935,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,meet(X0,X1))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f672,f2811])).
% 4.95/1.12 fof(f2973,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,join(meet(X0,X1),X2))))),
% 4.95/1.12 inference(paramodulation,[status(thm)],[f161,f2811])).
% 4.95/1.12 fof(f3146,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,meet(X0,X2))),meet(X0,X1)))),
% 4.95/1.12 inference(forward_demodulation,[status(thm)],[f233,f2935])).
% 4.95/1.12 fof(f3237,plain,(
% 4.95/1.12 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(X0,join(X2,meet(X1,X0))))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3275,f2542])).
% 4.95/1.14 fof(f3245,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(meet(X0,X1),meet(X1,join(meet(X0,X1),X2))),join(meet(X0,X1),meet(X1,join(X2,X3)))))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3275,f2293])).
% 4.95/1.14 fof(f3247,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,join(X1,X2)),meet(X0,X1)))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3275,f3146])).
% 4.95/1.14 fof(f3272,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=join(meet(X0,join(X1,X2)),meet(X0,X1)))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3275,f627])).
% 4.95/1.14 fof(f3275,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(X0,join(X1,X2)))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f574,f2973])).
% 4.95/1.14 fof(f3444,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(X1,X2))=join(meet(X0,join(X1,X2)),meet(X0,X1)))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f3275,f3247])).
% 4.95/1.14 fof(f3516,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(X0,join(X2,X1)))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3524,f3237])).
% 4.95/1.14 fof(f3524,plain,(
% 4.95/1.14 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,X2)))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f3444,f3272])).
% 4.95/1.14 fof(f3565,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(meet(X0,X1),meet(X1,join(X2,X0))),join(meet(X0,X1),meet(X1,join(X2,X3)))))),
% 4.95/1.14 inference(backward_demodulation,[status(thm)],[f3516,f3245])).
% 4.95/1.14 fof(f3571,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(meet(X1,join(X2,X0)),join(meet(X0,X1),meet(X1,join(X2,X3)))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f1011,f3565])).
% 4.95/1.14 fof(f3572,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(X2,X0),meet(X1,join(meet(X0,X1),meet(X1,join(X2,X3))))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f397,f3571])).
% 4.95/1.14 fof(f3573,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(X2,X0),meet(X1,join(join(X2,X3),meet(X0,X1)))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f2542,f3572])).
% 4.95/1.14 fof(f3574,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(X2,X0),meet(X1,join(join(X2,X3),X0))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f3524,f3573])).
% 4.95/1.14 fof(f3575,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(X2,X0),meet(X1,join(X3,join(X2,X0)))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f113,f3574])).
% 4.95/1.14 fof(f3576,plain,(
% 4.95/1.14 ![X0,X1,X2,X3]: (join(meet(X0,X1),meet(X1,join(X2,meet(X0,X3))))=meet(join(X2,X0),X1))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f163,f3575])).
% 4.95/1.14 fof(f3631,plain,(
% 4.95/1.14 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),meet(join(b,d),join(join(meet(c,a),meet(a,d)),meet(a,join(b,meet(c,d)))))))),
% 4.95/1.14 inference(paramodulation,[status(thm)],[f18,f394])).
% 4.95/1.14 fof(f3635,plain,(
% 4.95/1.14 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,d),join(meet(c,a),meet(a,join(b,meet(c,d))))))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f113,f3631])).
% 4.95/1.14 fof(f3636,plain,(
% 4.95/1.14 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,d),meet(join(b,c),a)))))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f3576,f3635])).
% 4.95/1.14 fof(f3637,plain,(
% 4.95/1.14 ~meet(a,meet(join(b,c),join(b,d)))=meet(a,meet(join(b,c),join(b,d)))),
% 4.95/1.14 inference(forward_demodulation,[status(thm)],[f1630,f3636])).
% 4.95/1.14 fof(f3638,plain,(
% 4.95/1.14 $false),
% 4.95/1.14 inference(trivial_equality_resolution,[status(thm)],[f3637])).
% 4.95/1.14 % SZS output end CNFRefutation for theBenchmark.p
% 12.66/2.35 % Elapsed time: 1.766182 seconds
% 12.66/2.35 % CPU time: 2.589700 seconds
% 12.66/2.35 % Total memory used: 39.165 MB
% 12.66/2.35 % Net memory used: 38.104 MB
%------------------------------------------------------------------------------