Vampire---5.0.1.UNS-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n002.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 : Tue Sep 29 11:45:50 AM UTC 2026

% Result   : Unsatisfiable 23.85s 4.63s
% Output   : Refutation 27.37s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   80
%            Number of leaves      :   11
% Syntax   : Number of formulae    :  621 ( 621 unt;   1 def)
%            Number of atoms       :  621 ( 616 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    4 (   4   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   4 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :    5 (   5 usr;   3 con; 0-2 aty)
%            Number of variables   : 1762 (1762   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X0] : meet(X0,X0) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_meet) ).

fof(f2,axiom,
    ! [X0] : join(X0,X0) = X0,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_of_join) ).

fof(f3,axiom,
    ! [X0,X1] : meet(X0,X1) = meet(X1,X0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).

fof(f4,axiom,
    ! [X0,X1] : join(X0,X1) = join(X1,X0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).

fof(f5,axiom,
    ! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,X2)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet) ).

fof(f6,axiom,
    ! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X1,X2)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_join) ).

fof(f7,axiom,
    ! [X2,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,X1)) = meet(X0,join(X1,X2)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',quasi_lattice1) ).

fof(f8,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,X2)),meet(X0,X1)),
    inference(reorient_equations,[],[f7]) ).

fof(f9,axiom,
    ! [X2,X0,X1] : meet(join(X0,meet(X1,X2)),join(X0,X1)) = join(X0,meet(X1,X2)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',quasi_lattice2) ).

fof(f10,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,meet(X1,X2)),join(X0,X1)),
    inference(reorient_equations,[],[f9]) ).

fof(f11,axiom,
    ! [X2,X0,X1] : join(meet(join(meet(X0,X1),X2),X1),meet(X2,X0)) = meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',self_dual_distributivity) ).

fof(f12,negated_conjecture,
    meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distributivity) ).

fof(f13,definition,
    ~ sP0(join(meet(a,b),meet(a,c))),
    introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).

fof(f14,plain,
    sP0(meet(a,join(b,c))),
    inference(inequality_splitting,[],[f12,f13]) ).

fof(f15,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,join(X1,X2))),
    inference(forward_demodulation,[],[f8,f4]) ).

fof(f16,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(X0,meet(X1,X2))),
    inference(forward_demodulation,[],[f10,f3]) ).

fof(f17,plain,
    ! [X2,X0,X1] : join(meet(join(meet(X0,X1),X2),X1),meet(X2,X0)) = meet(join(X2,X0),join(meet(join(X0,X1),X2),X1)),
    inference(forward_demodulation,[],[f11,f3]) ).

fof(f18,plain,
    ! [X2,X0,X1] : join(meet(join(meet(X0,X1),X2),X1),meet(X2,X0)) = meet(join(X2,X0),join(X1,meet(join(X0,X1),X2))),
    inference(forward_demodulation,[],[f17,f4]) ).

fof(f19,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(X1,meet(join(X0,X1),X2))) = join(meet(X2,X0),meet(join(meet(X0,X1),X2),X1)),
    inference(forward_demodulation,[],[f18,f4]) ).

fof(f20,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(X1,meet(join(X0,X1),X2))) = join(meet(X2,X0),meet(X1,join(meet(X0,X1),X2))),
    inference(forward_demodulation,[],[f19,f3]) ).

fof(f26,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))) = meet(join(meet(X0,X1),X2),meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),
    inference(superposition,[],[f16,f20]) ).

fof(f28,plain,
    ! [X2,X3,X0,X1] : meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(join(X0,meet(X1,X2)),X3),join(X0,X1)))) = join(join(X0,meet(X1,X2)),meet(X3,join(meet(join(X0,meet(X1,X2)),X3),join(X0,X1)))),
    inference(superposition,[],[f20,f16]) ).

fof(f29,plain,
    ! [X2,X3,X0,X1] : meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(join(X0,meet(X1,X2)),X3),join(X0,X1)))) = join(X0,join(meet(X1,X2),meet(X3,join(meet(join(X0,meet(X1,X2)),X3),join(X0,X1))))),
    inference(forward_demodulation,[],[f28,f6]) ).

fof(f32,plain,
    ! [X2,X3,X0,X1] : meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(join(X0,meet(X1,X2)),X3),join(X0,X1)))) = join(X0,join(meet(X1,X2),meet(X3,join(join(X0,X1),meet(join(X0,meet(X1,X2)),X3))))),
    inference(forward_demodulation,[],[f29,f4]) ).

fof(f35,plain,
    ! [X2,X3,X0,X1] : meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(join(X0,meet(X1,X2)),X3),join(X0,X1)))) = join(X0,join(meet(X1,X2),meet(X3,join(X0,join(X1,meet(join(X0,meet(X1,X2)),X3)))))),
    inference(forward_demodulation,[],[f32,f6]) ).

fof(f37,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X1,X2),meet(X3,join(X0,join(X1,meet(join(X0,meet(X1,X2)),X3)))))) = meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(X0,X1),join(join(X0,meet(X1,X2)),X3)))),
    inference(forward_demodulation,[],[f35,f3]) ).

fof(f38,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X1,X2),meet(X3,join(X0,join(X1,meet(join(X0,meet(X1,X2)),X3)))))) = meet(join(join(X0,X1),join(X0,meet(X1,X2))),join(X3,meet(join(X0,X1),join(X0,join(meet(X1,X2),X3))))),
    inference(forward_demodulation,[],[f37,f6]) ).

fof(f39,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X1,X2),meet(X3,join(X0,join(X1,meet(join(X0,meet(X1,X2)),X3)))))) = meet(join(X0,join(X1,join(X0,meet(X1,X2)))),join(X3,meet(join(X0,X1),join(X0,join(meet(X1,X2),X3))))),
    inference(forward_demodulation,[],[f38,f6]) ).

fof(f43,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = meet(join(X2,X1),join(X2,meet(X0,X1))),
    inference(superposition,[],[f16,f3]) ).

fof(f44,plain,
    ! [X2,X0,X1] : meet(join(X2,X1),join(X0,meet(join(X1,X0),X2))) = join(meet(X2,X1),meet(X0,join(meet(X0,X1),X2))),
    inference(superposition,[],[f20,f3]) ).

fof(f45,plain,
    ! [X2,X0,X1] : meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))) = join(meet(X0,X1),meet(X2,join(meet(X0,X2),X1))),
    inference(superposition,[],[f20,f3]) ).

fof(f49,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))) = join(meet(X0,X1),meet(X2,join(X0,meet(X1,X2)))),
    inference(superposition,[],[f20,f4]) ).

fof(f50,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,X2)) = meet(join(X0,X1),join(X1,meet(X0,X2))),
    inference(superposition,[],[f16,f4]) ).

fof(f51,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X0),join(meet(X0,X1),X2)),
    inference(superposition,[],[f16,f4]) ).

fof(f52,plain,
    ! [X2,X3,X0,X1] : meet(join(X0,meet(X1,X2)),X3) = meet(join(X0,X1),meet(join(X0,meet(X1,X2)),X3)),
    inference(superposition,[],[f5,f16]) ).

fof(f54,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
    inference(superposition,[],[f5,f3]) ).

fof(f59,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
    inference(superposition,[],[f3,f5]) ).

fof(f62,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(X0,X1),X2),join(X3,meet(join(X2,X3),meet(X0,X1)))) = join(meet(X0,meet(X1,X2)),meet(X3,join(meet(X2,X3),meet(X0,X1)))),
    inference(superposition,[],[f20,f5]) ).

fof(f63,plain,
    ! [X2,X3,X0,X1] : meet(join(X3,X2),join(meet(X0,X1),meet(join(X2,meet(X0,X1)),X3))) = join(meet(X3,X2),meet(X0,meet(X1,join(meet(X2,meet(X0,X1)),X3)))),
    inference(superposition,[],[f20,f5]) ).

fof(f68,plain,
    ! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X0,X1),meet(X1,join(X0,X2))),
    inference(superposition,[],[f15,f3]) ).

fof(f73,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,X1),meet(X2,join(X0,X1))),
    inference(superposition,[],[f15,f4]) ).

fof(f74,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X0,X1),X0),join(X0,meet(X1,X2))),
    inference(superposition,[],[f15,f16]) ).

fof(f76,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = join(meet(X2,X0),meet(join(X0,X1),X2)),
    inference(superposition,[],[f15,f3]) ).

fof(f79,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,X1),X0),meet(X0,join(X1,X2))),
    inference(superposition,[],[f16,f15]) ).

fof(f82,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X1),X0))),
    inference(forward_demodulation,[],[f79,f59]) ).

fof(f85,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X0,join(X0,X1)),join(X0,meet(X1,X2))),
    inference(forward_demodulation,[],[f74,f3]) ).

fof(f89,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f82,f4]) ).

fof(f101,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X2,join(X2,X1)),join(X2,meet(X0,X1))),
    inference(superposition,[],[f85,f3]) ).

fof(f106,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(meet(X2,join(X2,X0)),join(meet(X0,X1),X2)),
    inference(superposition,[],[f85,f4]) ).

fof(f143,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
    inference(superposition,[],[f4,f6]) ).

fof(f162,plain,
    ! [X2,X0,X1] : meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))) = join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))),
    inference(superposition,[],[f49,f3]) ).

fof(f174,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(meet(X0,X1),join(X0,meet(X1,join(X0,X1)))),
    inference(superposition,[],[f49,f16]) ).

fof(f191,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(X0,join(meet(X1,join(X0,X1)),meet(X0,X1))),
    inference(forward_demodulation,[],[f174,f143]) ).

fof(f203,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(X0,join(meet(X0,X1),meet(X1,join(X0,X1)))),
    inference(forward_demodulation,[],[f191,f4]) ).

fof(f212,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,X1))) = meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))),
    inference(forward_demodulation,[],[f203,f68]) ).

fof(f220,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,X1))) = meet(join(X0,X1),join(X0,join(X1,meet(join(X1,join(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f212,f6]) ).

fof(f227,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,X1))) = meet(join(X0,X1),join(X0,join(X1,meet(X0,join(X1,join(X0,X1)))))),
    inference(forward_demodulation,[],[f220,f3]) ).

fof(f238,plain,
    ! [X2,X0,X1] : meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),X1))),
    inference(superposition,[],[f44,f3]) ).

fof(f388,plain,
    ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
    inference(superposition,[],[f6,f2]) ).

fof(f394,plain,
    ! [X0,X1] : meet(X0,X1) = meet(join(meet(X0,X1),X0),meet(X0,X1)),
    inference(superposition,[],[f16,f2]) ).

fof(f402,plain,
    ! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),join(meet(X0,X1),X0)),
    inference(forward_demodulation,[],[f394,f3]) ).

fof(f411,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(meet(X0,X1),X0))),
    inference(forward_demodulation,[],[f402,f5]) ).

fof(f420,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f411,f4]) ).

fof(f433,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
    inference(superposition,[],[f5,f1]) ).

fof(f434,plain,
    ! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X0,join(X0,X1))),
    inference(superposition,[],[f15,f1]) ).

fof(f438,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,meet(join(X0,X0),X1))) = join(meet(X1,X0),meet(X0,join(X0,X1))),
    inference(superposition,[],[f44,f1]) ).

fof(f442,plain,
    ! [X0,X1] : meet(join(X0,X0),join(X1,meet(join(X0,X1),X0))) = join(X0,meet(X1,join(X0,meet(X0,X1)))),
    inference(superposition,[],[f49,f1]) ).

fof(f443,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,meet(join(X0,X0),X1))) = join(meet(X1,X0),meet(X0,join(X1,X0))),
    inference(superposition,[],[f49,f1]) ).

fof(f444,plain,
    ! [X0,X1] : join(X1,X0) = join(meet(X1,join(X1,X0)),join(X1,X0)),
    inference(superposition,[],[f85,f1]) ).

fof(f448,plain,
    ! [X0,X1] : join(X1,X0) = join(join(X1,X0),meet(X1,join(X1,X0))),
    inference(forward_demodulation,[],[f444,f4]) ).

fof(f449,plain,
    ! [X0,X1] : meet(X0,join(X1,X0)) = meet(join(X1,X0),join(X0,meet(join(X0,X0),X1))),
    inference(forward_demodulation,[],[f443,f68]) ).

fof(f450,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(join(X0,X0),join(X1,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f442,f3]) ).

fof(f454,plain,
    ! [X0,X1] : join(meet(X1,X0),meet(X0,join(X0,X1))) = meet(join(X1,X0),join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f438,f2]) ).

fof(f463,plain,
    ! [X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,join(X1,X0)))),
    inference(forward_demodulation,[],[f448,f6]) ).

fof(f464,plain,
    ! [X0,X1] : meet(X0,join(X1,X0)) = meet(join(X1,X0),join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f449,f2]) ).

fof(f465,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(X0,join(X1,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f450,f2]) ).

fof(f473,plain,
    ! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X1,X0),meet(X0,join(X0,X1))),
    inference(backward_demodulation,[],[f454,f464]) ).

fof(f479,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,X1)),
    inference(superposition,[],[f433,f3]) ).

fof(f482,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),meet(X0,meet(X1,X2))),
    inference(superposition,[],[f433,f5]) ).

fof(f487,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(join(X0,meet(X0,X1)),X2))) = join(meet(X2,X0),meet(meet(X0,X1),join(meet(X0,X1),X2))),
    inference(superposition,[],[f20,f433]) ).

fof(f505,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(join(X0,meet(X0,X1)),X2))) = join(meet(X2,X0),meet(X0,meet(X1,join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f487,f5]) ).

fof(f508,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(meet(X1,X2),meet(X0,X1))),
    inference(forward_demodulation,[],[f482,f59]) ).

fof(f517,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(meet(X1,X2),X0))),
    inference(forward_demodulation,[],[f508,f59]) ).

fof(f523,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X1,meet(X2,X0)))),
    inference(forward_demodulation,[],[f517,f5]) ).

fof(f525,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X2,X0))),
    inference(forward_demodulation,[],[f523,f433]) ).

fof(f537,plain,
    ! [X0,X1] : meet(X1,join(X0,X1)) = join(X1,meet(X1,join(X0,X1))),
    inference(superposition,[],[f434,f4]) ).

fof(f547,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,join(X0,X1))) = join(meet(X2,X0),meet(X2,meet(X0,join(X0,X1)))),
    inference(superposition,[],[f15,f434]) ).

fof(f612,plain,
    ! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,X1),meet(X0,join(X0,X1))),
    inference(superposition,[],[f473,f3]) ).

