Vampire---5.0.1.UNS-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : LAT401-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n017.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:47:37 AM UTC 2026

% Result   : Unsatisfiable 181.78s 40.54s
% Output   : Refutation 282.16s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   64
%            Number of leaves      :   23
% Syntax   : Number of formulae    :  721 ( 721 unt;   9 def)
%            Number of atoms       :  721 ( 720 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :    3 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    6 (   3 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :   18 (  18 usr;  13 con; 0-3 aty)
%            Number of variables   : 1161 (1161   !;   0   ?)

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

fof(f2,axiom,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).

fof(f3,axiom,
    ! [X0,X1] : join(X0,X1) = join(X1,X0),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_001) ).

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

fof(f5,axiom,
    ! [X0,X1] : join(X0,meet(X0,X1)) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption) ).

fof(f6,axiom,
    ! [X0,X1] : meet(X0,join(X0,X1)) = X0,
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption_003) ).

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

fof(f8,negated_conjecture,
    ! [X2,X0,X1] : upjo(X0,X1,X2) = meet(join(X0,X1),join(X0,X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_upjo) ).

fof(f9,negated_conjecture,
    ! [X2,X0,X1] : lojo(X0,X1,X2) = join(X0,meet(X1,X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_lojo) ).

fof(f10,negated_conjecture,
    ! [X2,X0,X1] : join(upme(meet(a,X0),X1,X2),meet(X1,X2)) = meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',upme_property_1) ).

fof(f11,negated_conjecture,
    ! [X2,X0,X1] : upme(X0,X1,X2) = join(upme(X0,X1,meet(a,X2)),upme(X0,X2,meet(a,X1))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',upme_property_2) ).

fof(f12,negated_conjecture,
    upme(a,x2,y2) = upme(a,x2,z2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).

fof(f13,negated_conjecture,
    upme(a,x2,y2) = upme(a,y2,z2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture_1) ).

fof(f14,negated_conjecture,
    upjo(x2,y2,z2) != lojo(x2,y2,z2),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture_2) ).

fof(f15,plain,
    ! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(meet(a,X0),join(X1,X2)),meet(X1,X2)),
    inference(definition_unfolding,[],[f10,f7]) ).

fof(f16,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X0,join(X1,meet(a,X2))),meet(X0,join(X2,meet(a,X1)))),
    inference(definition_unfolding,[],[f11,f7,f7,f7]) ).

fof(f17,plain,
    meet(a,join(x2,y2)) = meet(a,join(x2,z2)),
    inference(definition_unfolding,[],[f12,f7,f7]) ).

fof(f18,plain,
    meet(a,join(x2,y2)) = meet(a,join(y2,z2)),
    inference(definition_unfolding,[],[f13,f7,f7]) ).

fof(f19,plain,
    meet(join(x2,y2),join(x2,z2)) != join(x2,meet(y2,z2)),
    inference(definition_unfolding,[],[f14,f8,f9]) ).

fof(f20,definition,
    sF0 = join(x2,y2),
    introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).

fof(f21,plain,
    join(x2,y2) = sF0,
    inference(reorient_equations,[],[f20]) ).

fof(f22,definition,
    sF1 = meet(a,sF0),
    introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).

fof(f23,plain,
    meet(a,sF0) = sF1,
    inference(reorient_equations,[],[f22]) ).

fof(f24,definition,
    sF2 = join(x2,z2),
    introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).

fof(f25,plain,
    join(x2,z2) = sF2,
    inference(reorient_equations,[],[f24]) ).

fof(f26,definition,
    sF3 = meet(a,sF2),
    introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).

fof(f27,plain,
    meet(a,sF2) = sF3,
    inference(reorient_equations,[],[f26]) ).

fof(f28,plain,
    sF1 = sF3,
    inference(definition_folding,[],[f17,f27,f25,f23,f21]) ).

fof(f29,definition,
    sF4 = join(y2,z2),
    introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).

fof(f30,plain,
    join(y2,z2) = sF4,
    inference(reorient_equations,[],[f29]) ).

fof(f31,definition,
    sF5 = meet(a,sF4),
    introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).

fof(f32,plain,
    meet(a,sF4) = sF5,
    inference(reorient_equations,[],[f31]) ).

fof(f33,plain,
    sF1 = sF5,
    inference(definition_folding,[],[f18,f32,f30,f23,f21]) ).

fof(f34,definition,
    sF6 = meet(sF0,sF2),
    introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).

fof(f35,plain,
    meet(sF0,sF2) = sF6,
    inference(reorient_equations,[],[f34]) ).

fof(f36,definition,
    sF7 = meet(y2,z2),
    introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).

fof(f37,plain,
    meet(y2,z2) = sF7,
    inference(reorient_equations,[],[f36]) ).

fof(f38,definition,
    sF8 = join(x2,sF7),
    introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).

fof(f39,plain,
    join(x2,sF7) = sF8,
    inference(reorient_equations,[],[f38]) ).

fof(f40,plain,
    sF6 != sF8,
    inference(definition_folding,[],[f19,f39,f37,f35,f25,f21]) ).

fof(f41,plain,
    ! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(X1,X2),meet(meet(a,X0),join(X1,X2))),
    inference(backward_demodulation,[],[f15,f3]) ).

fof(f42,plain,
    sF1 = meet(sF0,a),
    inference(forward_demodulation,[],[f23,f1]) ).

fof(f43,plain,
    sF1 = meet(a,sF2),
    inference(forward_demodulation,[],[f27,f28]) ).

fof(f44,plain,
    sF1 = meet(a,sF4),
    inference(forward_demodulation,[],[f32,f33]) ).

fof(f45,plain,
    sF8 = join(sF7,x2),
    inference(forward_demodulation,[],[f39,f3]) ).

fof(f46,plain,
    ! [X2,X0,X1] : meet(join(meet(meet(a,X0),X1),X2),join(meet(meet(a,X0),X2),X1)) = join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f41,f2]) ).

fof(f47,plain,
    sF1 = meet(sF2,a),
    inference(forward_demodulation,[],[f43,f1]) ).

fof(f48,plain,
    sF1 = meet(sF4,a),
    inference(forward_demodulation,[],[f44,f1]) ).

fof(f49,plain,
    ! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(meet(meet(a,X0),X1),X2),join(meet(a,meet(X0,X2)),X1)),
    inference(forward_demodulation,[],[f46,f2]) ).

fof(f50,plain,
    ! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X0,X2)),X1)),
    inference(forward_demodulation,[],[f49,f2]) ).

fof(f68,plain,
    ! [X0] : join(meet(X0,sF2),meet(a,meet(sF0,join(X0,sF2)))) = meet(join(meet(a,meet(sF0,X0)),sF2),join(meet(a,sF6),X0)),
    inference(superposition,[],[f50,f35]) ).

fof(f69,plain,
    ! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(meet(a,meet(sF0,X0)),sF2)),
    inference(superposition,[],[f50,f35]) ).

fof(f70,plain,
    ! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))),
    inference(forward_demodulation,[],[f69,f3]) ).

fof(f71,plain,
    ! [X0] : join(meet(X0,sF2),meet(a,meet(sF0,join(X0,sF2)))) = meet(join(meet(a,sF6),X0),join(meet(a,meet(sF0,X0)),sF2)),
    inference(forward_demodulation,[],[f68,f1]) ).

fof(f72,plain,
    ! [X0] : join(meet(X0,sF2),meet(a,meet(sF0,join(X0,sF2)))) = meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))),
    inference(forward_demodulation,[],[f71,f3]) ).

fof(f74,plain,
    sF0 = join(sF0,sF1),
    inference(superposition,[],[f5,f42]) ).

fof(f97,plain,
    ! [X0] : meet(X0,X0) = X0,
    inference(superposition,[],[f6,f5]) ).

fof(f98,plain,
    ! [X0] : join(X0,X0) = X0,
    inference(superposition,[],[f5,f6]) ).

fof(f99,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,meet(X0,X1)),join(X0,X2)),join(meet(a,X0),X1)),
    inference(superposition,[],[f50,f6]) ).

fof(f100,plain,
    ! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,meet(X0,join(join(X0,X1),X2)))) = meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))),
    inference(superposition,[],[f50,f6]) ).

fof(f101,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(join(X0,X1),X2),meet(a,meet(X0,join(X0,join(X1,X2))))),
    inference(forward_demodulation,[],[f100,f4]) ).

fof(f102,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),join(X0,X2))),
    inference(forward_demodulation,[],[f99,f1]) ).

fof(f103,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(join(X0,X1),X2),meet(a,X0)),
    inference(forward_demodulation,[],[f101,f6]) ).

fof(f104,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X0,X1))) = join(meet(a,X0),meet(join(X0,X1),X2)),
    inference(forward_demodulation,[],[f103,f3]) ).

fof(f105,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X0,X2)),meet(a,meet(X0,join(X1,join(X0,X2))))) = join(meet(a,X0),meet(join(X0,X2),X1)),
    inference(backward_demodulation,[],[f102,f104]) ).

fof(f115,plain,
    ! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,join(X1,meet(a,X0))),X0),
    inference(superposition,[],[f16,f6]) ).

fof(f118,plain,
    ! [X0,X1] : join(X0,meet(X0,join(X1,meet(a,X0)))) = meet(X0,join(X1,X0)),
    inference(forward_demodulation,[],[f115,f3]) ).

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

fof(f145,plain,
    sF2 = join(sF2,sF1),
    inference(superposition,[],[f5,f47]) ).

fof(f155,plain,
    x2 = meet(x2,sF2),
    inference(superposition,[],[f6,f25]) ).

fof(f156,plain,
    x2 = meet(sF2,x2),
    inference(forward_demodulation,[],[f155,f1]) ).

fof(f157,plain,
    y2 = join(y2,sF7),
    inference(superposition,[],[f5,f37]) ).

fof(f162,plain,
    y2 = join(sF7,y2),
    inference(forward_demodulation,[],[f157,f3]) ).

fof(f166,plain,
    sF4 = join(sF4,sF1),
    inference(superposition,[],[f5,f48]) ).

fof(f167,plain,
    ! [X0] : join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))) = meet(join(meet(a,meet(sF4,X0)),a),join(meet(a,sF1),X0)),
    inference(superposition,[],[f50,f48]) ).

fof(f170,plain,
    ! [X0] : join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))) = meet(join(meet(a,sF1),X0),join(meet(a,meet(sF4,X0)),a)),
    inference(forward_demodulation,[],[f167,f1]) ).

fof(f172,plain,
    ! [X0] : join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))) = meet(join(meet(a,sF1),X0),join(a,meet(a,meet(sF4,X0)))),
    inference(forward_demodulation,[],[f170,f3]) ).

fof(f174,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))),
    inference(forward_demodulation,[],[f172,f5]) ).

fof(f175,plain,
    ! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))),
    inference(forward_demodulation,[],[f174,f1]) ).

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

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

fof(f189,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),meet(a,meet(X1,join(X0,X2)))) = meet(join(meet(a,meet(X1,X0)),X2),join(X0,meet(a,meet(X1,X2)))),
    inference(superposition,[],[f50,f3]) ).

fof(f190,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),meet(a,meet(X1,join(X2,X0)))) = meet(join(X0,meet(a,meet(X1,X2))),join(meet(a,meet(X1,X0)),X2)),
    inference(superposition,[],[f50,f3]) ).

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

fof(f192,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),meet(a,meet(X1,join(X0,X2)))) = meet(join(X0,meet(a,meet(X1,X2))),join(meet(a,meet(X1,X0)),X2)),
    inference(forward_demodulation,[],[f189,f1]) ).

fof(f193,plain,
    ! [X2,X0,X1] : meet(X2,join(X1,X0)) = join(meet(X2,join(X0,meet(a,X1))),meet(X2,join(meet(a,X0),X1))),
    inference(forward_demodulation,[],[f187,f3]) ).

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

fof(f200,plain,
    y2 = meet(y2,sF0),
    inference(superposition,[],[f128,f21]) ).

fof(f201,plain,
    z2 = meet(z2,sF2),
    inference(superposition,[],[f128,f25]) ).

fof(f207,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,meet(X0,X1)),join(X2,X0)),join(meet(a,X0),X1)),
    inference(superposition,[],[f50,f128]) ).

fof(f208,plain,
    ! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(join(X1,X0),X2)))) = meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X1,X0))),
    inference(superposition,[],[f50,f128]) ).

fof(f213,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(meet(a,meet(X0,X2)),join(X1,X0))) = join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))),
    inference(forward_demodulation,[],[f208,f4]) ).

fof(f214,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),join(X2,X0))),
    inference(forward_demodulation,[],[f207,f1]) ).

fof(f218,plain,
    z2 = meet(sF2,z2),
    inference(forward_demodulation,[],[f201,f1]) ).

fof(f219,plain,
    y2 = meet(sF0,y2),
    inference(forward_demodulation,[],[f200,f1]) ).

fof(f221,plain,
    ! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
    inference(forward_demodulation,[],[f196,f2]) ).

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

fof(f241,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),meet(a,meet(X1,join(X2,X0)))) = meet(join(meet(a,meet(X1,X2)),X0),join(meet(a,meet(X0,X1)),X2)),
    inference(superposition,[],[f50,f1]) ).

fof(f242,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),meet(a,meet(X1,join(X0,X2)))) = meet(join(meet(a,meet(X0,X1)),X2),join(meet(a,meet(X1,X2)),X0)),
    inference(superposition,[],[f50,f1]) ).

fof(f243,plain,
    ! [X2,X0,X1] : meet(X2,join(X1,X0)) = join(meet(X2,join(X1,meet(a,X0))),meet(join(X0,meet(a,X1)),X2)),
    inference(superposition,[],[f16,f1]) ).

fof(f244,plain,
    ! [X2,X0,X1] : meet(X2,join(X0,X1)) = join(meet(join(X0,meet(a,X1)),X2),meet(X2,join(X1,meet(a,X0)))),
    inference(superposition,[],[f16,f1]) ).

fof(f246,plain,
    ! [X2,X0,X1] : meet(X1,join(X0,X2)) = join(meet(X1,join(X0,meet(a,X2))),meet(X1,join(X2,meet(X0,a)))),
    inference(superposition,[],[f16,f1]) ).

fof(f247,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,meet(X0,a))),meet(X1,join(X0,meet(a,X2)))),
    inference(superposition,[],[f16,f1]) ).

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

fof(f253,plain,
    z2 = join(z2,sF7),
    inference(superposition,[],[f240,f37]) ).

fof(f257,plain,
    a = join(a,sF1),
    inference(superposition,[],[f240,f48]) ).

fof(f269,plain,
    z2 = join(sF7,z2),
    inference(forward_demodulation,[],[f253,f3]) ).

fof(f272,plain,
    ! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
    inference(forward_demodulation,[],[f248,f4]) ).

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

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

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

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

fof(f292,plain,
    ! [X0] : join(sF7,join(x2,X0)) = join(sF8,X0),
    inference(superposition,[],[f4,f45]) ).

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

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

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

fof(f305,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))),
    inference(backward_demodulation,[],[f214,f303]) ).

fof(f306,plain,
    ! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))) = meet(join(meet(a,X0),X2),join(X0,join(meet(a,meet(X0,X2)),X1))),
    inference(backward_demodulation,[],[f213,f303]) ).

fof(f312,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))) = join(meet(X1,join(X2,X0)),meet(a,X0)),
    inference(forward_demodulation,[],[f305,f301]) ).

fof(f314,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X0,X1)),X2))) = join(meet(a,X0),meet(X1,join(X2,X0))),
    inference(forward_demodulation,[],[f312,f3]) ).

fof(f315,plain,
    ! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,meet(X0,join(X1,join(X0,X2))))) = join(meet(a,X0),meet(X2,join(X1,X0))),
    inference(backward_demodulation,[],[f306,f314]) ).

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

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

fof(f319,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
    inference(superposition,[],[f2,f1]) ).

fof(f322,plain,
    ! [X0] : meet(y2,meet(z2,X0)) = meet(sF7,X0),
    inference(superposition,[],[f2,f37]) ).

fof(f323,plain,
    ! [X0] : meet(sF0,meet(a,X0)) = meet(sF1,X0),
    inference(superposition,[],[f2,f42]) ).

fof(f324,plain,
    ! [X0] : meet(sF0,meet(sF2,X0)) = meet(sF6,X0),
    inference(superposition,[],[f2,f35]) ).

fof(f325,plain,
    ! [X0] : meet(sF1,X0) = meet(sF2,meet(a,X0)),
    inference(superposition,[],[f2,f47]) ).

fof(f326,plain,
    ! [X0] : meet(sF1,X0) = meet(sF4,meet(a,X0)),
    inference(superposition,[],[f2,f48]) ).

fof(f332,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
    inference(superposition,[],[f1,f2]) ).

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

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

fof(f341,plain,
    ! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = join(meet(X0,meet(X1,join(X2,meet(a,X3)))),meet(X0,meet(X1,join(X3,meet(a,X2))))),
    inference(forward_demodulation,[],[f339,f2]) ).

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

fof(f349,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(X0,sF2),meet(sF0,meet(join(X0,sF2),a))),
    inference(backward_demodulation,[],[f72,f332]) ).

fof(f350,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(sF2,X0),meet(sF0,meet(join(sF2,X0),a))),
    inference(backward_demodulation,[],[f70,f332]) ).

fof(f354,plain,
    ! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF4,meet(join(X0,a),a))),
    inference(backward_demodulation,[],[f175,f332]) ).

fof(f356,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,meet(X1,join(X2,meet(a,X3)))),meet(X0,meet(X1,join(X3,meet(a,X2))))) = meet(X0,meet(X1,join(X2,X3))),
    inference(forward_demodulation,[],[f341,f2]) ).

