%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT007-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:39 AM UTC 2026
% Result : Unsatisfiable 45.24s 6.90s
% Output : Refutation 45.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 7
% Syntax : Number of formulae : 456 ( 456 unt; 4 def)
% Number of atoms : 456 ( 455 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 388 ( 388 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = join(meet(X2,X0),meet(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distribution) ).
fof(f3,negated_conjecture,
join(join(a,b),c) != join(a,join(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_associativity_of_join) ).
fof(f4,definition,
sF0 = join(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
join(a,b) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = join(sF0,c),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
join(sF0,c) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = join(b,c),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
join(b,c) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF3 = join(a,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f11,plain,
join(a,sF2) = sF3,
inference(reorient_equations,[],[f10]) ).
fof(f12,plain,
sF1 != sF3,
inference(definition_folding,[],[f3,f11,f9,f7,f5]) ).
fof(f13,plain,
a = meet(a,sF0),
inference(superposition,[],[f1,f5]) ).
fof(f14,plain,
a = meet(a,sF3),
inference(superposition,[],[f1,f11]) ).
fof(f15,plain,
sF0 = meet(sF0,sF1),
inference(superposition,[],[f1,f7]) ).
fof(f16,plain,
b = meet(b,sF2),
inference(superposition,[],[f1,f9]) ).
fof(f17,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X2,X0)) = join(X0,meet(X2,join(X0,X1))),
inference(superposition,[],[f2,f1]) ).
fof(f18,plain,
! [X0] : meet(sF0,join(X0,a)) = join(a,meet(X0,sF0)),
inference(superposition,[],[f2,f13]) ).
fof(f19,plain,
! [X2,X0,X1] : meet(join(X0,X1),join(X0,X2)) = join(meet(X2,join(X0,X1)),X0),
inference(superposition,[],[f2,f1]) ).
fof(f20,plain,
! [X0] : meet(sF0,join(a,X0)) = join(meet(X0,sF0),a),
inference(superposition,[],[f2,f13]) ).
fof(f21,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(meet(X2,X0),meet(X0,join(X1,X2))),
inference(superposition,[],[f1,f2]) ).
fof(f22,plain,
! [X0] : meet(sF3,join(a,X0)) = join(meet(X0,sF3),a),
inference(superposition,[],[f2,f14]) ).
fof(f23,plain,
! [X0] : meet(sF3,join(X0,a)) = join(a,meet(X0,sF3)),
inference(superposition,[],[f2,f14]) ).
fof(f24,plain,
! [X0] : meet(sF1,join(sF0,X0)) = join(meet(X0,sF1),sF0),
inference(superposition,[],[f2,f15]) ).
fof(f25,plain,
! [X0] : meet(sF1,join(X0,sF0)) = join(sF0,meet(X0,sF1)),
inference(superposition,[],[f2,f15]) ).
fof(f26,plain,
! [X0] : meet(sF2,join(b,X0)) = join(meet(X0,sF2),b),
inference(superposition,[],[f2,f16]) ).
fof(f27,plain,
! [X0] : meet(sF2,join(X0,b)) = join(b,meet(X0,sF2)),
inference(superposition,[],[f2,f16]) ).
fof(f35,plain,
! [X0] : meet(b,X0) = meet(meet(b,X0),meet(X0,sF0)),
inference(superposition,[],[f21,f5]) ).
fof(f37,plain,
! [X0] : meet(c,X0) = meet(meet(c,X0),meet(X0,sF2)),
inference(superposition,[],[f21,f9]) ).
fof(f38,plain,
! [X0] : meet(c,X0) = meet(meet(c,X0),meet(X0,sF1)),
inference(superposition,[],[f21,f7]) ).
fof(f39,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f21,f1]) ).
fof(f40,plain,
! [X2,X3,X0,X1] : meet(meet(X1,join(X2,X0)),join(meet(X0,X1),X3)) = join(meet(X3,meet(X1,join(X2,X0))),meet(X0,X1)),
inference(superposition,[],[f2,f21]) ).
fof(f57,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = join(meet(X2,X1),meet(X0,X1)),
inference(superposition,[],[f2,f39]) ).
fof(f58,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X2,X1)) = meet(X1,join(X2,meet(X0,X1))),
inference(superposition,[],[f2,f39]) ).
fof(f59,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X2,meet(X0,X1))),
inference(forward_demodulation,[],[f58,f2]) ).
fof(f60,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,X1),X2)) = meet(X1,join(X0,X2)),
inference(forward_demodulation,[],[f57,f2]) ).
fof(f66,plain,
! [X2,X3,X0,X1] : join(meet(X1,X0),meet(meet(X2,X0),join(meet(X1,X0),X3))) = meet(join(meet(X1,X0),X3),meet(X0,join(X1,X2))),
inference(superposition,[],[f17,f2]) ).
fof(f68,plain,
! [X0] : join(sF2,meet(a,join(sF2,X0))) = meet(join(sF2,X0),sF3),
inference(superposition,[],[f17,f11]) ).
fof(f70,plain,
! [X0] : join(c,meet(sF0,join(c,X0))) = meet(join(c,X0),sF1),
inference(superposition,[],[f17,f7]) ).
fof(f72,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(join(X0,X1),join(X0,X1))),
inference(superposition,[],[f1,f17]) ).
fof(f74,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,meet(X1,join(X0,X2))),join(X1,X0)),
inference(superposition,[],[f39,f17]) ).
fof(f75,plain,
! [X2,X3,X0,X1] : join(X0,meet(X1,join(X0,X2))) = meet(join(X0,meet(X1,join(X0,X2))),meet(join(X1,X0),join(X3,join(X0,X2)))),
inference(superposition,[],[f21,f17]) ).
fof(f76,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X0,X2),X3)) = join(meet(X3,join(X1,X0)),join(X0,meet(X1,join(X0,X2)))),
inference(superposition,[],[f2,f17]) ).
fof(f77,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(X3,join(X0,X2))) = join(join(X0,meet(X1,join(X0,X2))),meet(X3,join(X1,X0))),
inference(superposition,[],[f2,f17]) ).
fof(f78,plain,
! [X2,X0,X1] : join(X0,meet(X1,join(X0,X2))) = join(X0,meet(X1,join(X0,meet(X1,join(X0,X2))))),
inference(forward_demodulation,[],[f74,f17]) ).
fof(f80,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(meet(X1,join(X0,X1)),X0)),
inference(forward_demodulation,[],[f72,f19]) ).
fof(f83,plain,
sF0 = join(a,meet(sF0,sF0)),
inference(superposition,[],[f1,f18]) ).
fof(f85,plain,
! [X0] : join(a,meet(X0,sF0)) = meet(join(a,meet(X0,sF0)),join(X0,a)),
inference(superposition,[],[f39,f18]) ).
fof(f89,plain,
! [X0] : join(a,meet(X0,sF0)) = join(a,meet(X0,join(a,meet(X0,sF0)))),
inference(forward_demodulation,[],[f85,f17]) ).
fof(f97,plain,
! [X0] : join(meet(b,join(a,X0)),a) = meet(join(a,X0),sF0),
inference(superposition,[],[f19,f5]) ).
fof(f98,plain,
! [X0] : join(meet(sF2,join(a,X0)),a) = meet(join(a,X0),sF3),
inference(superposition,[],[f19,f11]) ).
fof(f99,plain,
! [X0] : join(meet(c,join(b,X0)),b) = meet(join(b,X0),sF2),
inference(superposition,[],[f19,f9]) ).
fof(f100,plain,
! [X0] : join(meet(c,join(sF0,X0)),sF0) = meet(join(sF0,X0),sF1),
inference(superposition,[],[f19,f7]) ).
fof(f104,plain,
! [X2,X0,X1] : join(meet(X0,join(X1,X2)),X1) = meet(join(meet(X0,join(X1,X2)),X1),join(X1,X0)),
inference(superposition,[],[f39,f19]) ).
fof(f105,plain,
! [X2,X3,X0,X1] : join(meet(X0,join(X1,X2)),X1) = meet(join(meet(X0,join(X1,X2)),X1),meet(join(X1,X0),join(X3,join(X1,X2)))),
inference(superposition,[],[f21,f19]) ).
fof(f106,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X1,X2),X3)) = join(meet(X3,join(X1,X0)),join(meet(X0,join(X1,X2)),X1)),
inference(superposition,[],[f2,f19]) ).
fof(f114,plain,
meet(sF0,sF0) = join(meet(b,sF0),a),
inference(superposition,[],[f20,f5]) ).
fof(f116,plain,
meet(sF0,sF0) = join(meet(meet(sF0,sF0),sF0),a),
inference(superposition,[],[f20,f83]) ).
fof(f122,plain,
! [X0,X1] : meet(join(a,X0),join(sF0,X1)) = join(meet(X1,join(a,X0)),join(meet(X0,sF0),a)),
inference(superposition,[],[f2,f20]) ).
fof(f124,plain,
meet(sF0,sF0) = join(meet(sF0,sF0),a),
inference(forward_demodulation,[],[f116,f39]) ).
fof(f125,plain,
join(a,meet(meet(b,sF0),sF0)) = meet(sF0,meet(sF0,sF0)),
inference(superposition,[],[f18,f114]) ).
fof(f132,plain,
meet(sF0,meet(sF0,sF0)) = join(a,meet(b,sF0)),
inference(forward_demodulation,[],[f125,f39]) ).
fof(f133,plain,
join(meet(b,sF3),a) = meet(sF3,sF0),
inference(superposition,[],[f22,f5]) ).
fof(f134,plain,
join(meet(sF2,sF3),a) = meet(sF3,sF3),
inference(superposition,[],[f22,f11]) ).
fof(f154,plain,
sF3 = join(a,meet(sF3,sF3)),
inference(superposition,[],[f1,f23]) ).
fof(f158,plain,
! [X0,X1] : meet(join(X0,a),join(sF3,X1)) = join(meet(X1,join(X0,a)),join(a,meet(X0,sF3))),
inference(superposition,[],[f2,f23]) ).
fof(f162,plain,
meet(sF3,sF3) = join(meet(meet(sF3,sF3),sF3),a),
inference(superposition,[],[f22,f154]) ).
fof(f170,plain,
meet(sF3,sF3) = join(meet(sF3,sF3),a),
inference(forward_demodulation,[],[f162,f39]) ).
fof(f171,plain,
join(meet(c,sF1),sF0) = meet(sF1,sF1),
inference(superposition,[],[f24,f7]) ).
fof(f175,plain,
! [X0,X1] : meet(join(sF0,X0),join(sF1,X1)) = join(meet(X1,join(sF0,X0)),join(meet(X0,sF1),sF0)),
inference(superposition,[],[f2,f24]) ).
fof(f189,plain,
sF1 = join(sF0,meet(sF1,sF1)),
inference(superposition,[],[f1,f25]) ).
fof(f191,plain,
! [X0] : join(sF0,meet(X0,sF1)) = meet(join(sF0,meet(X0,sF1)),join(X0,sF0)),
inference(superposition,[],[f39,f25]) ).
fof(f193,plain,
! [X0,X1] : meet(join(X0,sF0),join(sF1,X1)) = join(meet(X1,join(X0,sF0)),join(sF0,meet(X0,sF1))),
inference(superposition,[],[f2,f25]) ).
fof(f195,plain,
! [X0] : join(sF0,meet(X0,sF1)) = join(sF0,meet(X0,join(sF0,meet(X0,sF1)))),
inference(forward_demodulation,[],[f191,f17]) ).
fof(f197,plain,
meet(sF1,sF1) = join(meet(meet(sF1,sF1),sF1),sF0),
inference(superposition,[],[f24,f189]) ).
fof(f204,plain,
meet(sF1,sF1) = join(meet(sF1,sF1),sF0),
inference(forward_demodulation,[],[f197,f39]) ).
fof(f209,plain,
! [X0,X1] : meet(join(b,X0),join(sF2,X1)) = join(meet(X1,join(b,X0)),join(meet(X0,sF2),b)),
inference(superposition,[],[f2,f26]) ).
fof(f211,plain,
join(a,meet(meet(sF2,sF3),sF3)) = meet(sF3,meet(sF3,sF3)),
inference(superposition,[],[f23,f134]) ).
fof(f219,plain,
meet(sF3,meet(sF3,sF3)) = join(a,meet(sF2,sF3)),
inference(forward_demodulation,[],[f211,f39]) ).
fof(f224,plain,
sF2 = join(b,meet(sF2,sF2)),
inference(superposition,[],[f1,f27]) ).
fof(f232,plain,
meet(sF2,sF2) = join(meet(meet(sF2,sF2),sF2),b),
inference(superposition,[],[f26,f224]) ).
fof(f239,plain,
meet(sF2,sF2) = join(meet(sF2,sF2),b),
inference(forward_demodulation,[],[f232,f39]) ).
fof(f246,plain,
! [X0,X1] : meet(meet(X0,sF0),join(meet(b,X0),X1)) = join(meet(X1,meet(X0,sF0)),meet(b,X0)),
inference(superposition,[],[f2,f35]) ).
fof(f247,plain,
! [X0,X1] : meet(meet(X0,sF0),join(X1,meet(b,X0))) = join(meet(b,X0),meet(X1,meet(X0,sF0))),
inference(superposition,[],[f2,f35]) ).
fof(f266,plain,
join(sF0,meet(meet(c,sF1),sF1)) = meet(sF1,meet(sF1,sF1)),
inference(superposition,[],[f25,f171]) ).
fof(f273,plain,
meet(sF1,meet(sF1,sF1)) = join(sF0,meet(c,sF1)),
inference(forward_demodulation,[],[f266,f39]) ).
fof(f368,plain,
! [X0] : join(c,meet(sF0,meet(join(c,X0),sF1))) = meet(meet(join(c,X0),sF1),sF1),
inference(superposition,[],[f70,f70]) ).
fof(f378,plain,
! [X0] : meet(join(c,X0),sF1) = join(c,meet(sF0,meet(join(c,X0),sF1))),
inference(forward_demodulation,[],[f368,f39]) ).
fof(f390,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(meet(join(meet(X1,join(X0,X1)),X0),join(X0,X1)),X0)),
inference(superposition,[],[f80,f80]) ).
fof(f411,plain,
! [X0] : join(X0,X0) = join(X0,join(X0,X0)),
inference(superposition,[],[f80,f1]) ).
fof(f412,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,join(join(meet(join(X0,X1),join(X0,X1)),X0),X0)),
inference(superposition,[],[f80,f19]) ).
fof(f413,plain,
join(a,sF0) = join(a,join(join(meet(sF0,sF0),a),a)),
inference(superposition,[],[f80,f20]) ).
fof(f414,plain,
join(sF0,sF1) = join(sF0,join(join(meet(sF1,sF1),sF0),sF0)),
inference(superposition,[],[f80,f24]) ).
fof(f432,plain,
! [X0] : meet(sF1,join(sF0,X0)) = join(meet(join(meet(X0,join(sF0,X0)),sF0),sF1),sF0),
inference(superposition,[],[f24,f80]) ).
fof(f435,plain,
! [X0] : join(meet(X0,sF1),sF0) = join(meet(join(meet(X0,join(sF0,X0)),sF0),sF1),sF0),
inference(forward_demodulation,[],[f432,f24]) ).
fof(f442,plain,
join(sF0,sF1) = join(sF0,join(meet(sF1,sF1),sF0)),
inference(forward_demodulation,[],[f414,f204]) ).
fof(f443,plain,
join(a,sF0) = join(a,join(meet(sF0,sF0),a)),
inference(forward_demodulation,[],[f413,f124]) ).
fof(f444,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,join(join(join(meet(X1,join(X0,X1)),X0),X0),X0)),
inference(forward_demodulation,[],[f412,f19]) ).
fof(f453,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(join(meet(X1,join(X0,X1)),X0),X0)),
inference(forward_demodulation,[],[f390,f104]) ).
fof(f456,plain,
join(sF0,meet(sF1,sF1)) = join(sF0,sF1),
inference(forward_demodulation,[],[f442,f204]) ).
fof(f457,plain,
join(a,meet(sF0,sF0)) = join(a,sF0),
inference(forward_demodulation,[],[f443,f124]) ).
fof(f464,plain,
sF1 = join(sF0,sF1),
inference(forward_demodulation,[],[f456,f189]) ).
fof(f465,plain,
sF0 = join(a,sF0),
inference(forward_demodulation,[],[f457,f83]) ).
fof(f556,plain,
join(sF0,meet(a,sF1)) = meet(sF1,sF0),
inference(superposition,[],[f25,f465]) ).
fof(f723,plain,
meet(sF0,meet(sF0,sF0)) = join(a,meet(meet(sF0,sF0),sF0)),
inference(superposition,[],[f18,f124]) ).
fof(f727,plain,
! [X0] : meet(meet(sF0,sF0),join(meet(sF0,sF0),X0)) = join(meet(X0,meet(sF0,sF0)),meet(sF0,sF0)),
inference(superposition,[],[f19,f124]) ).
fof(f732,plain,
! [X0] : meet(sF0,sF0) = join(meet(X0,meet(sF0,sF0)),meet(sF0,sF0)),
inference(forward_demodulation,[],[f727,f1]) ).
fof(f733,plain,
join(a,meet(sF0,sF0)) = meet(sF0,meet(sF0,sF0)),
inference(forward_demodulation,[],[f723,f39]) ).
fof(f734,plain,
join(a,meet(sF0,sF0)) = join(a,meet(b,sF0)),
inference(forward_demodulation,[],[f733,f132]) ).
fof(f735,plain,
sF0 = join(a,meet(b,sF0)),
inference(forward_demodulation,[],[f734,f83]) ).
fof(f823,plain,
! [X0,X1] : meet(X1,join(meet(X0,X1),X0)) = join(meet(X0,meet(X1,join(meet(X0,X1),X0))),meet(X0,X1)),
inference(superposition,[],[f39,f40]) ).
fof(f834,plain,
! [X0,X1] : meet(X1,join(X0,X0)) = join(meet(X0,meet(X1,join(X0,X0))),meet(X0,X1)),
inference(forward_demodulation,[],[f823,f60]) ).
fof(f1011,plain,
meet(sF3,meet(sF3,sF3)) = join(a,meet(meet(sF3,sF3),sF3)),
inference(superposition,[],[f23,f170]) ).
fof(f1023,plain,
join(a,meet(sF3,sF3)) = meet(sF3,meet(sF3,sF3)),
inference(forward_demodulation,[],[f1011,f39]) ).
fof(f1024,plain,
join(a,meet(sF3,sF3)) = join(a,meet(sF2,sF3)),
inference(forward_demodulation,[],[f1023,f219]) ).
fof(f1025,plain,
sF3 = join(a,meet(sF2,sF3)),
inference(forward_demodulation,[],[f1024,f154]) ).
fof(f1117,plain,
! [X0,X1] : meet(join(sF1,X0),join(join(X0,sF0),X1)) = join(meet(X1,join(sF1,X0)),join(X0,join(sF0,meet(X0,sF1)))),
inference(superposition,[],[f76,f25]) ).
fof(f1233,plain,
! [X2,X0,X1] : meet(join(X0,X0),join(X1,join(X0,X2))) = join(join(X0,X0),meet(X1,join(X0,X0))),
inference(superposition,[],[f77,f1]) ).
fof(f1357,plain,
meet(sF1,meet(sF1,sF1)) = join(sF0,meet(meet(sF1,sF1),sF1)),
inference(superposition,[],[f25,f204]) ).
fof(f1372,plain,
join(sF0,meet(sF1,sF1)) = meet(sF1,meet(sF1,sF1)),
inference(forward_demodulation,[],[f1357,f39]) ).
fof(f1373,plain,
join(sF0,meet(sF1,sF1)) = join(sF0,meet(c,sF1)),
inference(forward_demodulation,[],[f1372,f273]) ).
fof(f1374,plain,
sF1 = join(sF0,meet(c,sF1)),
inference(forward_demodulation,[],[f1373,f189]) ).
fof(f1415,plain,
! [X2,X3,X0,X1] : meet(join(X1,X0),join(join(X1,X3),join(X1,X2))) = join(join(meet(X0,join(X1,X2)),X1),join(meet(X0,join(X1,X3)),X1)),
inference(superposition,[],[f106,f19]) ).
fof(f1876,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X1)) = meet(join(meet(X0,X1),X2),meet(X1,join(X0,X0))),
inference(superposition,[],[f66,f1]) ).
fof(f1901,plain,
! [X2,X0,X1] : meet(X1,join(X0,X0)) = meet(join(meet(X0,X1),X2),meet(X1,join(X0,X0))),
inference(forward_demodulation,[],[f1876,f2]) ).
fof(f1971,plain,
! [X2,X0,X1] : join(X0,X0) = meet(join(X0,X0),meet(join(X0,X0),join(X2,join(X0,X1)))),
inference(superposition,[],[f75,f1]) ).
fof(f2571,plain,
join(meet(meet(a,sF1),sF1),sF0) = meet(sF1,meet(sF1,sF0)),
inference(superposition,[],[f24,f556]) ).
fof(f2595,plain,
meet(sF1,meet(sF1,sF0)) = join(meet(a,sF1),sF0),
inference(forward_demodulation,[],[f2571,f39]) ).
fof(f2611,plain,
! [X2,X0,X1] : meet(X0,join(meet(X2,X0),X1)) = meet(X0,meet(X0,join(X1,X2))),
inference(superposition,[],[f59,f2]) ).
fof(f2727,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = meet(X0,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f2611,f60]) ).
fof(f2775,plain,
! [X0] : meet(join(a,X0),join(b,a)) = meet(join(a,X0),meet(join(a,X0),sF0)),
inference(superposition,[],[f60,f97]) ).
fof(f2857,plain,
! [X0] : meet(join(a,X0),meet(join(a,X0),sF0)) = join(a,meet(b,join(a,X0))),
inference(forward_demodulation,[],[f2775,f17]) ).
fof(f4118,plain,
meet(sF0,sF0) = join(meet(sF0,sF0),join(join(meet(a,meet(sF0,sF0)),meet(sF0,sF0)),meet(sF0,sF0))),
inference(superposition,[],[f453,f124]) ).
fof(f4273,plain,
meet(sF0,sF0) = join(meet(sF0,sF0),join(meet(sF0,sF0),meet(sF0,sF0))),
inference(forward_demodulation,[],[f4118,f732]) ).
fof(f4303,plain,
meet(sF0,sF0) = join(meet(sF0,sF0),meet(sF0,sF0)),
inference(forward_demodulation,[],[f4273,f411]) ).
fof(f4308,plain,
meet(sF0,sF0) = meet(sF0,join(sF0,sF0)),
inference(forward_demodulation,[],[f4303,f2]) ).
fof(f4309,plain,
sF0 = meet(sF0,sF0),
inference(forward_demodulation,[],[f4308,f1]) ).
fof(f4313,plain,
sF0 = join(sF0,a),
inference(superposition,[],[f124,f4309]) ).
fof(f4318,plain,
! [X0] : meet(sF0,join(X0,sF0)) = join(sF0,meet(X0,sF0)),
inference(superposition,[],[f2,f4309]) ).
fof(f4319,plain,
! [X0] : meet(sF0,join(sF0,X0)) = join(meet(X0,sF0),sF0),
inference(superposition,[],[f2,f4309]) ).
fof(f4336,plain,
! [X0] : sF0 = join(meet(X0,sF0),sF0),
inference(forward_demodulation,[],[f4319,f1]) ).
fof(f4409,plain,
sF0 = join(sF0,join(meet(a,sF0),sF0)),
inference(superposition,[],[f80,f4313]) ).
fof(f4421,plain,
sF0 = join(sF0,sF0),
inference(forward_demodulation,[],[f4409,f4336]) ).
fof(f4477,plain,
join(sF0,meet(sF0,sF1)) = meet(sF1,sF0),
inference(superposition,[],[f25,f4421]) ).
fof(f4516,plain,
join(sF0,sF0) = meet(sF1,sF0),
inference(forward_demodulation,[],[f4477,f15]) ).
fof(f4530,plain,
sF0 = meet(sF1,sF0),
inference(forward_demodulation,[],[f4516,f4421]) ).
fof(f4592,plain,
! [X0] : meet(sF0,join(sF1,X0)) = meet(sF0,join(sF0,X0)),
inference(superposition,[],[f60,f4530]) ).
fof(f4600,plain,
! [X0] : sF0 = meet(sF0,join(sF1,X0)),
inference(forward_demodulation,[],[f4592,f1]) ).
fof(f4673,plain,
! [X0] : meet(sF0,sF0) = meet(sF0,join(X0,sF0)),
inference(superposition,[],[f60,f4336]) ).
fof(f4677,plain,
! [X0] : meet(sF1,sF0) = join(sF0,meet(meet(X0,sF0),sF1)),
inference(superposition,[],[f25,f4336]) ).
fof(f4718,plain,
! [X0] : sF0 = join(sF0,meet(meet(X0,sF0),sF1)),
inference(forward_demodulation,[],[f4677,f4530]) ).
fof(f4722,plain,
! [X0] : sF0 = meet(sF0,join(X0,sF0)),
inference(forward_demodulation,[],[f4673,f4309]) ).
fof(f5014,plain,
! [X0] : sF0 = meet(sF0,meet(join(sF0,X0),sF1)),
inference(superposition,[],[f4722,f100]) ).
fof(f5022,plain,
join(c,sF0) = meet(join(c,sF0),sF1),
inference(superposition,[],[f70,f4722]) ).
fof(f5040,plain,
! [X0] : join(X0,sF0) = join(X0,join(sF0,X0)),
inference(superposition,[],[f80,f4722]) ).
fof(f5377,plain,
! [X0,X1] : meet(join(sF1,X0),join(X1,sF0)) = join(sF0,meet(X1,join(sF1,X0))),
inference(superposition,[],[f2,f4600]) ).
fof(f6115,plain,
! [X0] : sF0 = join(sF0,meet(meet(X0,sF0),sF0)),
inference(superposition,[],[f195,f4718]) ).
fof(f6165,plain,
! [X0] : sF0 = join(sF0,meet(X0,sF0)),
inference(forward_demodulation,[],[f6115,f39]) ).
fof(f6785,plain,
join(sF1,sF0) = join(sF1,sF1),
inference(superposition,[],[f5040,f464]) ).
fof(f7076,plain,
! [X0] : meet(join(sF1,X0),join(sF1,sF0)) = join(meet(sF1,join(sF1,X0)),sF1),
inference(superposition,[],[f19,f6785]) ).
fof(f7104,plain,
! [X0] : join(sF1,sF1) = meet(join(sF1,X0),join(sF1,sF0)),
inference(forward_demodulation,[],[f7076,f1]) ).
fof(f7114,plain,
! [X0] : join(sF1,sF1) = join(meet(sF0,join(sF1,X0)),sF1),
inference(forward_demodulation,[],[f7104,f19]) ).
fof(f7122,plain,
join(sF0,sF1) = join(sF1,sF1),
inference(forward_demodulation,[],[f7114,f4600]) ).
fof(f7126,plain,
sF1 = join(sF1,sF1),
inference(forward_demodulation,[],[f7122,f464]) ).
fof(f7215,plain,
sF1 = join(sF1,sF0),
inference(superposition,[],[f6785,f7126]) ).
fof(f7221,plain,
! [X0] : meet(sF1,join(sF1,X0)) = join(meet(X0,sF1),sF1),
inference(superposition,[],[f19,f7126]) ).
fof(f7254,plain,
! [X0] : sF1 = join(meet(X0,sF1),sF1),
inference(forward_demodulation,[],[f7221,f1]) ).
fof(f7362,plain,
! [X0] : meet(join(sF0,X0),sF1) = join(sF0,meet(sF1,join(sF0,X0))),
inference(superposition,[],[f17,f7215]) ).
fof(f7397,plain,
! [X0] : meet(join(sF0,X0),sF1) = join(sF0,join(meet(X0,sF1),sF0)),
inference(forward_demodulation,[],[f7362,f24]) ).
fof(f7590,plain,
sF1 = join(join(c,sF0),sF1),
inference(superposition,[],[f7254,f5022]) ).
fof(f8306,plain,
meet(sF3,join(sF3,sF3)) = meet(meet(sF3,sF3),meet(sF3,join(sF3,sF3))),
inference(superposition,[],[f1901,f170]) ).
fof(f8314,plain,
meet(sF2,join(sF2,sF2)) = meet(meet(sF2,sF2),meet(sF2,join(sF2,sF2))),
inference(superposition,[],[f1901,f239]) ).
fof(f8316,plain,
! [X0] : meet(sF1,join(join(meet(X0,join(sF0,X0)),sF0),join(meet(X0,join(sF0,X0)),sF0))) = meet(join(meet(X0,sF1),sF0),meet(sF1,join(join(meet(X0,join(sF0,X0)),sF0),join(meet(X0,join(sF0,X0)),sF0)))),
inference(superposition,[],[f1901,f435]) ).
fof(f8330,plain,
! [X0,X1] : meet(join(meet(X0,X0),X1),X0) = X0,
inference(superposition,[],[f1901,f1]) ).
fof(f8404,plain,
! [X0] : meet(sF1,meet(join(sF0,X0),join(join(sF0,X0),join(sF0,X0)))) = meet(join(meet(X0,sF1),sF0),meet(sF1,meet(join(sF0,X0),join(join(sF0,X0),join(sF0,X0))))),
inference(forward_demodulation,[],[f8316,f1415]) ).
fof(f8405,plain,
meet(sF2,sF2) = meet(sF2,join(sF2,sF2)),
inference(forward_demodulation,[],[f8314,f21]) ).
fof(f8408,plain,
meet(sF3,sF3) = meet(sF3,join(sF3,sF3)),
inference(forward_demodulation,[],[f8306,f21]) ).
fof(f8504,plain,
! [X0] : meet(sF1,join(sF0,X0)) = meet(join(meet(X0,sF1),sF0),meet(sF1,join(sF0,X0))),
inference(forward_demodulation,[],[f8404,f1]) ).
fof(f8505,plain,
sF2 = meet(sF2,sF2),
inference(forward_demodulation,[],[f8405,f1]) ).
fof(f8507,plain,
sF3 = meet(sF3,sF3),
inference(forward_demodulation,[],[f8408,f1]) ).
fof(f8578,plain,
! [X0] : join(meet(X0,sF1),sF0) = meet(join(meet(X0,sF1),sF0),join(meet(X0,sF1),sF0)),
inference(forward_demodulation,[],[f8504,f24]) ).
fof(f8639,plain,
! [X0] : join(meet(X0,sF1),sF0) = join(meet(sF0,join(meet(X0,sF1),sF0)),meet(X0,sF1)),
inference(forward_demodulation,[],[f8578,f19]) ).
fof(f8680,plain,
! [X0] : join(meet(X0,sF1),sF0) = join(join(sF0,meet(meet(X0,sF1),sF0)),meet(X0,sF1)),
inference(forward_demodulation,[],[f8639,f4318]) ).
fof(f8705,plain,
! [X0] : join(meet(X0,sF1),sF0) = join(sF0,meet(X0,sF1)),
inference(forward_demodulation,[],[f8680,f6165]) ).
fof(f8738,plain,
! [X0] : meet(sF2,join(sF2,X0)) = join(meet(X0,sF2),sF2),
inference(superposition,[],[f2,f8505]) ).
fof(f8751,plain,
meet(sF2,join(sF2,sF2)) = join(meet(sF2,meet(sF2,join(sF2,sF2))),sF2),
inference(superposition,[],[f834,f8505]) ).
fof(f8754,plain,
meet(sF2,join(sF2,sF2)) = join(meet(sF2,join(sF2,sF2)),sF2),
inference(forward_demodulation,[],[f8751,f2727]) ).
fof(f8762,plain,
! [X0] : sF2 = join(meet(X0,sF2),sF2),
inference(forward_demodulation,[],[f8738,f1]) ).
fof(f8769,plain,
sF2 = join(sF2,sF2),
inference(forward_demodulation,[],[f8754,f1]) ).
fof(f8807,plain,
! [X0] : join(meet(sF3,sF3),meet(sF3,sF3)) = meet(join(meet(sF3,sF3),meet(sF3,sF3)),meet(join(meet(sF3,sF3),meet(sF3,sF3)),join(X0,meet(sF3,sF3)))),
inference(superposition,[],[f1971,f170]) ).
fof(f8874,plain,
! [X0,X1] : join(join(meet(X1,join(X0,X1)),X0),join(meet(X1,join(X0,X1)),X0)) = meet(join(join(meet(X1,join(X0,X1)),X0),join(meet(X1,join(X0,X1)),X0)),meet(join(join(meet(X1,join(X0,X1)),X0),join(meet(X1,join(X0,X1)),X0)),join(X0,X1))),
inference(superposition,[],[f1971,f453]) ).
fof(f8908,plain,
! [X0,X1] : join(join(meet(X1,join(X0,X1)),X0),join(meet(X1,join(X0,X1)),X0)) = meet(join(join(meet(X1,join(X0,X1)),X0),join(meet(X1,join(X0,X1)),X0)),join(X1,X0)),
inference(forward_demodulation,[],[f8874,f2727]) ).
fof(f8970,plain,
! [X0] : join(meet(sF3,sF3),meet(sF3,sF3)) = meet(join(meet(sF3,sF3),meet(sF3,sF3)),join(meet(sF3,sF3),X0)),
inference(forward_demodulation,[],[f8807,f2727]) ).
fof(f8998,plain,
! [X0,X1] : meet(join(X0,X1),join(join(X0,X1),join(X0,X1))) = meet(meet(join(X0,X1),join(join(X0,X1),join(X0,X1))),join(X1,X0)),
inference(forward_demodulation,[],[f8908,f1415]) ).
fof(f9028,plain,
! [X0] : join(meet(sF3,sF3),meet(sF3,sF3)) = join(meet(X0,join(meet(sF3,sF3),meet(sF3,sF3))),meet(sF3,sF3)),
inference(forward_demodulation,[],[f8970,f19]) ).
fof(f9050,plain,
! [X0,X1] : join(X0,X1) = meet(join(X0,X1),join(X1,X0)),
inference(forward_demodulation,[],[f8998,f1]) ).
fof(f9066,plain,
! [X0] : join(sF3,sF3) = join(meet(X0,join(sF3,sF3)),sF3),
inference(forward_demodulation,[],[f9028,f8507]) ).
fof(f9079,plain,
! [X0,X1] : join(X0,X1) = join(X0,meet(X1,join(X0,X1))),
inference(forward_demodulation,[],[f9050,f17]) ).
fof(f9108,plain,
! [X0] : meet(sF3,join(sF3,X0)) = join(meet(X0,sF3),sF3),
inference(superposition,[],[f2,f8507]) ).
fof(f9121,plain,
meet(sF3,join(sF3,sF3)) = join(meet(sF3,meet(sF3,join(sF3,sF3))),sF3),
inference(superposition,[],[f834,f8507]) ).
fof(f9122,plain,
! [X0] : meet(sF3,join(sF3,sF3)) = meet(join(sF3,X0),meet(sF3,join(sF3,sF3))),
inference(superposition,[],[f1901,f8507]) ).
fof(f9123,plain,
! [X0] : sF3 = meet(join(sF3,X0),sF3),
inference(forward_demodulation,[],[f9122,f1]) ).
fof(f9124,plain,
meet(sF3,join(sF3,sF3)) = join(meet(sF3,join(sF3,sF3)),sF3),
inference(forward_demodulation,[],[f9121,f2727]) ).
fof(f9132,plain,
! [X0] : sF3 = join(meet(X0,sF3),sF3),
inference(forward_demodulation,[],[f9108,f1]) ).
fof(f9135,plain,
join(sF3,sF3) = meet(sF3,join(sF3,sF3)),
inference(forward_demodulation,[],[f9124,f9066]) ).
fof(f9140,plain,
sF3 = join(sF3,sF3),
inference(forward_demodulation,[],[f9135,f1]) ).
fof(f9267,plain,
! [X0,X1] : join(X0,meet(join(X0,X1),join(X0,X1))) = join(X0,meet(join(X0,X1),join(X0,join(X0,X1)))),
inference(superposition,[],[f78,f59]) ).
fof(f9413,plain,
! [X0,X1] : join(X0,meet(join(X0,X1),join(X0,X1))) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f9267,f9079]) ).
fof(f9450,plain,
! [X0,X1] : join(X0,join(meet(X1,join(X0,X1)),X0)) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f9413,f19]) ).
fof(f9463,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(forward_demodulation,[],[f9450,f80]) ).
fof(f11016,plain,
! [X0] : meet(sF2,sF2) = meet(sF2,join(X0,sF2)),
inference(superposition,[],[f60,f8762]) ).
fof(f11073,plain,
! [X0] : sF2 = meet(sF2,join(X0,sF2)),
inference(forward_demodulation,[],[f11016,f8505]) ).
fof(f11426,plain,
! [X0] : meet(sF3,sF3) = meet(sF3,join(X0,sF3)),
inference(superposition,[],[f60,f9132]) ).
fof(f11484,plain,
! [X0] : sF3 = meet(sF3,join(X0,sF3)),
inference(forward_demodulation,[],[f11426,f8507]) ).
fof(f11858,plain,
sF2 = meet(sF2,sF3),
inference(superposition,[],[f11073,f11]) ).
fof(f11866,plain,
meet(join(a,sF2),sF3) = join(sF2,a),
inference(superposition,[],[f98,f11073]) ).
fof(f11945,plain,
meet(sF3,sF3) = join(sF2,a),
inference(forward_demodulation,[],[f11866,f11]) ).
fof(f11957,plain,
sF3 = join(sF2,a),
inference(forward_demodulation,[],[f11945,f8507]) ).
fof(f12095,plain,
sF3 = join(sF2,sF3),
inference(superposition,[],[f9132,f11858]) ).
fof(f12096,plain,
! [X0] : meet(sF3,join(X0,sF2)) = join(sF2,meet(X0,sF3)),
inference(superposition,[],[f2,f11858]) ).
fof(f12325,plain,
sF3 = join(sF2,join(join(meet(a,sF3),sF2),sF2)),
inference(superposition,[],[f453,f11957]) ).
fof(f12327,plain,
! [X0] : join(sF2,sF2) = meet(join(sF2,sF2),meet(join(sF2,sF2),join(X0,sF3))),
inference(superposition,[],[f1971,f11957]) ).
fof(f12328,plain,
! [X0] : join(sF2,sF2) = meet(join(sF2,sF2),join(sF3,X0)),
inference(forward_demodulation,[],[f12327,f2727]) ).
fof(f12329,plain,
sF3 = join(sF2,join(join(a,sF2),sF2)),
inference(forward_demodulation,[],[f12325,f14]) ).
fof(f12338,plain,
! [X0] : sF2 = meet(sF2,join(sF3,X0)),
inference(forward_demodulation,[],[f12328,f8769]) ).
fof(f12339,plain,
sF3 = join(sF2,join(sF3,sF2)),
inference(forward_demodulation,[],[f12329,f11]) ).
fof(f12513,plain,
! [X0] : meet(join(sF3,X0),sF3) = join(sF3,meet(sF2,join(sF3,X0))),
inference(superposition,[],[f17,f12095]) ).
fof(f12551,plain,
! [X0] : meet(join(sF3,X0),sF3) = join(sF3,sF2),
inference(forward_demodulation,[],[f12513,f12338]) ).
fof(f12559,plain,
sF3 = join(sF3,sF2),
inference(forward_demodulation,[],[f12551,f9123]) ).
fof(f13299,plain,
! [X0,X1] : meet(join(X0,sF3),join(sF3,sF3)) = meet(join(sF3,X1),meet(join(X0,sF3),join(sF3,sF3))),
inference(superposition,[],[f1901,f11484]) ).
fof(f13300,plain,
! [X0,X1] : meet(join(X0,sF3),sF3) = meet(join(sF3,X1),meet(join(X0,sF3),sF3)),
inference(forward_demodulation,[],[f13299,f9140]) ).
fof(f13754,plain,
! [X0] : join(meet(X0,join(sF3,sF2)),sF3) = meet(join(meet(X0,join(sF3,sF2)),sF3),meet(join(sF3,X0),sF3)),
inference(superposition,[],[f105,f12339]) ).
fof(f13755,plain,
! [X0] : join(sF3,meet(X0,join(sF3,sF2))) = meet(join(sF3,meet(X0,join(sF3,sF2))),meet(join(X0,sF3),sF3)),
inference(superposition,[],[f75,f12339]) ).
fof(f13800,plain,
! [X0] : join(sF3,meet(X0,join(sF3,sF2))) = meet(join(X0,sF3),sF3),
inference(forward_demodulation,[],[f13755,f13300]) ).
fof(f13801,plain,
! [X0] : join(meet(X0,join(sF3,sF2)),sF3) = meet(join(meet(X0,join(sF3,sF2)),sF3),sF3),
inference(forward_demodulation,[],[f13754,f9123]) ).
fof(f13818,plain,
! [X0] : join(sF3,meet(X0,sF3)) = meet(join(X0,sF3),sF3),
inference(forward_demodulation,[],[f13800,f12559]) ).
fof(f13819,plain,
! [X0] : join(meet(X0,sF3),sF3) = meet(join(meet(X0,sF3),sF3),sF3),
inference(forward_demodulation,[],[f13801,f12559]) ).
fof(f13828,plain,
! [X0] : join(meet(X0,sF3),sF3) = join(sF3,meet(meet(X0,sF3),sF3)),
inference(forward_demodulation,[],[f13819,f13818]) ).
fof(f13830,plain,
! [X0] : join(sF3,meet(X0,sF3)) = join(meet(X0,sF3),sF3),
inference(forward_demodulation,[],[f13828,f39]) ).
fof(f13832,plain,
! [X0] : sF3 = join(sF3,meet(X0,sF3)),
inference(forward_demodulation,[],[f13830,f9132]) ).
fof(f14482,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f39,f8330]) ).
fof(f14901,plain,
! [X0,X1] : meet(join(X0,X1),X0) = X0,
inference(superposition,[],[f8330,f14482]) ).
fof(f14903,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(X0,meet(X1,X0)),
inference(superposition,[],[f2,f14482]) ).
fof(f14904,plain,
! [X0,X1] : meet(X0,join(X0,X1)) = join(meet(X1,X0),X0),
inference(superposition,[],[f2,f14482]) ).
fof(f14917,plain,
! [X0] : meet(X0,join(X0,X0)) = join(meet(X0,meet(X0,join(X0,X0))),X0),
inference(superposition,[],[f834,f14482]) ).
fof(f15009,plain,
! [X0,X1] : join(X0,X1) = join(meet(X1,join(X0,X1)),X0),
inference(superposition,[],[f19,f14482]) ).
fof(f15020,plain,
b = meet(b,meet(b,sF0)),
inference(superposition,[],[f35,f14482]) ).
fof(f15023,plain,
c = meet(c,meet(c,sF1)),
inference(superposition,[],[f38,f14482]) ).
fof(f15114,plain,
! [X0] : meet(X0,join(X0,X0)) = join(meet(X0,join(X0,X0)),X0),
inference(forward_demodulation,[],[f14917,f2727]) ).
fof(f15122,plain,
! [X0,X1] : join(meet(X1,X0),X0) = X0,
inference(forward_demodulation,[],[f14904,f1]) ).
fof(f15154,plain,
! [X0] : join(X0,X0) = meet(X0,join(X0,X0)),
inference(forward_demodulation,[],[f15114,f15009]) ).
fof(f15170,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[],[f15154,f1]) ).
fof(f15302,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(X0,meet(X1,join(X0,meet(X1,X0)))),
inference(superposition,[],[f78,f15170]) ).
fof(f15315,plain,
! [X0,X1] : join(X0,X0) = meet(join(X0,X0),meet(join(X0,X0),join(X0,X1))),
inference(superposition,[],[f1971,f15170]) ).
fof(f15349,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,join(X0,X0)),
inference(superposition,[],[f2,f15170]) ).
fof(f15352,plain,
! [X0,X1] : meet(X1,meet(X0,X1)) = meet(X1,join(X0,meet(X0,X1))),
inference(superposition,[],[f60,f15170]) ).
fof(f15362,plain,
! [X0] : meet(a,join(sF0,X0)) = join(meet(X0,a),join(meet(a,sF0),a)),
inference(superposition,[],[f122,f15170]) ).
fof(f15381,plain,
! [X0] : meet(b,join(sF2,X0)) = join(meet(X0,b),join(meet(b,sF2),b)),
inference(superposition,[],[f209,f15170]) ).
fof(f15439,plain,
! [X0] : meet(b,join(sF2,X0)) = join(meet(X0,b),join(b,b)),
inference(forward_demodulation,[],[f15381,f16]) ).
fof(f15455,plain,
! [X0] : meet(a,join(sF0,X0)) = join(meet(X0,a),join(a,a)),
inference(forward_demodulation,[],[f15362,f13]) ).
fof(f15465,plain,
! [X0,X1] : meet(X1,join(X0,X0)) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f15352,f59]) ).
fof(f15468,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,X1),
inference(forward_demodulation,[],[f15349,f15170]) ).
fof(f15488,plain,
! [X0,X1] : join(X0,X0) = meet(join(X0,X0),join(X1,X0)),
inference(forward_demodulation,[],[f15315,f2727]) ).
fof(f15516,plain,
! [X0] : meet(b,join(sF2,X0)) = join(meet(X0,b),b),
inference(forward_demodulation,[],[f15439,f15170]) ).
fof(f15525,plain,
! [X0] : meet(a,join(sF0,X0)) = join(meet(X0,a),a),
inference(forward_demodulation,[],[f15455,f15170]) ).
fof(f15531,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f15465,f15170]) ).
fof(f15550,plain,
! [X0,X1] : join(X0,X0) = join(X0,meet(X1,join(X0,X0))),
inference(forward_demodulation,[],[f15488,f17]) ).
fof(f15566,plain,
! [X0] : b = meet(b,join(sF2,X0)),
inference(forward_demodulation,[],[f15516,f15122]) ).
fof(f15571,plain,
! [X0] : a = meet(a,join(sF0,X0)),
inference(forward_demodulation,[],[f15525,f15122]) ).
fof(f15587,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[],[f15550,f15170]) ).
fof(f15803,plain,
join(c,sF0) = meet(sF1,join(c,sF0)),
inference(superposition,[],[f14901,f7590]) ).
fof(f16175,plain,
join(sF0,meet(c,sF1)) = join(c,sF0),
inference(forward_demodulation,[],[f15803,f25]) ).
fof(f16248,plain,
sF1 = join(c,sF0),
inference(forward_demodulation,[],[f16175,f1374]) ).
fof(f16561,plain,
c = meet(c,sF1),
inference(superposition,[],[f1,f16248]) ).
fof(f16655,plain,
meet(meet(sF1,sF0),sF1) = join(meet(sF1,meet(sF1,sF0)),meet(b,sF1)),
inference(superposition,[],[f246,f7254]) ).
fof(f16754,plain,
meet(meet(sF1,sF0),sF1) = join(join(meet(a,sF1),sF0),meet(b,sF1)),
inference(forward_demodulation,[],[f16655,f2595]) ).
fof(f16808,plain,
meet(meet(sF1,sF0),sF1) = join(join(sF0,meet(a,sF1)),meet(b,sF1)),
inference(forward_demodulation,[],[f16754,f8705]) ).
fof(f16848,plain,
meet(meet(sF1,sF0),sF1) = join(meet(sF1,sF0),meet(b,sF1)),
inference(forward_demodulation,[],[f16808,f556]) ).
fof(f16879,plain,
meet(meet(sF0,sF1),sF1) = join(meet(sF0,sF1),meet(b,sF1)),
inference(forward_demodulation,[],[f16848,f15468]) ).
fof(f16904,plain,
meet(meet(sF0,sF1),sF1) = meet(sF1,join(b,sF0)),
inference(forward_demodulation,[],[f16879,f2]) ).
fof(f16921,plain,
meet(meet(sF0,sF1),sF1) = join(sF0,meet(b,sF1)),
inference(forward_demodulation,[],[f16904,f25]) ).
fof(f16928,plain,
meet(sF1,meet(sF0,sF1)) = join(sF0,meet(b,sF1)),
inference(forward_demodulation,[],[f16921,f15468]) ).
fof(f16932,plain,
meet(sF1,sF0) = join(sF0,meet(b,sF1)),
inference(forward_demodulation,[],[f16928,f15531]) ).
fof(f16936,plain,
meet(sF0,sF1) = join(sF0,meet(b,sF1)),
inference(forward_demodulation,[],[f16932,f15468]) ).
fof(f16939,plain,
sF0 = join(sF0,meet(b,sF1)),
inference(forward_demodulation,[],[f16936,f15]) ).
fof(f17050,plain,
join(meet(b,join(a,meet(b,sF0))),meet(a,meet(join(a,meet(b,sF0)),sF0))) = meet(meet(join(a,meet(b,sF0)),sF0),join(a,meet(b,sF0))),
inference(superposition,[],[f247,f89]) ).
fof(f17159,plain,
join(meet(b,join(a,meet(b,sF0))),meet(a,meet(join(a,meet(b,sF0)),sF0))) = meet(join(a,meet(b,sF0)),meet(join(a,meet(b,sF0)),sF0)),
inference(forward_demodulation,[],[f17050,f15468]) ).
fof(f17205,plain,
join(a,meet(b,join(a,meet(b,sF0)))) = join(meet(b,join(a,meet(b,sF0))),meet(a,meet(join(a,meet(b,sF0)),sF0))),
inference(forward_demodulation,[],[f17159,f2857]) ).
fof(f17240,plain,
join(a,meet(b,join(a,meet(b,sF0)))) = join(meet(b,join(a,meet(b,sF0))),meet(a,meet(sF0,join(a,meet(b,sF0))))),
inference(forward_demodulation,[],[f17205,f15468]) ).
fof(f17269,plain,
join(a,meet(b,join(a,meet(b,sF0)))) = join(meet(b,join(a,meet(b,sF0))),meet(a,meet(sF0,join(a,b)))),
inference(forward_demodulation,[],[f17240,f59]) ).
fof(f17290,plain,
join(a,meet(b,join(a,meet(b,sF0)))) = join(meet(b,join(a,meet(b,sF0))),meet(a,join(meet(b,sF0),a))),
inference(forward_demodulation,[],[f17269,f20]) ).
fof(f17302,plain,
join(a,meet(b,join(a,meet(b,sF0)))) = join(meet(b,join(a,meet(b,sF0))),join(a,meet(meet(b,sF0),a))),
inference(forward_demodulation,[],[f17290,f14903]) ).
fof(f17310,plain,
join(meet(b,join(a,meet(b,sF0))),a) = join(a,meet(b,join(a,meet(b,sF0)))),
inference(forward_demodulation,[],[f17302,f15587]) ).
fof(f17315,plain,
join(a,meet(b,sF0)) = join(meet(b,join(a,meet(b,sF0))),a),
inference(forward_demodulation,[],[f17310,f89]) ).
fof(f17318,plain,
join(a,meet(b,sF0)) = meet(join(a,meet(b,sF0)),sF0),
inference(forward_demodulation,[],[f17315,f97]) ).
fof(f17320,plain,
join(a,meet(b,sF0)) = meet(sF0,join(a,meet(b,sF0))),
inference(forward_demodulation,[],[f17318,f15468]) ).
fof(f17322,plain,
meet(sF0,join(a,b)) = join(a,meet(b,sF0)),
inference(forward_demodulation,[],[f17320,f59]) ).
fof(f17324,plain,
sF0 = meet(sF0,join(a,b)),
inference(forward_demodulation,[],[f17322,f735]) ).
fof(f17325,plain,
sF0 = join(meet(b,sF0),a),
inference(forward_demodulation,[],[f17324,f20]) ).
fof(f18598,plain,
b = meet(b,meet(meet(b,sF0),sF0)),
inference(superposition,[],[f35,f15020]) ).
fof(f18627,plain,
b = meet(b,meet(sF0,meet(b,sF0))),
inference(forward_demodulation,[],[f18598,f15468]) ).
fof(f18635,plain,
b = meet(b,meet(sF0,b)),
inference(forward_demodulation,[],[f18627,f15531]) ).
fof(f18642,plain,
b = meet(b,sF0),
inference(forward_demodulation,[],[f18635,f15531]) ).
fof(f18915,plain,
sF0 = join(b,a),
inference(superposition,[],[f17325,f18642]) ).
fof(f18935,plain,
sF0 = join(b,sF0),
inference(superposition,[],[f4336,f18642]) ).
fof(f19373,plain,
! [X0] : join(b,b) = meet(join(b,b),meet(join(b,b),join(X0,sF0))),
inference(superposition,[],[f1971,f18915]) ).
fof(f19376,plain,
! [X0] : join(b,b) = meet(join(b,b),join(sF0,X0)),
inference(forward_demodulation,[],[f19373,f2727]) ).
fof(f19402,plain,
! [X0] : b = meet(b,join(sF0,X0)),
inference(forward_demodulation,[],[f19376,f15170]) ).
fof(f20671,plain,
c = meet(c,meet(meet(c,sF1),sF2)),
inference(superposition,[],[f37,f15023]) ).
fof(f20716,plain,
c = meet(c,meet(sF2,meet(c,sF1))),
inference(forward_demodulation,[],[f20671,f15468]) ).
fof(f20734,plain,
c = meet(c,meet(sF2,c)),
inference(forward_demodulation,[],[f20716,f16561]) ).
fof(f20745,plain,
c = meet(c,sF2),
inference(forward_demodulation,[],[f20734,f15531]) ).
fof(f21174,plain,
sF2 = join(c,sF2),
inference(superposition,[],[f8762,f20745]) ).
fof(f21621,plain,
! [X0] : join(c,c) = meet(join(c,c),meet(join(c,c),join(X0,sF2))),
inference(superposition,[],[f1971,f21174]) ).
fof(f21624,plain,
! [X0] : join(c,c) = meet(join(c,c),join(sF2,X0)),
inference(forward_demodulation,[],[f21621,f2727]) ).
fof(f21647,plain,
! [X0] : c = meet(c,join(sF2,X0)),
inference(forward_demodulation,[],[f21624,f15170]) ).
fof(f24059,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(meet(join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))),sF0),sF1),sF0),
inference(superposition,[],[f435,f444]) ).
fof(f24080,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))),sF0),sF1)),
inference(forward_demodulation,[],[f24059,f8705]) ).
fof(f24291,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))),sF0))),
inference(forward_demodulation,[],[f24080,f15468]) ).
fof(f24464,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,join(sF0,meet(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))),sF1))),
inference(forward_demodulation,[],[f24291,f25]) ).
fof(f24624,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))),sF1)),
inference(forward_demodulation,[],[f24464,f9463]) ).
fof(f24748,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f24624,f15468]) ).
fof(f24858,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0)))),
inference(forward_demodulation,[],[f24748,f15468]) ).
fof(f24948,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,join(sF0,meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0)))))),
inference(forward_demodulation,[],[f24858,f17]) ).
fof(f25018,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,join(meet(meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0))),sF1),sF0)),
inference(forward_demodulation,[],[f24948,f24]) ).
fof(f25078,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(join(sF0,meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0)))),sF1),
inference(forward_demodulation,[],[f25018,f7397]) ).
fof(f25132,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(sF1,join(sF0,meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25078,f15468]) ).
fof(f25170,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(meet(meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0))),sF1),sF0),
inference(forward_demodulation,[],[f25132,f24]) ).
fof(f25199,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0))),sF1)),
inference(forward_demodulation,[],[f25170,f8705]) ).
fof(f25224,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(join(meet(X0,join(sF0,X0)),sF0),sF0),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25199,f15468]) ).
fof(f25243,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),join(join(meet(X0,join(sF0,X0)),sF0),sF0)))),
inference(forward_demodulation,[],[f25224,f15468]) ).
fof(f25257,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,join(sF0,meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0)))))),
inference(forward_demodulation,[],[f25243,f17]) ).
fof(f25270,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,join(meet(meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0))),sF1),sF0)),
inference(forward_demodulation,[],[f25257,f24]) ).
fof(f25283,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(join(sF0,meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0)))),sF1),
inference(forward_demodulation,[],[f25270,f7397]) ).
fof(f25295,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(sF1,join(sF0,meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25283,f15468]) ).
fof(f25307,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(meet(meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0))),sF1),sF0),
inference(forward_demodulation,[],[f25295,f24]) ).
fof(f25315,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0))),sF1)),
inference(forward_demodulation,[],[f25307,f8705]) ).
fof(f25323,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(meet(X0,join(sF0,X0)),sF0),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25315,f15468]) ).
fof(f25331,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),join(meet(X0,join(sF0,X0)),sF0)))),
inference(forward_demodulation,[],[f25323,f15468]) ).
fof(f25339,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,join(sF0,meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0)))))),
inference(forward_demodulation,[],[f25331,f17]) ).
fof(f25347,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,join(meet(meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0))),sF1),sF0)),
inference(forward_demodulation,[],[f25339,f24]) ).
fof(f25352,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(join(sF0,meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0)))),sF1),
inference(forward_demodulation,[],[f25347,f7397]) ).
fof(f25357,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = meet(sF1,join(sF0,meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25352,f15468]) ).
fof(f25361,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(meet(meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0))),sF1),sF0),
inference(forward_demodulation,[],[f25357,f24]) ).
fof(f25365,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0))),sF1)),
inference(forward_demodulation,[],[f25361,f8705]) ).
fof(f25369,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(meet(X0,join(sF0,X0)),join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25365,f15468]) ).
fof(f25373,plain,
! [X0] : join(meet(join(join(join(meet(X0,join(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),meet(X0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25369,f15468]) ).
fof(f25377,plain,
! [X0] : join(meet(join(join(join(join(X0,meet(sF0,X0)),sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),join(X0,meet(sF0,X0))))),
inference(forward_demodulation,[],[f25373,f14903]) ).
fof(f25381,plain,
! [X0] : join(meet(join(join(join(X0,sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(join(sF0,join(sF0,X0)),X0))),
inference(forward_demodulation,[],[f25377,f15587]) ).
fof(f25385,plain,
! [X0] : join(meet(join(join(join(X0,sF0),sF0),sF0),sF1),sF0) = join(sF0,meet(sF1,meet(X0,join(sF0,join(sF0,X0))))),
inference(forward_demodulation,[],[f25381,f15468]) ).
fof(f25389,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(meet(join(join(join(X0,sF0),sF0),sF0),sF1),sF0),
inference(forward_demodulation,[],[f25385,f9463]) ).
fof(f25393,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,meet(join(join(join(X0,sF0),sF0),sF0),sF1)),
inference(forward_demodulation,[],[f25389,f8705]) ).
fof(f25397,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,meet(sF1,join(join(join(X0,sF0),sF0),sF0))),
inference(forward_demodulation,[],[f25393,f15468]) ).
fof(f25401,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,join(sF0,meet(join(join(X0,sF0),sF0),sF1))),
inference(forward_demodulation,[],[f25397,f25]) ).
fof(f25405,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,meet(join(join(X0,sF0),sF0),sF1)),
inference(forward_demodulation,[],[f25401,f9463]) ).
fof(f25409,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,meet(sF1,join(join(X0,sF0),sF0))),
inference(forward_demodulation,[],[f25405,f15468]) ).
fof(f25413,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,join(sF0,meet(join(X0,sF0),sF1))),
inference(forward_demodulation,[],[f25409,f25]) ).
fof(f25417,plain,
! [X0] : join(sF0,meet(sF1,meet(X0,join(sF0,X0)))) = join(sF0,meet(join(X0,sF0),sF1)),
inference(forward_demodulation,[],[f25413,f9463]) ).
fof(f25421,plain,
! [X0] : join(sF0,meet(sF1,join(X0,sF0))) = join(sF0,meet(sF1,meet(X0,join(sF0,X0)))),
inference(forward_demodulation,[],[f25417,f15468]) ).
fof(f25425,plain,
! [X0] : join(sF0,meet(sF1,join(X0,sF0))) = join(sF0,meet(sF1,join(X0,meet(sF0,X0)))),
inference(forward_demodulation,[],[f25421,f14903]) ).
fof(f25426,plain,
! [X0] : join(sF0,meet(sF1,join(X0,sF0))) = join(sF0,meet(sF1,X0)),
inference(forward_demodulation,[],[f25425,f15587]) ).
fof(f25427,plain,
! [X0] : join(sF0,join(sF0,meet(X0,sF1))) = join(sF0,meet(sF1,X0)),
inference(forward_demodulation,[],[f25426,f25]) ).
fof(f25428,plain,
! [X0] : join(sF0,meet(X0,sF1)) = join(sF0,meet(sF1,X0)),
inference(forward_demodulation,[],[f25427,f9463]) ).
fof(f27196,plain,
! [X2,X0,X1] : meet(X0,join(X2,X1)) = join(meet(X0,X1),meet(X2,X0)),
inference(superposition,[],[f2,f15468]) ).
fof(f27227,plain,
! [X2,X0,X1] : join(X0,meet(join(X0,X1),X2)) = join(X0,meet(X2,join(X0,meet(join(X0,X1),X2)))),
inference(superposition,[],[f78,f15468]) ).
fof(f27322,plain,
! [X2,X0,X1] : join(X1,meet(X0,join(X1,X2))) = meet(join(X0,X1),join(X1,X2)),
inference(superposition,[],[f17,f15468]) ).
fof(f27521,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,join(X0,X1)))) = join(X0,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f27227,f59]) ).
fof(f27712,plain,
! [X2,X0,X1] : join(X0,meet(X2,join(X0,X1))) = join(X0,meet(join(X0,X1),X2)),
inference(forward_demodulation,[],[f27521,f9463]) ).
fof(f29811,plain,
b = meet(b,sF3),
inference(superposition,[],[f15566,f12095]) ).
fof(f29861,plain,
meet(join(sF2,sF0),join(sF1,b)) = join(b,join(sF0,meet(sF2,sF1))),
inference(superposition,[],[f193,f15566]) ).
fof(f29885,plain,
meet(join(sF2,sF0),join(sF1,b)) = join(b,join(sF0,meet(sF1,sF2))),
inference(forward_demodulation,[],[f29861,f25428]) ).
fof(f29926,plain,
meet(join(sF1,b),join(sF2,sF0)) = join(b,join(sF0,meet(sF1,sF2))),
inference(forward_demodulation,[],[f29885,f15468]) ).
fof(f29954,plain,
join(sF0,meet(sF2,join(sF1,b))) = join(b,join(sF0,meet(sF1,sF2))),
inference(forward_demodulation,[],[f29926,f5377]) ).
fof(f29971,plain,
join(sF0,join(b,meet(sF1,sF2))) = join(b,join(sF0,meet(sF1,sF2))),
inference(forward_demodulation,[],[f29954,f27]) ).
fof(f30070,plain,
! [X0] : meet(join(sF0,sF0),join(X0,sF1)) = join(join(sF0,sF0),meet(X0,join(sF0,sF0))),
inference(superposition,[],[f1233,f464]) ).
fof(f30146,plain,
! [X0,X1] : join(X1,join(X0,X0)) = join(X1,join(join(join(X0,X0),meet(X1,join(X0,X0))),X1)),
inference(superposition,[],[f80,f1233]) ).
fof(f30160,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = meet(join(join(join(X0,X0),meet(X1,join(X0,X0))),X1),join(X1,join(X0,X0))),
inference(superposition,[],[f104,f1233]) ).
fof(f30332,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = meet(join(X1,join(X0,X0)),join(join(join(X0,X0),meet(X1,join(X0,X0))),X1)),
inference(forward_demodulation,[],[f30160,f15468]) ).
fof(f30344,plain,
! [X0,X1] : join(X1,join(X0,X0)) = join(X1,join(join(X0,X0),X1)),
inference(forward_demodulation,[],[f30146,f15587]) ).
fof(f30407,plain,
! [X0] : join(sF0,sF0) = meet(join(sF0,sF0),join(X0,sF1)),
inference(forward_demodulation,[],[f30070,f15587]) ).
fof(f30539,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = join(X1,meet(join(join(X0,X0),meet(X1,join(X0,X0))),join(X1,join(X0,X0)))),
inference(forward_demodulation,[],[f30332,f17]) ).
fof(f30550,plain,
! [X0,X1] : join(X1,X0) = join(X1,join(X0,X1)),
inference(forward_demodulation,[],[f30344,f15170]) ).
fof(f30606,plain,
! [X0] : sF0 = meet(sF0,join(X0,sF1)),
inference(forward_demodulation,[],[f30407,f4421]) ).
fof(f30696,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = join(X1,meet(join(X1,join(X0,X0)),join(join(X0,X0),meet(X1,join(X0,X0))))),
inference(forward_demodulation,[],[f30539,f27712]) ).
fof(f30815,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = join(X1,join(join(X0,X0),meet(X1,join(join(X0,X0),meet(X1,join(X0,X0)))))),
inference(forward_demodulation,[],[f30696,f27322]) ).
fof(f30884,plain,
! [X0,X1] : join(join(join(X0,X0),meet(X1,join(X0,X0))),X1) = join(X1,join(join(X0,X0),meet(X1,join(X0,X0)))),
inference(forward_demodulation,[],[f30815,f15302]) ).
fof(f30928,plain,
! [X0,X1] : join(join(X0,X0),X1) = join(X1,join(X0,X0)),
inference(forward_demodulation,[],[f30884,f15587]) ).
fof(f30947,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(forward_demodulation,[],[f30928,f15170]) ).
fof(f32596,plain,
meet(sF3,sF0) = join(b,a),
inference(superposition,[],[f133,f29811]) ).
fof(f32656,plain,
sF0 = meet(sF3,sF0),
inference(forward_demodulation,[],[f32596,f18915]) ).
fof(f32672,plain,
sF0 = meet(sF0,sF3),
inference(forward_demodulation,[],[f32656,f15468]) ).
fof(f33905,plain,
sF3 = join(sF0,sF3),
inference(superposition,[],[f15122,f32672]) ).
fof(f34380,plain,
sF0 = meet(sF0,meet(sF3,sF1)),
inference(superposition,[],[f5014,f33905]) ).
fof(f34447,plain,
sF0 = meet(sF0,meet(sF1,sF3)),
inference(forward_demodulation,[],[f34380,f15468]) ).
fof(f35012,plain,
! [X0,X1] : meet(join(X0,sF1),join(sF0,X1)) = join(meet(X1,join(X0,sF1)),sF0),
inference(superposition,[],[f2,f30606]) ).
fof(f35036,plain,
! [X0,X1] : meet(join(X0,sF1),join(sF0,X1)) = join(sF0,meet(X1,join(X0,sF1))),
inference(forward_demodulation,[],[f35012,f30947]) ).
fof(f42102,plain,
! [X0] : a = meet(a,join(X0,sF0)),
inference(superposition,[],[f15571,f30947]) ).
fof(f42955,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = join(meet(X1,join(X2,X0)),meet(X0,X1)),
inference(superposition,[],[f15587,f21]) ).
fof(f43395,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,join(X2,X0))),
inference(forward_demodulation,[],[f42955,f27196]) ).
fof(f43516,plain,
! [X2,X0,X1] : meet(X1,join(X2,X0)) = meet(X1,join(X0,X2)),
inference(forward_demodulation,[],[f43395,f30550]) ).
fof(f57678,plain,
join(sF2,a) = meet(join(sF2,sF0),sF3),
inference(superposition,[],[f68,f42102]) ).
fof(f57798,plain,
join(sF2,a) = meet(sF3,join(sF2,sF0)),
inference(forward_demodulation,[],[f57678,f15468]) ).
fof(f57841,plain,
join(sF2,a) = meet(sF3,join(sF0,sF2)),
inference(forward_demodulation,[],[f57798,f43516]) ).
fof(f57868,plain,
join(sF2,a) = join(sF2,meet(sF0,sF3)),
inference(forward_demodulation,[],[f57841,f12096]) ).
fof(f57888,plain,
join(sF2,a) = join(sF2,sF0),
inference(forward_demodulation,[],[f57868,f32672]) ).
fof(f57902,plain,
join(sF2,a) = join(sF0,sF2),
inference(forward_demodulation,[],[f57888,f30947]) ).
fof(f57913,plain,
sF3 = join(sF0,sF2),
inference(forward_demodulation,[],[f57902,f11957]) ).
fof(f59922,plain,
meet(sF1,sF3) = join(meet(sF2,sF1),sF0),
inference(superposition,[],[f24,f57913]) ).
fof(f60031,plain,
join(sF0,meet(sF2,sF1)) = meet(sF1,sF3),
inference(forward_demodulation,[],[f59922,f8705]) ).
fof(f60058,plain,
meet(sF1,sF3) = join(sF0,meet(sF1,sF2)),
inference(forward_demodulation,[],[f60031,f25428]) ).
fof(f60880,plain,
b = meet(b,sF1),
inference(superposition,[],[f19402,f464]) ).
fof(f60905,plain,
! [X0] : meet(join(sF0,X0),join(sF1,b)) = join(b,join(meet(X0,sF1),sF0)),
inference(superposition,[],[f175,f19402]) ).
fof(f60966,plain,
! [X0] : join(sF0,X0) = join(b,join(sF0,X0)),
inference(superposition,[],[f15122,f19402]) ).
fof(f61016,plain,
! [X0] : meet(join(sF0,X0),join(sF1,b)) = join(b,join(sF0,meet(X0,sF1))),
inference(forward_demodulation,[],[f60905,f8705]) ).
fof(f61064,plain,
! [X0] : join(sF0,meet(X0,sF1)) = meet(join(sF0,X0),join(sF1,b)),
inference(forward_demodulation,[],[f61016,f60966]) ).
fof(f61096,plain,
! [X0] : join(sF0,meet(X0,sF1)) = meet(join(sF0,X0),join(b,sF1)),
inference(forward_demodulation,[],[f61064,f43516]) ).
fof(f61118,plain,
! [X0] : join(sF0,meet(X0,sF1)) = meet(join(b,sF1),join(sF0,X0)),
inference(forward_demodulation,[],[f61096,f15468]) ).
fof(f61134,plain,
! [X0] : join(sF0,meet(X0,sF1)) = join(sF0,meet(X0,join(b,sF1))),
inference(forward_demodulation,[],[f61118,f35036]) ).
fof(f63148,plain,
sF1 = join(b,sF1),
inference(superposition,[],[f15122,f60880]) ).
fof(f64107,plain,
meet(sF1,sF2) = join(meet(c,sF1),b),
inference(superposition,[],[f99,f63148]) ).
fof(f64234,plain,
meet(sF1,sF2) = join(b,meet(c,sF1)),
inference(forward_demodulation,[],[f64107,f30947]) ).
fof(f64281,plain,
join(b,c) = meet(sF1,sF2),
inference(forward_demodulation,[],[f64234,f16561]) ).
fof(f64317,plain,
sF2 = meet(sF1,sF2),
inference(forward_demodulation,[],[f64281,f9]) ).
fof(f68529,plain,
meet(join(sF2,a),join(sF3,c)) = join(c,join(a,meet(sF2,sF3))),
inference(superposition,[],[f158,f21647]) ).
fof(f68581,plain,
join(c,sF3) = meet(join(sF2,a),join(sF3,c)),
inference(forward_demodulation,[],[f68529,f1025]) ).
fof(f68635,plain,
join(c,sF3) = meet(join(sF2,a),join(c,sF3)),
inference(forward_demodulation,[],[f68581,f43516]) ).
fof(f68677,plain,
join(c,sF3) = meet(join(c,sF3),join(sF2,a)),
inference(forward_demodulation,[],[f68635,f15468]) ).
fof(f68699,plain,
join(c,sF3) = meet(join(c,sF3),join(a,sF2)),
inference(forward_demodulation,[],[f68677,f43516]) ).
fof(f68714,plain,
join(c,sF3) = meet(join(a,sF2),join(c,sF3)),
inference(forward_demodulation,[],[f68699,f15468]) ).
fof(f68725,plain,
join(c,sF3) = meet(sF3,join(c,sF3)),
inference(forward_demodulation,[],[f68714,f11]) ).
fof(f68735,plain,
join(c,sF3) = join(sF3,meet(c,sF3)),
inference(forward_demodulation,[],[f68725,f14903]) ).
fof(f68743,plain,
sF3 = join(c,sF3),
inference(forward_demodulation,[],[f68735,f13832]) ).
fof(f70061,plain,
meet(sF3,sF1) = join(c,meet(sF0,meet(sF3,sF1))),
inference(superposition,[],[f378,f68743]) ).
fof(f70154,plain,
meet(sF1,sF3) = join(c,meet(sF0,meet(sF1,sF3))),
inference(forward_demodulation,[],[f70061,f15468]) ).
fof(f70199,plain,
join(c,sF0) = meet(sF1,sF3),
inference(forward_demodulation,[],[f70154,f34447]) ).
fof(f70235,plain,
sF1 = meet(sF1,sF3),
inference(forward_demodulation,[],[f70199,f16248]) ).
fof(f70364,plain,
meet(join(sF1,b),join(join(b,sF0),sF2)) = join(join(b,meet(sF1,sF2)),join(b,join(sF0,meet(b,sF1)))),
inference(superposition,[],[f1117,f27]) ).
fof(f70513,plain,
meet(join(sF1,b),join(join(b,sF0),sF2)) = join(join(b,meet(sF1,sF2)),join(sF0,meet(b,sF1))),
inference(forward_demodulation,[],[f70364,f60966]) ).
fof(f70612,plain,
join(join(b,meet(sF1,sF2)),sF0) = meet(join(sF1,b),join(join(b,sF0),sF2)),
inference(forward_demodulation,[],[f70513,f16939]) ).
fof(f70694,plain,
join(join(b,meet(sF1,sF2)),sF0) = meet(join(sF1,b),join(sF2,join(b,sF0))),
inference(forward_demodulation,[],[f70612,f43516]) ).
fof(f70765,plain,
meet(join(sF1,b),join(sF2,sF0)) = join(join(b,meet(sF1,sF2)),sF0),
inference(forward_demodulation,[],[f70694,f18935]) ).
fof(f70829,plain,
meet(join(sF1,b),join(sF2,sF0)) = join(sF0,join(b,meet(sF1,sF2))),
inference(forward_demodulation,[],[f70765,f30947]) ).
fof(f70879,plain,
meet(join(sF1,b),join(sF2,sF0)) = join(b,join(sF0,meet(sF1,sF2))),
inference(forward_demodulation,[],[f70829,f29971]) ).
fof(f70924,plain,
meet(join(sF1,b),join(sF2,sF0)) = join(sF0,meet(sF1,sF2)),
inference(forward_demodulation,[],[f70879,f60966]) ).
fof(f70956,plain,
meet(sF1,sF3) = meet(join(sF1,b),join(sF2,sF0)),
inference(forward_demodulation,[],[f70924,f60058]) ).
fof(f70978,plain,
meet(sF1,sF3) = meet(join(sF1,b),join(sF0,sF2)),
inference(forward_demodulation,[],[f70956,f43516]) ).
fof(f70996,plain,
meet(sF1,sF3) = meet(join(sF0,sF2),join(sF1,b)),
inference(forward_demodulation,[],[f70978,f15468]) ).
fof(f71012,plain,
meet(sF1,sF3) = meet(join(sF0,sF2),join(b,sF1)),
inference(forward_demodulation,[],[f70996,f43516]) ).
fof(f71025,plain,
meet(sF1,sF3) = meet(join(b,sF1),join(sF0,sF2)),
inference(forward_demodulation,[],[f71012,f15468]) ).
fof(f71035,plain,
meet(sF1,sF3) = join(sF0,meet(sF2,join(b,sF1))),
inference(forward_demodulation,[],[f71025,f35036]) ).
fof(f71045,plain,
join(sF0,meet(sF2,sF1)) = meet(sF1,sF3),
inference(forward_demodulation,[],[f71035,f61134]) ).
fof(f71053,plain,
sF1 = join(sF0,meet(sF2,sF1)),
inference(forward_demodulation,[],[f71045,f70235]) ).
fof(f71060,plain,
sF1 = join(sF0,meet(sF1,sF2)),
inference(forward_demodulation,[],[f71053,f25428]) ).
fof(f71066,plain,
sF1 = join(sF0,sF2),
inference(forward_demodulation,[],[f71060,f64317]) ).
fof(f71074,plain,
sF1 = sF3,
inference(superposition,[],[f57913,f71066]) ).
fof(f71182,plain,
$false,
inference(forward_subsumption_resolution,[],[f71074,f12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT007-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n017.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 13:51:20 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.47/2.68 % (2564903)Will run a generic schedule for satisfiability detection.
% 15.47/2.68 % (2564912)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4073030703:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.47/2.68 % (2564909)% WARNING: option uhcvi not known.
% 15.47/2.68 % (2564908)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1661792499_2999 on theBenchmark for (2999ds/0Mi)
% 15.47/2.68 % (2564909)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3014377434:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.47/2.68 % (2564910)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4086185868:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.47/2.68 % (2564911)dis+10_1_sil=32000:sp=arity:random_seed=359846905:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.47/2.68 % (2564914)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3382644055:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.47/2.68 % (2564913)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3129031080:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.47/2.68 % TRYING [1]
% 15.47/2.68 % TRYING [2]
% 15.47/2.68 % TRYING [3]
% 15.47/2.68 % TRYING [4]
% 15.47/2.68 % TRYING [5]
% 15.47/2.68 % (2564912)Instruction limit reached!
% 15.47/2.68 % (2564912)------------------------------
% 15.47/2.68 % (2564912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.68 % (2564912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.68 % (2564912)CaDiCaL version: 2.1.3
% 15.47/2.68 % (2564912)Termination reason: Instruction limit
% 15.47/2.68 % (2564912)Termination phase: Saturation
% 15.47/2.68 % (2564912)Time elapsed: 0.041 s
% 15.47/2.68 % (2564912)Peak memory usage: 12 MB
% 15.47/2.68 % (2564912)Instructions burned: 119 (million)
% 15.47/2.68 % (2564922)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3177297152:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.47/2.68 % TRYING [1]
% 15.47/2.68 % TRYING [2]
% 15.47/2.68 % TRYING [3]
% 15.47/2.68 % TRYING [4]
% 15.47/2.68 % (2564911)Instruction limit reached!
% 15.47/2.68 % (2564911)------------------------------
% 15.47/2.68 % (2564911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.68 % (2564911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.68 % (2564911)CaDiCaL version: 2.1.3
% 15.47/2.68 % (2564911)Termination reason: Instruction limit
% 15.47/2.68 % (2564911)Termination phase: Saturation
% 15.47/2.68 % (2564911)Time elapsed: 0.059 s
% 15.47/2.68 % (2564911)Peak memory usage: 12 MB
% 15.47/2.68 % (2564911)Instructions burned: 103 (million)
% 15.47/2.68 % TRYING [5]
% 15.47/2.68 % (2564924)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=665557036:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.47/2.68 % TRYING [6]
% 15.47/2.68 % (2564913)Instruction limit reached!
% 15.47/2.68 % (2564913)------------------------------
% 15.47/2.68 % (2564913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.68 % (2564913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.68 % (2564913)CaDiCaL version: 2.1.3
% 15.47/2.68 % (2564913)Termination reason: Instruction limit
% 15.47/2.68 % (2564913)Termination phase: Saturation
% 15.47/2.68 % (2564913)Time elapsed: 0.081 s
% 15.47/2.68 % (2564913)Peak memory usage: 13 MB
% 15.47/2.68 % (2564913)Instructions burned: 131 (million)
% 15.47/2.68 % (2564914)Instruction limit reached!
% 15.47/2.68 % (2564914)------------------------------
% 15.47/2.68 % (2564914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.47/2.68 % (2564914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.47/2.68 % (2564914)CaDiCaL version: 2.1.3
% 15.47/2.68 % (2564914)Termination reason: Instruction limit
% 15.47/2.68 % (2564914)Termination phase: Saturation
% 15.47/2.68 % (2564914)Time elapsed: 0.098 s
% 15.47/2.68 % (2564914)Peak memory usage: 12 MB
% 15.47/2.68 % (2564914)Instructions burned: 160 (million)
% 15.47/2.68 % (2564926)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1360836575:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.47/2.68 % TRYING [6]
% 15.47/2.68 % (2564927)ott-21_1_sil=16000:fs=off:random_seed=2486696983:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.47/2.68 % (2564924)Instruction limit reached!
% 15.47/2.68 % (2564924)------------------------------
% 15.47/2.68 % (2564924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564924)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564924)Termination reason: Instruction limit
% 45.24/6.90 % (2564924)Termination phase: Saturation
% 45.24/6.90 % (2564924)Time elapsed: 0.086 s
% 45.24/6.90 % (2564924)Peak memory usage: 12 MB
% 45.24/6.90 % (2564924)Instructions burned: 131 (million)
% 45.24/6.90 % (2564930)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=38070649:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 45.24/6.90 % (2564927)Instruction limit reached!
% 45.24/6.90 % (2564927)------------------------------
% 45.24/6.90 % (2564927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564927)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564927)Termination reason: Instruction limit
% 45.24/6.90 % (2564927)Termination phase: Saturation
% 45.24/6.90 % (2564927)Time elapsed: 0.088 s
% 45.24/6.90 % (2564927)Peak memory usage: 12 MB
% 45.24/6.90 % (2564927)Instructions burned: 181 (million)
% 45.24/6.90 % (2564932)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3645767373:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 45.24/6.90 % TRYING [1]
% 45.24/6.90 % TRYING [2]
% 45.24/6.90 % TRYING [3]
% 45.24/6.90 % TRYING [4]
% 45.24/6.90 % TRYING [5]
% 45.24/6.90 % (2564922)Instruction limit reached!
% 45.24/6.90 % (2564922)------------------------------
% 45.24/6.90 % (2564922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564922)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564922)Termination reason: Instruction limit
% 45.24/6.90 % (2564922)Termination phase: Finite model building SAT solving
% 45.24/6.90 % (2564922)Time elapsed: 0.220 s
% 45.24/6.90 % (2564922)Peak memory usage: 19 MB
% 45.24/6.90 % (2564922)Instructions burned: 715 (million)
% 45.24/6.90 % (2564934)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1016116661:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 45.24/6.90 % TRYING [7]
% 45.24/6.90 % TRYING [6]
% 45.24/6.90 % (2564930)Instruction limit reached!
% 45.24/6.90 % (2564930)------------------------------
% 45.24/6.90 % (2564930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564930)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564930)Termination reason: Instruction limit
% 45.24/6.90 % (2564930)Termination phase: Saturation
% 45.24/6.90 % (2564930)Time elapsed: 0.262 s
% 45.24/6.90 % (2564930)Peak memory usage: 15 MB
% 45.24/6.90 % (2564930)Instructions burned: 478 (million)
% 45.24/6.90 % (2564926)Instruction limit reached!
% 45.24/6.90 % (2564926)------------------------------
% 45.24/6.90 % (2564926)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564926)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564926)Termination reason: Instruction limit
% 45.24/6.90 % (2564926)Termination phase: Saturation
% 45.24/6.90 % (2564926)Time elapsed: 0.364 s
% 45.24/6.90 % (2564926)Peak memory usage: 18 MB
% 45.24/6.90 % (2564926)Instructions burned: 685 (million)
% 45.24/6.90 % (2564936)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1794674709:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 45.24/6.90 % (2564937)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2737897692:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 45.24/6.90 % TRYING [14]
% 45.24/6.90 % TRYING [7]
% 45.24/6.90 % (2564932)Instruction limit reached!
% 45.24/6.90 % (2564932)------------------------------
% 45.24/6.90 % (2564932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564932)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564932)Termination reason: Instruction limit
% 45.24/6.90 % (2564932)Termination phase: Finite model building SAT solving
% 45.24/6.90 % (2564932)Time elapsed: 0.378 s
% 45.24/6.90 % (2564932)Peak memory usage: 18 MB
% 45.24/6.90 % (2564932)Instructions burned: 866 (million)
% 45.24/6.90 % (2564940)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=467349601:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 45.24/6.90 % (2564934)Instruction limit reached!
% 45.24/6.90 % (2564934)------------------------------
% 45.24/6.90 % (2564934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564934)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564934)Termination reason: Instruction limit
% 45.24/6.90 % (2564934)Termination phase: Saturation
% 45.24/6.90 % (2564934)Time elapsed: 0.398 s
% 45.24/6.90 % (2564934)Peak memory usage: 29 MB
% 45.24/6.90 % (2564934)Instructions burned: 1179 (million)
% 45.24/6.90 % (2564942)fmb+10_1_sil=64000:random_seed=3751779879:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 45.24/6.90 % TRYING [1]
% 45.24/6.90 % TRYING [2]
% 45.24/6.90 % TRYING [3]
% 45.24/6.90 % TRYING [4]
% 45.24/6.90 % TRYING [5]
% 45.24/6.90 % TRYING [6]
% 45.24/6.90 % (2564936)Instruction limit reached!
% 45.24/6.90 % (2564936)------------------------------
% 45.24/6.90 % (2564936)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564936)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564936)Termination reason: Instruction limit
% 45.24/6.90 % (2564936)Termination phase: Finite model building constraint generation
% 45.24/6.90 % (2564936)Time elapsed: 0.317 s
% 45.24/6.90 % (2564936)Peak memory usage: 75 MB
% 45.24/6.90 % (2564936)Instructions burned: 890 (million)
% 45.24/6.90 % (2564944)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2347242405:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 45.24/6.90 % TRYING [20]
% 45.24/6.90 % TRYING [7]
% 45.24/6.90 % (2564937)Instruction limit reached!
% 45.24/6.90 % (2564937)------------------------------
% 45.24/6.90 % (2564937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564937)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564937)Termination reason: Instruction limit
% 45.24/6.90 % (2564937)Termination phase: Saturation
% 45.24/6.90 % (2564937)Time elapsed: 0.404 s
% 45.24/6.90 % (2564937)Peak memory usage: 17 MB
% 45.24/6.90 % (2564937)Instructions burned: 693 (million)
% 45.24/6.90 % (2564946)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1777417867:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 45.24/6.90 % TRYING [8]
% 45.24/6.90 % TRYING [8]
% 45.24/6.90 % (2564940)Instruction limit reached!
% 45.24/6.90 % (2564940)------------------------------
% 45.24/6.90 % (2564940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564940)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564940)Termination reason: Instruction limit
% 45.24/6.90 % (2564940)Termination phase: Saturation
% 45.24/6.90 % (2564940)Time elapsed: 0.458 s
% 45.24/6.90 % (2564940)Peak memory usage: 17 MB
% 45.24/6.90 % (2564940)Instructions burned: 881 (million)
% 45.24/6.90 % (2564948)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3327898648:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 45.24/6.90 % TRYING [8]
% 45.24/6.90 % (2564946)Instruction limit reached!
% 45.24/6.90 % (2564946)------------------------------
% 45.24/6.90 % (2564946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564946)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564946)Termination reason: Instruction limit
% 45.24/6.90 % (2564946)Termination phase: Finite model building SAT solving
% 45.24/6.90 % (2564946)Time elapsed: 0.517 s
% 45.24/6.90 % (2564946)Peak memory usage: 40 MB
% 45.24/6.90 % (2564946)Instructions burned: 921 (million)
% 45.24/6.90 % (2564950)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2680764862:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 45.24/6.90 % TRYING [9]
% 45.24/6.90 % (2564950)Instruction limit reached!
% 45.24/6.90 % (2564950)------------------------------
% 45.24/6.90 % (2564950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564950)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564950)Termination reason: Instruction limit
% 45.24/6.90 % (2564950)Termination phase: Saturation
% 45.24/6.90 % (2564950)Time elapsed: 0.754 s
% 45.24/6.90 % (2564950)Peak memory usage: 26 MB
% 45.24/6.90 % (2564950)Instructions burned: 1473 (million)
% 45.24/6.90 % (2564952)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2316386025:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 45.24/6.90 % TRYING [77]
% 45.24/6.90 % TRYING [9]
% 45.24/6.90 % (2564948)Instruction limit reached!
% 45.24/6.90 % (2564948)------------------------------
% 45.24/6.90 % (2564948)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564948)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564948)Termination reason: Instruction limit
% 45.24/6.90 % (2564948)Termination phase: Saturation
% 45.24/6.90 % (2564948)Time elapsed: 2.812 s
% 45.24/6.90 % (2564948)Peak memory usage: 56 MB
% 45.24/6.90 % (2564948)Instructions burned: 5132 (million)
% 45.24/6.90 % (2564954)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1977256688:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 45.24/6.90 % TRYING [16]
% 45.24/6.90 % TRYING [10]
% 45.24/6.90 % (2564944)Instruction limit reached!
% 45.24/6.90 % (2564944)------------------------------
% 45.24/6.90 % (2564944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564944)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564944)Termination reason: Instruction limit
% 45.24/6.90 % (2564944)Termination phase: Finite model building constraint generation
% 45.24/6.90 % (2564944)Time elapsed: 3.716 s
% 45.24/6.90 % (2564944)Peak memory usage: 704 MB
% 45.24/6.90 % (2564944)Instructions burned: 9515 (million)
% 45.24/6.90 % (2564952)Instruction limit reached!
% 45.24/6.90 % (2564952)------------------------------
% 45.24/6.90 % (2564952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564952)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564952)Termination reason: Instruction limit
% 45.24/6.90 % (2564952)Termination phase: Finite model building constraint generation
% 45.24/6.90 % (2564952)Time elapsed: 2.320 s
% 45.24/6.90 % (2564952)Peak memory usage: 424 MB
% 45.24/6.90 % (2564952)Instructions burned: 6324 (million)
% 45.24/6.90 % (2564956)ott-2_1_sil=16000:newcnf=on:random_seed=3328281338:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2953 on theBenchmark for (2953ds/869Mi)
% 45.24/6.90 % (2564957)ott+10_1_sil=32000:tgt=ground:random_seed=2277776606:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 45.24/6.90 % (2564954)Instruction limit reached!
% 45.24/6.90 % (2564954)------------------------------
% 45.24/6.90 % (2564954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564954)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564954)Termination reason: Instruction limit
% 45.24/6.90 % (2564954)Termination phase: Finite model building constraint generation
% 45.24/6.90 % (2564954)Time elapsed: 0.731 s
% 45.24/6.90 % (2564954)Peak memory usage: 132 MB
% 45.24/6.90 % (2564954)Instructions burned: 2175 (million)
% 45.24/6.90 % (2564960)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2700222491:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 45.24/6.90 % TRYING [1]
% 45.24/6.90 % TRYING [2]
% 45.24/6.90 % TRYING [3]
% 45.24/6.90 % TRYING [4]
% 45.24/6.90 % TRYING [5]
% 45.24/6.90 % TRYING [6]
% 45.24/6.90 % TRYING [7]
% 45.24/6.90 % (2564956)Instruction limit reached!
% 45.24/6.90 % (2564956)------------------------------
% 45.24/6.90 % (2564956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.24/6.90 % (2564956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.24/6.90 % (2564956)CaDiCaL version: 2.1.3
% 45.24/6.90 % (2564956)Termination reason: Instruction limit
% 45.24/6.90 % (2564956)Termination phase: Saturation
% 45.24/6.90 % (2564956)Time elapsed: 0.546 s
% 45.24/6.90 % (2564956)Peak memory usage: 19 MB
% 45.24/6.90 % (2564956)Instructions burned: 869 (million)
% 45.24/6.90 % (2564962)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3359733078:i=3512:aac=none_2947 on theBenchmark for (2947ds/3512Mi)
% 45.24/6.90 % TRYING [8]
% 45.24/6.90 % TRYING [11]
% 45.24/6.90 % (2564957) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2564903-2564957"...
% 45.24/6.90 % (2564957)...printing done.
% 45.24/6.90 % (2564957)Refutation found. Thanks to Tanya!
% 45.24/6.90 % SZS status Unsatisfiable for theBenchmark
% 45.24/6.90 % SZS output start Proof for theBenchmark
% See solution above
% 45.97/6.90 % (2564957)------------------------------
% 45.97/6.90 % (2564957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.97/6.90 % (2564957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.97/6.91 % (2564957)CaDiCaL version: 2.1.3
% 45.97/6.91 % (2564957)Termination reason: Refutation
% 45.97/6.91 % (2564957)Time elapsed: 1.778 s
% 45.97/6.91 % (2564957)Peak memory usage: 43 MB
% 45.97/6.91 % (2564957)Instructions burned: 2805 (million)
% 45.97/6.91 % (2564903)Success in time 6.475 s
% 45.97/6.91 % Vampire exiting
%------------------------------------------------------------------------------