fof(f615,plain,
    ! [X2,X0,X1] : meet(X2,join(meet(X0,X1),X2)) = join(meet(X0,meet(X1,X2)),meet(X2,join(X2,meet(X0,X1)))),
    inference(superposition,[],[f473,f5]) ).

fof(f621,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(meet(X0,join(X0,X1)),meet(X1,X0)),meet(meet(X1,X0),meet(X0,join(X1,X0)))),
    inference(superposition,[],[f473,f473]) ).

fof(f628,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,meet(X0,X1))) = join(meet(X2,meet(X0,X1)),meet(X0,meet(X1,join(meet(X0,X1),X2)))),
    inference(superposition,[],[f473,f5]) ).

fof(f635,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),join(meet(X0,join(X0,X1)),X2)) = join(meet(X0,join(X1,X0)),X2),
    inference(superposition,[],[f6,f473]) ).

fof(f639,plain,
    ! [X0,X1] : meet(meet(X1,X0),meet(X0,join(X1,X0))) = join(meet(X1,X0),meet(meet(X1,X0),meet(X0,join(X1,X0)))),
    inference(superposition,[],[f434,f473]) ).

fof(f640,plain,
    ! [X0,X1] : meet(X0,meet(join(X1,X0),meet(X1,X0))) = join(meet(X1,X0),meet(X0,meet(join(X1,X0),meet(X1,X0)))),
    inference(forward_demodulation,[],[f639,f59]) ).

fof(f649,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(X2,meet(X0,X1)))) = join(meet(X2,meet(X0,X1)),meet(X0,meet(X1,join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f628,f5]) ).

fof(f652,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(meet(X1,X0),meet(X0,join(X1,X0))),meet(meet(X0,join(X0,X1)),meet(X1,X0))),
    inference(forward_demodulation,[],[f621,f4]) ).

fof(f659,plain,
    ! [X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X1,X0)),
    inference(forward_demodulation,[],[f612,f73]) ).

fof(f662,plain,
    ! [X0,X1] : meet(X0,meet(join(X1,X0),X1)) = join(meet(X1,X0),meet(X0,meet(join(X1,X0),X1))),
    inference(forward_demodulation,[],[f640,f525]) ).

fof(f673,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(meet(X1,X0),meet(X0,join(X1,X0))),meet(meet(X1,X0),meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f652,f3]) ).

fof(f680,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X1,X0))) = join(meet(X1,X0),meet(X0,meet(X1,join(X1,X0)))),
    inference(forward_demodulation,[],[f662,f3]) ).

fof(f690,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(meet(X1,X0),meet(X0,join(X1,X0))),meet(X0,meet(join(X0,X1),meet(X1,X0)))),
    inference(forward_demodulation,[],[f673,f59]) ).

fof(f705,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X0,X1),meet(X1,X0))),meet(meet(X1,X0),meet(X0,join(X1,X0)))),
    inference(forward_demodulation,[],[f690,f4]) ).

fof(f719,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X0,X1),meet(X1,X0))),meet(X0,meet(join(X1,X0),meet(X1,X0)))),
    inference(forward_demodulation,[],[f705,f59]) ).

fof(f730,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X0,X1),meet(X1,X0))),meet(X0,meet(join(X1,X0),X1))),
    inference(forward_demodulation,[],[f719,f525]) ).

fof(f739,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X1,X0),X1)),meet(X0,meet(join(X0,X1),meet(X1,X0)))),
    inference(forward_demodulation,[],[f730,f4]) ).

fof(f743,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X1,X0),X1)),meet(X0,meet(join(X0,X1),X1))),
    inference(forward_demodulation,[],[f739,f525]) ).

fof(f745,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(join(X1,X0),X1)),meet(X0,meet(X1,join(X0,X1)))),
    inference(forward_demodulation,[],[f743,f3]) ).

fof(f747,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(join(X1,X0),X1))),
    inference(forward_demodulation,[],[f745,f4]) ).

fof(f748,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X0,join(X0,X1)),meet(X1,X0))) = join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(X1,join(X1,X0)))),
    inference(forward_demodulation,[],[f747,f3]) ).

fof(f749,plain,
    ! [X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),meet(X0,join(X0,X1)))) = join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(X1,join(X1,X0)))),
    inference(forward_demodulation,[],[f748,f659]) ).

fof(f750,plain,
    ! [X0,X1] : join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(X1,join(X1,X0)))) = meet(X1,meet(X0,join(meet(X1,X0),meet(X0,join(X0,X1))))),
    inference(forward_demodulation,[],[f749,f5]) ).

fof(f751,plain,
    ! [X0,X1] : join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(X1,join(X1,X0)))) = meet(X1,meet(X0,meet(X0,join(X1,X0)))),
    inference(forward_demodulation,[],[f750,f473]) ).

fof(f752,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = join(meet(X0,meet(X1,join(X0,X1))),meet(X0,meet(X1,join(X1,X0)))),
    inference(forward_demodulation,[],[f751,f433]) ).

fof(f762,plain,
    ! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
    inference(superposition,[],[f388,f4]) ).

fof(f765,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),join(X0,join(X1,X2))),
    inference(superposition,[],[f388,f6]) ).

fof(f785,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(join(X1,X2),join(X0,X1))),
    inference(forward_demodulation,[],[f765,f143]) ).

fof(f787,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,X1))) = meet(join(X0,X1),join(X0,join(X1,meet(X0,join(X0,X1))))),
    inference(backward_demodulation,[],[f227,f762]) ).

fof(f791,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(join(X1,X2),X0))),
    inference(forward_demodulation,[],[f785,f143]) ).

fof(f792,plain,
    ! [X0,X1] : join(X0,meet(X1,join(X0,X1))) = meet(join(X0,X1),join(X0,X1)),
    inference(forward_demodulation,[],[f787,f463]) ).

fof(f794,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(X1,join(X2,X0)))),
    inference(forward_demodulation,[],[f791,f6]) ).

fof(f795,plain,
    ! [X0,X1] : join(X0,X1) = join(X0,meet(X1,join(X0,X1))),
    inference(forward_demodulation,[],[f792,f1]) ).

fof(f797,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X1,join(X2,X0))),
    inference(forward_demodulation,[],[f794,f388]) ).

fof(f814,plain,
    ! [X0,X1] : join(X0,X1) = join(X1,meet(X0,join(X0,X1))),
    inference(superposition,[],[f795,f4]) ).

fof(f825,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),join(X0,X1))),
    inference(superposition,[],[f49,f795]) ).

fof(f837,plain,
    ! [X0,X1] : join(meet(X0,X1),X0) = meet(join(X0,X1),join(X0,meet(join(X1,X0),X0))),
    inference(superposition,[],[f44,f795]) ).

fof(f838,plain,
    ! [X0,X1] : join(meet(X0,X1),X1) = meet(join(X1,X0),join(X1,meet(join(X0,X1),X1))),
    inference(superposition,[],[f45,f795]) ).

fof(f847,plain,
    ! [X0,X1] : join(meet(X0,X1),X1) = meet(join(X1,X0),join(X1,meet(X1,join(X0,X1)))),
    inference(forward_demodulation,[],[f838,f3]) ).

fof(f848,plain,
    ! [X0,X1] : join(meet(X0,X1),X0) = meet(join(X0,X1),join(X0,meet(X0,join(X1,X0)))),
    inference(forward_demodulation,[],[f837,f3]) ).

fof(f856,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(meet(X0,X1),join(X0,X1)),
    inference(forward_demodulation,[],[f825,f1]) ).

fof(f869,plain,
    ! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X1,join(X0,meet(X0,X1)))),
    inference(backward_demodulation,[],[f465,f814]) ).

fof(f881,plain,
    ! [X0,X1] : join(meet(X0,X1),X1) = meet(join(X1,X0),meet(X1,join(X0,X1))),
    inference(forward_demodulation,[],[f847,f537]) ).

fof(f882,plain,
    ! [X0,X1] : join(meet(X0,X1),X0) = meet(join(X0,X1),meet(X0,join(X1,X0))),
    inference(forward_demodulation,[],[f848,f537]) ).

fof(f887,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(X1,join(meet(X0,X1),X0)),
    inference(forward_demodulation,[],[f856,f143]) ).

fof(f897,plain,
    ! [X0,X1] : join(meet(X0,X1),X1) = meet(X1,meet(join(X0,X1),join(X1,X0))),
    inference(forward_demodulation,[],[f881,f59]) ).

fof(f898,plain,
    ! [X0,X1] : join(meet(X0,X1),X0) = meet(X0,meet(join(X1,X0),join(X0,X1))),
    inference(forward_demodulation,[],[f882,f59]) ).

fof(f902,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),meet(join(X1,join(X0,X1)),X0))) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f887,f4]) ).

fof(f912,plain,
    ! [X0,X1] : join(X1,meet(X0,X1)) = meet(X1,meet(join(X0,X1),join(X1,X0))),
    inference(forward_demodulation,[],[f897,f4]) ).

fof(f913,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,meet(join(X1,X0),join(X0,X1))),
    inference(forward_demodulation,[],[f898,f4]) ).

fof(f916,plain,
    ! [X0,X1] : meet(join(X0,X1),join(X0,join(X1,meet(join(X1,join(X0,X1)),X0)))) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f902,f6]) ).

fof(f923,plain,
    ! [X0,X1] : meet(join(X0,X1),join(X0,join(X1,meet(X0,join(X1,join(X0,X1)))))) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f916,f3]) ).

fof(f927,plain,
    ! [X0,X1] : meet(join(X0,X1),join(X0,join(X1,meet(X0,join(X0,X1))))) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f923,f762]) ).

fof(f930,plain,
    ! [X0,X1] : meet(join(X0,X1),join(X0,join(X0,X1))) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f927,f814]) ).

fof(f931,plain,
    ! [X0,X1] : meet(join(X0,X1),join(X0,X1)) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f930,f388]) ).

fof(f932,plain,
    ! [X0,X1] : join(X0,X1) = join(X1,join(X0,meet(X0,X1))),
    inference(forward_demodulation,[],[f931,f1]) ).

fof(f939,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(meet(X1,meet(X0,X1)),X0),meet(join(X0,X1),join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0))))),
    inference(superposition,[],[f869,f20]) ).

fof(f942,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X0,meet(X1,meet(X0,X1))),meet(join(X0,X1),join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0))))),
    inference(superposition,[],[f869,f49]) ).

fof(f951,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,meet(X0,X1)),meet(join(X1,join(X0,meet(X0,X1))),X0))) = join(meet(X0,X1),meet(join(X0,meet(X0,X1)),meet(X0,join(X0,X1)))),
    inference(superposition,[],[f49,f869]) ).

fof(f955,plain,
    ! [X2,X0,X1] : join(meet(X0,join(X0,X1)),X2) = join(X0,join(meet(X1,join(X0,meet(X0,X1))),X2)),
    inference(superposition,[],[f6,f869]) ).

fof(f976,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,meet(X0,X1)),meet(join(X1,join(X0,meet(X0,X1))),X0))) = join(meet(X0,X1),meet(meet(X0,join(X0,X1)),join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f951,f3]) ).

fof(f983,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0)),join(X0,meet(X1,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f942,f59]) ).

fof(f986,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0)),join(meet(X1,meet(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f939,f59]) ).

fof(f998,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,meet(X0,X1)),meet(join(X1,join(X0,meet(X0,X1))),X0))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),join(X0,meet(X0,X1))))),
    inference(forward_demodulation,[],[f976,f5]) ).

fof(f1005,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(X0,meet(X1,meet(X0,X1))),join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0))))),
    inference(forward_demodulation,[],[f983,f3]) ).

fof(f1008,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(meet(X1,meet(X0,X1)),X0),join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0))))),
    inference(forward_demodulation,[],[f986,f3]) ).

fof(f1017,plain,
    ! [X0,X1] : meet(join(X0,X1),join(join(X0,meet(X0,X1)),meet(join(X1,join(X0,meet(X0,X1))),X0))) = join(meet(X0,X1),meet(X0,join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f998,f43]) ).

fof(f1021,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X0,meet(X1,meet(X0,X1))),join(meet(X0,X1),meet(join(X1,meet(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f1005,f52]) ).

fof(f1024,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(meet(X1,meet(X0,X1)),X0),meet(join(X1,meet(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f1008,f76]) ).

fof(f1031,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),join(join(X0,meet(X0,X1)),meet(join(X1,join(X0,meet(X0,X1))),X0))),
    inference(forward_demodulation,[],[f1017,f814]) ).

fof(f1033,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X0,meet(X1,meet(X0,X1))),meet(join(X1,meet(X0,X1)),X0))),
    inference(forward_demodulation,[],[f1021,f76]) ).

fof(f1036,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(meet(join(X1,meet(X0,X1)),X0),join(meet(X1,meet(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f1024,f3]) ).

fof(f1042,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),join(X0,join(meet(X0,X1),meet(join(X1,join(X0,meet(X0,X1))),X0)))),
    inference(forward_demodulation,[],[f1031,f6]) ).

fof(f1043,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(meet(join(X1,meet(X0,X1)),X0),join(X0,meet(X1,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1033,f3]) ).

fof(f1046,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(join(X1,meet(X0,X1)),meet(X0,join(meet(X1,meet(X0,X1)),X0))))),
    inference(forward_demodulation,[],[f1036,f5]) ).

fof(f1050,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),join(X0,meet(join(X1,join(X0,meet(X0,X1))),X0))),
    inference(forward_demodulation,[],[f1042,f76]) ).

fof(f1051,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(join(X1,meet(X0,X1)),meet(X0,join(X0,meet(X1,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1043,f5]) ).

fof(f1054,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(join(X0,X1),meet(X0,meet(join(meet(X1,meet(X0,X1)),X0),join(X1,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1046,f59]) ).

fof(f1056,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),join(X0,meet(X0,join(X1,join(X0,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1050,f3]) ).

fof(f1057,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(X0,meet(join(X0,meet(X1,meet(X0,X1))),join(X1,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1051,f59]) ).

fof(f1060,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(X0,meet(meet(join(meet(X1,meet(X0,X1)),X0),join(X1,meet(X0,X1))),join(X0,X1)))),
    inference(forward_demodulation,[],[f1054,f59]) ).

fof(f1062,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),join(X0,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f1056,f932]) ).

fof(f1063,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(X0,meet(join(X1,meet(X0,X1)),join(X0,meet(X1,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1057,f3]) ).

fof(f1066,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(meet(X1,meet(X0,X1)),X0),join(X1,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1060,f3]) ).

fof(f1067,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(join(X0,X1),meet(X0,join(X0,X1))),
    inference(forward_demodulation,[],[f1062,f434]) ).

fof(f1068,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X0,meet(join(X1,meet(X0,X1)),join(X0,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1063,f479]) ).

fof(f1071,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(meet(X1,meet(X0,X1)),X0))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(X1,meet(X0,X1)),join(meet(X1,meet(X0,X1)),X0))))),
    inference(forward_demodulation,[],[f1066,f3]) ).