fof(f357,plain,
    ! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X3,X2)) = join(meet(X0,meet(X1,join(X2,meet(a,X3)))),meet(X0,meet(X1,join(X3,meet(a,X2))))),
    inference(forward_demodulation,[],[f342,f2]) ).

fof(f360,plain,
    ! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF4,meet(a,join(X0,a)))),
    inference(forward_demodulation,[],[f354,f1]) ).

fof(f364,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(sF2,X0),meet(sF0,meet(a,join(sF2,X0)))),
    inference(forward_demodulation,[],[f350,f1]) ).

fof(f365,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(X0,sF2),meet(sF0,meet(a,join(X0,sF2)))),
    inference(forward_demodulation,[],[f349,f1]) ).

fof(f369,plain,
    ! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X3,X2)) = meet(X0,meet(X1,join(X2,X3))),
    inference(forward_demodulation,[],[f357,f356]) ).

fof(f370,plain,
    ! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF1,join(X0,a))),
    inference(forward_demodulation,[],[f360,f326]) ).

fof(f374,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(sF2,X0),meet(sF1,join(sF2,X0))),
    inference(forward_demodulation,[],[f364,f323]) ).

fof(f375,plain,
    ! [X0] : meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(sF0,X0)))) = join(meet(X0,sF2),meet(sF1,join(X0,sF2))),
    inference(forward_demodulation,[],[f365,f323]) ).

fof(f378,plain,
    ! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
    inference(forward_demodulation,[],[f369,f2]) ).

fof(f379,plain,
    ! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF0,meet(X0,a)))),
    inference(forward_demodulation,[],[f374,f332]) ).

fof(f380,plain,
    ! [X0] : join(meet(X0,sF2),meet(sF1,join(X0,sF2))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF0,meet(X0,a)))),
    inference(forward_demodulation,[],[f375,f332]) ).

fof(f382,plain,
    ! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
    inference(superposition,[],[f283,f128]) ).

fof(f388,plain,
    ! [X0] : join(sF0,X0) = join(sF0,join(sF1,X0)),
    inference(superposition,[],[f283,f42]) ).

fof(f394,plain,
    ! [X2,X0,X1] : join(X0,meet(X0,X1)) = join(X0,meet(X2,meet(X0,X1))),
    inference(superposition,[],[f283,f240]) ).

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

fof(f400,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
    inference(superposition,[],[f128,f283]) ).

fof(f408,plain,
    ! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
    inference(forward_demodulation,[],[f400,f1]) ).

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

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

fof(f445,plain,
    ! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
    inference(superposition,[],[f316,f128]) ).

fof(f447,plain,
    ! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
    inference(superposition,[],[f316,f1]) ).

fof(f457,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(a,meet(join(a,X2),join(X1,X0)))) = meet(join(meet(a,meet(join(a,X2),X1)),X0),join(meet(a,X0),X1)),
    inference(superposition,[],[f50,f316]) ).

fof(f458,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(join(a,X2),join(X0,X1)))) = meet(join(meet(a,X0),X1),join(meet(a,meet(join(a,X2),X1)),X0)),
    inference(superposition,[],[f50,f316]) ).

fof(f462,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(join(a,X2),join(X0,X1)))) = meet(join(meet(a,X0),X1),join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f458,f316]) ).

fof(f463,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(a,meet(join(a,X2),join(X1,X0)))) = meet(join(meet(a,X0),X1),join(meet(a,meet(join(a,X2),X1)),X0)),
    inference(forward_demodulation,[],[f457,f1]) ).

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

fof(f481,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(meet(a,X1),X0)) = join(meet(X0,X1),meet(a,join(X0,X1))),
    inference(forward_demodulation,[],[f462,f316]) ).

fof(f482,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(a,meet(join(a,X2),join(X1,X0)))) = meet(join(meet(a,X0),X1),join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f463,f316]) ).

fof(f485,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(X2,join(X1,X0))) = join(meet(join(X1,X0),X2),meet(a,X0)),
    inference(backward_demodulation,[],[f315,f471]) ).

fof(f486,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X2),X1)) = join(meet(X1,join(X0,X2)),meet(a,X0)),
    inference(backward_demodulation,[],[f105,f471]) ).

fof(f490,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),meet(a,meet(join(a,X2),join(X1,X0)))) = join(meet(X0,X1),meet(a,join(X0,X1))),
    inference(forward_demodulation,[],[f482,f481]) ).

fof(f491,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X2),X1)) = join(meet(a,X0),meet(X1,join(X0,X2))),
    inference(forward_demodulation,[],[f486,f3]) ).

fof(f492,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(X2,join(X1,X0))) = join(meet(a,X0),meet(join(X1,X0),X2)),
    inference(forward_demodulation,[],[f485,f3]) ).

fof(f495,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,join(X0,X1))) = join(meet(X1,X0),meet(a,join(X1,X0))),
    inference(forward_demodulation,[],[f490,f316]) ).

fof(f518,plain,
    ! [X2,X3,X0,X1] : join(meet(a,X2),meet(join(X2,X3),meet(X0,X1))) = join(meet(a,X2),meet(X0,meet(X1,join(X2,X3)))),
    inference(superposition,[],[f491,f2]) ).

fof(f588,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,meet(X1,X0)),join(X2,X0)),join(meet(a,X0),X1)),
    inference(superposition,[],[f242,f128]) ).

fof(f650,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X1,X0)),join(X2,X0))),
    inference(forward_demodulation,[],[f588,f1]) ).

fof(f692,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,meet(X0,join(X1,join(X2,X0))))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
    inference(forward_demodulation,[],[f650,f303]) ).

fof(f727,plain,
    ! [X2,X0,X1] : join(meet(X1,join(X2,X0)),meet(a,X0)) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
    inference(forward_demodulation,[],[f692,f301]) ).

fof(f754,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X2,X0))) = meet(join(meet(a,X0),X1),join(X0,join(meet(a,meet(X1,X0)),X2))),
    inference(forward_demodulation,[],[f727,f3]) ).

fof(f847,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(meet(a,meet(X0,sF4)),a)),
    inference(superposition,[],[f241,f48]) ).

fof(f932,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(a,meet(a,meet(X0,sF4)))),
    inference(forward_demodulation,[],[f847,f3]) ).

fof(f979,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))),
    inference(forward_demodulation,[],[f932,f5]) ).

fof(f1017,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,sF4)),
    inference(forward_demodulation,[],[f979,f447]) ).

fof(f1045,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(sF4,a)),
    inference(forward_demodulation,[],[f1017,f1]) ).

fof(f1064,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(sF4,a),meet(a,X0)),
    inference(forward_demodulation,[],[f1045,f3]) ).

fof(f1078,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(sF1,meet(a,X0)),
    inference(forward_demodulation,[],[f1064,f48]) ).

fof(f1085,plain,
    ! [X0] : meet(a,join(meet(a,sF1),X0)) = join(sF1,meet(a,X0)),
    inference(forward_demodulation,[],[f1078,f1]) ).

fof(f1092,plain,
    ! [X0] : join(meet(X0,a),meet(sF1,join(X0,a))) = join(sF1,meet(a,X0)),
    inference(backward_demodulation,[],[f370,f1085]) ).

fof(f1127,plain,
    ! [X0,X1] : meet(X1,join(X0,X0)) = join(meet(X0,X1),meet(X1,X0)),
    inference(superposition,[],[f244,f240]) ).

fof(f1168,plain,
    ! [X0,X1] : meet(X1,X0) = join(meet(X0,X1),meet(X1,X0)),
    inference(forward_demodulation,[],[f1127,f98]) ).

fof(f1300,plain,
    ! [X2,X3,X0,X1] : join(meet(a,X3),meet(join(X2,X3),meet(X0,X1))) = join(meet(a,X3),meet(X0,meet(X1,join(X2,X3)))),
    inference(superposition,[],[f492,f2]) ).

fof(f1439,plain,
    ! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X0,X1))),
    inference(superposition,[],[f303,f4]) ).

fof(f1450,plain,
    ! [X2,X0,X1] : join(X2,X0) = join(X0,join(meet(X1,X0),X2)),
    inference(superposition,[],[f303,f240]) ).

fof(f1486,plain,
    ! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
    inference(superposition,[],[f283,f303]) ).

fof(f1502,plain,
    ! [X2,X3,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X0,join(X1,meet(X2,X3)))),
    inference(superposition,[],[f283,f303]) ).

fof(f1567,plain,
    ! [X2,X3,X0,X1,X4] : meet(X3,meet(X4,join(X2,join(X0,X1)))) = meet(X3,meet(X4,join(X0,join(X1,X2)))),
    inference(superposition,[],[f378,f4]) ).

fof(f1571,plain,
    ! [X2,X3,X0,X1] : meet(X3,meet(X2,join(X1,X0))) = meet(X3,meet(join(X0,X1),X2)),
    inference(superposition,[],[f378,f1]) ).

fof(f1610,plain,
    ! [X2,X3,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,X3))) = meet(X0,join(X3,X2)),
    inference(superposition,[],[f316,f378]) ).

fof(f1612,plain,
    ! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(meet(X1,join(X3,X2)),X0),
    inference(superposition,[],[f1,f378]) ).

fof(f1617,plain,
    ! [X2,X3,X0,X1] : meet(X1,join(X3,X2)) = join(meet(X1,join(X3,X2)),meet(X0,meet(X1,join(X2,X3)))),
    inference(superposition,[],[f240,f378]) ).

fof(f1652,plain,
    ! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X1,meet(join(X3,X2),X0)),
    inference(forward_demodulation,[],[f1612,f2]) ).

fof(f1654,plain,
    ! [X2,X3,X0] : meet(X0,join(X3,X2)) = meet(X0,join(X2,X3)),
    inference(forward_demodulation,[],[f1610,f316]) ).

fof(f1721,plain,
    ! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
    inference(superposition,[],[f1654,f4]) ).

fof(f1769,plain,
    ! [X2,X0,X1] : join(meet(a,X2),meet(X0,join(X1,X2))) = join(meet(a,X2),meet(join(X2,X1),X0)),
    inference(superposition,[],[f491,f1654]) ).

fof(f1771,plain,
    ! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
    inference(superposition,[],[f1,f1654]) ).

fof(f1834,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,join(X0,X1))) = meet(join(X0,meet(a,X1)),join(meet(a,X0),X1)),
    inference(backward_demodulation,[],[f481,f1771]) ).

fof(f1888,plain,
    ! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
    inference(superposition,[],[f303,f98]) ).

fof(f1939,plain,
    sF0 = join(sF0,y2),
    inference(superposition,[],[f5,f219]) ).

fof(f1941,plain,
    ! [X0] : join(sF0,X0) = join(sF0,join(y2,X0)),
    inference(superposition,[],[f283,f219]) ).

fof(f1954,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(meet(join(X0,meet(a,X1)),join(X1,meet(a,X0))),join(X0,meet(a,X1))),
    inference(superposition,[],[f16,f97]) ).

fof(f1957,plain,
    ! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
    inference(superposition,[],[f1654,f97]) ).

fof(f1975,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(join(X0,meet(a,X1)),meet(join(X0,meet(a,X1)),join(X1,meet(a,X0)))),
    inference(forward_demodulation,[],[f1954,f3]) ).

fof(f1986,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(X0,join(meet(a,X1),meet(join(X0,meet(a,X1)),join(X1,meet(a,X0))))),
    inference(forward_demodulation,[],[f1975,f4]) ).

fof(f1991,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X0,meet(a,X1)),join(X1,X0)),
    inference(forward_demodulation,[],[f1986,f297]) ).

fof(f1993,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X1,X0),join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f1991,f1771]) ).

fof(f2000,plain,
    ! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(meet(X1,join(X3,X2)),meet(X4,X0)),
    inference(superposition,[],[f332,f378]) ).

fof(f2022,plain,
    ! [X0,X1] : meet(X1,X0) = meet(X0,meet(X0,X1)),
    inference(superposition,[],[f332,f97]) ).

fof(f2031,plain,
    ! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X1,X0),X2)),
    inference(superposition,[],[f332,f128]) ).

fof(f2050,plain,
    ! [X2,X3,X0,X1] : meet(join(X0,X1),meet(X2,X3)) = meet(X2,meet(X3,join(X1,X0))),
    inference(superposition,[],[f378,f332]) ).

fof(f2061,plain,
    ! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
    inference(superposition,[],[f316,f332]) ).

fof(f2077,plain,
    ! [X2,X3,X0,X1] : join(X2,X3) = join(X2,join(meet(X0,meet(X1,X2)),X3)),
    inference(superposition,[],[f283,f332]) ).

fof(f2091,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X2,X0))) = meet(join(meet(a,X0),X1),join(X0,X2)),
    inference(backward_demodulation,[],[f754,f2077]) ).

fof(f2124,plain,
    ! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(X1,meet(join(X3,X2),meet(X4,X0))),
    inference(forward_demodulation,[],[f2000,f2]) ).

fof(f2128,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(join(X1,X0),X2)) = meet(join(meet(a,X0),X2),join(X0,X1)),
    inference(backward_demodulation,[],[f492,f2091]) ).

fof(f2133,plain,
    ! [X2,X0,X1] : join(meet(a,X2),meet(join(X2,X1),X0)) = meet(join(meet(a,X2),X0),join(X2,X1)),
    inference(backward_demodulation,[],[f1769,f2091]) ).

fof(f2158,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(X1,join(X0,X2))) = meet(join(meet(a,X0),X1),join(X0,X2)),
    inference(backward_demodulation,[],[f491,f2133]) ).

fof(f2166,plain,
    ! [X2,X3,X0,X1] : join(meet(a,X2),meet(X0,meet(X1,join(X2,X3)))) = meet(join(meet(a,X2),meet(X0,X1)),join(X2,X3)),
    inference(backward_demodulation,[],[f518,f2133]) ).

fof(f2181,plain,
    ! [X2,X3,X0,X1] : join(meet(a,X3),meet(X0,meet(X1,join(X2,X3)))) = meet(join(meet(a,X3),meet(X0,X1)),join(X3,X2)),
    inference(backward_demodulation,[],[f1300,f2128]) ).

fof(f2245,plain,
    sF1 = meet(sF1,sF2),
    inference(superposition,[],[f128,f145]) ).

fof(f2250,plain,
    sF1 = meet(sF2,sF1),
    inference(forward_demodulation,[],[f2245,f1]) ).

fof(f2443,plain,
    sF1 = meet(sF1,a),
    inference(superposition,[],[f128,f257]) ).

fof(f2448,plain,
    sF1 = meet(a,sF1),
    inference(forward_demodulation,[],[f2443,f1]) ).

fof(f2455,plain,
    ! [X0] : join(sF1,meet(a,X0)) = meet(a,join(sF1,X0)),
    inference(backward_demodulation,[],[f1085,f2448]) ).

fof(f2457,plain,
    ! [X0] : join(meet(X0,a),meet(sF1,join(X0,a))) = meet(a,join(sF1,X0)),
    inference(backward_demodulation,[],[f1092,f2455]) ).

fof(f2491,plain,
    ! [X0,X1] : meet(meet(X0,a),X1) = meet(meet(X0,a),meet(meet(a,join(sF1,X0)),X1)),
    inference(superposition,[],[f316,f2457]) ).

fof(f2492,plain,
    ! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(meet(a,join(sF1,X0)),X1))),
    inference(forward_demodulation,[],[f2491,f2]) ).

fof(f2506,plain,
    ! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(a,meet(join(sF1,X0),X1)))),
    inference(forward_demodulation,[],[f2492,f2]) ).

fof(f2517,plain,
    ! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(join(sF1,X0),X1))),
    inference(forward_demodulation,[],[f2506,f433]) ).

fof(f2526,plain,
    ! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(a,meet(join(sF1,X0),X1))),
    inference(forward_demodulation,[],[f2517,f2]) ).

fof(f2535,plain,
    ! [X0] : meet(a,join(sF1,X0)) = join(sF1,meet(X0,a)),
    inference(superposition,[],[f2455,f1]) ).

fof(f2553,plain,
    ! [X0,X1] : join(meet(a,join(sF1,X0)),X1) = join(sF1,join(meet(a,X0),X1)),
    inference(superposition,[],[f4,f2455]) ).

fof(f2616,plain,
    sF0 = join(x2,sF0),
    inference(superposition,[],[f382,f21]) ).

fof(f2617,plain,
    sF2 = join(x2,sF2),
    inference(superposition,[],[f382,f25]) ).

fof(f2621,plain,
    sF8 = join(sF7,sF8),
    inference(superposition,[],[f382,f45]) ).

fof(f2643,plain,
    sF2 = join(sF2,x2),
    inference(forward_demodulation,[],[f2617,f3]) ).

fof(f2644,plain,
    sF0 = join(sF0,x2),
    inference(forward_demodulation,[],[f2616,f3]) ).

fof(f2749,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(a,X1))) = meet(meet(X0,join(X2,meet(a,X1))),meet(X0,join(X1,X2))),
    inference(superposition,[],[f128,f247]) ).

fof(f2764,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(a,X1))) = meet(X0,meet(join(X2,meet(a,X1)),meet(X0,join(X1,X2)))),
    inference(forward_demodulation,[],[f2749,f2]) ).

fof(f2808,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(a,X1))) = meet(X0,meet(join(X2,X1),meet(X0,join(X2,meet(a,X1))))),
    inference(forward_demodulation,[],[f2764,f2124]) ).

fof(f2958,plain,
    ! [X2,X0,X1] : join(X0,X2) = join(meet(X1,X0),join(X0,X2)),
    inference(superposition,[],[f286,f240]) ).

fof(f2972,plain,
    ! [X0] : join(sF2,X0) = join(z2,join(x2,X0)),
    inference(superposition,[],[f286,f25]) ).

fof(f3044,plain,
    ! [X0] : join(sF2,X0) = join(x2,join(X0,z2)),
    inference(forward_demodulation,[],[f2972,f303]) ).

