%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT027-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:09 PM UTC 2026
% Result : Unsatisfiable 28.54s 4.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT027-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n014.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 23:07:04 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.37 % Drodi V4.1.1
% 28.54/4.06 % Refutation found
% 28.54/4.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 28.54/4.06 % SZS output start CNFRefutation for theBenchmark
% 28.54/4.06 fof(f2,axiom,(
% 28.54/4.06 (![X]: (join(X,X) = X ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f3,axiom,(
% 28.54/4.06 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f4,axiom,(
% 28.54/4.06 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f5,axiom,(
% 28.54/4.06 (![X,Y,Z]: (meet(meet(join(X,Y),join(Z,Y)),Y) = Y ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f6,axiom,(
% 28.54/4.06 (![X,Y,Z]: (join(join(meet(X,Y),meet(Z,Y)),Y) = Y ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f7,hypothesis,(
% 28.54/4.06 (![X,Y,Z]: (meet(X,join(Y,join(X,Z))) = X ))),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f8,negated_conjecture,(
% 28.54/4.06 join(join(a,b),c) != join(a,join(b,c)) ),
% 28.54/4.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.54/4.06 fof(f10,plain,(
% 28.54/4.06 ![X0]: (join(X0,X0)=X0)),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f2])).
% 28.54/4.06 fof(f11,plain,(
% 28.54/4.06 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f3])).
% 28.54/4.06 fof(f12,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f4])).
% 28.54/4.06 fof(f13,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X1)),X1)=X1)),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f5])).
% 28.54/4.06 fof(f14,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(meet(X0,X1),meet(X2,X1)),X1)=X1)),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f6])).
% 28.54/4.06 fof(f15,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(X0,join(X1,join(X0,X2)))=X0)),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f7])).
% 28.54/4.06 fof(f16,plain,(
% 28.54/4.06 ~join(join(a,b),c)=join(a,join(b,c))),
% 28.54/4.06 inference(cnf_transformation,[status(thm)],[f8])).
% 28.54/4.06 fof(f22,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X2,X0)))=X0)),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f11,f13])).
% 28.54/4.06 fof(f23,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(meet(X1,X0),meet(X2,X0)))=X0)),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f14])).
% 28.54/4.06 fof(f24,plain,(
% 28.54/4.06 ~join(c,join(a,b))=join(a,join(b,c))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f16])).
% 28.54/4.06 fof(f31,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f10,f23])).
% 28.54/4.06 fof(f42,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f11,f31])).
% 28.54/4.06 fof(f44,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(meet(X0,X1),meet(X2,X0)))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f11,f23])).
% 28.54/4.06 fof(f109,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(X0,join(join(X0,X1),X2))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f15])).
% 28.54/4.06 fof(f111,plain,(
% 28.54/4.06 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f10,f15])).
% 28.54/4.06 fof(f112,plain,(
% 28.54/4.06 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f42,f15])).
% 28.54/4.06 fof(f118,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f15])).
% 28.54/4.06 fof(f160,plain,(
% 28.54/4.06 ![X0,X1]: (join(join(X0,X1),X1)=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f112,f31])).
% 28.54/4.06 fof(f161,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(meet(X2,join(X0,X1)),X1))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f112,f23])).
% 28.54/4.06 fof(f176,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,join(X1,X0))=join(X1,X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f160])).
% 28.54/4.06 fof(f177,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X1,meet(X2,join(X0,X1))))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f161])).
% 28.54/4.06 fof(f198,plain,(
% 28.54/4.06 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f111,f31])).
% 28.54/4.06 fof(f199,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(meet(X2,join(X0,X1)),X0))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f111,f23])).
% 28.54/4.06 fof(f208,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f198])).
% 28.54/4.06 fof(f209,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X0,meet(X2,join(X0,X1))))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f199])).
% 28.54/4.06 fof(f217,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,join(X0,X1))=join(X1,X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f176])).
% 28.54/4.06 fof(f262,plain,(
% 28.54/4.06 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f208])).
% 28.54/4.06 fof(f325,plain,(
% 28.54/4.06 ![X0,X1]: (join(join(X0,X1),join(X1,X0))=join(X0,join(X0,X1)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f217,f176])).
% 28.54/4.06 fof(f327,plain,(
% 28.54/4.06 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f217,f112])).
% 28.54/4.06 fof(f348,plain,(
% 28.54/4.06 ![X0,X1]: (join(join(X0,X1),join(X1,X0))=join(X1,X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f325])).
% 28.54/4.06 fof(f386,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),X0)=join(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f109,f31])).
% 28.54/4.06 fof(f399,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(join(X0,X1),X2))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f386])).
% 28.54/4.06 fof(f420,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,join(X1,X0)))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f217,f118])).
% 28.54/4.06 fof(f783,plain,(
% 28.54/4.06 ![X0,X1]: (join(join(X0,X1),join(X1,X0))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f348])).
% 28.54/4.06 fof(f823,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(join(X1,X0),X2))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f348,f109])).
% 28.54/4.06 fof(f1068,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(meet(join(X0,X1),X2),join(X1,X0)))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f327,f44])).
% 28.54/4.06 fof(f1077,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(meet(X2,join(X0,X1)),join(X1,X0)))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f327,f23])).
% 28.54/4.06 fof(f1148,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X0),meet(join(X0,X1),X2)))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1068])).
% 28.54/4.06 fof(f1152,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X0),meet(X2,join(X0,X1))))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1077])).
% 28.54/4.06 fof(f1355,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,join(X1,X2)),join(X2,X1))=join(X0,join(X1,X2)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f420,f31])).
% 28.54/4.06 fof(f1356,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,join(X1,X2)),join(meet(X3,join(X0,join(X1,X2))),join(X2,X1)))=join(X0,join(X1,X2)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f420,f23])).
% 28.54/4.06 fof(f1451,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,join(X1,X0)))=join(X2,join(X1,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1355])).
% 28.54/4.06 fof(f1452,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,join(X1,X2)),join(join(X2,X1),meet(X3,join(X0,join(X1,X2)))))=join(X0,join(X1,X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1356])).
% 28.54/4.06 fof(f1527,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(X1,X0))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f823,f31])).
% 28.54/4.06 fof(f1619,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),meet(join(X1,X0),X2))=join(X1,X0))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f1621,f1148])).
% 28.54/4.06 fof(f1620,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),meet(X2,join(X1,X0)))=join(X1,X0))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f1621,f1152])).
% 28.54/4.06 fof(f1621,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X0),X2))=join(join(X1,X0),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1527])).
% 28.54/4.06 fof(f1643,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,join(X1,X2)),join(X2,X1))=join(join(X1,X2),X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f823,f1620])).
% 28.54/4.06 fof(f1644,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(X1,X0))=join(X2,join(X0,X1)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f420,f1620])).
% 28.54/4.06 fof(f1649,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),X0)=join(X2,join(X0,X1)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f15,f1620])).
% 28.54/4.06 fof(f1692,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X1,X0))=join(meet(X2,join(X1,X0)),join(X0,X1)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f1620,f217])).
% 28.54/4.06 fof(f1753,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,join(X1,X0)))=join(join(X1,X0),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1643])).
% 28.54/4.06 fof(f1754,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X0),X2))=join(X2,join(X1,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1644])).
% 28.54/4.06 fof(f1758,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(join(X0,X1),X2))=join(X2,join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1649])).
% 28.54/4.06 fof(f1839,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,X1)=join(meet(X2,join(X1,X0)),join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f783,f1692])).
% 28.54/4.06 fof(f1840,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,X1)=join(join(X0,X1),meet(X2,join(X1,X0))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1839])).
% 28.54/4.06 fof(f1873,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(join(join(X0,X1),X2),X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f118,f1840])).
% 28.54/4.06 fof(f1877,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,X1)=join(join(X0,X1),meet(join(X1,X0),X2)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f11,f1840])).
% 28.54/4.06 fof(f1980,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(join(X0,X1),X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f1873])).
% 28.54/4.06 fof(f2434,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(meet(join(X0,X1),X2),join(X1,X0))=meet(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f1877,f112])).
% 28.54/4.06 fof(f2608,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),meet(join(X1,X0),X2))=meet(join(X1,X0),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f11,f2434])).
% 28.54/4.06 fof(f2628,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X0,meet(X2,join(X1,X0))))=join(X1,X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f177])).
% 28.54/4.06 fof(f2638,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(X2,X0))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f109,f177])).
% 28.54/4.06 fof(f2768,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X2),X0))=join(join(X1,X2),X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f2638])).
% 28.54/4.06 fof(f2932,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,join(X1,X2)),join(X0,X2))=join(X0,join(X1,X2)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f118,f209])).
% 28.54/4.06 fof(f3088,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X0,join(X2,X1)))=join(X0,join(X2,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f2932])).
% 28.54/4.06 fof(f3280,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(meet(join(X0,X1),X2),join(X1,X0)),join(X3,join(X0,X1)))=join(X3,join(join(X1,X0),meet(join(X0,X1),X2))))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f1619,f1451])).
% 28.54/4.06 fof(f3414,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),meet(join(X1,X0),X2)),join(X3,join(X1,X0)))=join(X3,join(join(X0,X1),meet(join(X1,X0),X2))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f3280])).
% 28.54/4.06 fof(f3415,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,X1),join(X2,join(X1,X0)))=join(X2,join(join(X0,X1),meet(join(X1,X0),X3))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1877,f3414])).
% 28.54/4.06 fof(f3416,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(X1,X2))=join(X0,join(join(X2,X1),meet(join(X1,X2),X3))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1451,f3415])).
% 28.54/4.06 fof(f3417,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X0,join(X2,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1877,f3416])).
% 28.54/4.06 fof(f3583,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),meet(join(X1,X0),join(X2,join(X0,X1))))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f783,f22])).
% 28.54/4.06 fof(f3646,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,join(X1,X0)))=join(X1,X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f2608,f3583])).
% 28.54/4.06 fof(f4679,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(join(X1,X0),X2))=join(X1,X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f3646])).
% 28.54/4.06 fof(f7999,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X0),meet(X3,join(join(join(X0,X1),X2),join(X1,X0)))))=join(join(join(X0,X1),X2),join(X1,X0)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f1621,f2628])).
% 28.54/4.06 fof(f8184,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X0),meet(X3,join(join(X1,X0),join(join(X0,X1),X2)))))=join(join(join(X0,X1),X2),join(X1,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f7999])).
% 28.54/4.06 fof(f8185,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X0),meet(X3,join(X2,join(X0,X1)))))=join(join(join(X0,X1),X2),join(X1,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1754,f8184])).
% 28.54/4.06 fof(f8186,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X0),meet(X3,join(X2,join(X0,X1)))))=join(join(X1,X0),join(join(X0,X1),X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f8185])).
% 28.54/4.06 fof(f8187,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X0),meet(X3,join(X2,join(X0,X1)))))=join(X2,join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1754,f8186])).
% 28.54/4.06 fof(f8628,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(join(X0,X1),X2),X2),join(join(X0,X1),X2))=join(join(X2,X0),join(join(X0,X1),X2)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f2768,f2768])).
% 28.54/4.06 fof(f8637,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,meet(X1,join(X2,X0))),X2),join(X2,X0))=join(join(X2,X0),join(X0,meet(X1,join(X2,X0)))))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f177,f2768])).
% 28.54/4.06 fof(f8662,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,join(X1,X2)),join(join(join(X2,X1),X3),X0))=join(join(join(X1,X2),join(join(X2,X1),X3)),X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f1621,f2768])).
% 28.54/4.06 fof(f8693,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(join(X0,X2),X1))=join(X1,X0))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f2768,f4679])).
% 28.54/4.06 fof(f8694,plain,(
% 28.54/4.06 ![X0,X1,X2]: (meet(join(X0,X1),join(join(X0,X2),X1))=join(X0,X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f2768,f823])).
% 28.54/4.06 fof(f8837,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(join(join(X0,X1),X2),X2))=join(join(X2,X0),join(join(X0,X1),X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f8628])).
% 28.54/4.06 fof(f8838,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(join(X1,X2),X0))=join(join(X0,X1),join(join(X1,X2),X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f8837])).
% 28.54/4.06 fof(f8839,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),join(join(X1,X2),X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f262,f8838])).
% 28.54/4.06 fof(f8867,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,meet(X2,join(X0,X1))),X0))=join(join(X0,X1),join(X1,meet(X2,join(X0,X1)))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f8637])).
% 28.54/4.06 fof(f8868,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,meet(X1,join(X2,X0))),X2)=join(join(X2,X0),join(X0,meet(X1,join(X2,X0)))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f2768,f8867])).
% 28.54/4.06 fof(f8869,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,join(X0,X1))))=join(join(X0,X1),join(X1,meet(X2,join(X0,X1)))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f8868])).
% 28.54/4.06 fof(f8870,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,join(X0,X1))))=join(X0,X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f177,f8869])).
% 28.54/4.06 fof(f8922,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,join(X1,X2)),join(join(join(X2,X1),X3),X0))=join(join(X3,join(X2,X1)),X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1754,f8662])).
% 28.54/4.06 fof(f9125,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,X0))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f109,f8870])).
% 28.54/4.06 fof(f9270,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,join(X1,X2)),join(join(X2,X1),X3))=join(join(X3,join(X2,X1)),X0))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f9125,f8922])).
% 28.54/4.06 fof(f9276,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),join(X1,X2)))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f9125,f8839])).
% 28.54/4.06 fof(f9528,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(meet(X0,join(X1,join(X2,X3))),join(X3,X2)),X1)=join(X1,join(X2,X3)))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f9270,f1452])).
% 28.54/4.06 fof(f9562,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(meet(X1,join(X0,join(X2,X3))),join(X3,X2)))=join(X0,join(X2,X3)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f9528])).
% 28.54/4.06 fof(f9563,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(join(X1,X2),meet(X3,join(X0,join(X2,X1)))))=join(X0,join(X2,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f3417,f9562])).
% 28.54/4.06 fof(f9668,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,join(X2,X0)))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f8693,f8870])).
% 28.54/4.06 fof(f9851,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,X1))=join(X0,join(X2,X1)))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f9857,f3088])).
% 28.54/4.06 fof(f9857,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X0,X2))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f9668])).
% 28.54/4.06 fof(f10418,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,X1))=join(join(X1,join(X1,X0)),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f217,f9125])).
% 28.54/4.06 fof(f10421,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(X2,X1))=join(join(X1,X0),X2))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f12,f9125])).
% 28.54/4.06 fof(f10433,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),X2),join(join(X1,X3),X0))=join(join(join(X0,X1),X2),join(X1,X3)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f9125,f9125])).
% 28.54/4.06 fof(f10445,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(X1,X0))=join(join(join(X0,X1),X2),X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f262,f9125])).
% 28.54/4.06 fof(f10448,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(join(X0,X1),X2),join(X0,X1))=join(join(join(X0,X1),X2),X1))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f176,f9125])).
% 28.54/4.06 fof(f10476,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(join(X0,X1),X2),join(join(join(X0,X1),X3),join(X2,X0)))=join(join(X0,X1),join(X2,X0)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f9125,f8694])).
% 28.54/4.06 fof(f10478,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(join(X0,X1),X2),join(join(join(X0,X1),X3),join(X2,X0)))=join(join(X2,X0),join(X0,X1)))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f9125,f8693])).
% 28.54/4.06 fof(f10484,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),join(X1,X2)),join(join(join(X1,X2),X0),X3))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f9125,f1621])).
% 28.54/4.06 fof(f10486,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(join(X0,X1),join(X1,X2)),join(X3,join(join(X1,X2),X0)))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.06 inference(paramodulation,[status(thm)],[f9125,f1753])).
% 28.54/4.06 fof(f10568,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X2,join(X2,X0)),X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9851,f10418])).
% 28.54/4.06 fof(f10623,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(join(X0,X1),join(join(join(X1,X0),meet(X2,join(X3,join(X0,X1)))),X3))=join(X3,join(X0,X1)))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f10741,f8187])).
% 28.54/4.06 fof(f10739,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(join(X0,X1),X2))=join(X0,join(X2,X1)))),
% 28.54/4.06 inference(backward_demodulation,[status(thm)],[f10741,f399])).
% 28.54/4.06 fof(f10741,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X2),X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f10568])).
% 28.54/4.06 fof(f10747,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X2,X0),X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9851,f10421])).
% 28.54/4.06 fof(f10797,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(join(join(X1,X2),X3),join(X3,X1)))=join(join(join(X3,X1),X0),join(X1,X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10747,f10433])).
% 28.54/4.06 fof(f10798,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(join(X1,X2),join(join(X2,X3),X1)))=join(join(join(X1,X2),X0),join(X2,X3)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f3417,f10797])).
% 28.54/4.06 fof(f10799,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(join(X1,X2),join(X2,X3)))=join(join(join(X1,X2),X0),join(X2,X3)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9125,f10798])).
% 28.54/4.06 fof(f10800,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(join(join(X1,X2),X0),join(X2,X3)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9276,f10799])).
% 28.54/4.06 fof(f10801,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X0,join(join(X2,X3),join(X1,X2))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10747,f10800])).
% 28.54/4.06 fof(f10802,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X0,join(join(X2,X3),X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9125,f10801])).
% 28.54/4.06 fof(f10803,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X0,join(X3,join(X1,X2))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10747,f10802])).
% 28.54/4.06 fof(f10819,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X1,X0),X2))=join(join(join(X1,X0),X2),X0))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f10445])).
% 28.54/4.06 fof(f10820,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(join(X1,X2),X0),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f1754,f10819])).
% 28.54/4.06 fof(f10821,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(join(X1,X2),X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f10820])).
% 28.54/4.06 fof(f10822,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X2,join(X0,X1))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10747,f10821])).
% 28.54/4.06 fof(f10823,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f10822])).
% 28.54/4.06 fof(f10834,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(join(X0,X1),join(join(X0,X1),X2))=join(join(join(X0,X1),X2),X1))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f10448])).
% 28.54/4.06 fof(f10835,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(join(X1,X2),X0),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f217,f10834])).
% 28.54/4.06 fof(f10836,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(join(X1,X2),X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f12,f10835])).
% 28.54/4.06 fof(f10837,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X2,X0))))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10836])).
% 28.54/4.06 fof(f10903,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(join(join(X0,X1),X3),join(X2,X0)))=join(join(X0,X1),join(X2,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10476])).
% 28.54/4.06 fof(f10904,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(join(X0,X1),join(X3,join(X2,X0))))=join(join(X0,X1),join(X2,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10903])).
% 28.54/4.06 fof(f10905,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X0,join(X1,join(X3,join(X2,X0)))))=join(join(X0,X1),join(X2,X0)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10904])).
% 28.54/4.06 fof(f10906,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X0,join(X1,join(X3,join(X2,X0)))))=join(join(X0,X1),X2))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f9125,f10905])).
% 28.54/4.06 fof(f10907,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X0,join(X1,join(X3,join(X2,X0)))))=join(X0,join(X1,X2)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10906])).
% 28.54/4.06 fof(f10909,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(join(join(X0,X1),X3),join(X2,X0)))=join(join(X2,X0),join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10478])).
% 28.54/4.06 fof(f10910,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(join(X0,X1),join(X3,join(X2,X0))))=join(join(X2,X0),join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10909])).
% 28.54/4.06 fof(f10911,plain,(
% 28.54/4.06 ![X0,X1,X2,X3]: (meet(join(X0,join(X1,X2)),join(X0,join(X1,join(X3,join(X2,X0)))))=join(join(X2,X0),join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10823,f10910])).
% 28.54/4.06 fof(f10912,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X2,X0),join(X0,X1)))),
% 28.54/4.06 inference(forward_demodulation,[status(thm)],[f10907,f10911])).
% 28.54/4.06 fof(f10913,plain,(
% 28.54/4.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,join(X0,X1))))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10912])).
% 28.54/4.08 fof(f10914,plain,(
% 28.54/4.08 ~join(b,join(a,c))=join(a,join(b,c))),
% 28.54/4.08 inference(backward_demodulation,[status(thm)],[f10915,f24])).
% 28.54/4.08 fof(f10915,plain,(
% 28.54/4.08 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,X0)))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f217,f10913])).
% 28.54/4.08 fof(f10947,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(join(X0,X1),join(join(X1,X2),join(join(join(X1,X2),X0),X3)))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10484])).
% 28.54/4.08 fof(f10948,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(join(X1,X2),join(join(join(X1,X2),X0),X3))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10947])).
% 28.54/4.08 fof(f10949,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(join(join(join(X1,X2),X0),X3),join(X1,X2)))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f1758,f10948])).
% 28.54/4.08 fof(f10950,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(join(join(X1,X2),X0),X3))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10803,f10949])).
% 28.54/4.08 fof(f10951,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(join(X1,X2),join(X0,X3)))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10950])).
% 28.54/4.08 fof(f10952,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(join(X1,X2),join(X0,X3))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f1980,f10951])).
% 28.54/4.08 fof(f10953,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(join(X0,X1),join(X2,X3)))=join(join(join(X2,X3),join(X0,X2)),X1))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f1758,f10952])).
% 28.54/4.08 fof(f10954,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(join(X0,X1),join(X2,X3))=join(join(join(X0,X1),join(X2,X0)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f1758,f10953])).
% 28.54/4.08 fof(f10955,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(join(join(X0,X1),join(X2,X0)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10954])).
% 28.54/4.08 fof(f10956,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(join(X0,X1),join(join(X2,X0),X3)))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10955])).
% 28.54/4.08 fof(f10957,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X0,join(X1,join(join(X2,X0),X3))))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10956])).
% 28.54/4.08 fof(f10959,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X0,join(X1,join(X2,join(X0,X3)))))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10957])).
% 28.54/4.08 fof(f10974,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(join(X0,X1),join(join(X1,X2),join(X3,join(join(X1,X2),X0))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10486])).
% 28.54/4.08 fof(f10975,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(join(X1,X2),join(X3,join(join(X1,X2),X0)))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10974])).
% 28.54/4.08 fof(f10976,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(join(X1,join(join(X2,X3),X0)),join(X2,X3)))=join(join(join(X2,X3),join(X0,X2)),X1))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f1758,f10975])).
% 28.54/4.08 fof(f10977,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(X3,join(join(X1,X2),X0)))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10803,f10976])).
% 28.54/4.08 fof(f10978,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(X3,join(X1,join(X2,X0))))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10977])).
% 28.54/4.08 fof(f10979,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(X3,join(X2,X0)))))=join(join(join(X1,X2),join(X0,X1)),X3))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10959,f10978])).
% 28.54/4.08 fof(f10980,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X0,join(X2,X3))))=join(join(join(X1,X3),join(X0,X1)),X2))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10837,f10979])).
% 28.54/4.08 fof(f10981,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(join(X0,X1),join(X2,X3))=join(join(join(X2,X1),join(X3,X2)),X0))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10837,f10980])).
% 28.54/4.08 fof(f10982,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(join(join(X2,X1),join(X3,X2)),X0))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10981])).
% 28.54/4.08 fof(f10983,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(join(X2,X1),join(join(X3,X2),X0)))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10982])).
% 28.54/4.08 fof(f10984,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X2,join(X1,join(join(X3,X2),X0))))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10983])).
% 28.54/4.08 fof(f10985,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,X3)))=join(X2,join(X1,join(X3,join(X2,X0)))))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10984])).
% 28.54/4.08 fof(f11276,plain,(
% 28.54/4.08 ![X0,X1,X2,X3]: (join(X0,join(X1,join(join(join(X1,X0),meet(X2,join(X3,join(X0,X1)))),X3)))=join(X3,join(X0,X1)))),
% 28.54/4.08 inference(forward_demodulation,[status(thm)],[f10823,f10623])).
% 28.54/4.10 fof(f11277,plain,(
% 28.54/4.10 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,join(join(X1,X0),meet(X3,join(X2,join(X0,X1)))))))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f3417,f11276])).
% 28.54/4.10 fof(f11278,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,join(X2,join(X0,X1))))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f9563,f11277])).
% 28.54/4.10 fof(f11279,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X0,join(X1,X2)))=join(X2,join(X1,X0)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f10985,f11278])).
% 28.54/4.10 fof(f11280,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f217,f11279])).
% 28.54/4.10 fof(f11504,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,join(X0,X2)))=join(X0,join(X2,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f11280,f10739])).
% 28.54/4.10 fof(f11525,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(join(join(X0,X1),X2),X1))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(paramodulation,[status(thm)],[f217,f10741])).
% 28.54/4.10 fof(f11616,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,join(join(X0,X1),X2)))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f3417,f11525])).
% 28.54/4.10 fof(f11617,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,join(X0,join(X2,X1))))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f10741,f11616])).
% 28.54/4.10 fof(f11618,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(join(X1,X2),X2))=join(X1,join(X0,X2)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f11504,f11617])).
% 28.54/4.10 fof(f11619,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,join(X2,X1)))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f3417,f11618])).
% 28.54/4.10 fof(f11620,plain,(
% 28.54/4.10 ~join(a,join(c,b))=join(a,join(b,c))),
% 28.54/4.10 inference(backward_demodulation,[status(thm)],[f11621,f10914])).
% 28.54/4.10 fof(f11621,plain,(
% 28.54/4.10 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f262,f11619])).
% 28.54/4.10 fof(f11716,plain,(
% 28.54/4.10 ~join(a,join(b,c))=join(a,join(b,c))),
% 28.54/4.10 inference(forward_demodulation,[status(thm)],[f3417,f11620])).
% 28.54/4.10 fof(f11717,plain,(
% 28.54/4.10 $false),
% 28.54/4.10 inference(trivial_equality_resolution,[status(thm)],[f11716])).
% 28.54/4.10 % SZS output end CNFRefutation for theBenchmark.p
% 15.92/4.15 % Elapsed time: 3.780580 seconds
% 15.92/4.15 % CPU time: 29.512176 seconds
% 15.92/4.15 % Total memory used: 223.219 MB
% 15.92/4.15 % Net memory used: 217.748 MB
%------------------------------------------------------------------------------