fof(f1072,plain,
    ! [X0,X1] : join(X0,meet(X0,X1)) = meet(X0,meet(join(X0,X1),join(X0,X1))),
    inference(forward_demodulation,[],[f1067,f59]) ).

fof(f1073,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X0,join(X1,meet(X0,X1)))),
    inference(forward_demodulation,[],[f1068,f89]) ).

fof(f1076,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X1,meet(X0,X1))))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(X1,meet(X0,X1)),join(X0,meet(X1,meet(X0,X1))))))),
    inference(forward_demodulation,[],[f1071,f4]) ).

fof(f1077,plain,
    ! [X0,X1] : meet(X0,join(X0,X1)) = join(X0,meet(X0,X1)),
    inference(forward_demodulation,[],[f1072,f1]) ).

fof(f1078,plain,
    ! [X0,X1] : meet(X0,join(X1,meet(X0,X1))) = meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f1073,f15]) ).

fof(f1081,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),join(X0,meet(X0,X1)))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(X1,meet(X0,X1)),join(X0,meet(X0,X1)))))),
    inference(forward_demodulation,[],[f1076,f479]) ).

fof(f1082,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),meet(X0,join(X0,X1)))),
    inference(backward_demodulation,[],[f89,f1077]) ).

fof(f1084,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,meet(X0,join(X0,X1)))),
    inference(backward_demodulation,[],[f420,f1077]) ).

fof(f1090,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),meet(X0,meet(X1,join(meet(X0,X1),X2)))) = meet(join(X2,X0),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2))),
    inference(backward_demodulation,[],[f505,f1077]) ).

fof(f1103,plain,
    ! [X0,X1] : meet(X0,join(X0,X1)) = meet(X0,meet(join(X1,X0),join(X0,X1))),
    inference(backward_demodulation,[],[f913,f1077]) ).

fof(f1105,plain,
    ! [X2,X0,X1] : join(meet(X0,join(X0,X1)),X2) = join(X0,join(meet(X1,meet(X0,join(X0,X1))),X2)),
    inference(backward_demodulation,[],[f955,f1077]) ).

fof(f1122,plain,
    ! [X0,X1] : meet(X0,join(X1,meet(X0,X1))) = meet(X0,meet(X1,join(meet(X0,X1),join(X0,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1078,f5]) ).

fof(f1125,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),meet(X0,join(X0,X1)))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(X1,meet(X0,X1)),meet(X0,join(X0,X1)))))),
    inference(forward_demodulation,[],[f1081,f1077]) ).

fof(f1135,plain,
    ! [X0,X1] : meet(X1,join(X1,X0)) = join(X1,meet(X0,X1)),
    inference(backward_demodulation,[],[f912,f1103]) ).

fof(f1140,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),meet(X0,meet(X1,join(meet(X0,X1),X2)))) = meet(join(X2,X0),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2)))),
    inference(forward_demodulation,[],[f1090,f5]) ).

fof(f1146,plain,
    ! [X0,X1] : meet(X0,join(X1,meet(X0,X1))) = meet(X0,meet(X1,join(X0,join(meet(X0,X1),meet(X0,X1))))),
    inference(forward_demodulation,[],[f1122,f143]) ).

fof(f1149,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),meet(X0,join(X0,X1)))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),meet(join(X1,meet(X0,X1)),X0)))),
    inference(forward_demodulation,[],[f1125,f525]) ).

fof(f1163,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(X0,join(X1,meet(X0,X1))),
    inference(forward_demodulation,[],[f1146,f2]) ).

fof(f1166,plain,
    ! [X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),meet(X0,join(X0,X1)))) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),join(X1,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1149,f525]) ).

fof(f1178,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X0,meet(X0,X1)))) = meet(X0,meet(X1,join(X1,X0))),
    inference(forward_demodulation,[],[f1163,f1135]) ).

fof(f1181,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(X0,join(X1,meet(X0,X1)))) = meet(meet(X0,X1),join(meet(X0,X1),meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f1166,f50]) ).

fof(f1188,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X1,X0))) = meet(X0,meet(X1,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f1178,f1077]) ).

fof(f1191,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(X0,join(X1,meet(X0,X1)))) = meet(X0,meet(X1,join(meet(X0,X1),meet(X0,join(X0,X1))))),
    inference(forward_demodulation,[],[f1181,f5]) ).

fof(f1197,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X1,X0))),
    inference(forward_demodulation,[],[f1188,f1084]) ).

fof(f1200,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(X0,join(X1,meet(X0,X1)))) = meet(X0,meet(X1,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f1191,f73]) ).

fof(f1203,plain,
    ! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
    inference(backward_demodulation,[],[f680,f1197]) ).

fof(f1205,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = join(meet(X0,meet(X1,join(X0,X1))),meet(X0,X1)),
    inference(backward_demodulation,[],[f752,f1197]) ).

fof(f1208,plain,
    ! [X2,X0,X1] : join(X0,join(meet(X1,X0),X2)) = join(meet(X0,join(X0,X1)),X2),
    inference(backward_demodulation,[],[f1105,f1197]) ).

fof(f1212,plain,
    ! [X0,X1] : meet(X0,meet(X1,X0)) = join(meet(X0,X1),meet(X0,join(X1,meet(X0,X1)))),
    inference(forward_demodulation,[],[f1200,f1197]) ).

fof(f1214,plain,
    ! [X2,X0,X1] : join(meet(X0,join(X1,X0)),X2) = join(meet(X1,X0),join(X0,join(meet(X1,X0),X2))),
    inference(backward_demodulation,[],[f635,f1208]) ).

fof(f1223,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X0),join(X0,meet(X1,X2)))),
    inference(backward_demodulation,[],[f85,f1208]) ).

fof(f1224,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X2),join(X2,meet(X0,X1)))),
    inference(backward_demodulation,[],[f101,f1208]) ).

fof(f1225,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X2),join(meet(X0,X1),X2))),
    inference(backward_demodulation,[],[f106,f1208]) ).

fof(f1228,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = join(meet(X0,X1),meet(X0,meet(X1,join(X0,X1)))),
    inference(forward_demodulation,[],[f1205,f4]) ).

fof(f1232,plain,
    ! [X0,X1] : meet(X0,meet(X1,X0)) = meet(X0,join(X1,meet(X0,X1))),
    inference(forward_demodulation,[],[f1212,f15]) ).

fof(f1236,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X2),meet(X0,X1))),
    inference(forward_demodulation,[],[f1225,f797]) ).

fof(f1237,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(X2,join(meet(X0,X1),meet(X1,X2)))),
    inference(forward_demodulation,[],[f1224,f143]) ).

fof(f1238,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(X0,join(meet(X1,X2),meet(X1,X0)))),
    inference(forward_demodulation,[],[f1223,f143]) ).

fof(f1240,plain,
    ! [X2,X0,X1] : join(meet(X0,join(X1,X0)),X2) = join(X0,join(join(meet(X1,X0),X2),meet(X1,X0))),
    inference(forward_demodulation,[],[f1214,f143]) ).

fof(f1244,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X1,X0))) = meet(X0,meet(X1,X0)),
    inference(forward_demodulation,[],[f1232,f1135]) ).

fof(f1248,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X0,X1),meet(X1,X2))),
    inference(forward_demodulation,[],[f1237,f388]) ).

fof(f1249,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X1,X0))),
    inference(forward_demodulation,[],[f1238,f388]) ).

fof(f1251,plain,
    ! [X2,X0,X1] : join(meet(X0,join(X1,X0)),X2) = join(X0,join(meet(X1,X0),join(meet(X1,X0),X2))),
    inference(forward_demodulation,[],[f1240,f4]) ).

fof(f1255,plain,
    ! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X1,X0))),
    inference(forward_demodulation,[],[f1244,f479]) ).

fof(f1259,plain,
    ! [X2,X0,X1] : join(X0,join(meet(X1,X0),X2)) = join(meet(X0,join(X1,X0)),X2),
    inference(forward_demodulation,[],[f1251,f388]) ).

fof(f1271,plain,
    ! [X2,X0,X1] : meet(X2,join(X2,meet(X0,X1))) = join(X2,meet(X0,meet(X1,X2))),
    inference(superposition,[],[f1135,f5]) ).

fof(f1349,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
    inference(superposition,[],[f1077,f5]) ).

fof(f1394,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = join(meet(X0,X1),meet(X0,meet(X1,X2))),
    inference(forward_demodulation,[],[f1349,f5]) ).

fof(f1423,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,join(X0,X1))) = meet(X2,meet(X0,join(meet(X2,X0),join(X0,X1)))),
    inference(backward_demodulation,[],[f547,f1394]) ).

fof(f1425,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = meet(X0,meet(X1,join(meet(X0,X1),join(X0,X1)))),
    inference(backward_demodulation,[],[f1228,f1394]) ).

fof(f1442,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = meet(X0,meet(X1,join(X1,join(meet(X0,X1),X0)))),
    inference(forward_demodulation,[],[f1425,f143]) ).

fof(f1443,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,join(X0,X1))) = meet(X2,meet(X0,join(X0,join(X1,meet(X2,X0))))),
    inference(forward_demodulation,[],[f1423,f143]) ).

fof(f1461,plain,
    ! [X0,X1] : meet(X1,meet(X0,join(X1,X0))) = meet(X0,meet(X1,join(X1,join(X0,meet(X0,X1))))),
    inference(forward_demodulation,[],[f1442,f4]) ).

fof(f1479,plain,
    ! [X0,X1] : meet(X0,meet(X1,join(X1,X0))) = meet(X1,meet(X0,join(X1,X0))),
    inference(forward_demodulation,[],[f1461,f1443]) ).

fof(f1495,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X1,meet(X0,join(X1,X0))),
    inference(forward_demodulation,[],[f1479,f1197]) ).

fof(f1629,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X1,X2),meet(X2,join(X0,X1))),
    inference(superposition,[],[f68,f4]) ).

fof(f1806,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X0,join(X2,meet(X0,X1)))),
    inference(superposition,[],[f73,f433]) ).

fof(f1823,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X0,X1),meet(X1,X2)),join(X0,meet(X1,X2))),
    inference(superposition,[],[f73,f16]) ).

fof(f1825,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = join(meet(X2,X1),meet(join(X0,X1),X2)),
    inference(superposition,[],[f73,f3]) ).

fof(f1840,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,X2),X0),meet(X0,join(X1,X2))),
    inference(superposition,[],[f16,f73]) ).

fof(f1850,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X2),X0))),
    inference(forward_demodulation,[],[f1840,f59]) ).

fof(f1865,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(join(X0,meet(X1,X2)),meet(join(X0,X1),meet(X1,X2))),
    inference(forward_demodulation,[],[f1823,f4]) ).

fof(f1872,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X0,meet(X0,X2)))),
    inference(forward_demodulation,[],[f1850,f4]) ).

fof(f1886,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(join(X0,X1),meet(X1,X2)))),
    inference(forward_demodulation,[],[f1865,f6]) ).

fof(f1887,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),meet(X0,join(X0,X2)))),
    inference(forward_demodulation,[],[f1872,f1077]) ).

fof(f1901,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(meet(X1,X2),join(meet(X1,X2),join(X0,X1)))),
    inference(forward_demodulation,[],[f1886,f1135]) ).

fof(f1913,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(meet(X1,X2),join(X0,X1))))),
    inference(forward_demodulation,[],[f1901,f5]) ).

fof(f1922,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(X1,join(meet(X1,X2),X0))))),
    inference(forward_demodulation,[],[f1913,f143]) ).

fof(f1978,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(join(meet(X1,X0),X2),meet(X0,meet(X0,join(X0,X1))))),
    inference(superposition,[],[f1082,f1135]) ).

fof(f1979,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(meet(X0,X1),X2),meet(X0,meet(X0,join(X0,X1))))),
    inference(superposition,[],[f1082,f1077]) ).

fof(f1985,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(meet(X0,join(X0,X1)),join(X1,X2))),
    inference(superposition,[],[f1082,f3]) ).

fof(f2022,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(X0,meet(join(X0,X1),join(X1,X2)))),
    inference(forward_demodulation,[],[f1985,f5]) ).

fof(f2027,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(X0,meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f1979,f59]) ).

fof(f2028,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(X0,meet(meet(X0,join(X0,X1)),join(meet(X1,X0),X2)))),
    inference(forward_demodulation,[],[f1978,f59]) ).

fof(f2063,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,X1),join(X1,X2))),
    inference(forward_demodulation,[],[f2022,f433]) ).

fof(f2068,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2))),
    inference(forward_demodulation,[],[f2027,f433]) ).

fof(f2069,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(meet(X0,join(X0,X1)),join(meet(X1,X0),X2))),
    inference(forward_demodulation,[],[f2028,f433]) ).

fof(f2093,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(X0,meet(join(X0,X1),join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f2068,f5]) ).

fof(f2094,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2)))),
    inference(forward_demodulation,[],[f2069,f5]) ).

fof(f2112,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(X0,X1),join(meet(X0,X1),X2))),
    inference(forward_demodulation,[],[f2093,f433]) ).

fof(f2113,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X1,X0),X2)) = meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2))),
    inference(forward_demodulation,[],[f2094,f433]) ).

fof(f2181,plain,
    ! [X2,X0,X1] : join(X1,meet(X2,X0)) = meet(join(X0,X1),join(X1,meet(X2,X0))),
    inference(superposition,[],[f43,f4]) ).

fof(f2198,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,X1),join(X1,X2)),meet(X0,join(X1,X2))),
    inference(superposition,[],[f43,f15]) ).

fof(f2199,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,X2),join(X1,X2)),meet(X0,join(X1,X2))),
    inference(superposition,[],[f43,f73]) ).

fof(f2200,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X1,X0),join(X1,X2)),meet(X0,join(X1,X2))),
    inference(superposition,[],[f43,f68]) ).

fof(f2206,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X1),join(meet(X0,X1),X2)),
    inference(superposition,[],[f43,f4]) ).

fof(f2247,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X1,X0),join(X1,X2))),
    inference(forward_demodulation,[],[f2200,f3]) ).