fof(f3054,plain,
    ! [X2,X0,X1] : join(X0,X2) = join(X0,join(X2,meet(X1,X0))),
    inference(forward_demodulation,[],[f2958,f303]) ).

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

fof(f3110,plain,
    ! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
    inference(superposition,[],[f317,f1]) ).

fof(f3115,plain,
    ! [X2,X3,X0,X1] : meet(X3,meet(X0,X1)) = meet(X3,meet(X0,meet(X1,join(X2,X3)))),
    inference(superposition,[],[f317,f332]) ).

fof(f3116,plain,
    ! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
    inference(superposition,[],[f317,f332]) ).

fof(f3166,plain,
    ! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(X1,a)),
    inference(backward_demodulation,[],[f2526,f3116]) ).

fof(f3188,plain,
    ! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X0,meet(X1,meet(X0,X2))),
    inference(forward_demodulation,[],[f3086,f2]) ).

fof(f3203,plain,
    ! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X0,meet(X1,meet(X0,X2))),
    inference(forward_demodulation,[],[f3188,f2]) ).

fof(f3214,plain,
    ! [X2,X0,X1] : meet(X0,join(X2,meet(a,X1))) = meet(X0,meet(join(X2,X1),join(X2,meet(a,X1)))),
    inference(backward_demodulation,[],[f2808,f3203]) ).

fof(f3284,plain,
    ! [X0] : meet(sF7,X0) = meet(z2,meet(y2,X0)),
    inference(superposition,[],[f319,f37]) ).

fof(f3285,plain,
    ! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
    inference(superposition,[],[f319,f42]) ).

fof(f3332,plain,
    ! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
    inference(superposition,[],[f128,f319]) ).

fof(f3336,plain,
    ! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(X4,meet(meet(X1,X0),join(X3,X2))),
    inference(superposition,[],[f378,f319]) ).

fof(f3341,plain,
    ! [X2,X3,X0,X1,X4] : meet(X4,meet(X0,meet(X1,join(X2,X3)))) = meet(X4,meet(X1,meet(X0,join(X3,X2)))),
    inference(forward_demodulation,[],[f3336,f2]) ).

fof(f3376,plain,
    ! [X0] : meet(sF1,X0) = meet(sF0,meet(X0,a)),
    inference(forward_demodulation,[],[f3285,f332]) ).

fof(f3377,plain,
    ! [X0] : meet(sF7,X0) = meet(y2,meet(X0,z2)),
    inference(forward_demodulation,[],[f3284,f332]) ).

fof(f3399,plain,
    ! [X0] : join(meet(X0,sF2),meet(sF1,join(X0,sF2))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF1,X0))),
    inference(backward_demodulation,[],[f380,f3376]) ).

fof(f3400,plain,
    ! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF1,X0))),
    inference(backward_demodulation,[],[f379,f3376]) ).

fof(f3418,plain,
    ! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(join(sF2,meet(sF1,X0)),join(X0,meet(a,sF6))),
    inference(forward_demodulation,[],[f3400,f1771]) ).

fof(f3419,plain,
    ! [X0] : join(meet(X0,sF2),meet(sF1,join(X0,sF2))) = meet(join(sF2,meet(sF1,X0)),join(X0,meet(a,sF6))),
    inference(forward_demodulation,[],[f3399,f1771]) ).

fof(f3592,plain,
    ! [X2,X0,X1] : join(join(X1,meet(a,X2)),meet(X0,join(X1,X2))) = join(join(X1,meet(a,X2)),meet(X0,join(X2,meet(X1,a)))),
    inference(superposition,[],[f284,f246]) ).

fof(f3603,plain,
    ! [X2,X3,X0,X1] : join(X2,join(X3,X0)) = join(X2,join(X0,join(meet(X1,X2),X3))),
    inference(superposition,[],[f284,f303]) ).

fof(f3610,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(meet(X2,X0),X1),join(X0,X1)),
    inference(superposition,[],[f128,f284]) ).

fof(f3631,plain,
    ! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(X1,meet(X2,X0))),
    inference(forward_demodulation,[],[f3610,f1771]) ).

fof(f3644,plain,
    ! [X2,X0,X1] : join(join(X1,meet(a,X2)),meet(X0,join(X1,X2))) = join(X1,join(meet(a,X2),meet(X0,join(X2,meet(X1,a))))),
    inference(forward_demodulation,[],[f3592,f4]) ).

fof(f3663,plain,
    ! [X2,X0,X1] : join(join(X1,meet(a,X2)),meet(X0,join(X1,X2))) = join(X1,meet(join(meet(a,X2),X0),join(X2,meet(X1,a)))),
    inference(forward_demodulation,[],[f3644,f2158]) ).

fof(f3674,plain,
    ! [X2,X0,X1] : join(X1,join(meet(a,X2),meet(X0,join(X1,X2)))) = join(X1,meet(join(meet(a,X2),X0),join(X2,meet(X1,a)))),
    inference(forward_demodulation,[],[f3663,f4]) ).

fof(f3676,plain,
    ! [X2,X0,X1] : join(X1,meet(join(meet(a,X2),X0),join(X2,X1))) = join(X1,meet(join(meet(a,X2),X0),join(X2,meet(X1,a)))),
    inference(forward_demodulation,[],[f3674,f2091]) ).

fof(f3726,plain,
    ! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X0,meet(X1,X2))),
    inference(superposition,[],[f221,f2]) ).

fof(f3757,plain,
    ! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
    inference(superposition,[],[f284,f221]) ).

fof(f3933,plain,
    sF1 = meet(sF1,sF0),
    inference(superposition,[],[f128,f74]) ).

fof(f3943,plain,
    sF1 = meet(sF0,sF1),
    inference(forward_demodulation,[],[f3933,f1]) ).

fof(f3980,plain,
    ! [X0] : sF2 = join(sF2,meet(sF1,X0)),
    inference(superposition,[],[f5,f325]) ).

fof(f3992,plain,
    ! [X0] : join(meet(X0,sF2),meet(sF1,join(X0,sF2))) = meet(sF2,join(X0,meet(a,sF6))),
    inference(backward_demodulation,[],[f3419,f3980]) ).

fof(f3993,plain,
    ! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(sF2,join(X0,meet(a,sF6))),
    inference(backward_demodulation,[],[f3418,f3980]) ).

fof(f4047,plain,
    meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF1,join(sF2,x2))),
    inference(superposition,[],[f3993,f156]) ).

fof(f4083,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(meet(sF1,join(sF2,X0)),meet(sF2,join(X0,meet(a,sF6)))),
    inference(superposition,[],[f128,f3993]) ).

fof(f4085,plain,
    ! [X0,X1] : join(meet(sF2,X0),join(meet(sF1,join(sF2,X0)),X1)) = join(X1,meet(sF2,join(X0,meet(a,sF6)))),
    inference(superposition,[],[f303,f3993]) ).

fof(f4094,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,meet(join(sF2,X0),meet(sF2,join(X0,meet(a,sF6))))),
    inference(forward_demodulation,[],[f4083,f2]) ).

fof(f4120,plain,
    meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF1,sF2)),
    inference(forward_demodulation,[],[f4047,f2643]) ).

fof(f4124,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(join(meet(a,sF6),X0),meet(sF1,join(sF2,X0)))),
    inference(forward_demodulation,[],[f4094,f2124]) ).

fof(f4140,plain,
    meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF2,sF1)),
    inference(forward_demodulation,[],[f4120,f1]) ).

fof(f4144,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(sF1,meet(join(meet(a,sF6),X0),join(X0,sF2)))),
    inference(forward_demodulation,[],[f4124,f3341]) ).

fof(f4155,plain,
    meet(sF2,join(x2,meet(a,sF6))) = join(x2,sF1),
    inference(forward_demodulation,[],[f4140,f2250]) ).

fof(f4158,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(sF1,join(meet(a,sF6),X0))),
    inference(forward_demodulation,[],[f4144,f3115]) ).

fof(f4197,plain,
    ! [X0,X1] : meet(meet(X0,sF2),X1) = meet(meet(X0,sF2),meet(meet(sF2,join(X0,meet(a,sF6))),X1)),
    inference(superposition,[],[f316,f3992]) ).

fof(f4201,plain,
    ! [X0,X1] : meet(meet(X0,sF2),X1) = meet(X0,meet(sF2,meet(meet(sF2,join(X0,meet(a,sF6))),X1))),
    inference(forward_demodulation,[],[f4197,f2]) ).

fof(f4215,plain,
    ! [X0,X1] : meet(meet(X0,sF2),X1) = meet(X0,meet(sF2,meet(sF2,meet(join(X0,meet(a,sF6)),X1)))),
    inference(forward_demodulation,[],[f4201,f2]) ).

fof(f4223,plain,
    ! [X0,X1] : meet(X0,meet(sF2,meet(join(X0,meet(a,sF6)),X1))) = meet(meet(X0,sF2),X1),
    inference(forward_demodulation,[],[f4215,f433]) ).

fof(f4229,plain,
    ! [X0,X1] : meet(X0,meet(sF2,X1)) = meet(X0,meet(sF2,meet(join(X0,meet(a,sF6)),X1))),
    inference(forward_demodulation,[],[f4223,f2]) ).

fof(f4234,plain,
    ! [X0,X1] : meet(X0,meet(X1,sF2)) = meet(X0,meet(sF2,X1)),
    inference(forward_demodulation,[],[f4229,f2061]) ).

fof(f4563,plain,
    join(sF8,y2) = join(sF7,sF0),
    inference(superposition,[],[f292,f21]) ).

fof(f4564,plain,
    join(sF8,z2) = join(sF7,sF2),
    inference(superposition,[],[f292,f25]) ).

fof(f4600,plain,
    join(sF8,z2) = join(sF2,sF7),
    inference(forward_demodulation,[],[f4564,f3]) ).

fof(f4601,plain,
    join(sF8,y2) = join(sF0,sF7),
    inference(forward_demodulation,[],[f4563,f3]) ).

fof(f4610,plain,
    join(sF2,sF7) = join(z2,sF8),
    inference(forward_demodulation,[],[f4600,f3]) ).

fof(f4611,plain,
    join(sF0,sF7) = join(y2,sF8),
    inference(forward_demodulation,[],[f4601,f3]) ).

fof(f4620,plain,
    ! [X0] : join(X0,y2) = join(sF7,join(y2,X0)),
    inference(superposition,[],[f303,f162]) ).

fof(f4653,plain,
    ! [X0] : meet(sF1,X0) = meet(sF2,meet(sF1,X0)),
    inference(superposition,[],[f433,f325]) ).

fof(f4723,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,join(meet(a,sF6),X0)),
    inference(backward_demodulation,[],[f4158,f4653]) ).

fof(f4747,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(X1,meet(a,X0)),join(meet(a,meet(X0,X1)),X0)),
    inference(superposition,[],[f190,f97]) ).

fof(f4760,plain,
    ! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,meet(X0,join(join(X0,X1),X2)))) = meet(join(X2,meet(a,X0)),join(meet(a,meet(X0,X2)),join(X0,X1))),
    inference(superposition,[],[f190,f6]) ).

fof(f4794,plain,
    ! [X0,X1] : join(meet(X0,a),meet(a,meet(X1,join(X0,a)))) = meet(a,join(meet(a,meet(X1,a)),X0)),
    inference(superposition,[],[f190,f5]) ).

fof(f4876,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(join(X1,meet(a,meet(X2,X0))),join(meet(X0,X1),meet(a,meet(X2,join(X0,X1))))),
    inference(superposition,[],[f5,f190]) ).

fof(f4891,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(X1,join(meet(a,meet(X2,X0)),join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))))),
    inference(forward_demodulation,[],[f4876,f4]) ).

fof(f4953,plain,
    ! [X0,X1] : join(meet(X0,a),meet(a,meet(X1,join(X0,a)))) = meet(a,join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f4794,f221]) ).

fof(f4983,plain,
    ! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,meet(X0,join(join(X0,X1),X2)))) = meet(join(X2,meet(a,X0)),join(X0,join(X1,meet(a,meet(X0,X2))))),
    inference(forward_demodulation,[],[f4760,f1721]) ).

fof(f4994,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(X1,meet(a,X0)),join(X0,meet(a,meet(X0,X1)))),
    inference(forward_demodulation,[],[f4747,f1654]) ).

fof(f4999,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(X1,join(meet(a,meet(X2,join(X0,X1))),meet(a,meet(X2,X0)))),
    inference(forward_demodulation,[],[f4891,f3603]) ).

fof(f5047,plain,
    ! [X0,X1] : join(meet(X0,a),meet(a,X1)) = meet(a,join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f4953,f3110]) ).

fof(f5072,plain,
    ! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,meet(X0,join(X0,join(X1,X2))))) = meet(join(X2,meet(a,X0)),join(X0,join(X1,meet(a,meet(X0,X2))))),
    inference(forward_demodulation,[],[f4983,f4]) ).

fof(f5075,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(X1,meet(a,X0)),X0),
    inference(forward_demodulation,[],[f4994,f414]) ).

fof(f5078,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(X1,join(meet(a,meet(X2,X0)),meet(a,meet(X2,join(X0,X1))))),
    inference(forward_demodulation,[],[f4999,f3]) ).

fof(f5146,plain,
    ! [X2,X0,X1] : join(meet(join(X0,X1),X2),meet(a,X0)) = meet(join(X2,meet(a,X0)),join(X0,join(X1,meet(a,meet(X0,X2))))),
    inference(forward_demodulation,[],[f5072,f6]) ).

fof(f5149,plain,
    ! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(X0,join(meet(a,X0),X1)),
    inference(forward_demodulation,[],[f5075,f1771]) ).

fof(f5209,plain,
    ! [X2,X0,X1] : join(meet(a,X0),meet(join(X0,X1),X2)) = meet(join(X2,meet(a,X0)),join(X0,join(X1,meet(a,meet(X0,X2))))),
    inference(forward_demodulation,[],[f5146,f3]) ).

fof(f5210,plain,
    ! [X0,X1] : meet(X0,join(meet(a,X0),X1)) = join(meet(X0,X1),meet(a,X0)),
    inference(forward_demodulation,[],[f5149,f6]) ).

fof(f5262,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(X0,X1)) = meet(join(X2,meet(a,X0)),join(X0,join(X1,meet(a,meet(X0,X2))))),
    inference(forward_demodulation,[],[f5209,f2133]) ).

fof(f5434,plain,
    ! [X0] : join(meet(a,sF2),meet(X0,sF2)) = meet(join(meet(a,sF2),X0),sF2),
    inference(superposition,[],[f2158,f2643]) ).

fof(f5435,plain,
    ! [X0] : join(meet(a,sF4),meet(X0,sF4)) = meet(join(meet(a,sF4),X0),sF4),
    inference(superposition,[],[f2158,f166]) ).

fof(f5496,plain,
    ! [X0] : join(meet(a,sF4),meet(X0,sF4)) = meet(sF4,join(X0,meet(a,sF4))),
    inference(forward_demodulation,[],[f5435,f1771]) ).

fof(f5497,plain,
    ! [X0] : join(meet(a,sF2),meet(X0,sF2)) = meet(sF2,join(X0,meet(a,sF2))),
    inference(forward_demodulation,[],[f5434,f1771]) ).

fof(f5557,plain,
    ! [X0] : join(meet(sF4,a),meet(X0,sF4)) = meet(sF4,join(X0,meet(sF4,a))),
    inference(forward_demodulation,[],[f5496,f1]) ).

fof(f5558,plain,
    ! [X0] : join(meet(sF2,a),meet(X0,sF2)) = meet(sF2,join(X0,meet(sF2,a))),
    inference(forward_demodulation,[],[f5497,f1]) ).

fof(f5596,plain,
    ! [X0] : join(sF1,meet(X0,sF4)) = meet(sF4,join(X0,sF1)),
    inference(forward_demodulation,[],[f5557,f48]) ).

fof(f5597,plain,
    ! [X0] : join(sF1,meet(X0,sF2)) = meet(sF2,join(X0,sF1)),
    inference(forward_demodulation,[],[f5558,f47]) ).

fof(f5858,plain,
    ! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X2,X0)),
    inference(superposition,[],[f1571,f98]) ).

fof(f6484,plain,
    meet(sF0,sF1) = meet(sF6,a),
    inference(superposition,[],[f324,f47]) ).

fof(f6486,plain,
    meet(sF6,z2) = meet(sF0,z2),
    inference(superposition,[],[f324,f218]) ).

fof(f6568,plain,
    meet(sF0,z2) = meet(z2,sF6),
    inference(forward_demodulation,[],[f6486,f1]) ).

fof(f6570,plain,
    meet(a,sF6) = meet(sF0,sF1),
    inference(forward_demodulation,[],[f6484,f1]) ).

fof(f6586,plain,
    sF1 = meet(a,sF6),
    inference(forward_demodulation,[],[f6570,f3943]) ).

fof(f6606,plain,
    ! [X0,X1] : join(meet(sF2,X0),join(meet(sF1,join(sF2,X0)),X1)) = join(X1,meet(sF2,join(X0,sF1))),
    inference(backward_demodulation,[],[f4085,f6586]) ).

fof(f6618,plain,
    join(x2,sF1) = meet(sF2,join(x2,sF1)),
    inference(backward_demodulation,[],[f4155,f6586]) ).

fof(f6635,plain,
    ! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,join(sF1,X0)),
    inference(backward_demodulation,[],[f4723,f6586]) ).

fof(f6656,plain,
    ! [X0] : sF1 = meet(sF1,join(sF2,X0)),
    inference(forward_demodulation,[],[f6635,f6]) ).

fof(f6688,plain,
    ! [X0,X1] : join(X1,meet(sF2,join(X0,sF1))) = join(meet(sF2,X0),join(sF1,X1)),
    inference(backward_demodulation,[],[f6606,f6656]) ).

