%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT398-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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:36 AM UTC 2026
% Result : Unsatisfiable 69.55s 10.78s
% Output : Refutation 70.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 28
% Syntax : Number of formulae : 331 ( 324 unt; 17 def)
% Number of atoms : 338 ( 337 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 18 ( 11 ~; 7 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 25 con; 0-3 aty)
% Number of variables : 423 ( 423 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity) ).
fof(f2,axiom,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(meet(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity) ).
fof(f3,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_001) ).
fof(f4,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_002) ).
fof(f5,axiom,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption) ).
fof(f6,axiom,
! [X0,X1] : meet(X0,join(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption_003) ).
fof(f7,axiom,
! [X2,X0,X1] : upme(X0,X1,X2) = meet(X0,join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_upme) ).
fof(f8,axiom,
! [X2,X0,X1] : lome(X0,X1,X2) = join(meet(X0,X1),meet(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',definition_of_lome) ).
fof(f9,axiom,
! [X2,X0,X1] : upme(meet(a,X0),X1,X2) = lome(meet(a,X0),X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq1) ).
fof(f10,axiom,
! [X2,X0,X1] :
( upme(a,X0,X1) != upme(a,X0,X2)
| upme(X0,X1,X2) = lome(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qu2) ).
fof(f11,negated_conjecture,
meet(t,join(meet(join(x,y),join(x,z)),meet(join(u,w),join(u,v)))) != join(meet(t,join(meet(join(x,y),join(x,z)),join(u,meet(w,v)))),meet(t,join(meet(join(u,w),join(u,v)),join(x,meet(y,z))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rl2) ).
fof(f12,plain,
! [X2,X0,X1] : meet(meet(a,X0),join(X1,X2)) = join(meet(meet(a,X0),X1),meet(meet(a,X0),X2)),
inference(definition_unfolding,[],[f9,f7,f8]) ).
fof(f13,plain,
! [X2,X0,X1] :
( meet(X0,join(X1,X2)) = join(meet(X0,X1),meet(X0,X2))
| meet(a,join(X0,X1)) != meet(a,join(X0,X2)) ),
inference(definition_unfolding,[],[f10,f7,f7,f7,f8]) ).
fof(f14,definition,
sF0 = join(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f15,plain,
join(x,y) = sF0,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF1 = join(x,z),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f17,plain,
join(x,z) = sF1,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF2 = meet(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f19,plain,
meet(sF0,sF1) = sF2,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF3 = join(u,w),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f21,plain,
join(u,w) = sF3,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF4 = join(u,v),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f23,plain,
join(u,v) = sF4,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF5 = meet(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f25,plain,
meet(sF3,sF4) = sF5,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF6 = join(sF2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f27,plain,
join(sF2,sF5) = sF6,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF7 = meet(t,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f29,plain,
meet(t,sF6) = sF7,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF8 = meet(w,v),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f31,plain,
meet(w,v) = sF8,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF9 = join(u,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f33,plain,
join(u,sF8) = sF9,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF10 = join(sF2,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f35,plain,
join(sF2,sF9) = sF10,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF11 = meet(t,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f37,plain,
meet(t,sF10) = sF11,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF12 = meet(y,z),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f39,plain,
meet(y,z) = sF12,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF13 = join(x,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f41,plain,
join(x,sF12) = sF13,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF14 = join(sF5,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f43,plain,
join(sF5,sF13) = sF14,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF15 = meet(t,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f45,plain,
meet(t,sF14) = sF15,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF16 = join(sF11,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f47,plain,
join(sF11,sF15) = sF16,
inference(reorient_equations,[],[f46]) ).
fof(f48,plain,
sF7 != sF16,
inference(definition_folding,[],[f11,f47,f45,f43,f41,f39,f25,f23,f21,f37,f35,f33,f31,f19,f17,f15,f29,f27,f25,f23,f21,f19,f17,f15]) ).
fof(f49,plain,
! [X2,X0,X1] : meet(meet(a,X0),join(X1,X2)) = join(meet(a,meet(X0,X1)),meet(meet(a,X0),X2)),
inference(backward_demodulation,[],[f12,f2]) ).
fof(f50,plain,
sF0 = join(y,x),
inference(forward_demodulation,[],[f15,f3]) ).
fof(f51,plain,
sF1 = join(z,x),
inference(forward_demodulation,[],[f17,f3]) ).
fof(f52,plain,
sF3 = join(w,u),
inference(forward_demodulation,[],[f21,f3]) ).
fof(f53,plain,
sF4 = join(v,u),
inference(forward_demodulation,[],[f23,f3]) ).
fof(f54,plain,
sF10 = join(sF9,sF2),
inference(forward_demodulation,[],[f35,f3]) ).
fof(f55,plain,
join(x,meet(y,z)) = sF13,
inference(forward_demodulation,[],[f41,f39]) ).
fof(f56,plain,
sF14 = join(sF13,sF5),
inference(forward_demodulation,[],[f43,f3]) ).
fof(f57,plain,
! [X2,X0,X1] : meet(meet(a,X0),join(X1,X2)) = join(meet(a,meet(X0,X1)),meet(a,meet(X0,X2))),
inference(forward_demodulation,[],[f49,f2]) ).
fof(f58,plain,
! [X2,X0,X1] : join(meet(a,meet(X0,X1)),meet(a,meet(X0,X2))) = meet(a,meet(X0,join(X1,X2))),
inference(forward_demodulation,[],[f57,f2]) ).
fof(f59,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f5,f6]) ).
fof(f60,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f6,f5]) ).
fof(f64,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f6,f3]) ).
fof(f65,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f64,f5]) ).
fof(f70,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f65,f1]) ).
fof(f72,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f5,f1]) ).
fof(f77,plain,
u = meet(u,sF4),
inference(superposition,[],[f64,f53]) ).
fof(f81,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f72,f6]) ).
fof(f90,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f81,f4]) ).
fof(f94,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X0,X2))) = join(meet(a,meet(X0,X1)),meet(a,meet(X1,X2))),
inference(superposition,[],[f58,f1]) ).
fof(f99,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X2,X0))) = join(meet(a,meet(X1,X2)),meet(a,meet(X0,X1))),
inference(superposition,[],[f58,f1]) ).
fof(f107,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = join(meet(a,meet(X0,X2)),meet(a,meet(X0,X1))),
inference(superposition,[],[f3,f58]) ).
fof(f134,plain,
v = join(v,sF8),
inference(superposition,[],[f72,f31]) ).
fof(f135,plain,
w = join(w,sF8),
inference(superposition,[],[f5,f31]) ).
fof(f144,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f4,f5]) ).
fof(f145,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f4,f72]) ).
fof(f147,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f4,f3]) ).
fof(f150,plain,
! [X0] : join(y,join(x,X0)) = join(sF0,X0),
inference(superposition,[],[f4,f50]) ).
fof(f151,plain,
! [X0] : join(z,join(x,X0)) = join(sF1,X0),
inference(superposition,[],[f4,f51]) ).
fof(f154,plain,
! [X0] : join(sF10,X0) = join(sF9,join(sF2,X0)),
inference(superposition,[],[f4,f54]) ).
fof(f163,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f177,plain,
! [X0] : join(u,join(sF8,X0)) = join(sF9,X0),
inference(superposition,[],[f4,f33]) ).
fof(f191,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f4,f59]) ).
fof(f200,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f191,f3]) ).
fof(f234,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f2,f6]) ).
fof(f235,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f2,f64]) ).
fof(f244,plain,
! [X0] : meet(sF0,meet(sF1,X0)) = meet(sF2,X0),
inference(superposition,[],[f2,f19]) ).
fof(f245,plain,
! [X0] : meet(sF3,meet(sF4,X0)) = meet(sF5,X0),
inference(superposition,[],[f2,f25]) ).
fof(f254,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f258,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f72,f2]) ).
fof(f284,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(sF6,X0)),
inference(superposition,[],[f234,f27]) ).
fof(f301,plain,
! [X2,X0,X1] : meet(a,meet(join(a,X1),join(X0,X2))) = join(meet(a,X0),meet(a,meet(join(a,X1),X2))),
inference(superposition,[],[f58,f234]) ).
fof(f302,plain,
! [X2,X0,X1] : meet(a,meet(join(a,X1),join(X0,X2))) = join(meet(a,X0),meet(a,X2)),
inference(forward_demodulation,[],[f301,f234]) ).
fof(f313,plain,
! [X0] : meet(sF2,X0) = meet(sF6,meet(X0,sF2)),
inference(forward_demodulation,[],[f284,f254]) ).
fof(f315,plain,
! [X2,X0] : meet(a,join(X0,X2)) = join(meet(a,X0),meet(a,X2)),
inference(forward_demodulation,[],[f302,f234]) ).
fof(f321,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,join(meet(X0,X2),meet(X0,X1))),
inference(backward_demodulation,[],[f107,f315]) ).
fof(f322,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,join(meet(X0,X1),meet(X0,X2))),
inference(backward_demodulation,[],[f58,f315]) ).
fof(f323,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X2,X0))) = meet(a,join(meet(X1,X2),meet(X0,X1))),
inference(backward_demodulation,[],[f99,f315]) ).
fof(f324,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X0,X2))) = meet(a,join(meet(X0,X1),meet(X1,X2))),
inference(backward_demodulation,[],[f94,f315]) ).
fof(f378,plain,
! [X2,X3,X0,X1] : meet(a,meet(a,join(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(a,join(meet(a,X3),meet(a,meet(X0,join(X1,X2))))),
inference(superposition,[],[f322,f322]) ).
fof(f398,plain,
! [X2,X3,X0,X1] : meet(a,meet(a,join(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(a,meet(a,join(X3,meet(X0,join(X1,X2))))),
inference(forward_demodulation,[],[f378,f322]) ).
fof(f419,plain,
! [X2,X3,X0,X1] : meet(a,meet(a,join(X3,join(meet(X0,X1),meet(X0,X2))))) = meet(a,join(X3,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f398,f70]) ).
fof(f433,plain,
! [X2,X3,X0,X1] : meet(a,join(X3,join(meet(X0,X1),meet(X0,X2)))) = meet(a,join(X3,meet(X0,join(X1,X2)))),
inference(forward_demodulation,[],[f419,f70]) ).
fof(f444,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X0,X2))) = meet(a,join(X0,meet(join(X1,X0),X2))),
inference(superposition,[],[f324,f64]) ).
fof(f456,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X2,X0))) = meet(a,join(meet(X2,X1),meet(X0,X1))),
inference(superposition,[],[f324,f1]) ).
fof(f472,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X2,X1))) = meet(a,join(meet(X0,X1),meet(X2,X0))),
inference(superposition,[],[f324,f3]) ).
fof(f552,plain,
! [X0] : meet(a,meet(sF1,join(X0,sF0))) = meet(a,join(meet(sF1,X0),sF2)),
inference(superposition,[],[f323,f19]) ).
fof(f553,plain,
! [X0] : meet(a,meet(sF4,join(X0,sF3))) = meet(a,join(meet(sF4,X0),sF5)),
inference(superposition,[],[f323,f25]) ).
fof(f644,plain,
sF13 = join(meet(y,z),sF13),
inference(superposition,[],[f200,f55]) ).
fof(f647,plain,
sF9 = join(sF8,sF9),
inference(superposition,[],[f200,f33]) ).
fof(f673,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(X0,X2)),
inference(superposition,[],[f235,f72]) ).
fof(f681,plain,
! [X0] : meet(u,X0) = meet(u,meet(sF3,X0)),
inference(superposition,[],[f235,f52]) ).
fof(f684,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(sF10,X0)),
inference(superposition,[],[f235,f54]) ).
fof(f686,plain,
! [X0] : meet(sF5,X0) = meet(sF5,meet(sF14,X0)),
inference(superposition,[],[f235,f56]) ).
fof(f720,plain,
! [X0] : meet(sF5,X0) = meet(sF14,meet(X0,sF5)),
inference(forward_demodulation,[],[f686,f254]) ).
fof(f721,plain,
! [X0] : meet(sF2,X0) = meet(sF10,meet(X0,sF2)),
inference(forward_demodulation,[],[f684,f254]) ).
fof(f724,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f673,f254]) ).
fof(f732,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f724,f2]) ).
fof(f769,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f254,f6]) ).
fof(f770,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f254,f64]) ).
fof(f788,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(meet(X1,X0),X1)),
inference(superposition,[],[f60,f254]) ).
fof(f833,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,meet(X1,X0))),
inference(forward_demodulation,[],[f788,f1]) ).
fof(f869,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f833,f732]) ).
fof(f903,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f144,f3]) ).
fof(f912,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f64,f144]) ).
fof(f921,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f912,f1]) ).
fof(f951,plain,
! [X0] :
( meet(t,join(sF10,X0)) = join(sF11,meet(t,X0))
| meet(a,join(t,X0)) != meet(a,join(t,sF10)) ),
inference(superposition,[],[f13,f37]) ).
fof(f1108,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f144,f163]) ).
fof(f1206,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f64,f90]) ).
fof(f1843,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f145,f3]) ).
fof(f2232,plain,
join(sF0,meet(y,z)) = join(y,sF13),
inference(superposition,[],[f150,f55]) ).
fof(f2235,plain,
! [X0] : join(sF0,X0) = join(y,join(X0,x)),
inference(superposition,[],[f150,f3]) ).
fof(f2312,plain,
! [X0] : join(y,x) = join(sF0,meet(y,X0)),
inference(superposition,[],[f144,f2235]) ).
fof(f2331,plain,
! [X0] : sF0 = join(sF0,meet(y,X0)),
inference(forward_demodulation,[],[f2312,f50]) ).
fof(f2344,plain,
sF0 = join(y,sF13),
inference(backward_demodulation,[],[f2232,f2331]) ).
fof(f2477,plain,
join(sF1,meet(y,z)) = join(z,sF13),
inference(superposition,[],[f151,f55]) ).
fof(f2480,plain,
! [X0] : join(sF1,X0) = join(z,join(X0,x)),
inference(superposition,[],[f151,f3]) ).
fof(f2558,plain,
! [X0] : join(z,x) = join(sF1,meet(X0,z)),
inference(superposition,[],[f145,f2480]) ).
fof(f2575,plain,
! [X0] : sF1 = join(sF1,meet(X0,z)),
inference(forward_demodulation,[],[f2558,f51]) ).
fof(f2589,plain,
sF1 = join(z,sF13),
inference(backward_demodulation,[],[f2477,f2575]) ).
fof(f2812,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,meet(X0,join(X2,X1))),
inference(superposition,[],[f322,f321]) ).
fof(f3088,plain,
! [X2,X0,X1] : meet(a,meet(X2,join(X1,X0))) = meet(a,meet(join(X0,X1),X2)),
inference(superposition,[],[f2812,f1]) ).
fof(f3134,plain,
! [X0,X1] : meet(a,join(X1,X0)) = meet(a,meet(a,join(X0,X1))),
inference(superposition,[],[f70,f2812]) ).
fof(f3170,plain,
! [X0,X1] : meet(a,join(X0,X1)) = meet(a,join(X1,X0)),
inference(forward_demodulation,[],[f3134,f70]) ).
fof(f3888,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(join(X1,meet(X0,X2)),X3)),
inference(superposition,[],[f4,f903]) ).
fof(f3929,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X1,join(meet(X0,X2),X3))),
inference(forward_demodulation,[],[f3888,f4]) ).
fof(f3950,plain,
! [X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X3,X1)),
inference(forward_demodulation,[],[f3929,f1108]) ).
fof(f4086,plain,
! [X0] : join(sF9,X0) = join(u,join(X0,sF8)),
inference(superposition,[],[f177,f3]) ).
fof(f4670,plain,
sF13 = meet(sF13,sF1),
inference(superposition,[],[f64,f2589]) ).
fof(f4685,plain,
sF13 = meet(sF1,sF13),
inference(forward_demodulation,[],[f4670,f1]) ).
fof(f4690,plain,
sF13 = meet(sF13,sF0),
inference(superposition,[],[f64,f2344]) ).
fof(f4705,plain,
sF13 = meet(sF0,sF13),
inference(forward_demodulation,[],[f4690,f1]) ).
fof(f5358,plain,
! [X2,X3,X0,X1] : meet(a,join(meet(a,X3),meet(a,meet(X0,join(X1,X2))))) = meet(a,meet(a,join(meet(join(X2,X1),X0),X3))),
inference(superposition,[],[f321,f3088]) ).
fof(f5378,plain,
! [X2,X3,X0,X1] : meet(a,join(meet(a,X3),meet(a,meet(X0,join(X1,X2))))) = meet(a,join(meet(join(X2,X1),X0),X3)),
inference(forward_demodulation,[],[f5358,f70]) ).
fof(f5501,plain,
! [X2,X3,X0,X1] : meet(a,meet(a,join(X3,meet(X0,join(X1,X2))))) = meet(a,join(meet(join(X2,X1),X0),X3)),
inference(forward_demodulation,[],[f5378,f322]) ).
fof(f5600,plain,
! [X2,X3,X0,X1] : meet(a,join(X3,meet(X0,join(X1,X2)))) = meet(a,join(meet(join(X2,X1),X0),X3)),
inference(forward_demodulation,[],[f5501,f70]) ).
fof(f5654,plain,
join(u,v) = join(sF9,v),
inference(superposition,[],[f4086,f134]) ).
fof(f5675,plain,
join(u,v) = join(v,sF9),
inference(forward_demodulation,[],[f5654,f3]) ).
fof(f5678,plain,
join(v,u) = join(v,sF9),
inference(forward_demodulation,[],[f5675,f3]) ).
fof(f5680,plain,
sF4 = join(v,sF9),
inference(forward_demodulation,[],[f5678,f53]) ).
fof(f5788,plain,
! [X2,X0,X1] : meet(a,meet(a,join(X2,join(X1,X0)))) = meet(a,join(meet(X2,a),meet(a,join(X0,X1)))),
inference(superposition,[],[f324,f3170]) ).
fof(f5794,plain,
! [X2,X0,X1] : meet(a,meet(a,join(X2,join(X1,X0)))) = meet(a,meet(a,join(X2,join(X0,X1)))),
inference(forward_demodulation,[],[f5788,f324]) ).
fof(f5836,plain,
! [X2,X0,X1] : meet(a,join(X2,join(X0,X1))) = meet(a,meet(a,join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f5794,f70]) ).
fof(f5866,plain,
! [X2,X0,X1] : meet(a,join(X2,join(X0,X1))) = meet(a,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f5836,f70]) ).
fof(f5953,plain,
! [X0] : join(sF6,X0) = join(sF5,join(sF2,X0)),
inference(superposition,[],[f147,f27]) ).
fof(f5956,plain,
! [X0] : join(sF14,X0) = join(sF5,join(sF13,X0)),
inference(superposition,[],[f147,f56]) ).
fof(f6029,plain,
! [X0] : join(sF14,X0) = join(sF13,join(X0,sF5)),
inference(forward_demodulation,[],[f5956,f163]) ).
fof(f6032,plain,
! [X0] : join(sF6,X0) = join(sF2,join(X0,sF5)),
inference(forward_demodulation,[],[f5953,f163]) ).
fof(f6110,plain,
join(u,w) = join(sF9,w),
inference(superposition,[],[f4086,f135]) ).
fof(f6133,plain,
join(u,w) = join(w,sF9),
inference(forward_demodulation,[],[f6110,f3]) ).
fof(f6136,plain,
join(w,u) = join(w,sF9),
inference(forward_demodulation,[],[f6133,f3]) ).
fof(f6137,plain,
sF3 = join(w,sF9),
inference(forward_demodulation,[],[f6136,f52]) ).
fof(f6141,plain,
sF9 = meet(sF9,sF3),
inference(superposition,[],[f64,f6137]) ).
fof(f6164,plain,
sF9 = meet(sF3,sF9),
inference(forward_demodulation,[],[f6141,f1]) ).
fof(f6966,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f72,f869]) ).
fof(f9870,plain,
sF9 = meet(sF9,sF4),
inference(superposition,[],[f64,f5680]) ).
fof(f9900,plain,
sF9 = meet(sF4,sF9),
inference(forward_demodulation,[],[f9870,f1]) ).
fof(f10135,plain,
join(sF10,sF5) = join(sF9,sF6),
inference(superposition,[],[f154,f27]) ).
fof(f10217,plain,
join(sF10,sF5) = join(sF6,sF9),
inference(forward_demodulation,[],[f10135,f3]) ).
fof(f11592,plain,
! [X0,X1] : join(meet(a,X1),meet(a,X0)) = meet(a,join(X1,meet(a,X0))),
inference(superposition,[],[f315,f70]) ).
fof(f11664,plain,
! [X0,X1] : meet(a,join(X1,X0)) = meet(a,join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f11592,f315]) ).
fof(f12670,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f200,f6966]) ).
fof(f13286,plain,
( join(sF11,sF15) = meet(t,join(sF10,sF14))
| meet(a,join(t,sF14)) != meet(a,join(t,sF10)) ),
inference(superposition,[],[f951,f45]) ).
fof(f13633,plain,
meet(u,sF4) = meet(u,sF5),
inference(superposition,[],[f681,f25]) ).
fof(f13742,plain,
u = meet(u,sF5),
inference(forward_demodulation,[],[f13633,f77]) ).
fof(f13824,plain,
sF5 = join(sF5,u),
inference(superposition,[],[f72,f13742]) ).
fof(f13879,plain,
sF5 = join(u,sF5),
inference(forward_demodulation,[],[f13824,f3]) ).
fof(f14280,plain,
! [X0] : meet(a,meet(sF3,join(sF9,X0))) = meet(a,join(sF9,meet(sF3,X0))),
inference(superposition,[],[f322,f6164]) ).
fof(f14283,plain,
! [X0] : meet(a,meet(sF3,join(sF9,X0))) = meet(a,join(sF9,meet(X0,sF3))),
inference(superposition,[],[f323,f6164]) ).
fof(f18493,plain,
meet(sF3,sF9) = meet(sF5,sF9),
inference(superposition,[],[f245,f9900]) ).
fof(f18512,plain,
! [X0] : meet(a,meet(sF4,join(X0,sF9))) = meet(a,join(sF9,meet(sF4,X0))),
inference(superposition,[],[f321,f9900]) ).
fof(f18560,plain,
meet(sF3,sF9) = meet(sF9,sF5),
inference(forward_demodulation,[],[f18493,f1]) ).
fof(f18570,plain,
sF9 = meet(sF9,sF5),
inference(forward_demodulation,[],[f18560,f6164]) ).
fof(f18580,plain,
sF5 = join(sF5,sF9),
inference(superposition,[],[f72,f18570]) ).
fof(f18646,plain,
sF5 = join(sF9,sF5),
inference(forward_demodulation,[],[f18580,f3]) ).
fof(f20702,plain,
! [X0] : meet(a,meet(sF0,join(sF13,X0))) = meet(a,join(sF13,meet(sF0,X0))),
inference(superposition,[],[f322,f4705]) ).
fof(f20705,plain,
! [X0] : meet(a,meet(sF0,join(sF13,X0))) = meet(a,join(sF13,meet(X0,sF0))),
inference(superposition,[],[f323,f4705]) ).
fof(f22299,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X0,X2))) = meet(a,join(meet(join(X0,X1),X2),X0)),
inference(superposition,[],[f472,f6]) ).
fof(f22599,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X0,X2))) = meet(a,join(X0,meet(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f22299,f5600]) ).
fof(f23648,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X0,X2))) = meet(a,join(X0,meet(X2,join(X1,X0)))),
inference(superposition,[],[f456,f64]) ).
fof(f27593,plain,
meet(sF0,sF13) = meet(sF2,sF13),
inference(superposition,[],[f244,f4685]) ).
fof(f27613,plain,
! [X0] : meet(a,meet(sF1,join(X0,sF13))) = meet(a,join(sF13,meet(sF1,X0))),
inference(superposition,[],[f321,f4685]) ).
fof(f27673,plain,
meet(sF0,sF13) = meet(sF13,sF2),
inference(forward_demodulation,[],[f27593,f1]) ).
fof(f27685,plain,
sF13 = meet(sF13,sF2),
inference(forward_demodulation,[],[f27673,f4705]) ).
fof(f27694,plain,
sF2 = join(sF2,sF13),
inference(superposition,[],[f72,f27685]) ).
fof(f27772,plain,
sF2 = join(sF13,sF2),
inference(forward_demodulation,[],[f27694,f3]) ).
fof(f29308,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f770,f1]) ).
fof(f31428,plain,
join(sF2,sF5) = join(sF6,u),
inference(superposition,[],[f6032,f13879]) ).
fof(f31436,plain,
join(sF2,sF5) = join(sF6,sF9),
inference(superposition,[],[f6032,f18646]) ).
fof(f31518,plain,
sF6 = join(sF6,sF9),
inference(forward_demodulation,[],[f31436,f27]) ).
fof(f31525,plain,
join(sF2,sF5) = join(u,sF6),
inference(forward_demodulation,[],[f31428,f3]) ).
fof(f31546,plain,
sF6 = join(sF10,sF5),
inference(backward_demodulation,[],[f10217,f31518]) ).
fof(f31552,plain,
sF6 = join(u,sF6),
inference(forward_demodulation,[],[f31525,f27]) ).
fof(f31674,plain,
! [X0] : join(meet(u,X0),sF6) = meet(sF6,join(meet(u,X0),sF6)),
inference(superposition,[],[f921,f31552]) ).
fof(f31690,plain,
! [X0] : sF6 = join(meet(u,X0),sF6),
inference(forward_demodulation,[],[f31674,f64]) ).
fof(f31701,plain,
! [X0] : sF6 = join(sF6,meet(u,X0)),
inference(forward_demodulation,[],[f31690,f3]) ).
fof(f37183,plain,
meet(sF5,u) = meet(sF14,u),
inference(superposition,[],[f720,f13742]) ).
fof(f37296,plain,
meet(sF5,u) = meet(u,sF14),
inference(forward_demodulation,[],[f37183,f1]) ).
fof(f37329,plain,
meet(u,sF5) = meet(u,sF14),
inference(forward_demodulation,[],[f37296,f1]) ).
fof(f37348,plain,
u = meet(u,sF14),
inference(forward_demodulation,[],[f37329,f13742]) ).
fof(f37376,plain,
sF14 = join(sF14,u),
inference(superposition,[],[f72,f37348]) ).
fof(f37455,plain,
sF14 = join(u,sF14),
inference(forward_demodulation,[],[f37376,f3]) ).
fof(f37550,plain,
! [X0] : join(meet(u,X0),sF14) = meet(sF14,join(meet(u,X0),sF14)),
inference(superposition,[],[f921,f37455]) ).
fof(f37566,plain,
! [X0] : sF14 = join(meet(u,X0),sF14),
inference(forward_demodulation,[],[f37550,f64]) ).
fof(f38146,plain,
meet(sF2,sF13) = meet(sF10,sF13),
inference(superposition,[],[f721,f27685]) ).
fof(f38246,plain,
meet(sF13,sF2) = meet(sF10,sF13),
inference(forward_demodulation,[],[f38146,f1]) ).
fof(f38278,plain,
sF13 = meet(sF10,sF13),
inference(forward_demodulation,[],[f38246,f27685]) ).
fof(f38705,plain,
sF10 = join(sF10,sF13),
inference(superposition,[],[f5,f38278]) ).
fof(f42840,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f4,f3950]) ).
fof(f43137,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f42840,f6966]) ).
fof(f43322,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f3,f42840]) ).
fof(f43519,plain,
! [X2,X0,X1] : join(X2,meet(X0,X1)) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f43137,f6966]) ).
fof(f45779,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(meet(X2,meet(X3,X0)),meet(X1,X0)),
inference(superposition,[],[f29308,f258]) ).
fof(f45873,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(meet(X2,meet(X3,X0)),X1)),
inference(forward_demodulation,[],[f45779,f254]) ).
fof(f45947,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(X2,meet(meet(X3,X0),X1))),
inference(forward_demodulation,[],[f45873,f2]) ).
fof(f45968,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(X2,meet(X3,meet(X0,X1)))),
inference(forward_demodulation,[],[f45947,f2]) ).
fof(f48067,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(meet(X1,X0),meet(meet(X0,X1),X2)),
inference(superposition,[],[f769,f12670]) ).
fof(f48105,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X1,meet(X0,meet(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f48067,f2]) ).
fof(f48474,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X1,meet(X0,meet(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f48105,f2]) ).
fof(f48730,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f48474,f45968]) ).
fof(f48873,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f48730,f70]) ).
fof(f49214,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f48873,f1206]) ).
fof(f49790,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f49214,f1206]) ).
fof(f49938,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f49790,f4]) ).
fof(f50211,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = meet(X0,meet(X1,join(X3,X2))),
inference(superposition,[],[f2,f49790]) ).
fof(f50327,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X3,X2))) = meet(X0,meet(X1,join(X2,X3))),
inference(forward_demodulation,[],[f50211,f2]) ).
fof(f64053,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f43322,f6966]) ).
fof(f64605,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f64053,f6966]) ).
fof(f69108,plain,
! [X2,X3,X0,X1] : meet(X3,join(meet(X2,X1),X0)) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f49790,f43519]) ).
fof(f69781,plain,
join(sF14,sF10) = join(sF13,sF6),
inference(superposition,[],[f6029,f31546]) ).
fof(f69892,plain,
join(sF14,sF10) = join(sF6,sF13),
inference(forward_demodulation,[],[f69781,f3]) ).
fof(f69937,plain,
join(sF10,sF14) = join(sF6,sF13),
inference(forward_demodulation,[],[f69892,f3]) ).
fof(f75264,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X2,X1))) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f49790,f64605]) ).
fof(f81990,plain,
meet(sF2,sF13) = meet(sF6,sF13),
inference(superposition,[],[f313,f27685]) ).
fof(f82136,plain,
meet(sF13,sF2) = meet(sF6,sF13),
inference(forward_demodulation,[],[f81990,f1]) ).
fof(f82182,plain,
sF13 = meet(sF6,sF13),
inference(forward_demodulation,[],[f82136,f27685]) ).
fof(f82230,plain,
sF6 = join(sF6,sF13),
inference(superposition,[],[f5,f82182]) ).
fof(f82342,plain,
sF6 = join(sF10,sF14),
inference(backward_demodulation,[],[f69937,f82230]) ).
fof(f91523,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(X1,X2))) = meet(a,join(X0,meet(X1,join(X2,X0)))),
inference(superposition,[],[f433,f1843]) ).
fof(f91738,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X0,X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f22599,f91523]) ).
fof(f91739,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X0,X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f23648,f91523]) ).
fof(f92252,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(join(X1,X0),X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f444,f91739]) ).
fof(f93298,plain,
! [X0] : meet(a,meet(join(sF6,X0),sF6)) = meet(a,join(sF6,meet(sF13,X0))),
inference(superposition,[],[f91738,f82230]) ).
fof(f93322,plain,
! [X0] : meet(a,meet(join(sF10,X0),sF10)) = meet(a,join(sF10,meet(sF13,X0))),
inference(superposition,[],[f91738,f38705]) ).
fof(f93602,plain,
! [X0] : meet(a,meet(sF10,join(sF10,X0))) = meet(a,join(sF10,meet(sF13,X0))),
inference(forward_demodulation,[],[f93322,f48873]) ).
fof(f93624,plain,
! [X0] : meet(a,meet(sF6,join(sF6,X0))) = meet(a,join(sF6,meet(sF13,X0))),
inference(forward_demodulation,[],[f93298,f48873]) ).
fof(f94010,plain,
! [X0] : meet(a,sF10) = meet(a,join(sF10,meet(sF13,X0))),
inference(forward_demodulation,[],[f93602,f6]) ).
fof(f94026,plain,
! [X0] : meet(a,sF6) = meet(a,join(sF6,meet(sF13,X0))),
inference(forward_demodulation,[],[f93624,f6]) ).
fof(f94789,plain,
! [X0] : meet(a,join(sF13,meet(sF0,X0))) = meet(a,join(sF13,meet(X0,y))),
inference(superposition,[],[f92252,f2344]) ).
fof(f94799,plain,
! [X0] : meet(a,join(sF13,meet(sF1,X0))) = meet(a,join(sF13,meet(X0,z))),
inference(superposition,[],[f92252,f2589]) ).
fof(f94822,plain,
! [X0] : meet(a,join(sF9,meet(sF3,X0))) = meet(a,join(sF9,meet(X0,w))),
inference(superposition,[],[f92252,f6137]) ).
fof(f94832,plain,
! [X0] : meet(a,join(sF9,meet(sF4,X0))) = meet(a,join(sF9,meet(X0,v))),
inference(superposition,[],[f92252,f5680]) ).
fof(f95225,plain,
! [X0] : meet(a,meet(sF4,join(X0,sF9))) = meet(a,join(sF9,meet(X0,v))),
inference(backward_demodulation,[],[f18512,f94832]) ).
fof(f95242,plain,
! [X0] : meet(a,meet(sF3,join(sF9,X0))) = meet(a,join(sF9,meet(X0,w))),
inference(backward_demodulation,[],[f14280,f94822]) ).
fof(f95278,plain,
! [X0] : meet(a,meet(sF1,join(X0,sF13))) = meet(a,join(sF13,meet(X0,z))),
inference(backward_demodulation,[],[f27613,f94799]) ).
fof(f95296,plain,
! [X0] : meet(a,meet(sF0,join(sF13,X0))) = meet(a,join(sF13,meet(X0,y))),
inference(backward_demodulation,[],[f20702,f94789]) ).
fof(f95513,plain,
! [X0] : meet(a,join(sF9,meet(X0,sF3))) = meet(a,join(sF9,meet(X0,w))),
inference(backward_demodulation,[],[f14283,f95242]) ).
fof(f95534,plain,
! [X0] : meet(a,join(sF13,meet(X0,sF0))) = meet(a,join(sF13,meet(X0,y))),
inference(backward_demodulation,[],[f20705,f95296]) ).
fof(f108899,plain,
meet(a,join(sF13,sF2)) = meet(a,meet(sF1,join(sF13,sF0))),
inference(superposition,[],[f552,f4685]) ).
fof(f109131,plain,
meet(a,join(sF13,sF2)) = meet(a,meet(sF1,join(sF0,sF13))),
inference(forward_demodulation,[],[f108899,f50327]) ).
fof(f109229,plain,
meet(a,join(sF13,sF2)) = meet(a,join(sF13,meet(sF0,z))),
inference(forward_demodulation,[],[f109131,f95278]) ).
fof(f109291,plain,
meet(a,join(sF13,sF2)) = meet(a,join(sF13,meet(z,sF0))),
inference(forward_demodulation,[],[f109229,f75264]) ).
fof(f109330,plain,
meet(a,join(sF13,sF2)) = meet(a,join(sF13,meet(z,y))),
inference(forward_demodulation,[],[f109291,f95534]) ).
fof(f109353,plain,
meet(a,join(sF13,sF2)) = meet(a,join(meet(y,z),sF13)),
inference(forward_demodulation,[],[f109330,f69108]) ).
fof(f109366,plain,
meet(a,sF13) = meet(a,join(sF13,sF2)),
inference(forward_demodulation,[],[f109353,f644]) ).
fof(f109374,plain,
meet(a,sF2) = meet(a,sF13),
inference(forward_demodulation,[],[f109366,f27772]) ).
fof(f109396,plain,
! [X0] : meet(a,join(sF2,X0)) = join(meet(a,sF13),meet(a,X0)),
inference(superposition,[],[f315,f109374]) ).
fof(f109430,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(X1,sF2)))) = meet(a,join(X0,join(meet(a,X1),meet(a,sF13)))),
inference(superposition,[],[f433,f109374]) ).
fof(f109514,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(X1,sF2)))) = meet(a,join(X0,meet(a,join(X1,sF13)))),
inference(forward_demodulation,[],[f109430,f433]) ).
fof(f109574,plain,
! [X0] : meet(a,join(sF13,X0)) = meet(a,join(sF2,X0)),
inference(forward_demodulation,[],[f109396,f315]) ).
fof(f109609,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(X1,sF2)))) = meet(a,join(X0,join(X1,sF13))),
inference(forward_demodulation,[],[f109514,f11664]) ).
fof(f109818,plain,
! [X0,X1] : meet(a,join(X0,join(X1,sF13))) = meet(a,join(X0,join(X1,sF2))),
inference(forward_demodulation,[],[f109609,f11664]) ).
fof(f110688,plain,
meet(a,join(sF9,sF5)) = meet(a,meet(sF4,join(sF9,sF3))),
inference(superposition,[],[f553,f9900]) ).
fof(f110920,plain,
meet(a,join(sF9,sF5)) = meet(a,meet(sF4,join(sF3,sF9))),
inference(forward_demodulation,[],[f110688,f50327]) ).
fof(f111017,plain,
meet(a,join(sF9,sF5)) = meet(a,join(sF9,meet(sF3,v))),
inference(forward_demodulation,[],[f110920,f95225]) ).
fof(f111080,plain,
meet(a,join(sF9,sF5)) = meet(a,join(sF9,meet(v,sF3))),
inference(forward_demodulation,[],[f111017,f75264]) ).
fof(f111119,plain,
meet(a,join(sF9,sF5)) = meet(a,join(sF9,meet(v,w))),
inference(forward_demodulation,[],[f111080,f95513]) ).
fof(f111142,plain,
meet(a,join(sF9,sF5)) = meet(a,join(sF9,meet(w,v))),
inference(forward_demodulation,[],[f111119,f75264]) ).
fof(f111155,plain,
meet(a,join(sF9,sF8)) = meet(a,join(sF9,sF5)),
inference(forward_demodulation,[],[f111142,f31]) ).
fof(f111163,plain,
meet(a,sF5) = meet(a,join(sF9,sF8)),
inference(forward_demodulation,[],[f111155,f18646]) ).
fof(f111170,plain,
meet(a,sF5) = meet(a,join(sF8,sF9)),
inference(forward_demodulation,[],[f111163,f49790]) ).
fof(f111175,plain,
meet(a,sF5) = meet(a,sF9),
inference(forward_demodulation,[],[f111170,f647]) ).
fof(f111223,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(sF5,X1)))) = meet(a,join(X0,join(meet(a,sF9),meet(a,X1)))),
inference(superposition,[],[f433,f111175]) ).
fof(f111309,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(sF5,X1)))) = meet(a,join(X0,meet(a,join(sF9,X1)))),
inference(forward_demodulation,[],[f111223,f433]) ).
fof(f111404,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(sF5,X1)))) = meet(a,join(X0,join(sF9,X1))),
inference(forward_demodulation,[],[f111309,f11664]) ).
fof(f111614,plain,
! [X0,X1] : meet(a,join(X0,join(sF9,X1))) = meet(a,join(X0,join(sF5,X1))),
inference(forward_demodulation,[],[f111404,f11664]) ).
fof(f113122,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF2,join(sF5,X0))),
inference(superposition,[],[f5866,f6032]) ).
fof(f113127,plain,
! [X0] : meet(a,join(sF10,X0)) = meet(a,join(sF9,join(X0,sF2))),
inference(superposition,[],[f5866,f154]) ).
fof(f113132,plain,
! [X0] : meet(a,join(sF14,X0)) = meet(a,join(sF13,join(sF5,X0))),
inference(superposition,[],[f5866,f6029]) ).
fof(f113499,plain,
! [X0] : meet(a,join(sF14,X0)) = meet(a,join(sF13,join(sF9,X0))),
inference(forward_demodulation,[],[f113132,f111614]) ).
fof(f113502,plain,
! [X0] : meet(a,join(sF10,X0)) = meet(a,join(sF9,join(X0,sF13))),
inference(forward_demodulation,[],[f113127,f109818]) ).
fof(f113507,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF13,join(sF5,X0))),
inference(forward_demodulation,[],[f113122,f109574]) ).
fof(f113729,plain,
! [X0] : meet(a,join(sF14,X0)) = meet(a,join(sF9,join(X0,sF13))),
inference(forward_demodulation,[],[f113499,f49938]) ).
fof(f113731,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF13,join(sF9,X0))),
inference(forward_demodulation,[],[f113507,f111614]) ).
fof(f113868,plain,
! [X0] : meet(a,join(sF14,X0)) = meet(a,join(sF10,X0)),
inference(forward_demodulation,[],[f113729,f113502]) ).
fof(f113870,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF9,join(X0,sF13))),
inference(forward_demodulation,[],[f113731,f49938]) ).
fof(f114074,plain,
! [X0] : meet(a,join(sF10,X0)) = meet(a,join(sF6,X0)),
inference(backward_demodulation,[],[f113502,f113870]) ).
fof(f114301,plain,
! [X0] : meet(a,join(sF14,X0)) = meet(a,join(sF6,X0)),
inference(backward_demodulation,[],[f113868,f114074]) ).
fof(f114412,plain,
! [X0] : meet(a,sF10) = meet(a,join(sF6,meet(sF13,X0))),
inference(backward_demodulation,[],[f94010,f114074]) ).
fof(f114554,plain,
meet(a,sF6) = meet(a,sF10),
inference(forward_demodulation,[],[f114412,f94026]) ).
fof(f115704,plain,
! [X0] : meet(a,join(X0,sF10)) = join(meet(a,X0),meet(a,sF6)),
inference(superposition,[],[f315,f114554]) ).
fof(f115926,plain,
! [X0] : meet(a,join(X0,sF10)) = meet(a,join(X0,sF6)),
inference(forward_demodulation,[],[f115704,f315]) ).
fof(f123123,plain,
! [X0] : meet(a,sF14) = meet(a,join(sF14,meet(u,X0))),
inference(superposition,[],[f3170,f37566]) ).
fof(f123163,plain,
! [X0] : meet(a,sF14) = meet(a,join(sF6,meet(u,X0))),
inference(forward_demodulation,[],[f123123,f114301]) ).
fof(f123192,plain,
meet(a,sF6) = meet(a,sF14),
inference(forward_demodulation,[],[f123163,f31701]) ).
fof(f123259,plain,
! [X0] : meet(a,join(X0,sF14)) = join(meet(a,X0),meet(a,sF6)),
inference(superposition,[],[f315,f123192]) ).
fof(f123483,plain,
! [X0] : meet(a,join(X0,sF14)) = meet(a,join(X0,sF6)),
inference(forward_demodulation,[],[f123259,f315]) ).
fof(f124081,plain,
( meet(t,sF6) = join(sF11,sF15)
| meet(a,join(t,sF14)) != meet(a,join(t,sF10)) ),
inference(forward_demodulation,[],[f13286,f82342]) ).
fof(f124085,plain,
( meet(t,sF6) = sF16
| meet(a,join(t,sF14)) != meet(a,join(t,sF10)) ),
inference(forward_demodulation,[],[f124081,f47]) ).
fof(f124090,plain,
( sF7 = sF16
| meet(a,join(t,sF14)) != meet(a,join(t,sF10)) ),
inference(forward_demodulation,[],[f124085,f29]) ).
fof(f124093,plain,
meet(a,join(t,sF14)) != meet(a,join(t,sF10)),
inference(forward_subsumption_resolution,[],[f124090,f48]) ).
fof(f124096,plain,
meet(a,join(t,sF6)) != meet(a,join(t,sF14)),
inference(forward_demodulation,[],[f124093,f115926]) ).
fof(f124099,plain,
$false,
inference(forward_subsumption_resolution,[],[f124096,f123483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT398-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n003.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 15:16:41 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.15/2.72 % (682819)Input is clausal, will run a generic CNF schedule.
% 13.15/2.72 % (682825)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=557968530:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 13.15/2.72 % (682828)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3285533348:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 13.15/2.72 % (682827)lrs+10_1_sil=8000:sp=occurrence:random_seed=403855556:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 13.15/2.72 % (682826)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2269242855:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 13.15/2.72 % (682824)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=826013438:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 13.15/2.72 % (682829)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1859311088:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 13.15/2.72 % (682830)dis-21_1_sil=8000:lcm=predicate:random_seed=3496914949:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 13.15/2.72 % (682830)Refutation not found, incomplete strategy
% 13.15/2.72 % (682830)------------------------------
% 13.15/2.72 % (682830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.72 % (682830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.72 % (682830)CaDiCaL version: 2.1.3
% 13.15/2.72 % (682830)Termination reason: Refutation not found, incomplete strategy
% 13.15/2.72 % (682830)Time elapsed: 0.001 s
% 13.15/2.72 % (682830)Peak memory usage: 88 MB
% 13.15/2.72 % (682830)Instructions burned: 1 (million)
% 13.15/2.72 % (682827)Instruction limit reached!
% 13.15/2.72 % (682827)------------------------------
% 13.15/2.72 % (682827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.72 % (682827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.72 % (682827)CaDiCaL version: 2.1.3
% 13.15/2.72 % (682827)Termination reason: Instruction limit
% 13.15/2.72 % (682827)Termination phase: Saturation
% 13.15/2.72 % (682827)Time elapsed: 0.063 s
% 13.15/2.72 % (682827)Peak memory usage: 88 MB
% 13.15/2.72 % (682827)Instructions burned: 108 (million)
% 13.15/2.72 % (682828)Instruction limit reached!
% 13.15/2.72 % (682828)------------------------------
% 13.15/2.72 % (682828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.72 % (682828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.72 % (682828)CaDiCaL version: 2.1.3
% 13.15/2.72 % (682828)Termination reason: Instruction limit
% 13.15/2.72 % (682828)Termination phase: Saturation
% 13.15/2.72 % (682828)Time elapsed: 0.066 s
% 13.15/2.72 % (682828)Peak memory usage: 88 MB
% 13.15/2.72 % (682828)Instructions burned: 115 (million)
% 13.15/2.72 % (682829)Instruction limit reached!
% 13.15/2.72 % (682829)------------------------------
% 13.15/2.72 % (682829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.72 % (682829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.72 % (682829)CaDiCaL version: 2.1.3
% 13.15/2.72 % (682829)Termination reason: Instruction limit
% 13.15/2.72 % (682829)Termination phase: Saturation
% 13.15/2.72 % (682829)Time elapsed: 0.103 s
% 13.15/2.72 % (682829)Peak memory usage: 89 MB
% 13.15/2.72 % (682829)Instructions burned: 181 (million)
% 13.15/2.72 % (682838)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3892696077:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 13.15/2.72 % (682839)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3475078584:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 13.15/2.72 % (682838)Refutation not found, incomplete strategy
% 13.15/2.72 % (682838)------------------------------
% 13.15/2.72 % (682838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.15/2.72 % (682838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.15/2.72 % (682838)CaDiCaL version: 2.1.3
% 13.15/2.72 % (682838)Termination reason: Refutation not found, incomplete strategy
% 23.53/4.14 % (682838)Time elapsed: 0.002 s
% 23.53/4.14 % (682838)Peak memory usage: 88 MB
% 23.53/4.14 % (682838)Instructions burned: 1 (million)
% 23.53/4.14 % (682839)Refutation not found, incomplete strategy
% 23.53/4.14 % (682839)------------------------------
% 23.53/4.14 % (682839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.53/4.14 % (682839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.53/4.14 % (682839)CaDiCaL version: 2.1.3
% 23.53/4.14 % (682839)Termination reason: Refutation not found, incomplete strategy
% 23.53/4.14 % (682839)Time elapsed: 0.002 s
% 23.53/4.14 % (682839)Peak memory usage: 88 MB
% 23.53/4.14 % (682839)Instructions burned: 2 (million)
% 23.53/4.14 % (682830)------------------------------
% 23.53/4.14 % (682830)------------------------------
% 23.53/4.14 % (682840)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3997098080:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 23.53/4.14 % (682840)Refutation not found, incomplete strategy
% 23.53/4.14 % (682840)------------------------------
% 23.53/4.14 % (682840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.53/4.14 % (682840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.53/4.14 % (682840)CaDiCaL version: 2.1.3
% 23.53/4.14 % (682840)Termination reason: Refutation not found, incomplete strategy
% 23.53/4.14 % (682840)Time elapsed: 0.001 s
% 23.53/4.14 % (682840)Peak memory usage: 88 MB
% 23.53/4.14 % (682840)Instructions burned: 1 (million)
% 23.53/4.14 % (682843)lrs+10_64_to=lpo:sil=8000:random_seed=2093810352:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 23.53/4.14 % (682839)------------------------------
% 23.53/4.14 % (682839)------------------------------
% 23.53/4.14 % (682838)------------------------------
% 23.53/4.14 % (682838)------------------------------
% 23.53/4.14 % (682843)Instruction limit reached!
% 23.53/4.14 % (682843)------------------------------
% 23.53/4.14 % (682843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.53/4.14 % (682843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.53/4.14 % (682843)CaDiCaL version: 2.1.3
% 23.53/4.14 % (682843)Termination reason: Instruction limit
% 23.53/4.14 % (682843)Termination phase: Saturation
% 23.53/4.14 % (682843)Time elapsed: 0.072 s
% 23.53/4.14 % (682843)Peak memory usage: 88 MB
% 23.53/4.14 % (682843)Instructions burned: 127 (million)
% 23.53/4.14 % (682840)------------------------------
% 23.53/4.14 % (682840)------------------------------
% 23.53/4.14 % (682846)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3006861294:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 23.53/4.14 % (682847)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3388252824:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 23.53/4.14 % (682848)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2348967317:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 23.53/4.14 % (682849)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2346827905:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 23.53/4.14 % (682849)Instruction limit reached!
% 23.53/4.14 % (682849)------------------------------
% 23.53/4.14 % (682849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.53/4.14 % (682849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.53/4.14 % (682849)CaDiCaL version: 2.1.3
% 23.53/4.14 % (682849)Termination reason: Instruction limit
% 23.53/4.14 % (682849)Termination phase: Saturation
% 23.53/4.14 % (682849)Time elapsed: 0.056 s
% 23.53/4.14 % (682849)Peak memory usage: 89 MB
% 23.53/4.14 % (682849)Instructions burned: 107 (million)
% 23.53/4.14 % (682847)Instruction limit reached!
% 23.53/4.14 % (682847)------------------------------
% 23.53/4.14 % (682847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.53/4.14 % (682847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.53/4.14 % (682847)CaDiCaL version: 2.1.3
% 23.53/4.14 % (682847)Termination reason: Instruction limit
% 23.53/4.14 % (682847)Termination phase: Saturation
% 23.53/4.14 % (682847)Time elapsed: 0.091 s
% 23.53/4.14 % (682847)Peak memory usage: 90 MB
% 23.53/4.14 % (682847)Instructions burned: 157 (million)
% 23.53/4.14 % (682846)Instruction limit reached!
% 23.53/4.14 % (682846)------------------------------
% 23.53/4.14 % (682846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682846)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682846)Termination reason: Instruction limit
% 36.93/6.08 % (682846)Termination phase: Saturation
% 36.93/6.08 % (682846)Time elapsed: 0.113 s
% 36.93/6.08 % (682846)Peak memory usage: 89 MB
% 36.93/6.08 % (682846)Instructions burned: 194 (million)
% 36.93/6.08 % (682855)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3296914601:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 36.93/6.08 % (682854)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2960842326:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 36.93/6.08 % (682854)Refutation not found, incomplete strategy
% 36.93/6.08 % (682854)------------------------------
% 36.93/6.08 % (682854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682854)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682854)Termination reason: Refutation not found, incomplete strategy
% 36.93/6.08 % (682854)Time elapsed: 0.002 s
% 36.93/6.08 % (682854)Peak memory usage: 88 MB
% 36.93/6.08 % (682854)Instructions burned: 2 (million)
% 36.93/6.08 % (682856)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2251884767:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 36.93/6.08 % (682855)Instruction limit reached!
% 36.93/6.08 % (682855)------------------------------
% 36.93/6.08 % (682855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682855)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682855)Termination reason: Instruction limit
% 36.93/6.08 % (682855)Termination phase: Saturation
% 36.93/6.08 % (682855)Time elapsed: 0.138 s
% 36.93/6.08 % (682855)Peak memory usage: 90 MB
% 36.93/6.08 % (682855)Instructions burned: 243 (million)
% 36.93/6.08 % (682854)------------------------------
% 36.93/6.08 % (682854)------------------------------
% 36.93/6.08 % (682860)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=939044868:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 36.93/6.08 % (682860)Instruction limit reached!
% 36.93/6.08 % (682860)------------------------------
% 36.93/6.08 % (682860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682860)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682860)Termination reason: Instruction limit
% 36.93/6.08 % (682860)Termination phase: Saturation
% 36.93/6.08 % (682860)Time elapsed: 0.077 s
% 36.93/6.08 % (682860)Peak memory usage: 89 MB
% 36.93/6.08 % (682860)Instructions burned: 134 (million)
% 36.93/6.08 % (682861)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2913113920:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 36.93/6.08 % (682863)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=290462133:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 36.93/6.08 % (682863)Instruction limit reached!
% 36.93/6.08 % (682863)------------------------------
% 36.93/6.08 % (682863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682863)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682863)Termination reason: Instruction limit
% 36.93/6.08 % (682863)Termination phase: Saturation
% 36.93/6.08 % (682863)Time elapsed: 0.116 s
% 36.93/6.08 % (682863)Peak memory usage: 90 MB
% 36.93/6.08 % (682863)Instructions burned: 191 (million)
% 36.93/6.08 % (682861)Instruction limit reached!
% 36.93/6.08 % (682861)------------------------------
% 36.93/6.08 % (682861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.93/6.08 % (682861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.93/6.08 % (682861)CaDiCaL version: 2.1.3
% 36.93/6.08 % (682861)Termination reason: Instruction limit
% 36.93/6.08 % (682861)Termination phase: Saturation
% 36.93/6.08 % (682861)Time elapsed: 0.312 s
% 36.93/6.08 % (682861)Peak memory usage: 93 MB
% 36.93/6.08 % (682861)Instructions burned: 499 (million)
% 36.93/6.08 % (682866)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4081741846:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 63.66/9.83 % (682867)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4158780619:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 63.66/9.83 % (682867)Instruction limit reached!
% 63.66/9.83 % (682867)------------------------------
% 63.66/9.83 % (682867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.66/9.83 % (682867)CaDiCaL version: 2.1.3
% 63.66/9.83 % (682867)Termination reason: Instruction limit
% 63.66/9.83 % (682867)Termination phase: Saturation
% 63.66/9.83 % (682867)Time elapsed: 0.090 s
% 63.66/9.83 % (682867)Peak memory usage: 89 MB
% 63.66/9.83 % (682867)Instructions burned: 157 (million)
% 63.66/9.83 % (682866)Instruction limit reached!
% 63.66/9.83 % (682866)------------------------------
% 63.66/9.83 % (682866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.66/9.83 % (682866)CaDiCaL version: 2.1.3
% 63.66/9.83 % (682866)Termination reason: Instruction limit
% 63.66/9.83 % (682866)Termination phase: Saturation
% 63.66/9.83 % (682866)Time elapsed: 0.149 s
% 63.66/9.83 % (682866)Peak memory usage: 91 MB
% 63.66/9.83 % (682866)Instructions burned: 265 (million)
% 63.66/9.83 % (682870)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=912025039:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 63.66/9.83 % (682871)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=150293018:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 63.66/9.83 % (682871)Instruction limit reached!
% 63.66/9.83 % (682871)------------------------------
% 63.66/9.83 % (682871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.66/9.83 % (682871)CaDiCaL version: 2.1.3
% 63.66/9.83 % (682871)Termination reason: Instruction limit
% 63.66/9.83 % (682871)Termination phase: Saturation
% 63.66/9.83 % (682871)Time elapsed: 0.286 s
% 63.66/9.83 % (682871)Peak memory usage: 93 MB
% 63.66/9.83 % (682871)Instructions burned: 538 (million)
% 63.66/9.83 % (682874)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2526469259:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 63.66/9.83 % (682874)Instruction limit reached!
% 63.66/9.83 % (682874)------------------------------
% 63.66/9.83 % (682874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.66/9.83 % (682874)CaDiCaL version: 2.1.3
% 63.66/9.83 % (682874)Termination reason: Instruction limit
% 63.66/9.83 % (682874)Termination phase: Saturation
% 63.66/9.83 % (682874)Time elapsed: 0.100 s
% 63.66/9.83 % (682874)Peak memory usage: 89 MB
% 63.66/9.83 % (682874)Instructions burned: 180 (million)
% 63.66/9.83 % (682848)Instruction limit reached!
% 63.66/9.83 % (682848)------------------------------
% 63.66/9.83 % (682848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.66/9.83 % (682848)CaDiCaL version: 2.1.3
% 63.66/9.83 % (682848)Termination reason: Instruction limit
% 63.66/9.83 % (682848)Termination phase: Saturation
% 63.66/9.83 % (682848)Time elapsed: 2.042 s
% 63.66/9.83 % (682848)Peak memory usage: 150 MB
% 63.66/9.83 % (682848)Instructions burned: 3395 (million)
% 63.66/9.83 % (682876)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=2241057877:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 63.66/9.83 % (682877)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=506321197:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 63.66/9.83 % (682877)Instruction limit reached!
% 63.66/9.83 % (682877)------------------------------
% 63.66/9.83 % (682877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.66/9.83 % (682877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682877)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682877)Termination reason: Instruction limit
% 69.55/10.78 % (682877)Termination phase: Saturation
% 69.55/10.78 % (682877)Time elapsed: 0.253 s
% 69.55/10.78 % (682877)Peak memory usage: 95 MB
% 69.55/10.78 % (682877)Instructions burned: 412 (million)
% 69.55/10.78 % (682880)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=269441533:s2pl=no:i=8478:s2at=4:nm=6_2967 on theBenchmark for (2967ds/8478Mi)
% 69.55/10.78 % (682856)Instruction limit reached!
% 69.55/10.78 % (682856)------------------------------
% 69.55/10.78 % (682856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682856)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682856)Termination reason: Instruction limit
% 69.55/10.78 % (682856)Termination phase: Saturation
% 69.55/10.78 % (682856)Time elapsed: 3.060 s
% 69.55/10.78 % (682856)Peak memory usage: 169 MB
% 69.55/10.78 % (682856)Instructions burned: 5209 (million)
% 69.55/10.78 % (682870)Instruction limit reached!
% 69.55/10.78 % (682870)------------------------------
% 69.55/10.78 % (682870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682870)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682870)Termination reason: Instruction limit
% 69.55/10.78 % (682870)Termination phase: Saturation
% 69.55/10.78 % (682870)Time elapsed: 1.970 s
% 69.55/10.78 % (682870)Peak memory usage: 147 MB
% 69.55/10.78 % (682870)Instructions burned: 3257 (million)
% 69.55/10.78 % (682883)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2819268307:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi)
% 69.55/10.78 % (682882)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3126174026:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi)
% 69.55/10.78 % (682883)Refutation not found, incomplete strategy
% 69.55/10.78 % (682883)------------------------------
% 69.55/10.78 % (682883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682883)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682883)Termination reason: Refutation not found, incomplete strategy
% 69.55/10.78 % (682883)Time elapsed: 0.002 s
% 69.55/10.78 % (682883)Peak memory usage: 88 MB
% 69.55/10.78 % (682883)Instructions burned: 1 (million)
% 69.55/10.78 % (682882)Refutation not found, incomplete strategy
% 69.55/10.78 % (682882)------------------------------
% 69.55/10.78 % (682882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682882)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682882)Termination reason: Refutation not found, incomplete strategy
% 69.55/10.78 % (682882)Time elapsed: 0.002 s
% 69.55/10.78 % (682882)Peak memory usage: 88 MB
% 69.55/10.78 % (682882)Instructions burned: 1 (million)
% 69.55/10.78 % (682883)------------------------------
% 69.55/10.78 % (682883)------------------------------
% 69.55/10.78 % (682882)------------------------------
% 69.55/10.78 % (682882)------------------------------
% 69.55/10.78 % (682886)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3142461202:i=598:bs=on:bd=preordered:av=off:ss=axioms_2954 on theBenchmark for (2954ds/598Mi)
% 69.55/10.78 % (682887)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3552649619:i=2989:sd=3:ss=axioms:sgt=60_2954 on theBenchmark for (2954ds/2989Mi)
% 69.55/10.78 % (682886)Instruction limit reached!
% 69.55/10.78 % (682886)------------------------------
% 69.55/10.78 % (682886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682886)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682886)Termination reason: Instruction limit
% 69.55/10.78 % (682886)Termination phase: Saturation
% 69.55/10.78 % (682886)Time elapsed: 0.368 s
% 69.55/10.78 % (682886)Peak memory usage: 94 MB
% 69.55/10.78 % (682886)Instructions burned: 599 (million)
% 69.55/10.78 % (682890)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3301653583:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2949 on theBenchmark for (2949ds/1997Mi)
% 69.55/10.78 % (682887)Instruction limit reached!
% 69.55/10.78 % (682887)------------------------------
% 69.55/10.78 % (682887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682887)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682887)Termination reason: Instruction limit
% 69.55/10.78 % (682887)Termination phase: Saturation
% 69.55/10.78 % (682887)Time elapsed: 1.700 s
% 69.55/10.78 % (682887)Peak memory usage: 147 MB
% 69.55/10.78 % (682887)Instructions burned: 2989 (million)
% 69.55/10.78 % (682890)Instruction limit reached!
% 69.55/10.78 % (682890)------------------------------
% 69.55/10.78 % (682890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682890)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682890)Termination reason: Instruction limit
% 69.55/10.78 % (682890)Termination phase: Saturation
% 69.55/10.78 % (682890)Time elapsed: 1.206 s
% 69.55/10.78 % (682890)Peak memory usage: 138 MB
% 69.55/10.78 % (682890)Instructions burned: 1998 (million)
% 69.55/10.78 % (682892)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3491056361:i=2088:bd=preordered:av=off_2935 on theBenchmark for (2935ds/2088Mi)
% 69.55/10.78 % (682893)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3342880189:i=1098:nicw=on_2935 on theBenchmark for (2935ds/1098Mi)
% 69.55/10.78 % (682893)Instruction limit reached!
% 69.55/10.78 % (682893)------------------------------
% 69.55/10.78 % (682893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682893)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682893)Termination reason: Instruction limit
% 69.55/10.78 % (682893)Termination phase: Saturation
% 69.55/10.78 % (682893)Time elapsed: 0.635 s
% 69.55/10.78 % (682893)Peak memory usage: 99 MB
% 69.55/10.78 % (682893)Instructions burned: 1098 (million)
% 69.55/10.78 % (682896)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3844381423:i=433:bd=preordered_2927 on theBenchmark for (2927ds/433Mi)
% 69.55/10.78 % (682896)Refutation not found, incomplete strategy
% 69.55/10.78 % (682896)------------------------------
% 69.55/10.78 % (682896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682896)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682896)Termination reason: Refutation not found, incomplete strategy
% 69.55/10.78 % (682896)Time elapsed: 0.002 s
% 69.55/10.78 % (682896)Peak memory usage: 88 MB
% 69.55/10.78 % (682896)Instructions burned: 1 (million)
% 69.55/10.78 % (682896)------------------------------
% 69.55/10.78 % (682896)------------------------------
% 69.55/10.78 % (682898)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4266989696:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2923 on theBenchmark for (2923ds/2942Mi)
% 69.55/10.78 % (682892)Instruction limit reached!
% 69.55/10.78 % (682892)------------------------------
% 69.55/10.78 % (682892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682892)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682892)Termination reason: Instruction limit
% 69.55/10.78 % (682892)Termination phase: Saturation
% 69.55/10.78 % (682892)Time elapsed: 1.284 s
% 69.55/10.78 % (682892)Peak memory usage: 138 MB
% 69.55/10.78 % (682892)Instructions burned: 2089 (million)
% 69.55/10.78 % (682900)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2108916202:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2921 on theBenchmark for (2921ds/6922Mi)
% 69.55/10.78 % (682880)Instruction limit reached!
% 69.55/10.78 % (682880)------------------------------
% 69.55/10.78 % (682880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682880)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682880)Termination reason: Instruction limit
% 69.55/10.78 % (682880)Termination phase: Saturation
% 69.55/10.78 % (682880)Time elapsed: 5.514 s
% 69.55/10.78 % (682880)Peak memory usage: 175 MB
% 69.55/10.78 % (682880)Instructions burned: 8479 (million)
% 69.55/10.78 % (682876)Instruction limit reached!
% 69.55/10.78 % (682876)------------------------------
% 69.55/10.78 % (682876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682876)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682876)Termination reason: Instruction limit
% 69.55/10.78 % (682876)Termination phase: Saturation
% 69.55/10.78 % (682876)Time elapsed: 6.174 s
% 69.55/10.78 % (682876)Peak memory usage: 209 MB
% 69.55/10.78 % (682876)Instructions burned: 10307 (million)
% 69.55/10.78 % (682902)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=3951739940:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2910 on theBenchmark for (2910ds/596Mi)
% 69.55/10.78 % (682902)Refutation not found, incomplete strategy
% 69.55/10.78 % (682902)------------------------------
% 69.55/10.78 % (682902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682902)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682902)Termination reason: Refutation not found, incomplete strategy
% 69.55/10.78 % (682902)Time elapsed: 0.002 s
% 69.55/10.78 % (682902)Peak memory usage: 88 MB
% 69.55/10.78 % (682902)Instructions burned: 2 (million)
% 69.55/10.78 % (682903)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=4211027399:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2909 on theBenchmark for (2909ds/4123Mi)
% 69.55/10.78 % (682902)------------------------------
% 69.55/10.78 % (682902)------------------------------
% 69.55/10.78 % (682906)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3530257910:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2906 on theBenchmark for (2906ds/16411Mi)
% 69.55/10.78 % (682826)First to succeed.
% 69.55/10.78 % (682826)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-682819"
% 69.55/10.78 % (682898)Instruction limit reached!
% 69.55/10.78 % (682898)------------------------------
% 69.55/10.78 % (682898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 69.55/10.78 % (682898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 69.55/10.78 % (682898)CaDiCaL version: 2.1.3
% 69.55/10.78 % (682898)Termination reason: Instruction limit
% 69.55/10.78 % (682898)Termination phase: Saturation
% 69.55/10.78 % (682898)Time elapsed: 1.945 s
% 69.55/10.78 % (682898)Peak memory usage: 144 MB
% 69.55/10.78 % (682898)Instructions burned: 2942 (million)
% 69.55/10.78 % (682826)Refutation found. Thanks to Tanya!
% 69.55/10.78 % SZS status Unsatisfiable for theBenchmark
% 69.55/10.78 % SZS output start Proof for theBenchmark
% See solution above
% 70.65/10.98 % (682826)------------------------------
% 70.65/10.98 % (682826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.65/10.98 % (682826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.65/10.98 % (682826)CaDiCaL version: 2.1.3
% 70.65/10.98 % (682826)Termination reason: Refutation
% 70.65/10.98 % (682826)Time elapsed: 9.444 s
% 70.65/10.98 % (682826)Peak memory usage: 252 MB
% 70.65/10.98 % (682826)Instructions burned: 15567 (million)
% 70.65/10.98 % (682826)------------------------------
% 70.65/10.98 % (682826)------------------------------
% 70.65/10.98 % (682819)Success in time 9.913 s
% 70.65/10.98 % Vampire exiting
%------------------------------------------------------------------------------