%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT400-4 : 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 : n007.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 120.23s 34.84s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 20
% Syntax : Number of formulae : 241 ( 159 unt; 7 def)
% Number of atoms : 337 ( 216 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 188 ( 92 ~; 89 |; 0 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 8 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 434 ( 0 sgn 434 !; 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(f8,axiom,
! [X2,X0,X1] : lome(X0,X1,X2) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_of_lome) ).
fof(f11,axiom,
! [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',rh1) ).
fof(f12,axiom,
! [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',rh2) ).
fof(f13,axiom,
! [X2,X0,X1] : lome(X0,X1,X2) = upme(X0,upme(X1,X0,X2),upme(X2,X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rl1) ).
fof(f14,negated_conjecture,
upme(a,x2,y2) = upme(a,x2,z2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(f15,negated_conjecture,
upme(x2,y2,z2) != lome(x2,y2,z2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture_1) ).
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,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,X2)),meet(X2,join(X0,X1)))),
inference(definition_unfolding,[],[f13,f8,f7,f7,f7]) ).
fof(f19,plain,
meet(a,join(x2,y2)) = meet(a,join(x2,z2)),
inference(definition_unfolding,[],[f14,f7,f7]) ).
fof(f20,plain,
meet(x2,join(y2,z2)) != join(meet(x2,y2),meet(x2,z2)),
inference(definition_unfolding,[],[f15,f7,f8]) ).
fof(f22,definition,
( spl0_1
<=> meet(x2,join(y2,z2)) = join(meet(x2,y2),meet(x2,z2)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f24,plain,
( meet(x2,join(y2,z2)) != join(meet(x2,y2),meet(x2,z2))
| spl0_1 ),
inference(avatar_component_clause,[],[f22]) ).
fof(f25,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f20,f22]) ).
fof(f27,definition,
( spl0_2
<=> meet(a,join(x2,y2)) = meet(a,join(x2,z2)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f29,plain,
( meet(a,join(x2,y2)) = meet(a,join(x2,z2))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f27]) ).
fof(f30,plain,
spl0_2,
inference(avatar_split_clause,[],[f19,f27]) ).
fof(f31,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f5,f6]) ).
fof(f32,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f6,f5]) ).
fof(f40,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = join(meet(X0,join(X1,meet(a,X0))),X0),
inference(superposition,[],[f17,f6]) ).
fof(f43,plain,
! [X0,X1] : join(X0,meet(X0,join(X1,meet(a,X0)))) = meet(X0,join(X1,X0)),
inference(forward_demodulation,[],[f40,f3]) ).
fof(f52,plain,
! [X0,X1] : meet(X0,join(X1,X0)) = X0,
inference(forward_demodulation,[],[f43,f5]) ).
fof(f137,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(f138,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X1,join(X0,X2)),meet(join(X0,X1),X2))),
inference(superposition,[],[f18,f1]) ).
fof(f139,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X0,X2)))),
inference(superposition,[],[f18,f1]) ).
fof(f140,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f5,f1]) ).
fof(f143,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,join(X0,X2)),meet(join(X0,X1),X2))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f139,f3]) ).
fof(f165,plain,
( ! [X0,X1] : meet(X0,join(X1,join(x2,z2))) = join(meet(X0,join(X1,meet(a,join(x2,y2)))),meet(X0,join(join(x2,z2),meet(a,X1))))
| ~ spl0_2 ),
inference(superposition,[],[f17,f29]) ).
fof(f173,plain,
( ! [X0,X1] : meet(X0,join(X1,join(x2,z2))) = join(meet(X0,join(X1,meet(a,join(x2,y2)))),meet(X0,join(x2,join(z2,meet(a,X1)))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f165,f4]) ).
fof(f200,plain,
! [X2,X0,X1] : meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X1,X0)))) = join(meet(X1,X2),meet(X1,X0)),
inference(superposition,[],[f18,f3]) ).
fof(f201,plain,
! [X2,X0,X1] : join(meet(X1,X0),meet(X1,X2)) = meet(X1,join(meet(X0,join(X1,X2)),meet(X2,join(X0,X1)))),
inference(superposition,[],[f18,f3]) ).
fof(f204,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(f208,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f2,f6]) ).
fof(f219,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(f220,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(f222,plain,
! [X2,X3,X0,X1] : join(meet(X2,meet(X0,X1)),meet(X2,X3)) = meet(X2,join(meet(X0,meet(X1,join(X2,X3))),meet(X3,join(X2,meet(X0,X1))))),
inference(superposition,[],[f18,f2]) ).
fof(f226,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f229,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,[],[f220,f2]) ).
fof(f230,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,[],[f219,f3]) ).
fof(f235,plain,
! [X2,X3,X0,X1] : meet(X0,meet(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,[],[f229,f2]) ).
fof(f236,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,[],[f230,f2]) ).
fof(f239,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X3,X2)) = meet(X0,meet(X1,join(X2,X3))),
inference(forward_demodulation,[],[f236,f235]) ).
fof(f240,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X2,X3))) = meet(X0,meet(X1,join(X3,X2))),
inference(forward_demodulation,[],[f239,f2]) ).
fof(f268,plain,
! [X2,X0,X1] : join(X1,meet(X0,meet(X1,X2))) = X1,
inference(superposition,[],[f5,f226]) ).
fof(f299,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(superposition,[],[f208,f140]) ).
fof(f301,plain,
! [X2,X0,X1] : meet(X1,X2) = meet(X1,meet(join(X0,X1),X2)),
inference(superposition,[],[f208,f3]) ).
fof(f305,plain,
! [X2,X0,X1] : meet(X1,X0) = meet(X1,meet(X0,join(X1,X2))),
inference(superposition,[],[f208,f1]) ).
fof(f344,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f4,f5]) ).
fof(f346,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f4,f140]) ).
fof(f355,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f404,plain,
! [X2,X0,X1] : meet(X2,join(X0,join(X1,X2))) = X2,
inference(superposition,[],[f6,f355]) ).
fof(f434,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f344,f3]) ).
fof(f477,plain,
! [X0,X1] : meet(X1,X0) = meet(meet(X1,X0),X0),
inference(superposition,[],[f52,f140]) ).
fof(f480,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f52,f344]) ).
fof(f488,plain,
! [X0,X1] : join(X1,X0) = join(join(X1,X0),X0),
inference(superposition,[],[f140,f52]) ).
fof(f500,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f488,f3]) ).
fof(f505,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f480,f1]) ).
fof(f506,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,X0)),
inference(forward_demodulation,[],[f477,f1]) ).
fof(f612,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(meet(X0,X2),join(X0,X1)))) = join(meet(X0,meet(X0,X2)),meet(X0,X1)),
inference(superposition,[],[f200,f5]) ).
fof(f703,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(meet(X0,X2),join(X0,X1)))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f612,f299]) ).
fof(f732,plain,
! [X2,X0,X1] : meet(X0,join(meet(X1,X0),meet(X0,meet(X2,join(X0,X1))))) = join(meet(X0,X2),meet(X0,X1)),
inference(forward_demodulation,[],[f703,f2]) ).
fof(f754,plain,
! [X2,X0,X1] : join(meet(X0,X2),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(X0,X2))),
inference(forward_demodulation,[],[f732,f305]) ).
fof(f842,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(join(X0,X1),join(X0,X2)),
inference(superposition,[],[f346,f6]) ).
fof(f849,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f346,f3]) ).
fof(f892,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f842,f355]) ).
fof(f904,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,join(X0,X1))),
inference(forward_demodulation,[],[f892,f4]) ).
fof(f1134,plain,
! [X2,X3,X0,X1] : meet(X3,meet(X2,join(X1,X0))) = meet(X3,meet(join(X0,X1),X2)),
inference(superposition,[],[f240,f1]) ).
fof(f1163,plain,
! [X2,X3,X0,X1] : meet(X0,join(X3,X2)) = meet(X0,meet(join(X0,X1),join(X2,X3))),
inference(superposition,[],[f208,f240]) ).
fof(f1171,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,[],[f226,f240]) ).
fof(f1174,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,f240]) ).
fof(f1180,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,[],[f1174,f2]) ).
fof(f1181,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,[],[f1171,f2]) ).
fof(f1187,plain,
! [X2,X3,X0] : meet(X0,join(X2,X3)) = meet(X0,join(X3,X2)),
inference(forward_demodulation,[],[f1163,f208]) ).
fof(f1242,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,join(X1,X2))) = meet(X3,join(X2,join(X0,X1))),
inference(superposition,[],[f1187,f4]) ).
fof(f1296,plain,
! [X2,X0,X1] : meet(X0,join(X1,X2)) = meet(join(X2,X1),X0),
inference(superposition,[],[f1,f1187]) ).
fof(f1369,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X1,meet(X2,X0)),
inference(superposition,[],[f1134,f31]) ).
fof(f1422,plain,
! [X2,X0,X1] : meet(X0,X1) = meet(X0,meet(X1,join(X2,X0))),
inference(superposition,[],[f208,f1134]) ).
fof(f1426,plain,
! [X2,X3,X0,X1,X4] : meet(X0,meet(join(X1,X2),join(X3,X4))) = meet(X0,meet(join(X4,X3),join(X2,X1))),
inference(superposition,[],[f240,f1134]) ).
fof(f1591,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X2,X1),X0),
inference(superposition,[],[f1,f1369]) ).
fof(f1594,plain,
! [X2,X0,X1] : meet(X2,X1) = join(meet(X2,X1),meet(X0,meet(X1,X2))),
inference(superposition,[],[f140,f1369]) ).
fof(f1653,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(X0,X1),meet(X0,X2))),
inference(superposition,[],[f505,f5]) ).
fof(f1823,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X1,join(X0,meet(X1,X2))),join(X0,meet(X1,X2))),
inference(superposition,[],[f505,f500]) ).
fof(f1826,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(meet(X1,X2),X0),join(X1,join(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f1823,f1296]) ).
fof(f1851,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(meet(X1,X2),X0),join(X1,X0)),
inference(forward_demodulation,[],[f1826,f434]) ).
fof(f1869,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(forward_demodulation,[],[f1851,f1296]) ).
fof(f1891,plain,
! [X2,X3,X0,X1] : meet(X2,join(X3,meet(X1,X0))) = join(meet(join(X3,meet(a,meet(X0,X1))),X2),meet(X2,join(meet(X1,X0),meet(a,X3)))),
inference(superposition,[],[f137,f1369]) ).
fof(f1955,plain,
! [X0,X1] : meet(X1,join(X0,X0)) = join(meet(X0,X1),meet(X1,X0)),
inference(superposition,[],[f137,f140]) ).
fof(f2034,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X0,X1),meet(X1,X0)),
inference(forward_demodulation,[],[f1955,f31]) ).
fof(f2725,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(X0,X2)),
inference(superposition,[],[f301,f140]) ).
fof(f2826,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f2725,f226]) ).
fof(f2839,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f2826,f2]) ).
fof(f6106,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(meet(join(meet(a,X0),X1),join(X0,meet(a,X1))),join(meet(a,X0),X1)),
inference(superposition,[],[f204,f32]) ).
fof(f6186,plain,
! [X0,X1] : meet(join(meet(a,X0),X1),join(X0,X1)) = join(join(meet(a,X0),X1),meet(join(meet(a,X0),X1),join(X0,meet(a,X1)))),
inference(forward_demodulation,[],[f6106,f3]) ).
fof(f6280,plain,
! [X0,X1] : join(meet(a,X0),X1) = meet(join(meet(a,X0),X1),join(X0,X1)),
inference(forward_demodulation,[],[f6186,f5]) ).
fof(f6355,plain,
! [X0,X1] : join(meet(a,X0),X1) = meet(join(X1,X0),join(meet(a,X0),X1)),
inference(forward_demodulation,[],[f6280,f1296]) ).
fof(f6552,plain,
! [X0,X1] : join(meet(a,meet(X0,X1)),meet(X1,X0)) = meet(meet(X0,X1),join(meet(a,meet(X0,X1)),meet(X1,X0))),
inference(superposition,[],[f6355,f2034]) ).
fof(f6641,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(join(X1,X0),join(join(meet(a,X0),X1),X2)),
inference(superposition,[],[f344,f6355]) ).
fof(f6650,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(join(meet(a,X0),X1),X2))),
inference(forward_demodulation,[],[f6641,f4]) ).
fof(f6711,plain,
! [X0,X1] : join(meet(a,meet(X0,X1)),meet(X1,X0)) = meet(meet(X0,X1),join(meet(X1,X0),meet(a,meet(X0,X1)))),
inference(forward_demodulation,[],[f6552,f1187]) ).
fof(f6723,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(meet(a,X0),join(X1,X2)))),
inference(forward_demodulation,[],[f6650,f4]) ).
fof(f6774,plain,
! [X0,X1] : join(meet(a,meet(X0,X1)),meet(X1,X0)) = meet(X0,meet(X1,join(meet(X1,X0),meet(a,meet(X0,X1))))),
inference(forward_demodulation,[],[f6711,f2]) ).
fof(f6784,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X0,join(X1,X2))),
inference(forward_demodulation,[],[f6723,f346]) ).
fof(f6832,plain,
! [X0,X1] : meet(X0,meet(X1,meet(X1,X0))) = join(meet(a,meet(X0,X1)),meet(X1,X0)),
inference(forward_demodulation,[],[f6774,f1594]) ).
fof(f6838,plain,
! [X2,X0,X1] : join(join(X1,X0),X2) = join(X1,join(X2,X0)),
inference(forward_demodulation,[],[f6784,f904]) ).
fof(f6862,plain,
! [X0,X1] : meet(X0,meet(X1,meet(X1,X0))) = join(meet(X1,X0),meet(a,meet(X0,X1))),
inference(forward_demodulation,[],[f6832,f3]) ).
fof(f6882,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,meet(X1,X0))),
inference(forward_demodulation,[],[f6862,f1594]) ).
fof(f6889,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f6882,f2839]) ).
fof(f7142,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f4,f6838]) ).
fof(f7290,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X0,X1),meet(X1,X0))),
inference(superposition,[],[f7142,f2034]) ).
fof(f7456,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f7290,f2034]) ).
fof(f9438,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2))) = meet(X0,join(meet(X1,join(X0,meet(join(X0,X1),X2))),meet(join(X0,X1),X2))),
inference(superposition,[],[f138,f299]) ).
fof(f9460,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2))) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X0,meet(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f9438,f1187]) ).
fof(f9488,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X0,meet(join(X0,X1),X2))))),
inference(forward_demodulation,[],[f9460,f208]) ).
fof(f9621,plain,
! [X2,X0,X1] : join(meet(meet(a,X0),join(X1,join(X2,meet(a,X0)))),meet(X1,join(X2,meet(a,X0)))) = meet(join(meet(meet(a,X0),X1),join(X2,meet(a,X0))),join(meet(a,X0),X1)),
inference(superposition,[],[f16,f52]) ).
fof(f9798,plain,
! [X2,X0,X1] : join(meet(meet(a,X0),join(X1,join(X2,meet(a,X0)))),meet(X1,join(X2,meet(a,X0)))) = meet(join(X1,meet(a,X0)),join(meet(meet(a,X0),X1),join(X2,meet(a,X0)))),
inference(forward_demodulation,[],[f9621,f1296]) ).
fof(f9980,plain,
! [X2,X0,X1] : join(meet(meet(a,X0),join(X1,join(X2,meet(a,X0)))),meet(X1,join(X2,meet(a,X0)))) = meet(join(X1,meet(a,X0)),join(meet(a,X0),join(meet(meet(a,X0),X1),X2))),
inference(forward_demodulation,[],[f9798,f1242]) ).
fof(f10161,plain,
! [X2,X0,X1] : join(meet(meet(a,X0),join(X1,join(X2,meet(a,X0)))),meet(X1,join(X2,meet(a,X0)))) = meet(join(X1,meet(a,X0)),join(meet(a,X0),X2)),
inference(forward_demodulation,[],[f9980,f344]) ).
fof(f10331,plain,
! [X2,X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X0),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(meet(a,X0),join(X1,join(X2,meet(a,X0))))),
inference(forward_demodulation,[],[f10161,f3]) ).
fof(f10496,plain,
! [X2,X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X0),X2)) = join(meet(X1,join(X2,meet(a,X0))),meet(a,X0)),
inference(forward_demodulation,[],[f10331,f404]) ).
fof(f10624,plain,
! [X2,X0,X1] : meet(join(X1,meet(a,X0)),join(meet(a,X0),X2)) = join(meet(a,X0),meet(X1,join(X2,meet(a,X0)))),
inference(forward_demodulation,[],[f10496,f3]) ).
fof(f11585,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X1,join(X0,X2)),join(meet(X0,X1),X3)),
inference(superposition,[],[f346,f305]) ).
fof(f11638,plain,
! [X2,X3,X0,X1] : join(meet(X1,join(X0,X2)),X3) = join(meet(X0,X1),join(X3,meet(X1,join(X0,X2)))),
inference(forward_demodulation,[],[f11585,f355]) ).
fof(f11777,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(join(meet(y2,x2),meet(y2,a)),meet(y2,join(x2,join(z2,meet(a,meet(x2,join(y2,a)))))))
| ~ spl0_2 ),
inference(superposition,[],[f173,f201]) ).
fof(f11985,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,x2),join(meet(y2,a),meet(y2,join(x2,join(z2,meet(a,meet(x2,join(y2,a))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f11777,f4]) ).
fof(f12081,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(y2,join(x2,join(z2,meet(a,meet(x2,join(y2,a)))))),meet(y2,x2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f11985,f355]) ).
fof(f12160,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(y2,x2),meet(y2,join(x2,join(z2,meet(a,meet(x2,join(y2,a))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12081,f7142]) ).
fof(f12218,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(y2,x2),meet(y2,join(x2,join(z2,meet(a,meet(x2,join(a,y2))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12160,f240]) ).
fof(f12261,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(y2,x2),meet(y2,join(x2,join(z2,meet(a,x2))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12218,f305]) ).
fof(f12299,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(y2,x2),meet(y2,join(x2,z2))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12261,f849]) ).
fof(f12326,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,a),join(meet(x2,y2),meet(y2,join(x2,z2))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12299,f1]) ).
fof(f12338,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(x2,y2),join(meet(y2,join(x2,z2)),meet(y2,a)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12326,f355]) ).
fof(f12345,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(x2,y2),join(meet(y2,a),meet(y2,join(x2,z2))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12338,f7142]) ).
fof(f12351,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,join(x2,z2)),meet(y2,a))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12345,f11638]) ).
fof(f12355,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(y2,join(x2,z2)),meet(a,y2))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12351,f7456]) ).
fof(f12359,plain,
( meet(y2,join(meet(x2,join(y2,a)),join(x2,z2))) = join(meet(a,y2),meet(y2,join(x2,z2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12355,f3]) ).
fof(f12363,plain,
( join(meet(a,y2),meet(y2,join(x2,z2))) = meet(y2,join(z2,join(meet(x2,join(y2,a)),x2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12359,f1242]) ).
fof(f12366,plain,
( join(meet(a,y2),meet(y2,join(x2,z2))) = meet(y2,join(x2,join(z2,meet(x2,join(y2,a)))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12363,f1242]) ).
fof(f12369,plain,
( meet(y2,join(x2,z2)) = join(meet(a,y2),meet(y2,join(x2,z2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f12366,f434]) ).
fof(f12373,definition,
( spl0_9
<=> meet(y2,join(x2,z2)) = join(meet(a,y2),meet(y2,join(x2,z2))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f12375,plain,
( meet(y2,join(x2,z2)) = join(meet(a,y2),meet(y2,join(x2,z2)))
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f12373]) ).
fof(f12376,plain,
( spl0_9
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f12369,f27,f12373]) ).
fof(f14583,plain,
! [X2,X0,X1] : join(meet(X0,meet(X2,X0)),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(join(X0,X1),meet(X2,X0)))),
inference(superposition,[],[f143,f140]) ).
fof(f14888,plain,
! [X2,X0,X1] : join(meet(X0,meet(X2,X0)),meet(X0,X1)) = meet(X0,join(meet(X1,X0),meet(X0,meet(join(X0,X1),X2)))),
inference(forward_demodulation,[],[f14583,f226]) ).
fof(f15011,plain,
! [X2,X0,X1] : join(meet(X0,meet(X2,X0)),meet(X0,X1)) = join(meet(X0,meet(join(X0,X1),X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f14888,f754]) ).
fof(f15115,plain,
! [X2,X0,X1] : join(meet(X0,meet(X2,X0)),meet(X0,X1)) = join(meet(X0,X1),meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f15011,f3]) ).
fof(f15203,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,meet(X2,X0)),meet(X0,X1)),
inference(forward_demodulation,[],[f15115,f208]) ).
fof(f15278,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X2,X0),meet(X0,X1)),
inference(forward_demodulation,[],[f15203,f506]) ).
fof(f19775,plain,
! [X2,X0,X1] : join(meet(X0,meet(join(X0,X1),X2)),meet(X0,X1)) = meet(X0,join(meet(join(X0,X1),X2),meet(X1,join(X0,meet(join(X0,X1),X2))))),
inference(superposition,[],[f222,f6889]) ).
fof(f20159,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,meet(join(X0,X1),X2)),meet(X0,X1)),
inference(forward_demodulation,[],[f19775,f9488]) ).
fof(f20338,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X1,X0),meet(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f20159,f15278]) ).
fof(f20470,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X1,X0),meet(X0,X2)),
inference(forward_demodulation,[],[f20338,f208]) ).
fof(f21334,plain,
! [X2,X0,X1] : join(meet(meet(a,X1),join(X0,meet(X0,X2))),meet(X0,meet(X0,X2))) = meet(join(meet(X0,meet(a,X1)),meet(X0,X2)),join(meet(meet(a,X1),meet(X0,X2)),X0)),
inference(superposition,[],[f16,f20470]) ).
fof(f21344,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(X0,a))) = join(meet(join(X1,meet(a,meet(X0,a))),X2),meet(X2,join(meet(a,X0),meet(a,X1)))),
inference(superposition,[],[f137,f20470]) ).
fof(f21359,plain,
! [X2,X0,X1] : join(meet(X0,X1),meet(X0,X2)) = join(meet(X0,X2),meet(X1,X0)),
inference(superposition,[],[f3,f20470]) ).
fof(f21442,plain,
! [X2,X0,X1] : meet(X2,join(X1,meet(a,X0))) = meet(X2,join(X1,meet(X0,a))),
inference(forward_demodulation,[],[f21344,f1891]) ).
fof(f21449,plain,
! [X2,X0,X1] : join(meet(meet(a,X1),join(X0,meet(X0,X2))),meet(X0,meet(X0,X2))) = meet(join(meet(X0,meet(a,X1)),meet(X0,X2)),join(X0,meet(meet(a,X1),meet(X0,X2)))),
inference(forward_demodulation,[],[f21334,f1187]) ).
fof(f21569,plain,
! [X2,X0,X1] : join(meet(meet(a,X1),join(X0,meet(X0,X2))),meet(X0,meet(X0,X2))) = meet(join(X0,meet(meet(a,X1),meet(X0,X2))),join(meet(X0,meet(a,X1)),meet(X0,X2))),
inference(forward_demodulation,[],[f21449,f1]) ).
fof(f21646,plain,
! [X2,X0,X1] : join(meet(meet(a,X1),join(X0,meet(X0,X2))),meet(X0,meet(X0,X2))) = meet(X0,join(meet(X0,meet(a,X1)),meet(X0,X2))),
inference(forward_demodulation,[],[f21569,f268]) ).
fof(f21696,plain,
! [X2,X0,X1] : join(meet(X0,meet(a,X1)),meet(X0,X2)) = join(meet(meet(a,X1),join(X0,meet(X0,X2))),meet(X0,meet(X0,X2))),
inference(forward_demodulation,[],[f21646,f1653]) ).
fof(f21739,plain,
! [X2,X0,X1] : join(meet(X0,meet(a,X1)),meet(X0,X2)) = join(meet(X0,meet(X0,X2)),meet(meet(a,X1),join(X0,meet(X0,X2)))),
inference(forward_demodulation,[],[f21696,f3]) ).
fof(f21762,plain,
! [X2,X0,X1] : join(meet(X0,meet(a,X1)),meet(X0,X2)) = join(meet(X0,meet(X0,X2)),meet(a,meet(X1,join(X0,meet(X0,X2))))),
inference(forward_demodulation,[],[f21739,f2]) ).
fof(f21771,plain,
! [X2,X0,X1] : join(meet(X0,meet(a,X1)),meet(X0,X2)) = join(meet(X0,meet(X0,X2)),meet(a,meet(X1,X0))),
inference(forward_demodulation,[],[f21762,f5]) ).
fof(f21776,plain,
! [X2,X0,X1] : join(meet(X0,meet(a,X1)),meet(X0,X2)) = join(meet(X0,X2),meet(a,meet(X1,X0))),
inference(forward_demodulation,[],[f21771,f299]) ).
fof(f24045,plain,
( meet(a,y2) = meet(meet(a,y2),meet(y2,join(x2,z2)))
| ~ spl0_9 ),
inference(superposition,[],[f6,f12375]) ).
fof(f24115,plain,
( meet(a,y2) = meet(y2,meet(join(x2,z2),meet(a,y2)))
| ~ spl0_9 ),
inference(forward_demodulation,[],[f24045,f226]) ).
fof(f24154,plain,
( meet(a,y2) = meet(a,meet(y2,meet(y2,join(z2,x2))))
| ~ spl0_9 ),
inference(forward_demodulation,[],[f24115,f1181]) ).
fof(f24185,plain,
( meet(a,y2) = meet(a,meet(y2,meet(y2,join(x2,z2))))
| ~ spl0_9 ),
inference(forward_demodulation,[],[f24154,f1180]) ).
fof(f24215,plain,
( meet(a,y2) = meet(a,meet(y2,join(x2,z2)))
| ~ spl0_9 ),
inference(forward_demodulation,[],[f24185,f299]) ).
fof(f24240,definition,
( spl0_15
<=> meet(a,y2) = meet(a,meet(y2,join(x2,z2))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f24242,plain,
( meet(a,y2) = meet(a,meet(y2,join(x2,z2)))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f24240]) ).
fof(f24243,plain,
( spl0_15
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f24215,f12373,f24240]) ).
fof(f28637,plain,
! [X2,X3,X0,X1] : join(X3,meet(X0,meet(X1,X2))) = join(X3,meet(X0,meet(X2,X1))),
inference(superposition,[],[f7456,f1591]) ).
fof(f28821,plain,
! [X2,X0,X1] : join(X0,meet(X1,X2)) = join(meet(X2,X1),X0),
inference(superposition,[],[f3,f7456]) ).
fof(f28860,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(meet(X2,X1),X0)),
inference(superposition,[],[f1187,f7456]) ).
fof(f29402,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X1,X2))) = meet(X3,join(X0,meet(X2,X1))),
inference(superposition,[],[f1187,f28821]) ).
fof(f33906,plain,
( meet(z2,a) = meet(z2,meet(a,join(x2,y2)))
| ~ spl0_2 ),
inference(superposition,[],[f1422,f29]) ).
fof(f34101,plain,
( meet(z2,a) = meet(a,meet(join(x2,y2),z2))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f33906,f226]) ).
fof(f34190,plain,
( meet(z2,a) = meet(a,meet(z2,join(y2,x2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f34101,f1134]) ).
fof(f34247,plain,
( meet(z2,a) = meet(a,meet(z2,join(x2,y2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f34190,f240]) ).
fof(f34286,plain,
( meet(a,z2) = meet(a,meet(z2,join(x2,y2)))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f34247,f1]) ).
fof(f34308,definition,
( spl0_19
<=> meet(a,z2) = meet(a,meet(z2,join(x2,y2))) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f34310,plain,
( meet(a,z2) = meet(a,meet(z2,join(x2,y2)))
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f34308]) ).
fof(f34311,plain,
( spl0_19
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f34286,f27,f34308]) ).
fof(f61122,plain,
( join(meet(x2,meet(a,y2)),meet(x2,z2)) = meet(x2,join(meet(a,y2),meet(z2,join(x2,meet(a,y2)))))
| ~ spl0_15 ),
inference(superposition,[],[f222,f24242]) ).
fof(f61232,plain,
( join(meet(x2,meet(a,y2)),meet(x2,z2)) = meet(x2,meet(join(z2,meet(a,y2)),join(meet(a,y2),x2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61122,f10624]) ).
fof(f61297,plain,
( join(meet(x2,meet(a,y2)),meet(x2,z2)) = meet(x2,meet(join(x2,meet(a,y2)),join(meet(a,y2),z2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61232,f1426]) ).
fof(f61337,plain,
( meet(x2,join(meet(a,y2),z2)) = join(meet(x2,meet(a,y2)),meet(x2,z2))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61297,f208]) ).
fof(f61374,plain,
( meet(x2,join(meet(a,y2),z2)) = join(meet(x2,z2),meet(a,meet(y2,x2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61337,f21776]) ).
fof(f61398,plain,
( meet(x2,join(meet(a,y2),z2)) = join(meet(x2,z2),meet(a,meet(x2,y2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61374,f28637]) ).
fof(f61415,plain,
( meet(x2,join(z2,meet(y2,a))) = join(meet(x2,z2),meet(a,meet(x2,y2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61398,f28860]) ).
fof(f61429,plain,
( meet(x2,join(z2,meet(a,y2))) = join(meet(x2,z2),meet(a,meet(x2,y2)))
| ~ spl0_15 ),
inference(forward_demodulation,[],[f61415,f21442]) ).
fof(f61440,definition,
( spl0_34
<=> meet(x2,join(z2,meet(a,y2))) = join(meet(x2,z2),meet(a,meet(x2,y2))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f61442,plain,
( meet(x2,join(z2,meet(a,y2))) = join(meet(x2,z2),meet(a,meet(x2,y2)))
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f61440]) ).
fof(f61443,plain,
( spl0_34
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f61429,f24240,f61440]) ).
fof(f164746,plain,
( join(meet(x2,meet(a,z2)),meet(x2,y2)) = meet(x2,join(meet(a,z2),meet(y2,join(x2,meet(a,z2)))))
| ~ spl0_19 ),
inference(superposition,[],[f222,f34310]) ).
fof(f164918,plain,
( join(meet(x2,meet(a,z2)),meet(x2,y2)) = meet(x2,meet(join(y2,meet(a,z2)),join(meet(a,z2),x2)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f164746,f10624]) ).
fof(f165018,plain,
( join(meet(x2,meet(a,z2)),meet(x2,y2)) = meet(x2,meet(join(x2,meet(a,z2)),join(meet(a,z2),y2)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f164918,f1426]) ).
fof(f165090,plain,
( meet(x2,join(meet(a,z2),y2)) = join(meet(x2,meet(a,z2)),meet(x2,y2))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f165018,f208]) ).
fof(f165156,plain,
( meet(x2,join(meet(a,z2),y2)) = join(meet(x2,y2),meet(a,meet(z2,x2)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f165090,f21776]) ).
fof(f165213,plain,
( join(meet(x2,y2),meet(a,meet(x2,z2))) = meet(x2,join(meet(a,z2),y2))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f165156,f28637]) ).
fof(f165247,plain,
( join(meet(x2,y2),meet(a,meet(x2,z2))) = meet(x2,join(y2,meet(z2,a)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f165213,f28860]) ).
fof(f165272,plain,
( join(meet(x2,y2),meet(a,meet(x2,z2))) = meet(x2,join(y2,meet(a,z2)))
| ~ spl0_19 ),
inference(forward_demodulation,[],[f165247,f21442]) ).
fof(f165294,definition,
( spl0_100
<=> join(meet(x2,y2),meet(a,meet(x2,z2))) = meet(x2,join(y2,meet(a,z2))) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f165296,plain,
( join(meet(x2,y2),meet(a,meet(x2,z2))) = meet(x2,join(y2,meet(a,z2)))
| ~ spl0_100 ),
inference(avatar_component_clause,[],[f165294]) ).
fof(f165297,plain,
( spl0_100
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f165272,f34308,f165294]) ).
fof(f165411,plain,
( ! [X0] : meet(X0,join(meet(x2,y2),meet(x2,z2))) = join(meet(X0,meet(x2,join(y2,meet(a,z2)))),meet(X0,join(meet(x2,z2),meet(a,meet(x2,y2)))))
| ~ spl0_100 ),
inference(superposition,[],[f17,f165296]) ).
fof(f165655,plain,
( ! [X0] : meet(X0,join(meet(x2,y2),meet(x2,z2))) = join(meet(X0,meet(x2,join(y2,meet(a,z2)))),meet(X0,meet(x2,join(z2,meet(a,y2)))))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f165411,f61442]) ).
fof(f165771,plain,
( ! [X0] : meet(X0,join(meet(x2,y2),meet(x2,z2))) = meet(X0,meet(x2,join(y2,z2)))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f165655,f235]) ).
fof(f166420,plain,
( join(meet(x2,z2),meet(x2,y2)) = meet(join(meet(x2,z2),x2),meet(x2,join(y2,z2)))
| ~ spl0_34
| ~ spl0_100 ),
inference(superposition,[],[f165771,f1869]) ).
fof(f166855,plain,
( join(meet(x2,z2),meet(x2,y2)) = meet(meet(x2,join(y2,z2)),join(meet(x2,z2),x2))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f166420,f1]) ).
fof(f167015,plain,
( join(meet(x2,z2),meet(x2,y2)) = meet(meet(x2,join(y2,z2)),join(x2,meet(z2,x2)))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f166855,f28860]) ).
fof(f167141,plain,
( join(meet(x2,z2),meet(x2,y2)) = meet(meet(x2,join(y2,z2)),join(x2,meet(x2,z2)))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f167015,f29402]) ).
fof(f167253,plain,
( join(meet(x2,z2),meet(x2,y2)) = meet(x2,meet(join(y2,z2),join(x2,meet(x2,z2))))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f167141,f2]) ).
fof(f167336,plain,
( meet(x2,join(y2,z2)) = join(meet(x2,z2),meet(x2,y2))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f167253,f305]) ).
fof(f167402,plain,
( meet(x2,join(y2,z2)) = join(meet(x2,y2),meet(z2,x2))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f167336,f21359]) ).
fof(f167449,plain,
( meet(x2,join(y2,z2)) = join(meet(x2,y2),meet(x2,z2))
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_demodulation,[],[f167402,f7456]) ).
fof(f167488,plain,
( $false
| spl0_1
| ~ spl0_34
| ~ spl0_100 ),
inference(forward_subsumption_resolution,[],[f167449,f24]) ).
fof(f167489,plain,
( spl0_1
| ~ spl0_34
| ~ spl0_100 ),
inference(avatar_contradiction_clause,[],[f167488]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f25]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f30]) ).
cnf(s10,plain,
( ~ spl0_2
| spl0_9 ),
inference(sat_conversion,[],[f12376]) ).
cnf(s27,plain,
( ~ spl0_9
| spl0_15 ),
inference(sat_conversion,[],[f24243]) ).
cnf(s37,plain,
( ~ spl0_2
| spl0_19 ),
inference(sat_conversion,[],[f34311]) ).
cnf(s71,plain,
( ~ spl0_15
| spl0_34 ),
inference(sat_conversion,[],[f61443]) ).
cnf(s203,plain,
( ~ spl0_19
| spl0_100 ),
inference(sat_conversion,[],[f165297]) ).
cnf(s235,plain,
( spl0_1
| ~ spl0_34
| ~ spl0_100 ),
inference(sat_conversion,[],[f167489]) ).
cnf(s241,plain,
spl0_19,
inference(rat,[],[s37,s2]) ).
cnf(s243,plain,
spl0_9,
inference(rat,[],[s10,s2]) ).
cnf(s255,plain,
spl0_100,
inference(rat,[],[s203,s241]) ).
cnf(s258,plain,
spl0_15,
inference(rat,[],[s27,s243]) ).
cnf(s296,plain,
spl0_34,
inference(rat,[],[s71,s258]) ).
cnf(s307,plain,
spl0_1,
inference(rat,[],[s235,s255,s296]) ).
cnf(s347,plain,
$false,
inference(rat,[],[s1,s307]) ).
fof(f167608,plain,
$false,
inference(avatar_sat_refutation,[],[s347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT400-4 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n007.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 27 15:14:10 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 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
% 84.86/13.01 % (1568535)Detected a unit-equality problem, will run specialized UEQ schedule.
% 84.86/13.01 % (1568545)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=787517653:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 84.86/13.01 % (1568542)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2499268584:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 84.86/13.01 % (1568543)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1684342939:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 84.86/13.01 % (1568540)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=372392479:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 84.86/13.01 % (1568541)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=278789655:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 84.86/13.01 % (1568544)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2907045811:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 84.86/13.01 % (1568546)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=843735820:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 84.86/13.01 % (1568545)Instruction limit reached!
% 84.86/13.01 % (1568545)------------------------------
% 84.86/13.01 % (1568545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.86/13.01 % (1568545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.86/13.01 % (1568545)CaDiCaL version: 2.1.3
% 84.86/13.01 % (1568545)Termination reason: Instruction limit
% 84.86/13.01 % (1568545)Termination phase: Saturation
% 84.86/13.01 % (1568545)Time elapsed: 0.092 s
% 84.86/13.01 % (1568545)Peak memory usage: 91 MB
% 84.86/13.01 % (1568545)Instructions burned: 259 (million)
% 84.86/13.01 % (1568543)Instruction limit reached!
% 84.86/13.01 % (1568543)------------------------------
% 84.86/13.01 % (1568543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.86/13.01 % (1568543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.86/13.01 % (1568543)CaDiCaL version: 2.1.3
% 84.86/13.01 % (1568543)Termination reason: Instruction limit
% 84.86/13.01 % (1568543)Termination phase: Saturation
% 84.86/13.01 % (1568543)Time elapsed: 0.078 s
% 84.86/13.01 % (1568543)Peak memory usage: 88 MB
% 84.86/13.01 % (1568543)Instructions burned: 137 (million)
% 84.86/13.01 % (1568544)Instruction limit reached!
% 84.86/13.01 % (1568544)------------------------------
% 84.86/13.01 % (1568544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.86/13.01 % (1568544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.86/13.01 % (1568544)CaDiCaL version: 2.1.3
% 84.86/13.01 % (1568544)Termination reason: Instruction limit
% 84.86/13.01 % (1568544)Termination phase: Saturation
% 84.86/13.01 % (1568544)Time elapsed: 0.100 s
% 84.86/13.01 % (1568544)Peak memory usage: 89 MB
% 84.86/13.01 % (1568544)Instructions burned: 182 (million)
% 84.86/13.01 % (1568554)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=3113324509:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 84.86/13.01 % (1568555)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3168168226:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 84.86/13.01 % (1568556)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2138215205:i=215:ep=RSTC_2997 on theBenchmark for (2997ds/215Mi)
% 84.86/13.01 % (1568556)Instruction limit reached!
% 84.86/13.01 % (1568556)------------------------------
% 84.86/13.01 % (1568556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.86/13.01 % (1568556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.86/13.01 % (1568556)CaDiCaL version: 2.1.3
% 84.86/13.01 % (1568556)Termination reason: Instruction limit
% 84.86/13.01 % (1568556)Termination phase: Saturation
% 84.86/13.01 % (1568556)Time elapsed: 0.118 s
% 143.38/21.16 % (1568556)Peak memory usage: 91 MB
% 143.38/21.16 % (1568556)Instructions burned: 216 (million)
% 143.38/21.16 % (1568560)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=3744925461:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2994 on theBenchmark for (2994ds/317Mi)
% 143.38/21.16 % (1568546)Instruction limit reached!
% 143.38/21.16 % (1568546)------------------------------
% 143.38/21.16 % (1568546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.38/21.16 % (1568546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.38/21.16 % (1568546)CaDiCaL version: 2.1.3
% 143.38/21.16 % (1568546)Termination reason: Instruction limit
% 143.38/21.16 % (1568546)Termination phase: Saturation
% 143.38/21.16 % (1568546)Time elapsed: 0.645 s
% 143.38/21.16 % (1568546)Peak memory usage: 97 MB
% 143.38/21.16 % (1568546)Instructions burned: 1188 (million)
% 143.38/21.16 % (1568560)Instruction limit reached!
% 143.38/21.16 % (1568560)------------------------------
% 143.38/21.16 % (1568560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.38/21.16 % (1568560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.38/21.16 % (1568560)CaDiCaL version: 2.1.3
% 143.38/21.16 % (1568560)Termination reason: Instruction limit
% 143.38/21.16 % (1568560)Termination phase: Saturation
% 143.38/21.16 % (1568560)Time elapsed: 0.179 s
% 143.38/21.16 % (1568560)Peak memory usage: 92 MB
% 143.38/21.16 % (1568560)Instructions burned: 317 (million)
% 143.38/21.16 % (1568562)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=2790486321:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 143.38/21.16 % (1568563)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3726953389:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 143.38/21.16 % (1568554)Instruction limit reached!
% 143.38/21.16 % (1568554)------------------------------
% 143.38/21.16 % (1568554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.38/21.16 % (1568554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.38/21.16 % (1568554)CaDiCaL version: 2.1.3
% 143.38/21.16 % (1568554)Termination reason: Instruction limit
% 143.38/21.16 % (1568554)Termination phase: Saturation
% 143.38/21.16 % (1568554)Time elapsed: 1.091 s
% 143.38/21.16 % (1568554)Peak memory usage: 141 MB
% 143.38/21.16 % (1568554)Instructions burned: 2051 (million)
% 143.38/21.16 % (1568566)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1460415686:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2985 on theBenchmark for (2985ds/14534Mi)
% 143.38/21.16 % (1568563)Instruction limit reached!
% 143.38/21.16 % (1568563)------------------------------
% 143.38/21.16 % (1568563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.38/21.16 % (1568563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.38/21.16 % (1568563)CaDiCaL version: 2.1.3
% 143.38/21.16 % (1568563)Termination reason: Instruction limit
% 143.38/21.16 % (1568563)Termination phase: Saturation
% 143.38/21.16 % (1568563)Time elapsed: 1.806 s
% 143.38/21.16 % (1568563)Peak memory usage: 128 MB
% 143.38/21.16 % (1568563)Instructions burned: 2836 (million)
% 143.38/21.16 % (1568568)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=3142134239:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/11832Mi)
% 143.38/21.16 % (1568555)Instruction limit reached!
% 143.38/21.16 % (1568555)------------------------------
% 143.38/21.16 % (1568555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.38/21.16 % (1568555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.38/21.16 % (1568555)CaDiCaL version: 2.1.3
% 143.38/21.16 % (1568555)Termination reason: Instruction limit
% 143.38/21.16 % (1568555)Termination phase: Saturation
% 143.38/21.16 % (1568555)Time elapsed: 2.926 s
% 143.38/21.16 % (1568555)Peak memory usage: 163 MB
% 143.38/21.16 % (1568555)Instructions burned: 4948 (million)
% 143.38/21.16 % (1568570)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=122682252:i=2279:fgj=on:bd=all_2966 on theBenchmark for (2966ds/2279Mi)
% 143.38/21.16 % (1568570)Instruction limit reached!
% 143.38/21.16 % (1568570)------------------------------
% 237.35/34.43 % (1568570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568570)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568570)Termination reason: Instruction limit
% 237.35/34.43 % (1568570)Termination phase: Saturation
% 237.35/34.43 % (1568570)Time elapsed: 1.373 s
% 237.35/34.43 % (1568570)Peak memory usage: 138 MB
% 237.35/34.43 % (1568570)Instructions burned: 2280 (million)
% 237.35/34.43 % (1568572)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=2869197691:st=3:i=6225:bd=all:gtg=exists_all:ss=included:er=filter:sgt=10_2951 on theBenchmark for (2951ds/6225Mi)
% 237.35/34.43 % (1568562)Instruction limit reached!
% 237.35/34.43 % (1568562)------------------------------
% 237.35/34.43 % (1568562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568562)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568562)Termination reason: Instruction limit
% 237.35/34.43 % (1568562)Termination phase: Saturation
% 237.35/34.43 % (1568562)Time elapsed: 7.251 s
% 237.35/34.43 % (1568562)Peak memory usage: 230 MB
% 237.35/34.43 % (1568562)Instructions burned: 12125 (million)
% 237.35/34.43 % (1568574)lrs-1010_1_sil=32000:tgt=ground:etr=on:sp=const_frequency:spb=goal_then_units:rnwc=on:lwlo=on:random_seed=2276697263:lrd=on:i=21755:kws=frequency:fgj=on:bd=preordered:nm=4:ins=20:av=off_2917 on theBenchmark for (2917ds/21755Mi)
% 237.35/34.43 % (1568572)Instruction limit reached!
% 237.35/34.43 % (1568572)------------------------------
% 237.35/34.43 % (1568572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568572)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568572)Termination reason: Instruction limit
% 237.35/34.43 % (1568572)Termination phase: Saturation
% 237.35/34.43 % (1568572)Time elapsed: 3.728 s
% 237.35/34.43 % (1568572)Peak memory usage: 157 MB
% 237.35/34.43 % (1568572)Instructions burned: 6226 (million)
% 237.35/34.43 % (1568576)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:flr=on:random_seed=2574624249:s2pl=no:i=16427:s2at=1.5:bd=all:fsr=off_2912 on theBenchmark for (2912ds/16427Mi)
% 237.35/34.43 % (1568568)Instruction limit reached!
% 237.35/34.43 % (1568568)------------------------------
% 237.35/34.43 % (1568568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568568)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568568)Termination reason: Instruction limit
% 237.35/34.43 % (1568568)Termination phase: Saturation
% 237.35/34.43 % (1568568)Time elapsed: 7.444 s
% 237.35/34.43 % (1568568)Peak memory usage: 215 MB
% 237.35/34.43 % (1568568)Instructions burned: 11832 (million)
% 237.35/34.43 % (1568578)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=3512973149:i=9356:fgj=on:bd=preordered:av=off_2895 on theBenchmark for (2895ds/9356Mi)
% 237.35/34.43 % (1568566)Instruction limit reached!
% 237.35/34.43 % (1568566)------------------------------
% 237.35/34.43 % (1568566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568566)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568566)Termination reason: Instruction limit
% 237.35/34.43 % (1568566)Termination phase: Saturation
% 237.35/34.43 % (1568566)Time elapsed: 9.072 s
% 237.35/34.43 % (1568566)Peak memory usage: 231 MB
% 237.35/34.43 % (1568566)Instructions burned: 14534 (million)
% 237.35/34.43 % (1568580)dis+10_6_sil=8000:tgt=ground:prc=on:drc=ordering:spb=non_intro:fd=preordered:foolp=on:slsqc=1:slsq=on:random_seed=3629431853:i=2070:kws=inv_precedence:slsql=off:bd=all_2892 on theBenchmark for (2892ds/2070Mi)
% 237.35/34.43 % (1568580)Instruction limit reached!
% 237.35/34.43 % (1568580)------------------------------
% 237.35/34.43 % (1568580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 237.35/34.43 % (1568580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 237.35/34.43 % (1568580)CaDiCaL version: 2.1.3
% 237.35/34.43 % (1568580)Termination reason: Instruction limit
% 237.35/34.43 % (1568580)Termination phase: Saturation
% 120.23/34.84 % (1568580)Time elapsed: 1.237 s
% 120.23/34.84 % (1568580)Peak memory usage: 131 MB
% 120.23/34.84 % (1568580)Instructions burned: 2071 (million)
% 120.23/34.84 % (1568582)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=1918377871:st=3:i=6461:fgj=on:bd=preordered:av=off:ss=axioms_2878 on theBenchmark for (2878ds/6461Mi)
% 120.23/34.84 % (1568582)Instruction limit reached!
% 120.23/34.84 % (1568582)------------------------------
% 120.23/34.84 % (1568582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568582)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568582)Termination reason: Instruction limit
% 120.23/34.84 % (1568582)Termination phase: Saturation
% 120.23/34.84 % (1568582)Time elapsed: 3.992 s
% 120.23/34.84 % (1568582)Peak memory usage: 170 MB
% 120.23/34.84 % (1568582)Instructions burned: 6462 (million)
% 120.23/34.84 % (1568578)Instruction limit reached!
% 120.23/34.84 % (1568578)------------------------------
% 120.23/34.84 % (1568578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568578)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568578)Termination reason: Instruction limit
% 120.23/34.84 % (1568578)Termination phase: Saturation
% 120.23/34.84 % (1568578)Time elapsed: 5.659 s
% 120.23/34.84 % (1568578)Peak memory usage: 196 MB
% 120.23/34.84 % (1568578)Instructions burned: 9356 (million)
% 120.23/34.84 % (1568584)lrs+10_6_to=lpo:lpd=off:sil=8000:tgt=ground:drc=off:sp=arity:spb=goal:fd=preordered:random_seed=3215850140:i=2310:bd=all:ss=included_2837 on theBenchmark for (2837ds/2310Mi)
% 120.23/34.84 % (1568585)dis+11_1_sil=8000:fd=off:nwc=20:random_seed=794198669:st=3:s2pl=on:i=2616:av=off:fsr=off:ss=axioms:sgt=8_2836 on theBenchmark for (2836ds/2616Mi)
% 120.23/34.84 % (1568584)Instruction limit reached!
% 120.23/34.84 % (1568584)------------------------------
% 120.23/34.84 % (1568584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568584)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568584)Termination reason: Instruction limit
% 120.23/34.84 % (1568584)Termination phase: Saturation
% 120.23/34.84 % (1568584)Time elapsed: 1.435 s
% 120.23/34.84 % (1568584)Peak memory usage: 104 MB
% 120.23/34.84 % (1568584)Instructions burned: 2310 (million)
% 120.23/34.84 % (1568588)lrs+0_1_ncem=casc2026/models/loop3.pt:sil=32000:tgt=ground:npcc=on:sp=occurrence:urr=ec_only:fd=preordered:random_seed=3964125064:i=30521:gtgl=2:kws=inv_arity:bd=all:gtg=exists_sym_2821 on theBenchmark for (2821ds/30521Mi)
% 120.23/34.84 % (1568585)Instruction limit reached!
% 120.23/34.84 % (1568585)------------------------------
% 120.23/34.84 % (1568585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568585)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568585)Termination reason: Instruction limit
% 120.23/34.84 % (1568585)Termination phase: Saturation
% 120.23/34.84 % (1568585)Time elapsed: 1.539 s
% 120.23/34.84 % (1568585)Peak memory usage: 125 MB
% 120.23/34.84 % (1568585)Instructions burned: 2616 (million)
% 120.23/34.84 % (1568590)lrs+11_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:tgt=full:npcc=on:prc=on:fde=unused:sp=reverse_frequency:spb=goal:acc=on:urr=ec_only:s2agt=32:random_seed=1566616855:i=3258:fgj=on:bd=all:ins=1_2819 on theBenchmark for (2819ds/3258Mi)
% 120.23/34.84 % (1568576)Instruction limit reached!
% 120.23/34.84 % (1568576)------------------------------
% 120.23/34.84 % (1568576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568576)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568576)Termination reason: Instruction limit
% 120.23/34.84 % (1568576)Termination phase: Saturation
% 120.23/34.84 % (1568576)Time elapsed: 10.197 s
% 120.23/34.84 % (1568576)Peak memory usage: 223 MB
% 120.23/34.84 % (1568576)Instructions burned: 16428 (million)
% 120.23/34.84 % (1568592)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=reverse_frequency:kmz=on:random_seed=3978133528:i=5037:kws=precedence_2800 on theBenchmark for (2800ds/5037Mi)
% 120.23/34.84 % (1568590)Instruction limit reached!
% 120.23/34.84 % (1568590)------------------------------
% 120.23/34.84 % (1568590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568590)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568590)Termination reason: Instruction limit
% 120.23/34.84 % (1568590)Termination phase: Saturation
% 120.23/34.84 % (1568590)Time elapsed: 2.038 s
% 120.23/34.84 % (1568590)Peak memory usage: 152 MB
% 120.23/34.84 % (1568590)Instructions burned: 3258 (million)
% 120.23/34.84 % (1568594)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:acc=on:urr=on:bsr=unit_only:br=off:random_seed=2863993532:i=65240_2797 on theBenchmark for (2797ds/65240Mi)
% 120.23/34.84 % (1568592)Instruction limit reached!
% 120.23/34.84 % (1568592)------------------------------
% 120.23/34.84 % (1568592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568592)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568592)Termination reason: Instruction limit
% 120.23/34.84 % (1568592)Termination phase: Saturation
% 120.23/34.84 % (1568592)Time elapsed: 3.044 s
% 120.23/34.84 % (1568592)Peak memory usage: 164 MB
% 120.23/34.84 % (1568592)Instructions burned: 5037 (million)
% 120.23/34.84 % (1568596)lrs-1011_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:urr=ec_only:random_seed=4017304774:i=16502:kws=inv_precedence:fgj=on:bd=preordered:ins=3:av=off_2768 on theBenchmark for (2768ds/16502Mi)
% 120.23/34.84 % (1568574)Instruction limit reached!
% 120.23/34.84 % (1568574)------------------------------
% 120.23/34.84 % (1568574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568574)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568574)Termination reason: Instruction limit
% 120.23/34.84 % (1568574)Termination phase: Saturation
% 120.23/34.84 % (1568574)Time elapsed: 15.228 s
% 120.23/34.84 % (1568574)Peak memory usage: 231 MB
% 120.23/34.84 % (1568574)Instructions burned: 21756 (million)
% 120.23/34.84 % (1568598)lrs-1011_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=32000:npcc=on:drc=off:sp=const_max:spb=goal_then_units:urr=ec_only:fd=preordered:random_seed=3605806670:i=7623:bd=preordered:er=filter_2763 on theBenchmark for (2763ds/7623Mi)
% 120.23/34.84 % (1568598)Instruction limit reached!
% 120.23/34.84 % (1568598)------------------------------
% 120.23/34.84 % (1568598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568598)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568598)Termination reason: Instruction limit
% 120.23/34.84 % (1568598)Termination phase: Saturation
% 120.23/34.84 % (1568598)Time elapsed: 4.623 s
% 120.23/34.84 % (1568598)Peak memory usage: 185 MB
% 120.23/34.84 % (1568598)Instructions burned: 7623 (million)
% 120.23/34.84 % (1568600)dis+1010_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:tgt=full:npcc=on:sp=const_min:spb=non_intro:lcm=predicate:acc=on:urr=ec_only:rp=on:gs=on:random_seed=3431437267:i=8183:kws=frequency:add=off:gsp=on_2715 on theBenchmark for (2715ds/8183Mi)
% 120.23/34.84 % (1568600)Instruction limit reached!
% 120.23/34.84 % (1568600)------------------------------
% 120.23/34.84 % (1568600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568600)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568600)Termination reason: Instruction limit
% 120.23/34.84 % (1568600)Termination phase: Saturation
% 120.23/34.84 % (1568600)Time elapsed: 4.563 s
% 120.23/34.84 % (1568600)Peak memory usage: 200 MB
% 120.23/34.84 % (1568600)Instructions burned: 8184 (million)
% 120.23/34.84 % (1568603)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:bsr=unit_only:random_seed=4163469515:i=8387_2667 on theBenchmark for (2667ds/8387Mi)
% 120.23/34.84 % (1568596)Instruction limit reached!
% 120.23/34.84 % (1568596)------------------------------
% 120.23/34.84 % (1568596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.23/34.84 % (1568596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.23/34.84 % (1568596)CaDiCaL version: 2.1.3
% 120.23/34.84 % (1568596)Termination reason: Instruction limit
% 120.23/34.84 % (1568596)Termination phase: Saturation
% 120.23/34.84 % (1568596)Time elapsed: 10.221 s
% 120.23/34.84 % (1568596)Peak memory usage: 242 MB
% 120.23/34.84 % (1568596)Instructions burned: 16502 (million)
% 120.23/34.84 % (1568594)First to succeed.
% 120.23/34.84 % (1568594)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1568535"
% 120.23/34.84 % (1568605)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=1123152967:i=53964:kws=inv_arity_squared:fgj=on:bd=preordered_2664 on theBenchmark for (2664ds/53964Mi)
% 120.23/34.84 % (1568594)Refutation found. Thanks to Tanya!
% 120.23/34.84 % SZS status Unsatisfiable for theBenchmark
% 120.23/34.84 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/35.04 % (1568594)------------------------------
% 0.18/35.04 % (1568594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/35.04 % (1568594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/35.04 % (1568594)CaDiCaL version: 2.1.3
% 0.18/35.04 % (1568594)Termination reason: Refutation
% 0.18/35.04 % (1568594)Time elapsed: 13.159 s
% 0.18/35.04 % (1568594)Peak memory usage: 276 MB
% 0.18/35.04 % (1568594)Instructions burned: 20716 (million)
% 0.18/35.04 % (1568594)------------------------------
% 0.18/35.04 % (1568594)------------------------------
% 0.18/35.04 % (1568535)Success in time 33.951 s
% 0.18/35.04 % Vampire exiting
%------------------------------------------------------------------------------