fof(f6717,plain,
    ! [X0,X1] : join(X1,meet(sF2,join(X0,sF1))) = join(sF1,join(X1,meet(sF2,X0))),
    inference(forward_demodulation,[],[f6688,f303]) ).

fof(f8932,plain,
    ! [X2,X0,X1] : join(meet(X0,a),meet(join(X1,X0),X2)) = meet(join(meet(X0,a),X2),join(X0,X1)),
    inference(superposition,[],[f2128,f1]) ).

fof(f8974,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),join(sF1,a)) = join(meet(a,sF1),meet(a,X0)),
    inference(superposition,[],[f2128,f257]) ).

fof(f8977,plain,
    ! [X0] : join(meet(a,y2),meet(sF0,X0)) = meet(join(meet(a,y2),X0),join(y2,x2)),
    inference(superposition,[],[f2128,f21]) ).

fof(f9008,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(a,X1),meet(X3,X2)),join(X1,X0)) = join(meet(a,X1),meet(join(X0,X1),meet(X2,X3))),
    inference(superposition,[],[f2128,f5858]) ).

fof(f9018,plain,
    ! [X2,X0,X1] : join(meet(a,X1),meet(join(X0,X1),meet(X2,sF2))) = meet(join(meet(a,X1),meet(sF2,X2)),join(X1,X0)),
    inference(superposition,[],[f2128,f4234]) ).

fof(f9069,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X1),meet(X2,sF2)),join(X1,X0)) = meet(join(meet(a,X1),meet(sF2,X2)),join(X1,X0)),
    inference(forward_demodulation,[],[f9018,f2128]) ).

fof(f9077,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(a,X1),meet(X3,X2)),join(X1,X0)) = meet(join(meet(a,X1),meet(X2,X3)),join(X1,X0)),
    inference(forward_demodulation,[],[f9008,f2128]) ).

fof(f9106,plain,
    ! [X0] : join(meet(a,y2),meet(sF0,X0)) = meet(join(y2,x2),join(X0,meet(a,y2))),
    inference(forward_demodulation,[],[f8977,f1771]) ).

fof(f9109,plain,
    ! [X0] : join(sF1,meet(a,X0)) = meet(join(sF1,X0),join(sF1,a)),
    inference(forward_demodulation,[],[f8974,f2448]) ).

fof(f9186,plain,
    ! [X0] : join(meet(a,y2),meet(sF0,X0)) = meet(join(x2,y2),join(X0,meet(a,y2))),
    inference(forward_demodulation,[],[f9106,f3]) ).

fof(f9189,plain,
    ! [X0] : join(sF1,meet(a,X0)) = meet(join(sF1,X0),join(a,sF1)),
    inference(forward_demodulation,[],[f9109,f1654]) ).

fof(f9253,plain,
    ! [X0] : join(meet(a,y2),meet(sF0,X0)) = meet(sF0,join(X0,meet(a,y2))),
    inference(forward_demodulation,[],[f9186,f21]) ).

fof(f9256,plain,
    ! [X0] : join(sF1,meet(a,X0)) = meet(join(a,sF1),join(X0,sF1)),
    inference(forward_demodulation,[],[f9189,f1771]) ).

fof(f9307,plain,
    ! [X0] : join(sF1,meet(a,X0)) = meet(a,join(X0,sF1)),
    inference(forward_demodulation,[],[f9256,f257]) ).

fof(f9399,plain,
    meet(sF0,join(a,meet(a,y2))) = join(meet(a,y2),sF1),
    inference(superposition,[],[f9253,f42]) ).

fof(f9492,plain,
    meet(sF0,join(a,meet(a,y2))) = join(sF1,meet(a,y2)),
    inference(forward_demodulation,[],[f9399,f3]) ).

fof(f9523,plain,
    meet(sF0,join(a,meet(a,y2))) = meet(a,join(sF1,y2)),
    inference(forward_demodulation,[],[f9492,f2455]) ).

fof(f9545,plain,
    meet(sF0,join(a,meet(a,y2))) = meet(a,join(y2,sF1)),
    inference(forward_demodulation,[],[f9523,f1654]) ).

fof(f9557,plain,
    meet(sF0,a) = meet(a,join(y2,sF1)),
    inference(forward_demodulation,[],[f9545,f5]) ).

fof(f9564,plain,
    sF1 = meet(a,join(y2,sF1)),
    inference(forward_demodulation,[],[f9557,f42]) ).

fof(f10150,plain,
    join(sF0,sF7) = join(y2,join(sF0,sF7)),
    inference(superposition,[],[f382,f4611]) ).

fof(f10159,plain,
    join(sF0,sF7) = join(sF7,join(y2,sF0)),
    inference(forward_demodulation,[],[f10150,f303]) ).

fof(f10168,plain,
    join(sF0,y2) = join(sF0,sF7),
    inference(forward_demodulation,[],[f10159,f4620]) ).

fof(f10172,plain,
    sF0 = join(sF0,sF7),
    inference(forward_demodulation,[],[f10168,f1939]) ).

fof(f10283,plain,
    sF7 = meet(sF7,sF0),
    inference(superposition,[],[f128,f10172]) ).

fof(f10301,plain,
    sF7 = meet(sF0,sF7),
    inference(forward_demodulation,[],[f10283,f1]) ).

fof(f10442,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(join(a,meet(a,meet(sF0,X0))),join(meet(a,sF1),X0)),
    inference(superposition,[],[f192,f42]) ).

fof(f10450,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF2,join(a,X0)))) = meet(join(a,meet(a,meet(sF2,X0))),join(meet(a,sF1),X0)),
    inference(superposition,[],[f192,f47]) ).

fof(f10455,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))) = meet(join(a,meet(a,meet(sF4,X0))),join(meet(a,sF1),X0)),
    inference(superposition,[],[f192,f48]) ).

fof(f10568,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(meet(a,meet(sF4,X0)),a)),
    inference(forward_demodulation,[],[f10455,f1771]) ).

fof(f10573,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF2,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(meet(a,meet(sF2,X0)),a)),
    inference(forward_demodulation,[],[f10450,f1771]) ).

fof(f10581,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(meet(a,meet(sF0,X0)),a)),
    inference(forward_demodulation,[],[f10442,f1771]) ).

fof(f10700,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(a,meet(a,meet(sF4,X0)))),
    inference(forward_demodulation,[],[f10568,f1654]) ).

fof(f10705,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF2,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(a,meet(a,meet(sF2,X0)))),
    inference(forward_demodulation,[],[f10573,f1654]) ).

fof(f10713,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(join(meet(a,sF1),X0),join(a,meet(a,meet(sF0,X0)))),
    inference(forward_demodulation,[],[f10581,f1654]) ).

fof(f10800,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))),
    inference(forward_demodulation,[],[f10700,f5]) ).

fof(f10805,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,meet(sF2,join(a,X0)))),
    inference(forward_demodulation,[],[f10705,f5]) ).

fof(f10813,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(join(meet(a,sF1),X0),a),
    inference(forward_demodulation,[],[f10713,f5]) ).

fof(f10882,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(meet(a,X0),meet(a,sF4)),join(X0,a)),
    inference(forward_demodulation,[],[f10800,f2181]) ).

fof(f10887,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(meet(a,X0),meet(a,sF2)),join(X0,a)),
    inference(forward_demodulation,[],[f10805,f2181]) ).

fof(f10895,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(a,join(X0,meet(a,sF1))),
    inference(forward_demodulation,[],[f10813,f1771]) ).

fof(f10950,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(meet(a,X0),meet(sF4,a)),join(X0,a)),
    inference(forward_demodulation,[],[f10882,f9077]) ).

fof(f10955,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(meet(a,X0),meet(sF2,a)),join(X0,a)),
    inference(forward_demodulation,[],[f10887,f9069]) ).

fof(f10963,plain,
    ! [X0] : join(meet(a,X0),meet(a,meet(sF0,join(a,X0)))) = meet(a,join(X0,sF1)),
    inference(forward_demodulation,[],[f10895,f2448]) ).

fof(f11013,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(X0,a),join(meet(sF4,a),meet(a,X0))),
    inference(forward_demodulation,[],[f10950,f1771]) ).

fof(f11018,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(X0,a),join(meet(sF2,a),meet(a,X0))),
    inference(forward_demodulation,[],[f10955,f1771]) ).

fof(f11026,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(join(meet(a,X0),meet(a,sF0)),join(X0,a)),
    inference(forward_demodulation,[],[f10963,f2181]) ).

fof(f11059,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(X0,a),meet(a,join(meet(a,X0),sF4))),
    inference(forward_demodulation,[],[f11013,f5047]) ).

fof(f11064,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(join(X0,a),meet(a,join(meet(a,X0),sF2))),
    inference(forward_demodulation,[],[f11018,f5047]) ).

fof(f11072,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(join(meet(a,X0),meet(sF0,a)),join(X0,a)),
    inference(forward_demodulation,[],[f11026,f9077]) ).

fof(f11098,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(meet(a,X0),sF4),join(a,X0))),
    inference(forward_demodulation,[],[f11059,f2050]) ).

fof(f11103,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(meet(a,X0),sF2),join(a,X0))),
    inference(forward_demodulation,[],[f11064,f2050]) ).

fof(f11109,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(join(X0,a),join(meet(sF0,a),meet(a,X0))),
    inference(forward_demodulation,[],[f11072,f1771]) ).

fof(f11127,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(X0,a),join(meet(a,X0),sF4))),
    inference(forward_demodulation,[],[f11098,f1571]) ).

fof(f11130,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(X0,a),join(meet(a,X0),sF2))),
    inference(forward_demodulation,[],[f11103,f1571]) ).

fof(f11133,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(join(X0,a),meet(a,join(meet(a,X0),sF0))),
    inference(forward_demodulation,[],[f11109,f5047]) ).

fof(f11150,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(X0,a),join(sF4,meet(a,X0)))),
    inference(forward_demodulation,[],[f11127,f378]) ).

fof(f11153,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,meet(join(X0,a),join(sF2,meet(a,X0)))),
    inference(forward_demodulation,[],[f11130,f378]) ).

fof(f11155,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,meet(join(meet(a,X0),sF0),join(a,X0))),
    inference(forward_demodulation,[],[f11133,f2050]) ).

fof(f11167,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,join(sF4,meet(a,X0))),
    inference(forward_demodulation,[],[f11150,f317]) ).

fof(f11169,plain,
    ! [X0] : meet(join(meet(a,sF1),X0),a) = meet(a,join(sF2,meet(a,X0))),
    inference(forward_demodulation,[],[f11153,f317]) ).

fof(f11171,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,meet(join(X0,a),join(meet(a,X0),sF0))),
    inference(forward_demodulation,[],[f11155,f1571]) ).

fof(f11179,plain,
    ! [X0] : meet(a,join(X0,meet(a,sF1))) = meet(a,join(sF4,meet(a,X0))),
    inference(forward_demodulation,[],[f11167,f1771]) ).

fof(f11181,plain,
    ! [X0] : meet(a,join(X0,meet(a,sF1))) = meet(a,join(sF2,meet(a,X0))),
    inference(forward_demodulation,[],[f11169,f1771]) ).

fof(f11183,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,meet(join(X0,a),join(sF0,meet(a,X0)))),
    inference(forward_demodulation,[],[f11171,f378]) ).

fof(f11187,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,join(sF4,meet(a,X0))),
    inference(forward_demodulation,[],[f11179,f2448]) ).

fof(f11188,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,join(sF2,meet(a,X0))),
    inference(forward_demodulation,[],[f11181,f2448]) ).

fof(f11190,plain,
    ! [X0] : meet(a,join(X0,sF1)) = meet(a,join(sF0,meet(a,X0))),
    inference(forward_demodulation,[],[f11183,f317]) ).

fof(f11445,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X0,X1),join(X2,meet(X1,X0))),
    inference(superposition,[],[f303,f1168]) ).

fof(f13605,plain,
    ! [X2,X3,X0,X1] : join(X1,X3) = join(X1,join(X3,meet(X0,meet(X1,X2)))),
    inference(superposition,[],[f396,f332]) ).

fof(f13719,plain,
    ! [X0] : join(sF7,x2) = join(sF8,meet(sF7,X0)),
    inference(superposition,[],[f292,f396]) ).

fof(f13720,plain,
    ! [X0] : sF8 = join(sF8,meet(sF7,X0)),
    inference(forward_demodulation,[],[f13719,f45]) ).

fof(f13785,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X2),join(X0,X1)) = meet(join(X2,meet(a,X0)),join(X0,X1)),
    inference(backward_demodulation,[],[f5262,f13605]) ).

fof(f14999,plain,
    meet(y2,a) = meet(y2,sF1),
    inference(superposition,[],[f447,f9564]) ).

fof(f15157,plain,
    meet(a,y2) = meet(y2,sF1),
    inference(forward_demodulation,[],[f14999,f1]) ).

fof(f15878,plain,
    meet(sF7,sF6) = meet(y2,meet(sF0,z2)),
    inference(superposition,[],[f322,f6568]) ).

fof(f15906,plain,
    meet(sF7,sF0) = meet(sF7,sF6),
    inference(forward_demodulation,[],[f15878,f3377]) ).

fof(f15915,plain,
    meet(sF0,sF7) = meet(sF7,sF6),
    inference(forward_demodulation,[],[f15906,f1]) ).

fof(f15922,plain,
    sF7 = meet(sF7,sF6),
    inference(forward_demodulation,[],[f15915,f10301]) ).

fof(f16214,plain,
    sF6 = join(sF6,sF7),
    inference(superposition,[],[f240,f15922]) ).

fof(f16229,plain,
    sF6 = join(sF7,sF6),
    inference(forward_demodulation,[],[f16214,f3]) ).

fof(f16426,plain,
    ! [X0,X1] : meet(X0,join(meet(X0,a),X1)) = join(meet(X0,X1),meet(X0,a)),
    inference(superposition,[],[f5210,f1]) ).

fof(f17998,plain,
    join(x2,z2) = join(sF2,sF7),
    inference(superposition,[],[f3044,f269]) ).

fof(f18051,plain,
    sF2 = join(sF2,sF7),
    inference(forward_demodulation,[],[f17998,f25]) ).

fof(f18068,plain,
    sF2 = join(z2,sF8),
    inference(backward_demodulation,[],[f4610,f18051]) ).

fof(f19208,plain,
    ! [X0,X1] : join(meet(X1,meet(a,X0)),meet(a,join(X1,meet(a,X0)))) = meet(join(X1,meet(a,X0)),join(meet(a,X1),meet(a,X0))),
    inference(superposition,[],[f1834,f433]) ).

fof(f19294,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(join(join(X0,meet(a,X1)),meet(a,meet(a,join(X1,meet(X0,a))))),meet(a,join(X0,X1))),
    inference(superposition,[],[f1834,f246]) ).

fof(f19318,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(join(meet(X0,X1),meet(a,join(X0,X1))),meet(join(meet(a,X0),X1),join(X1,meet(a,X0)))),
    inference(superposition,[],[f244,f1834]) ).

fof(f19343,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(join(X0,meet(a,X1)),join(meet(X0,X1),meet(a,join(X0,X1)))),
    inference(superposition,[],[f5,f1834]) ).

fof(f19376,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,join(meet(a,X1),join(meet(X0,X1),meet(a,join(X0,X1))))),
    inference(forward_demodulation,[],[f19343,f4]) ).

fof(f19394,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),meet(join(meet(a,X0),X1),join(X1,meet(a,X0))))),
    inference(forward_demodulation,[],[f19318,f4]) ).

fof(f19412,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(meet(a,meet(a,join(X1,meet(X0,a)))),join(X0,meet(a,X1))))),
    inference(forward_demodulation,[],[f19294,f2050]) ).

fof(f19481,plain,
    ! [X0,X1] : join(meet(a,X0),meet(a,X1)) = join(meet(X1,meet(a,X0)),meet(a,join(X1,meet(a,X0)))),
    inference(forward_demodulation,[],[f19208,f1993]) ).

fof(f19498,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,join(meet(a,join(X0,X1)),meet(a,X1))),
    inference(forward_demodulation,[],[f19376,f1486]) ).

fof(f19515,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),join(meet(a,X0),X1))),
    inference(forward_demodulation,[],[f19394,f1957]) ).

fof(f19533,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(join(X0,meet(a,X1)),meet(a,meet(a,join(X1,meet(X0,a))))))),
    inference(forward_demodulation,[],[f19412,f378]) ).

fof(f19598,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,join(meet(a,X1),meet(a,join(X0,X1)))),
    inference(forward_demodulation,[],[f19498,f3]) ).

fof(f19615,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(X1,join(meet(X0,X1),join(meet(a,join(X0,X1)),meet(a,X0)))),
    inference(forward_demodulation,[],[f19515,f1439]) ).

fof(f19633,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,join(meet(a,X1),meet(a,meet(a,join(X1,meet(X0,a)))))))),
    inference(forward_demodulation,[],[f19533,f4]) ).

fof(f19684,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(join(meet(a,X1),a),join(X1,X0))),
    inference(forward_demodulation,[],[f19598,f2091]) ).

fof(f19701,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(X1,join(meet(a,join(X0,X1)),meet(a,X0))),
    inference(forward_demodulation,[],[f19615,f284]) ).

fof(f19719,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(join(meet(a,X1),meet(a,a)),join(X1,meet(X0,a)))))),
    inference(forward_demodulation,[],[f19633,f2166]) ).

fof(f19763,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(join(a,meet(a,X1)),join(X1,X0))),
    inference(forward_demodulation,[],[f19684,f13785]) ).

fof(f19778,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(X1,join(meet(a,X0),meet(a,join(X0,X1)))),
    inference(forward_demodulation,[],[f19701,f3]) ).

