%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT401-2 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:37 AM UTC 2026
% Result : Unsatisfiable 79.20s 16.42s
% Output : Refutation 110.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 23
% Syntax : Number of formulae : 973 ( 973 unt; 9 def)
% Number of atoms : 973 ( 972 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 : 10 ( 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 : 1658 (1658 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity) ).
fof(f3,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_001) ).
fof(f4,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_002) ).
fof(f5,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption) ).
fof(f6,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorption_003) ).
fof(f7,axiom,
! [X2,X0,X1] : upme(X0,X1,X2) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_of_upme) ).
fof(f9,negated_conjecture,
! [X2,X0,X1] : upjo(X0,X1,X2) = meet(join(X0,X1),join(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_of_upjo) ).
fof(f10,negated_conjecture,
! [X2,X0,X1] : lojo(X0,X1,X2) = join(X0,meet(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_of_lojo) ).
fof(f11,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/sandbox/benchmark/theBenchmark.p',upme_property_1) ).
fof(f12,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/sandbox/benchmark/theBenchmark.p',upme_property_2) ).
fof(f13,negated_conjecture,
upme(a,x2,y2) = upme(a,x2,z2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(f14,negated_conjecture,
upme(a,x2,y2) = upme(a,y2,z2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
fof(f15,negated_conjecture,
upjo(x2,y2,z2) != lojo(x2,y2,z2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_2) ).
fof(f16,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,[],[f11,f7]) ).
fof(f17,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,[],[f12,f7,f7,f7]) ).
fof(f18,plain,
meet(a,join(x2,y2)) = meet(a,join(x2,z2)),
inference(definition_unfolding,[],[f13,f7,f7]) ).
fof(f19,plain,
meet(a,join(x2,y2)) = meet(a,join(y2,z2)),
inference(definition_unfolding,[],[f14,f7,f7]) ).
fof(f20,plain,
meet(join(x2,y2),join(x2,z2)) != join(x2,meet(y2,z2)),
inference(definition_unfolding,[],[f15,f9,f10]) ).
fof(f21,definition,
sF0 = join(x2,y2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f22,plain,
join(x2,y2) = sF0,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF1 = meet(a,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f24,plain,
meet(a,sF0) = sF1,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF2 = join(x2,z2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f26,plain,
join(x2,z2) = sF2,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF3 = meet(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f28,plain,
meet(a,sF2) = sF3,
inference(reorient_equations,[],[f27]) ).
fof(f29,plain,
sF1 = sF3,
inference(definition_folding,[],[f18,f28,f26,f24,f22]) ).
fof(f30,definition,
sF4 = join(y2,z2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f31,plain,
join(y2,z2) = sF4,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF5 = meet(a,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f33,plain,
meet(a,sF4) = sF5,
inference(reorient_equations,[],[f32]) ).
fof(f34,plain,
sF1 = sF5,
inference(definition_folding,[],[f19,f33,f31,f24,f22]) ).
fof(f35,definition,
sF6 = meet(sF0,sF2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f36,plain,
meet(sF0,sF2) = sF6,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF7 = meet(y2,z2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f38,plain,
meet(y2,z2) = sF7,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF8 = join(x2,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f40,plain,
join(x2,sF7) = sF8,
inference(reorient_equations,[],[f39]) ).
fof(f41,plain,
sF6 != sF8,
inference(definition_folding,[],[f20,f40,f38,f36,f26,f22]) ).
fof(f42,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,[],[f16,f3]) ).
fof(f43,plain,
sF1 = meet(sF0,a),
inference(forward_demodulation,[],[f24,f1]) ).
fof(f44,plain,
sF1 = meet(a,sF2),
inference(forward_demodulation,[],[f28,f29]) ).
fof(f45,plain,
sF1 = meet(a,sF4),
inference(forward_demodulation,[],[f33,f34]) ).
fof(f46,plain,
sF8 = join(sF7,x2),
inference(forward_demodulation,[],[f40,f3]) ).
fof(f47,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,[],[f42,f2]) ).
fof(f48,plain,
sF1 = meet(sF2,a),
inference(forward_demodulation,[],[f44,f1]) ).
fof(f49,plain,
sF1 = meet(sF4,a),
inference(forward_demodulation,[],[f45,f1]) ).
fof(f50,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,[],[f47,f2]) ).
fof(f51,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,[],[f50,f2]) ).
fof(f70,plain,
sF0 = join(sF0,sF1),
inference(superposition,[],[f5,f43]) ).
fof(f92,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,[],[f51,f36]) ).
fof(f93,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,[],[f51,f36]) ).
fof(f94,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,[],[f93,f3]) ).
fof(f95,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,[],[f92,f1]) ).
fof(f96,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,[],[f95,f3]) ).
fof(f97,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f6,f5]) ).
fof(f99,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f5,f6]) ).
fof(f100,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,[],[f51,f6]) ).
fof(f101,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,[],[f51,f6]) ).
fof(f102,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,[],[f101,f4]) ).
fof(f103,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,[],[f100,f1]) ).
fof(f104,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,[],[f102,f6]) ).
fof(f105,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,[],[f104,f3]) ).
fof(f106,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,[],[f103,f105]) ).
fof(f114,plain,
! [X2,X0,X1] : meet(X2,join(join(X1,meet(a,X0)),meet(a,join(X0,meet(a,X1))))) = join(meet(X2,join(join(X1,meet(a,X0)),meet(a,meet(a,join(X0,meet(a,X1)))))),meet(X2,meet(a,join(X0,X1)))),
inference(superposition,[],[f17,f17]) ).
fof(f116,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,join(X1,meet(a,X0))),X0),
inference(superposition,[],[f17,f6]) ).
fof(f119,plain,
! [X0,X1] : join(X0,meet(X0,join(X1,meet(a,X0)))) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[],[f116,f3]) ).
fof(f121,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(join(X1,meet(a,X0)),meet(a,meet(a,join(X0,meet(a,X1))))))) = meet(X2,join(join(X1,meet(a,X0)),meet(a,join(X0,meet(a,X1))))),
inference(forward_demodulation,[],[f114,f3]) ).
fof(f129,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(forward_demodulation,[],[f119,f5]) ).
fof(f131,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(join(X1,meet(a,X0)),meet(a,meet(a,join(X0,meet(a,X1))))))) = meet(X2,join(X1,join(meet(a,X0),meet(a,join(X0,meet(a,X1)))))),
inference(forward_demodulation,[],[f121,f4]) ).
fof(f137,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,join(meet(a,X0),meet(a,meet(a,join(X0,meet(a,X1)))))))) = meet(X2,join(X1,join(meet(a,X0),meet(a,join(X0,meet(a,X1)))))),
inference(forward_demodulation,[],[f131,f4]) ).
fof(f144,plain,
x2 = meet(x2,sF0),
inference(superposition,[],[f6,f22]) ).
fof(f145,plain,
x2 = meet(sF0,x2),
inference(forward_demodulation,[],[f144,f1]) ).
fof(f146,plain,
sF2 = join(sF2,sF1),
inference(superposition,[],[f5,f48]) ).
fof(f156,plain,
x2 = meet(x2,sF2),
inference(superposition,[],[f6,f26]) ).
fof(f157,plain,
x2 = meet(sF2,x2),
inference(forward_demodulation,[],[f156,f1]) ).
fof(f158,plain,
sF4 = join(sF4,sF1),
inference(superposition,[],[f5,f49]) ).
fof(f159,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,[],[f51,f49]) ).
fof(f162,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,[],[f159,f1]) ).
fof(f164,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,[],[f162,f3]) ).
fof(f166,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))),
inference(forward_demodulation,[],[f164,f5]) ).
fof(f167,plain,
! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(a,meet(sF4,join(X0,a)))),
inference(forward_demodulation,[],[f166,f1]) ).
fof(f168,plain,
y2 = join(y2,sF7),
inference(superposition,[],[f5,f38]) ).
fof(f173,plain,
y2 = join(sF7,y2),
inference(forward_demodulation,[],[f168,f3]) ).
fof(f187,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,[],[f17,f3]) ).
fof(f188,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,[],[f17,f3]) ).
fof(f190,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,[],[f51,f3]) ).
fof(f191,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,[],[f51,f3]) ).
fof(f192,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,[],[f17,f3]) ).
fof(f193,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,[],[f190,f1]) ).
fof(f194,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,[],[f188,f3]) ).
fof(f197,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f129,f5]) ).
fof(f201,plain,
y2 = meet(y2,sF0),
inference(superposition,[],[f129,f22]) ).
fof(f202,plain,
z2 = meet(z2,sF2),
inference(superposition,[],[f129,f26]) ).
fof(f203,plain,
z2 = meet(z2,sF4),
inference(superposition,[],[f129,f31]) ).
fof(f208,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,[],[f51,f129]) ).
fof(f209,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,[],[f51,f129]) ).
fof(f214,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,[],[f209,f4]) ).
fof(f215,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,[],[f208,f1]) ).
fof(f218,plain,
z2 = meet(sF4,z2),
inference(forward_demodulation,[],[f203,f1]) ).
fof(f219,plain,
z2 = meet(sF2,z2),
inference(forward_demodulation,[],[f202,f1]) ).
fof(f220,plain,
y2 = meet(sF0,y2),
inference(forward_demodulation,[],[f201,f1]) ).
fof(f222,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f197,f2]) ).
fof(f241,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f5,f1]) ).
fof(f242,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,[],[f51,f1]) ).
fof(f244,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,[],[f17,f1]) ).
fof(f245,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,[],[f17,f1]) ).
fof(f247,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,[],[f17,f1]) ).
fof(f248,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,[],[f17,f1]) ).
fof(f249,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f241,f6]) ).
fof(f253,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(join(meet(a,meet(X2,X1)),X0),join(meet(X0,X1),meet(a,meet(X2,join(X0,X1))))),
inference(superposition,[],[f241,f51]) ).
fof(f256,plain,
sF2 = join(sF2,sF6),
inference(superposition,[],[f241,f36]) ).
fof(f258,plain,
a = join(a,sF1),
inference(superposition,[],[f241,f49]) ).
fof(f271,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(meet(a,meet(X2,X1)),join(X0,join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f253,f4]) ).
fof(f273,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f249,f4]) ).
fof(f284,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f4,f5]) ).
fof(f285,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f4,f241]) ).
fof(f287,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f4,f3]) ).
fof(f288,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,f17]) ).
fof(f290,plain,
! [X0] : join(x2,join(y2,X0)) = join(sF0,X0),
inference(superposition,[],[f4,f22]) ).
fof(f291,plain,
! [X0] : join(sF2,X0) = join(x2,join(z2,X0)),
inference(superposition,[],[f4,f26]) ).
fof(f292,plain,
! [X0] : join(y2,join(z2,X0)) = join(sF4,X0),
inference(superposition,[],[f4,f31]) ).
fof(f293,plain,
! [X0] : join(sF7,join(x2,X0)) = join(sF8,X0),
inference(superposition,[],[f4,f46]) ).
fof(f298,plain,
! [X2,X0,X1] : join(X0,X1) = join(X0,join(X1,meet(join(X0,X1),X2))),
inference(superposition,[],[f5,f4]) ).
fof(f302,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f129,f4]) ).
fof(f304,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f306,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,[],[f215,f304]) ).
fof(f307,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,[],[f214,f304]) ).
fof(f312,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(meet(a,meet(X2,X1)),join(X0,meet(a,meet(X2,join(X0,X1))))),
inference(backward_demodulation,[],[f271,f284]) ).
fof(f313,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,[],[f306,f302]) ).
fof(f315,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,[],[f313,f3]) ).
fof(f316,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,[],[f307,f315]) ).
fof(f318,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f284,f129]) ).
fof(f323,plain,
! [X0] : join(sF0,X0) = join(sF0,join(sF1,X0)),
inference(superposition,[],[f284,f43]) ).
fof(f325,plain,
! [X0] : join(sF2,X0) = join(sF2,join(sF1,X0)),
inference(superposition,[],[f284,f48]) ).
fof(f329,plain,
! [X2,X0,X1] : join(X0,meet(X0,X1)) = join(X0,meet(X2,meet(X0,X1))),
inference(superposition,[],[f284,f241]) ).
fof(f331,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f284,f3]) ).
fof(f335,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f129,f284]) ).
fof(f343,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f335,f1]) ).
fof(f349,plain,
! [X2,X0,X1] : join(X0,meet(X2,meet(X0,X1))) = X0,
inference(forward_demodulation,[],[f329,f5]) ).
fof(f368,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f2,f6]) ).
fof(f369,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f2,f129]) ).
fof(f371,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(X1,meet(X0,X2)),
inference(superposition,[],[f2,f1]) ).
fof(f374,plain,
! [X0] : meet(y2,meet(z2,X0)) = meet(sF7,X0),
inference(superposition,[],[f2,f38]) ).
fof(f375,plain,
! [X0] : meet(sF0,meet(a,X0)) = meet(sF1,X0),
inference(superposition,[],[f2,f43]) ).
fof(f376,plain,
! [X0] : meet(sF0,meet(sF2,X0)) = meet(sF6,X0),
inference(superposition,[],[f2,f36]) ).
fof(f377,plain,
! [X0] : meet(sF1,X0) = meet(sF2,meet(a,X0)),
inference(superposition,[],[f2,f48]) ).
fof(f378,plain,
! [X0] : meet(sF1,X0) = meet(sF4,meet(a,X0)),
inference(superposition,[],[f2,f49]) ).
fof(f384,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f391,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,[],[f17,f2]) ).
fof(f392,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,[],[f17,f2]) ).
fof(f394,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,[],[f392,f2]) ).
fof(f395,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,[],[f391,f3]) ).
fof(f402,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,[],[f96,f384]) ).
fof(f403,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,[],[f94,f384]) ).
fof(f407,plain,
! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF4,meet(join(X0,a),a))),
inference(backward_demodulation,[],[f167,f384]) ).
fof(f409,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,[],[f394,f2]) ).
fof(f410,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,[],[f395,f2]) ).
fof(f413,plain,
! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF4,meet(a,join(X0,a)))),
inference(forward_demodulation,[],[f407,f1]) ).
fof(f417,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,[],[f403,f1]) ).
fof(f418,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,[],[f402,f1]) ).
fof(f422,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X3,X2)) = meet(X0,meet(X1,join(X2,X3))),
inference(forward_demodulation,[],[f410,f409]) ).
fof(f423,plain,
! [X0] : meet(a,join(meet(a,sF1),X0)) = join(meet(X0,a),meet(sF1,join(X0,a))),
inference(forward_demodulation,[],[f413,f378]) ).
fof(f427,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,[],[f417,f375]) ).
fof(f428,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,[],[f418,f375]) ).
fof(f431,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
inference(forward_demodulation,[],[f422,f2]) ).
fof(f432,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,[],[f427,f384]) ).
fof(f433,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,[],[f428,f384]) ).
fof(f435,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f368,f241]) ).
fof(f447,plain,
! [X2,X0,X1] : meet(X0,join(X0,X1)) = meet(X0,join(X2,join(X0,X1))),
inference(superposition,[],[f368,f129]) ).
fof(f449,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f368,f1]) ).
fof(f456,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(join(X0,X2),X1),meet(X0,X1)),
inference(superposition,[],[f241,f368]) ).
fof(f459,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,[],[f51,f368]) ).
fof(f460,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,[],[f51,f368]) ).
fof(f464,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,[],[f460,f368]) ).
fof(f465,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,[],[f459,f1]) ).
fof(f467,plain,
! [X2,X0,X1] : meet(join(X0,X2),X1) = join(meet(X0,X1),meet(join(X0,X2),X1)),
inference(forward_demodulation,[],[f456,f3]) ).
fof(f473,plain,
! [X2,X0,X1] : meet(X0,join(X2,join(X0,X1))) = X0,
inference(forward_demodulation,[],[f447,f6]) ).
fof(f480,plain,
! [X2,X0,X1] : meet(X2,join(X1,join(meet(a,X0),meet(a,join(X0,meet(a,X1)))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,join(meet(a,X0),meet(a,join(X0,meet(a,X1))))))),
inference(backward_demodulation,[],[f137,f435]) ).
fof(f483,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,[],[f464,f368]) ).
fof(f484,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,[],[f465,f368]) ).
fof(f487,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,[],[f316,f473]) ).
fof(f488,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,[],[f106,f473]) ).
fof(f492,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,[],[f484,f483]) ).
fof(f493,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,[],[f488,f3]) ).
fof(f494,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,[],[f487,f3]) ).
fof(f497,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,join(X0,X1))) = join(meet(X1,X0),meet(a,join(X1,X0))),
inference(forward_demodulation,[],[f492,f368]) ).
fof(f508,plain,
! [X2,X0] : join(meet(a,X0),meet(X0,X2)) = join(meet(a,X0),meet(X2,X0)),
inference(superposition,[],[f493,f241]) ).
fof(f520,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,[],[f493,f2]) ).
fof(f569,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(X2,X0)),join(X1,X0))),
inference(superposition,[],[f242,f129]) ).
fof(f578,plain,
! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(meet(a,meet(X0,sF0)),sF2)),
inference(superposition,[],[f242,f36]) ).
fof(f580,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,[],[f242,f49]) ).
fof(f623,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(join(meet(a,meet(X1,X2)),X0),join(meet(X0,X1),meet(a,meet(X2,join(X0,X1))))),
inference(superposition,[],[f241,f242]) ).
fof(f626,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(meet(a,meet(X1,X2)),join(X0,join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f623,f4]) ).
fof(f659,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,[],[f580,f3]) ).
fof(f661,plain,
! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(sF2,meet(a,meet(X0,sF0)))),
inference(forward_demodulation,[],[f578,f3]) ).
fof(f668,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(X0,join(meet(a,meet(X2,X0)),X1))),
inference(forward_demodulation,[],[f569,f304]) ).
fof(f671,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(meet(a,meet(X1,X2)),join(X0,meet(a,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f626,f284]) ).
fof(f702,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,meet(sF4,join(a,X0)))),
inference(forward_demodulation,[],[f659,f5]) ).
fof(f704,plain,
! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF0,meet(a,X0)))),
inference(forward_demodulation,[],[f661,f384]) ).
fof(f709,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(X2,X0)),X1))),
inference(forward_demodulation,[],[f668,f4]) ).
fof(f736,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(a,sF4)),
inference(forward_demodulation,[],[f702,f449]) ).
fof(f738,plain,
! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(meet(a,sF6),X0),join(sF2,meet(sF1,X0))),
inference(forward_demodulation,[],[f704,f375]) ).
fof(f742,plain,
! [X2,X0,X1] : join(meet(join(X1,X0),X2),meet(a,X0)) = meet(join(meet(a,X0),X2),join(X0,join(meet(a,meet(X2,X0)),X1))),
inference(forward_demodulation,[],[f709,f473]) ).
fof(f763,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(a,X0),meet(sF4,a)),
inference(forward_demodulation,[],[f736,f1]) ).
fof(f765,plain,
! [X0] : join(meet(sF2,X0),meet(a,meet(sF0,join(sF2,X0)))) = meet(join(sF2,meet(sF1,X0)),join(meet(a,sF6),X0)),
inference(forward_demodulation,[],[f738,f1]) ).
fof(f767,plain,
! [X2,X0,X1] : join(meet(a,X0),meet(join(X1,X0),X2)) = meet(join(meet(a,X0),X2),join(X0,join(meet(a,meet(X2,X0)),X1))),
inference(forward_demodulation,[],[f742,f3]) ).
fof(f782,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(meet(sF4,a),meet(a,X0)),
inference(forward_demodulation,[],[f763,f3]) ).
fof(f784,plain,
! [X0] : join(meet(sF2,X0),meet(sF0,meet(join(sF2,X0),a))) = meet(join(sF2,meet(sF1,X0)),join(meet(a,sF6),X0)),
inference(forward_demodulation,[],[f765,f384]) ).
fof(f794,plain,
! [X0] : meet(join(meet(a,sF1),X0),a) = join(sF1,meet(a,X0)),
inference(forward_demodulation,[],[f782,f49]) ).
fof(f796,plain,
! [X0] : join(meet(sF2,X0),meet(sF0,meet(a,join(sF2,X0)))) = meet(join(sF2,meet(sF1,X0)),join(meet(a,sF6),X0)),
inference(forward_demodulation,[],[f784,f1]) ).
fof(f801,plain,
! [X0] : meet(a,join(meet(a,sF1),X0)) = join(sF1,meet(a,X0)),
inference(forward_demodulation,[],[f794,f1]) ).
fof(f803,plain,
! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(join(sF2,meet(sF1,X0)),join(meet(a,sF6),X0)),
inference(forward_demodulation,[],[f796,f375]) ).
fof(f808,plain,
! [X0] : join(meet(X0,a),meet(sF1,join(X0,a))) = join(sF1,meet(a,X0)),
inference(backward_demodulation,[],[f423,f801]) ).
fof(f1131,plain,
! [X0,X1] : meet(X1,join(X0,X0)) = join(meet(X0,X1),meet(X1,X0)),
inference(superposition,[],[f245,f241]) ).
fof(f1147,plain,
! [X2,X0,X1] : join(join(X1,meet(a,X2)),meet(X0,join(X2,meet(a,X1)))) = join(join(X1,meet(a,X2)),meet(X0,join(X1,X2))),
inference(superposition,[],[f284,f245]) ).
fof(f1163,plain,
! [X2,X0,X1] : join(join(X1,meet(a,X2)),meet(X0,join(X2,meet(a,X1)))) = join(X1,join(meet(a,X2),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f1147,f4]) ).
fof(f1172,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[],[f1131,f99]) ).
fof(f1196,plain,
! [X2,X0,X1] : join(X1,join(meet(a,X2),meet(X0,join(X1,X2)))) = join(X1,join(meet(a,X2),meet(X0,join(X2,meet(a,X1))))),
inference(forward_demodulation,[],[f1163,f4]) ).
fof(f1222,plain,
! [X2,X0,X1] : meet(X2,join(X1,join(meet(a,X0),meet(a,join(X1,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,join(meet(a,X0),meet(a,join(X1,X0)))))),
inference(backward_demodulation,[],[f480,f1196]) ).
fof(f1308,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),join(X3,X2)) = join(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f304,f304]) ).
fof(f1314,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f304,f4]) ).
fof(f1325,plain,
! [X2,X0,X1] : join(X2,X0) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f304,f241]) ).
fof(f1358,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f284,f304]) ).
fof(f1373,plain,
! [X2,X3,X0,X1] : join(X2,join(X0,X1)) = join(X2,join(X0,join(X1,meet(X2,X3)))),
inference(superposition,[],[f284,f304]) ).
fof(f1374,plain,
! [X2,X3,X0,X1] : join(X0,join(X1,join(X2,X3))) = join(X2,join(X3,join(X0,X1))),
inference(superposition,[],[f4,f304]) ).
fof(f1398,plain,
! [X2,X3,X0,X1] : join(X3,join(X0,join(X1,X2))) = join(X0,join(X1,join(X3,X2))),
inference(forward_demodulation,[],[f1308,f4]) ).
fof(f1415,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,[],[f494,f2]) ).
fof(f1470,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(meet(join(X2,X0),X1),join(meet(a,X0),meet(X1,join(X2,X0)))),
inference(superposition,[],[f129,f494]) ).
fof(f1476,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,join(meet(a,X0),meet(X1,join(X2,X0))))),
inference(forward_demodulation,[],[f1470,f2]) ).
fof(f1570,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,[],[f431,f4]) ).
fof(f1574,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X2,join(X1,X0))) = meet(X3,meet(join(X0,X1),X2)),
inference(superposition,[],[f431,f1]) ).
fof(f1613,plain,
! [X2,X3,X0,X1] : meet(X0,meet(join(X0,X1),join(X2,X3))) = meet(X0,join(X3,X2)),
inference(superposition,[],[f368,f431]) ).
fof(f1615,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(meet(X1,join(X3,X2)),X0),
inference(superposition,[],[f1,f431]) ).
fof(f1626,plain,
! [X2,X3,X0,X1,X4] : meet(meet(X0,X1),meet(X2,join(X3,X4))) = meet(X0,meet(X1,meet(X2,join(X4,X3)))),
inference(superposition,[],[f2,f431]) ).
fof(f1649,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(X1,meet(X2,join(X3,X4)))) = meet(X0,meet(X1,meet(X2,join(X4,X3)))),
inference(forward_demodulation,[],[f1626,f2]) ).
fof(f1655,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X1,meet(join(X3,X2),X0)),
inference(forward_demodulation,[],[f1615,f2]) ).
fof(f1657,plain,
! [X2,X3,X0] : meet(X0,join(X3,X2)) = meet(X0,join(X2,X3)),
inference(forward_demodulation,[],[f1613,f368]) ).
fof(f1724,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f1657,f4]) ).
fof(f1753,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(meet(a,meet(X0,X1)),X2),join(X1,meet(a,meet(X0,X2)))),
inference(superposition,[],[f51,f1657]) ).
fof(f1771,plain,
! [X2,X0,X1] : join(meet(a,X1),meet(X0,join(X1,X2))) = join(meet(a,X1),meet(join(X2,X1),X0)),
inference(superposition,[],[f494,f1657]) ).
fof(f1772,plain,
! [X2,X0,X1] : join(meet(a,X2),meet(X0,join(X1,X2))) = join(meet(a,X2),meet(join(X2,X1),X0)),
inference(superposition,[],[f493,f1657]) ).
fof(f1774,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f1,f1657]) ).
fof(f1837,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,[],[f483,f1774]) ).
fof(f1847,plain,
! [X2,X0,X1] : join(meet(X1,X2),meet(a,meet(X0,join(X1,X2)))) = meet(join(X1,meet(a,meet(X0,X2))),join(X2,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f1753,f1774]) ).
fof(f1883,plain,
sF0 = join(sF0,y2),
inference(superposition,[],[f5,f220]) ).
fof(f1957,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,[],[f17,f97]) ).
fof(f1960,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(superposition,[],[f1657,f97]) ).
fof(f1978,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,[],[f1957,f3]) ).
fof(f1989,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,[],[f1978,f4]) ).
fof(f1994,plain,
! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X0,meet(a,X1)),join(X1,X0)),
inference(forward_demodulation,[],[f1989,f298]) ).
fof(f1996,plain,
! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X1,X0),join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f1994,f1774]) ).
fof(f2003,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,[],[f384,f431]) ).
fof(f2053,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),meet(X2,X3)) = meet(X2,meet(X3,join(X1,X0))),
inference(superposition,[],[f431,f384]) ).
fof(f2060,plain,
! [X2,X3,X0,X1] : join(X1,X3) = join(X1,join(meet(X0,meet(X1,X2)),X3)),
inference(superposition,[],[f284,f384]) ).
fof(f2063,plain,
! [X2,X3,X0,X1] : join(meet(a,X1),meet(meet(X3,X0),join(X1,X2))) = join(meet(a,X1),meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f493,f384]) ).
fof(f2064,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X3,X0)) = meet(X1,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f368,f384]) ).
fof(f2080,plain,
! [X2,X3,X0,X1] : join(X2,X3) = join(X2,join(meet(X0,meet(X1,X2)),X3)),
inference(superposition,[],[f284,f384]) ).
fof(f2094,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,[],[f767,f2080]) ).
fof(f2098,plain,
! [X2,X3,X0,X1] : join(meet(a,X1),meet(X0,meet(join(X1,X2),X3))) = join(meet(a,X1),meet(X3,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f2063,f2]) ).
fof(f2102,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,[],[f315,f2060]) ).
fof(f2127,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,[],[f2003,f2]) ).
fof(f2131,plain,
! [X2,X0,X1] : join(meet(a,X1),meet(X0,join(X1,X2))) = meet(join(meet(a,X1),X0),join(X1,X2)),
inference(backward_demodulation,[],[f1771,f2094]) ).
fof(f2141,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,[],[f1415,f2094]) ).
fof(f2145,plain,
! [X2,X0,X1] : join(X1,join(meet(a,X2),meet(X0,join(X2,meet(a,X1))))) = join(X1,meet(join(meet(a,X2),X0),join(X2,X1))),
inference(backward_demodulation,[],[f1196,f2102]) ).
fof(f2148,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,meet(join(meet(a,X0),X1),join(X0,X2)))),
inference(backward_demodulation,[],[f1476,f2102]) ).
fof(f2149,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,[],[f1772,f2102]) ).
fof(f2154,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(join(meet(a,X0),a),join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,meet(join(meet(a,X0),a),join(X0,X1))))),
inference(backward_demodulation,[],[f1222,f2102]) ).
fof(f2179,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(join(a,meet(a,X0)),join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,meet(join(a,meet(a,X0)),join(X0,X1))))),
inference(forward_demodulation,[],[f2154,f3]) ).
fof(f2194,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,[],[f520,f2149]) ).
fof(f2197,plain,
! [X2,X0,X1] : meet(join(X2,X0),X1) = meet(join(X2,X0),meet(X1,join(X0,X2))),
inference(forward_demodulation,[],[f2148,f369]) ).
fof(f2199,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(a,X1)))),
inference(forward_demodulation,[],[f2145,f2131]) ).
fof(f2211,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(a,join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,meet(a,join(X0,X1))))),
inference(forward_demodulation,[],[f2179,f5]) ).
fof(f2218,plain,
! [X2,X3,X0,X1] : join(meet(a,X1),meet(X0,meet(join(X1,X2),X3))) = meet(join(meet(a,X1),meet(X3,X0)),join(X1,X2)),
inference(backward_demodulation,[],[f2098,f2194]) ).
fof(f2237,plain,
sF2 = join(sF2,z2),
inference(superposition,[],[f5,f219]) ).
fof(f2245,plain,
sF1 = meet(sF1,a),
inference(superposition,[],[f129,f258]) ).
fof(f2250,plain,
sF1 = meet(a,sF1),
inference(forward_demodulation,[],[f2245,f1]) ).
fof(f2254,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(sF1,X0)),
inference(backward_demodulation,[],[f801,f2250]) ).
fof(f2262,plain,
! [X0] : join(meet(X0,a),meet(sF1,join(X0,a))) = meet(a,join(sF1,X0)),
inference(backward_demodulation,[],[f808,f2254]) ).
fof(f2293,plain,
! [X0,X1] : meet(meet(X0,a),X1) = meet(meet(X0,a),meet(meet(a,join(sF1,X0)),X1)),
inference(superposition,[],[f368,f2262]) ).
fof(f2294,plain,
! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(meet(a,join(sF1,X0)),X1))),
inference(forward_demodulation,[],[f2293,f2]) ).
fof(f2308,plain,
! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(a,meet(join(sF1,X0),X1)))),
inference(forward_demodulation,[],[f2294,f2]) ).
fof(f2319,plain,
! [X0,X1] : meet(meet(X0,a),X1) = meet(X0,meet(a,meet(join(sF1,X0),X1))),
inference(forward_demodulation,[],[f2308,f435]) ).
fof(f2328,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(a,meet(join(sF1,X0),X1))),
inference(forward_demodulation,[],[f2319,f2]) ).
fof(f2337,plain,
! [X0] : meet(a,join(sF1,X0)) = join(sF1,meet(X0,a)),
inference(superposition,[],[f2254,f1]) ).
fof(f2353,plain,
! [X0,X1] : join(meet(a,join(sF1,X0)),X1) = join(sF1,join(meet(a,X0),X1)),
inference(superposition,[],[f4,f2254]) ).
fof(f2356,plain,
! [X0,X1] : join(X1,meet(a,join(sF1,X0))) = join(sF1,join(meet(a,X0),X1)),
inference(superposition,[],[f304,f2254]) ).
fof(f2396,plain,
sF1 = meet(sF1,sF2),
inference(superposition,[],[f129,f146]) ).
fof(f2401,plain,
sF1 = meet(sF2,sF1),
inference(forward_demodulation,[],[f2396,f1]) ).
fof(f2602,plain,
sF4 = join(sF4,z2),
inference(superposition,[],[f5,f218]) ).
fof(f2624,plain,
sF2 = join(x2,sF2),
inference(superposition,[],[f318,f26]) ).
fof(f2650,plain,
sF2 = join(sF2,x2),
inference(forward_demodulation,[],[f2624,f3]) ).
fof(f2756,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,[],[f129,f248]) ).
fof(f2771,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,[],[f2756,f2]) ).
fof(f2815,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,[],[f2771,f2127]) ).
fof(f2965,plain,
! [X2,X0,X1] : join(X0,X2) = join(meet(X1,X0),join(X0,X2)),
inference(superposition,[],[f287,f241]) ).
fof(f2978,plain,
! [X0] : join(sF0,X0) = join(y2,join(x2,X0)),
inference(superposition,[],[f287,f22]) ).
fof(f2979,plain,
! [X0] : join(sF2,X0) = join(z2,join(x2,X0)),
inference(superposition,[],[f287,f26]) ).
fof(f3051,plain,
! [X0] : join(sF2,X0) = join(x2,join(X0,z2)),
inference(forward_demodulation,[],[f2979,f304]) ).
fof(f3052,plain,
! [X0] : join(sF0,X0) = join(x2,join(X0,y2)),
inference(forward_demodulation,[],[f2978,f304]) ).
fof(f3061,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f2965,f304]) ).
fof(f3086,plain,
! [X2,X0,X1] : meet(meet(X0,X1),X2) = meet(meet(X0,X1),meet(X0,X2)),
inference(superposition,[],[f369,f5]) ).
fof(f3101,plain,
! [X0] : meet(z2,X0) = meet(z2,meet(sF2,X0)),
inference(superposition,[],[f369,f26]) ).
fof(f3110,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f369,f1]) ).
fof(f3115,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X0,X1)) = meet(X3,meet(X0,meet(X1,join(X2,X3)))),
inference(superposition,[],[f369,f384]) ).
fof(f3116,plain,
! [X2,X3,X0,X1] : meet(X2,meet(X3,X0)) = meet(X2,meet(X0,meet(join(X1,X2),X3))),
inference(superposition,[],[f369,f384]) ).
fof(f3166,plain,
! [X0,X1] : meet(X0,meet(a,X1)) = meet(X0,meet(X1,a)),
inference(backward_demodulation,[],[f2328,f3116]) ).
fof(f3178,plain,
! [X0] : meet(z2,X0) = meet(sF2,meet(X0,z2)),
inference(forward_demodulation,[],[f3101,f384]) ).
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,[],[f2815,f3203]) ).
fof(f3270,plain,
join(sF0,z2) = join(x2,sF4),
inference(superposition,[],[f290,f31]) ).
fof(f3305,plain,
join(sF0,z2) = join(sF4,x2),
inference(forward_demodulation,[],[f3270,f3]) ).
fof(f3327,plain,
! [X0] : meet(sF7,X0) = meet(z2,meet(y2,X0)),
inference(superposition,[],[f371,f38]) ).
fof(f3328,plain,
! [X0] : meet(a,meet(sF0,X0)) = meet(sF1,X0),
inference(superposition,[],[f371,f43]) ).
fof(f3332,plain,
! [X0] : meet(a,meet(sF2,X0)) = meet(sF1,X0),
inference(superposition,[],[f371,f48]) ).
fof(f3375,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X0,meet(X1,join(X2,meet(X1,X0)))),
inference(superposition,[],[f129,f371]) ).
fof(f3379,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,[],[f431,f371]) ).
fof(f3384,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,[],[f3379,f2]) ).
fof(f3415,plain,
! [X0] : meet(sF1,X0) = meet(sF2,meet(X0,a)),
inference(forward_demodulation,[],[f3332,f384]) ).
fof(f3419,plain,
! [X0] : meet(sF1,X0) = meet(sF0,meet(X0,a)),
inference(forward_demodulation,[],[f3328,f384]) ).
fof(f3420,plain,
! [X0] : meet(sF7,X0) = meet(y2,meet(X0,z2)),
inference(forward_demodulation,[],[f3327,f384]) ).
fof(f3442,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,[],[f433,f3419]) ).
fof(f3443,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,[],[f432,f3419]) ).
fof(f3461,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,[],[f3443,f1774]) ).
fof(f3462,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,[],[f3442,f1774]) ).
fof(f3593,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,[],[f285,f247]) ).
fof(f3594,plain,
! [X2,X0,X1] : join(join(X1,meet(X2,a)),meet(X0,join(X2,meet(a,X1)))) = join(join(X1,meet(X2,a)),meet(X0,join(X1,X2))),
inference(superposition,[],[f285,f248]) ).
fof(f3611,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(meet(X2,X0),X1),join(X0,X1)),
inference(superposition,[],[f129,f285]) ).
fof(f3617,plain,
! [X2,X3,X0,X1] : meet(join(meet(X2,X0),X1),X3) = meet(join(meet(X2,X0),X1),meet(join(X0,X1),X3)),
inference(superposition,[],[f369,f285]) ).
fof(f3628,plain,
! [X2,X3,X0,X1] : meet(join(meet(X2,X0),X1),X3) = meet(join(X0,X1),meet(X3,join(X1,meet(X2,X0)))),
inference(forward_demodulation,[],[f3617,f2053]) ).
fof(f3632,plain,
! [X2,X0,X1] : join(meet(X2,X0),X1) = meet(join(X0,X1),join(X1,meet(X2,X0))),
inference(forward_demodulation,[],[f3611,f1774]) ).
fof(f3644,plain,
! [X2,X0,X1] : join(join(X1,meet(X2,a)),meet(X0,join(X2,meet(a,X1)))) = join(X1,join(meet(X2,a),meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f3594,f4]) ).
fof(f3645,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,[],[f3593,f4]) ).
fof(f3663,plain,
! [X2,X0,X1] : join(X1,join(meet(X2,a),meet(X0,join(X1,X2)))) = join(X1,join(meet(X2,a),meet(X0,join(X2,meet(a,X1))))),
inference(forward_demodulation,[],[f3644,f4]) ).
fof(f3664,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,[],[f3645,f2131]) ).
fof(f3675,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,[],[f3664,f4]) ).
fof(f3677,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,[],[f3675,f2102]) ).
fof(f3691,plain,
sF1 = meet(sF1,sF0),
inference(superposition,[],[f129,f70]) ).
fof(f3701,plain,
sF1 = meet(sF0,sF1),
inference(forward_demodulation,[],[f3691,f1]) ).
fof(f3706,plain,
! [X0] : join(sF4,join(x2,X0)) = join(X0,join(sF0,z2)),
inference(superposition,[],[f304,f3305]) ).
fof(f3708,plain,
join(sF0,z2) = join(sF4,join(sF0,z2)),
inference(superposition,[],[f318,f3305]) ).
fof(f3711,plain,
join(sF0,z2) = join(sF0,join(z2,sF4)),
inference(forward_demodulation,[],[f3708,f304]) ).
fof(f3715,plain,
join(sF0,z2) = join(sF0,join(sF4,z2)),
inference(forward_demodulation,[],[f3711,f3]) ).
fof(f3717,plain,
join(sF0,z2) = join(sF0,sF4),
inference(forward_demodulation,[],[f3715,f2602]) ).
fof(f3719,plain,
! [X0] : join(sF4,join(x2,X0)) = join(X0,join(sF0,sF4)),
inference(backward_demodulation,[],[f3706,f3717]) ).
fof(f3798,plain,
meet(sF2,sF0) = meet(sF2,sF6),
inference(superposition,[],[f222,f36]) ).
fof(f3824,plain,
! [X2,X0,X1] : join(meet(X1,X0),X2) = join(meet(X1,X0),join(meet(X0,X1),X2)),
inference(superposition,[],[f285,f222]) ).
fof(f3835,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,a),X2)) = join(meet(join(meet(X0,a),meet(a,X2)),X1),meet(X1,join(X2,meet(a,X0)))),
inference(superposition,[],[f245,f222]) ).
fof(f3846,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,a),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(join(meet(X0,a),meet(a,X2)),X1)),
inference(forward_demodulation,[],[f3835,f3]) ).
fof(f3872,plain,
meet(sF0,sF2) = meet(sF2,sF6),
inference(forward_demodulation,[],[f3798,f1]) ).
fof(f3901,plain,
sF6 = meet(sF2,sF6),
inference(forward_demodulation,[],[f3872,f36]) ).
fof(f3962,plain,
! [X0] : join(X0,y2) = join(sF7,join(y2,X0)),
inference(superposition,[],[f304,f173]) ).
fof(f3992,plain,
! [X0] : sF2 = join(sF2,meet(sF1,X0)),
inference(superposition,[],[f5,f377]) ).
fof(f4004,plain,
! [X0] : join(meet(X0,sF2),meet(sF1,join(X0,sF2))) = meet(sF2,join(X0,meet(a,sF6))),
inference(backward_demodulation,[],[f3462,f3992]) ).
fof(f4005,plain,
! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(sF2,join(X0,meet(a,sF6))),
inference(backward_demodulation,[],[f3461,f3992]) ).
fof(f4006,plain,
! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(sF2,join(meet(a,sF6),X0)),
inference(backward_demodulation,[],[f803,f3992]) ).
fof(f4059,plain,
meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF1,join(sF2,x2))),
inference(superposition,[],[f4005,f157]) ).
fof(f4060,plain,
meet(sF2,join(z2,meet(a,sF6))) = join(z2,meet(sF1,join(sF2,z2))),
inference(superposition,[],[f4005,f219]) ).
fof(f4061,plain,
meet(sF2,join(sF6,meet(a,sF6))) = join(sF6,meet(sF1,join(sF2,sF6))),
inference(superposition,[],[f4005,f3901]) ).
fof(f4064,plain,
! [X0] : meet(sF2,join(X0,meet(a,sF6))) = join(meet(X0,sF2),meet(sF1,join(sF2,X0))),
inference(superposition,[],[f4005,f1]) ).
fof(f4095,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(meet(sF1,join(sF2,X0)),meet(sF2,join(X0,meet(a,sF6)))),
inference(superposition,[],[f129,f4005]) ).
fof(f4097,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,[],[f304,f4005]) ).
fof(f4106,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,meet(join(sF2,X0),meet(sF2,join(X0,meet(a,sF6))))),
inference(forward_demodulation,[],[f4095,f2]) ).
fof(f4130,plain,
meet(sF2,join(sF6,meet(a,sF6))) = join(sF6,meet(sF1,sF2)),
inference(forward_demodulation,[],[f4061,f256]) ).
fof(f4131,plain,
meet(sF2,join(z2,meet(a,sF6))) = join(z2,meet(sF1,sF2)),
inference(forward_demodulation,[],[f4060,f2237]) ).
fof(f4132,plain,
meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF1,sF2)),
inference(forward_demodulation,[],[f4059,f2650]) ).
fof(f4136,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(join(meet(a,sF6),X0),meet(sF1,join(sF2,X0)))),
inference(forward_demodulation,[],[f4106,f2127]) ).
fof(f4150,plain,
meet(sF2,join(sF6,meet(a,sF6))) = join(sF6,meet(sF2,sF1)),
inference(forward_demodulation,[],[f4130,f1]) ).
fof(f4151,plain,
meet(sF2,join(z2,meet(a,sF6))) = join(z2,meet(sF2,sF1)),
inference(forward_demodulation,[],[f4131,f1]) ).
fof(f4152,plain,
meet(sF2,join(x2,meet(a,sF6))) = join(x2,meet(sF2,sF1)),
inference(forward_demodulation,[],[f4132,f1]) ).
fof(f4156,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(sF1,meet(join(meet(a,sF6),X0),join(X0,sF2)))),
inference(forward_demodulation,[],[f4136,f3384]) ).
fof(f4165,plain,
meet(sF2,join(sF6,meet(a,sF6))) = join(sF6,sF1),
inference(forward_demodulation,[],[f4150,f2401]) ).
fof(f4166,plain,
meet(sF2,join(z2,meet(a,sF6))) = join(z2,sF1),
inference(forward_demodulation,[],[f4151,f2401]) ).
fof(f4167,plain,
meet(sF2,join(x2,meet(a,sF6))) = join(x2,sF1),
inference(forward_demodulation,[],[f4152,f2401]) ).
fof(f4170,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF2,meet(sF1,join(meet(a,sF6),X0))),
inference(forward_demodulation,[],[f4156,f3115]) ).
fof(f4178,plain,
meet(sF2,join(sF6,meet(a,sF6))) = join(sF1,sF6),
inference(forward_demodulation,[],[f4165,f3]) ).
fof(f4183,plain,
meet(sF2,sF6) = join(sF1,sF6),
inference(forward_demodulation,[],[f4178,f241]) ).
fof(f4186,plain,
sF6 = join(sF1,sF6),
inference(forward_demodulation,[],[f4183,f3901]) ).
fof(f4192,plain,
meet(sF2,join(sF0,meet(a,sF6))) = join(sF6,meet(sF1,join(sF0,sF2))),
inference(superposition,[],[f4004,f36]) ).
fof(f4210,plain,
! [X0,X1] : meet(meet(X0,sF2),X1) = meet(meet(X0,sF2),meet(meet(sF2,join(X0,meet(a,sF6))),X1)),
inference(superposition,[],[f368,f4004]) ).
fof(f4213,plain,
! [X0,X1] : meet(meet(X0,sF2),X1) = meet(X0,meet(sF2,meet(meet(sF2,join(X0,meet(a,sF6))),X1))),
inference(forward_demodulation,[],[f4210,f2]) ).
fof(f4227,plain,
! [X0,X1] : meet(meet(X0,sF2),X1) = meet(X0,meet(sF2,meet(sF2,meet(join(X0,meet(a,sF6)),X1)))),
inference(forward_demodulation,[],[f4213,f2]) ).
fof(f4235,plain,
! [X0,X1] : meet(X0,meet(sF2,meet(join(X0,meet(a,sF6)),X1))) = meet(meet(X0,sF2),X1),
inference(forward_demodulation,[],[f4227,f435]) ).
fof(f4241,plain,
! [X0,X1] : meet(X0,meet(sF2,X1)) = meet(X0,meet(sF2,meet(join(X0,meet(a,sF6)),X1))),
inference(forward_demodulation,[],[f4235,f2]) ).
fof(f4246,plain,
! [X0,X1] : meet(X0,meet(X1,sF2)) = meet(X0,meet(sF2,X1)),
inference(forward_demodulation,[],[f4241,f2064]) ).
fof(f4427,plain,
! [X0] : join(sF6,X0) = join(sF6,join(sF1,X0)),
inference(superposition,[],[f287,f4186]) ).
fof(f4434,plain,
! [X0] : join(sF6,X0) = join(sF1,join(X0,sF6)),
inference(forward_demodulation,[],[f4427,f304]) ).
fof(f4445,plain,
! [X0] : join(sF1,sF6) = join(sF6,meet(sF1,X0)),
inference(superposition,[],[f284,f4434]) ).
fof(f4464,plain,
! [X0] : sF6 = join(sF6,meet(sF1,X0)),
inference(forward_demodulation,[],[f4445,f4186]) ).
fof(f4472,plain,
sF6 = meet(sF2,join(sF0,meet(a,sF6))),
inference(backward_demodulation,[],[f4192,f4464]) ).
fof(f4575,plain,
join(sF8,y2) = join(sF7,sF0),
inference(superposition,[],[f293,f22]) ).
fof(f4576,plain,
join(sF8,z2) = join(sF7,sF2),
inference(superposition,[],[f293,f26]) ).
fof(f4612,plain,
join(sF8,z2) = join(sF2,sF7),
inference(forward_demodulation,[],[f4576,f3]) ).
fof(f4613,plain,
join(sF8,y2) = join(sF0,sF7),
inference(forward_demodulation,[],[f4575,f3]) ).
fof(f4622,plain,
join(sF2,sF7) = join(z2,sF8),
inference(forward_demodulation,[],[f4612,f3]) ).
fof(f4623,plain,
join(sF0,sF7) = join(y2,sF8),
inference(forward_demodulation,[],[f4613,f3]) ).
fof(f4628,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,[],[f191,f97]) ).
fof(f4640,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,[],[f191,f6]) ).
fof(f4666,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(X1,meet(a,X0)),join(meet(a,meet(X0,X1)),a)),
inference(superposition,[],[f191,f222]) ).
fof(f4673,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,[],[f191,f5]) ).
fof(f4681,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))) = meet(join(X0,meet(a,meet(X0,X1))),join(meet(a,X0),X1)),
inference(superposition,[],[f191,f97]) ).
fof(f4708,plain,
! [X0] : join(meet(X0,join(sF0,meet(a,sF6))),meet(a,meet(sF2,join(X0,join(sF0,meet(a,sF6)))))) = meet(join(join(sF0,meet(a,sF6)),meet(a,meet(sF2,X0))),join(meet(a,sF6),X0)),
inference(superposition,[],[f191,f4472]) ).
fof(f4800,plain,
! [X0] : join(meet(X0,join(sF0,meet(a,sF6))),meet(a,meet(sF2,join(X0,join(sF0,meet(a,sF6)))))) = meet(join(meet(a,sF6),X0),join(meet(a,meet(sF2,X0)),join(sF0,meet(a,sF6)))),
inference(forward_demodulation,[],[f4708,f1774]) ).
fof(f4821,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),X0)),
inference(forward_demodulation,[],[f4681,f1774]) ).
fof(f4827,plain,
! [X0,X1] : join(meet(X0,a),meet(a,meet(X1,join(X0,a)))) = meet(a,join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f4673,f222]) ).
fof(f4830,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(X1,meet(a,X0)),join(a,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f4666,f1657]) ).
fof(f4856,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,[],[f4640,f1724]) ).
fof(f4866,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,[],[f4628,f1657]) ).
fof(f4898,plain,
! [X0] : join(meet(X0,join(sF0,meet(a,sF6))),meet(a,meet(sF2,join(X0,join(sF0,meet(a,sF6)))))) = meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(a,meet(sF2,X0))))),
inference(forward_demodulation,[],[f4800,f1724]) ).
fof(f4914,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))) = meet(join(meet(a,X0),X1),join(X0,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f4821,f1657]) ).
fof(f4918,plain,
! [X0,X1] : join(meet(X0,a),meet(a,X1)) = meet(a,join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f4827,f3110]) ).
fof(f4919,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(X1,meet(a,X0)),a),
inference(forward_demodulation,[],[f4830,f5]) ).
fof(f4942,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,[],[f4856,f4]) ).
fof(f4945,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(join(X1,meet(a,X0)),X0),
inference(forward_demodulation,[],[f4866,f349]) ).
fof(f4975,plain,
! [X0] : join(meet(X0,join(sF0,meet(a,sF6))),meet(a,meet(sF2,join(X0,join(sF0,meet(a,sF6)))))) = meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(sF2,meet(X0,a))))),
inference(forward_demodulation,[],[f4898,f384]) ).
fof(f4986,plain,
! [X0,X1] : join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))) = meet(join(meet(a,X0),X1),X0),
inference(forward_demodulation,[],[f4914,f349]) ).
fof(f4990,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,a),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(meet(a,join(meet(a,X2),X0)),X1)),
inference(backward_demodulation,[],[f3846,f4918]) ).
fof(f4996,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(a,join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f4919,f1774]) ).
fof(f5014,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,[],[f4942,f6]) ).
fof(f5017,plain,
! [X0,X1] : join(meet(X0,X1),meet(a,meet(X0,join(X0,X1)))) = meet(X0,join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f4945,f1774]) ).
fof(f5045,plain,
! [X0] : join(meet(X0,join(sF0,meet(a,sF6))),meet(a,meet(sF2,join(X0,join(sF0,meet(a,sF6)))))) = meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(sF1,X0)))),
inference(forward_demodulation,[],[f4975,f3415]) ).
fof(f5053,plain,
! [X0,X1] : meet(X0,join(X1,meet(a,X0))) = join(meet(X1,X0),meet(a,meet(X0,join(X1,X0)))),
inference(forward_demodulation,[],[f4986,f1774]) ).
fof(f5059,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,a),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(a,meet(join(meet(a,X2),X0),X1))),
inference(forward_demodulation,[],[f4990,f2]) ).
fof(f5060,plain,
! [X0,X1] : meet(a,join(meet(a,X0),X1)) = meet(join(meet(a,X1),meet(a,X0)),join(X1,a)),
inference(forward_demodulation,[],[f4996,f2141]) ).
fof(f5076,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,[],[f5014,f3]) ).
fof(f5077,plain,
! [X0,X1] : meet(X0,join(meet(a,X0),X1)) = join(meet(X0,X1),meet(a,X0)),
inference(forward_demodulation,[],[f5017,f6]) ).
fof(f5102,plain,
! [X0] : meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(sF1,X0)))) = join(meet(X0,join(sF0,meet(a,sF6))),meet(sF2,meet(join(join(sF0,meet(a,sF6)),X0),a))),
inference(forward_demodulation,[],[f5045,f1655]) ).
fof(f5110,plain,
! [X0,X1] : meet(X0,join(X1,meet(a,X0))) = join(meet(X1,X0),meet(a,X0)),
inference(forward_demodulation,[],[f5053,f129]) ).
fof(f5113,plain,
! [X0,X1] : meet(a,join(meet(a,X0),X1)) = meet(join(X1,a),join(meet(a,X0),meet(a,X1))),
inference(forward_demodulation,[],[f5060,f1774]) ).
fof(f5129,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,[],[f5076,f2149]) ).
fof(f5152,plain,
! [X0] : meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(sF1,X0)))) = join(meet(X0,join(sF0,meet(a,sF6))),meet(sF1,join(join(sF0,meet(a,sF6)),X0))),
inference(forward_demodulation,[],[f5102,f3415]) ).
fof(f5184,plain,
! [X0] : meet(join(meet(a,sF6),X0),join(sF0,join(meet(a,sF6),meet(sF1,X0)))) = join(meet(X0,join(sF0,meet(a,sF6))),meet(sF1,join(sF0,join(meet(a,sF6),X0)))),
inference(forward_demodulation,[],[f5152,f4]) ).
fof(f5304,plain,
! [X0] : meet(sF1,X0) = meet(sF2,meet(sF1,X0)),
inference(superposition,[],[f435,f377]) ).
fof(f5382,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,join(meet(a,sF6),X0)),
inference(backward_demodulation,[],[f4170,f5304]) ).
fof(f5569,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X2,X0)),
inference(superposition,[],[f1574,f99]) ).
fof(f5681,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(join(X3,X2),meet(X1,X0)),
inference(superposition,[],[f384,f1574]) ).
fof(f6179,plain,
! [X0] : meet(sF6,meet(a,X0)) = meet(sF0,meet(sF1,X0)),
inference(superposition,[],[f376,f377]) ).
fof(f6181,plain,
meet(sF0,sF1) = meet(sF6,a),
inference(superposition,[],[f376,f48]) ).
fof(f6183,plain,
meet(sF6,z2) = meet(sF0,z2),
inference(superposition,[],[f376,f219]) ).
fof(f6265,plain,
meet(sF0,z2) = meet(z2,sF6),
inference(forward_demodulation,[],[f6183,f1]) ).
fof(f6267,plain,
meet(a,sF6) = meet(sF0,sF1),
inference(forward_demodulation,[],[f6181,f1]) ).
fof(f6269,plain,
! [X0] : meet(sF0,meet(sF1,X0)) = meet(a,meet(X0,sF6)),
inference(forward_demodulation,[],[f6179,f384]) ).
fof(f6283,plain,
sF1 = meet(a,sF6),
inference(forward_demodulation,[],[f6267,f3701]) ).
fof(f6294,plain,
! [X0] : join(meet(sF2,X0),meet(sF1,join(sF2,X0))) = meet(sF2,join(sF1,X0)),
inference(backward_demodulation,[],[f4006,f6283]) ).
fof(f6297,plain,
! [X0] : join(meet(X0,sF2),meet(sF1,join(sF2,X0))) = meet(sF2,join(X0,sF1)),
inference(backward_demodulation,[],[f4064,f6283]) ).
fof(f6303,plain,
! [X0,X1] : join(meet(sF2,X0),join(meet(sF1,join(sF2,X0)),X1)) = join(X1,meet(sF2,join(X0,sF1))),
inference(backward_demodulation,[],[f4097,f6283]) ).
fof(f6314,plain,
join(z2,sF1) = meet(sF2,join(z2,sF1)),
inference(backward_demodulation,[],[f4166,f6283]) ).
fof(f6315,plain,
join(x2,sF1) = meet(sF2,join(x2,sF1)),
inference(backward_demodulation,[],[f4167,f6283]) ).
fof(f6332,plain,
! [X0] : meet(join(sF1,X0),join(sF0,join(sF1,meet(sF1,X0)))) = join(meet(X0,join(sF0,sF1)),meet(sF1,join(sF0,join(sF1,X0)))),
inference(backward_demodulation,[],[f5184,f6283]) ).
fof(f6337,plain,
! [X0] : meet(sF1,join(sF2,X0)) = meet(sF1,join(sF1,X0)),
inference(backward_demodulation,[],[f5382,f6283]) ).
fof(f6351,plain,
! [X0] : sF1 = meet(sF1,join(sF2,X0)),
inference(forward_demodulation,[],[f6337,f6]) ).
fof(f6353,plain,
! [X0] : meet(join(sF1,X0),join(sF0,join(sF1,meet(sF1,X0)))) = join(meet(X0,join(sF0,sF1)),sF1),
inference(forward_demodulation,[],[f6332,f473]) ).
fof(f6378,plain,
! [X0] : join(meet(sF2,X0),sF1) = meet(sF2,join(sF1,X0)),
inference(backward_demodulation,[],[f6294,f6351]) ).
fof(f6379,plain,
! [X0] : meet(sF2,join(X0,sF1)) = join(meet(X0,sF2),sF1),
inference(backward_demodulation,[],[f6297,f6351]) ).
fof(f6382,plain,
! [X0,X1] : join(X1,meet(sF2,join(X0,sF1))) = join(meet(sF2,X0),join(sF1,X1)),
inference(backward_demodulation,[],[f6303,f6351]) ).
fof(f6395,plain,
! [X0] : meet(join(sF1,X0),join(sF0,join(sF1,meet(sF1,X0)))) = join(sF1,meet(X0,join(sF0,sF1))),
inference(forward_demodulation,[],[f6353,f3]) ).
fof(f6410,plain,
! [X0,X1] : join(X1,meet(sF2,join(X0,sF1))) = join(sF1,join(X1,meet(sF2,X0))),
inference(forward_demodulation,[],[f6382,f304]) ).
fof(f6412,plain,
! [X0] : join(sF1,meet(X0,sF2)) = meet(sF2,join(X0,sF1)),
inference(forward_demodulation,[],[f6379,f3]) ).
fof(f6413,plain,
! [X0] : join(sF1,meet(sF2,X0)) = meet(sF2,join(sF1,X0)),
inference(forward_demodulation,[],[f6378,f3]) ).
fof(f6428,plain,
! [X0] : meet(join(sF1,X0),join(sF0,join(sF1,meet(sF1,X0)))) = join(sF1,meet(X0,sF0)),
inference(forward_demodulation,[],[f6395,f70]) ).
fof(f6448,plain,
! [X0] : join(sF1,meet(X0,sF0)) = meet(join(sF1,X0),join(sF0,meet(sF1,X0))),
inference(forward_demodulation,[],[f6428,f323]) ).
fof(f7170,plain,
! [X0] : join(x2,join(y2,X0)) = join(sF0,join(X0,y2)),
inference(superposition,[],[f290,f273]) ).
fof(f7177,plain,
! [X0] : join(sF0,X0) = join(sF0,join(X0,y2)),
inference(forward_demodulation,[],[f7170,f290]) ).
fof(f7431,plain,
! [X2,X0,X1] : meet(meet(join(X0,meet(a,X1)),X2),join(X1,X0)) = join(meet(meet(join(X0,meet(a,X1)),X2),join(X1,meet(a,X0))),meet(join(X0,meet(a,X1)),X2)),
inference(superposition,[],[f244,f435]) ).
fof(f7512,plain,
! [X2,X0,X1] : join(meet(join(X0,meet(a,X1)),X2),meet(meet(join(X0,meet(a,X1)),X2),join(X1,meet(a,X0)))) = meet(meet(join(X0,meet(a,X1)),X2),join(X1,X0)),
inference(forward_demodulation,[],[f7431,f3]) ).
fof(f7594,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,X1)),meet(X2,join(X1,X0))) = join(meet(join(X0,meet(a,X1)),X2),meet(meet(join(X0,meet(a,X1)),X2),join(X1,meet(a,X0)))),
inference(forward_demodulation,[],[f7512,f2]) ).
fof(f7656,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,X1)),meet(X2,join(X1,X0))) = meet(join(X0,meet(a,X1)),X2),
inference(forward_demodulation,[],[f7594,f5]) ).
fof(f7701,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,X1)),X2) = meet(join(X1,X0),meet(X2,join(meet(a,X1),X0))),
inference(forward_demodulation,[],[f7656,f5681]) ).
fof(f7924,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,join(join(X0,meet(X1,a)),meet(a,meet(a,join(X1,meet(a,X0)))))),meet(X2,meet(a,join(X0,X1)))),
inference(superposition,[],[f187,f248]) ).
fof(f7926,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,join(join(X0,meet(a,X1)),meet(a,meet(join(X1,meet(a,X0)),a)))),meet(X2,meet(a,join(X0,X1)))),
inference(superposition,[],[f187,f244]) ).
fof(f8003,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(join(X0,meet(a,X1)),meet(a,meet(join(X1,meet(a,X0)),a))))),
inference(forward_demodulation,[],[f7926,f3]) ).
fof(f8005,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(join(X0,meet(X1,a)),meet(a,meet(a,join(X1,meet(a,X0))))))),
inference(forward_demodulation,[],[f7924,f3]) ).
fof(f8073,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,join(meet(a,X1),meet(a,meet(join(X1,meet(a,X0)),a)))))),
inference(forward_demodulation,[],[f8003,f4]) ).
fof(f8075,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,join(meet(X1,a),meet(a,meet(a,join(X1,meet(a,X0)))))))),
inference(forward_demodulation,[],[f8005,f4]) ).
fof(f8129,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(join(meet(a,X1),meet(a,a)),join(X1,meet(a,X0)))))),
inference(forward_demodulation,[],[f8073,f2218]) ).
fof(f8131,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(meet(a,meet(a,join(X1,meet(a,X0)))),X1))))),
inference(forward_demodulation,[],[f8075,f4918]) ).
fof(f8168,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(join(meet(a,X1),meet(a,a)),join(X1,X0))))),
inference(forward_demodulation,[],[f8129,f2199]) ).
fof(f8170,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,meet(a,join(X1,meet(a,X0))))))))),
inference(forward_demodulation,[],[f8131,f1657]) ).
fof(f8192,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(meet(a,join(meet(a,a),X1)),join(X1,X0))))),
inference(forward_demodulation,[],[f8168,f5077]) ).
fof(f8194,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(X1,a)),meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))),
inference(forward_demodulation,[],[f8170,f435]) ).
fof(f8208,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,meet(join(meet(a,a),X1),join(X1,X0)))))),
inference(forward_demodulation,[],[f8192,f2]) ).
fof(f8210,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))) = meet(X2,join(X0,join(meet(X1,a),meet(a,join(X1,meet(a,X0)))))),
inference(forward_demodulation,[],[f8194,f4]) ).
fof(f8223,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,meet(join(a,X1),join(X1,X0)))))),
inference(forward_demodulation,[],[f8208,f97]) ).
fof(f8225,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))) = meet(X2,join(X0,join(meet(X1,a),meet(a,join(X0,X1))))),
inference(forward_demodulation,[],[f8210,f3663]) ).
fof(f8237,plain,
! [X2,X0,X1] : meet(X2,join(join(X0,meet(a,X1)),meet(join(X1,meet(a,X0)),a))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))),
inference(forward_demodulation,[],[f8223,f368]) ).
fof(f8239,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))) = meet(X2,join(X0,meet(a,join(meet(a,join(X0,X1)),X1)))),
inference(forward_demodulation,[],[f8225,f4918]) ).
fof(f8249,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))) = meet(X2,join(X0,join(meet(a,X1),meet(join(X1,meet(a,X0)),a)))),
inference(forward_demodulation,[],[f8237,f4]) ).
fof(f8251,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))) = meet(X2,join(X0,meet(a,join(X1,meet(a,join(X0,X1)))))),
inference(forward_demodulation,[],[f8239,f1657]) ).
fof(f8260,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))) = meet(X2,join(X0,meet(join(meet(a,X1),a),join(X1,meet(a,X0))))),
inference(forward_demodulation,[],[f8249,f2149]) ).
fof(f8269,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))) = meet(X2,join(X0,meet(join(meet(a,X1),a),join(X1,X0)))),
inference(forward_demodulation,[],[f8260,f2199]) ).
fof(f8277,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))) = meet(X2,join(X0,meet(join(a,meet(a,X1)),join(X1,X0)))),
inference(forward_demodulation,[],[f8269,f3]) ).
fof(f8285,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,join(X1,X0)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))),
inference(forward_demodulation,[],[f8277,f5]) ).
fof(f8352,plain,
join(sF0,sF7) = join(y2,join(sF0,sF7)),
inference(superposition,[],[f318,f4623]) ).
fof(f8359,plain,
join(sF0,sF7) = join(sF7,join(y2,sF0)),
inference(forward_demodulation,[],[f8352,f304]) ).
fof(f8367,plain,
join(sF0,y2) = join(sF0,sF7),
inference(forward_demodulation,[],[f8359,f3962]) ).
fof(f8370,plain,
sF0 = join(sF0,sF7),
inference(forward_demodulation,[],[f8367,f1883]) ).
fof(f8465,plain,
sF7 = meet(sF7,sF0),
inference(superposition,[],[f129,f8370]) ).
fof(f8479,plain,
sF7 = meet(sF0,sF7),
inference(forward_demodulation,[],[f8465,f1]) ).
fof(f8648,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(a,meet(a,meet(X0,X1))),join(meet(a,X0),X1)),
inference(superposition,[],[f193,f222]) ).
fof(f8743,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(meet(a,X0),X1),join(meet(a,meet(X0,X1)),a)),
inference(forward_demodulation,[],[f8648,f1774]) ).
fof(f8865,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(meet(a,X0),X1),join(a,meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f8743,f1657]) ).
fof(f8957,plain,
! [X0,X1] : join(meet(a,X1),meet(a,meet(X0,join(a,X1)))) = meet(join(meet(a,X0),X1),a),
inference(forward_demodulation,[],[f8865,f5]) ).
fof(f9029,plain,
! [X0,X1] : meet(a,join(X1,meet(a,X0))) = join(meet(a,X1),meet(a,meet(X0,join(a,X1)))),
inference(forward_demodulation,[],[f8957,f1774]) ).
fof(f9090,plain,
! [X0,X1] : meet(a,join(X1,meet(a,X0))) = meet(join(meet(a,X1),meet(a,X0)),join(X1,a)),
inference(forward_demodulation,[],[f9029,f2141]) ).
fof(f9146,plain,
! [X0,X1] : meet(a,join(X1,meet(a,X0))) = meet(join(X1,a),join(meet(a,X0),meet(a,X1))),
inference(forward_demodulation,[],[f9090,f1774]) ).
fof(f9298,plain,
join(sF4,sF8) = join(y2,join(sF2,sF7)),
inference(superposition,[],[f292,f4622]) ).
fof(f9318,plain,
join(sF4,sF8) = join(sF7,join(y2,sF2)),
inference(forward_demodulation,[],[f9298,f304]) ).
fof(f9325,plain,
join(sF4,sF8) = join(sF2,y2),
inference(forward_demodulation,[],[f9318,f3962]) ).
fof(f9395,plain,
! [X2,X0,X1] : meet(join(meet(a,meet(X2,X0)),X1),join(X0,meet(a,meet(X2,X1)))) = join(join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))),meet(join(meet(a,meet(X2,X0)),X1),join(X0,meet(a,meet(X2,X1))))),
inference(superposition,[],[f1172,f193]) ).
fof(f9502,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(meet(X0,X1),join(X2,meet(X1,X0))),
inference(superposition,[],[f304,f1172]) ).
fof(f9610,plain,
! [X2,X0,X1] : meet(join(meet(a,meet(X2,X0)),X1),join(X0,meet(a,meet(X2,X1)))) = join(meet(X0,X1),join(meet(a,meet(X2,join(X0,X1))),meet(join(meet(a,meet(X2,X0)),X1),join(X0,meet(a,meet(X2,X1)))))),
inference(forward_demodulation,[],[f9395,f4]) ).
fof(f9694,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,meet(X2,X1))),join(X1,meet(a,meet(X2,X0)))) = join(meet(X0,X1),join(meet(a,meet(X2,join(X0,X1))),meet(join(X0,meet(a,meet(X2,X1))),join(X1,meet(a,meet(X2,X0)))))),
inference(forward_demodulation,[],[f9610,f1774]) ).
fof(f9734,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),join(meet(a,meet(X2,join(X0,X1))),join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f9694,f1847]) ).
fof(f9765,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),join(meet(X0,X1),join(meet(a,meet(X2,join(X0,X1))),meet(a,meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f9734,f1398]) ).
fof(f9783,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),join(meet(a,meet(X2,join(X0,X1))),meet(a,meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f9765,f318]) ).
fof(f9790,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(meet(X2,join(X0,X1)),join(a,meet(a,meet(X2,join(X0,X1)))))),
inference(forward_demodulation,[],[f9783,f5110]) ).
fof(f9796,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X2,meet(join(X0,X1),join(a,meet(a,meet(X2,join(X0,X1))))))),
inference(forward_demodulation,[],[f9790,f2]) ).
fof(f9802,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X2,meet(join(X0,X1),a))),
inference(forward_demodulation,[],[f9796,f5]) ).
fof(f9808,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(a,meet(X2,join(X0,X1)))) = join(meet(X0,X1),meet(X2,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f9802,f5569]) ).
fof(f10388,plain,
! [X2,X3,X0,X1] : join(X1,X3) = join(X1,join(X3,meet(X0,meet(X1,X2)))),
inference(superposition,[],[f331,f384]) ).
fof(f10547,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,[],[f5129,f10388]) ).
fof(f11260,plain,
! [X0] : sF0 = join(sF0,meet(sF1,X0)),
inference(superposition,[],[f5,f375]) ).
fof(f11273,plain,
! [X0] : meet(sF1,X0) = meet(sF0,meet(sF1,X0)),
inference(superposition,[],[f435,f375]) ).
fof(f11278,plain,
! [X0] : meet(sF1,X0) = meet(a,meet(X0,sF6)),
inference(backward_demodulation,[],[f6269,f11273]) ).
fof(f11288,plain,
! [X0] : join(sF1,meet(X0,sF0)) = meet(join(sF1,X0),sF0),
inference(backward_demodulation,[],[f6448,f11260]) ).
fof(f11327,plain,
! [X0] : join(sF1,meet(X0,sF0)) = meet(sF0,join(X0,sF1)),
inference(forward_demodulation,[],[f11288,f1774]) ).
fof(f12080,plain,
! [X0] : meet(sF4,a) = meet(sF1,join(sF4,X0)),
inference(superposition,[],[f378,f449]) ).
fof(f12081,plain,
! [X0] : sF1 = meet(sF1,join(sF4,X0)),
inference(forward_demodulation,[],[f12080,f49]) ).
fof(f12767,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,X0)),meet(X0,X1)),
inference(superposition,[],[f241,f3110]) ).
fof(f12851,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X0,X1),meet(X1,join(X2,X0))),
inference(forward_demodulation,[],[f12767,f3]) ).
fof(f13480,plain,
meet(sF7,sF6) = meet(y2,meet(sF0,z2)),
inference(superposition,[],[f374,f6265]) ).
fof(f13508,plain,
meet(sF7,sF0) = meet(sF7,sF6),
inference(forward_demodulation,[],[f13480,f3420]) ).
fof(f13517,plain,
meet(sF0,sF7) = meet(sF7,sF6),
inference(forward_demodulation,[],[f13508,f1]) ).
fof(f13524,plain,
sF7 = meet(sF7,sF6),
inference(forward_demodulation,[],[f13517,f8479]) ).
fof(f13565,plain,
! [X0,X1] : join(meet(a,join(sF1,X0)),X1) = join(meet(X0,a),join(sF1,X1)),
inference(superposition,[],[f287,f2337]) ).
fof(f13584,plain,
! [X0,X1] : join(meet(a,join(sF1,X0)),X1) = join(sF1,join(X1,meet(X0,a))),
inference(forward_demodulation,[],[f13565,f304]) ).
fof(f13919,plain,
meet(sF0,join(meet(a,sF0),x2)) = join(x2,meet(a,sF0)),
inference(superposition,[],[f5077,f145]) ).
fof(f13942,plain,
! [X0,X1] : meet(X0,join(meet(X0,a),X1)) = join(meet(X0,X1),meet(X0,a)),
inference(superposition,[],[f5077,f1]) ).
fof(f13998,plain,
! [X0,X1] : join(meet(a,X0),meet(X0,X1)) = meet(X0,join(meet(a,X0),X1)),
inference(superposition,[],[f3,f5077]) ).
fof(f14028,plain,
! [X2,X0] : join(meet(a,X0),meet(X2,X0)) = meet(X0,join(meet(a,X0),X2)),
inference(backward_demodulation,[],[f508,f13998]) ).
fof(f14100,plain,
meet(sF0,join(meet(sF0,a),x2)) = join(x2,meet(sF0,a)),
inference(forward_demodulation,[],[f13919,f1]) ).
fof(f14205,plain,
join(x2,sF1) = meet(sF0,join(sF1,x2)),
inference(forward_demodulation,[],[f14100,f43]) ).
fof(f14280,plain,
join(x2,sF1) = meet(sF0,join(x2,sF1)),
inference(forward_demodulation,[],[f14205,f1657]) ).
fof(f14442,plain,
! [X0,X1] : join(meet(a,join(X0,X1)),X0) = meet(join(X0,X1),join(meet(a,join(X0,X1)),X0)),
inference(superposition,[],[f14028,f6]) ).
fof(f14623,plain,
! [X0,X1] : join(meet(a,join(X0,X1)),X0) = meet(join(X0,X1),join(X0,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f14442,f1657]) ).
fof(f14737,plain,
! [X0,X1] : join(X0,meet(a,join(X0,X1))) = meet(join(X0,X1),join(X0,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f14623,f3]) ).
fof(f15484,plain,
sF6 = join(sF6,sF7),
inference(superposition,[],[f241,f13524]) ).
fof(f15505,plain,
sF6 = join(sF7,sF6),
inference(forward_demodulation,[],[f15484,f3]) ).
fof(f15641,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,[],[f1837,f435]) ).
fof(f15683,plain,
! [X0] : join(meet(sF1,X0),meet(a,join(sF1,X0))) = meet(meet(a,join(sF1,X0)),join(meet(a,sF1),X0)),
inference(superposition,[],[f1837,f2254]) ).
fof(f15719,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,[],[f1837,f247]) ).
fof(f15742,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(meet(join(meet(a,X0),X1),join(X1,meet(a,X0))),join(meet(X0,X1),meet(a,join(X0,X1)))),
inference(superposition,[],[f244,f1837]) ).
fof(f15743,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,[],[f245,f1837]) ).
fof(f15766,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,f1837]) ).
fof(f15801,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,[],[f15766,f4]) ).
fof(f15817,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,[],[f15743,f4]) ).
fof(f15818,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(join(meet(X0,X1),meet(a,join(X0,X1))),meet(join(meet(a,X0),X1),join(X1,meet(a,X0)))),
inference(forward_demodulation,[],[f15742,f3]) ).
fof(f15835,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,[],[f15719,f2053]) ).
fof(f15869,plain,
! [X0] : join(meet(sF1,X0),meet(a,join(sF1,X0))) = meet(a,meet(join(sF1,X0),join(meet(a,sF1),X0))),
inference(forward_demodulation,[],[f15683,f2]) ).
fof(f15896,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,[],[f15641,f1996]) ).
fof(f15912,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,join(meet(a,join(X0,X1)),meet(a,X1))),
inference(forward_demodulation,[],[f15801,f1358]) ).
fof(f15927,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,[],[f15817,f1960]) ).
fof(f15928,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),meet(join(meet(a,X0),X1),join(X1,meet(a,X0))))),
inference(forward_demodulation,[],[f15818,f4]) ).
fof(f15945,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,[],[f15835,f431]) ).
fof(f15971,plain,
! [X0] : meet(a,join(X0,meet(a,sF1))) = join(meet(sF1,X0),meet(a,join(sF1,X0))),
inference(forward_demodulation,[],[f15869,f1996]) ).
fof(f16001,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,join(meet(a,X1),meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f15912,f3]) ).
fof(f16016,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,[],[f15927,f1314]) ).
fof(f16017,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),join(meet(a,X0),X1))),
inference(forward_demodulation,[],[f15928,f1960]) ).
fof(f16034,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,[],[f15945,f4]) ).
fof(f16053,plain,
! [X0] : meet(a,join(X0,meet(a,sF1))) = join(sF1,join(meet(a,X0),meet(sF1,X0))),
inference(forward_demodulation,[],[f15971,f2356]) ).
fof(f16078,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(join(meet(a,X1),a),join(X1,X0))),
inference(forward_demodulation,[],[f16001,f2102]) ).
fof(f16093,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,[],[f16016,f285]) ).
fof(f16094,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(X1,join(meet(X0,X1),join(meet(a,join(X0,X1)),meet(a,X0)))),
inference(forward_demodulation,[],[f16017,f1314]) ).
fof(f16111,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,[],[f16034,f2194]) ).
fof(f16127,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(X0,meet(a,sF1))),
inference(forward_demodulation,[],[f16053,f331]) ).
fof(f16149,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(join(a,meet(a,X1)),join(X1,X0))),
inference(forward_demodulation,[],[f16078,f10547]) ).
fof(f16162,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,[],[f16093,f3]) ).
fof(f16163,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(X1,join(meet(a,join(X0,X1)),meet(a,X0))),
inference(forward_demodulation,[],[f16094,f285]) ).
fof(f16176,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,[],[f16111,f3677]) ).
fof(f16188,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(X0,sF1)),
inference(forward_demodulation,[],[f16127,f2250]) ).
fof(f16208,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(a,join(X1,X0))),
inference(forward_demodulation,[],[f16149,f5]) ).
fof(f16221,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,[],[f16162,f2131]) ).
fof(f16222,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X1,X0)) = join(X1,join(meet(a,X0),meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f16163,f3]) ).
fof(f16233,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,[],[f16176,f13942]) ).
fof(f16258,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(a,X0))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X1,meet(a,X0)))),
inference(backward_demodulation,[],[f2211,f16208]) ).
fof(f16267,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,join(X1,meet(a,X0))))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X1,meet(a,X0)))))))),
inference(backward_demodulation,[],[f8251,f16208]) ).
fof(f16268,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,X1))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,X1)))),
inference(backward_demodulation,[],[f8285,f16208]) ).
fof(f16286,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,[],[f16221,f1774]) ).
fof(f16287,plain,
! [X0,X1] : join(X1,meet(join(meet(a,X0),a),join(X0,X1))) = meet(join(meet(a,X0),X1),join(X1,X0)),
inference(forward_demodulation,[],[f16222,f2131]) ).
fof(f16294,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,[],[f16233,f2]) ).
fof(f16328,plain,
! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(join(meet(a,X0),a),join(X0,X1))),
inference(forward_demodulation,[],[f16286,f3632]) ).
fof(f16329,plain,
! [X0,X1] : join(X1,meet(join(meet(a,X0),a),join(X0,X1))) = meet(join(X1,X0),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f16287,f1774]) ).
fof(f16335,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,[],[f16294,f97]) ).
fof(f16363,plain,
! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(join(a,meet(a,X0)),join(X0,X1))),
inference(forward_demodulation,[],[f16328,f10547]) ).
fof(f16364,plain,
! [X0,X1] : join(X1,meet(join(a,meet(a,X0)),join(X0,X1))) = meet(join(X1,X0),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f16329,f10547]) ).
fof(f16369,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,[],[f16335,f368]) ).
fof(f16393,plain,
! [X0,X1] : join(meet(a,X0),X1) = join(X1,meet(a,join(X0,X1))),
inference(forward_demodulation,[],[f16363,f5]) ).
fof(f16394,plain,
! [X0,X1] : join(X1,meet(a,join(X0,X1))) = meet(join(X1,X0),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f16364,f5]) ).
fof(f16399,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,[],[f16369,f16208]) ).
fof(f16412,plain,
! [X0,X1] : join(X1,meet(a,X0)) = meet(join(X1,X0),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f16394,f16208]) ).
fof(f16417,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,[],[f16399,f3214]) ).
fof(f16428,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,[],[f16417,f15896]) ).
fof(f16438,plain,
! [X0,X1] : meet(a,join(X0,meet(a,X1))) = meet(a,join(X1,X0)),
inference(forward_demodulation,[],[f16428,f248]) ).
fof(f16454,plain,
! [X0,X1] : meet(a,join(X0,X1)) = meet(join(X1,a),join(meet(a,X0),meet(a,X1))),
inference(backward_demodulation,[],[f9146,f16438]) ).
fof(f16464,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,meet(a,join(X0,X1))))))),
inference(backward_demodulation,[],[f16267,f16438]) ).
fof(f16537,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(join(X0,X1),X1))))),
inference(forward_demodulation,[],[f16464,f16438]) ).
fof(f16541,plain,
! [X0,X1] : meet(a,join(X0,X1)) = meet(a,join(meet(a,X0),X1)),
inference(backward_demodulation,[],[f5113,f16454]) ).
fof(f16553,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,join(X0,X1)))) = join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,join(X0,X1)))))),
inference(forward_demodulation,[],[f16537,f1657]) ).
fof(f16557,plain,
! [X0,X1] : meet(a,join(X1,X0)) = join(meet(X0,a),meet(a,X1)),
inference(backward_demodulation,[],[f4918,f16541]) ).
fof(f16581,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,join(X1,X0))))) = meet(X2,join(X0,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f16553,f273]) ).
fof(f16593,plain,
! [X2,X0,X1] : join(meet(X2,meet(a,join(X0,X1))),meet(X2,join(X0,meet(a,X1)))) = meet(X2,join(X0,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f16581,f16208]) ).
fof(f16602,plain,
! [X2,X0,X1] : meet(X2,join(X0,meet(a,X1))) = meet(X2,join(X0,meet(a,join(X0,X1)))),
inference(forward_demodulation,[],[f16593,f16268]) ).
fof(f16614,plain,
! [X0,X1] : meet(join(X0,X1),join(X0,meet(a,X1))) = join(X0,meet(a,join(X0,X1))),
inference(backward_demodulation,[],[f14737,f16602]) ).
fof(f16623,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(a,join(X0,X1))),
inference(forward_demodulation,[],[f16614,f16412]) ).
fof(f16664,plain,
! [X2,X0,X1] : join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(X0,join(X1,X2)))) = join(meet(a,meet(join(X1,meet(a,X2)),X0)),meet(X0,join(X2,meet(a,X1)))),
inference(superposition,[],[f16393,f245]) ).
fof(f16674,plain,
join(y2,meet(a,sF0)) = join(meet(a,x2),y2),
inference(superposition,[],[f16393,f22]) ).
fof(f16675,plain,
join(z2,meet(a,sF2)) = join(meet(a,x2),z2),
inference(superposition,[],[f16393,f26]) ).
fof(f16678,plain,
join(meet(a,y2),z2) = join(z2,meet(a,sF4)),
inference(superposition,[],[f16393,f31]) ).
fof(f16708,plain,
join(x2,meet(a,sF8)) = join(meet(a,sF7),x2),
inference(superposition,[],[f16393,f46]) ).
fof(f16716,plain,
! [X0,X1] : join(meet(a,X1),X0) = join(X0,meet(a,join(X0,X1))),
inference(superposition,[],[f16393,f1657]) ).
fof(f16752,plain,
! [X2,X0,X1] : meet(meet(a,join(X0,X1)),X2) = meet(meet(a,join(X0,X1)),meet(X2,join(meet(a,X0),X1))),
inference(superposition,[],[f3110,f16393]) ).
fof(f16754,plain,
! [X2,X0,X1] : join(X2,meet(a,join(X0,meet(X1,X2)))) = join(X2,join(meet(a,X0),meet(X1,X2))),
inference(superposition,[],[f285,f16393]) ).
fof(f16758,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,[],[f1837,f16393]) ).
fof(f16780,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,[],[f16758,f1774]) ).
fof(f16784,plain,
! [X2,X0,X1] : join(X2,meet(a,X0)) = join(X2,meet(a,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f16754,f3061]) ).
fof(f16786,plain,
! [X2,X0,X1] : meet(meet(a,join(X0,X1)),X2) = meet(a,meet(join(X0,X1),meet(X2,join(meet(a,X0),X1)))),
inference(forward_demodulation,[],[f16752,f2]) ).
fof(f16820,plain,
join(x2,meet(a,sF8)) = join(x2,meet(a,sF7)),
inference(forward_demodulation,[],[f16708,f3]) ).
fof(f16838,plain,
join(meet(a,y2),z2) = join(z2,meet(sF4,a)),
inference(forward_demodulation,[],[f16678,f1]) ).
fof(f16841,plain,
join(z2,meet(a,sF2)) = join(z2,meet(a,x2)),
inference(forward_demodulation,[],[f16675,f3]) ).
fof(f16842,plain,
join(y2,meet(a,sF0)) = join(y2,meet(a,x2)),
inference(forward_demodulation,[],[f16674,f3]) ).
fof(f16850,plain,
! [X2,X0,X1] : join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(X0,join(X1,X2)))) = join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(join(X1,meet(a,X2)),X0))),
inference(forward_demodulation,[],[f16664,f3]) ).
fof(f16873,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,[],[f16780,f1657]) ).
fof(f16880,plain,
! [X2,X0,X1] : meet(meet(a,join(X0,X1)),X2) = meet(a,meet(join(X1,meet(a,X0)),X2)),
inference(forward_demodulation,[],[f16786,f7701]) ).
fof(f16908,plain,
join(x2,meet(a,sF8)) = join(x2,meet(sF7,a)),
inference(forward_demodulation,[],[f16820,f1]) ).
fof(f16925,plain,
join(z2,sF1) = join(meet(a,y2),z2),
inference(forward_demodulation,[],[f16838,f49]) ).
fof(f16928,plain,
join(z2,meet(sF2,a)) = join(z2,meet(a,x2)),
inference(forward_demodulation,[],[f16841,f1]) ).
fof(f16929,plain,
join(y2,meet(sF0,a)) = join(y2,meet(a,x2)),
inference(forward_demodulation,[],[f16842,f1]) ).
fof(f16950,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,[],[f16873,f435]) ).
fof(f16954,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),X2)) = meet(a,meet(join(X1,meet(a,X0)),X2)),
inference(forward_demodulation,[],[f16880,f2]) ).
fof(f16990,plain,
join(z2,sF1) = join(z2,meet(a,y2)),
inference(forward_demodulation,[],[f16925,f3]) ).
fof(f16991,plain,
join(z2,sF1) = join(z2,meet(a,x2)),
inference(forward_demodulation,[],[f16928,f48]) ).
fof(f16992,plain,
join(y2,sF1) = join(y2,meet(a,x2)),
inference(forward_demodulation,[],[f16929,f43]) ).
fof(f17005,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,[],[f16950,f16784]) ).
fof(f17009,plain,
! [X2,X0,X1] : join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(X0,join(X1,X2)))) = join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(join(X2,X1),X0))),
inference(backward_demodulation,[],[f16850,f16954]) ).
fof(f17058,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,[],[f17005,f1774]) ).
fof(f17093,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,[],[f17058,f3]) ).
fof(f17104,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,[],[f17093,f3375]) ).
fof(f17111,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,[],[f17104,f3]) ).
fof(f17115,plain,
! [X0,X1] : join(meet(a,X1),meet(a,join(X1,meet(a,X0)))) = join(meet(a,X0),meet(a,X1)),
inference(forward_demodulation,[],[f17111,f1996]) ).
fof(f17119,plain,
! [X0,X1] : join(meet(a,X0),meet(a,X1)) = meet(join(meet(a,X1),a),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f17115,f2131]) ).
fof(f17131,plain,
! [X0,X1] : join(meet(a,X0),meet(a,X1)) = meet(join(a,meet(a,X1)),join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f17119,f10547]) ).
fof(f17140,plain,
! [X0,X1] : meet(a,join(X1,meet(a,X0))) = join(meet(a,X0),meet(a,X1)),
inference(forward_demodulation,[],[f17131,f5]) ).
fof(f17142,plain,
! [X0,X1] : meet(a,join(X0,X1)) = join(meet(a,X0),meet(a,X1)),
inference(forward_demodulation,[],[f17140,f16438]) ).
fof(f17301,plain,
! [X2,X0,X1] : meet(meet(a,join(X1,X0)),X2) = meet(meet(a,join(X1,X0)),meet(X2,join(X0,meet(a,X1)))),
inference(superposition,[],[f3110,f16208]) ).
fof(f17339,plain,
! [X2,X0,X1] : meet(meet(a,join(X1,X0)),X2) = meet(a,meet(join(X1,X0),meet(X2,join(X0,meet(a,X1))))),
inference(forward_demodulation,[],[f17301,f2]) ).
fof(f17424,plain,
! [X2,X0,X1] : meet(meet(a,join(X1,X0)),X2) = meet(a,meet(join(meet(a,X1),X0),X2)),
inference(forward_demodulation,[],[f17339,f3628]) ).
fof(f17492,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),X2)) = meet(a,meet(join(meet(a,X1),X0),X2)),
inference(forward_demodulation,[],[f17424,f2]) ).
fof(f17540,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,a),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(a,meet(join(X2,X0),X1))),
inference(backward_demodulation,[],[f5059,f17492]) ).
fof(f17600,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,a),X2)) = join(meet(X0,join(X2,meet(a,X1))),meet(a,meet(X0,join(X1,X2)))),
inference(backward_demodulation,[],[f17009,f17540]) ).
fof(f17681,plain,
join(x2,meet(a,sF0)) = join(meet(a,y2),x2),
inference(superposition,[],[f16716,f22]) ).
fof(f17682,plain,
join(x2,meet(a,sF2)) = join(meet(a,z2),x2),
inference(superposition,[],[f16716,f26]) ).
fof(f17685,plain,
join(y2,meet(a,sF4)) = join(meet(a,z2),y2),
inference(superposition,[],[f16716,f31]) ).
fof(f17715,plain,
join(meet(a,x2),sF7) = join(sF7,meet(a,sF8)),
inference(superposition,[],[f16716,f46]) ).
fof(f17752,plain,
! [X2,X0,X1] : join(X2,join(meet(a,X0),X1)) = join(X1,join(meet(a,join(X1,X0)),X2)),
inference(superposition,[],[f304,f16716]) ).
fof(f17832,plain,
join(sF7,meet(a,sF8)) = join(sF7,meet(a,x2)),
inference(forward_demodulation,[],[f17715,f3]) ).
fof(f17861,plain,
join(y2,meet(a,sF4)) = join(y2,meet(a,z2)),
inference(forward_demodulation,[],[f17685,f3]) ).
fof(f17862,plain,
join(x2,meet(a,sF2)) = join(x2,meet(a,z2)),
inference(forward_demodulation,[],[f17682,f3]) ).
fof(f17863,plain,
join(x2,meet(a,sF0)) = join(x2,meet(a,y2)),
inference(forward_demodulation,[],[f17681,f3]) ).
fof(f17964,plain,
join(y2,meet(sF4,a)) = join(y2,meet(a,z2)),
inference(forward_demodulation,[],[f17861,f1]) ).
fof(f17965,plain,
join(x2,meet(sF2,a)) = join(x2,meet(a,z2)),
inference(forward_demodulation,[],[f17862,f1]) ).
fof(f17966,plain,
join(x2,meet(sF0,a)) = join(x2,meet(a,y2)),
inference(forward_demodulation,[],[f17863,f1]) ).
fof(f18038,plain,
join(y2,sF1) = join(y2,meet(a,z2)),
inference(forward_demodulation,[],[f17964,f49]) ).
fof(f18039,plain,
join(x2,sF1) = join(x2,meet(a,z2)),
inference(forward_demodulation,[],[f17965,f48]) ).
fof(f18040,plain,
join(x2,sF1) = join(x2,meet(a,y2)),
inference(forward_demodulation,[],[f17966,f43]) ).
fof(f18299,plain,
! [X0] : meet(X0,join(x2,y2)) = join(meet(X0,join(y2,sF1)),meet(X0,join(x2,meet(a,y2)))),
inference(superposition,[],[f192,f16992]) ).
fof(f18347,plain,
! [X0] : meet(X0,join(x2,y2)) = join(meet(X0,join(y2,sF1)),meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f18299,f18040]) ).
fof(f18369,plain,
! [X0] : meet(X0,join(x2,y2)) = join(meet(X0,join(x2,sF1)),meet(X0,join(y2,sF1))),
inference(forward_demodulation,[],[f18347,f3]) ).
fof(f18386,plain,
! [X0] : meet(X0,sF0) = join(meet(X0,join(x2,sF1)),meet(X0,join(y2,sF1))),
inference(forward_demodulation,[],[f18369,f22]) ).
fof(f18443,plain,
! [X0] : meet(meet(a,sF8),X0) = meet(meet(a,sF8),meet(join(x2,meet(sF7,a)),X0)),
inference(superposition,[],[f369,f16908]) ).
fof(f18458,plain,
! [X0] : meet(meet(a,sF8),X0) = meet(a,meet(sF8,meet(join(x2,meet(sF7,a)),X0))),
inference(forward_demodulation,[],[f18443,f2]) ).
fof(f18483,plain,
! [X0] : meet(a,meet(sF8,meet(join(x2,meet(sF7,a)),X0))) = meet(a,meet(sF8,X0)),
inference(forward_demodulation,[],[f18458,f2]) ).
fof(f18539,plain,
join(sF2,meet(a,y2)) = join(x2,join(z2,sF1)),
inference(superposition,[],[f291,f16990]) ).
fof(f18552,plain,
join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(meet(a,z2),y2)),
inference(superposition,[],[f1837,f16990]) ).
fof(f18584,plain,
join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(y2,meet(a,z2))),
inference(forward_demodulation,[],[f18552,f1657]) ).
fof(f18597,plain,
join(sF2,sF1) = join(sF2,meet(a,y2)),
inference(forward_demodulation,[],[f18539,f291]) ).
fof(f18607,plain,
join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(z2,sF1),join(y2,sF1)),
inference(forward_demodulation,[],[f18584,f18038]) ).
fof(f18620,plain,
sF2 = join(sF2,meet(a,y2)),
inference(forward_demodulation,[],[f18597,f146]) ).
fof(f18625,plain,
join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(y2,sF1),join(sF1,z2)),
inference(forward_demodulation,[],[f18607,f1774]) ).
fof(f18641,plain,
join(meet(z2,y2),meet(a,join(z2,y2))) = meet(join(y2,sF1),join(z2,sF1)),
inference(forward_demodulation,[],[f18625,f1657]) ).
fof(f18651,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(meet(y2,z2),meet(a,join(y2,z2))),
inference(forward_demodulation,[],[f18641,f497]) ).
fof(f18658,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(meet(y2,z2),meet(a,sF4)),
inference(forward_demodulation,[],[f18651,f31]) ).
fof(f18661,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(meet(a,sF4),meet(y2,z2)),
inference(forward_demodulation,[],[f18658,f3]) ).
fof(f18664,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(meet(a,sF4),sF7),
inference(forward_demodulation,[],[f18661,f38]) ).
fof(f18666,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(sF7,meet(a,sF4)),
inference(forward_demodulation,[],[f18664,f3]) ).
fof(f18667,plain,
meet(join(y2,sF1),join(z2,sF1)) = join(sF7,meet(sF4,a)),
inference(forward_demodulation,[],[f18666,f1]) ).
fof(f18668,plain,
join(sF7,sF1) = meet(join(y2,sF1),join(z2,sF1)),
inference(forward_demodulation,[],[f18667,f49]) ).
fof(f18674,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(X0,join(z2,sF1)),meet(X0,join(x2,meet(a,z2)))),
inference(superposition,[],[f192,f16991]) ).
fof(f18679,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(join(x2,meet(a,z2)),X0),meet(X0,join(z2,sF1))),
inference(superposition,[],[f245,f16991]) ).
fof(f18717,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(X0,join(z2,sF1)),meet(join(x2,meet(a,z2)),X0)),
inference(forward_demodulation,[],[f18679,f3]) ).
fof(f18722,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(X0,join(z2,sF1)),meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f18674,f18039]) ).
fof(f18740,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(X0,join(z2,sF1)),meet(join(x2,sF1),X0)),
inference(forward_demodulation,[],[f18717,f18039]) ).
fof(f18745,plain,
! [X0] : meet(X0,join(x2,z2)) = join(meet(X0,join(x2,sF1)),meet(X0,join(z2,sF1))),
inference(forward_demodulation,[],[f18722,f3]) ).
fof(f18758,plain,
! [X0] : meet(X0,sF2) = join(meet(X0,join(z2,sF1)),meet(join(x2,sF1),X0)),
inference(forward_demodulation,[],[f18740,f26]) ).
fof(f18763,plain,
! [X0] : meet(X0,sF2) = join(meet(X0,join(x2,sF1)),meet(X0,join(z2,sF1))),
inference(forward_demodulation,[],[f18745,f26]) ).
fof(f19528,plain,
meet(a,y2) = meet(meet(a,y2),sF2),
inference(superposition,[],[f129,f18620]) ).
fof(f19549,plain,
meet(a,y2) = meet(a,meet(y2,sF2)),
inference(forward_demodulation,[],[f19528,f2]) ).
fof(f19568,plain,
meet(a,y2) = meet(sF2,meet(a,y2)),
inference(forward_demodulation,[],[f19549,f384]) ).
fof(f19583,plain,
meet(a,y2) = meet(sF1,y2),
inference(forward_demodulation,[],[f19568,f377]) ).
fof(f19594,plain,
meet(a,y2) = meet(y2,sF1),
inference(forward_demodulation,[],[f19583,f1]) ).
fof(f19956,plain,
join(sF0,z2) = join(sF2,y2),
inference(superposition,[],[f291,f3052]) ).
fof(f20000,plain,
join(sF0,sF4) = join(sF2,y2),
inference(forward_demodulation,[],[f19956,f3717]) ).
fof(f20024,plain,
join(sF0,sF4) = join(sF4,sF8),
inference(backward_demodulation,[],[f9325,f20000]) ).
fof(f20062,plain,
join(sF4,meet(a,join(sF0,sF4))) = join(meet(a,sF8),sF4),
inference(superposition,[],[f16716,f20024]) ).
fof(f20063,plain,
join(sF4,meet(a,join(sF0,sF4))) = join(sF4,meet(a,sF8)),
inference(forward_demodulation,[],[f20062,f3]) ).
fof(f20072,plain,
join(sF4,meet(a,sF0)) = join(sF4,meet(a,sF8)),
inference(forward_demodulation,[],[f20063,f16208]) ).
fof(f20079,plain,
join(sF4,meet(sF0,a)) = join(sF4,meet(a,sF8)),
inference(forward_demodulation,[],[f20072,f1]) ).
fof(f20083,plain,
join(sF4,sF1) = join(sF4,meet(a,sF8)),
inference(forward_demodulation,[],[f20079,f43]) ).
fof(f20086,plain,
sF4 = join(sF4,meet(a,sF8)),
inference(forward_demodulation,[],[f20083,f158]) ).
fof(f20207,plain,
! [X2,X0,X1] : meet(meet(a,join(X0,X1)),X2) = meet(meet(a,join(X0,X1)),meet(X2,join(X0,meet(a,X1)))),
inference(superposition,[],[f3110,f16623]) ).
fof(f20249,plain,
! [X2,X0,X1] : meet(meet(a,join(X0,X1)),X2) = meet(a,meet(join(X0,X1),meet(X2,join(X0,meet(a,X1))))),
inference(forward_demodulation,[],[f20207,f2]) ).
fof(f20354,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),X2)) = meet(a,meet(join(X0,X1),meet(X2,join(X0,meet(a,X1))))),
inference(forward_demodulation,[],[f20249,f2]) ).
fof(f20874,plain,
! [X0] : meet(a,join(X0,sF0)) = join(sF1,meet(a,X0)),
inference(superposition,[],[f16557,f43]) ).
fof(f20875,plain,
! [X0] : meet(a,join(X0,sF2)) = join(sF1,meet(a,X0)),
inference(superposition,[],[f16557,f48]) ).
fof(f20876,plain,
! [X0] : meet(a,join(X0,sF4)) = join(sF1,meet(a,X0)),
inference(superposition,[],[f16557,f49]) ).
fof(f21060,plain,
! [X0] : meet(a,join(X0,sF4)) = meet(a,join(X0,sF1)),
inference(backward_demodulation,[],[f16188,f20876]) ).
fof(f21061,plain,
! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF4)),
inference(backward_demodulation,[],[f20876,f20875]) ).
fof(f21062,plain,
! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF0)),
inference(backward_demodulation,[],[f20875,f20874]) ).
fof(f21132,plain,
! [X0] : meet(a,join(X0,sF2)) = meet(a,join(X0,sF1)),
inference(backward_demodulation,[],[f21060,f21061]) ).
fof(f21185,plain,
! [X0] : meet(a,join(X0,sF0)) = meet(a,join(X0,sF1)),
inference(forward_demodulation,[],[f21132,f21062]) ).
fof(f21286,plain,
! [X0] : meet(a,join(sF1,join(X0,sF2))) = join(sF1,meet(a,join(X0,sF0))),
inference(superposition,[],[f2254,f21062]) ).
fof(f21296,plain,
! [X0] : meet(a,join(sF2,X0)) = meet(a,join(X0,sF0)),
inference(superposition,[],[f1657,f21062]) ).
fof(f21340,plain,
! [X0] : meet(a,join(sF1,join(X0,sF2))) = meet(a,join(sF1,join(X0,sF0))),
inference(forward_demodulation,[],[f21286,f2254]) ).
fof(f21385,plain,
! [X0] : meet(a,join(sF1,join(X0,sF2))) = meet(a,join(sF0,join(sF1,X0))),
inference(forward_demodulation,[],[f21340,f1724]) ).
fof(f21417,plain,
! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF1,join(X0,sF2))),
inference(forward_demodulation,[],[f21385,f323]) ).
fof(f21440,plain,
! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF2,join(sF1,X0))),
inference(forward_demodulation,[],[f21417,f1724]) ).
fof(f21459,plain,
! [X0] : meet(a,join(sF2,X0)) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f21440,f325]) ).
fof(f22342,plain,
! [X0] : join(sF1,meet(a,meet(X0,sF2))) = meet(a,join(meet(sF2,X0),sF0)),
inference(superposition,[],[f20874,f4246]) ).
fof(f22383,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(join(sF1,X0),sF0)),
inference(superposition,[],[f16623,f20874]) ).
fof(f22428,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(sF2,join(sF1,X0))),
inference(forward_demodulation,[],[f22383,f21296]) ).
fof(f22465,plain,
! [X0] : join(sF1,meet(a,meet(X0,sF2))) = meet(a,join(sF2,meet(sF2,X0))),
inference(forward_demodulation,[],[f22342,f21296]) ).
fof(f22509,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(sF0,join(sF1,X0))),
inference(forward_demodulation,[],[f22428,f21459]) ).
fof(f22544,plain,
! [X0] : join(sF1,meet(a,meet(X0,sF2))) = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22465,f21459]) ).
fof(f22585,plain,
! [X0] : join(sF1,meet(a,X0)) = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f22509,f323]) ).
fof(f22614,plain,
! [X0] : meet(a,join(sF1,meet(X0,sF2))) = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22544,f2254]) ).
fof(f22650,plain,
! [X0] : meet(a,join(sF0,X0)) = meet(a,join(sF1,X0)),
inference(backward_demodulation,[],[f2254,f22585]) ).
fof(f22673,plain,
! [X0] : meet(a,meet(sF2,join(X0,sF1))) = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22614,f6412]) ).
fof(f22702,plain,
! [X0,X1] : join(sF1,join(meet(a,X0),X1)) = join(meet(a,join(sF0,X0)),X1),
inference(backward_demodulation,[],[f2353,f22650]) ).
fof(f22723,plain,
! [X0,X1] : join(sF1,join(X1,meet(X0,a))) = join(meet(a,join(sF0,X0)),X1),
inference(backward_demodulation,[],[f13584,f22650]) ).
fof(f22751,plain,
! [X0] : meet(sF2,meet(join(sF1,X0),a)) = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22673,f1655]) ).
fof(f22784,plain,
! [X0] : meet(sF1,join(sF1,X0)) = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22751,f3415]) ).
fof(f22804,plain,
! [X0] : sF1 = meet(a,join(sF0,meet(sF2,X0))),
inference(forward_demodulation,[],[f22784,f6]) ).
fof(f22851,plain,
! [X0,X1] : meet(a,join(X0,join(X1,sF1))) = meet(a,join(sF0,join(X0,X1))),
inference(superposition,[],[f22650,f304]) ).
fof(f23393,plain,
join(x2,join(sF0,sF4)) = join(sF2,sF0),
inference(superposition,[],[f3051,f3717]) ).
fof(f23457,plain,
join(sF0,sF2) = join(x2,join(sF0,sF4)),
inference(forward_demodulation,[],[f23393,f3]) ).
fof(f23484,plain,
join(sF0,sF2) = join(sF4,join(x2,sF0)),
inference(forward_demodulation,[],[f23457,f304]) ).
fof(f23498,plain,
join(sF0,sF2) = join(sF0,join(sF0,sF4)),
inference(forward_demodulation,[],[f23484,f3719]) ).
fof(f23504,plain,
join(sF0,sF4) = join(sF0,sF2),
inference(forward_demodulation,[],[f23498,f318]) ).
fof(f23509,plain,
join(sF0,z2) = join(sF0,sF2),
inference(backward_demodulation,[],[f3717,f23504]) ).
fof(f24222,plain,
! [X2,X0,X1] : join(X1,join(sF1,join(meet(a,X0),meet(X1,X2)))) = join(X1,meet(a,join(sF0,X0))),
inference(superposition,[],[f331,f22702]) ).
fof(f24232,plain,
! [X0,X1] : join(meet(a,join(sF0,X0)),X1) = join(sF1,join(meet(a,X0),join(meet(a,join(sF0,X0)),X1))),
inference(superposition,[],[f318,f22702]) ).
fof(f24260,plain,
! [X0,X1] : join(sF1,join(X1,meet(X0,a))) = join(sF1,join(meet(a,X0),join(sF1,join(X1,meet(X0,a))))),
inference(forward_demodulation,[],[f24232,f22723]) ).
fof(f24270,plain,
! [X0,X1] : join(X1,join(sF1,meet(a,X0))) = join(X1,meet(a,join(sF0,X0))),
inference(forward_demodulation,[],[f24222,f1373]) ).
fof(f24370,plain,
! [X0,X1] : join(sF1,join(X1,meet(X0,a))) = join(sF1,join(sF1,join(meet(a,X0),join(X1,meet(X0,a))))),
inference(forward_demodulation,[],[f24260,f1398]) ).
fof(f24380,plain,
! [X0,X1] : join(X1,meet(a,join(X0,sF0))) = join(X1,meet(a,join(sF0,X0))),
inference(forward_demodulation,[],[f24270,f20874]) ).
fof(f24467,plain,
! [X0,X1] : join(sF1,join(X1,meet(X0,a))) = join(sF1,join(meet(a,X0),join(X1,meet(X0,a)))),
inference(forward_demodulation,[],[f24370,f318]) ).
fof(f24551,plain,
! [X0,X1] : join(sF1,join(X1,meet(a,X0))) = join(sF1,join(X1,meet(X0,a))),
inference(forward_demodulation,[],[f24467,f9502]) ).
fof(f25263,plain,
meet(z2,a) = meet(sF1,z2),
inference(superposition,[],[f377,f3178]) ).
fof(f25316,plain,
meet(z2,sF1) = meet(z2,a),
inference(forward_demodulation,[],[f25263,f1]) ).
fof(f25339,plain,
meet(a,z2) = meet(z2,sF1),
inference(forward_demodulation,[],[f25316,f1]) ).
fof(f30456,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(join(X0,X1),meet(join(X1,X0),X2)),
inference(superposition,[],[f1655,f97]) ).
fof(f34478,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(join(X0,X1),meet(a,X0))),join(meet(X2,join(X0,meet(a,X1))),X3)),
inference(superposition,[],[f288,f16623]) ).
fof(f34550,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,[],[f288,f288]) ).
fof(f34561,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,[],[f288,f273]) ).
fof(f34665,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,[],[f34561,f288]) ).
fof(f34674,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,[],[f34550,f304]) ).
fof(f34737,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(join(X0,X1),meet(a,X0))))),
inference(forward_demodulation,[],[f34478,f304]) ).
fof(f34883,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,[],[f34674,f34665]) ).
fof(f34942,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(meet(a,X0),join(X0,X1))))),
inference(forward_demodulation,[],[f34737,f1657]) ).
fof(f35089,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(X0,join(X1,meet(a,X0)))))),
inference(forward_demodulation,[],[f34942,f1724]) ).
fof(f35192,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(X0,meet(a,X1))),join(X3,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f35089,f3061]) ).
fof(f35267,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(join(X0,X1),X0)),X3) = join(meet(X2,join(X0,X1)),join(meet(X2,join(X0,meet(a,X1))),X3)),
inference(forward_demodulation,[],[f35192,f304]) ).
fof(f35311,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X1,X0)),X3) = join(meet(X2,join(join(X0,X1),X0)),X3),
inference(forward_demodulation,[],[f35267,f34883]) ).
fof(f35349,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X1,X0)),X3) = join(meet(X2,join(X0,join(X0,X1))),X3),
inference(forward_demodulation,[],[f35311,f1657]) ).
fof(f35383,plain,
! [X2,X3,X0,X1] : join(meet(X2,join(X0,X1)),X3) = join(meet(X2,join(X1,X0)),X3),
inference(forward_demodulation,[],[f35349,f318]) ).
fof(f39371,plain,
meet(y2,join(z2,sF1)) = meet(y2,join(sF7,sF1)),
inference(superposition,[],[f368,f18668]) ).
fof(f42693,plain,
! [X2,X0,X1] : meet(meet(join(meet(a,X2),X1),X0),join(X1,X2)) = join(meet(X0,join(X1,meet(a,X2))),meet(meet(join(meet(a,X2),X1),X0),join(X2,meet(a,X1)))),
inference(superposition,[],[f245,f30456]) ).
fof(f42705,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X2,X3)) = meet(join(X3,X2),meet(join(X1,X0),join(X2,X3))),
inference(superposition,[],[f1655,f30456]) ).
fof(f42762,plain,
! [X2,X3,X0,X1] : meet(join(X0,X1),join(X2,X3)) = meet(join(X3,X2),join(X1,X0)),
inference(forward_demodulation,[],[f42705,f2197]) ).
fof(f42765,plain,
! [X2,X0,X1] : meet(meet(join(meet(a,X2),X1),X0),join(X1,X2)) = join(meet(X0,join(X1,meet(a,X2))),meet(join(meet(a,X2),X1),meet(X0,join(X2,meet(a,X1))))),
inference(forward_demodulation,[],[f42693,f2]) ).
fof(f43015,plain,
! [X2,X0,X1] : meet(meet(join(meet(a,X2),X1),X0),join(X1,X2)) = join(meet(X0,join(X1,meet(a,X2))),meet(join(X2,meet(a,X1)),meet(X0,join(X1,meet(a,X2))))),
inference(forward_demodulation,[],[f42765,f5681]) ).
fof(f43239,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(a,X2))) = meet(meet(join(meet(a,X2),X1),X0),join(X1,X2)),
inference(forward_demodulation,[],[f43015,f241]) ).
fof(f43391,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(a,X2))) = meet(join(meet(a,X2),X1),meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f43239,f2]) ).
fof(f43534,plain,
! [X2,X0,X1] : meet(X0,join(X1,meet(a,X2))) = meet(join(X1,X2),meet(X0,join(X1,meet(a,X2)))),
inference(forward_demodulation,[],[f43391,f5681]) ).
fof(f43620,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),X2)) = meet(a,meet(X2,join(X0,meet(a,X1)))),
inference(backward_demodulation,[],[f20354,f43534]) ).
fof(f43862,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(X0,meet(a,join(z2,sF1))),join(meet(a,meet(sF2,X0)),join(z2,sF1))),
inference(superposition,[],[f193,f6314]) ).
fof(f43896,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(X0,meet(a,join(z2,sF1))),join(z2,join(sF1,meet(a,meet(sF2,X0))))),
inference(forward_demodulation,[],[f43862,f1724]) ).
fof(f43919,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(X0,meet(a,join(z2,sF1))),join(z2,meet(a,join(meet(sF2,X0),sF0)))),
inference(forward_demodulation,[],[f43896,f20874]) ).
fof(f43936,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(X0,meet(a,join(z2,sF1))),join(z2,meet(a,join(sF0,meet(sF2,X0))))),
inference(forward_demodulation,[],[f43919,f24380]) ).
fof(f43950,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(X0,meet(a,join(z2,sF1))),join(z2,sF1)),
inference(forward_demodulation,[],[f43936,f22804]) ).
fof(f43963,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(sF1,z2),join(meet(a,join(z2,sF1)),X0)),
inference(forward_demodulation,[],[f43950,f42762]) ).
fof(f43975,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(sF1,z2),join(meet(a,join(z2,sF0)),X0)),
inference(forward_demodulation,[],[f43963,f21185]) ).
fof(f43984,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(sF1,z2),join(meet(a,join(sF0,z2)),X0)),
inference(forward_demodulation,[],[f43975,f35383]) ).
fof(f43993,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(sF1,z2),join(sF1,join(X0,meet(z2,a)))),
inference(forward_demodulation,[],[f43984,f22723]) ).
fof(f44001,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(sF1,z2),join(sF1,join(X0,meet(a,z2)))),
inference(forward_demodulation,[],[f43993,f24551]) ).
fof(f44009,plain,
! [X0] : join(meet(X0,join(z2,sF1)),meet(a,meet(sF2,join(X0,join(z2,sF1))))) = meet(join(z2,sF1),join(sF1,join(X0,meet(a,z2)))),
inference(forward_demodulation,[],[f44001,f3]) ).
fof(f44015,plain,
! [X0] : meet(join(z2,sF1),join(sF1,join(X0,meet(a,z2)))) = join(meet(X0,join(z2,sF1)),meet(sF2,meet(a,join(X0,join(z2,sF1))))),
inference(forward_demodulation,[],[f44009,f9808]) ).
fof(f44021,plain,
! [X0] : meet(join(z2,sF1),join(sF1,join(X0,meet(a,z2)))) = join(meet(X0,join(z2,sF1)),meet(sF1,join(X0,join(z2,sF1)))),
inference(forward_demodulation,[],[f44015,f377]) ).
fof(f44027,plain,
! [X0] : meet(join(z2,sF1),join(sF1,join(X0,meet(a,z2)))) = join(meet(X0,join(z2,sF1)),sF1),
inference(forward_demodulation,[],[f44021,f302]) ).
fof(f44033,plain,
! [X0] : join(sF1,meet(X0,join(z2,sF1))) = meet(join(z2,sF1),join(sF1,join(X0,meet(a,z2)))),
inference(forward_demodulation,[],[f44027,f3]) ).
fof(f44509,plain,
meet(sF2,sF0) = join(join(x2,sF1),meet(sF2,join(y2,sF1))),
inference(superposition,[],[f18386,f6315]) ).
fof(f44519,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,join(join(x2,sF1),meet(a,meet(a,join(y2,sF1))))),meet(X0,meet(a,sF0))),
inference(superposition,[],[f187,f18386]) ).
fof(f44520,plain,
! [X0] : join(join(x2,sF1),meet(X0,join(y2,sF1))) = join(join(x2,sF1),meet(X0,sF0)),
inference(superposition,[],[f285,f18386]) ).
fof(f44613,plain,
! [X0] : join(join(x2,sF1),meet(X0,join(y2,sF1))) = join(x2,join(sF1,meet(X0,sF0))),
inference(forward_demodulation,[],[f44520,f4]) ).
fof(f44614,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(join(x2,sF1),meet(a,meet(a,join(y2,sF1)))))),
inference(forward_demodulation,[],[f44519,f3]) ).
fof(f44622,plain,
meet(sF2,sF0) = join(x2,join(sF1,meet(sF2,join(y2,sF1)))),
inference(forward_demodulation,[],[f44509,f4]) ).
fof(f44668,plain,
! [X0] : join(join(x2,sF1),meet(X0,join(y2,sF1))) = join(x2,meet(sF0,join(X0,sF1))),
inference(forward_demodulation,[],[f44613,f11327]) ).
fof(f44669,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,join(sF1,meet(a,meet(a,join(y2,sF1))))))),
inference(forward_demodulation,[],[f44614,f4]) ).
fof(f44677,plain,
meet(sF2,sF0) = join(x2,meet(sF2,join(sF1,join(y2,sF1)))),
inference(forward_demodulation,[],[f44622,f6413]) ).
fof(f44719,plain,
! [X0] : join(x2,meet(sF0,join(X0,sF1))) = join(x2,join(sF1,meet(X0,join(y2,sF1)))),
inference(forward_demodulation,[],[f44668,f4]) ).
fof(f44720,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(meet(a,join(y2,sF1)),sF0))))),
inference(forward_demodulation,[],[f44669,f20874]) ).
fof(f44728,plain,
meet(sF2,sF0) = join(x2,meet(sF2,join(y2,join(sF1,sF1)))),
inference(forward_demodulation,[],[f44677,f1724]) ).
fof(f44761,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(sF0,meet(a,join(y2,sF1))))))),
inference(forward_demodulation,[],[f44720,f24380]) ).
fof(f44767,plain,
meet(sF2,sF0) = join(x2,meet(sF2,join(y2,sF1))),
inference(forward_demodulation,[],[f44728,f99]) ).
fof(f44794,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(join(y2,sF1),sF0))))),
inference(forward_demodulation,[],[f44761,f16438]) ).
fof(f44799,plain,
meet(sF0,sF2) = join(x2,meet(sF2,join(y2,sF1))),
inference(forward_demodulation,[],[f44767,f1]) ).
fof(f44822,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(sF0,join(y2,sF1)))))),
inference(forward_demodulation,[],[f44794,f24380]) ).
fof(f44826,plain,
sF6 = join(x2,meet(sF2,join(y2,sF1))),
inference(forward_demodulation,[],[f44799,f36]) ).
fof(f44846,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(sF0,join(sF0,y2)))))),
inference(forward_demodulation,[],[f44822,f22851]) ).
fof(f44867,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,join(sF0,sF0))))),
inference(forward_demodulation,[],[f44846,f7177]) ).
fof(f44887,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(a,sF0)),meet(X0,join(x2,meet(a,sF0)))),
inference(forward_demodulation,[],[f44867,f99]) ).
fof(f44907,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,meet(sF0,a)),meet(X0,join(x2,meet(sF0,a)))),
inference(forward_demodulation,[],[f44887,f1]) ).
fof(f44926,plain,
! [X0] : meet(X0,join(join(x2,sF1),meet(a,join(y2,sF1)))) = join(meet(X0,sF1),meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f44907,f43]) ).
fof(f44944,plain,
! [X0] : join(meet(X0,sF1),meet(X0,join(x2,sF1))) = meet(X0,join(x2,join(sF1,meet(a,join(y2,sF1))))),
inference(forward_demodulation,[],[f44926,f4]) ).
fof(f44962,plain,
! [X0] : join(meet(X0,sF1),meet(X0,join(x2,sF1))) = meet(X0,join(x2,meet(sF0,join(a,sF1)))),
inference(forward_demodulation,[],[f44944,f44719]) ).
fof(f44980,plain,
! [X0] : meet(X0,join(x2,meet(sF0,a))) = join(meet(X0,sF1),meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f44962,f258]) ).
fof(f44998,plain,
! [X0] : meet(X0,join(x2,sF1)) = join(meet(X0,sF1),meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f44980,f43]) ).
fof(f45069,plain,
join(sF7,sF6) = join(sF8,meet(sF2,join(y2,sF1))),
inference(superposition,[],[f293,f44826]) ).
fof(f45125,plain,
join(sF7,sF6) = join(sF1,join(sF8,meet(sF2,y2))),
inference(forward_demodulation,[],[f45069,f6410]) ).
fof(f45147,plain,
sF6 = join(sF1,join(sF8,meet(sF2,y2))),
inference(forward_demodulation,[],[f45125,f15505]) ).
fof(f48689,plain,
! [X0] : join(sF1,X0) = join(sF1,join(X0,meet(a,z2))),
inference(superposition,[],[f3061,f25339]) ).
fof(f48698,plain,
! [X0] : join(sF1,meet(X0,join(z2,sF1))) = meet(join(z2,sF1),join(sF1,X0)),
inference(backward_demodulation,[],[f44033,f48689]) ).
fof(f49596,plain,
! [X0] : meet(a,sF8) = meet(meet(a,sF8),join(X0,sF4)),
inference(superposition,[],[f302,f20086]) ).
fof(f49859,plain,
! [X0] : meet(a,sF8) = meet(a,meet(sF8,join(X0,sF4))),
inference(forward_demodulation,[],[f49596,f2]) ).
fof(f50767,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(meet(join(X0,meet(a,X1)),join(X0,meet(a,X1))),join(meet(X0,X1),meet(a,join(X0,X1)))),
inference(superposition,[],[f194,f1837]) ).
fof(f50914,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(join(meet(X0,X1),meet(a,join(X0,X1))),meet(join(X0,meet(a,X1)),join(X0,meet(a,X1)))),
inference(forward_demodulation,[],[f50767,f3]) ).
fof(f51142,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),meet(join(X0,meet(a,X1)),join(X0,meet(a,X1))))),
inference(forward_demodulation,[],[f50914,f4]) ).
fof(f51339,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(meet(X0,X1),join(meet(a,join(X0,X1)),join(X0,meet(a,X1)))),
inference(forward_demodulation,[],[f51142,f97]) ).
fof(f51501,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(X0,join(meet(a,X1),join(meet(X0,X1),meet(a,join(X0,X1))))),
inference(forward_demodulation,[],[f51339,f1374]) ).
fof(f51636,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(X0,join(meet(a,join(X0,X1)),meet(a,X1))),
inference(forward_demodulation,[],[f51501,f1358]) ).
fof(f51735,plain,
! [X0,X1] : meet(join(X0,meet(a,X1)),join(X1,X0)) = join(meet(a,X1),join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f51636,f17752]) ).
fof(f51803,plain,
! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,meet(a,X1)),join(X1,X0)),
inference(forward_demodulation,[],[f51735,f318]) ).
fof(f51863,plain,
! [X0,X1] : join(meet(a,X1),X0) = meet(join(X0,X1),join(meet(a,X1),X0)),
inference(forward_demodulation,[],[f51803,f42762]) ).
fof(f61281,plain,
! [X2,X0,X1] : meet(join(X0,X1),X2) = meet(join(X1,X0),X2),
inference(superposition,[],[f1,f1774]) ).
fof(f61417,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(a,X1)),join(X2,X3)) = join(meet(join(X3,X2),meet(a,join(X1,X0))),meet(join(X0,meet(a,X1)),join(X2,X3))),
inference(superposition,[],[f16258,f1774]) ).
fof(f61502,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(a,X1)),join(X2,X3)) = join(meet(a,meet(join(X1,X0),join(X2,X3))),meet(join(X0,meet(a,X1)),join(X2,X3))),
inference(forward_demodulation,[],[f61417,f2053]) ).
fof(f63746,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X3,meet(a,X2))),meet(X0,meet(X1,join(X2,meet(a,X3))))) = join(meet(X1,join(X3,meet(a,X2))),meet(X0,meet(X1,join(X2,X3)))),
inference(superposition,[],[f3061,f409]) ).
fof(f68270,plain,
! [X2,X3,X0,X1,X4] : meet(X2,meet(X3,join(X4,meet(X0,X1)))) = meet(X2,meet(X3,join(meet(X1,X0),join(meet(X0,X1),X4)))),
inference(superposition,[],[f1570,f1172]) ).
fof(f69522,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,[],[f68270,f3824]) ).
fof(f74402,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(superposition,[],[f343,f3]) ).
fof(f74437,plain,
! [X2,X0,X1] : join(meet(meet(X1,a),X2),meet(a,X0)) = meet(meet(a,join(X0,X1)),join(meet(meet(X1,a),X2),meet(a,X0))),
inference(superposition,[],[f343,f16557]) ).
fof(f74569,plain,
! [X0] : join(meet(sF7,X0),x2) = meet(sF8,join(meet(sF7,X0),x2)),
inference(superposition,[],[f343,f46]) ).
fof(f74816,plain,
! [X2,X0,X1] : meet(join(meet(X0,X1),X2),join(X0,X2)) = meet(join(meet(X0,X1),X2),join(meet(X0,X1),X2)),
inference(superposition,[],[f222,f343]) ).
fof(f74850,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(meet(X0,X1),X2),join(X0,X2)),
inference(forward_demodulation,[],[f74816,f97]) ).
fof(f74978,plain,
! [X0] : join(meet(sF7,X0),x2) = meet(sF8,join(x2,meet(sF7,X0))),
inference(forward_demodulation,[],[f74569,f1657]) ).
fof(f75097,plain,
! [X2,X0,X1] : join(meet(meet(X1,a),X2),meet(a,X0)) = meet(a,meet(join(X0,X1),join(meet(meet(X1,a),X2),meet(a,X0)))),
inference(forward_demodulation,[],[f74437,f2]) ).
fof(f75128,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = meet(join(X2,X0),join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f74850,f42762]) ).
fof(f75189,plain,
! [X0] : join(x2,meet(sF7,X0)) = meet(sF8,join(x2,meet(sF7,X0))),
inference(forward_demodulation,[],[f74978,f3]) ).
fof(f75294,plain,
! [X2,X0,X1] : join(meet(meet(X1,a),X2),meet(a,X0)) = meet(a,meet(join(meet(meet(X1,a),X2),X0),join(X0,X1))),
inference(forward_demodulation,[],[f75097,f43620]) ).
fof(f75392,plain,
! [X2,X0,X1] : join(meet(meet(X1,a),X2),meet(a,X0)) = meet(a,meet(join(X0,X1),join(X0,meet(meet(X1,a),X2)))),
inference(forward_demodulation,[],[f75294,f1574]) ).
fof(f75473,plain,
! [X2,X0,X1] : join(meet(X1,meet(a,X2)),meet(a,X0)) = meet(a,meet(join(X0,X1),join(X0,meet(X1,meet(a,X2))))),
inference(forward_demodulation,[],[f75392,f2]) ).
fof(f75522,plain,
! [X2,X0,X1] : join(meet(X1,meet(a,X2)),meet(a,X0)) = meet(a,join(meet(X1,meet(a,X2)),X0)),
inference(forward_demodulation,[],[f75473,f75128]) ).
fof(f75940,plain,
! [X0,X1] : meet(X1,join(x2,meet(sF7,X0))) = meet(sF8,meet(join(x2,meet(sF7,X0)),X1)),
inference(superposition,[],[f384,f75189]) ).
fof(f75962,plain,
! [X0] : meet(a,meet(sF8,X0)) = meet(a,meet(X0,join(x2,meet(sF7,a)))),
inference(backward_demodulation,[],[f18483,f75940]) ).
fof(f81355,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(meet(X0,join(X1,X2)),join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0))),
inference(superposition,[],[f51863,f245]) ).
fof(f81918,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(X0,meet(join(X1,X2),join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)))),
inference(forward_demodulation,[],[f81355,f2]) ).
fof(f82164,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,meet(a,X2))),meet(a,meet(X0,join(X2,meet(a,X1))))))),
inference(forward_demodulation,[],[f81918,f69522]) ).
fof(f82365,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(X0,meet(join(X1,X2),join(meet(X0,join(X1,meet(a,X2))),meet(a,meet(X0,join(X2,X1)))))),
inference(forward_demodulation,[],[f82164,f63746]) ).
fof(f82548,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(X0,meet(join(X1,X2),meet(X0,join(meet(X2,a),X1)))),
inference(forward_demodulation,[],[f82365,f17600]) ).
fof(f82695,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)) = meet(X0,meet(join(X1,X2),join(meet(X2,a),X1))),
inference(forward_demodulation,[],[f82548,f3203]) ).
fof(f82793,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,a),X1)) = join(meet(a,meet(X0,join(X2,meet(a,X1)))),meet(join(X1,meet(a,X2)),X0)),
inference(forward_demodulation,[],[f82695,f74402]) ).
fof(f82874,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,a),X1)) = join(meet(join(X1,meet(a,X2)),X0),meet(a,meet(X0,join(X2,meet(a,X1))))),
inference(forward_demodulation,[],[f82793,f3]) ).
fof(f82939,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,a),X1)) = join(meet(join(X1,meet(a,X2)),X0),meet(a,meet(join(X2,X1),X0))),
inference(forward_demodulation,[],[f82874,f43620]) ).
fof(f82986,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,a),X1)) = join(meet(a,meet(join(X2,X1),X0)),meet(join(X1,meet(a,X2)),X0)),
inference(forward_demodulation,[],[f82939,f3]) ).
fof(f83027,plain,
! [X2,X3,X0,X1] : meet(join(X0,meet(a,X1)),join(X2,X3)) = meet(join(X2,X3),join(meet(X1,a),X0)),
inference(backward_demodulation,[],[f61502,f82986]) ).
fof(f84268,plain,
meet(sF0,sF2) = join(join(x2,sF1),meet(sF0,join(z2,sF1))),
inference(superposition,[],[f18763,f14280]) ).
fof(f84433,plain,
meet(sF0,sF2) = join(x2,join(sF1,meet(sF0,join(z2,sF1)))),
inference(forward_demodulation,[],[f84268,f4]) ).
fof(f84511,plain,
meet(sF0,sF2) = join(x2,meet(join(z2,sF1),join(sF1,sF0))),
inference(forward_demodulation,[],[f84433,f48698]) ).
fof(f84578,plain,
meet(sF0,sF2) = join(x2,meet(join(sF0,sF1),join(sF1,z2))),
inference(forward_demodulation,[],[f84511,f42762]) ).
fof(f84637,plain,
meet(sF0,sF2) = join(x2,meet(join(sF0,sF1),join(z2,sF1))),
inference(forward_demodulation,[],[f84578,f1657]) ).
fof(f84689,plain,
meet(sF0,sF2) = join(x2,meet(sF0,join(z2,sF1))),
inference(forward_demodulation,[],[f84637,f70]) ).
fof(f84731,plain,
sF6 = join(x2,meet(sF0,join(z2,sF1))),
inference(forward_demodulation,[],[f84689,f36]) ).
fof(f86963,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(meet(X0,a),join(z2,sF1)),meet(join(x2,sF1),meet(a,X0))),
inference(superposition,[],[f18758,f3166]) ).
fof(f87098,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(meet(X0,a),join(z2,sF1)),meet(a,meet(X0,join(sF1,x2)))),
inference(forward_demodulation,[],[f86963,f2053]) ).
fof(f87181,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(meet(X0,a),join(z2,sF1))),
inference(forward_demodulation,[],[f87098,f3]) ).
fof(f87254,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,join(z2,sF1)))),
inference(forward_demodulation,[],[f87181,f2]) ).
fof(f87321,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,join(z2,sF0)))),
inference(forward_demodulation,[],[f87254,f21185]) ).
fof(f87375,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,join(sF0,z2)))),
inference(forward_demodulation,[],[f87321,f431]) ).
fof(f87420,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,join(sF0,sF2)))),
inference(forward_demodulation,[],[f87375,f23509]) ).
fof(f87453,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,join(sF0,sF0)))),
inference(forward_demodulation,[],[f87420,f21062]) ).
fof(f87479,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(a,meet(X0,join(sF1,x2))),meet(X0,meet(a,sF0))),
inference(forward_demodulation,[],[f87453,f99]) ).
fof(f87500,plain,
! [X0] : meet(meet(X0,a),sF2) = join(meet(X0,meet(a,sF0)),meet(a,meet(X0,join(sF1,x2)))),
inference(forward_demodulation,[],[f87479,f3]) ).
fof(f87513,plain,
! [X0] : meet(meet(X0,a),sF2) = meet(a,join(meet(X0,meet(a,sF0)),meet(X0,join(sF1,x2)))),
inference(forward_demodulation,[],[f87500,f75522]) ).
fof(f87524,plain,
! [X0] : meet(meet(X0,a),sF2) = meet(a,join(meet(X0,meet(a,sF0)),meet(X0,join(x2,sF1)))),
inference(forward_demodulation,[],[f87513,f1657]) ).
fof(f87533,plain,
! [X0] : meet(meet(X0,a),sF2) = meet(a,join(meet(X0,meet(sF0,a)),meet(X0,join(x2,sF1)))),
inference(forward_demodulation,[],[f87524,f3166]) ).
fof(f87541,plain,
! [X0] : meet(meet(X0,a),sF2) = meet(a,join(meet(X0,sF1),meet(X0,join(x2,sF1)))),
inference(forward_demodulation,[],[f87533,f43]) ).
fof(f87549,plain,
! [X0] : meet(meet(X0,a),sF2) = meet(a,meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f87541,f44998]) ).
fof(f87556,plain,
! [X0] : meet(X0,meet(a,sF2)) = meet(a,meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f87549,f2]) ).
fof(f87563,plain,
! [X0] : meet(X0,meet(sF2,a)) = meet(a,meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f87556,f3166]) ).
fof(f87567,plain,
! [X0] : meet(X0,sF1) = meet(a,meet(X0,join(x2,sF1))),
inference(forward_demodulation,[],[f87563,f48]) ).
fof(f93564,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,[],[f187,f1960]) ).
fof(f93647,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,[],[f93564,f3]) ).
fof(f94028,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,[],[f93647,f4]) ).
fof(f94353,plain,
! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X0,meet(a,X1)),join(X1,X0)),
inference(forward_demodulation,[],[f94028,f298]) ).
fof(f94603,plain,
! [X0,X1] : join(X0,meet(a,X1)) = meet(join(X1,X0),join(meet(X1,a),X0)),
inference(forward_demodulation,[],[f94353,f83027]) ).
fof(f94771,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(meet(X1,a),X0),
inference(forward_demodulation,[],[f94603,f343]) ).
fof(f97225,plain,
! [X2,X0,X1] : join(X0,X2) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f1325,f3]) ).
fof(f99785,plain,
! [X2,X0,X1] : meet(join(X0,X1),meet(X2,a)) = join(meet(X0,meet(a,X2)),meet(join(X0,X1),meet(X2,a))),
inference(superposition,[],[f467,f3166]) ).
fof(f99913,plain,
! [X2,X0,X1] : meet(a,meet(X2,join(X1,X0))) = join(meet(X0,meet(a,X2)),meet(a,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f99785,f5681]) ).
fof(f100156,plain,
! [X2,X0,X1] : meet(a,meet(X2,join(X1,X0))) = meet(a,join(meet(X0,meet(a,X2)),meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f99913,f75522]) ).
fof(f111364,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(a,X1))) = join(meet(meet(X1,X0),a),X2),
inference(superposition,[],[f94771,f384]) ).
fof(f111469,plain,
! [X0,X1] : join(meet(a,X0),X1) = join(meet(X0,a),X1),
inference(superposition,[],[f3,f94771]) ).
fof(f111573,plain,
! [X0,X1] : join(X0,meet(a,X1)) = join(X0,meet(X1,a)),
inference(superposition,[],[f3,f94771]) ).
fof(f111626,plain,
! [X2,X0,X1] : meet(join(X0,meet(a,X1)),X2) = meet(join(X0,meet(X1,a)),X2),
inference(superposition,[],[f61281,f94771]) ).
fof(f111899,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X0)),X2) = join(X2,meet(X0,meet(a,X1))),
inference(forward_demodulation,[],[f111364,f111469]) ).
fof(f116002,plain,
! [X2,X0,X1] : meet(a,join(meet(X1,X0),X2)) = join(meet(X0,meet(a,X1)),meet(a,X2)),
inference(superposition,[],[f17142,f384]) ).
fof(f116221,plain,
! [X2,X0,X1] : join(X2,meet(a,join(X0,X1))) = join(meet(a,X1),join(X2,meet(a,X0))),
inference(superposition,[],[f304,f17142]) ).
fof(f116325,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(X0,meet(a,join(meet(X2,join(X0,X1)),meet(X2,X1)))),
inference(backward_demodulation,[],[f312,f116221]) ).
fof(f116333,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(X0,meet(a,join(meet(X2,join(X0,X1)),meet(X1,X2)))),
inference(backward_demodulation,[],[f671,f116221]) ).
fof(f116597,plain,
! [X2,X0,X1] : meet(a,join(meet(X2,X1),X0)) = meet(a,join(meet(X1,meet(a,X2)),X0)),
inference(backward_demodulation,[],[f75522,f116002]) ).
fof(f116741,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(X0,meet(a,join(meet(X1,X2),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f116333,f1657]) ).
fof(f116749,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(X0,meet(a,join(meet(X2,X1),meet(X2,join(X0,X1))))),
inference(forward_demodulation,[],[f116325,f1657]) ).
fof(f116948,plain,
! [X2,X0,X1] : meet(a,meet(X2,join(X1,X0))) = meet(a,join(meet(X2,X0),meet(X2,join(X1,X0)))),
inference(backward_demodulation,[],[f100156,f116597]) ).
fof(f117020,plain,
! [X2,X0,X1] : join(meet(a,meet(X1,X2)),X0) = join(X0,meet(a,meet(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f116741,f12851]) ).
fof(f117126,plain,
! [X2,X0,X1] : join(meet(a,meet(X2,X1)),X0) = join(X0,meet(a,meet(X2,join(X0,X1)))),
inference(backward_demodulation,[],[f116749,f116948]) ).
fof(f117729,plain,
! [X0] : join(x2,meet(a,meet(X0,sF2))) = join(meet(a,meet(X0,z2)),x2),
inference(superposition,[],[f117126,f26]) ).
fof(f118391,plain,
! [X0] : join(x2,meet(a,meet(X0,sF2))) = join(x2,meet(z2,meet(a,X0))),
inference(forward_demodulation,[],[f117729,f111899]) ).
fof(f118796,plain,
! [X0] : join(x2,meet(a,meet(X0,sF2))) = join(x2,meet(a,meet(X0,z2))),
inference(forward_demodulation,[],[f118391,f384]) ).
fof(f119103,plain,
! [X0] : join(x2,meet(a,meet(X0,z2))) = join(x2,meet(sF2,meet(a,X0))),
inference(forward_demodulation,[],[f118796,f384]) ).
fof(f119377,plain,
! [X0] : join(x2,meet(sF1,X0)) = join(x2,meet(a,meet(X0,z2))),
inference(forward_demodulation,[],[f119103,f377]) ).
fof(f125000,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(meet(a,meet(meet(sF0,join(z2,sF1)),X0)),x2),
inference(superposition,[],[f117020,f84731]) ).
fof(f125676,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(x2,meet(X0,meet(a,meet(sF0,join(z2,sF1))))),
inference(forward_demodulation,[],[f125000,f111899]) ).
fof(f126042,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(x2,meet(X0,meet(sF0,meet(a,join(sF1,z2))))),
inference(forward_demodulation,[],[f125676,f3384]) ).
fof(f126338,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(x2,meet(X0,meet(sF0,meet(a,join(z2,sF1))))),
inference(forward_demodulation,[],[f126042,f1649]) ).
fof(f126547,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(x2,meet(X0,meet(sF1,join(z2,sF1)))),
inference(forward_demodulation,[],[f126338,f375]) ).
fof(f126693,plain,
! [X0] : join(x2,meet(a,meet(X0,sF6))) = join(x2,meet(X0,sF1)),
inference(forward_demodulation,[],[f126547,f129]) ).
fof(f126805,plain,
! [X0] : join(x2,meet(sF1,X0)) = join(x2,meet(X0,sF1)),
inference(forward_demodulation,[],[f126693,f11278]) ).
fof(f130685,plain,
join(x2,meet(a,sF7)) = join(x2,meet(sF1,y2)),
inference(superposition,[],[f119377,f38]) ).
fof(f130849,plain,
join(x2,meet(a,sF7)) = join(x2,meet(y2,sF1)),
inference(forward_demodulation,[],[f130685,f126805]) ).
fof(f130910,plain,
join(x2,meet(a,sF7)) = join(x2,meet(a,y2)),
inference(forward_demodulation,[],[f130849,f19594]) ).
fof(f130941,plain,
join(x2,sF1) = join(x2,meet(a,sF7)),
inference(forward_demodulation,[],[f130910,f18040]) ).
fof(f130959,plain,
join(x2,sF1) = join(x2,meet(sF7,a)),
inference(forward_demodulation,[],[f130941,f111573]) ).
fof(f130986,plain,
! [X0] : meet(a,meet(sF8,X0)) = meet(a,meet(X0,join(x2,sF1))),
inference(backward_demodulation,[],[f75962,f130959]) ).
fof(f131002,plain,
! [X0] : meet(X0,sF1) = meet(a,meet(sF8,X0)),
inference(forward_demodulation,[],[f130986,f87567]) ).
fof(f131067,plain,
! [X0] : meet(a,sF8) = meet(join(X0,sF4),sF1),
inference(backward_demodulation,[],[f49859,f131002]) ).
fof(f131123,plain,
! [X0] : meet(a,sF8) = meet(sF1,join(sF4,X0)),
inference(forward_demodulation,[],[f131067,f1774]) ).
fof(f131195,plain,
sF1 = meet(a,sF8),
inference(forward_demodulation,[],[f131123,f12081]) ).
fof(f131235,plain,
join(sF7,sF1) = join(sF7,meet(a,x2)),
inference(backward_demodulation,[],[f17832,f131195]) ).
fof(f131444,plain,
! [X0] : join(X0,sF8) = join(sF8,join(X0,sF1)),
inference(superposition,[],[f97225,f131195]) ).
fof(f131448,plain,
! [X0] : join(X0,sF8) = join(sF1,join(sF8,X0)),
inference(forward_demodulation,[],[f131444,f304]) ).
fof(f131558,plain,
sF6 = join(meet(sF2,y2),sF8),
inference(backward_demodulation,[],[f45147,f131448]) ).
fof(f131731,plain,
sF6 = join(sF8,meet(sF2,y2)),
inference(forward_demodulation,[],[f131558,f3]) ).
fof(f134489,plain,
! [X0] : meet(X0,join(sF7,x2)) = join(meet(X0,join(sF7,sF1)),meet(join(x2,meet(a,sF7)),X0)),
inference(superposition,[],[f244,f131235]) ).
fof(f134608,plain,
! [X0] : meet(X0,join(sF7,x2)) = join(meet(X0,join(sF7,sF1)),meet(join(x2,meet(sF7,a)),X0)),
inference(forward_demodulation,[],[f134489,f111626]) ).
fof(f134663,plain,
! [X0] : meet(X0,join(sF7,x2)) = join(meet(X0,join(sF7,sF1)),meet(join(x2,sF1),X0)),
inference(forward_demodulation,[],[f134608,f130959]) ).
fof(f134707,plain,
! [X0] : meet(X0,sF8) = join(meet(X0,join(sF7,sF1)),meet(join(x2,sF1),X0)),
inference(forward_demodulation,[],[f134663,f46]) ).
fof(f249007,plain,
meet(y2,sF2) = join(meet(y2,join(sF7,sF1)),meet(join(x2,sF1),y2)),
inference(superposition,[],[f18758,f39371]) ).
fof(f249127,plain,
meet(y2,sF8) = meet(y2,sF2),
inference(forward_demodulation,[],[f249007,f134707]) ).
fof(f249180,plain,
meet(y2,sF8) = meet(sF2,y2),
inference(forward_demodulation,[],[f249127,f1]) ).
fof(f249467,plain,
sF8 = join(sF8,meet(sF2,y2)),
inference(superposition,[],[f241,f249180]) ).
fof(f249527,plain,
sF6 = sF8,
inference(forward_demodulation,[],[f249467,f131731]) ).
fof(f250197,plain,
$false,
inference(forward_subsumption_resolution,[],[f249527,f41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT401-2 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n002.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 15:18:22 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 88.57/13.32 % (3655665)Detected a unit-equality problem, will run specialized UEQ schedule.
% 88.57/13.32 % (3655676)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3034275486:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 88.57/13.32 % (3655674)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=1013785673:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 88.57/13.32 % (3655670)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=2272674760:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 88.57/13.32 % (3655673)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=2538268211:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 88.57/13.32 % (3655671)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=4169142688:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 88.57/13.32 % (3655672)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4203651645:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 88.57/13.32 % (3655675)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1553533328:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 88.57/13.32 % (3655673)Instruction limit reached!
% 88.57/13.32 % (3655673)------------------------------
% 88.57/13.32 % (3655673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.57/13.32 % (3655673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.57/13.32 % (3655673)CaDiCaL version: 2.1.3
% 88.57/13.32 % (3655673)Termination reason: Instruction limit
% 88.57/13.32 % (3655673)Termination phase: Saturation
% 88.57/13.32 % (3655673)Time elapsed: 0.078 s
% 88.57/13.32 % (3655673)Peak memory usage: 89 MB
% 88.57/13.32 % (3655673)Instructions burned: 136 (million)
% 88.57/13.32 % (3655674)Instruction limit reached!
% 88.57/13.32 % (3655674)------------------------------
% 88.57/13.32 % (3655674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.57/13.32 % (3655674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.57/13.32 % (3655674)CaDiCaL version: 2.1.3
% 88.57/13.32 % (3655674)Termination reason: Instruction limit
% 88.57/13.32 % (3655674)Termination phase: Saturation
% 88.57/13.32 % (3655674)Time elapsed: 0.105 s
% 88.57/13.32 % (3655674)Peak memory usage: 89 MB
% 88.57/13.32 % (3655674)Instructions burned: 182 (million)
% 88.57/13.32 % (3655675)Instruction limit reached!
% 88.57/13.32 % (3655675)------------------------------
% 88.57/13.32 % (3655675)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.57/13.32 % (3655675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.57/13.32 % (3655675)CaDiCaL version: 2.1.3
% 88.57/13.32 % (3655675)Termination reason: Instruction limit
% 88.57/13.32 % (3655675)Termination phase: Saturation
% 88.57/13.32 % (3655675)Time elapsed: 0.170 s
% 88.57/13.32 % (3655675)Peak memory usage: 90 MB
% 88.57/13.32 % (3655675)Instructions burned: 259 (million)
% 88.57/13.32 % (3655684)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2634868162:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 88.57/13.32 % (3655685)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1313056523:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 88.57/13.32 % (3655686)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3553159921:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 88.57/13.32 % (3655676)Instruction limit reached!
% 88.57/13.32 % (3655676)------------------------------
% 88.57/13.32 % (3655676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.57/13.32 % (3655676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.57/13.32 % (3655676)CaDiCaL version: 2.1.3
% 88.57/13.32 % (3655676)Termination reason: Instruction limit
% 88.57/13.32 % (3655676)Termination phase: Saturation
% 88.57/13.32 % (3655676)Time elapsed: 0.354 s
% 79.20/16.42 % (3655676)Peak memory usage: 99 MB
% 79.20/16.42 % (3655676)Instructions burned: 1188 (million)
% 79.20/16.42 % (3655686)Instruction limit reached!
% 79.20/16.42 % (3655686)------------------------------
% 79.20/16.42 % (3655686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655686)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655686)Termination reason: Instruction limit
% 79.20/16.42 % (3655686)Termination phase: Saturation
% 79.20/16.42 % (3655686)Time elapsed: 0.117 s
% 79.20/16.42 % (3655686)Peak memory usage: 92 MB
% 79.20/16.42 % (3655686)Instructions burned: 215 (million)
% 79.20/16.42 % (3655690)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=4075664536: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)
% 79.20/16.42 % (3655690)Instruction limit reached!
% 79.20/16.42 % (3655690)------------------------------
% 79.20/16.42 % (3655690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655690)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655690)Termination reason: Instruction limit
% 79.20/16.42 % (3655690)Termination phase: Saturation
% 79.20/16.42 % (3655690)Time elapsed: 0.086 s
% 79.20/16.42 % (3655690)Peak memory usage: 90 MB
% 79.20/16.42 % (3655690)Instructions burned: 320 (million)
% 79.20/16.42 % (3655691)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=3881462411:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 79.20/16.42 % (3655693)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=1435895994:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 79.20/16.42 % (3655684)Instruction limit reached!
% 79.20/16.42 % (3655684)------------------------------
% 79.20/16.42 % (3655684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655684)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655684)Termination reason: Instruction limit
% 79.20/16.42 % (3655684)Termination phase: Saturation
% 79.20/16.42 % (3655684)Time elapsed: 1.339 s
% 79.20/16.42 % (3655684)Peak memory usage: 140 MB
% 79.20/16.42 % (3655684)Instructions burned: 2052 (million)
% 79.20/16.42 % (3655696)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1076057342:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2982 on theBenchmark for (2982ds/14534Mi)
% 79.20/16.42 % (3655693)Instruction limit reached!
% 79.20/16.42 % (3655693)------------------------------
% 79.20/16.42 % (3655693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655693)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655693)Termination reason: Instruction limit
% 79.20/16.42 % (3655693)Termination phase: Saturation
% 79.20/16.42 % (3655693)Time elapsed: 1.788 s
% 79.20/16.42 % (3655693)Peak memory usage: 130 MB
% 79.20/16.42 % (3655693)Instructions burned: 2836 (million)
% 79.20/16.42 % (3655698)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=2413016737:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/11832Mi)
% 79.20/16.42 % (3655685)Instruction limit reached!
% 79.20/16.42 % (3655685)------------------------------
% 79.20/16.42 % (3655685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655685)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655685)Termination reason: Instruction limit
% 79.20/16.42 % (3655685)Termination phase: Saturation
% 79.20/16.42 % (3655685)Time elapsed: 2.954 s
% 79.20/16.42 % (3655685)Peak memory usage: 164 MB
% 79.20/16.42 % (3655685)Instructions burned: 4948 (million)
% 79.20/16.42 % (3655700)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=1314384206:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 79.20/16.42 % (3655700)Instruction limit reached!
% 79.20/16.42 % (3655700)------------------------------
% 79.20/16.42 % (3655700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655700)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655700)Termination reason: Instruction limit
% 79.20/16.42 % (3655700)Termination phase: Saturation
% 79.20/16.42 % (3655700)Time elapsed: 1.401 s
% 79.20/16.42 % (3655700)Peak memory usage: 140 MB
% 79.20/16.42 % (3655700)Instructions burned: 2280 (million)
% 79.20/16.42 % (3655702)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=3686875803:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 79.20/16.42 % (3655691)Instruction limit reached!
% 79.20/16.42 % (3655691)------------------------------
% 79.20/16.42 % (3655691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655691)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655691)Termination reason: Instruction limit
% 79.20/16.42 % (3655691)Termination phase: Saturation
% 79.20/16.42 % (3655691)Time elapsed: 7.440 s
% 79.20/16.42 % (3655691)Peak memory usage: 233 MB
% 79.20/16.42 % (3655691)Instructions burned: 12126 (million)
% 79.20/16.42 % (3655704)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=3550825157:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2918 on theBenchmark for (2918ds/21755Mi)
% 79.20/16.42 % (3655702)Instruction limit reached!
% 79.20/16.42 % (3655702)------------------------------
% 79.20/16.42 % (3655702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655702)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655702)Termination reason: Instruction limit
% 79.20/16.42 % (3655702)Termination phase: Saturation
% 79.20/16.42 % (3655702)Time elapsed: 3.665 s
% 79.20/16.42 % (3655702)Peak memory usage: 157 MB
% 79.20/16.42 % (3655702)Instructions burned: 6226 (million)
% 79.20/16.42 % (3655706)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=2451260851:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2913 on theBenchmark for (2913ds/16427Mi)
% 79.20/16.42 % (3655698)Instruction limit reached!
% 79.20/16.42 % (3655698)------------------------------
% 79.20/16.42 % (3655698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655698)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655698)Termination reason: Instruction limit
% 79.20/16.42 % (3655698)Termination phase: Saturation
% 79.20/16.42 % (3655698)Time elapsed: 7.725 s
% 79.20/16.42 % (3655698)Peak memory usage: 213 MB
% 79.20/16.42 % (3655698)Instructions burned: 11832 (million)
% 79.20/16.42 % (3655708)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=1667877402:i=9356:fgj=on:bd=preordered:av=off_2895 on theBenchmark for (2895ds/9356Mi)
% 79.20/16.42 % (3655696)Instruction limit reached!
% 79.20/16.42 % (3655696)------------------------------
% 79.20/16.42 % (3655696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655696)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655696)Termination reason: Instruction limit
% 79.20/16.42 % (3655696)Termination phase: Saturation
% 79.20/16.42 % (3655696)Time elapsed: 9.232 s
% 79.20/16.42 % (3655696)Peak memory usage: 231 MB
% 79.20/16.42 % (3655696)Instructions burned: 14534 (million)
% 79.20/16.42 % (3655710)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=1086617435:i=2070:kws=inv_precedence:slsql=off:bd=all_2889 on theBenchmark for (2889ds/2070Mi)
% 79.20/16.42 % (3655710)Instruction limit reached!
% 79.20/16.42 % (3655710)------------------------------
% 79.20/16.42 % (3655710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.20/16.42 % (3655710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.20/16.42 % (3655710)CaDiCaL version: 2.1.3
% 79.20/16.42 % (3655710)Termination reason: Instruction limit
% 79.20/16.42 % (3655710)Termination phase: Saturation
% 79.20/16.42 % (3655710)Time elapsed: 1.232 s
% 79.20/16.42 % (3655710)Peak memory usage: 131 MB
% 79.20/16.42 % (3655710)Instructions burned: 2070 (million)
% 79.20/16.42 % (3655712)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=1729163355:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2875 on theBenchmark for (2875ds/6461Mi)
% 79.20/16.42 % (3655672)First to succeed.
% 79.20/16.42 % (3655672)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3655665"
% 79.20/16.42 % (3655672)Refutation found. Thanks to Tanya!
% 79.20/16.42 % SZS status Unsatisfiable for theBenchmark
% 79.20/16.42 % SZS output start Proof for theBenchmark
% See solution above
% 110.87/16.61 % (3655672)------------------------------
% 110.87/16.61 % (3655672)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.87/16.61 % (3655672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.87/16.61 % (3655672)CaDiCaL version: 2.1.3
% 110.87/16.61 % (3655672)Termination reason: Refutation
% 110.87/16.61 % (3655672)Time elapsed: 15.093 s
% 110.87/16.61 % (3655672)Peak memory usage: 292 MB
% 110.87/16.61 % (3655672)Instructions burned: 23609 (million)
% 110.87/16.61 % (3655672)------------------------------
% 110.87/16.61 % (3655672)------------------------------
% 110.87/16.61 % (3655665)Success in time 15.554 s
% 110.87/16.61 % Vampire exiting
%------------------------------------------------------------------------------