%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT398-2 : 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 : n008.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 48.06s 12.06s
% Output : Refutation 79.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 28
% Syntax : Number of formulae : 315 ( 310 unt; 17 def)
% Number of atoms : 320 ( 319 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 12 ( 7 ~; 5 |; 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 : 395 ( 395 !; 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(f11,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(f12,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(f13,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(f14,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,[],[f11,f7,f8]) ).
fof(f15,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,[],[f12,f7,f7,f7,f8]) ).
fof(f16,definition,
sF0 = join(x,y),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f17,plain,
join(x,y) = sF0,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF1 = join(x,z),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f19,plain,
join(x,z) = sF1,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF2 = meet(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f21,plain,
meet(sF0,sF1) = sF2,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF3 = join(u,w),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f23,plain,
join(u,w) = sF3,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF4 = join(u,v),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f25,plain,
join(u,v) = sF4,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF5 = meet(sF3,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f27,plain,
meet(sF3,sF4) = sF5,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF6 = join(sF2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f29,plain,
join(sF2,sF5) = sF6,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF7 = meet(t,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f31,plain,
meet(t,sF6) = sF7,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF8 = meet(w,v),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f33,plain,
meet(w,v) = sF8,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF9 = join(u,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f35,plain,
join(u,sF8) = sF9,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF10 = join(sF2,sF9),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f37,plain,
join(sF2,sF9) = sF10,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF11 = meet(t,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f39,plain,
meet(t,sF10) = sF11,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF12 = meet(y,z),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f41,plain,
meet(y,z) = sF12,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF13 = join(x,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f43,plain,
join(x,sF12) = sF13,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF14 = join(sF5,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f45,plain,
join(sF5,sF13) = sF14,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF15 = meet(t,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f47,plain,
meet(t,sF14) = sF15,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF16 = join(sF11,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f49,plain,
join(sF11,sF15) = sF16,
inference(reorient_equations,[],[f48]) ).
fof(f50,plain,
sF7 != sF16,
inference(definition_folding,[],[f13,f49,f47,f45,f43,f41,f27,f25,f23,f39,f37,f35,f33,f21,f19,f17,f31,f29,f27,f25,f23,f21,f19,f17]) ).
fof(f51,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,[],[f14,f2]) ).
fof(f52,plain,
sF0 = join(y,x),
inference(forward_demodulation,[],[f17,f3]) ).
fof(f53,plain,
sF1 = join(z,x),
inference(forward_demodulation,[],[f19,f3]) ).
fof(f54,plain,
sF3 = join(w,u),
inference(forward_demodulation,[],[f23,f3]) ).
fof(f55,plain,
sF4 = join(v,u),
inference(forward_demodulation,[],[f25,f3]) ).
fof(f56,plain,
sF10 = join(sF9,sF2),
inference(forward_demodulation,[],[f37,f3]) ).
fof(f57,plain,
join(x,meet(y,z)) = sF13,
inference(forward_demodulation,[],[f43,f41]) ).
fof(f58,plain,
sF14 = join(sF13,sF5),
inference(forward_demodulation,[],[f45,f3]) ).
fof(f59,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,[],[f51,f2]) ).
fof(f60,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,[],[f59,f2]) ).
fof(f61,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f5,f6]) ).
fof(f62,plain,
! [X0] : meet(X0,X0) = X0,
inference(superposition,[],[f6,f5]) ).
fof(f66,plain,
! [X0,X1] : meet(X1,join(X0,X1)) = X1,
inference(superposition,[],[f6,f3]) ).
fof(f67,plain,
! [X0,X1] : meet(X0,X1) = meet(meet(X0,X1),X0),
inference(superposition,[],[f66,f5]) ).
fof(f72,plain,
! [X0,X1] : meet(X0,X1) = meet(X0,meet(X0,X1)),
inference(forward_demodulation,[],[f67,f1]) ).
fof(f74,plain,
! [X0,X1] : join(X1,meet(X0,X1)) = X1,
inference(superposition,[],[f5,f1]) ).
fof(f75,plain,
x = meet(x,sF1),
inference(superposition,[],[f66,f53]) ).
fof(f78,plain,
v = meet(v,sF4),
inference(superposition,[],[f6,f55]) ).
fof(f83,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),X0),
inference(superposition,[],[f74,f6]) ).
fof(f92,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f83,f4]) ).
fof(f96,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X0,X2))) = join(meet(a,meet(X0,X1)),meet(a,meet(X1,X2))),
inference(superposition,[],[f60,f1]) ).
fof(f101,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X2,X0))) = join(meet(a,meet(X1,X2)),meet(a,meet(X0,X1))),
inference(superposition,[],[f60,f1]) ).
fof(f109,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,f60]) ).
fof(f132,plain,
sF9 = meet(sF9,sF10),
inference(superposition,[],[f6,f56]) ).
fof(f136,plain,
v = join(v,sF8),
inference(superposition,[],[f74,f33]) ).
fof(f137,plain,
w = join(w,sF8),
inference(superposition,[],[f5,f33]) ).
fof(f143,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X0,X1),X2)),
inference(superposition,[],[f4,f5]) ).
fof(f144,plain,
! [X2,X0,X1] : join(X0,X2) = join(X0,join(meet(X1,X0),X2)),
inference(superposition,[],[f4,f74]) ).
fof(f146,plain,
! [X2,X0,X1] : join(join(X0,X1),X2) = join(X1,join(X0,X2)),
inference(superposition,[],[f4,f3]) ).
fof(f149,plain,
! [X0] : join(y,join(x,X0)) = join(sF0,X0),
inference(superposition,[],[f4,f52]) ).
fof(f150,plain,
! [X0] : join(z,join(x,X0)) = join(sF1,X0),
inference(superposition,[],[f4,f53]) ).
fof(f151,plain,
! [X0] : join(w,join(u,X0)) = join(sF3,X0),
inference(superposition,[],[f4,f54]) ).
fof(f153,plain,
! [X0] : join(sF9,join(sF2,X0)) = join(sF10,X0),
inference(superposition,[],[f4,f56]) ).
fof(f162,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f3,f4]) ).
fof(f172,plain,
! [X0] : meet(a,meet(sF3,join(X0,sF4))) = join(meet(a,meet(sF3,X0)),meet(a,sF5)),
inference(superposition,[],[f60,f27]) ).
fof(f176,plain,
! [X0] : meet(a,meet(sF3,join(X0,sF4))) = join(meet(a,sF5),meet(a,meet(sF3,X0))),
inference(forward_demodulation,[],[f172,f3]) ).
fof(f181,plain,
! [X0] : join(u,join(sF8,X0)) = join(sF9,X0),
inference(superposition,[],[f4,f35]) ).
fof(f182,plain,
sF8 = meet(sF8,sF9),
inference(superposition,[],[f66,f35]) ).
fof(f195,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X0,X1)),
inference(superposition,[],[f4,f61]) ).
fof(f204,plain,
! [X0,X1] : join(X0,X1) = join(X1,join(X0,X1)),
inference(superposition,[],[f195,f3]) ).
fof(f219,plain,
sF14 = join(sF13,sF14),
inference(superposition,[],[f195,f58]) ).
fof(f238,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f2,f6]) ).
fof(f239,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f2,f66]) ).
fof(f247,plain,
! [X0] : meet(w,meet(v,X0)) = meet(sF8,X0),
inference(superposition,[],[f2,f33]) ).
fof(f248,plain,
! [X0] : meet(sF0,meet(sF1,X0)) = meet(sF2,X0),
inference(superposition,[],[f2,f21]) ).
fof(f249,plain,
! [X0] : meet(sF3,meet(sF4,X0)) = meet(sF5,X0),
inference(superposition,[],[f2,f27]) ).
fof(f258,plain,
! [X2,X0,X1] : meet(X0,meet(X1,X2)) = meet(X2,meet(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f262,plain,
! [X2,X0,X1] : join(X2,meet(X0,meet(X1,X2))) = X2,
inference(superposition,[],[f74,f2]) ).
fof(f288,plain,
! [X0] : meet(sF2,X0) = meet(sF2,meet(sF6,X0)),
inference(superposition,[],[f238,f29]) ).
fof(f305,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,[],[f60,f238]) ).
fof(f306,plain,
! [X2,X0,X1] : meet(a,meet(join(a,X1),join(X0,X2))) = join(meet(a,X0),meet(a,X2)),
inference(forward_demodulation,[],[f305,f238]) ).
fof(f317,plain,
! [X0] : meet(sF2,X0) = meet(sF6,meet(X0,sF2)),
inference(forward_demodulation,[],[f288,f258]) ).
fof(f319,plain,
! [X2,X0] : meet(a,join(X0,X2)) = join(meet(a,X0),meet(a,X2)),
inference(forward_demodulation,[],[f306,f238]) ).
fof(f325,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,join(meet(X0,X2),meet(X0,X1))),
inference(backward_demodulation,[],[f109,f319]) ).
fof(f326,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,join(meet(X0,X1),meet(X0,X2))),
inference(backward_demodulation,[],[f60,f319]) ).
fof(f327,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X2,X0))) = meet(a,join(meet(X1,X2),meet(X0,X1))),
inference(backward_demodulation,[],[f101,f319]) ).
fof(f328,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X0,X2))) = meet(a,join(meet(X0,X1),meet(X1,X2))),
inference(backward_demodulation,[],[f96,f319]) ).
fof(f330,plain,
! [X0] : meet(a,meet(sF3,join(X0,sF4))) = meet(a,join(sF5,meet(sF3,X0))),
inference(backward_demodulation,[],[f176,f319]) ).
fof(f382,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,[],[f326,f326]) ).
fof(f403,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,[],[f382,f326]) ).
fof(f424,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,[],[f403,f72]) ).
fof(f439,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,[],[f424,f72]) ).
fof(f448,plain,
! [X2,X0,X1] : meet(a,meet(X1,join(X0,X2))) = meet(a,join(meet(X0,X1),meet(X2,X1))),
inference(superposition,[],[f327,f1]) ).
fof(f465,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X2,X0))) = meet(a,join(meet(join(X0,X1),X2),X0)),
inference(superposition,[],[f327,f6]) ).
fof(f466,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X2,X0))) = meet(a,join(meet(join(X1,X0),X2),X0)),
inference(superposition,[],[f327,f66]) ).
fof(f498,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X2,X0))) = meet(a,join(X0,meet(join(X1,X0),X2))),
inference(forward_demodulation,[],[f466,f3]) ).
fof(f499,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X2,X0))) = meet(a,join(X0,meet(join(X0,X1),X2))),
inference(forward_demodulation,[],[f465,f3]) ).
fof(f542,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(join(X0,X1),X2))) = meet(a,meet(join(X0,X1),join(X0,X2))),
inference(superposition,[],[f328,f6]) ).
fof(f543,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(join(X1,X0),X2))) = meet(a,meet(join(X1,X0),join(X0,X2))),
inference(superposition,[],[f328,f66]) ).
fof(f659,plain,
sF1 = join(x,sF1),
inference(superposition,[],[f204,f53]) ).
fof(f660,plain,
sF9 = join(sF8,sF9),
inference(superposition,[],[f204,f35]) ).
fof(f686,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(meet(X1,X0),meet(X0,X2)),
inference(superposition,[],[f239,f74]) ).
fof(f693,plain,
! [X0] : meet(sF8,X0) = meet(sF8,meet(sF9,X0)),
inference(superposition,[],[f239,f35]) ).
fof(f737,plain,
! [X2,X0,X1] : meet(meet(X1,X0),X2) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f686,f258]) ).
fof(f745,plain,
! [X2,X0,X1] : meet(X1,meet(X0,X2)) = meet(X0,meet(X2,meet(X1,X0))),
inference(forward_demodulation,[],[f737,f2]) ).
fof(f782,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X0,X1),X2)),
inference(superposition,[],[f258,f6]) ).
fof(f783,plain,
! [X2,X0,X1] : meet(X2,X0) = meet(X0,meet(join(X1,X0),X2)),
inference(superposition,[],[f258,f66]) ).
fof(f801,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(meet(X1,X0),X1)),
inference(superposition,[],[f62,f258]) ).
fof(f846,plain,
! [X0,X1] : meet(X1,X0) = meet(X0,meet(X1,meet(X1,X0))),
inference(forward_demodulation,[],[f801,f1]) ).
fof(f882,plain,
! [X0,X1] : meet(X1,X0) = meet(X1,meet(X0,X1)),
inference(forward_demodulation,[],[f846,f745]) ).
fof(f916,plain,
! [X2,X0,X1] : join(X1,X0) = join(X1,join(X0,meet(X1,X2))),
inference(superposition,[],[f143,f3]) ).
fof(f925,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(meet(X0,X2),X1),join(X0,X1)),
inference(superposition,[],[f66,f143]) ).
fof(f934,plain,
! [X2,X0,X1] : join(meet(X0,X2),X1) = meet(join(X0,X1),join(meet(X0,X2),X1)),
inference(forward_demodulation,[],[f925,f1]) ).
fof(f964,plain,
! [X0] :
( meet(t,join(sF10,X0)) = join(sF11,meet(t,X0))
| meet(a,join(t,X0)) != meet(a,join(t,sF10)) ),
inference(superposition,[],[f15,f39]) ).
fof(f1123,plain,
! [X2,X3,X0,X1] : join(X1,join(X3,X0)) = join(X1,join(X0,join(meet(X1,X2),X3))),
inference(superposition,[],[f143,f162]) ).
fof(f1261,plain,
! [X0,X1] : join(X1,X0) = meet(join(X1,X0),join(X0,X1)),
inference(superposition,[],[f66,f92]) ).
fof(f1453,plain,
! [X0] : meet(a,meet(sF1,join(x,X0))) = meet(a,join(x,meet(sF1,X0))),
inference(superposition,[],[f328,f75]) ).
fof(f1506,plain,
! [X2,X0,X1] : join(X2,X0) = join(X2,join(X0,meet(X1,X2))),
inference(superposition,[],[f144,f3]) ).
fof(f2168,plain,
! [X2,X0,X1] : meet(a,meet(X0,join(X1,X2))) = meet(a,meet(X0,join(X2,X1))),
inference(superposition,[],[f326,f325]) ).
fof(f2468,plain,
! [X0,X1] : meet(a,join(X1,X0)) = meet(a,meet(a,join(X0,X1))),
inference(superposition,[],[f72,f2168]) ).
fof(f2504,plain,
! [X0,X1] : meet(a,join(X0,X1)) = meet(a,join(X1,X0)),
inference(forward_demodulation,[],[f2468,f72]) ).
fof(f2912,plain,
join(sF0,meet(y,z)) = join(y,sF13),
inference(superposition,[],[f149,f57]) ).
fof(f2915,plain,
! [X0] : join(sF0,X0) = join(y,join(X0,x)),
inference(superposition,[],[f149,f3]) ).
fof(f2993,plain,
! [X0] : join(y,x) = join(sF0,meet(y,X0)),
inference(superposition,[],[f143,f2915]) ).
fof(f3013,plain,
! [X0] : sF0 = join(sF0,meet(y,X0)),
inference(forward_demodulation,[],[f2993,f52]) ).
fof(f3026,plain,
sF0 = join(y,sF13),
inference(backward_demodulation,[],[f2912,f3013]) ).
fof(f3037,plain,
join(sF3,sF8) = join(w,sF9),
inference(superposition,[],[f151,f35]) ).
fof(f3285,plain,
join(sF1,meet(y,z)) = join(z,sF13),
inference(superposition,[],[f150,f57]) ).
fof(f3288,plain,
! [X0] : join(sF1,X0) = join(z,join(X0,x)),
inference(superposition,[],[f150,f3]) ).
fof(f3367,plain,
! [X0] : join(z,x) = join(sF1,meet(X0,z)),
inference(superposition,[],[f144,f3288]) ).
fof(f3385,plain,
! [X0] : sF1 = join(sF1,meet(X0,z)),
inference(forward_demodulation,[],[f3367,f53]) ).
fof(f3399,plain,
sF1 = join(z,sF13),
inference(backward_demodulation,[],[f3285,f3385]) ).
fof(f3811,plain,
meet(w,v) = meet(sF8,sF4),
inference(superposition,[],[f247,f78]) ).
fof(f3848,plain,
meet(w,v) = meet(sF4,sF8),
inference(forward_demodulation,[],[f3811,f1]) ).
fof(f3858,plain,
sF8 = meet(sF4,sF8),
inference(forward_demodulation,[],[f3848,f33]) ).
fof(f4034,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(join(X1,meet(X0,X2)),X3)),
inference(superposition,[],[f4,f916]) ).
fof(f4075,plain,
! [X2,X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X1,join(meet(X0,X2),X3))),
inference(forward_demodulation,[],[f4034,f4]) ).
fof(f4096,plain,
! [X3,X0,X1] : join(join(X0,X1),X3) = join(X0,join(X3,X1)),
inference(forward_demodulation,[],[f4075,f1123]) ).
fof(f4558,plain,
sF13 = meet(sF13,sF1),
inference(superposition,[],[f66,f3399]) ).
fof(f4573,plain,
sF13 = meet(sF1,sF13),
inference(forward_demodulation,[],[f4558,f1]) ).
fof(f4986,plain,
sF13 = meet(sF13,sF0),
inference(superposition,[],[f66,f3026]) ).
fof(f5005,plain,
sF13 = meet(sF0,sF13),
inference(forward_demodulation,[],[f4986,f1]) ).
fof(f5012,plain,
! [X0] : join(sF9,X0) = join(u,join(X0,sF8)),
inference(superposition,[],[f181,f3]) ).
fof(f5649,plain,
join(u,v) = join(sF9,v),
inference(superposition,[],[f5012,f136]) ).
fof(f5670,plain,
join(u,v) = join(v,sF9),
inference(forward_demodulation,[],[f5649,f3]) ).
fof(f5673,plain,
join(v,u) = join(v,sF9),
inference(forward_demodulation,[],[f5670,f3]) ).
fof(f5675,plain,
sF4 = join(v,sF9),
inference(forward_demodulation,[],[f5673,f55]) ).
fof(f5904,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,[],[f328,f2504]) ).
fof(f5910,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,[],[f5904,f328]) ).
fof(f5952,plain,
! [X2,X0,X1] : meet(a,join(X2,join(X0,X1))) = meet(a,meet(a,join(X2,join(X1,X0)))),
inference(forward_demodulation,[],[f5910,f72]) ).
fof(f5982,plain,
! [X2,X0,X1] : meet(a,join(X2,join(X0,X1))) = meet(a,join(X2,join(X1,X0))),
inference(forward_demodulation,[],[f5952,f72]) ).
fof(f6093,plain,
! [X0,X1] : meet(X1,X0) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f74,f882]) ).
fof(f6650,plain,
! [X0] : join(sF6,X0) = join(sF5,join(sF2,X0)),
inference(superposition,[],[f146,f29]) ).
fof(f6651,plain,
! [X0] : join(sF10,X0) = join(sF2,join(sF9,X0)),
inference(superposition,[],[f146,f56]) ).
fof(f6653,plain,
! [X0] : join(sF14,X0) = join(sF5,join(sF13,X0)),
inference(superposition,[],[f146,f58]) ).
fof(f6726,plain,
! [X0] : join(sF14,X0) = join(sF13,join(X0,sF5)),
inference(forward_demodulation,[],[f6653,f162]) ).
fof(f6728,plain,
! [X0] : join(sF10,X0) = join(sF9,join(X0,sF2)),
inference(forward_demodulation,[],[f6651,f162]) ).
fof(f6729,plain,
! [X0] : join(sF6,X0) = join(sF2,join(X0,sF5)),
inference(forward_demodulation,[],[f6650,f162]) ).
fof(f7428,plain,
join(u,w) = join(sF9,w),
inference(superposition,[],[f5012,f137]) ).
fof(f7453,plain,
join(u,w) = join(w,sF9),
inference(forward_demodulation,[],[f7428,f3]) ).
fof(f7456,plain,
join(w,u) = join(w,sF9),
inference(forward_demodulation,[],[f7453,f3]) ).
fof(f7457,plain,
sF3 = join(w,sF9),
inference(forward_demodulation,[],[f7456,f54]) ).
fof(f7458,plain,
sF3 = join(sF3,sF8),
inference(backward_demodulation,[],[f3037,f7457]) ).
fof(f7461,plain,
sF9 = meet(sF9,sF3),
inference(superposition,[],[f66,f7457]) ).
fof(f7487,plain,
sF9 = meet(sF3,sF9),
inference(forward_demodulation,[],[f7461,f1]) ).
fof(f9912,plain,
join(sF10,sF5) = join(sF9,sF6),
inference(superposition,[],[f153,f29]) ).
fof(f9994,plain,
join(sF10,sF5) = join(sF6,sF9),
inference(forward_demodulation,[],[f9912,f3]) ).
fof(f10220,plain,
sF8 = meet(sF8,sF3),
inference(superposition,[],[f66,f7458]) ).
fof(f10244,plain,
sF8 = meet(sF3,sF8),
inference(forward_demodulation,[],[f10220,f1]) ).
fof(f10253,plain,
sF9 = meet(sF9,sF4),
inference(superposition,[],[f66,f5675]) ).
fof(f10283,plain,
sF9 = meet(sF4,sF9),
inference(forward_demodulation,[],[f10253,f1]) ).
fof(f10342,plain,
! [X0,X1] : join(meet(a,X1),meet(a,X0)) = meet(a,join(X1,meet(a,X0))),
inference(superposition,[],[f319,f72]) ).
fof(f10411,plain,
! [X0,X1] : meet(a,join(X1,X0)) = meet(a,join(X1,meet(a,X0))),
inference(forward_demodulation,[],[f10342,f319]) ).
fof(f12802,plain,
! [X0,X1] : meet(X0,X1) = join(meet(X1,X0),meet(X0,X1)),
inference(superposition,[],[f204,f6093]) ).
fof(f14156,plain,
! [X0] : meet(a,meet(sF3,join(X0,sF9))) = meet(a,join(sF9,meet(sF3,X0))),
inference(superposition,[],[f325,f7487]) ).
fof(f15386,plain,
! [X2,X0,X1] : join(meet(X1,X2),X0) = meet(join(X0,X1),join(meet(X1,X2),X0)),
inference(superposition,[],[f934,f3]) ).
fof(f19822,plain,
meet(sF3,sF9) = meet(sF5,sF9),
inference(superposition,[],[f249,f10283]) ).
fof(f19843,plain,
! [X0] : meet(a,meet(sF4,join(sF9,X0))) = meet(a,join(sF9,meet(sF4,X0))),
inference(superposition,[],[f326,f10283]) ).
fof(f19846,plain,
! [X0] : meet(a,meet(sF4,join(sF9,X0))) = meet(a,join(sF9,meet(X0,sF4))),
inference(superposition,[],[f327,f10283]) ).
fof(f19891,plain,
meet(sF3,sF9) = meet(sF9,sF5),
inference(forward_demodulation,[],[f19822,f1]) ).
fof(f19901,plain,
sF9 = meet(sF9,sF5),
inference(forward_demodulation,[],[f19891,f7487]) ).
fof(f19911,plain,
sF5 = join(sF5,sF9),
inference(superposition,[],[f74,f19901]) ).
fof(f19979,plain,
sF5 = join(sF9,sF5),
inference(forward_demodulation,[],[f19911,f3]) ).
fof(f22179,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X0,X2))) = meet(a,join(X0,meet(X2,join(X0,X1)))),
inference(superposition,[],[f448,f6]) ).
fof(f22180,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X0,X2))) = meet(a,join(X0,meet(X2,join(X1,X0)))),
inference(superposition,[],[f448,f66]) ).
fof(f22224,plain,
! [X0] : meet(a,meet(sF1,join(x,X0))) = meet(a,join(x,meet(X0,sF1))),
inference(superposition,[],[f448,f75]) ).
fof(f27728,plain,
meet(sF3,sF8) = meet(sF5,sF8),
inference(superposition,[],[f249,f3858]) ).
fof(f27808,plain,
meet(sF3,sF8) = meet(sF8,sF5),
inference(forward_demodulation,[],[f27728,f1]) ).
fof(f27820,plain,
sF8 = meet(sF8,sF5),
inference(forward_demodulation,[],[f27808,f10244]) ).
fof(f27828,plain,
sF5 = join(sF5,sF8),
inference(superposition,[],[f74,f27820]) ).
fof(f27906,plain,
sF5 = join(sF8,sF5),
inference(forward_demodulation,[],[f27828,f3]) ).
fof(f28417,plain,
meet(sF0,sF13) = meet(sF2,sF13),
inference(superposition,[],[f248,f4573]) ).
fof(f28497,plain,
meet(sF0,sF13) = meet(sF13,sF2),
inference(forward_demodulation,[],[f28417,f1]) ).
fof(f28509,plain,
sF13 = meet(sF13,sF2),
inference(forward_demodulation,[],[f28497,f5005]) ).
fof(f30648,plain,
! [X2,X0,X1] : meet(X0,X2) = meet(X2,meet(X0,join(X1,X2))),
inference(superposition,[],[f783,f1]) ).
fof(f32876,plain,
meet(sF8,sF9) = meet(sF8,sF10),
inference(superposition,[],[f693,f132]) ).
fof(f33033,plain,
sF8 = meet(sF8,sF10),
inference(forward_demodulation,[],[f32876,f182]) ).
fof(f33084,plain,
sF10 = join(sF10,sF8),
inference(superposition,[],[f74,f33033]) ).
fof(f33164,plain,
sF10 = join(sF8,sF10),
inference(forward_demodulation,[],[f33084,f3]) ).
fof(f35819,plain,
join(sF2,sF5) = join(sF6,sF8),
inference(superposition,[],[f6729,f27906]) ).
fof(f35820,plain,
join(sF2,sF5) = join(sF6,sF9),
inference(superposition,[],[f6729,f19979]) ).
fof(f35821,plain,
join(sF6,sF13) = join(sF2,sF14),
inference(superposition,[],[f6729,f58]) ).
fof(f35903,plain,
join(sF6,sF13) = join(sF14,sF2),
inference(forward_demodulation,[],[f35821,f3]) ).
fof(f35904,plain,
sF6 = join(sF6,sF9),
inference(forward_demodulation,[],[f35820,f29]) ).
fof(f35905,plain,
sF6 = join(sF6,sF8),
inference(forward_demodulation,[],[f35819,f29]) ).
fof(f35932,plain,
sF6 = join(sF10,sF5),
inference(backward_demodulation,[],[f9994,f35904]) ).
fof(f41872,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X0,join(X2,X1)),
inference(superposition,[],[f4,f4096]) ).
fof(f42322,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X2,X1),X0),
inference(superposition,[],[f3,f41872]) ).
fof(f43718,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(meet(X2,meet(X3,X0)),meet(X1,X0)),
inference(superposition,[],[f30648,f262]) ).
fof(f43812,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(meet(X2,meet(X3,X0)),X1)),
inference(forward_demodulation,[],[f43718,f258]) ).
fof(f43899,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(X2,meet(meet(X3,X0),X1))),
inference(forward_demodulation,[],[f43812,f2]) ).
fof(f43925,plain,
! [X2,X3,X0,X1] : meet(X1,meet(X2,meet(X3,X0))) = meet(X0,meet(X2,meet(X3,meet(X0,X1)))),
inference(forward_demodulation,[],[f43899,f2]) ).
fof(f50195,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(meet(X1,X0),meet(meet(X0,X1),X2)),
inference(superposition,[],[f782,f12802]) ).
fof(f50235,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X1,meet(X0,meet(meet(X0,X1),X2))),
inference(forward_demodulation,[],[f50195,f2]) ).
fof(f50614,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X1,meet(X0,meet(X0,meet(X1,X2)))),
inference(forward_demodulation,[],[f50235,f2]) ).
fof(f50880,plain,
! [X2,X0,X1] : meet(X2,meet(X1,X0)) = meet(X2,meet(X0,meet(X0,X1))),
inference(forward_demodulation,[],[f50614,f43925]) ).
fof(f51032,plain,
! [X2,X0,X1] : meet(X2,meet(X0,X1)) = meet(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f50880,f72]) ).
fof(f51395,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,meet(join(X1,X0),join(X0,X1))),
inference(superposition,[],[f51032,f1261]) ).
fof(f51972,plain,
! [X2,X0,X1] : meet(X2,join(X0,X1)) = meet(X2,join(X1,X0)),
inference(forward_demodulation,[],[f51395,f1261]) ).
fof(f52115,plain,
! [X2,X3,X0,X1] : meet(X3,join(X2,join(X0,X1))) = meet(X3,join(X0,join(X1,X2))),
inference(superposition,[],[f51972,f4]) ).
fof(f52383,plain,
! [X2,X3,X0,X1] : meet(meet(X0,X1),join(X2,X3)) = meet(X0,meet(X1,join(X3,X2))),
inference(superposition,[],[f2,f51972]) ).
fof(f52499,plain,
! [X2,X3,X0,X1] : meet(X0,meet(X1,join(X3,X2))) = meet(X0,meet(X1,join(X2,X3))),
inference(forward_demodulation,[],[f52383,f2]) ).
fof(f65549,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,join(meet(X1,X0),meet(X0,X1))),
inference(superposition,[],[f42322,f6093]) ).
fof(f66092,plain,
! [X2,X0,X1] : join(meet(X0,X1),X2) = join(X2,meet(X1,X0)),
inference(forward_demodulation,[],[f65549,f6093]) ).
fof(f71223,plain,
join(sF14,sF10) = join(sF13,sF6),
inference(superposition,[],[f6726,f35932]) ).
fof(f71334,plain,
join(sF14,sF10) = join(sF6,sF13),
inference(forward_demodulation,[],[f71223,f3]) ).
fof(f71377,plain,
join(sF10,sF14) = join(sF6,sF13),
inference(forward_demodulation,[],[f71334,f3]) ).
fof(f73062,plain,
! [X0] : join(meet(sF8,X0),sF6) = meet(sF6,join(meet(sF8,X0),sF6)),
inference(superposition,[],[f15386,f35905]) ).
fof(f73593,plain,
! [X0] : sF6 = join(meet(sF8,X0),sF6),
inference(forward_demodulation,[],[f73062,f66]) ).
fof(f73816,plain,
! [X0] : sF6 = join(sF6,meet(X0,sF8)),
inference(forward_demodulation,[],[f73593,f66092]) ).
fof(f78988,plain,
! [X2,X3,X0,X1] : meet(X3,join(X0,meet(X2,X1))) = meet(X3,join(X0,meet(X1,X2))),
inference(superposition,[],[f51972,f66092]) ).
fof(f83897,plain,
meet(sF2,sF13) = meet(sF6,sF13),
inference(superposition,[],[f317,f28509]) ).
fof(f84043,plain,
meet(sF13,sF2) = meet(sF6,sF13),
inference(forward_demodulation,[],[f83897,f1]) ).
fof(f84089,plain,
sF13 = meet(sF6,sF13),
inference(forward_demodulation,[],[f84043,f28509]) ).
fof(f84824,plain,
sF6 = join(sF6,sF13),
inference(superposition,[],[f5,f84089]) ).
fof(f84934,plain,
sF6 = join(sF14,sF2),
inference(backward_demodulation,[],[f35903,f84824]) ).
fof(f84936,plain,
sF6 = join(sF10,sF14),
inference(backward_demodulation,[],[f71377,f84824]) ).
fof(f99179,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(X1,X2))) = meet(a,join(X0,meet(X1,join(X0,X2)))),
inference(superposition,[],[f439,f144]) ).
fof(f99183,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(X1,X2))) = meet(a,join(X0,meet(X1,join(X2,X0)))),
inference(superposition,[],[f439,f1506]) ).
fof(f99412,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X0,X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f22180,f99183]) ).
fof(f99450,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X0,X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f22179,f99179]) ).
fof(f99948,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(join(X1,X0),X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f543,f99412]) ).
fof(f99954,plain,
! [X2,X0,X1] : meet(a,join(X0,meet(join(X0,X1),X2))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f542,f99450]) ).
fof(f100246,plain,
! [X2,X0,X1] : meet(a,meet(join(X1,X0),join(X2,X0))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f498,f99948]) ).
fof(f100288,plain,
! [X2,X0,X1] : meet(a,meet(join(X0,X1),join(X2,X0))) = meet(a,join(X0,meet(X2,X1))),
inference(backward_demodulation,[],[f499,f99954]) ).
fof(f100756,plain,
! [X0] : meet(a,join(x,meet(sF1,X0))) = meet(a,join(x,meet(X0,z))),
inference(superposition,[],[f99948,f53]) ).
fof(f100782,plain,
! [X0] : meet(a,join(sF9,meet(sF3,X0))) = meet(a,join(sF9,meet(X0,w))),
inference(superposition,[],[f99948,f7457]) ).
fof(f100792,plain,
! [X0] : meet(a,join(sF9,meet(sF4,X0))) = meet(a,join(sF9,meet(X0,v))),
inference(superposition,[],[f99948,f5675]) ).
fof(f101207,plain,
! [X0] : meet(a,meet(sF4,join(sF9,X0))) = meet(a,join(sF9,meet(X0,v))),
inference(backward_demodulation,[],[f19843,f100792]) ).
fof(f101224,plain,
! [X0] : meet(a,meet(sF3,join(X0,sF9))) = meet(a,join(sF9,meet(X0,w))),
inference(backward_demodulation,[],[f14156,f100782]) ).
fof(f101267,plain,
! [X0] : meet(a,meet(sF1,join(x,X0))) = meet(a,join(x,meet(X0,z))),
inference(backward_demodulation,[],[f1453,f100756]) ).
fof(f101514,plain,
! [X0] : meet(a,join(sF9,meet(X0,sF4))) = meet(a,join(sF9,meet(X0,v))),
inference(backward_demodulation,[],[f19846,f101207]) ).
fof(f101536,plain,
! [X0] : meet(a,join(x,meet(X0,sF1))) = meet(a,join(x,meet(X0,z))),
inference(backward_demodulation,[],[f22224,f101267]) ).
fof(f103407,plain,
meet(a,join(sF5,sF9)) = meet(a,meet(sF3,join(sF9,sF4))),
inference(superposition,[],[f330,f7487]) ).
fof(f103631,plain,
meet(a,join(sF5,sF9)) = meet(a,meet(sF3,join(sF4,sF9))),
inference(forward_demodulation,[],[f103407,f52499]) ).
fof(f103728,plain,
meet(a,join(sF5,sF9)) = meet(a,join(sF9,meet(sF4,w))),
inference(forward_demodulation,[],[f103631,f101224]) ).
fof(f103797,plain,
meet(a,join(sF5,sF9)) = meet(a,join(sF9,meet(w,sF4))),
inference(forward_demodulation,[],[f103728,f78988]) ).
fof(f103841,plain,
meet(a,join(sF5,sF9)) = meet(a,join(sF9,meet(w,v))),
inference(forward_demodulation,[],[f103797,f101514]) ).
fof(f103867,plain,
meet(a,join(sF9,sF8)) = meet(a,join(sF5,sF9)),
inference(forward_demodulation,[],[f103841,f33]) ).
fof(f103882,plain,
meet(a,join(sF9,sF8)) = meet(a,join(sF9,sF5)),
inference(forward_demodulation,[],[f103867,f51972]) ).
fof(f103893,plain,
meet(a,sF5) = meet(a,join(sF9,sF8)),
inference(forward_demodulation,[],[f103882,f19979]) ).
fof(f103901,plain,
meet(a,sF5) = meet(a,join(sF8,sF9)),
inference(forward_demodulation,[],[f103893,f51972]) ).
fof(f103908,plain,
meet(a,sF5) = meet(a,sF9),
inference(forward_demodulation,[],[f103901,f660]) ).
fof(f103959,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,[],[f439,f103908]) ).
fof(f104045,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(sF5,X1)))) = meet(a,join(X0,meet(a,join(sF9,X1)))),
inference(forward_demodulation,[],[f103959,f439]) ).
fof(f104136,plain,
! [X0,X1] : meet(a,join(X0,meet(a,join(sF5,X1)))) = meet(a,join(X0,join(sF9,X1))),
inference(forward_demodulation,[],[f104045,f10411]) ).
fof(f104333,plain,
! [X0,X1] : meet(a,join(X0,join(sF9,X1))) = meet(a,join(X0,join(sF5,X1))),
inference(forward_demodulation,[],[f104136,f10411]) ).
fof(f115339,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF2,join(sF5,X0))),
inference(superposition,[],[f5982,f6729]) ).
fof(f115730,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF2,join(sF9,X0))),
inference(forward_demodulation,[],[f115339,f104333]) ).
fof(f115937,plain,
! [X0] : meet(a,join(sF6,X0)) = meet(a,join(sF9,join(X0,sF2))),
inference(forward_demodulation,[],[f115730,f52115]) ).
fof(f116068,plain,
! [X0] : meet(a,join(sF10,X0)) = meet(a,join(sF6,X0)),
inference(forward_demodulation,[],[f115937,f6728]) ).
fof(f118417,plain,
! [X0] : meet(a,join(sF10,meet(X0,sF8))) = meet(a,meet(sF10,join(X0,sF10))),
inference(superposition,[],[f100246,f33164]) ).
fof(f119175,plain,
! [X0] : meet(a,sF10) = meet(a,join(sF10,meet(X0,sF8))),
inference(forward_demodulation,[],[f118417,f66]) ).
fof(f119626,plain,
! [X0] : meet(a,sF10) = meet(a,join(sF6,meet(X0,sF8))),
inference(forward_demodulation,[],[f119175,f116068]) ).
fof(f119938,plain,
meet(a,sF6) = meet(a,sF10),
inference(forward_demodulation,[],[f119626,f73816]) ).
fof(f120555,plain,
! [X0] : meet(a,join(X0,sF10)) = join(meet(a,X0),meet(a,sF6)),
inference(superposition,[],[f319,f119938]) ).
fof(f120787,plain,
! [X0] : meet(a,join(X0,sF10)) = meet(a,join(X0,sF6)),
inference(forward_demodulation,[],[f120555,f319]) ).
fof(f120934,plain,
! [X0] :
( meet(t,join(sF10,X0)) = join(sF11,meet(t,X0))
| meet(a,join(t,sF6)) != meet(a,join(t,X0)) ),
inference(backward_demodulation,[],[f964,f120787]) ).
fof(f129289,plain,
( join(sF11,sF15) = meet(t,join(sF10,sF14))
| meet(a,join(t,sF6)) != meet(a,join(t,sF14)) ),
inference(superposition,[],[f120934,f47]) ).
fof(f131739,plain,
! [X0] : meet(a,join(x,meet(y,X0))) = meet(a,meet(join(x,X0),sF0)),
inference(superposition,[],[f100288,f52]) ).
fof(f132291,plain,
! [X0] : meet(a,meet(sF0,join(x,X0))) = meet(a,join(x,meet(y,X0))),
inference(forward_demodulation,[],[f131739,f51032]) ).
fof(f139702,plain,
meet(a,meet(sF0,sF1)) = meet(a,join(x,meet(y,sF1))),
inference(superposition,[],[f132291,f659]) ).
fof(f139955,plain,
meet(a,meet(sF0,sF1)) = meet(a,join(x,meet(y,z))),
inference(forward_demodulation,[],[f139702,f101536]) ).
fof(f140052,plain,
meet(a,meet(sF0,sF1)) = meet(a,sF13),
inference(forward_demodulation,[],[f139955,f57]) ).
fof(f140129,plain,
meet(a,sF2) = meet(a,sF13),
inference(forward_demodulation,[],[f140052,f21]) ).
fof(f140255,plain,
! [X0] : meet(a,join(X0,sF2)) = join(meet(a,X0),meet(a,sF13)),
inference(superposition,[],[f319,f140129]) ).
fof(f140436,plain,
! [X0] : meet(a,join(X0,sF13)) = meet(a,join(X0,sF2)),
inference(forward_demodulation,[],[f140255,f319]) ).
fof(f143660,plain,
meet(a,sF6) = meet(a,join(sF14,sF13)),
inference(superposition,[],[f140436,f84934]) ).
fof(f143842,plain,
meet(a,sF6) = meet(a,join(sF13,sF14)),
inference(forward_demodulation,[],[f143660,f51972]) ).
fof(f143942,plain,
meet(a,sF6) = meet(a,sF14),
inference(forward_demodulation,[],[f143842,f219]) ).
fof(f144141,plain,
! [X0] : meet(a,join(X0,sF14)) = join(meet(a,X0),meet(a,sF6)),
inference(superposition,[],[f319,f143942]) ).
fof(f144392,plain,
! [X0] : meet(a,join(X0,sF14)) = meet(a,join(X0,sF6)),
inference(forward_demodulation,[],[f144141,f319]) ).
fof(f145034,plain,
join(sF11,sF15) = meet(t,join(sF10,sF14)),
inference(forward_subsumption_resolution,[],[f129289,f144392]) ).
fof(f145039,plain,
meet(t,sF6) = join(sF11,sF15),
inference(forward_demodulation,[],[f145034,f84936]) ).
fof(f145043,plain,
meet(t,sF6) = sF16,
inference(forward_demodulation,[],[f145039,f49]) ).
fof(f145045,plain,
sF7 = sF16,
inference(forward_demodulation,[],[f145043,f31]) ).
fof(f145046,plain,
$false,
inference(forward_subsumption_resolution,[],[f145045,f50]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT398-2 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 % Computer : n008.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sun Sep 27 15:15:55 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/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
% 10.46/2.31 % (1358537)Input is clausal, will run a generic CNF schedule.
% 10.46/2.31 % (1358548)dis-21_1_sil=8000:lcm=predicate:random_seed=3044012556: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)
% 10.46/2.31 % (1358548)Refutation not found, incomplete strategy
% 10.46/2.31 % (1358548)------------------------------
% 10.46/2.31 % (1358548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (1358548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (1358548)CaDiCaL version: 2.1.3
% 10.46/2.31 % (1358548)Termination reason: Refutation not found, incomplete strategy
% 10.46/2.31 % (1358548)Time elapsed: 0.001 s
% 10.46/2.31 % (1358548)Peak memory usage: 88 MB
% 10.46/2.31 % (1358548)Instructions burned: 1 (million)
% 10.46/2.31 % (1358544)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3070481614:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.46/2.31 % (1358543)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=461537130:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.46/2.31 % (1358542)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=3145892464:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.46/2.31 % (1358547)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1505867254:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.46/2.31 % (1358546)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2454913772:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.46/2.31 % (1358545)lrs+10_1_sil=8000:sp=occurrence:random_seed=3480621424:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.46/2.31 % (1358545)Instruction limit reached!
% 10.46/2.31 % (1358545)------------------------------
% 10.46/2.31 % (1358545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (1358545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (1358545)CaDiCaL version: 2.1.3
% 10.46/2.31 % (1358545)Termination reason: Instruction limit
% 10.46/2.31 % (1358545)Termination phase: Saturation
% 10.46/2.31 % (1358545)Time elapsed: 0.062 s
% 10.46/2.31 % (1358545)Peak memory usage: 88 MB
% 10.46/2.31 % (1358545)Instructions burned: 108 (million)
% 10.46/2.31 % (1358546)Instruction limit reached!
% 10.46/2.31 % (1358546)------------------------------
% 10.46/2.31 % (1358546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (1358546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (1358546)CaDiCaL version: 2.1.3
% 10.46/2.31 % (1358546)Termination reason: Instruction limit
% 10.46/2.31 % (1358546)Termination phase: Saturation
% 10.46/2.31 % (1358546)Time elapsed: 0.068 s
% 10.46/2.31 % (1358546)Peak memory usage: 88 MB
% 10.46/2.31 % (1358546)Instructions burned: 115 (million)
% 10.46/2.31 % (1358547)Instruction limit reached!
% 10.46/2.31 % (1358547)------------------------------
% 10.46/2.31 % (1358547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (1358547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (1358547)CaDiCaL version: 2.1.3
% 10.46/2.31 % (1358547)Termination reason: Instruction limit
% 10.46/2.31 % (1358547)Termination phase: Saturation
% 10.46/2.31 % (1358547)Time elapsed: 0.105 s
% 10.46/2.31 % (1358547)Peak memory usage: 89 MB
% 10.46/2.31 % (1358547)Instructions burned: 181 (million)
% 10.46/2.31 % (1358548)------------------------------
% 10.46/2.31 % (1358548)------------------------------
% 10.46/2.31 % (1358559)lrs+10_64_to=lpo:sil=8000:random_seed=129918355:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 10.46/2.31 % (1358556)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=2832167813:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.46/2.31 % (1358556)Refutation not found, incomplete strategy
% 10.46/2.31 % (1358556)------------------------------
% 10.46/2.31 % (1358556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.46/2.31 % (1358556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.46/2.31 % (1358556)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358556)Termination reason: Refutation not found, incomplete strategy
% 19.83/3.73 % (1358556)Time elapsed: 0.001 s
% 19.83/3.73 % (1358556)Peak memory usage: 88 MB
% 19.83/3.73 % (1358556)Instructions burned: 1 (million)
% 19.83/3.73 % (1358557)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=549066566: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)
% 19.83/3.73 % (1358557)Refutation not found, incomplete strategy
% 19.83/3.73 % (1358557)------------------------------
% 19.83/3.73 % (1358557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.83/3.73 % (1358557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.73 % (1358557)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358557)Termination reason: Refutation not found, incomplete strategy
% 19.83/3.73 % (1358557)Time elapsed: 0.002 s
% 19.83/3.73 % (1358557)Peak memory usage: 88 MB
% 19.83/3.73 % (1358557)Instructions burned: 2 (million)
% 19.83/3.73 % (1358559)Instruction limit reached!
% 19.83/3.73 % (1358559)------------------------------
% 19.83/3.73 % (1358559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.83/3.73 % (1358559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.73 % (1358559)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358559)Termination reason: Instruction limit
% 19.83/3.73 % (1358559)Termination phase: Saturation
% 19.83/3.73 % (1358559)Time elapsed: 0.039 s
% 19.83/3.73 % (1358559)Peak memory usage: 88 MB
% 19.83/3.73 % (1358559)Instructions burned: 127 (million)
% 19.83/3.73 % (1358558)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2603038242:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 19.83/3.73 % (1358558)Refutation not found, incomplete strategy
% 19.83/3.73 % (1358558)------------------------------
% 19.83/3.73 % (1358558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.83/3.73 % (1358558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.73 % (1358558)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358558)Termination reason: Refutation not found, incomplete strategy
% 19.83/3.73 % (1358558)Time elapsed: 0.001 s
% 19.83/3.73 % (1358558)Peak memory usage: 88 MB
% 19.83/3.73 % (1358558)Instructions burned: 1 (million)
% 19.83/3.73 % (1358569)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3061936442:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 19.83/3.73 % (1358569)Instruction limit reached!
% 19.83/3.73 % (1358569)------------------------------
% 19.83/3.73 % (1358569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.83/3.73 % (1358569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.73 % (1358569)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358569)Termination reason: Instruction limit
% 19.83/3.73 % (1358569)Termination phase: Saturation
% 19.83/3.73 % (1358569)Time elapsed: 0.062 s
% 19.83/3.73 % (1358569)Peak memory usage: 90 MB
% 19.83/3.73 % (1358569)Instructions burned: 194 (million)
% 19.83/3.73 % (1358556)------------------------------
% 19.83/3.73 % (1358556)------------------------------
% 19.83/3.73 % (1358557)------------------------------
% 19.83/3.73 % (1358557)------------------------------
% 19.83/3.73 % (1358616)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1646617262:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 19.83/3.73 % (1358558)------------------------------
% 19.83/3.73 % (1358558)------------------------------
% 19.83/3.73 % (1358616)Instruction limit reached!
% 19.83/3.73 % (1358616)------------------------------
% 19.83/3.73 % (1358616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.83/3.73 % (1358616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.83/3.73 % (1358616)CaDiCaL version: 2.1.3
% 19.83/3.73 % (1358616)Termination reason: Instruction limit
% 19.83/3.73 % (1358616)Termination phase: Saturation
% 19.83/3.73 % (1358616)Time elapsed: 0.052 s
% 19.83/3.73 % (1358616)Peak memory usage: 91 MB
% 19.83/3.73 % (1358616)Instructions burned: 158 (million)
% 19.83/3.73 % (1358634)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2112347007:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 19.83/3.73 % (1358635)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=1495469688:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 32.48/5.52 % (1358643)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3780761119:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 32.48/5.52 % (1358643)Refutation not found, incomplete strategy
% 32.48/5.52 % (1358643)------------------------------
% 32.48/5.52 % (1358643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358643)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358643)Termination reason: Refutation not found, incomplete strategy
% 32.48/5.52 % (1358643)Time elapsed: 0.002 s
% 32.48/5.52 % (1358643)Peak memory usage: 88 MB
% 32.48/5.52 % (1358643)Instructions burned: 2 (million)
% 32.48/5.52 % (1358635)Instruction limit reached!
% 32.48/5.52 % (1358635)------------------------------
% 32.48/5.52 % (1358635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358635)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358635)Termination reason: Instruction limit
% 32.48/5.52 % (1358635)Termination phase: Saturation
% 32.48/5.52 % (1358635)Time elapsed: 0.058 s
% 32.48/5.52 % (1358635)Peak memory usage: 89 MB
% 32.48/5.52 % (1358635)Instructions burned: 107 (million)
% 32.48/5.52 % (1358647)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=603227046:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 32.48/5.52 % (1358666)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=114153405:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 32.48/5.52 % (1358647)Instruction limit reached!
% 32.48/5.52 % (1358647)------------------------------
% 32.48/5.52 % (1358647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358647)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358647)Termination reason: Instruction limit
% 32.48/5.52 % (1358647)Termination phase: Saturation
% 32.48/5.52 % (1358647)Time elapsed: 0.140 s
% 32.48/5.52 % (1358647)Peak memory usage: 91 MB
% 32.48/5.52 % (1358647)Instructions burned: 243 (million)
% 32.48/5.52 % (1358643)------------------------------
% 32.48/5.52 % (1358643)------------------------------
% 32.48/5.52 % (1358692)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=734375759:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 32.48/5.52 % (1358719)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=481464966:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 32.48/5.52 % (1358692)Instruction limit reached!
% 32.48/5.52 % (1358692)------------------------------
% 32.48/5.52 % (1358692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358692)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358692)Termination reason: Instruction limit
% 32.48/5.52 % (1358692)Termination phase: Saturation
% 32.48/5.52 % (1358692)Time elapsed: 0.077 s
% 32.48/5.52 % (1358692)Peak memory usage: 89 MB
% 32.48/5.52 % (1358692)Instructions burned: 134 (million)
% 32.48/5.52 % (1358735)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1752590565:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 32.48/5.52 % (1358735)Instruction limit reached!
% 32.48/5.52 % (1358735)------------------------------
% 32.48/5.52 % (1358735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358735)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358735)Termination reason: Instruction limit
% 32.48/5.52 % (1358735)Termination phase: Saturation
% 32.48/5.52 % (1358735)Time elapsed: 0.118 s
% 32.48/5.52 % (1358735)Peak memory usage: 90 MB
% 32.48/5.52 % (1358735)Instructions burned: 192 (million)
% 32.48/5.52 % (1358719)Instruction limit reached!
% 32.48/5.52 % (1358719)------------------------------
% 32.48/5.52 % (1358719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.48/5.52 % (1358719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.48/5.52 % (1358719)CaDiCaL version: 2.1.3
% 32.48/5.52 % (1358719)Termination reason: Instruction limit
% 52.96/8.38 % (1358719)Termination phase: Saturation
% 52.96/8.38 % (1358719)Time elapsed: 0.314 s
% 52.96/8.38 % (1358719)Peak memory usage: 93 MB
% 52.96/8.38 % (1358719)Instructions burned: 500 (million)
% 52.96/8.38 % (1358737)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=873492227:i=264:kws=precedence:fsr=off_2986 on theBenchmark for (2986ds/264Mi)
% 52.96/8.38 % (1358738)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2821992498:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 52.96/8.38 % (1358737)Instruction limit reached!
% 52.96/8.38 % (1358737)------------------------------
% 52.96/8.38 % (1358737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.96/8.38 % (1358737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.96/8.38 % (1358737)CaDiCaL version: 2.1.3
% 52.96/8.38 % (1358737)Termination reason: Instruction limit
% 52.96/8.38 % (1358737)Termination phase: Saturation
% 52.96/8.38 % (1358737)Time elapsed: 0.150 s
% 52.96/8.38 % (1358737)Peak memory usage: 91 MB
% 52.96/8.38 % (1358737)Instructions burned: 265 (million)
% 52.96/8.39 % (1358738)Instruction limit reached!
% 52.96/8.39 % (1358738)------------------------------
% 52.96/8.39 % (1358738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.96/8.39 % (1358738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.96/8.39 % (1358738)CaDiCaL version: 2.1.3
% 52.96/8.39 % (1358738)Termination reason: Instruction limit
% 52.96/8.39 % (1358738)Termination phase: Saturation
% 52.96/8.39 % (1358738)Time elapsed: 0.089 s
% 52.96/8.39 % (1358738)Peak memory usage: 89 MB
% 52.96/8.39 % (1358738)Instructions burned: 157 (million)
% 52.96/8.39 % (1358741)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=2617704331:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 52.96/8.39 % (1358742)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=940960088:i=537:av=off:ss=included_2983 on theBenchmark for (2983ds/537Mi)
% 52.96/8.39 % (1358742)Instruction limit reached!
% 52.96/8.39 % (1358742)------------------------------
% 52.96/8.39 % (1358742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.96/8.39 % (1358742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.96/8.39 % (1358742)CaDiCaL version: 2.1.3
% 52.96/8.39 % (1358742)Termination reason: Instruction limit
% 52.96/8.39 % (1358742)Termination phase: Saturation
% 52.96/8.39 % (1358742)Time elapsed: 0.288 s
% 52.96/8.39 % (1358742)Peak memory usage: 93 MB
% 52.96/8.39 % (1358742)Instructions burned: 538 (million)
% 52.96/8.39 % (1358745)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3720930604:i=180:bd=preordered:av=off_2979 on theBenchmark for (2979ds/180Mi)
% 52.96/8.39 % (1358745)Instruction limit reached!
% 52.96/8.39 % (1358745)------------------------------
% 52.96/8.39 % (1358745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.96/8.39 % (1358745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.96/8.39 % (1358745)CaDiCaL version: 2.1.3
% 52.96/8.39 % (1358745)Termination reason: Instruction limit
% 52.96/8.39 % (1358745)Termination phase: Saturation
% 52.96/8.39 % (1358745)Time elapsed: 0.101 s
% 52.96/8.39 % (1358745)Peak memory usage: 89 MB
% 52.96/8.39 % (1358745)Instructions burned: 181 (million)
% 52.96/8.39 % (1358747)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=86898649:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2976 on theBenchmark for (2976ds/10307Mi)
% 52.96/8.39 % (1358634)Instruction limit reached!
% 52.96/8.39 % (1358634)------------------------------
% 52.96/8.39 % (1358634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.96/8.39 % (1358634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.96/8.39 % (1358634)CaDiCaL version: 2.1.3
% 52.96/8.39 % (1358634)Termination reason: Instruction limit
% 52.96/8.39 % (1358634)Termination phase: Saturation
% 52.96/8.39 % (1358634)Time elapsed: 2.023 s
% 52.96/8.39 % (1358634)Peak memory usage: 149 MB
% 52.96/8.39 % (1358634)Instructions burned: 3395 (million)
% 52.96/8.39 % (1358749)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=4082477596:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 48.06/12.06 % (1358749)Instruction limit reached!
% 48.06/12.06 % (1358749)------------------------------
% 48.06/12.06 % (1358749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358749)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358749)Termination reason: Instruction limit
% 48.06/12.06 % (1358749)Termination phase: Saturation
% 48.06/12.06 % (1358749)Time elapsed: 0.253 s
% 48.06/12.06 % (1358749)Peak memory usage: 95 MB
% 48.06/12.06 % (1358749)Instructions burned: 412 (million)
% 48.06/12.06 % (1358751)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=3620371745:s2pl=no:i=8478:s2at=4:nm=6_2968 on theBenchmark for (2968ds/8478Mi)
% 48.06/12.06 % (1358741)Instruction limit reached!
% 48.06/12.06 % (1358741)------------------------------
% 48.06/12.06 % (1358741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358741)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358741)Termination reason: Instruction limit
% 48.06/12.06 % (1358741)Termination phase: Saturation
% 48.06/12.06 % (1358741)Time elapsed: 1.965 s
% 48.06/12.06 % (1358741)Peak memory usage: 147 MB
% 48.06/12.06 % (1358741)Instructions burned: 3256 (million)
% 48.06/12.06 % (1358753)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=3142621254:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi)
% 48.06/12.06 % (1358753)Refutation not found, incomplete strategy
% 48.06/12.06 % (1358753)------------------------------
% 48.06/12.06 % (1358753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358753)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358753)Termination reason: Refutation not found, incomplete strategy
% 48.06/12.06 % (1358753)Time elapsed: 0.002 s
% 48.06/12.06 % (1358753)Peak memory usage: 88 MB
% 48.06/12.06 % (1358753)Instructions burned: 1 (million)
% 48.06/12.06 % (1358666)Instruction limit reached!
% 48.06/12.06 % (1358666)------------------------------
% 48.06/12.06 % (1358666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358666)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358666)Termination reason: Instruction limit
% 48.06/12.06 % (1358666)Termination phase: Saturation
% 48.06/12.06 % (1358666)Time elapsed: 3.075 s
% 48.06/12.06 % (1358666)Peak memory usage: 170 MB
% 48.06/12.06 % (1358666)Instructions burned: 5208 (million)
% 48.06/12.06 % (1358753)------------------------------
% 48.06/12.06 % (1358753)------------------------------
% 48.06/12.06 % (1358755)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=74116319:st=4:i=720:sd=3:fsr=off:ss=axioms_2959 on theBenchmark for (2959ds/720Mi)
% 48.06/12.06 % (1358755)Refutation not found, incomplete strategy
% 48.06/12.06 % (1358755)------------------------------
% 48.06/12.06 % (1358755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358755)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358755)Termination reason: Refutation not found, incomplete strategy
% 48.06/12.06 % (1358755)Time elapsed: 0.001 s
% 48.06/12.06 % (1358755)Peak memory usage: 88 MB
% 48.06/12.06 % (1358755)Instructions burned: 1 (million)
% 48.06/12.06 % (1358757)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3322160319:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi)
% 48.06/12.06 % (1358755)------------------------------
% 48.06/12.06 % (1358755)------------------------------
% 48.06/12.06 % (1358759)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1799258881:i=2989:sd=3:ss=axioms:sgt=60_2956 on theBenchmark for (2956ds/2989Mi)
% 48.06/12.06 % (1358757)Instruction limit reached!
% 48.06/12.06 % (1358757)------------------------------
% 48.06/12.06 % (1358757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358757)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358757)Termination reason: Instruction limit
% 48.06/12.06 % (1358757)Termination phase: Saturation
% 48.06/12.06 % (1358757)Time elapsed: 0.372 s
% 48.06/12.06 % (1358757)Peak memory usage: 94 MB
% 48.06/12.06 % (1358757)Instructions burned: 599 (million)
% 48.06/12.06 % (1358761)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=4268585972:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2953 on theBenchmark for (2953ds/1997Mi)
% 48.06/12.06 % (1358761)Instruction limit reached!
% 48.06/12.06 % (1358761)------------------------------
% 48.06/12.06 % (1358761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358761)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358761)Termination reason: Instruction limit
% 48.06/12.06 % (1358761)Termination phase: Saturation
% 48.06/12.06 % (1358761)Time elapsed: 1.183 s
% 48.06/12.06 % (1358761)Peak memory usage: 139 MB
% 48.06/12.06 % (1358761)Instructions burned: 1997 (million)
% 48.06/12.06 % (1358763)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=1955025084:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi)
% 48.06/12.06 % (1358759)Instruction limit reached!
% 48.06/12.06 % (1358759)------------------------------
% 48.06/12.06 % (1358759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358759)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358759)Termination reason: Instruction limit
% 48.06/12.06 % (1358759)Termination phase: Saturation
% 48.06/12.06 % (1358759)Time elapsed: 1.685 s
% 48.06/12.06 % (1358759)Peak memory usage: 147 MB
% 48.06/12.06 % (1358759)Instructions burned: 2990 (million)
% 48.06/12.06 % (1358765)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=545419157:i=1098:nicw=on_2937 on theBenchmark for (2937ds/1098Mi)
% 48.06/12.06 % (1358765)Instruction limit reached!
% 48.06/12.06 % (1358765)------------------------------
% 48.06/12.06 % (1358765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358765)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358765)Termination reason: Instruction limit
% 48.06/12.06 % (1358765)Termination phase: Saturation
% 48.06/12.06 % (1358765)Time elapsed: 0.635 s
% 48.06/12.06 % (1358765)Peak memory usage: 99 MB
% 48.06/12.06 % (1358765)Instructions burned: 1099 (million)
% 48.06/12.06 % (1358767)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3069030960:i=433:bd=preordered_2930 on theBenchmark for (2930ds/433Mi)
% 48.06/12.06 % (1358767)Refutation not found, incomplete strategy
% 48.06/12.06 % (1358767)------------------------------
% 48.06/12.06 % (1358767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358767)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358767)Termination reason: Refutation not found, incomplete strategy
% 48.06/12.06 % (1358767)Time elapsed: 0.002 s
% 48.06/12.06 % (1358767)Peak memory usage: 88 MB
% 48.06/12.06 % (1358767)Instructions burned: 1 (million)
% 48.06/12.06 % (1358767)------------------------------
% 48.06/12.06 % (1358767)------------------------------
% 48.06/12.06 % (1358763)Instruction limit reached!
% 48.06/12.06 % (1358763)------------------------------
% 48.06/12.06 % (1358763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358763)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358763)Termination reason: Instruction limit
% 48.06/12.06 % (1358763)Termination phase: Saturation
% 48.06/12.06 % (1358763)Time elapsed: 1.279 s
% 48.06/12.06 % (1358763)Peak memory usage: 138 MB
% 48.06/12.06 % (1358763)Instructions burned: 2088 (million)
% 48.06/12.06 % (1358769)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2731035159:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2926 on theBenchmark for (2926ds/2942Mi)
% 48.06/12.06 % (1358770)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1730918706:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2926 on theBenchmark for (2926ds/6922Mi)
% 48.06/12.06 % (1358747)Instruction limit reached!
% 48.06/12.06 % (1358747)------------------------------
% 48.06/12.06 % (1358747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358747)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358747)Termination reason: Instruction limit
% 48.06/12.06 % (1358747)Termination phase: Saturation
% 48.06/12.06 % (1358747)Time elapsed: 6.169 s
% 48.06/12.06 % (1358747)Peak memory usage: 209 MB
% 48.06/12.06 % (1358747)Instructions burned: 10307 (million)
% 48.06/12.06 % (1358773)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=263317783:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2913 on theBenchmark for (2913ds/596Mi)
% 48.06/12.06 % (1358773)Refutation not found, incomplete strategy
% 48.06/12.06 % (1358773)------------------------------
% 48.06/12.06 % (1358773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358773)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358773)Termination reason: Refutation not found, incomplete strategy
% 48.06/12.06 % (1358773)Time elapsed: 0.002 s
% 48.06/12.06 % (1358773)Peak memory usage: 88 MB
% 48.06/12.06 % (1358773)Instructions burned: 2 (million)
% 48.06/12.06 % (1358751)Instruction limit reached!
% 48.06/12.06 % (1358751)------------------------------
% 48.06/12.06 % (1358751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358751)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358751)Termination reason: Instruction limit
% 48.06/12.06 % (1358751)Termination phase: Saturation
% 48.06/12.06 % (1358751)Time elapsed: 5.503 s
% 48.06/12.06 % (1358751)Peak memory usage: 174 MB
% 48.06/12.06 % (1358751)Instructions burned: 8478 (million)
% 48.06/12.06 % (1358775)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=2267220888:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2912 on theBenchmark for (2912ds/4123Mi)
% 48.06/12.06 % (1358773)------------------------------
% 48.06/12.06 % (1358773)------------------------------
% 48.06/12.06 % (1358777)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3501729982:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2910 on theBenchmark for (2910ds/16411Mi)
% 48.06/12.06 % (1358769)Instruction limit reached!
% 48.06/12.06 % (1358769)------------------------------
% 48.06/12.06 % (1358769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358769)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358769)Termination reason: Instruction limit
% 48.06/12.06 % (1358769)Termination phase: Saturation
% 48.06/12.06 % (1358769)Time elapsed: 1.922 s
% 48.06/12.06 % (1358769)Peak memory usage: 144 MB
% 48.06/12.06 % (1358769)Instructions burned: 2943 (million)
% 48.06/12.06 % (1358779)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3489167732:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2906 on theBenchmark for (2906ds/1670Mi)
% 48.06/12.06 % (1358779)Instruction limit reached!
% 48.06/12.06 % (1358779)------------------------------
% 48.06/12.06 % (1358779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.06/12.06 % (1358779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.06/12.06 % (1358779)CaDiCaL version: 2.1.3
% 48.06/12.06 % (1358779)Termination reason: Instruction limit
% 48.06/12.06 % (1358779)Termination phase: Saturation
% 48.06/12.06 % (1358779)Time elapsed: 1.056 s
% 48.06/12.06 % (1358779)Peak memory usage: 136 MB
% 48.06/12.06 % (1358779)Instructions burned: 1670 (million)
% 48.06/12.06 % (1358781)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=729497650:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2894 on theBenchmark for (2894ds/1722Mi)
% 48.06/12.06 % (1358544)First to succeed.
% 48.06/12.06 % (1358544)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1358537"
% 48.06/12.06 % (1358544)Refutation found. Thanks to Tanya!
% 48.06/12.06 % SZS status Unsatisfiable for theBenchmark
% 48.06/12.06 % SZS output start Proof for theBenchmark
% See solution above
% 79.79/12.26 % (1358544)------------------------------
% 79.79/12.26 % (1358544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.79/12.26 % (1358544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.79/12.26 % (1358544)CaDiCaL version: 2.1.3
% 79.79/12.26 % (1358544)Termination reason: Refutation
% 79.79/12.26 % (1358544)Time elapsed: 10.745 s
% 79.79/12.26 % (1358544)Peak memory usage: 263 MB
% 79.79/12.26 % (1358544)Instructions burned: 17617 (million)
% 79.79/12.26 % (1358544)------------------------------
% 79.79/12.26 % (1358544)------------------------------
% 79.79/12.26 % (1358537)Success in time 11.188 s
% 79.79/12.26 % Vampire exiting
%------------------------------------------------------------------------------