fof(f19791,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(join(meet(a,X1),meet(a,a)),join(X1,X0))))),
    inference(forward_demodulation,[],[f19719,f3676]) ).

fof(f19827,plain,
    ! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(a,join(X1,X0))),
    inference(forward_demodulation,[],[f19763,f5]) ).

fof(f19842,plain,
    ! [X0,X1] : join(X1,meet(join(meet(a,X0),a),join(X0,X1))) = meet(join(meet(a,X0),X1),join(X0,X1)),
    inference(forward_demodulation,[],[f19778,f2158]) ).

fof(f19853,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(meet(a,join(meet(a,a),X1)),join(X1,X0))))),
    inference(forward_demodulation,[],[f19791,f16426]) ).

fof(f19910,plain,
    ! [X0,X1] : join(X1,meet(join(meet(a,X0),a),join(X0,X1))) = meet(join(X0,X1),join(X1,meet(a,X0))),
    inference(forward_demodulation,[],[f19842,f1771]) ).

fof(f19919,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(a,meet(join(meet(a,a),X1),join(X1,X0)))))),
    inference(forward_demodulation,[],[f19853,f2]) ).

fof(f19961,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(join(meet(a,X0),a),join(X0,X1))),
    inference(forward_demodulation,[],[f19910,f3631]) ).

fof(f19968,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(a,meet(join(a,X1),join(X1,X0)))))),
    inference(forward_demodulation,[],[f19919,f97]) ).

fof(f20001,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(join(a,meet(a,X0)),join(X0,X1))),
    inference(forward_demodulation,[],[f19961,f13785]) ).

fof(f20007,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(a,join(X1,X0))))),
    inference(forward_demodulation,[],[f19968,f316]) ).

fof(f20035,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(a,join(X0,X1))),
    inference(forward_demodulation,[],[f20001,f5]) ).

fof(f20041,plain,
    ! [X0,X1] : join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))) = meet(a,meet(join(X0,X1),join(X0,meet(a,X1)))),
    inference(forward_demodulation,[],[f20007,f19827]) ).

fof(f20069,plain,
    ! [X0,X1] : meet(a,join(X0,meet(a,X1))) = join(meet(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))),meet(a,join(join(X0,meet(a,X1)),meet(a,join(X1,meet(X0,a)))))),
    inference(forward_demodulation,[],[f20041,f3214]) ).

fof(f20092,plain,
    ! [X0,X1] : meet(a,join(X0,meet(a,X1))) = join(meet(a,join(X1,meet(X0,a))),meet(a,join(X0,meet(a,X1)))),
    inference(forward_demodulation,[],[f20069,f19481]) ).

fof(f20114,plain,
    ! [X0,X1] : meet(a,join(X0,meet(a,X1))) = meet(a,join(X1,X0)),
    inference(forward_demodulation,[],[f20092,f247]) ).

fof(f20186,plain,
    ! [X0] : meet(a,join(X0,sF0)) = meet(a,join(X0,sF1)),
    inference(backward_demodulation,[],[f11190,f20114]) ).

fof(f20187,plain,
    ! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF1)),
    inference(backward_demodulation,[],[f11188,f20114]) ).

fof(f20188,plain,
    ! [X0] : meet(a,join(X0,sF4)) = meet(a,join(X0,sF1)),
    inference(backward_demodulation,[],[f11187,f20114]) ).

fof(f20207,plain,
    ! [X0] : meet(a,join(X0,sF4)) = join(sF1,meet(a,X0)),
    inference(backward_demodulation,[],[f9307,f20188]) ).

fof(f20210,plain,
    ! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF4)),
    inference(backward_demodulation,[],[f20188,f20187]) ).

fof(f20211,plain,
    ! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF0)),
    inference(backward_demodulation,[],[f20187,f20186]) ).

fof(f20269,plain,
    ! [X0] : meet(a,join(X0,sF2)) = join(sF1,meet(a,X0)),
    inference(backward_demodulation,[],[f20207,f20210]) ).

fof(f20310,plain,
    ! [X0] : meet(a,join(X0,sF0)) = join(sF1,meet(a,X0)),
    inference(forward_demodulation,[],[f20269,f20211]) ).

fof(f20402,plain,
    join(y2,meet(a,sF0)) = join(meet(a,x2),y2),
    inference(superposition,[],[f20035,f21]) ).

fof(f20406,plain,
    join(meet(a,y2),z2) = join(z2,meet(a,sF4)),
    inference(superposition,[],[f20035,f30]) ).

fof(f20409,plain,
    join(meet(a,z2),sF8) = join(sF8,meet(a,sF2)),
    inference(superposition,[],[f20035,f18068]) ).

fof(f20441,plain,
    join(meet(a,sF7),x2) = join(x2,meet(a,sF8)),
    inference(superposition,[],[f20035,f45]) ).

fof(f20449,plain,
    ! [X0,X1] : join(meet(a,X1),X0) = join(X0,meet(a,join(X0,X1))),
    inference(superposition,[],[f20035,f1654]) ).

fof(f20491,plain,
    ! [X2,X0,X1] : join(X2,meet(a,join(X0,meet(X1,X2)))) = join(X2,join(meet(a,X0),meet(X1,X2))),
    inference(superposition,[],[f284,f20035]) ).

fof(f20495,plain,
    ! [X0,X1] : join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,join(X0,meet(a,X1)))))) = meet(join(X1,meet(a,meet(a,join(X0,meet(a,X1))))),join(meet(a,X0),meet(a,X1))),
    inference(superposition,[],[f1834,f20035]) ).

fof(f20517,plain,
    ! [X0,X1] : join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,join(X0,meet(a,X1)))))) = meet(join(meet(a,X0),meet(a,X1)),join(meet(a,meet(a,join(X0,meet(a,X1)))),X1)),
    inference(forward_demodulation,[],[f20495,f1771]) ).

fof(f20521,plain,
    ! [X2,X0,X1] : join(X2,meet(a,X0)) = join(X2,meet(a,join(X0,meet(X1,X2)))),
    inference(forward_demodulation,[],[f20491,f3054]) ).

fof(f20568,plain,
    join(x2,meet(a,sF8)) = join(x2,meet(a,sF7)),
    inference(forward_demodulation,[],[f20441,f3]) ).

fof(f20586,plain,
    join(meet(a,z2),sF8) = join(sF8,meet(sF2,a)),
    inference(forward_demodulation,[],[f20409,f1]) ).

fof(f20589,plain,
    join(meet(a,y2),z2) = join(z2,meet(sF4,a)),
    inference(forward_demodulation,[],[f20406,f1]) ).

fof(f20593,plain,
    join(y2,meet(a,sF0)) = join(y2,meet(a,x2)),
    inference(forward_demodulation,[],[f20402,f3]) ).

fof(f20633,plain,
    ! [X0,X1] : join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,join(X0,meet(a,X1)))))) = meet(join(meet(a,X0),meet(a,X1)),join(X1,meet(a,meet(a,join(X0,meet(a,X1)))))),
    inference(forward_demodulation,[],[f20517,f1654]) ).

fof(f20677,plain,
    join(x2,meet(a,sF8)) = join(x2,meet(sF7,a)),
    inference(forward_demodulation,[],[f20568,f1]) ).

fof(f20695,plain,
    join(sF8,sF1) = join(meet(a,z2),sF8),
    inference(forward_demodulation,[],[f20586,f47]) ).

fof(f20698,plain,
    join(z2,sF1) = join(meet(a,y2),z2),
    inference(forward_demodulation,[],[f20589,f48]) ).

fof(f20702,plain,
    join(y2,meet(sF0,a)) = join(y2,meet(a,x2)),
    inference(forward_demodulation,[],[f20593,f1]) ).

fof(f20737,plain,
    ! [X0,X1] : join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,join(X0,meet(a,X1)))))) = meet(join(meet(a,X0),meet(a,X1)),join(X1,meet(a,join(X0,meet(a,X1))))),
    inference(forward_demodulation,[],[f20633,f433]) ).

fof(f20779,plain,
    join(sF8,sF1) = join(sF8,meet(a,z2)),
    inference(forward_demodulation,[],[f20695,f3]) ).

fof(f20782,plain,
    join(z2,sF1) = join(z2,meet(a,y2)),
    inference(forward_demodulation,[],[f20698,f3]) ).

fof(f20784,plain,
    join(y2,sF1) = join(y2,meet(a,x2)),
    inference(forward_demodulation,[],[f20702,f42]) ).

fof(f20813,plain,
    ! [X0,X1] : join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,X0)))) = meet(join(meet(a,X0),meet(a,X1)),join(X1,meet(a,X0))),
    inference(forward_demodulation,[],[f20737,f20521]) ).

fof(f20861,plain,
    join(sF1,sF8) = join(sF8,meet(a,z2)),
    inference(forward_demodulation,[],[f20779,f3]) ).

fof(f20884,plain,
    ! [X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X1),meet(a,X0))) = join(meet(X1,meet(a,join(X0,meet(a,X1)))),meet(a,join(X1,meet(a,X0)))),
    inference(forward_demodulation,[],[f20813,f1771]) ).

fof(f20928,plain,
    ! [X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X1),meet(a,X0))) = join(meet(a,join(X1,meet(a,X0))),meet(X1,meet(a,join(X0,meet(a,X1))))),
    inference(forward_demodulation,[],[f20884,f3]) ).

fof(f20947,plain,
    ! [X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X1),meet(a,X0))) = join(meet(a,join(X1,meet(a,X0))),meet(a,X1)),
    inference(forward_demodulation,[],[f20928,f3332]) ).

fof(f20965,plain,
    ! [X0,X1] : join(meet(a,X1),meet(a,join(X1,meet(a,X0)))) = meet(join(X1,meet(a,X0)),join(meet(a,X1),meet(a,X0))),
    inference(forward_demodulation,[],[f20947,f3]) ).

fof(f20976,plain,
    ! [X0,X1] : join(meet(a,X1),meet(a,join(X1,meet(a,X0)))) = join(meet(a,X0),meet(a,X1)),
    inference(forward_demodulation,[],[f20965,f1993]) ).

fof(f20979,plain,
    ! [X0,X1] : join(meet(a,X0),meet(a,X1)) = meet(join(meet(a,X1),a),join(X1,meet(a,X0))),
    inference(forward_demodulation,[],[f20976,f2158]) ).

fof(f20982,plain,
    ! [X0,X1] : join(meet(a,X0),meet(a,X1)) = meet(join(a,meet(a,X1)),join(X1,meet(a,X0))),
    inference(forward_demodulation,[],[f20979,f13785]) ).

fof(f20984,plain,
    ! [X0,X1] : meet(a,join(X1,meet(a,X0))) = join(meet(a,X0),meet(a,X1)),
    inference(forward_demodulation,[],[f20982,f5]) ).

fof(f20986,plain,
    ! [X0,X1] : meet(a,join(X0,X1)) = join(meet(a,X0),meet(a,X1)),
    inference(forward_demodulation,[],[f20984,f20114]) ).

fof(f21007,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(X1,meet(a,join(meet(X2,X0),meet(X2,join(X0,X1))))),
    inference(backward_demodulation,[],[f5078,f20986]) ).

fof(f21153,plain,
    ! [X0,X1] : join(meet(X0,join(X1,X0)),meet(a,join(X0,join(X1,X0)))) = meet(join(X0,meet(a,X1)),join(meet(a,X0),join(X1,X0))),
    inference(superposition,[],[f1834,f19827]) ).

fof(f21222,plain,
    ! [X0,X1] : join(meet(X0,join(X1,X0)),meet(a,join(X0,join(X1,X0)))) = meet(join(X0,meet(a,X1)),join(X0,join(meet(a,X0),X1))),
    inference(forward_demodulation,[],[f21153,f1721]) ).

fof(f21324,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X0,X1)) = join(meet(X0,join(X1,X0)),meet(a,join(X0,join(X1,X0)))),
    inference(forward_demodulation,[],[f21222,f284]) ).

fof(f21406,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X0,X1)) = join(meet(X0,join(X1,X0)),meet(a,join(X0,X1))),
    inference(forward_demodulation,[],[f21324,f272]) ).

fof(f21488,plain,
    ! [X0,X1] : meet(join(X0,meet(a,X1)),join(X0,X1)) = join(X0,meet(a,join(X0,X1))),
    inference(forward_demodulation,[],[f21406,f128]) ).

fof(f21542,plain,
    ! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,meet(a,X1)),join(X0,X1)),
    inference(forward_demodulation,[],[f21488,f20449]) ).

fof(f21580,plain,
    ! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,X1),join(meet(a,X1),X0)),
    inference(forward_demodulation,[],[f21542,f1771]) ).

fof(f21652,plain,
    join(meet(a,y2),x2) = join(x2,meet(a,sF0)),
    inference(superposition,[],[f20449,f21]) ).

fof(f21656,plain,
    join(meet(a,z2),y2) = join(y2,meet(a,sF4)),
    inference(superposition,[],[f20449,f30]) ).

fof(f21659,plain,
    join(z2,meet(a,sF2)) = join(meet(a,sF8),z2),
    inference(superposition,[],[f20449,f18068]) ).

fof(f21667,plain,
    ! [X0] : join(meet(a,meet(a,X0)),sF1) = join(sF1,meet(a,meet(a,join(sF1,X0)))),
    inference(superposition,[],[f20449,f2455]) ).

fof(f21670,plain,
    ! [X0] : join(sF1,meet(a,meet(a,join(sF1,X0)))) = join(meet(a,meet(X0,a)),sF1),
    inference(superposition,[],[f20449,f2535]) ).

fof(f21691,plain,
    join(meet(a,x2),sF7) = join(sF7,meet(a,sF8)),
    inference(superposition,[],[f20449,f45]) ).

fof(f21811,plain,
    join(sF7,meet(a,sF8)) = join(sF7,meet(a,x2)),
    inference(forward_demodulation,[],[f21691,f3]) ).

fof(f21831,plain,
    ! [X0] : join(sF1,meet(a,meet(X0,a))) = join(sF1,meet(a,meet(a,join(sF1,X0)))),
    inference(forward_demodulation,[],[f21670,f3]) ).

fof(f21834,plain,
    ! [X0] : join(meet(a,meet(a,X0)),sF1) = meet(a,join(sF1,meet(a,join(sF1,X0)))),
    inference(forward_demodulation,[],[f21667,f2455]) ).

fof(f21842,plain,
    join(z2,meet(a,sF2)) = join(z2,meet(a,sF8)),
    inference(forward_demodulation,[],[f21659,f3]) ).

fof(f21845,plain,
    join(meet(a,z2),y2) = join(y2,meet(sF4,a)),
    inference(forward_demodulation,[],[f21656,f1]) ).

fof(f21847,plain,
    join(meet(a,y2),x2) = join(x2,meet(sF0,a)),
    inference(forward_demodulation,[],[f21652,f1]) ).

fof(f21949,plain,
    ! [X0] : join(sF1,meet(a,meet(X0,a))) = meet(a,join(sF1,meet(a,join(sF1,X0)))),
    inference(forward_demodulation,[],[f21831,f2455]) ).

fof(f21952,plain,
    ! [X0] : join(meet(a,meet(a,X0)),sF1) = meet(a,join(join(sF1,X0),sF1)),
    inference(forward_demodulation,[],[f21834,f20114]) ).

fof(f21960,plain,
    join(z2,meet(sF2,a)) = join(z2,meet(a,sF8)),
    inference(forward_demodulation,[],[f21842,f1]) ).

fof(f21962,plain,
    join(y2,sF1) = join(meet(a,z2),y2),
    inference(forward_demodulation,[],[f21845,f48]) ).

fof(f21964,plain,
    join(x2,sF1) = join(meet(a,y2),x2),
    inference(forward_demodulation,[],[f21847,f42]) ).

fof(f22038,plain,
    ! [X0] : join(sF1,meet(a,meet(X0,a))) = meet(a,join(join(sF1,X0),sF1)),
    inference(forward_demodulation,[],[f21949,f20114]) ).

fof(f22041,plain,
    ! [X0] : join(meet(a,meet(a,X0)),sF1) = meet(a,join(join(sF1,X0),sF0)),
    inference(forward_demodulation,[],[f21952,f20186]) ).

fof(f22045,plain,
    join(z2,sF1) = join(z2,meet(a,sF8)),
    inference(forward_demodulation,[],[f21960,f47]) ).

fof(f22047,plain,
    join(y2,sF1) = join(y2,meet(a,z2)),
    inference(forward_demodulation,[],[f21962,f3]) ).

fof(f22049,plain,
    join(x2,sF1) = join(x2,meet(a,y2)),
    inference(forward_demodulation,[],[f21964,f3]) ).

fof(f22104,plain,
    ! [X0] : join(sF1,meet(a,meet(X0,a))) = meet(a,join(join(sF1,X0),sF0)),
    inference(forward_demodulation,[],[f22038,f20186]) ).

fof(f22107,plain,
    ! [X0] : join(meet(a,meet(a,X0)),sF1) = meet(a,join(sF0,join(sF1,X0))),
    inference(forward_demodulation,[],[f22041,f1654]) ).

fof(f22153,plain,
    ! [X0] : join(sF1,meet(a,meet(X0,a))) = meet(a,join(sF0,join(sF1,X0))),
    inference(forward_demodulation,[],[f22104,f1654]) ).

fof(f22156,plain,
    ! [X0] : meet(a,join(sF0,X0)) = join(meet(a,meet(a,X0)),sF1),
    inference(forward_demodulation,[],[f22107,f388]) ).

fof(f22191,plain,
    ! [X0] : meet(a,join(sF0,X0)) = join(sF1,meet(a,meet(X0,a))),
    inference(forward_demodulation,[],[f22153,f388]) ).

fof(f22194,plain,
    ! [X0] : meet(a,join(sF0,X0)) = join(sF1,meet(a,meet(a,X0))),
    inference(forward_demodulation,[],[f22156,f3]) ).