fof(f2248,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X0,X2),join(X1,X2))),
    inference(forward_demodulation,[],[f2199,f3]) ).

fof(f2249,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X0,X1),join(X1,X2))),
    inference(forward_demodulation,[],[f2198,f3]) ).

fof(f2283,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X1,X0),join(X1,X2)))),
    inference(forward_demodulation,[],[f2247,f5]) ).

fof(f2284,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X2),join(X1,X2)))),
    inference(forward_demodulation,[],[f2248,f5]) ).

fof(f2285,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,X1),join(X1,X2)))),
    inference(forward_demodulation,[],[f2249,f5]) ).

fof(f2307,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X1,join(X2,meet(X1,X0))))),
    inference(forward_demodulation,[],[f2283,f143]) ).

fof(f2308,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X2,join(meet(X0,X2),X1)))),
    inference(forward_demodulation,[],[f2284,f143]) ).

fof(f2309,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X1,join(X2,meet(X0,X1))))),
    inference(forward_demodulation,[],[f2285,f143]) ).

fof(f2364,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(meet(X0,X1),X3)) = meet(meet(X0,join(X1,X2)),join(meet(X0,join(X1,X2)),meet(meet(X0,X1),X3))),
    inference(superposition,[],[f50,f15]) ).

fof(f2371,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(meet(X0,join(X0,X1)),join(meet(X1,X0),meet(X0,X2))),
    inference(superposition,[],[f50,f1135]) ).

fof(f2373,plain,
    ! [X2,X0,X1] : join(join(X0,X1),meet(X0,X2)) = meet(join(X0,X1),join(join(X0,X1),meet(X0,X2))),
    inference(superposition,[],[f50,f388]) ).

fof(f2395,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X0,X2),join(meet(X0,X1),X2)),
    inference(superposition,[],[f50,f4]) ).

fof(f2398,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(join(X1,X0),meet(X1,X2)),join(X0,meet(X1,X2))),
    inference(superposition,[],[f73,f50]) ).

fof(f2433,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(join(X0,meet(X1,X2)),meet(join(X1,X0),meet(X1,X2))),
    inference(forward_demodulation,[],[f2398,f4]) ).

fof(f2449,plain,
    ! [X2,X0,X1] : join(X0,join(X1,meet(X0,X2))) = meet(join(X0,X1),join(X0,join(X1,meet(X0,X2)))),
    inference(forward_demodulation,[],[f2373,f6]) ).

fof(f2451,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,meet(join(X0,X1),join(meet(X1,X0),meet(X0,X2)))),
    inference(forward_demodulation,[],[f2371,f5]) ).

fof(f2456,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(meet(X0,X1),X3)) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,X2)),meet(meet(X0,X1),X3)))),
    inference(forward_demodulation,[],[f2364,f5]) ).

fof(f2474,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(join(X1,X0),meet(X1,X2)))),
    inference(forward_demodulation,[],[f2433,f6]) ).

fof(f2486,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(X2,meet(X1,X0)))),
    inference(backward_demodulation,[],[f2307,f2449]) ).

fof(f2488,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X0,X2)) = meet(X0,join(meet(X1,X0),meet(X0,X2))),
    inference(forward_demodulation,[],[f2451,f2113]) ).

fof(f2492,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))))),
    inference(forward_demodulation,[],[f2456,f5]) ).

fof(f2508,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(meet(X1,X2),join(meet(X1,X2),join(X1,X0)))),
    inference(forward_demodulation,[],[f2474,f1135]) ).

fof(f2525,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(meet(X1,X2),join(X1,X0))))),
    inference(forward_demodulation,[],[f2508,f5]) ).

fof(f2539,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(X1,join(X0,meet(X1,X2)))))),
    inference(forward_demodulation,[],[f2525,f143]) ).

fof(f2549,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(X1,X0)))),
    inference(forward_demodulation,[],[f2539,f2486]) ).

fof(f3233,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,join(meet(X1,X2),meet(X0,X1))),
    inference(superposition,[],[f1249,f3]) ).

fof(f3241,plain,
    ! [X2,X0,X1] : join(join(X1,X2),meet(X0,X1)) = join(join(X1,X2),meet(X0,join(X1,X2))),
    inference(superposition,[],[f1249,f15]) ).

fof(f3248,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,join(meet(X0,X1),meet(X0,X2))),
    inference(superposition,[],[f1249,f4]) ).

fof(f3286,plain,
    ! [X2,X0,X1] : join(join(X1,X2),meet(X0,X1)) = meet(join(X1,X2),join(join(X1,X2),X0)),
    inference(forward_demodulation,[],[f3241,f1135]) ).

fof(f3317,plain,
    ! [X2,X0,X1] : meet(join(X1,X2),join(X1,join(X2,X0))) = join(join(X1,X2),meet(X0,X1)),
    inference(forward_demodulation,[],[f3286,f6]) ).

fof(f3329,plain,
    ! [X2,X0,X1] : join(X1,join(X2,meet(X0,X1))) = meet(join(X1,X2),join(X1,join(X2,X0))),
    inference(forward_demodulation,[],[f3317,f6]) ).

fof(f3348,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(X2,meet(meet(X0,X1),X1)))),
    inference(backward_demodulation,[],[f2309,f3329]) ).

fof(f3376,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(X2,meet(X1,meet(X0,X1))))),
    inference(forward_demodulation,[],[f3348,f3]) ).

fof(f3394,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X1,join(X2,meet(X0,X1)))),
    inference(forward_demodulation,[],[f3376,f479]) ).

fof(f3473,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(meet(X2,join(meet(X1,X2),X0)),meet(X0,X1)),X3)) = join(meet(meet(X0,X1),meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),X3),
    inference(superposition,[],[f1208,f20]) ).

fof(f3474,plain,
    ! [X2,X3,X0,X1] : join(meet(meet(X0,X1),meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),X3) = join(meet(X0,X1),join(meet(meet(X2,join(meet(X2,X1),X0)),meet(X0,X1)),X3)),
    inference(superposition,[],[f1208,f44]) ).

fof(f3510,plain,
    ! [X2,X0,X1] : join(X0,join(meet(X1,X0),X2)) = meet(join(X2,X0),join(X0,join(meet(X1,X0),X2))),
    inference(superposition,[],[f51,f1208]) ).

fof(f3516,plain,
    ! [X2,X0,X1] : meet(join(join(X0,X1),X0),join(X2,meet(join(X0,X2),join(X0,X1)))) = join(X0,join(meet(X1,X0),meet(X2,join(meet(X0,X2),join(X0,X1))))),
    inference(superposition,[],[f45,f1208]) ).

fof(f3567,plain,
    ! [X2,X0,X1] : meet(join(join(X0,X1),X0),join(X2,meet(join(X0,X2),join(X0,X1)))) = join(X0,join(meet(X1,X0),meet(X2,join(X0,join(X1,meet(X0,X2)))))),
    inference(forward_demodulation,[],[f3516,f143]) ).

fof(f3573,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,join(meet(X0,X2),X1))),
    inference(backward_demodulation,[],[f2308,f3510]) ).

fof(f3606,plain,
    ! [X2,X3,X0,X1] : join(meet(meet(X0,X1),meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),X3) = join(meet(X0,X1),join(meet(meet(X0,X1),meet(X2,join(meet(X2,X1),X0))),X3)),
    inference(forward_demodulation,[],[f3474,f3]) ).

fof(f3607,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(meet(X2,join(meet(X1,X2),X0)),meet(X0,X1)),X3)) = join(meet(X0,meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),X3),
    inference(forward_demodulation,[],[f3473,f5]) ).

fof(f3617,plain,
    ! [X2,X0,X1] : meet(join(join(X0,X1),X0),join(X2,meet(join(X0,X2),join(X0,X1)))) = join(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))),
    inference(forward_demodulation,[],[f3567,f2486]) ).

fof(f3649,plain,
    ! [X2,X3,X0,X1] : join(meet(meet(X0,X1),meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),X3) = join(meet(X0,X1),join(meet(X0,meet(X1,meet(X2,join(meet(X2,X1),X0)))),X3)),
    inference(forward_demodulation,[],[f3606,f5]) ).

fof(f3650,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),X3) = join(meet(X0,X1),join(meet(meet(X0,X1),meet(X2,join(meet(X1,X2),X0))),X3)),
    inference(forward_demodulation,[],[f3607,f3]) ).

fof(f3656,plain,
    ! [X2,X0,X1] : join(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))) = meet(join(X0,join(X0,X1)),join(X2,meet(join(X0,X2),join(X0,X1)))),
    inference(forward_demodulation,[],[f3617,f4]) ).

fof(f3682,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),X3) = join(meet(X0,X1),join(meet(X0,meet(X1,meet(X2,join(meet(X2,X1),X0)))),X3)),
    inference(forward_demodulation,[],[f3649,f5]) ).

fof(f3683,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),X3) = join(meet(X0,X1),join(meet(X0,meet(X1,meet(X2,join(meet(X1,X2),X0)))),X3)),
    inference(forward_demodulation,[],[f3650,f5]) ).

fof(f3687,plain,
    ! [X2,X0,X1] : join(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))) = meet(join(X0,X1),join(X2,meet(join(X0,X2),join(X0,X1)))),
    inference(forward_demodulation,[],[f3656,f388]) ).

fof(f3746,plain,
    ! [X2,X3,X0,X1] : meet(X3,meet(X0,meet(X1,X2))) = meet(X2,meet(X3,meet(X0,X1))),
    inference(superposition,[],[f59,f5]) ).

fof(f3791,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X1,meet(X0,meet(X1,X2))),
    inference(superposition,[],[f433,f59]) ).

fof(f3792,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,meet(X1,X2))) = meet(X1,join(X1,meet(X2,X0))),
    inference(superposition,[],[f1077,f59]) ).

fof(f3819,plain,
    ! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X0,X1))) = join(meet(X0,meet(X1,X2)),meet(X2,join(X3,meet(X0,X1)))),
    inference(superposition,[],[f73,f59]) ).

fof(f3834,plain,
    ! [X2,X0,X1] : meet(X2,join(X2,meet(X0,X1))) = meet(X2,join(meet(X0,X1),X2)),
    inference(backward_demodulation,[],[f615,f3819]) ).

fof(f3863,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(X0,join(X0,X2))),
    inference(backward_demodulation,[],[f1887,f3791]) ).

fof(f3983,plain,
    ! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X0,X1))),
    inference(superposition,[],[f143,f6]) ).

fof(f3994,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X2,join(X0,meet(X1,X2))),X3)) = join(X3,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0)))),
    inference(superposition,[],[f143,f49]) ).

fof(f4033,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X1,join(X0,join(X1,X2))),
    inference(superposition,[],[f388,f143]) ).

fof(f4084,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X1,X2),meet(X3,join(X0,join(X1,meet(join(X0,meet(X1,X2)),X3)))))) = meet(join(X1,join(X0,meet(X1,X2))),join(X3,meet(join(X0,X1),join(X0,join(meet(X1,X2),X3))))),
    inference(backward_demodulation,[],[f39,f4033]) ).

fof(f4177,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,meet(X0,join(X0,X1))),meet(X2,join(X0,X1))),
    inference(superposition,[],[f73,f814]) ).

fof(f4206,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(X2,join(X0,X1)),meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f4177,f4]) ).

fof(f4566,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,X3),meet(X0,X1)) = join(meet(X0,X1),join(meet(X0,meet(X1,X2)),meet(X2,X3))),
    inference(superposition,[],[f1236,f59]) ).

fof(f4596,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X1),meet(X0,X2))),
    inference(superposition,[],[f1236,f4]) ).

fof(f4731,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X0,X1),meet(X2,X1))),
    inference(superposition,[],[f3233,f3]) ).

fof(f5070,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X2,meet(X0,meet(X1,join(meet(X0,X1),X2)))),
    inference(superposition,[],[f1255,f5]) ).

fof(f5141,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,meet(X1,join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f5070,f5]) ).

fof(f5179,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,meet(join(X0,X1),join(X2,meet(join(X1,X2),X0))))),X3) = join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)),
    inference(backward_demodulation,[],[f3683,f5141]) ).

fof(f5211,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X0,meet(X1,meet(X2,join(meet(X2,X1),X0)))),X3)) = join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)),
    inference(backward_demodulation,[],[f3682,f5179]) ).

fof(f5298,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X0)) = join(meet(X0,X1),meet(meet(X0,X1),join(X2,X0))),
    inference(superposition,[],[f1629,f433]) ).

fof(f5337,plain,
    ! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = join(meet(X3,meet(X0,X1)),meet(X0,meet(X1,join(X2,X3)))),
    inference(superposition,[],[f1629,f5]) ).

fof(f5350,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,join(X1,X2)),X2),meet(X0,join(X1,X2))),
    inference(superposition,[],[f51,f1629]) ).

fof(f5352,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = join(meet(meet(X0,join(X1,X2)),X0),meet(X2,meet(X0,join(X1,X2)))),
    inference(superposition,[],[f44,f1629]) ).

fof(f5370,plain,
    ! [X2,X3,X0,X1] : join(X3,meet(X0,join(X1,X2))) = join(meet(X2,X0),join(meet(X0,join(X1,X2)),X3)),
    inference(superposition,[],[f143,f1629]) ).

fof(f5394,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = join(meet(X0,meet(X0,join(X1,X2))),meet(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f5352,f3]) ).

fof(f5396,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X1,X2)),join(meet(X0,join(X1,X2)),X2)),
    inference(forward_demodulation,[],[f5350,f3]) ).

fof(f5407,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = meet(X0,meet(X1,join(X2,meet(X0,X1)))),
    inference(backward_demodulation,[],[f649,f5337]) ).

fof(f5429,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X0)) = meet(meet(X0,X1),join(meet(X0,X1),join(X2,X0))),
    inference(forward_demodulation,[],[f5298,f1077]) ).

fof(f5447,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = join(meet(X0,join(X1,X2)),meet(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f5394,f433]) ).

fof(f5449,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,X2)),X2))),
    inference(forward_demodulation,[],[f5396,f5]) ).

fof(f5468,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X0)) = meet(X0,meet(X1,join(meet(X0,X1),join(X2,X0)))),
    inference(forward_demodulation,[],[f5429,f5]) ).

fof(f5483,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = meet(meet(X0,join(X1,X2)),join(meet(X0,join(X1,X2)),X2)),
    inference(forward_demodulation,[],[f5447,f1135]) ).

fof(f5485,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X1,X2),join(X2,meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f5449,f5407]) ).