fof(f22219,plain,
    ! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF1,meet(X0,a))),
    inference(forward_demodulation,[],[f22191,f2455]) ).

fof(f22222,plain,
    ! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF1,meet(a,X0))),
    inference(forward_demodulation,[],[f22194,f2455]) ).

fof(f22241,plain,
    ! [X0] : meet(a,join(sF0,X0)) = meet(a,meet(a,join(sF1,X0))),
    inference(forward_demodulation,[],[f22219,f2535]) ).

fof(f22244,plain,
    ! [X0] : meet(a,join(sF0,X0)) = meet(a,join(X0,sF1)),
    inference(forward_demodulation,[],[f22222,f20114]) ).

fof(f22257,plain,
    ! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF1,X0)),
    inference(forward_demodulation,[],[f22241,f433]) ).

fof(f22276,plain,
    ! [X0,X1] : join(sF1,join(meet(a,X0),X1)) = join(meet(a,join(sF0,X0)),X1),
    inference(backward_demodulation,[],[f2553,f22257]) ).

fof(f22992,plain,
    ! [X0] : meet(meet(a,sF8),X0) = meet(meet(a,sF8),meet(join(x2,meet(sF7,a)),X0)),
    inference(superposition,[],[f317,f20677]) ).

fof(f23011,plain,
    ! [X0] : meet(meet(a,sF8),X0) = meet(a,meet(sF8,meet(join(x2,meet(sF7,a)),X0))),
    inference(forward_demodulation,[],[f22992,f2]) ).

fof(f23037,plain,
    ! [X0] : meet(a,meet(sF8,meet(join(x2,meet(sF7,a)),X0))) = meet(a,meet(sF8,X0)),
    inference(forward_demodulation,[],[f23011,f2]) ).

fof(f23100,plain,
    ! [X0] : meet(X0,join(y2,z2)) = join(meet(X0,join(z2,sF1)),meet(X0,join(y2,meet(a,z2)))),
    inference(superposition,[],[f191,f20782]) ).

fof(f23108,plain,
    join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(meet(a,z2),y2)),
    inference(superposition,[],[f1834,f20782]) ).

fof(f23143,plain,
    join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(y2,meet(a,z2))),
    inference(forward_demodulation,[],[f23108,f1654]) ).

fof(f23151,plain,
    ! [X0] : meet(X0,join(y2,z2)) = join(meet(X0,join(z2,sF1)),meet(X0,join(y2,sF1))),
    inference(forward_demodulation,[],[f23100,f22047]) ).

fof(f23169,plain,
    join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(y2,sF1)),
    inference(forward_demodulation,[],[f23143,f22047]) ).

fof(f23177,plain,
    ! [X0] : meet(X0,join(y2,z2)) = join(meet(X0,join(y2,sF1)),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f23151,f3]) ).

fof(f23188,plain,
    join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(y2,sF1),join(sF1,z2)),
    inference(forward_demodulation,[],[f23169,f1771]) ).

fof(f23196,plain,
    ! [X0] : meet(X0,sF4) = join(meet(X0,join(y2,sF1)),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f23177,f30]) ).

fof(f23205,plain,
    join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(y2,sF1),join(z2,sF1)),
    inference(forward_demodulation,[],[f23188,f1654]) ).

fof(f23216,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(meet(y2,z2),meet(a,join(y2,z2))),
    inference(forward_demodulation,[],[f23205,f495]) ).

fof(f23224,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(meet(y2,z2),meet(a,sF4)),
    inference(forward_demodulation,[],[f23216,f30]) ).

fof(f23228,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(meet(a,sF4),meet(y2,z2)),
    inference(forward_demodulation,[],[f23224,f3]) ).

fof(f23231,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(meet(a,sF4),sF7),
    inference(forward_demodulation,[],[f23228,f37]) ).

fof(f23234,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(sF7,meet(a,sF4)),
    inference(forward_demodulation,[],[f23231,f3]) ).

fof(f23237,plain,
    meet(join(y2,sF1),join(z2,sF1)) = join(sF7,meet(sF4,a)),
    inference(forward_demodulation,[],[f23234,f1]) ).

fof(f23240,plain,
    join(sF7,sF1) = meet(join(y2,sF1),join(z2,sF1)),
    inference(forward_demodulation,[],[f23237,f48]) ).

fof(f23250,plain,
    ! [X0] : meet(X0,join(x2,y2)) = join(meet(X0,join(x2,sF1)),meet(join(y2,meet(a,x2)),X0)),
    inference(superposition,[],[f243,f22049]) ).

fof(f23295,plain,
    ! [X0] : meet(X0,join(x2,y2)) = join(meet(X0,join(x2,sF1)),meet(join(y2,sF1),X0)),
    inference(forward_demodulation,[],[f23250,f20784]) ).

fof(f23319,plain,
    ! [X0] : meet(X0,sF0) = join(meet(X0,join(x2,sF1)),meet(join(y2,sF1),X0)),
    inference(forward_demodulation,[],[f23295,f21]) ).

fof(f23739,plain,
    ! [X0] : meet(X0,join(sF8,z2)) = join(meet(join(sF1,sF8),X0),meet(X0,join(z2,meet(a,sF8)))),
    inference(superposition,[],[f244,f20861]) ).

fof(f23782,plain,
    ! [X0] : meet(X0,join(sF8,z2)) = join(meet(join(sF1,sF8),X0),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f23739,f22045]) ).

fof(f23804,plain,
    ! [X0] : meet(X0,join(z2,sF8)) = join(meet(join(sF1,sF8),X0),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f23782,f1654]) ).

fof(f23821,plain,
    ! [X0] : meet(X0,sF2) = join(meet(join(sF1,sF8),X0),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f23804,f18068]) ).

fof(f24241,plain,
    ! [X2,X0,X1] : join(X1,join(sF1,join(meet(a,X0),meet(X1,X2)))) = join(X1,meet(a,join(sF0,X0))),
    inference(superposition,[],[f396,f22276]) ).

fof(f24279,plain,
    ! [X0,X1] : join(X1,join(sF1,meet(a,X0))) = join(X1,meet(a,join(sF0,X0))),
    inference(forward_demodulation,[],[f24241,f1502]) ).

fof(f24381,plain,
    ! [X0,X1] : join(X1,meet(a,join(sF0,X0))) = join(X1,meet(a,join(X0,sF0))),
    inference(forward_demodulation,[],[f24279,f20310]) ).

fof(f25565,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(meet(join(X1,X0),join(X0,meet(a,X1))),join(meet(a,X0),X1)),
    inference(superposition,[],[f186,f21580]) ).

fof(f25634,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(join(meet(a,X0),X1),meet(join(X1,X0),join(X0,meet(a,X1)))),
    inference(forward_demodulation,[],[f25565,f3]) ).

fof(f25800,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(meet(a,X0),join(X1,meet(join(X1,X0),join(X0,meet(a,X1))))),
    inference(forward_demodulation,[],[f25634,f4]) ).

fof(f25939,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(meet(a,X0),join(X1,join(meet(a,X1),X0))),
    inference(forward_demodulation,[],[f25800,f3631]) ).

fof(f26047,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(X0,join(meet(a,X0),join(X1,meet(a,X1)))),
    inference(forward_demodulation,[],[f25939,f1439]) ).

fof(f26134,plain,
    ! [X0,X1] : meet(join(X1,X0),join(X0,X1)) = join(X0,join(X1,meet(a,X1))),
    inference(forward_demodulation,[],[f26047,f284]) ).

fof(f26204,plain,
    ! [X0,X1] : join(X0,X1) = meet(join(X1,X0),join(X0,X1)),
    inference(forward_demodulation,[],[f26134,f240]) ).

fof(f34330,plain,
    ! [X0,X1] : join(meet(X0,a),X1) = meet(join(X1,meet(a,X0)),join(meet(X0,a),X1)),
    inference(superposition,[],[f21580,f2022]) ).

fof(f35018,plain,
    ! [X2,X3,X0,X1,X4] : meet(join(X0,X1),meet(join(X2,X3),X4)) = meet(X4,meet(join(X3,X2),join(X1,X0))),
    inference(superposition,[],[f1571,f1652]) ).

fof(f36472,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(join(X1,X0),meet(a,X0))),join(meet(X2,join(X0,meet(a,X1))),X3)),
    inference(superposition,[],[f287,f19827]) ).

fof(f36550,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X2,X1)),join(meet(X0,join(X2,meet(a,X1))),X3)) = join(meet(X0,join(X2,meet(a,X1))),join(meet(X0,join(X1,X2)),X3)),
    inference(superposition,[],[f287,f287]) ).

fof(f36560,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X2,meet(a,X1))),join(meet(X0,join(X1,meet(a,X2))),X3)) = join(meet(X0,join(X2,X1)),join(X3,meet(X0,join(X1,meet(a,X2))))),
    inference(superposition,[],[f287,f272]) ).

fof(f36670,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X2,X1)),X3) = join(meet(X0,join(X2,X1)),join(X3,meet(X0,join(X1,meet(a,X2))))),
    inference(forward_demodulation,[],[f36560,f287]) ).

fof(f36678,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X2,X1)),join(meet(X0,join(X2,meet(a,X1))),X3)) = join(meet(X0,join(X1,X2)),join(X3,meet(X0,join(X2,meet(a,X1))))),
    inference(forward_demodulation,[],[f36550,f303]) ).

fof(f36747,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(join(X1,X0),meet(a,X0))))),
    inference(forward_demodulation,[],[f36472,f303]) ).

fof(f36882,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(meet(X0,join(X2,X1)),join(meet(X0,join(X2,meet(a,X1))),X3)),
    inference(forward_demodulation,[],[f36678,f36670]) ).

fof(f36948,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(meet(a,X0),join(X1,X0))))),
    inference(forward_demodulation,[],[f36747,f1654]) ).

fof(f37097,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(X0,join(meet(a,X0),X1))))),
    inference(forward_demodulation,[],[f36948,f1721]) ).

fof(f37201,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(X0,X1)))),
    inference(forward_demodulation,[],[f37097,f284]) ).

fof(f37277,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(join(X1,X0),X0)),X3) = join(meet(X2,join(X0,X1)),join(meet(X2,join(X0,meet(a,X1))),X3)),
    inference(forward_demodulation,[],[f37201,f303]) ).

fof(f37319,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(X1,X0)),X3) = join(meet(X2,join(join(X1,X0),X0)),X3),
    inference(forward_demodulation,[],[f37277,f36882]) ).

fof(f37356,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(X1,X0)),X3) = join(meet(X2,join(X0,join(X1,X0))),X3),
    inference(forward_demodulation,[],[f37319,f1654]) ).

fof(f37386,plain,
    ! [X2,X3,X0,X1] : join(meet(X2,join(X0,X1)),X3) = join(meet(X2,join(X1,X0)),X3),
    inference(forward_demodulation,[],[f37356,f272]) ).

fof(f37809,plain,
    meet(y2,join(z2,sF1)) = meet(y2,join(sF7,sF1)),
    inference(superposition,[],[f316,f23240]) ).

fof(f45262,plain,
    ! [X2,X3,X0,X1] : meet(join(meet(a,meet(a,X0)),X3),meet(join(meet(a,X0),X1),join(X0,X2))) = meet(join(X3,meet(a,meet(a,X0))),meet(join(meet(a,X0),X1),join(X0,X2))),
    inference(superposition,[],[f13785,f2128]) ).

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

fof(f46737,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(join(z2,sF1),meet(a,meet(a,join(y2,sF1)))),X0)),
    inference(superposition,[],[f243,f23196]) ).

fof(f46746,plain,
    ! [X0] : join(join(z2,sF1),meet(X0,sF4)) = join(join(z2,sF1),meet(X0,join(y2,sF1))),
    inference(superposition,[],[f3054,f23196]) ).

fof(f46805,plain,
    ! [X0] : join(join(z2,sF1),meet(X0,sF4)) = join(z2,join(sF1,meet(X0,join(y2,sF1)))),
    inference(forward_demodulation,[],[f46746,f4]) ).

fof(f46814,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,join(sF1,meet(a,meet(a,join(y2,sF1))))),X0)),
    inference(forward_demodulation,[],[f46737,f4]) ).

fof(f46863,plain,
    ! [X0] : join(z2,join(sF1,meet(X0,sF4))) = join(z2,join(sF1,meet(X0,join(y2,sF1)))),
    inference(forward_demodulation,[],[f46805,f4]) ).

fof(f46872,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(meet(a,join(y2,sF1)),sF0))),X0)),
    inference(forward_demodulation,[],[f46814,f20310]) ).

fof(f46914,plain,
    ! [X0] : join(z2,meet(sF4,join(X0,sF1))) = join(z2,join(sF1,meet(X0,join(y2,sF1)))),
    inference(forward_demodulation,[],[f46863,f5596]) ).

fof(f46923,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(sF0,meet(a,join(y2,sF1))))),X0)),
    inference(forward_demodulation,[],[f46872,f24381]) ).

fof(f46967,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(join(y2,sF1),sF0))),X0)),
    inference(forward_demodulation,[],[f46923,f20114]) ).

fof(f47002,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(sF0,join(y2,sF1)))),X0)),
    inference(forward_demodulation,[],[f46967,f24381]) ).

fof(f47032,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(sF0,sF1))),X0)),
    inference(forward_demodulation,[],[f47002,f1941]) ).

fof(f47055,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,join(sF0,sF0))),X0)),
    inference(forward_demodulation,[],[f47032,f20186]) ).

fof(f47077,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(a,sF0)),X0)),
    inference(forward_demodulation,[],[f47055,f98]) ).

fof(f47096,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,meet(sF0,a)),X0)),
    inference(forward_demodulation,[],[f47077,f1]) ).

fof(f47115,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(a,sF4)),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47096,f42]) ).

fof(f47134,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,meet(sF4,a)),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47115,f3166]) ).

fof(f47152,plain,
    ! [X0] : meet(X0,join(meet(a,join(y2,sF1)),join(z2,sF1))) = join(meet(X0,sF1),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47134,f48]) ).

fof(f47170,plain,
    ! [X0] : meet(X0,join(z2,join(sF1,meet(a,join(y2,sF1))))) = join(meet(X0,sF1),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47152,f1721]) ).

fof(f47188,plain,
    ! [X0] : meet(X0,join(z2,meet(sF4,join(a,sF1)))) = join(meet(X0,sF1),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47170,f46914]) ).

fof(f47206,plain,
    ! [X0] : meet(X0,join(z2,meet(sF4,a))) = join(meet(X0,sF1),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47188,f257]) ).

fof(f47223,plain,
    ! [X0] : meet(X0,join(z2,sF1)) = join(meet(X0,sF1),meet(join(z2,sF1),X0)),
    inference(forward_demodulation,[],[f47206,f48]) ).

fof(f47419,plain,
    ! [X0,X1] : join(X1,meet(X0,join(z2,sF1))) = join(meet(X0,sF1),join(meet(join(z2,sF1),X0),X1)),
    inference(superposition,[],[f303,f47223]) ).

fof(f51660,plain,
    ! [X0] : meet(a,sF8) = meet(meet(a,sF8),join(X0,join(x2,meet(sF7,a)))),
    inference(superposition,[],[f301,f20677]) ).

fof(f52025,plain,
    ! [X0] : meet(a,sF8) = meet(a,meet(sF8,join(X0,join(x2,meet(sF7,a))))),
    inference(forward_demodulation,[],[f51660,f2]) ).

fof(f65031,plain,
    ! [X2,X3,X0,X1,X4] : meet(X2,meet(X3,join(meet(X1,X0),join(meet(X0,X1),X4)))) = meet(X2,meet(X3,join(X4,meet(X0,X1)))),
    inference(superposition,[],[f1567,f1168]) ).

fof(f66277,plain,
    ! [X2,X3,X0,X1,X4] : meet(X2,meet(X3,join(X4,meet(X0,X1)))) = meet(X2,meet(X3,join(meet(X1,X0),X4))),
    inference(forward_demodulation,[],[f65031,f3757]) ).

fof(f72924,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(meet(join(X2,X0),X1),meet(a,X0)),meet(join(meet(a,X0),X1),join(X0,X2))),
    inference(superposition,[],[f26204,f2128]) ).

fof(f73363,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(meet(a,X0),meet(join(X2,X0),X1)),meet(join(meet(a,X0),X1),join(X0,X2))),
    inference(forward_demodulation,[],[f72924,f45640]) ).

fof(f73714,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(X0,X2),meet(join(X1,meet(a,X0)),join(meet(join(X2,X0),X1),meet(a,X0)))),
    inference(forward_demodulation,[],[f73363,f35018]) ).

fof(f73995,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(X0,X2),meet(join(X1,meet(a,X0)),join(meet(X0,a),meet(join(X2,X0),X1)))),
    inference(forward_demodulation,[],[f73714,f66277]) ).

fof(f74200,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(X0,X2),meet(join(X1,meet(a,X0)),meet(join(meet(X0,a),X1),join(X0,X2)))),
    inference(forward_demodulation,[],[f73995,f8932]) ).

fof(f74343,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(X0,X2),meet(join(X1,meet(a,X0)),join(meet(X0,a),X1))),
    inference(forward_demodulation,[],[f74200,f3726]) ).

fof(f74400,plain,
    ! [X2,X0,X1] : meet(join(meet(a,X0),X1),join(X0,X2)) = meet(join(X0,X2),join(meet(X0,a),X1)),
    inference(forward_demodulation,[],[f74343,f34330]) ).

fof(f74779,plain,
    meet(sF2,sF0) = join(join(x2,sF1),meet(join(y2,sF1),sF2)),
    inference(superposition,[],[f23319,f6618]) ).

fof(f74958,plain,
    meet(sF2,sF0) = join(x2,join(sF1,meet(join(y2,sF1),sF2))),
    inference(forward_demodulation,[],[f74779,f4]) ).

fof(f75033,plain,
    meet(sF2,sF0) = join(x2,meet(sF2,join(join(y2,sF1),sF1))),
    inference(forward_demodulation,[],[f74958,f5597]) ).

fof(f75096,plain,
    meet(sF2,sF0) = join(x2,meet(sF2,join(sF1,join(y2,sF1)))),
    inference(forward_demodulation,[],[f75033,f1654]) ).

fof(f75155,plain,
    meet(sF2,sF0) = join(x2,meet(sF2,join(y2,join(sF1,sF1)))),
    inference(forward_demodulation,[],[f75096,f1721]) ).

fof(f75199,plain,
    meet(sF2,sF0) = join(x2,meet(sF2,join(y2,sF1))),
    inference(forward_demodulation,[],[f75155,f98]) ).

fof(f75231,plain,
    meet(sF0,sF2) = join(x2,meet(sF2,join(y2,sF1))),
    inference(forward_demodulation,[],[f75199,f1]) ).

fof(f75258,plain,
    sF6 = join(x2,meet(sF2,join(y2,sF1))),
    inference(forward_demodulation,[],[f75231,f35]) ).

fof(f75363,plain,
    join(sF7,sF6) = join(sF8,meet(sF2,join(y2,sF1))),
    inference(superposition,[],[f292,f75258]) ).

fof(f75437,plain,
    join(sF7,sF6) = join(sF1,join(sF8,meet(sF2,y2))),
    inference(forward_demodulation,[],[f75363,f6717]) ).

fof(f75464,plain,
    sF6 = join(sF1,join(sF8,meet(sF2,y2))),
    inference(forward_demodulation,[],[f75437,f16229]) ).

fof(f80563,plain,
    ! [X0] : join(meet(sF7,X0),x2) = meet(sF8,join(meet(sF7,X0),x2)),
    inference(superposition,[],[f408,f45]) ).

fof(f80999,plain,
    ! [X0] : join(meet(sF7,X0),x2) = meet(sF8,join(x2,meet(sF7,X0))),
    inference(forward_demodulation,[],[f80563,f1654]) ).

fof(f81239,plain,
    ! [X0] : join(x2,meet(sF7,X0)) = meet(sF8,join(x2,meet(sF7,X0))),
    inference(forward_demodulation,[],[f80999,f3]) ).

fof(f81994,plain,
    ! [X0,X1] : meet(X1,join(x2,meet(sF7,X0))) = meet(sF8,meet(join(x2,meet(sF7,X0)),X1)),
    inference(superposition,[],[f332,f81239]) ).

fof(f82017,plain,
    ! [X0] : meet(a,meet(sF8,X0)) = meet(a,meet(X0,join(x2,meet(sF7,a)))),
    inference(backward_demodulation,[],[f23037,f81994]) ).

fof(f85322,plain,
    ! [X0] : meet(X0,join(sF7,sF8)) = join(meet(X0,join(sF7,meet(a,x2))),meet(X0,join(sF8,meet(sF7,a)))),
    inference(superposition,[],[f246,f21811]) ).

fof(f85410,plain,
    ! [X0] : meet(X0,join(sF7,sF8)) = join(meet(X0,join(sF7,meet(a,x2))),meet(X0,sF8)),
    inference(forward_demodulation,[],[f85322,f13720]) ).

fof(f85458,plain,
    ! [X0] : meet(X0,join(sF7,sF8)) = join(meet(X0,sF8),meet(X0,join(sF7,meet(a,x2)))),
    inference(forward_demodulation,[],[f85410,f3]) ).

fof(f85492,plain,
    ! [X0] : meet(X0,sF8) = join(meet(X0,sF8),meet(X0,join(sF7,meet(a,x2)))),
    inference(forward_demodulation,[],[f85458,f2621]) ).

fof(f86098,plain,
    ! [X2,X3,X0,X1] : join(meet(join(X2,X1),X0),X3) = join(meet(join(X2,X1),X0),join(X3,meet(X0,X1))),
    inference(superposition,[],[f3054,f2031]) ).

fof(f86301,plain,
    ! [X2,X3,X0,X1] : join(meet(join(X2,X1),X0),X3) = join(meet(X0,X1),join(meet(join(X2,X1),X0),X3)),
    inference(forward_demodulation,[],[f86098,f303]) ).

fof(f86607,plain,
    ! [X0,X1] : join(X1,meet(X0,join(z2,sF1))) = join(meet(join(z2,sF1),X0),X1),
    inference(backward_demodulation,[],[f47419,f86301]) ).

fof(f86789,plain,
    ! [X0] : meet(X0,sF2) = join(meet(join(z2,sF1),X0),meet(join(sF1,sF8),X0)),
    inference(backward_demodulation,[],[f23821,f86607]) ).

fof(f97012,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(join(meet(a,X0),X1),meet(join(meet(a,X0),X1),join(meet(a,X1),X0))),
    inference(superposition,[],[f193,f1957]) ).

fof(f97135,plain,
    ! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(meet(a,X0),join(X1,meet(join(meet(a,X0),X1),join(meet(a,X1),X0)))),
    inference(forward_demodulation,[],[f97012,f4]) ).

fof(f97540,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = meet(join(meet(a,X0),X1),join(X0,X1)),
    inference(forward_demodulation,[],[f97135,f297]) ).

fof(f97885,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = meet(join(X0,X1),join(meet(X0,a),X1)),
    inference(forward_demodulation,[],[f97540,f74400]) ).

fof(f98148,plain,
    ! [X0,X1] : join(meet(a,X0),X1) = join(meet(X0,a),X1),
    inference(forward_demodulation,[],[f97885,f408]) ).

fof(f98822,plain,
    ! [X0,X1] : join(X1,meet(X0,a)) = join(meet(a,X0),join(X1,meet(X0,a))),
    inference(superposition,[],[f1888,f98148]) ).

fof(f98899,plain,
    ! [X0,X1] : join(X1,meet(a,X0)) = join(X1,meet(X0,a)),
    inference(forward_demodulation,[],[f98822,f11445]) ).

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

fof(f129802,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X3) = join(X3,meet(X0,join(X2,X1))),
    inference(superposition,[],[f3,f37386]) ).

fof(f131725,plain,
    ! [X2,X0,X1] : join(X2,join(X0,X1)) = join(meet(join(X1,X0),join(X1,X0)),X2),
    inference(superposition,[],[f129802,f26204]) ).

fof(f132297,plain,
    ! [X2,X0,X1] : join(join(X1,X0),X2) = join(X2,join(X0,X1)),
    inference(forward_demodulation,[],[f131725,f97]) ).

fof(f133558,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X0,X1),meet(X1,X0))),
    inference(superposition,[],[f132297,f1168]) ).

fof(f134026,plain,
    ! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
    inference(superposition,[],[f3,f132297]) ).

fof(f134866,plain,
    ! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,X0)),
    inference(forward_demodulation,[],[f133558,f1168]) ).

fof(f135700,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X0,X1),meet(X1,X0))),
    inference(superposition,[],[f134026,f1168]) ).

fof(f136390,plain,
    ! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
    inference(forward_demodulation,[],[f135700,f1168]) ).

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

fof(f137289,plain,
    ! [X2,X3,X0,X1,X4] : join(meet(X0,X1),meet(X2,join(X3,X4))) = join(meet(X2,join(X4,X3)),meet(X1,X0)),
    inference(superposition,[],[f37386,f134866]) ).

fof(f138802,plain,
    ! [X2,X3,X0,X1] : join(meet(X0,X1),meet(X2,X3)) = join(meet(X3,X2),meet(X1,X0)),
    inference(superposition,[],[f134866,f137169]) ).

fof(f139261,plain,
    ! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X2,meet(X0,X1))),
    inference(superposition,[],[f136390,f2]) ).

fof(f163151,plain,
    ! [X0,X1] : meet(a,meet(X1,join(sF0,X0))) = meet(a,meet(X1,meet(a,join(X0,sF1)))),
    inference(superposition,[],[f3203,f22244]) ).

fof(f163699,plain,
    ! [X0,X1] : meet(a,meet(X1,join(X0,sF1))) = meet(a,meet(X1,join(sF0,X0))),
    inference(forward_demodulation,[],[f163151,f3203]) ).

fof(f190936,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,X0)),meet(X0,X1)),
    inference(superposition,[],[f1617,f447]) ).

fof(f191199,plain,
    ! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,X0),meet(X1,join(X0,X2))),
    inference(forward_demodulation,[],[f190936,f137289]) ).

fof(f191916,plain,
    ! [X2,X0,X1] : join(X1,meet(a,meet(X2,X0))) = join(X1,meet(a,meet(X2,join(X1,X0)))),
    inference(backward_demodulation,[],[f21007,f191199]) ).

fof(f196522,plain,
    ! [X0] : join(x2,meet(a,meet(X0,sF2))) = join(x2,meet(a,meet(X0,z2))),
    inference(superposition,[],[f191916,f25]) ).

fof(f197288,plain,
    ! [X0] : join(x2,meet(a,meet(X0,z2))) = join(x2,meet(sF2,meet(a,X0))),
    inference(forward_demodulation,[],[f196522,f139261]) ).

fof(f197688,plain,
    ! [X0] : join(x2,meet(sF1,X0)) = join(x2,meet(a,meet(X0,z2))),
    inference(forward_demodulation,[],[f197288,f325]) ).

fof(f201560,plain,
    join(x2,meet(a,sF7)) = join(x2,meet(sF1,y2)),
    inference(superposition,[],[f197688,f37]) ).

fof(f201746,plain,
    join(x2,meet(a,sF7)) = join(x2,meet(y2,sF1)),
    inference(forward_demodulation,[],[f201560,f136390]) ).

fof(f201819,plain,
    join(x2,meet(a,y2)) = join(x2,meet(a,sF7)),
    inference(forward_demodulation,[],[f201746,f15157]) ).

fof(f201860,plain,
    join(x2,meet(a,y2)) = join(x2,meet(sF7,a)),
    inference(forward_demodulation,[],[f201819,f98899]) ).

fof(f201885,plain,
    join(x2,sF1) = join(x2,meet(sF7,a)),
    inference(forward_demodulation,[],[f201860,f22049]) ).

fof(f201911,plain,
    ! [X0] : meet(a,sF8) = meet(a,meet(sF8,join(X0,join(x2,sF1)))),
    inference(backward_demodulation,[],[f52025,f201885]) ).

fof(f201915,plain,
    ! [X0] : meet(a,meet(sF8,X0)) = meet(a,meet(X0,join(x2,sF1))),
    inference(backward_demodulation,[],[f82017,f201885]) ).

fof(f201981,plain,
    ! [X0] : meet(a,meet(sF8,X0)) = meet(a,meet(X0,join(sF0,x2))),
    inference(forward_demodulation,[],[f201915,f163699]) ).

fof(f202002,plain,
    ! [X0] : meet(a,meet(X0,sF0)) = meet(a,meet(sF8,X0)),
    inference(forward_demodulation,[],[f201981,f2644]) ).

fof(f202012,plain,
    ! [X0] : meet(sF0,meet(a,X0)) = meet(a,meet(sF8,X0)),
    inference(forward_demodulation,[],[f202002,f332]) ).

fof(f202017,plain,
    ! [X0] : meet(sF1,X0) = meet(a,meet(sF8,X0)),
    inference(forward_demodulation,[],[f202012,f323]) ).

fof(f202080,plain,
    ! [X0] : meet(a,sF8) = meet(sF1,join(X0,join(x2,sF1))),
    inference(backward_demodulation,[],[f201911,f202017]) ).

fof(f202098,plain,
    sF1 = meet(a,sF8),
    inference(forward_demodulation,[],[f202080,f301]) ).

fof(f202150,plain,
    join(sF7,sF1) = join(sF7,meet(a,x2)),
    inference(backward_demodulation,[],[f21811,f202098]) ).

fof(f202254,plain,
    ! [X0] : meet(X0,sF8) = join(meet(X0,sF8),meet(X0,join(sF7,sF1))),
    inference(backward_demodulation,[],[f85492,f202150]) ).

fof(f202367,plain,
    sF8 = join(sF8,sF1),
    inference(superposition,[],[f240,f202098]) ).

fof(f202398,plain,
    ! [X0] : join(X0,sF8) = join(sF8,join(X0,sF1)),
    inference(superposition,[],[f115605,f202098]) ).

fof(f202405,plain,
    ! [X0] : join(X0,sF8) = join(sF1,join(sF8,X0)),
    inference(forward_demodulation,[],[f202398,f303]) ).

fof(f202439,plain,
    sF8 = join(sF1,sF8),
    inference(forward_demodulation,[],[f202367,f3]) ).

fof(f202508,plain,
    sF6 = join(meet(sF2,y2),sF8),
    inference(backward_demodulation,[],[f75464,f202405]) ).

fof(f202586,plain,
    ! [X0] : meet(X0,sF2) = join(meet(join(z2,sF1),X0),meet(sF8,X0)),
    inference(backward_demodulation,[],[f86789,f202439]) ).

fof(f202670,plain,
    sF6 = join(sF8,meet(y2,sF2)),
    inference(forward_demodulation,[],[f202508,f134866]) ).

fof(f202736,plain,
    ! [X0] : meet(X0,sF2) = join(meet(X0,sF8),meet(X0,join(z2,sF1))),
    inference(forward_demodulation,[],[f202586,f138802]) ).

fof(f202794,plain,
    sF6 = join(sF8,meet(sF2,y2)),
    inference(forward_demodulation,[],[f202670,f136390]) ).

fof(f451014,plain,
    meet(y2,sF2) = join(meet(y2,sF8),meet(y2,join(sF7,sF1))),
    inference(superposition,[],[f202736,f37809]) ).

fof(f451284,plain,
    meet(y2,sF2) = meet(y2,sF8),
    inference(forward_demodulation,[],[f451014,f202254]) ).

fof(f451434,plain,
    meet(sF2,y2) = meet(y2,sF8),
    inference(forward_demodulation,[],[f451284,f1]) ).

fof(f452414,plain,
    sF8 = join(sF8,meet(sF2,y2)),
    inference(superposition,[],[f240,f451434]) ).

fof(f452500,plain,
    sF6 = sF8,
    inference(forward_demodulation,[],[f452414,f202794]) ).