fof(f5502,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(X0,join(meet(X0,X1),X2)))) = meet(meet(X0,X1),join(X2,X0)),
    inference(forward_demodulation,[],[f5468,f143]) ).

fof(f5514,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,X2)),X2))),
    inference(forward_demodulation,[],[f5483,f5]) ).

fof(f5527,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(X2,X0))) = meet(X0,meet(X1,join(X0,join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f5502,f5]) ).

fof(f5538,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = meet(X0,meet(join(X1,X2),join(X2,meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f5514,f5407]) ).

fof(f5550,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(X2,join(X0,X1)))),
    inference(backward_demodulation,[],[f1922,f5527]) ).

fof(f5558,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f5538,f5485]) ).

fof(f5572,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(X0,meet(join(X1,X2),join(X0,X2))))),
    inference(forward_demodulation,[],[f5558,f59]) ).

fof(f5577,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f5572,f2549]) ).

fof(f5582,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X0,meet(X0,join(X1,X2))),join(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f5577,f4]) ).

fof(f5586,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(meet(X0,join(X0,join(X1,X2))),join(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f5582,f1077]) ).

fof(f5588,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,meet(join(X0,join(X1,X2)),join(X2,meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f5586,f5]) ).

fof(f5598,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(meet(X0,X1),X2)) = join(meet(X1,X0),meet(meet(X0,X1),meet(X2,meet(X0,X1)))),
    inference(superposition,[],[f5550,f1203]) ).

fof(f5622,plain,
    ! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(X0,meet(X1,meet(join(X0,X1),X2))),
    inference(superposition,[],[f5550,f3]) ).

fof(f5626,plain,
    ! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,meet(join(X1,X2),X2))),
    inference(superposition,[],[f5550,f59]) ).

fof(f5655,plain,
    ! [X2,X0,X1] : join(X1,join(meet(X0,X1),meet(X0,X2))) = join(X1,meet(X0,meet(X2,join(meet(X0,X1),X0)))),
    inference(superposition,[],[f3248,f5550]) ).

fof(f5672,plain,
    ! [X2,X0,X1] : join(X1,join(meet(X0,X1),meet(X0,X2))) = join(X1,meet(X0,meet(X2,join(X0,meet(X0,X1))))),
    inference(forward_demodulation,[],[f5655,f4]) ).

fof(f5691,plain,
    ! [X2,X0,X1] : join(X1,meet(X2,X0)) = join(X1,meet(X0,meet(X2,join(X1,X2)))),
    inference(forward_demodulation,[],[f5626,f3]) ).

fof(f5712,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(meet(X0,X1),X2)) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
    inference(forward_demodulation,[],[f5598,f479]) ).

fof(f5728,plain,
    ! [X2,X0,X1] : join(X1,join(meet(X0,X1),meet(X0,X2))) = join(X1,meet(X0,meet(X2,meet(X0,join(X0,X1))))),
    inference(forward_demodulation,[],[f5672,f1077]) ).

fof(f5753,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,meet(X0,X1))) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
    inference(forward_demodulation,[],[f5712,f5]) ).

fof(f5764,plain,
    ! [X2,X0,X1] : join(X1,join(meet(X0,X1),meet(X0,X2))) = join(X1,meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f5728,f3791]) ).

fof(f5785,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f5764,f1236]) ).

fof(f6539,plain,
    ! [X2,X0,X1] : meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(join(meet(X0,join(X1,X0)),X2),X1))) = join(meet(X0,X1),meet(X2,join(X1,meet(meet(X0,join(X1,X0)),X2)))),
    inference(superposition,[],[f49,f1495]) ).

fof(f6543,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X1,meet(meet(X0,join(X1,X0)),X2)),
    inference(superposition,[],[f59,f1495]) ).

fof(f6580,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X1,meet(X0,meet(join(X1,X0),X2))),
    inference(forward_demodulation,[],[f6543,f5]) ).

fof(f6582,plain,
    ! [X2,X0,X1] : meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(join(meet(X0,join(X1,X0)),X2),X1))) = join(meet(X0,X1),meet(X2,join(X1,meet(X0,meet(join(X1,X0),X2))))),
    inference(forward_demodulation,[],[f6539,f5]) ).

fof(f6631,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)) = join(meet(join(X2,meet(join(X1,X2),X0)),meet(X1,X0)),X3),
    inference(backward_demodulation,[],[f5179,f6580]) ).

fof(f6638,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(join(meet(X0,join(X1,X0)),X2),X1))),
    inference(forward_demodulation,[],[f6582,f5622]) ).

fof(f6672,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)) = join(meet(meet(X1,X0),join(X2,meet(join(X1,X2),X0))),X3),
    inference(forward_demodulation,[],[f6631,f3]) ).

fof(f6680,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(X1,join(meet(X0,join(X1,X0)),X2)))),
    inference(forward_demodulation,[],[f6638,f3]) ).

fof(f6708,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)) = join(meet(X1,meet(X0,join(X2,meet(join(X1,X2),X0)))),X3),
    inference(forward_demodulation,[],[f6672,f5]) ).

fof(f6715,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(X1,join(X0,join(meet(X1,X0),X2))))),
    inference(forward_demodulation,[],[f6680,f1259]) ).

fof(f6730,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,meet(X0,join(X1,X0))),join(X2,meet(X1,join(X2,X0)))),
    inference(forward_demodulation,[],[f6715,f3573]) ).

fof(f6741,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,X0),join(X2,meet(X1,join(X2,X0)))),
    inference(forward_demodulation,[],[f6730,f795]) ).

fof(f6822,plain,
    ! [X2,X0,X1] : meet(meet(X1,X0),join(meet(X1,X0),X2)) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
    inference(superposition,[],[f1077,f54]) ).

fof(f6845,plain,
    ! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(X1,join(meet(X1,X0),X2)))),
    inference(superposition,[],[f1197,f54]) ).

fof(f6865,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)) = join(meet(X0,X1),join(meet(X0,meet(X2,X1)),X3)),
    inference(backward_demodulation,[],[f5211,f6845]) ).

fof(f6878,plain,
    ! [X2,X0,X1] : meet(X1,meet(X0,join(meet(X1,X0),X2))) = join(meet(X1,X0),meet(X0,meet(X1,X2))),
    inference(forward_demodulation,[],[f6822,f5]) ).

fof(f6908,plain,
    ! [X2,X0,X1] : meet(X1,meet(X0,join(meet(X1,X0),X2))) = join(meet(X1,X0),meet(X2,meet(X0,X1))),
    inference(backward_demodulation,[],[f5753,f6878]) ).

fof(f7013,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = join(meet(X0,meet(join(X1,X2),X0)),meet(X2,meet(X0,join(X1,X2)))),
    inference(superposition,[],[f62,f73]) ).

fof(f7132,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = join(meet(join(X1,X2),X0),meet(X2,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f7013,f479]) ).

fof(f7237,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = meet(join(X1,X2),meet(X0,join(meet(join(X1,X2),X0),X2))),
    inference(forward_demodulation,[],[f7132,f6908]) ).

fof(f7313,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(join(X0,X2),meet(X0,join(X1,X2))))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7237,f5407]) ).

fof(f7377,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(X0,meet(join(X1,X2),join(X0,X2))))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7313,f59]) ).

fof(f7428,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,join(X1,X2)),X0),join(X2,meet(X0,join(X1,X2)))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7377,f2549]) ).

fof(f7472,plain,
    ! [X2,X0,X1] : meet(join(X0,meet(X0,join(X1,X2))),join(X2,meet(X0,join(X1,X2)))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7428,f4]) ).

fof(f7506,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,join(X1,X2))),join(X2,meet(X0,join(X1,X2)))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7472,f1077]) ).

fof(f7539,plain,
    ! [X2,X0,X1] : meet(X0,meet(join(X0,join(X1,X2)),join(X2,meet(X0,join(X1,X2))))) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7506,f5]) ).

fof(f7571,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X1,X2),meet(X0,join(X2,meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f7539,f5588]) ).

fof(f8193,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(join(meet(X2,meet(X0,X1)),X1),meet(meet(X0,X1),join(meet(X0,X1),X2))),
    inference(superposition,[],[f2206,f1135]) ).

fof(f8225,plain,
    ! [X2,X3,X0,X1] : meet(X3,join(meet(X0,X1),X2)) = meet(join(X2,X1),meet(join(meet(X0,X1),X2),X3)),
    inference(superposition,[],[f59,f2206]) ).

fof(f8298,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(join(meet(X0,X1),X2),meet(join(meet(X2,meet(X0,X1)),X1),meet(X0,X1))),
    inference(forward_demodulation,[],[f8193,f59]) ).

fof(f8377,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X2,meet(X0,X1)),X1))),
    inference(forward_demodulation,[],[f8298,f59]) ).

fof(f8436,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(meet(X0,X1),join(meet(X2,meet(X0,X1)),X1)),
    inference(forward_demodulation,[],[f8377,f2113]) ).

fof(f8477,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(X0,meet(X1,join(meet(X2,meet(X0,X1)),X1))),
    inference(forward_demodulation,[],[f8436,f5]) ).

fof(f8505,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(X0,meet(X1,join(X1,meet(X2,meet(X0,X1))))),
    inference(forward_demodulation,[],[f8477,f3834]) ).

fof(f8529,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(X0,meet(X1,meet(X1,join(X1,meet(X2,X0))))),
    inference(forward_demodulation,[],[f8505,f1271]) ).

fof(f8548,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(meet(X0,X1),X2)) = meet(X0,meet(X1,join(X1,meet(X2,X0)))),
    inference(forward_demodulation,[],[f8529,f433]) ).

fof(f8560,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(meet(X0,X1),X2))) = meet(X0,meet(X1,join(X1,meet(X2,X0)))),
    inference(forward_demodulation,[],[f8548,f5]) ).

fof(f8567,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2)))) = join(meet(X2,X0),meet(X0,meet(X1,join(X1,meet(X2,X0))))),
    inference(backward_demodulation,[],[f1140,f8560]) ).

fof(f8569,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X0,meet(X1,X2))) = meet(X0,meet(X1,join(X1,meet(X2,X0)))),
    inference(backward_demodulation,[],[f1394,f8560]) ).

fof(f8585,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,meet(X0,X1))) = meet(X1,meet(X0,join(X0,meet(X2,X1)))),
    inference(backward_demodulation,[],[f6908,f8560]) ).

fof(f8596,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,meet(join(X1,X2),join(join(X1,X2),meet(meet(X0,meet(X1,X3)),X0)))),
    inference(backward_demodulation,[],[f2492,f8560]) ).

fof(f8604,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,meet(join(X1,X2),join(X1,join(X2,meet(meet(X0,meet(X1,X3)),X0))))),
    inference(forward_demodulation,[],[f8596,f6]) ).

fof(f8617,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2)))) = join(meet(X1,X0),meet(X2,X0)),
    inference(forward_demodulation,[],[f8567,f5785]) ).

fof(f8622,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,join(X1,join(X2,meet(meet(meet(X0,meet(X1,X3)),X0),X1)))),
    inference(forward_demodulation,[],[f8604,f3329]) ).

fof(f8637,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,join(X1,join(X2,meet(X1,meet(meet(X0,meet(X1,X3)),X0))))),
    inference(forward_demodulation,[],[f8622,f3]) ).

fof(f8647,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,join(X1,join(X2,meet(X1,meet(X0,meet(X0,meet(X1,X3))))))),
    inference(forward_demodulation,[],[f8637,f3]) ).

fof(f8652,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,join(X1,join(X2,meet(X1,meet(X0,meet(X1,X3)))))),
    inference(forward_demodulation,[],[f8647,f433]) ).

fof(f8655,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),meet(X0,meet(X1,X3))) = meet(X0,join(X1,join(X2,meet(X0,meet(X1,X3))))),
    inference(forward_demodulation,[],[f8652,f3791]) ).

fof(f8658,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,join(X1,meet(X2,meet(X0,join(X0,X1)))))),
    inference(backward_demodulation,[],[f4206,f8655]) ).

fof(f8659,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X0,join(meet(X0,X2),X1))),
    inference(forward_demodulation,[],[f8658,f5785]) ).

fof(f8661,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(X0,X2))) = meet(X0,meet(X1,join(X2,X0))),
    inference(backward_demodulation,[],[f5527,f8659]) ).

fof(f9528,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0))) = meet(join(meet(X0,meet(X1,join(X0,X1))),X2),meet(join(X0,X1),join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0)))),
    inference(superposition,[],[f26,f795]) ).

fof(f9561,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2))) = meet(join(meet(X2,X0),meet(X0,X1)),meet(join(X2,X0),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2)))),
    inference(superposition,[],[f26,f1077]) ).

fof(f9733,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2))) = meet(join(X2,X0),meet(join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2)),join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f9561,f59]) ).

fof(f9766,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0))) = meet(join(X0,X1),meet(join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0)),join(meet(X0,meet(X1,join(X0,X1))),X2))),
    inference(forward_demodulation,[],[f9528,f59]) ).

fof(f9905,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2))) = meet(join(X2,X0),meet(join(meet(X2,X0),meet(X0,X1)),join(meet(X0,X1),meet(meet(X0,join(X0,X1)),X2)))),
    inference(forward_demodulation,[],[f9733,f3]) ).

fof(f9938,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0))) = meet(join(X0,X1),meet(join(meet(X0,meet(X1,join(X0,X1))),X2),join(X2,meet(join(meet(X1,join(X0,X1)),X2),X0)))),
    inference(forward_demodulation,[],[f9766,f3]) ).

fof(f10067,plain,
    ! [X2,X0,X1] : meet(join(X2,X0),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2)))) = meet(join(X2,X0),meet(join(meet(X2,X0),meet(X0,X1)),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2))))),
    inference(forward_demodulation,[],[f9905,f5]) ).

fof(f10095,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(X0,join(meet(X1,join(X0,X1)),X2)))) = meet(join(X0,X1),meet(join(meet(X0,meet(X1,join(X0,X1))),X2),join(X2,meet(X0,join(meet(X1,join(X0,X1)),X2))))),
    inference(forward_demodulation,[],[f9938,f3]) ).

fof(f10202,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(join(X2,X0),meet(join(meet(X2,X0),meet(X0,X1)),join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2))))),
    inference(forward_demodulation,[],[f10067,f8617]) ).

fof(f10221,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(X0,join(X1,join(meet(X0,X1),X2))))) = meet(join(X0,X1),meet(join(meet(X0,meet(X1,join(X0,X1))),X2),join(X2,meet(X0,join(X1,join(meet(X0,X1),X2)))))),
    inference(forward_demodulation,[],[f10095,f1259]) ).