fof(f453456,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f452500,f40]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LAT401-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38  % Computer : n017.cluster.edu
% 0.10/0.38  % Model    : x86_64 x86_64
% 0.10/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38  % Memory   : 8046.5625MB
% 0.10/0.38  % OS       : Linux 6.8.0-71-generic
% 0.10/0.38  % CPULimit : 300
% 0.10/0.38  % WCLimit  : 300
% 0.10/0.38  % DateTime : Sun Sep 27 15:11:20 UTC 2026
% 0.10/0.38  % CPUTime  : 
% 0.10/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42  Running first-order theorem proving
% 0.10/0.42  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 88.69/13.33  % (2709404)Detected a unit-equality problem, will run specialized UEQ schedule.
% 88.69/13.33  % (2709415)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=526075197:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 88.69/13.33  % (2709412)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2936939919:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 88.69/13.33  % (2709410)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=801609880:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 88.69/13.33  % (2709414)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=3126814340:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 88.69/13.33  % (2709411)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3605454018:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 88.69/13.33  % (2709413)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2530369256:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 88.69/13.33  % (2709409)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=2720828755:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 88.69/13.33  % (2709412)Instruction limit reached! 
% 88.69/13.33  % (2709412)------------------------------
% 88.69/13.33  % (2709412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.69/13.33  % (2709412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.69/13.33  % (2709412)CaDiCaL version: 2.1.3
% 88.69/13.33  % (2709412)Termination reason: Instruction limit
% 88.69/13.33  % (2709412)Termination phase: Saturation
% 88.69/13.33  % (2709412)Time elapsed: 0.079 s
% 88.69/13.33  % (2709412)Peak memory usage: 89 MB
% 88.69/13.33  % (2709412)Instructions burned: 138 (million)
% 88.69/13.33  % (2709413)Instruction limit reached! 
% 88.69/13.33  % (2709413)------------------------------
% 88.69/13.33  % (2709413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.69/13.33  % (2709413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.69/13.33  % (2709413)CaDiCaL version: 2.1.3
% 88.69/13.33  % (2709413)Termination reason: Instruction limit
% 88.69/13.33  % (2709413)Termination phase: Saturation
% 88.69/13.33  % (2709413)Time elapsed: 0.105 s
% 88.69/13.33  % (2709413)Peak memory usage: 89 MB
% 88.69/13.33  % (2709413)Instructions burned: 182 (million)
% 88.69/13.33  % (2709414)Instruction limit reached! 
% 88.69/13.33  % (2709414)------------------------------
% 88.69/13.33  % (2709414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.69/13.33  % (2709414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.69/13.33  % (2709414)CaDiCaL version: 2.1.3
% 88.69/13.33  % (2709414)Termination reason: Instruction limit
% 88.69/13.33  % (2709414)Termination phase: Saturation
% 88.69/13.33  % (2709414)Time elapsed: 0.170 s
% 88.69/13.33  % (2709414)Peak memory usage: 90 MB
% 88.69/13.33  % (2709414)Instructions burned: 258 (million)
% 88.69/13.33  % (2709423)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3311542953:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 88.69/13.33  % (2709424)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4117624813:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 88.69/13.33  % (2709425)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2510567778:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 88.69/13.33  % (2709415)Instruction limit reached! 
% 88.69/13.33  % (2709415)------------------------------
% 88.69/13.33  % (2709415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.69/13.33  % (2709415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.69/13.33  % (2709415)CaDiCaL version: 2.1.3
% 88.69/13.33  % (2709415)Termination reason: Instruction limit
% 88.69/13.33  % (2709415)Termination phase: Saturation
% 88.69/13.33  % (2709415)Time elapsed: 0.359 s
% 142.74/21.02  % (2709415)Peak memory usage: 99 MB
% 142.74/21.02  % (2709415)Instructions burned: 1190 (million)
% 142.74/21.02  % (2709429)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=4006642434:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 142.74/21.02  % (2709425)Instruction limit reached! 
% 142.74/21.02  % (2709425)------------------------------
% 142.74/21.02  % (2709425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.74/21.02  % (2709425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.74/21.02  % (2709425)CaDiCaL version: 2.1.3
% 142.74/21.02  % (2709425)Termination reason: Instruction limit
% 142.74/21.02  % (2709425)Termination phase: Saturation
% 142.74/21.02  % (2709425)Time elapsed: 0.120 s
% 142.74/21.02  % (2709425)Peak memory usage: 92 MB
% 142.74/21.02  % (2709425)Instructions burned: 217 (million)
% 142.74/21.02  % (2709429)Instruction limit reached! 
% 142.74/21.02  % (2709429)------------------------------
% 142.74/21.02  % (2709429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.74/21.02  % (2709429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.74/21.02  % (2709429)CaDiCaL version: 2.1.3
% 142.74/21.02  % (2709429)Termination reason: Instruction limit
% 142.74/21.02  % (2709429)Termination phase: Saturation
% 142.74/21.02  % (2709429)Time elapsed: 0.095 s
% 142.74/21.02  % (2709429)Peak memory usage: 91 MB
% 142.74/21.02  % (2709429)Instructions burned: 319 (million)
% 142.74/21.02  % (2709431)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=1923607515:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 142.74/21.02  % (2709432)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2053976006:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 142.74/21.02  % (2709423)Instruction limit reached! 
% 142.74/21.02  % (2709423)------------------------------
% 142.74/21.02  % (2709423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.74/21.02  % (2709423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.74/21.02  % (2709423)CaDiCaL version: 2.1.3
% 142.74/21.02  % (2709423)Termination reason: Instruction limit
% 142.74/21.02  % (2709423)Termination phase: Saturation
% 142.74/21.02  % (2709423)Time elapsed: 1.334 s
% 142.74/21.02  % (2709423)Peak memory usage: 140 MB
% 142.74/21.02  % (2709423)Instructions burned: 2051 (million)
% 142.74/21.02  % (2709432)Instruction limit reached! 
% 142.74/21.02  % (2709432)------------------------------
% 142.74/21.02  % (2709432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.74/21.02  % (2709432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.74/21.02  % (2709432)CaDiCaL version: 2.1.3
% 142.74/21.02  % (2709432)Termination reason: Instruction limit
% 142.74/21.02  % (2709432)Termination phase: Saturation
% 142.74/21.02  % (2709432)Time elapsed: 0.994 s
% 142.74/21.02  % (2709432)Peak memory usage: 131 MB
% 142.74/21.02  % (2709432)Instructions burned: 2837 (million)
% 142.74/21.02  % (2709437)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=1717713807:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/11832Mi)
% 142.74/21.02  % (2709436)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2457386538:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 142.74/21.02  % (2709424)Instruction limit reached! 
% 142.74/21.02  % (2709424)------------------------------
% 142.74/21.02  % (2709424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.74/21.02  % (2709424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.74/21.02  % (2709424)CaDiCaL version: 2.1.3
% 142.74/21.02  % (2709424)Termination reason: Instruction limit
% 142.74/21.02  % (2709424)Termination phase: Saturation
% 142.74/21.02  % (2709424)Time elapsed: 2.960 s
% 142.74/21.02  % (2709424)Peak memory usage: 163 MB
% 142.74/21.02  % (2709424)Instructions burned: 4948 (million)
% 142.74/21.02  % (2709440)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=3929067046:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 142.74/21.02  % (2709440)Instruction limit reached! 
% 142.74/21.02  % (2709440)------------------------------
% 274.37/39.47  % (2709440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709440)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709440)Termination reason: Instruction limit
% 274.37/39.47  % (2709440)Termination phase: Saturation
% 274.37/39.47  % (2709440)Time elapsed: 1.388 s
% 274.37/39.47  % (2709440)Peak memory usage: 139 MB
% 274.37/39.47  % (2709440)Instructions burned: 2280 (million)
% 274.37/39.47  % (2709442)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:drc=off:fde=none:sp=reverse_arity:urr=ec_only:gs=on:s2agt=16:random_seed=577788837:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 274.37/39.47  % (2709437)Instruction limit reached! 
% 274.37/39.47  % (2709437)------------------------------
% 274.37/39.47  % (2709437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709437)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709437)Termination reason: Instruction limit
% 274.37/39.47  % (2709437)Termination phase: Saturation
% 274.37/39.47  % (2709437)Time elapsed: 4.172 s
% 274.37/39.47  % (2709437)Peak memory usage: 213 MB
% 274.37/39.47  % (2709437)Instructions burned: 11835 (million)
% 274.37/39.47  % (2709444)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=3650832680:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2939 on theBenchmark for (2939ds/21755Mi)
% 274.37/39.47  % (2709431)Instruction limit reached! 
% 274.37/39.47  % (2709431)------------------------------
% 274.37/39.47  % (2709431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709431)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709431)Termination reason: Instruction limit
% 274.37/39.47  % (2709431)Termination phase: Saturation
% 274.37/39.47  % (2709431)Time elapsed: 7.440 s
% 274.37/39.47  % (2709431)Peak memory usage: 232 MB
% 274.37/39.47  % (2709431)Instructions burned: 12127 (million)
% 274.37/39.47  % (2709446)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=3664210355:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2918 on theBenchmark for (2918ds/16427Mi)
% 274.37/39.47  % (2709442)Instruction limit reached! 
% 274.37/39.47  % (2709442)------------------------------
% 274.37/39.47  % (2709442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709442)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709442)Termination reason: Instruction limit
% 274.37/39.47  % (2709442)Termination phase: Saturation
% 274.37/39.47  % (2709442)Time elapsed: 3.542 s
% 274.37/39.47  % (2709442)Peak memory usage: 155 MB
% 274.37/39.47  % (2709442)Instructions burned: 6225 (million)
% 274.37/39.47  % (2709448)lrs+1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:drc=off:fde=none:sp=const_frequency:spb=goal:fd=preordered:random_seed=2282594261:i=9356:fgj=on:bd=preordered:av=off_2914 on theBenchmark for (2914ds/9356Mi)
% 274.37/39.47  % (2709436)Instruction limit reached! 
% 274.37/39.47  % (2709436)------------------------------
% 274.37/39.47  % (2709436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709436)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709436)Termination reason: Instruction limit
% 274.37/39.47  % (2709436)Termination phase: Saturation
% 274.37/39.47  % (2709436)Time elapsed: 9.229 s
% 274.37/39.47  % (2709436)Peak memory usage: 229 MB
% 274.37/39.47  % (2709436)Instructions burned: 14534 (million)
% 274.37/39.47  % (2709450)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=2415258895:i=2070:kws=inv_precedence:slsql=off:bd=all_2889 on theBenchmark for (2889ds/2070Mi)
% 274.37/39.47  % (2709450)Instruction limit reached! 
% 274.37/39.47  % (2709450)------------------------------
% 274.37/39.47  % (2709450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 274.37/39.47  % (2709450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.37/39.47  % (2709450)CaDiCaL version: 2.1.3
% 274.37/39.47  % (2709450)Termination reason: Instruction limit
% 274.37/39.47  % (2709450)Termination phase: Saturation
% 181.78/40.54  % (2709450)Time elapsed: 1.256 s
% 181.78/40.54  % (2709450)Peak memory usage: 131 MB
% 181.78/40.54  % (2709450)Instructions burned: 2070 (million)
% 181.78/40.54  % (2709452)lrs+1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=8000:tgt=ground:npcc=on:fde=unused:sp=const_min:urr=ec_only:s2agt=32:random_seed=2945565775:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2875 on theBenchmark for (2875ds/6461Mi)
% 181.78/40.54  % (2709448)Instruction limit reached! 
% 181.78/40.54  % (2709448)------------------------------
% 181.78/40.54  % (2709448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709448)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709448)Termination reason: Instruction limit
% 181.78/40.54  % (2709448)Termination phase: Saturation
% 181.78/40.54  % (2709448)Time elapsed: 5.660 s
% 181.78/40.54  % (2709448)Peak memory usage: 196 MB
% 181.78/40.54  % (2709448)Instructions burned: 9356 (million)
% 181.78/40.54  % (2709684)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=328103409:i=2310:bd=all:ss=included_2856 on theBenchmark for (2856ds/2310Mi)
% 181.78/40.54  % (2709444)Instruction limit reached! 
% 181.78/40.54  % (2709444)------------------------------
% 181.78/40.54  % (2709444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709444)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709444)Termination reason: Instruction limit
% 181.78/40.54  % (2709444)Termination phase: Saturation
% 181.78/40.54  % (2709444)Time elapsed: 8.524 s
% 181.78/40.54  % (2709444)Peak memory usage: 240 MB
% 181.78/40.54  % (2709444)Instructions burned: 21755 (million)
% 181.78/40.54  % (2709686)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=248125919:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2853 on theBenchmark for (2853ds/2616Mi)
% 181.78/40.54  % (2709686)Instruction limit reached! 
% 181.78/40.54  % (2709686)------------------------------
% 181.78/40.54  % (2709686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709686)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709686)Termination reason: Instruction limit
% 181.78/40.54  % (2709686)Termination phase: Saturation
% 181.78/40.54  % (2709686)Time elapsed: 1.107 s
% 181.78/40.54  % (2709686)Peak memory usage: 116 MB
% 181.78/40.54  % (2709686)Instructions burned: 2616 (million)
% 181.78/40.54  % (2709717)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=796217783:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2841 on theBenchmark for (2841ds/30521Mi)
% 181.78/40.54  % (2709684)Instruction limit reached! 
% 181.78/40.54  % (2709684)------------------------------
% 181.78/40.54  % (2709684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709684)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709684)Termination reason: Instruction limit
% 181.78/40.54  % (2709684)Termination phase: Saturation
% 181.78/40.54  % (2709684)Time elapsed: 2.192 s
% 181.78/40.54  % (2709684)Peak memory usage: 105 MB
% 181.78/40.54  % (2709684)Instructions burned: 2310 (million)
% 181.78/40.54  % (2709730)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=2323692803:i=3258:fgj=on:bd=all:ins=1_2832 on theBenchmark for (2832ds/3258Mi)
% 181.78/40.54  % (2709452)Instruction limit reached! 
% 181.78/40.54  % (2709452)------------------------------
% 181.78/40.54  % (2709452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709452)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709452)Termination reason: Instruction limit
% 181.78/40.54  % (2709452)Termination phase: Saturation
% 181.78/40.54  % (2709452)Time elapsed: 4.798 s
% 181.78/40.54  % (2709452)Peak memory usage: 161 MB
% 181.78/40.54  % (2709452)Instructions burned: 6462 (million)
% 181.78/40.54  % (2709738)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=1023216712:i=5037:kws=precedence_2825 on theBenchmark for (2825ds/5037Mi)
% 181.78/40.54  % (2709730)Instruction limit reached! 
% 181.78/40.54  % (2709730)------------------------------
% 181.78/40.54  % (2709730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709730)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709730)Termination reason: Instruction limit
% 181.78/40.54  % (2709730)Termination phase: Saturation
% 181.78/40.54  % (2709730)Time elapsed: 3.269 s
% 181.78/40.54  % (2709730)Peak memory usage: 152 MB
% 181.78/40.54  % (2709730)Instructions burned: 3258 (million)
% 181.78/40.54  % (2709753)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2886118668:i=65240_2798 on theBenchmark for (2798ds/65240Mi)
% 181.78/40.54  % (2709446)Instruction limit reached! 
% 181.78/40.54  % (2709446)------------------------------
% 181.78/40.54  % (2709446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709446)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709446)Termination reason: Instruction limit
% 181.78/40.54  % (2709446)Termination phase: Saturation
% 181.78/40.54  % (2709446)Time elapsed: 12.562 s
% 181.78/40.54  % (2709446)Peak memory usage: 221 MB
% 181.78/40.54  % (2709446)Instructions burned: 16427 (million)
% 181.78/40.54  % (2709755)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=995575823:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2790 on theBenchmark for (2790ds/16502Mi)
% 181.78/40.54  % (2709738)Instruction limit reached! 
% 181.78/40.54  % (2709738)------------------------------
% 181.78/40.54  % (2709738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709738)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709738)Termination reason: Instruction limit
% 181.78/40.54  % (2709738)Termination phase: Saturation
% 181.78/40.54  % (2709738)Time elapsed: 5.154 s
% 181.78/40.54  % (2709738)Peak memory usage: 164 MB
% 181.78/40.54  % (2709738)Instructions burned: 5037 (million)
% 181.78/40.54  % (2709765)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=1091858535:i=7623:bd=preordered:er=filter_2771 on theBenchmark for (2771ds/7623Mi)
% 181.78/40.54  % (2709765)Instruction limit reached! 
% 181.78/40.54  % (2709765)------------------------------
% 181.78/40.54  % (2709765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709765)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709765)Termination reason: Instruction limit
% 181.78/40.54  % (2709765)Termination phase: Saturation
% 181.78/40.54  % (2709765)Time elapsed: 7.812 s
% 181.78/40.54  % (2709765)Peak memory usage: 189 MB
% 181.78/40.54  % (2709765)Instructions burned: 7623 (million)
% 181.78/40.54  % (2709786)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=3716628028:i=8183:kws=frequency:add=off:gsp=on_2691 on theBenchmark for (2691ds/8183Mi)
% 181.78/40.54  % (2709717)Instruction limit reached! 
% 181.78/40.54  % (2709717)------------------------------
% 181.78/40.54  % (2709717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709717)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709717)Termination reason: Instruction limit
% 181.78/40.54  % (2709717)Termination phase: Saturation
% 181.78/40.54  % (2709717)Time elapsed: 17.802 s
% 181.78/40.54  % (2709717)Peak memory usage: 348 MB
% 181.78/40.54  % (2709717)Instructions burned: 30522 (million)
% 181.78/40.54  % (2709791)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=959227814:i=8387_2661 on theBenchmark for (2661ds/8387Mi)
% 181.78/40.54  % (2709755)Instruction limit reached! 
% 181.78/40.54  % (2709755)------------------------------
% 181.78/40.54  % (2709755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709755)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709755)Termination reason: Instruction limit
% 181.78/40.54  % (2709755)Termination phase: Saturation
% 181.78/40.54  % (2709755)Time elapsed: 17.486 s
% 181.78/40.54  % (2709755)Peak memory usage: 243 MB
% 181.78/40.54  % (2709755)Instructions burned: 16502 (million)
% 181.78/40.54  % (2709791)Instruction limit reached! 
% 181.78/40.54  % (2709791)------------------------------
% 181.78/40.54  % (2709791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709791)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709791)Termination reason: Instruction limit
% 181.78/40.54  % (2709791)Termination phase: Saturation
% 181.78/40.54  % (2709791)Time elapsed: 4.730 s
% 181.78/40.54  % (2709791)Peak memory usage: 190 MB
% 181.78/40.54  % (2709791)Instructions burned: 8388 (million)
% 181.78/40.54  % (2709799)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=1960132249:i=53964:kws=inv_arity_squared:fgj=on:bd=preordered_2613 on theBenchmark for (2613ds/53964Mi)
% 181.78/40.54  % (2709800)lrs-1011_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=reverse_frequency:spb=goal:lsd=20:urr=on:flr=on:random_seed=2889709475:i=10575:s2at=5:gtg=position_2612 on theBenchmark for (2612ds/10575Mi)
% 181.78/40.54  % (2709411)First to succeed.
% 181.78/40.54  % (2709411)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2709404"
% 181.78/40.54  % (2709786)Instruction limit reached! 
% 181.78/40.54  % (2709786)------------------------------
% 181.78/40.54  % (2709786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.78/40.54  % (2709786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.78/40.54  % (2709786)CaDiCaL version: 2.1.3
% 181.78/40.54  % (2709786)Termination reason: Instruction limit
% 181.78/40.54  % (2709786)Termination phase: Saturation
% 181.78/40.54  % (2709786)Time elapsed: 8.196 s
% 181.78/40.54  % (2709786)Peak memory usage: 198 MB
% 181.78/40.54  % (2709786)Instructions burned: 8183 (million)
% 181.78/40.54  % (2709803)ott-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=ground:npcc=on:lsd=50:urr=ec_only:random_seed=1556467054:i=12036:s2at=3:gtgl=2:kws=frequency:add=off:fgj=on:bd=preordered:ins=2:gtg=exists_sym_2606 on theBenchmark for (2606ds/12036Mi)
% 181.78/40.54  % (2709411)Refutation found. Thanks to Tanya!
% 181.78/40.54  % SZS status Unsatisfiable for theBenchmark
% 181.78/40.54  % SZS output start Proof for theBenchmark
% See solution above
% 282.16/40.72  % (2709411)------------------------------
% 282.16/40.72  % (2709411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 282.16/40.72  % (2709411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 282.16/40.72  % (2709411)CaDiCaL version: 2.1.3
% 282.16/40.72  % (2709411)Termination reason: Refutation
% 282.16/40.72  % (2709411)Time elapsed: 38.930 s
% 282.16/40.72  % (2709411)Peak memory usage: 405 MB
% 282.16/40.72  % (2709411)Instructions burned: 45836 (million)
% 282.16/40.72  % (2709411)------------------------------
% 282.16/40.72  % (2709411)------------------------------
% 282.16/40.72  % (2709404)Success in time 39.681 s
% 282.16/40.72  % Vampire exiting
%------------------------------------------------------------------------------