fof(f10333,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(X0,join(X2,X1)))) = meet(join(X0,X1),meet(join(meet(X0,meet(X1,join(X0,X1))),X2),join(X2,meet(X0,join(X2,X1))))),
    inference(forward_demodulation,[],[f10221,f3573]) ).

fof(f10437,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X2,meet(X0,join(X2,X1)))) = meet(join(X0,X1),meet(join(meet(X1,X0),X2),join(X2,meet(X0,join(X2,X1))))),
    inference(forward_demodulation,[],[f10333,f1495]) ).

fof(f11650,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X0,X1),join(X2,meet(X0,X1)))),
    inference(superposition,[],[f3394,f433]) ).

fof(f11828,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(X2,meet(X0,X1))),
    inference(forward_demodulation,[],[f11650,f762]) ).

fof(f12101,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = meet(join(X2,X1),join(meet(X1,X0),meet(X1,meet(join(X0,X1),X2)))),
    inference(superposition,[],[f8617,f4]) ).

fof(f12103,plain,
    ! [X2,X0,X1] : join(meet(meet(X0,join(X0,X1)),X1),meet(X2,X1)) = meet(join(X2,X1),join(meet(X1,meet(X0,join(X0,X1))),meet(X1,meet(join(X0,X1),X2)))),
    inference(superposition,[],[f8617,f814]) ).

fof(f12135,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X0,X1),join(meet(X1,X2),meet(X0,meet(X1,join(X1,X2))))),
    inference(superposition,[],[f8617,f59]) ).

fof(f12155,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(join(X2,X1),meet(X1,X0)),join(meet(X0,X1),meet(X2,X1))),
    inference(superposition,[],[f15,f8617]) ).

fof(f12172,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(X0,X1),meet(X2,X1)),X3) = meet(join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))),meet(join(X2,X1),X3)),
    inference(superposition,[],[f54,f8617]) ).

fof(f12230,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(X0,X1),meet(X2,X1)),X3) = meet(join(X2,X1),meet(X3,join(meet(X1,X0),meet(X1,meet(join(X1,X0),X2))))),
    inference(forward_demodulation,[],[f12172,f59]) ).

fof(f12245,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X2,X1),join(meet(join(X2,X1),meet(X1,X0)),meet(X0,X1))),
    inference(forward_demodulation,[],[f12155,f143]) ).

fof(f12291,plain,
    ! [X2,X0,X1] : join(meet(meet(X0,join(X0,X1)),X1),meet(X2,X1)) = meet(join(X2,X1),join(meet(X1,X0),meet(X1,meet(join(X0,X1),X2)))),
    inference(forward_demodulation,[],[f12103,f1197]) ).

fof(f12376,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(join(meet(X1,X0),meet(X2,X0)),join(meet(X2,X0),meet(X0,X1))),
    inference(backward_demodulation,[],[f10202,f12230]) ).

fof(f12388,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X2,X1),join(meet(X0,X1),meet(join(X2,X1),meet(X1,X0)))),
    inference(forward_demodulation,[],[f12245,f4]) ).

fof(f12426,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(meet(X0,join(X0,X1)),X1),meet(X2,X1)),
    inference(forward_demodulation,[],[f12291,f12101]) ).

fof(f12506,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X2,X1),meet(X0,meet(X1,join(X1,meet(join(X2,X1),X0))))),
    inference(forward_demodulation,[],[f12388,f8585]) ).

fof(f12540,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X1,meet(X0,join(X0,X1))),meet(X2,X1)),
    inference(forward_demodulation,[],[f12426,f3]) ).

fof(f12638,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X1,X0),meet(X2,X1)),
    inference(forward_demodulation,[],[f12540,f1197]) ).

fof(f13888,plain,
    ! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X2,X1),meet(join(X0,X1),X2)))) = join(meet(X2,meet(join(X0,X1),X2)),meet(X1,meet(join(X0,X1),X2))),
    inference(superposition,[],[f45,f1825]) ).

fof(f13897,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(meet(X2,X1),X2),meet(join(X0,X1),X2)),
    inference(superposition,[],[f43,f1825]) ).

fof(f13959,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(join(meet(X2,X1),X2),join(X0,X1))),
    inference(forward_demodulation,[],[f13897,f59]) ).

fof(f13968,plain,
    ! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X2,X1),meet(join(X0,X1),X2)))) = join(meet(join(X0,X1),X2),meet(X1,meet(join(X0,X1),X2))),
    inference(forward_demodulation,[],[f13888,f479]) ).

fof(f14046,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(join(X2,meet(X2,X1)),join(X0,X1))),
    inference(forward_demodulation,[],[f13959,f4]) ).

fof(f14054,plain,
    ! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X2,X1),meet(join(X0,X1),X2)))) = meet(meet(join(X0,X1),X2),join(meet(join(X0,X1),X2),X1)),
    inference(forward_demodulation,[],[f13968,f1135]) ).

fof(f14110,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(meet(X2,join(X2,X1)),join(X0,X1))),
    inference(forward_demodulation,[],[f14046,f1077]) ).

fof(f14118,plain,
    ! [X2,X0,X1] : meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X2,X1),meet(join(X0,X1),X2)))) = meet(join(X0,X1),meet(X2,join(meet(join(X0,X1),X2),X1))),
    inference(forward_demodulation,[],[f14054,f5]) ).

fof(f14159,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(X2,meet(join(X2,X1),join(X0,X1)))),
    inference(forward_demodulation,[],[f14110,f5]) ).

fof(f14165,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X2,X1),meet(join(X0,X1),X2)))),
    inference(forward_demodulation,[],[f14118,f5407]) ).

fof(f14198,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(X2,meet(join(X2,X1),join(X0,X1))),
    inference(forward_demodulation,[],[f14159,f433]) ).

fof(f14202,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(X2,meet(join(X2,X1),join(X0,X1))))),
    inference(forward_demodulation,[],[f14165,f59]) ).

fof(f14229,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(join(meet(join(X0,X1),X2),X2),join(X1,meet(join(X0,X1),X2))),
    inference(forward_demodulation,[],[f14202,f14198]) ).

fof(f14242,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(join(X2,meet(join(X0,X1),X2)),join(X1,meet(join(X0,X1),X2))),
    inference(forward_demodulation,[],[f14229,f4]) ).

fof(f14253,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(meet(X2,join(X2,join(X0,X1))),join(X1,meet(join(X0,X1),X2))),
    inference(forward_demodulation,[],[f14242,f1135]) ).

fof(f14263,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(X2,join(X1,meet(join(X0,X1),X2)))) = meet(X2,meet(join(X2,join(X0,X1)),join(X1,meet(join(X0,X1),X2)))),
    inference(forward_demodulation,[],[f14253,f5]) ).

fof(f14270,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X2,join(X0,X1)),join(X1,meet(join(X0,X1),X2)))),
    inference(forward_demodulation,[],[f14263,f7571]) ).

fof(f14301,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(meet(X0,join(X0,X1)),join(meet(X1,X0),meet(X2,X0))),
    inference(superposition,[],[f2181,f1135]) ).

fof(f14328,plain,
    ! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = meet(join(meet(X2,X0),X3),join(X3,meet(X0,meet(X1,X2)))),
    inference(superposition,[],[f2181,f59]) ).

fof(f14509,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(X0,meet(join(X0,X1),join(meet(X1,X0),meet(X2,X0)))),
    inference(forward_demodulation,[],[f14301,f5]) ).

fof(f14597,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(X2,X0)) = meet(X0,join(meet(X1,X0),meet(X2,X0))),
    inference(forward_demodulation,[],[f14509,f2113]) ).

fof(f14917,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(join(X2,meet(X1,X0)),meet(X0,meet(X0,join(X0,X1)))),
    inference(superposition,[],[f3863,f1135]) ).

fof(f14919,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(join(X2,meet(X0,X1)),meet(X0,meet(X0,join(X0,X1)))),
    inference(superposition,[],[f3863,f1077]) ).

fof(f15000,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X0,X2)),join(meet(X0,join(X1,X2)),meet(join(X1,X2),X3))) = join(meet(X0,join(X0,X2)),meet(join(X1,X2),X3)),
    inference(superposition,[],[f3248,f3863]) ).

fof(f15006,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X0,X2)),join(meet(X0,join(X1,X2)),meet(join(X1,X2),X3))) = join(X0,join(meet(X2,X0),meet(join(X1,X2),X3))),
    inference(forward_demodulation,[],[f15000,f1208]) ).

fof(f15069,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,meet(meet(X0,join(X0,X1)),join(X2,meet(X0,X1)))),
    inference(forward_demodulation,[],[f14919,f59]) ).

fof(f15071,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,meet(meet(X0,join(X0,X1)),join(X2,meet(X1,X0)))),
    inference(forward_demodulation,[],[f14917,f59]) ).

fof(f15101,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X2,X0),meet(join(X1,X2),X3))) = join(X0,join(meet(X2,X0),join(meet(X0,join(X1,X2)),meet(join(X1,X2),X3)))),
    inference(forward_demodulation,[],[f15006,f1208]) ).

fof(f15148,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1))))),
    inference(forward_demodulation,[],[f15069,f5]) ).

fof(f15150,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,meet(X0,meet(join(X0,X1),join(X2,meet(X1,X0))))),
    inference(forward_demodulation,[],[f15071,f5]) ).

fof(f15170,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X2,X0),meet(join(X1,X2),X3))) = join(X0,join(meet(join(X1,X2),X3),meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f15101,f5370]) ).

fof(f15200,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))),
    inference(forward_demodulation,[],[f15148,f433]) ).

fof(f15201,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X1,X0))) = meet(X0,meet(join(X0,X1),join(X2,meet(X1,X0)))),
    inference(forward_demodulation,[],[f15150,f433]) ).

fof(f15220,plain,
    ! [X2,X3,X0,X1] : join(X0,meet(join(X1,X2),X3)) = join(X0,join(meet(X2,X0),meet(join(X1,X2),X3))),
    inference(forward_demodulation,[],[f15170,f3233]) ).

fof(f15249,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,meet(X0,join(X1,X2)))),
    inference(backward_demodulation,[],[f5588,f15200]) ).

fof(f15252,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,meet(join(X0,X1),X2))),
    inference(backward_demodulation,[],[f14270,f15201]) ).

fof(f15288,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X1,meet(X2,X0)),X3)) = join(meet(X1,meet(X0,join(X1,X2))),X3),
    inference(backward_demodulation,[],[f6708,f15252]) ).

fof(f15299,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,join(meet(X1,X0),meet(X2,join(X0,X1)))),
    inference(backward_demodulation,[],[f3687,f15252]) ).

fof(f15332,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),join(meet(X0,meet(X2,X1)),X3)) = join(meet(X1,meet(X0,join(X1,X2))),X3),
    inference(backward_demodulation,[],[f6865,f15288]) ).

fof(f16617,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,meet(X2,join(meet(X1,meet(X0,X2)),X0)))) = join(X1,meet(join(X0,X1),join(meet(X0,X2),meet(join(X1,meet(X0,X2)),X0)))),
    inference(superposition,[],[f3248,f63]) ).

fof(f16737,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,meet(X2,join(meet(X1,meet(X0,X2)),X0)))) = join(X1,meet(join(X0,X1),join(meet(X0,X2),meet(X0,join(X1,meet(X0,X2)))))),
    inference(forward_demodulation,[],[f16617,f3]) ).

fof(f16876,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,meet(X2,join(meet(X1,meet(X0,X2)),X0)))) = join(X1,meet(join(X0,X1),meet(X0,join(X1,meet(X0,X2))))),
    inference(forward_demodulation,[],[f16737,f1806]) ).

fof(f16983,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,meet(X2,join(meet(X1,meet(X0,X2)),X0)))) = join(X1,meet(X0,meet(join(X1,meet(X0,X2)),join(X0,X1)))),
    inference(forward_demodulation,[],[f16876,f59]) ).

fof(f17075,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,join(X1,meet(X0,X2)))) = join(X1,meet(X0,meet(X2,join(meet(X1,meet(X0,X2)),X0)))),
    inference(forward_demodulation,[],[f16983,f2549]) ).

fof(f17150,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,join(X1,meet(X0,X2)))) = join(X1,meet(X0,meet(X2,join(X0,meet(X1,meet(X0,X2)))))),
    inference(forward_demodulation,[],[f17075,f8661]) ).

fof(f17209,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,join(X1,meet(X0,X2)))) = join(X1,meet(X0,meet(X2,meet(X0,join(X0,meet(X2,X1)))))),
    inference(forward_demodulation,[],[f17150,f3792]) ).

fof(f17260,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,join(X1,meet(X0,X2)))) = join(X1,meet(X2,meet(X0,join(X0,meet(X2,X1))))),
    inference(forward_demodulation,[],[f17209,f3791]) ).

fof(f17561,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X1,join(X2,meet(X0,X1)))),
    inference(superposition,[],[f73,f479]) ).

fof(f17572,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X1)) = join(meet(X0,X1),meet(meet(X0,X1),join(X2,X1))),
    inference(superposition,[],[f1629,f479]) ).

fof(f17607,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X1)) = meet(meet(X0,X1),join(meet(X0,X1),join(X2,X1))),
    inference(forward_demodulation,[],[f17572,f1077]) ).

fof(f17664,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X1)) = meet(X0,meet(X1,join(meet(X0,X1),join(X2,X1)))),
    inference(forward_demodulation,[],[f17607,f5]) ).

fof(f17711,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),join(X2,X1)) = meet(X0,meet(X1,join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f17664,f8560]) ).

fof(f17748,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,join(X2,X1))) = meet(X0,meet(X1,join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f17711,f5]) ).

fof(f17776,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = join(meet(X2,X1),meet(X0,meet(X1,join(X2,X1)))),
    inference(backward_demodulation,[],[f12506,f17748]) ).

fof(f17841,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,X1),X0),join(X2,meet(join(X0,X2),meet(X0,X1)))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))),
    inference(superposition,[],[f238,f433]) ).

fof(f18122,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,X1),X0),join(X2,meet(X0,meet(X1,join(X0,X2))))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f17841,f59]) ).

fof(f18244,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))) = meet(join(meet(X0,X1),X0),join(X2,meet(X0,X1))),
    inference(forward_demodulation,[],[f18122,f2549]) ).

fof(f18354,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))) = meet(join(X0,meet(X0,X1)),join(X2,meet(X0,X1))),
    inference(forward_demodulation,[],[f18244,f4]) ).

fof(f18446,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f18354,f1077]) ).

fof(f18529,plain,
    ! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,meet(X0,X1)))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f18446,f5]) ).

fof(f18594,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X2,join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f18529,f15200]) ).

fof(f21015,plain,
    ! [X2,X3,X0,X1] : join(meet(meet(X0,X1),X2),meet(X3,X2)) = join(meet(X3,X2),meet(X0,meet(X1,meet(X2,join(X3,X2))))),
    inference(superposition,[],[f17776,f5]) ).

fof(f21022,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,meet(meet(X1,join(X2,X1)),X2)),meet(X1,join(meet(X0,X1),meet(X2,X1)))),
    inference(superposition,[],[f62,f17776]) ).

fof(f21026,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X2,meet(X0,meet(X1,join(X2,X1)))),meet(X1,join(meet(X0,X1),meet(X2,X1)))),
    inference(superposition,[],[f45,f17776]) ).

fof(f21129,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X2,meet(X0,meet(X1,join(X2,X1)))),join(meet(X0,X1),meet(X2,X1))),
    inference(forward_demodulation,[],[f21026,f14597]) ).

fof(f21133,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,meet(meet(X1,join(X2,X1)),X2)),join(meet(X0,X1),meet(X2,X1))),
    inference(forward_demodulation,[],[f21022,f14597]) ).

fof(f21140,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,X2)),meet(X3,X2)) = join(meet(X3,X2),meet(X0,meet(X1,meet(X2,join(X3,X2))))),
    inference(forward_demodulation,[],[f21015,f5]) ).

fof(f21247,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(join(meet(X0,X1),meet(X2,X1)),meet(X2,meet(X0,meet(X1,join(X2,X1))))),
    inference(forward_demodulation,[],[f21129,f4]) ).

fof(f21251,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(join(meet(X0,X1),meet(X2,X1)),meet(X0,meet(meet(X1,join(X2,X1)),X2))),
    inference(forward_demodulation,[],[f21133,f4]) ).

fof(f21337,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,X1),join(meet(X2,X1),meet(X2,meet(X0,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21247,f6]) ).

fof(f21341,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,X1),join(meet(X2,X1),meet(X0,meet(meet(X1,join(X2,X1)),X2)))),
    inference(forward_demodulation,[],[f21251,f6]) ).

fof(f21410,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,X1),join(meet(X2,meet(X0,X1)),meet(X2,X1))),
    inference(forward_demodulation,[],[f21337,f21140]) ).

fof(f21414,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,X1),join(meet(X2,X1),meet(X0,meet(X2,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21341,f3]) ).

fof(f21472,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21410,f1236]) ).

fof(f21475,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X0,X1),join(meet(X0,meet(X2,X1)),meet(X2,X1))),
    inference(forward_demodulation,[],[f21414,f21140]) ).

fof(f21535,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,X1)))),
    inference(forward_demodulation,[],[f21472,f525]) ).

fof(f21538,plain,
    ! [X2,X0,X1] : meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))) = join(meet(X1,meet(X0,join(X1,X2))),meet(X2,X1)),
    inference(forward_demodulation,[],[f21475,f15332]) ).

fof(f21599,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),meet(X1,join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f21535,f1271]) ).

fof(f21602,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21538,f4]) ).

fof(f21649,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X1,meet(join(X2,X1),X0)),meet(join(meet(X0,meet(X1,join(X2,X1))),X2),X1)),
    inference(forward_demodulation,[],[f21599,f59]) ).

fof(f21652,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),join(X1,meet(join(X2,X1),meet(X0,X1)))),
    inference(forward_demodulation,[],[f21602,f525]) ).

fof(f21693,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(meet(X0,meet(X1,join(X2,X1))),X2))),
    inference(forward_demodulation,[],[f21649,f59]) ).

fof(f21695,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(join(meet(X0,meet(X1,join(X2,X1))),X2),meet(X1,join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f21652,f1271]) ).

fof(f21729,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(X2,meet(X0,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21693,f4]) ).

fof(f21731,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(join(X1,meet(join(X2,X1),X0)),meet(join(meet(X0,meet(X1,join(X2,X1))),X2),X1)),
    inference(forward_demodulation,[],[f21695,f59]) ).

fof(f21758,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(X2,meet(X1,X0)))),
    inference(forward_demodulation,[],[f21729,f5691]) ).

fof(f21760,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(meet(X0,meet(X1,join(X2,X1))),X2))),
    inference(forward_demodulation,[],[f21731,f59]) ).

fof(f21785,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(X2,meet(X1,X0)),join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f21758,f3]) ).

fof(f21787,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(X2,meet(X0,meet(X1,join(X2,X1)))))),
    inference(forward_demodulation,[],[f21760,f4]) ).

fof(f21806,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(X1,meet(join(X1,meet(join(X2,X1),X0)),join(X2,meet(X1,X0)))),
    inference(forward_demodulation,[],[f21787,f5691]) ).

fof(f21819,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))) = meet(X1,meet(join(X2,meet(X1,X0)),join(X1,meet(join(X2,X1),X0)))),
    inference(forward_demodulation,[],[f21806,f3]) ).

fof(f21828,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f21819,f21785]) ).

fof(f21879,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X0,X2)),meet(X3,join(X1,X2))) = join(meet(X0,join(X0,X2)),join(meet(X3,join(X1,X2)),meet(X0,join(X1,X2)))),
    inference(superposition,[],[f1248,f3863]) ).

fof(f21908,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(join(meet(X0,X1),X2),join(meet(X1,X2),meet(join(X2,meet(X1,X2)),meet(X0,X1))))),
    inference(superposition,[],[f1248,f62]) ).

fof(f22032,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(meet(X0,X1),X2),join(meet(meet(X1,X2),join(meet(X0,X1),meet(X2,meet(X1,X2)))),join(meet(X2,meet(X1,X2)),meet(X0,X1)))),
    inference(forward_demodulation,[],[f21908,f3994]) ).

fof(f22052,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X0,X2)),meet(X3,join(X1,X2))) = join(X0,join(meet(X2,X0),join(meet(X3,join(X1,X2)),meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f21879,f1208]) ).

fof(f22104,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),join(meet(meet(X0,X1),X2),join(meet(meet(X1,X2),join(meet(X0,X1),meet(X2,meet(X1,X2)))),meet(X2,meet(X1,X2))))),
    inference(forward_demodulation,[],[f22032,f3983]) ).

fof(f22120,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X2,X0),join(meet(X3,join(X1,X2)),meet(X0,join(X1,X2))))) = join(X0,join(meet(X2,X0),meet(X3,join(X1,X2)))),
    inference(forward_demodulation,[],[f22052,f1208]) ).

fof(f22143,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),join(meet(meet(X0,X1),X2),join(meet(X2,meet(X1,X2)),meet(meet(X1,X2),join(meet(X0,X1),meet(X2,meet(X1,X2))))))),
    inference(forward_demodulation,[],[f22104,f4]) ).

fof(f22172,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),join(meet(meet(X0,X1),X2),meet(meet(X1,X2),join(meet(X0,X1),meet(X2,meet(X1,X2)))))),
    inference(forward_demodulation,[],[f22143,f17561]) ).

fof(f22197,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X1,X2),meet(join(X2,meet(X1,X2)),meet(X0,X1))))),
    inference(forward_demodulation,[],[f22172,f49]) ).

fof(f22218,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X1,X2),meet(X1,meet(join(X2,meet(X1,X2)),X0))))),
    inference(forward_demodulation,[],[f22197,f59]) ).

fof(f22233,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X1,X2),meet(X1,meet(meet(X2,join(X2,X1)),X0))))),
    inference(forward_demodulation,[],[f22218,f1135]) ).

fof(f22245,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),join(meet(X1,X2),meet(X1,meet(X2,meet(join(X2,X1),X0)))))),
    inference(forward_demodulation,[],[f22233,f5]) ).

fof(f22256,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(join(meet(X0,X1),X2),meet(X1,meet(X2,join(X2,meet(meet(join(X2,X1),X0),X1)))))),
    inference(forward_demodulation,[],[f22245,f8569]) ).

fof(f22265,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(meet(X2,join(X2,meet(meet(join(X2,X1),X0),X1))),join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f22256,f59]) ).

fof(f22273,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(join(meet(X0,X1),X2),meet(X2,join(X2,meet(meet(join(X2,X1),X0),X1)))))),
    inference(forward_demodulation,[],[f22265,f3]) ).

fof(f22279,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(X2,meet(join(X2,meet(meet(join(X2,X1),X0),X1)),join(meet(X0,X1),X2))))),
    inference(forward_demodulation,[],[f22273,f59]) ).

fof(f22283,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(X2,meet(join(meet(X0,X1),X2),join(X2,meet(meet(join(X2,X1),X0),X1)))))),
    inference(forward_demodulation,[],[f22279,f3]) ).

fof(f22287,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(X2,meet(join(meet(X0,X1),X2),join(X2,meet(X1,meet(join(X2,X1),X0))))))),
    inference(forward_demodulation,[],[f22283,f3]) ).

fof(f22290,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,meet(join(X2,X1),X0)))))),
    inference(forward_demodulation,[],[f22287,f14328]) ).

fof(f22291,plain,
    ! [X2,X0,X1] : join(join(meet(X2,meet(X1,X2)),meet(X0,X1)),meet(X0,meet(X1,X2))) = join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))),
    inference(forward_demodulation,[],[f22290,f5622]) ).

fof(f22292,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))) = join(meet(X0,meet(X1,X2)),join(meet(X2,meet(X1,X2)),meet(X0,X1))),
    inference(forward_demodulation,[],[f22291,f4]) ).

fof(f22293,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))) = join(meet(X0,X1),join(meet(X0,meet(X1,X2)),meet(X2,meet(X1,X2)))),
    inference(forward_demodulation,[],[f22292,f143]) ).

fof(f22294,plain,
    ! [X2,X0,X1] : join(meet(X2,meet(X1,X2)),meet(X0,X1)) = join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))),
    inference(forward_demodulation,[],[f22293,f4566]) ).

fof(f22295,plain,
    ! [X2,X0,X1] : join(meet(X1,X2),meet(X0,X1)) = join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))),
    inference(forward_demodulation,[],[f22294,f479]) ).

fof(f22785,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2)))))) = meet(join(X0,meet(X0,X1)),join(X2,meet(join(meet(X0,X1),X0),join(meet(X0,X1),join(meet(X0,X1),X2))))),
    inference(superposition,[],[f4084,f2]) ).

fof(f23213,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2)))))) = meet(join(X0,meet(X0,X1)),join(X2,meet(join(meet(X0,X1),X0),join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f22785,f388]) ).

fof(f23412,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2)))))) = meet(join(X0,meet(X0,X1)),join(X2,meet(join(X0,meet(X0,X1)),join(meet(X0,X1),X2)))),
    inference(forward_demodulation,[],[f23213,f4]) ).

fof(f23579,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2)))))) = meet(join(X0,meet(X0,X1)),join(meet(X0,X1),X2)),
    inference(forward_demodulation,[],[f23412,f15249]) ).

fof(f23739,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X1),join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2)))))),
    inference(forward_demodulation,[],[f23579,f1077]) ).

fof(f23874,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,join(meet(X0,X1),join(X0,meet(meet(X0,X1),X2))))),
    inference(forward_demodulation,[],[f23739,f388]) ).

fof(f23996,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,join(meet(X0,X1),X0))),
    inference(forward_demodulation,[],[f23874,f2486]) ).

fof(f24090,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,join(X0,meet(X0,X1)))),
    inference(forward_demodulation,[],[f23996,f4]) ).

fof(f24171,plain,
    ! [X2,X0,X1] : meet(meet(X0,join(X0,X1)),join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f24090,f1077]) ).

fof(f24244,plain,
    ! [X2,X0,X1] : meet(X0,meet(join(X0,X1),join(meet(X0,X1),X2))) = join(meet(X0,X1),meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f24171,f5]) ).

fof(f24307,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = join(meet(X0,X1),meet(X2,meet(X0,join(X0,X1)))),
    inference(forward_demodulation,[],[f24244,f2112]) ).

fof(f24353,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(join(X0,X1),meet(X1,join(meet(X1,X2),X0))),
    inference(backward_demodulation,[],[f12135,f24307]) ).

fof(f24387,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(meet(X1,X2),X0),join(X0,X1))),
    inference(forward_demodulation,[],[f24353,f59]) ).

fof(f24410,plain,
    ! [X2,X0,X1] : join(meet(X2,X1),meet(X0,X1)) = meet(X1,meet(join(X0,X1),join(meet(X1,X2),X0))),
    inference(forward_demodulation,[],[f24387,f3]) ).

fof(f24427,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = join(meet(X2,X1),meet(X0,X1)),
    inference(forward_demodulation,[],[f24410,f51]) ).

fof(f24450,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,join(meet(X1,X0),X2))),
    inference(backward_demodulation,[],[f4731,f24427]) ).

fof(f24472,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(meet(X0,join(meet(X0,X1),X2)),join(meet(X2,X0),meet(X0,X1))),
    inference(backward_demodulation,[],[f12376,f24427]) ).

fof(f24475,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X0),X2)) = join(meet(X1,X0),meet(X2,X1)),
    inference(backward_demodulation,[],[f12638,f24427]) ).

fof(f24524,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = join(meet(X2,X1),meet(X1,meet(X0,join(X1,X2)))),
    inference(backward_demodulation,[],[f21828,f24427]) ).

fof(f24553,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X2,X0),meet(X3,join(X1,X2)))) = join(X0,join(meet(X2,X0),meet(join(X1,X2),join(meet(join(X1,X2),X3),X0)))),
    inference(backward_demodulation,[],[f22120,f24427]) ).

fof(f24593,plain,
    ! [X2,X3,X0,X1] : join(X0,join(meet(X2,X0),meet(X3,join(X1,X2)))) = join(X0,meet(join(X1,X2),join(meet(join(X1,X2),X3),X0))),
    inference(forward_demodulation,[],[f24553,f15220]) ).

fof(f24674,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = join(meet(X0,X1),meet(X1,meet(X2,join(X2,meet(X1,X0))))),
    inference(backward_demodulation,[],[f22295,f24475]) ).

fof(f24699,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,meet(join(meet(X0,X1),X2),join(meet(X2,X0),meet(X0,X1)))),
    inference(forward_demodulation,[],[f24472,f5]) ).

fof(f24712,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(X0,X1))) = join(meet(X0,X1),meet(X0,X2)),
    inference(backward_demodulation,[],[f18594,f24450]) ).

fof(f24734,plain,
    ! [X2,X3,X0,X1] : join(X0,meet(X3,join(X1,X2))) = join(X0,join(meet(X2,X0),meet(X3,join(X1,X2)))),
    inference(forward_demodulation,[],[f24593,f24450]) ).

fof(f24803,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X1),X2)) = meet(X0,join(meet(X2,X0),meet(X0,X1))),
    inference(forward_demodulation,[],[f24699,f51]) ).

fof(f24806,plain,
    ~ sP0(meet(a,join(c,meet(a,b)))),
    inference(backward_demodulation,[],[f13,f24712]) ).

fof(f24810,plain,
    ! [X2,X0,X1] : join(X1,meet(X0,X2)) = join(X1,meet(X0,join(X2,meet(X0,X1)))),
    inference(backward_demodulation,[],[f3248,f24712]) ).

fof(f24815,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X0,join(X2,meet(X0,X1)))),
    inference(backward_demodulation,[],[f4596,f24712]) ).

fof(f25196,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(X0,meet(X2,join(X0,X1))),
    inference(backward_demodulation,[],[f15299,f24734]) ).

fof(f25236,plain,
    ! [X2,X0,X1] : meet(X0,join(meet(X0,X2),X1)) = join(meet(X1,X0),meet(X0,X2)),
    inference(backward_demodulation,[],[f2488,f24803]) ).

fof(f25494,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),X1) = join(X1,meet(X2,meet(X0,join(X0,meet(X2,X1))))),
    inference(backward_demodulation,[],[f17260,f24815]) ).

fof(f25534,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(X2,join(X1,meet(X0,X2)))) = meet(join(X1,X0),meet(join(X2,X0),join(X2,X1))),
    inference(backward_demodulation,[],[f6741,f25196]) ).

fof(f25538,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(join(X2,X1),join(X2,X0))) = meet(join(X0,X1),meet(join(meet(X1,X0),X2),meet(join(X2,X1),join(X2,X0)))),
    inference(backward_demodulation,[],[f10437,f25196]) ).

fof(f25720,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,join(meet(X1,meet(X0,join(X1,X2))),X2)),
    inference(backward_demodulation,[],[f24524,f25236]) ).

fof(f25723,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,join(meet(X1,meet(X2,join(X2,meet(X1,X0)))),X0)),
    inference(backward_demodulation,[],[f24674,f25236]) ).

fof(f26002,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(join(X2,X1),join(X2,X0))) = meet(join(X0,X1),meet(join(X2,X0),meet(join(meet(X1,X0),X2),join(X2,X1)))),
    inference(forward_demodulation,[],[f25538,f59]) ).

fof(f26004,plain,
    ! [X2,X0,X1] : meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))) = meet(join(X1,X0),meet(join(X2,X0),join(X2,X1))),
    inference(backward_demodulation,[],[f162,f25534]) ).

fof(f26131,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,join(X0,meet(X1,meet(X2,join(X2,meet(X1,X0)))))),
    inference(forward_demodulation,[],[f25723,f11828]) ).

fof(f26133,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X1,X2),X0)) = meet(X1,join(X2,meet(X1,meet(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f25720,f11828]) ).

fof(f26451,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),meet(join(X2,X1),join(X2,X0))) = meet(join(X0,X1),meet(join(X2,X1),join(meet(X1,X0),X2))),
    inference(forward_demodulation,[],[f26002,f8225]) ).

fof(f26789,plain,
    ! [X2,X0,X1] : meet(X1,join(meet(X2,X1),X0)) = meet(X1,join(meet(X1,X2),X0)),
    inference(forward_demodulation,[],[f26131,f25494]) ).

fof(f26791,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(meet(X1,X2),X0)),
    inference(forward_demodulation,[],[f26133,f2549]) ).

fof(f27030,plain,
    ! [X2,X0,X1] : meet(join(X0,X1),join(meet(X1,X0),X2)) = meet(join(X0,X1),meet(join(X2,X1),join(X2,X0))),
    inference(forward_demodulation,[],[f26451,f51]) ).

fof(f27210,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,meet(X1,X0))) = meet(X1,join(meet(X2,X1),X0)),
    inference(backward_demodulation,[],[f26789,f26791]) ).

fof(f27520,plain,
    ! [X2,X0,X1] : meet(join(X1,X0),join(X2,meet(join(X0,X2),X1))) = meet(join(X1,X0),join(meet(X0,X1),X2)),
    inference(backward_demodulation,[],[f26004,f27030]) ).

fof(f27932,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,meet(X0,X2))) = meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2))),
    inference(backward_demodulation,[],[f2113,f27210]) ).

fof(f32851,plain,
    ! [X2,X0,X1] : join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))) = join(X2,meet(meet(join(X1,X2),X0),meet(join(X0,X1),join(meet(X1,X0),X2)))),
    inference(superposition,[],[f5550,f27520]) ).

fof(f32893,plain,
    ! [X2,X0,X1] : join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))) = join(X2,meet(join(X0,X1),meet(join(meet(X1,X0),X2),meet(join(X1,X2),X0)))),
    inference(forward_demodulation,[],[f32851,f59]) ).

fof(f32993,plain,
    ! [X2,X0,X1] : join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))) = join(X2,meet(X0,meet(join(X0,X1),meet(join(meet(X1,X0),X2),join(X1,X2))))),
    inference(forward_demodulation,[],[f32893,f3746]) ).

fof(f33096,plain,
    ! [X2,X0,X1] : join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))) = join(X2,meet(X0,meet(join(X0,X1),meet(join(X1,X2),join(meet(X1,X0),X2))))),
    inference(forward_demodulation,[],[f32993,f3]) ).

fof(f33181,plain,
    ! [X2,X0,X1] : join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))) = join(X2,meet(X0,meet(join(X0,X1),join(meet(X1,X0),X2)))),
    inference(forward_demodulation,[],[f33096,f2395]) ).

fof(f33248,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,join(X1,meet(X0,X2)))) = join(X2,meet(meet(join(X1,X2),X0),join(X0,X1))),
    inference(forward_demodulation,[],[f33181,f27932]) ).

fof(f33294,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,join(X1,meet(X0,X2)))) = join(X2,meet(join(X0,X1),meet(join(X1,X2),X0))),
    inference(forward_demodulation,[],[f33248,f3]) ).

fof(f33334,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,join(X1,meet(X0,X2)))) = join(X2,meet(X0,meet(join(X0,X1),join(X1,X2)))),
    inference(forward_demodulation,[],[f33294,f59]) ).

fof(f33370,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,join(X1,X2))) = join(X2,meet(X0,join(X1,meet(X0,X2)))),
    inference(forward_demodulation,[],[f33334,f2063]) ).

fof(f33398,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X0,join(X1,X2))),
    inference(forward_demodulation,[],[f33370,f24810]) ).

fof(f33428,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(X0,join(X2,meet(X0,X1))),
    inference(backward_demodulation,[],[f15249,f33398]) ).

fof(f34040,plain,
    ~ sP0(meet(a,join(b,c))),
    inference(backward_demodulation,[],[f24806,f33428]) ).

fof(f34085,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f34040,f14]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.38  % Computer : n002.cluster.edu
% 0.09/0.38  % Model    : x86_64 x86_64
% 0.09/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38  % Memory   : 8046.5625MB
% 0.09/0.38  % OS       : Linux 6.8.0-71-generic
% 0.09/0.38  % CPULimit : 300
% 0.09/0.38  % WCLimit  : 300
% 0.09/0.38  % DateTime : Sun Sep 27 13:59:36 UTC 2026
% 0.09/0.38  % CPUTime  : 
% 0.09/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.41  Running first-order theorem proving
% 0.09/0.41  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.85/4.63  % (3543625)Detected a unit-equality problem, will run specialized UEQ schedule.
% 23.85/4.63  % (3543634)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=319838671:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 23.85/4.63  % (3543633)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3410964486:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 23.85/4.63  % (3543631)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1511141453:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 23.85/4.63  % (3543636)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=395618201:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 23.85/4.63  % (3543632)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=607521579:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 23.85/4.63  % (3543630)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1085815098:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 23.85/4.63  % (3543635)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=967844509:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 23.85/4.63  % (3543634)Instruction limit reached! 
% 23.85/4.63  % (3543634)------------------------------
% 23.85/4.63  % (3543634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543634)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543634)Termination reason: Instruction limit
% 23.85/4.63  % (3543634)Termination phase: Saturation
% 23.85/4.63  % (3543634)Time elapsed: 0.049 s
% 23.85/4.63  % (3543634)Peak memory usage: 89 MB
% 23.85/4.63  % (3543634)Instructions burned: 183 (million)
% 23.85/4.63  % (3543633)Instruction limit reached! 
% 23.85/4.63  % (3543633)------------------------------
% 23.85/4.63  % (3543633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543633)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543633)Termination reason: Instruction limit
% 23.85/4.63  % (3543633)Termination phase: Saturation
% 23.85/4.63  % (3543633)Time elapsed: 0.084 s
% 23.85/4.63  % (3543633)Peak memory usage: 88 MB
% 23.85/4.63  % (3543633)Instructions burned: 136 (million)
% 23.85/4.63  % (3543644)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1768675589:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2998 on theBenchmark for (2998ds/2051Mi)
% 23.85/4.63  % (3543635)Instruction limit reached! 
% 23.85/4.63  % (3543635)------------------------------
% 23.85/4.63  % (3543635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543635)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543635)Termination reason: Instruction limit
% 23.85/4.63  % (3543635)Termination phase: Saturation
% 23.85/4.63  % (3543635)Time elapsed: 0.165 s
% 23.85/4.63  % (3543635)Peak memory usage: 89 MB
% 23.85/4.63  % (3543635)Instructions burned: 258 (million)
% 23.85/4.63  % (3543645)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3262835743:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 23.85/4.63  % (3543647)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=206269811:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 23.85/4.63  % (3543647)Instruction limit reached! 
% 23.85/4.63  % (3543647)------------------------------
% 23.85/4.63  % (3543647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543647)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543647)Termination reason: Instruction limit
% 23.85/4.63  % (3543647)Termination phase: Saturation
% 23.85/4.63  % (3543647)Time elapsed: 0.117 s
% 23.85/4.63  % (3543647)Peak memory usage: 90 MB
% 23.85/4.63  % (3543647)Instructions burned: 217 (million)
% 23.85/4.63  % (3543636)Instruction limit reached! 
% 23.85/4.63  % (3543636)------------------------------
% 23.85/4.63  % (3543636)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543636)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543636)Termination reason: Instruction limit
% 23.85/4.63  % (3543636)Termination phase: Saturation
% 23.85/4.63  % (3543636)Time elapsed: 0.598 s
% 23.85/4.63  % (3543636)Peak memory usage: 96 MB
% 23.85/4.63  % (3543636)Instructions burned: 1189 (million)
% 23.85/4.63  % (3543650)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=1276184276:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 23.85/4.63  % (3543651)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=4070798383:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 23.85/4.63  % (3543650)Instruction limit reached! 
% 23.85/4.63  % (3543650)------------------------------
% 23.85/4.63  % (3543650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543650)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543650)Termination reason: Instruction limit
% 23.85/4.63  % (3543650)Termination phase: Saturation
% 23.85/4.63  % (3543650)Time elapsed: 0.189 s
% 23.85/4.63  % (3543650)Peak memory usage: 92 MB
% 23.85/4.63  % (3543650)Instructions burned: 317 (million)
% 23.85/4.63  % (3543644)Instruction limit reached! 
% 23.85/4.63  % (3543644)------------------------------
% 23.85/4.63  % (3543644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543644)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543644)Termination reason: Instruction limit
% 23.85/4.63  % (3543644)Termination phase: Saturation
% 23.85/4.63  % (3543644)Time elapsed: 0.728 s
% 23.85/4.63  % (3543644)Peak memory usage: 141 MB
% 23.85/4.63  % (3543644)Instructions burned: 2052 (million)
% 23.85/4.63  % (3543654)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3069475568:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 23.85/4.63  % (3543655)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4076729821:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2989 on theBenchmark for (2989ds/14534Mi)
% 23.85/4.63  % (3543654)Instruction limit reached! 
% 23.85/4.63  % (3543654)------------------------------
% 23.85/4.63  % (3543654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543654)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543654)Termination reason: Instruction limit
% 23.85/4.63  % (3543654)Termination phase: Saturation
% 23.85/4.63  % (3543654)Time elapsed: 1.804 s
% 23.85/4.63  % (3543654)Peak memory usage: 124 MB
% 23.85/4.63  % (3543654)Instructions burned: 2837 (million)
% 23.85/4.63  % (3543658)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=974940555:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/11832Mi)
% 23.85/4.63  % (3543645)Instruction limit reached! 
% 23.85/4.63  % (3543645)------------------------------
% 23.85/4.63  % (3543645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.85/4.63  % (3543645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.85/4.63  % (3543645)CaDiCaL version: 2.1.3
% 23.85/4.63  % (3543645)Termination reason: Instruction limit
% 23.85/4.63  % (3543645)Termination phase: Saturation
% 23.85/4.63  % (3543645)Time elapsed: 2.942 s
% 23.85/4.63  % (3543645)Peak memory usage: 161 MB
% 23.85/4.63  % (3543645)Instructions burned: 4950 (million)
% 23.85/4.63  % (3543660)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:drc=off:fde=unused:sp=const_min:spb=goal:fd=preordered:random_seed=1577358768:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 23.85/4.63  % (3543655)First to succeed.
% 23.85/4.63  % (3543655)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3543625"
% 23.85/4.63  % (3543655)Refutation found. Thanks to Tanya!
% 23.85/4.63  % SZS status Unsatisfiable for theBenchmark
% 23.85/4.63  % SZS output start Proof for theBenchmark
% See solution above
% 27.37/4.82  % (3543655)------------------------------
% 27.37/4.82  % (3543655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.37/4.82  % (3543655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.37/4.82  % (3543655)CaDiCaL version: 2.1.3
% 27.37/4.82  % (3543655)Termination reason: Refutation
% 27.37/4.82  % (3543655)Time elapsed: 2.439 s
% 27.37/4.82  % (3543655)Peak memory usage: 179 MB
% 27.37/4.82  % (3543655)Instructions burned: 7457 (million)
% 27.37/4.82  % (3543655)------------------------------
% 27.37/4.82  % (3543655)------------------------------
% 27.37/4.82  % (3543625)Success in time 3.78 s
% 27.37/4.82  % Vampire exiting
%------------------------------------------------------------------------------