%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 09:07:32 AM UTC 2026
% Result : Unsatisfiable 179.13s 38.28s
% Output : Refutation 264.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 21
% Syntax : Number of formulae : 255 ( 154 unt; 13 def)
% Number of atoms : 419 ( 269 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 327 ( 163 ~; 159 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-2 aty)
% Number of variables : 198 ( 0 sgn 198 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(X0,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m3) ).
fof(f2,plain,
! [X0] : one = multiply(X0,one),
inference(reorient_equations,[],[f1]) ).
fof(f3,axiom,
! [X0] : multiply(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m4) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),multiply(multiply(X2,X0),multiply(X2,X1))) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m5) ).
fof(f5,plain,
! [X2,X0,X1] : one = multiply(multiply(X0,X1),multiply(multiply(X2,X0),multiply(X2,X1))),
inference(reorient_equations,[],[f4]) ).
fof(f6,axiom,
! [X0,X1] :
( multiply(X0,X1) != one
| multiply(X1,X0) != one
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m7) ).
fof(f7,plain,
! [X0,X1] :
( one != multiply(X1,X0)
| one != multiply(X0,X1)
| X0 = X1 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] : multiply(X0,X0) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m8) ).
fof(f9,plain,
! [X0] : one = multiply(X0,X0),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m9) ).
fof(f11,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),multiply(X0,X2)) = multiply(multiply(X1,X0),multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',h) ).
fof(f12,negated_conjecture,
multiply(multiply(multiply(multiply(a,b),b),a),a) != multiply(multiply(multiply(multiply(b,a),a),b),b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_j) ).
fof(f13,definition,
sF0 = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f14,plain,
multiply(a,b) = sF0,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF1 = multiply(sF0,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f16,plain,
multiply(sF0,b) = sF1,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF2 = multiply(sF1,a),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f18,plain,
multiply(sF1,a) = sF2,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF3 = multiply(sF2,a),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f20,plain,
multiply(sF2,a) = sF3,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF4 = multiply(b,a),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f22,plain,
multiply(b,a) = sF4,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF5 = multiply(sF4,a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f24,plain,
multiply(sF4,a) = sF5,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF6 = multiply(sF5,b),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f26,plain,
multiply(sF5,b) = sF6,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF7 = multiply(sF6,b),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f28,plain,
multiply(sF6,b) = sF7,
inference(reorient_equations,[],[f27]) ).
fof(f29,plain,
sF3 != sF7,
inference(definition_folding,[],[f12,f28,f26,f24,f22,f20,f18,f16,f14]) ).
fof(f53,plain,
! [X0,X1] : one = multiply(X0,multiply(multiply(X1,one),multiply(X1,X0))),
inference(superposition,[],[f5,f3]) ).
fof(f72,plain,
! [X0,X1] : one = multiply(X0,multiply(one,multiply(X1,X0))),
inference(forward_demodulation,[],[f53,f2]) ).
fof(f74,plain,
! [X0,X1] : one = multiply(X0,multiply(X1,X0)),
inference(forward_demodulation,[],[f72,f3]) ).
fof(f77,plain,
! [X0] : one = multiply(multiply(X0,b),multiply(multiply(a,X0),sF0)),
inference(superposition,[],[f5,f14]) ).
fof(f85,plain,
! [X0] : multiply(multiply(a,b),multiply(a,X0)) = multiply(sF4,multiply(b,X0)),
inference(superposition,[],[f11,f22]) ).
fof(f87,plain,
! [X0] : multiply(multiply(X0,b),multiply(X0,a)) = multiply(multiply(b,X0),sF4),
inference(superposition,[],[f11,f22]) ).
fof(f88,plain,
! [X0] : multiply(sF0,multiply(a,X0)) = multiply(sF4,multiply(b,X0)),
inference(forward_demodulation,[],[f85,f14]) ).
fof(f103,plain,
! [X0] : multiply(multiply(X0,sF6),multiply(X0,b)) = multiply(multiply(sF6,X0),sF7),
inference(superposition,[],[f11,f28]) ).
fof(f109,plain,
! [X0] : multiply(multiply(X0,sF2),multiply(X0,a)) = multiply(multiply(sF2,X0),sF3),
inference(superposition,[],[f11,f20]) ).
fof(f130,plain,
! [X2,X3,X0,X1] : multiply(multiply(X1,X0),multiply(X3,multiply(X1,X2))) = multiply(X3,multiply(multiply(X0,X1),multiply(X0,X2))),
inference(superposition,[],[f10,f11]) ).
fof(f133,plain,
! [X0] : multiply(b,multiply(X0,a)) = multiply(X0,sF4),
inference(superposition,[],[f10,f22]) ).
fof(f158,plain,
! [X2,X3,X0,X1] : multiply(multiply(X0,multiply(X1,X2)),multiply(X1,X3)) = multiply(multiply(multiply(X0,X2),X1),multiply(multiply(X0,X2),X3)),
inference(superposition,[],[f11,f10]) ).
fof(f164,plain,
! [X2,X0,X1] : multiply(multiply(X1,X0),multiply(X1,X2)) = multiply(X0,multiply(multiply(X0,X1),X2)),
inference(superposition,[],[f11,f10]) ).
fof(f165,plain,
! [X2,X0,X1] : one = multiply(multiply(X0,X1),multiply(multiply(X1,X2),multiply(X0,X2))),
inference(superposition,[],[f5,f10]) ).
fof(f175,plain,
! [X0] : multiply(sF0,multiply(X0,b)) = multiply(X0,sF1),
inference(superposition,[],[f10,f16]) ).
fof(f183,plain,
! [X0] : multiply(sF4,multiply(X0,a)) = multiply(X0,sF5),
inference(superposition,[],[f10,f24]) ).
fof(f191,plain,
! [X0] : multiply(X0,sF2) = multiply(sF1,multiply(X0,a)),
inference(superposition,[],[f10,f18]) ).
fof(f193,plain,
! [X0] : multiply(multiply(X0,sF1),multiply(X0,a)) = multiply(multiply(sF1,X0),sF2),
inference(superposition,[],[f11,f18]) ).
fof(f199,plain,
! [X0] : multiply(X0,sF6) = multiply(sF5,multiply(X0,b)),
inference(superposition,[],[f10,f26]) ).
fof(f201,plain,
! [X0] : multiply(multiply(X0,sF5),multiply(X0,b)) = multiply(multiply(sF5,X0),sF6),
inference(superposition,[],[f11,f26]) ).
fof(f215,plain,
! [X0,X1] : one = multiply(X0,multiply(multiply(X0,X1),X1)),
inference(superposition,[],[f10,f9]) ).
fof(f219,plain,
multiply(sF0,multiply(a,b)) = multiply(sF4,one),
inference(superposition,[],[f88,f9]) ).
fof(f220,plain,
one = multiply(sF0,multiply(a,b)),
inference(forward_demodulation,[],[f219,f2]) ).
fof(f231,plain,
one = multiply(a,sF1),
inference(forward_demodulation,[],[f220,f175]) ).
fof(f233,plain,
! [X2,X0,X1] : one = multiply(multiply(X0,X2),multiply(X0,multiply(X1,X2))),
inference(superposition,[],[f74,f10]) ).
fof(f240,plain,
one = multiply(b,sF0),
inference(superposition,[],[f74,f14]) ).
fof(f241,plain,
one = multiply(a,sF4),
inference(superposition,[],[f74,f22]) ).
fof(f244,plain,
one = multiply(a,sF3),
inference(superposition,[],[f74,f20]) ).
fof(f258,plain,
! [X2,X0,X1] : one = multiply(multiply(multiply(X0,X1),X2),multiply(one,multiply(X1,X2))),
inference(superposition,[],[f5,f74]) ).
fof(f278,plain,
! [X2,X0,X1] : one = multiply(multiply(multiply(X0,X1),X2),multiply(X1,X2)),
inference(forward_demodulation,[],[f258,f3]) ).
fof(f318,plain,
! [X2,X0,X1] :
( one != one
| one != multiply(multiply(multiply(X2,X0),multiply(X2,X1)),multiply(X0,X1))
| multiply(X0,X1) = multiply(multiply(X2,X0),multiply(X2,X1)) ),
inference(superposition,[],[f7,f5]) ).
fof(f328,plain,
! [X2,X0,X1] :
( one != multiply(multiply(multiply(X2,X0),multiply(X2,X1)),multiply(X0,X1))
| multiply(X0,X1) = multiply(multiply(X2,X0),multiply(X2,X1)) ),
inference(trivial_inequality_removal,[],[f318]) ).
fof(f337,definition,
( spl8_2
<=> one = multiply(b,sF5) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f338,plain,
( one = multiply(b,sF5)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f337]) ).
fof(f460,plain,
! [X2,X3,X0,X1] :
( one != multiply(multiply(multiply(X3,multiply(X1,X0)),multiply(X3,multiply(X1,X2))),multiply(multiply(X0,X1),multiply(X0,X2)))
| multiply(multiply(X0,X1),multiply(X0,X2)) = multiply(multiply(X3,multiply(X1,X0)),multiply(X3,multiply(X1,X2))) ),
inference(superposition,[],[f328,f11]) ).
fof(f527,plain,
! [X0] : multiply(sF0,multiply(a,X0)) = multiply(b,multiply(multiply(b,a),X0)),
inference(superposition,[],[f164,f14]) ).
fof(f530,plain,
! [X0] : multiply(sF2,multiply(sF1,X0)) = multiply(a,multiply(multiply(a,sF1),X0)),
inference(superposition,[],[f164,f18]) ).
fof(f546,plain,
! [X0] : multiply(multiply(a,X0),sF0) = multiply(X0,multiply(multiply(X0,a),b)),
inference(superposition,[],[f164,f14]) ).
fof(f547,plain,
! [X0] : multiply(multiply(b,X0),sF4) = multiply(X0,multiply(multiply(X0,b),a)),
inference(superposition,[],[f164,f22]) ).
fof(f548,plain,
! [X0] : multiply(multiply(sF0,X0),sF1) = multiply(X0,multiply(multiply(X0,sF0),b)),
inference(superposition,[],[f164,f16]) ).
fof(f550,plain,
! [X0] : multiply(multiply(sF2,X0),sF3) = multiply(X0,multiply(multiply(X0,sF2),a)),
inference(superposition,[],[f164,f20]) ).
fof(f585,plain,
! [X2,X0,X1] : multiply(X1,multiply(multiply(X1,X0),X2)) = multiply(X0,multiply(multiply(X0,X1),X2)),
inference(superposition,[],[f10,f164]) ).
fof(f631,plain,
! [X0] : multiply(sF2,multiply(sF1,X0)) = multiply(a,multiply(one,X0)),
inference(forward_demodulation,[],[f530,f231]) ).
fof(f634,plain,
! [X0] : multiply(sF0,multiply(a,X0)) = multiply(b,multiply(sF4,X0)),
inference(forward_demodulation,[],[f527,f22]) ).
fof(f645,plain,
! [X0] : multiply(a,X0) = multiply(sF2,multiply(sF1,X0)),
inference(forward_demodulation,[],[f631,f3]) ).
fof(f650,plain,
multiply(sF0,multiply(a,a)) = multiply(b,sF5),
inference(superposition,[],[f634,f24]) ).
fof(f681,plain,
multiply(sF0,one) = multiply(b,sF5),
inference(forward_demodulation,[],[f650,f9]) ).
fof(f683,plain,
one = multiply(b,sF5),
inference(forward_demodulation,[],[f681,f2]) ).
fof(f684,plain,
spl8_2,
inference(avatar_split_clause,[],[f683,f337]) ).
fof(f744,plain,
! [X2,X0,X1] : one = multiply(X1,multiply(multiply(multiply(X0,X1),X2),X2)),
inference(superposition,[],[f10,f278]) ).
fof(f746,plain,
! [X2,X3,X0,X1] : one = multiply(multiply(multiply(X0,X1),X2),multiply(one,multiply(multiply(multiply(X3,X0),X1),X2))),
inference(superposition,[],[f5,f278]) ).
fof(f776,plain,
! [X2,X3,X0,X1] : one = multiply(multiply(multiply(X0,X1),X2),multiply(multiply(multiply(X3,X0),X1),X2)),
inference(forward_demodulation,[],[f746,f3]) ).
fof(f1032,plain,
! [X0,X1] :
( one != one
| one != multiply(multiply(multiply(X0,X1),X1),X0)
| multiply(multiply(X0,X1),X1) = X0 ),
inference(superposition,[],[f7,f215]) ).
fof(f1054,plain,
! [X0,X1] :
( one != multiply(multiply(multiply(X0,X1),X1),X0)
| multiply(multiply(X0,X1),X1) = X0 ),
inference(trivial_inequality_removal,[],[f1032]) ).
fof(f1116,plain,
! [X0,X1] : multiply(X0,multiply(multiply(a,sF4),multiply(a,X1))) = multiply(sF5,multiply(X0,multiply(sF4,X1))),
inference(superposition,[],[f130,f24]) ).
fof(f1146,plain,
! [X2,X3,X0,X1] : multiply(X1,multiply(multiply(X3,X0),multiply(X3,X2))) = multiply(multiply(X0,X3),multiply(X0,multiply(X1,X2))),
inference(superposition,[],[f130,f10]) ).
fof(f1384,plain,
! [X0,X1] : multiply(sF5,multiply(X0,multiply(sF4,X1))) = multiply(X0,multiply(one,multiply(a,X1))),
inference(forward_demodulation,[],[f1116,f241]) ).
fof(f1428,plain,
! [X0,X1] : multiply(X0,multiply(a,X1)) = multiply(sF5,multiply(X0,multiply(sF4,X1))),
inference(forward_demodulation,[],[f1384,f3]) ).
fof(f1818,plain,
! [X2,X3,X0,X1] : multiply(multiply(X0,multiply(X1,X2)),multiply(X1,X3)) = multiply(X1,multiply(multiply(X1,multiply(X0,X2)),X3)),
inference(superposition,[],[f164,f158]) ).
fof(f2111,plain,
multiply(multiply(a,sF4),sF0) = multiply(sF4,multiply(sF5,b)),
inference(superposition,[],[f546,f24]) ).
fof(f2164,plain,
multiply(multiply(a,sF4),sF0) = multiply(sF4,sF6),
inference(forward_demodulation,[],[f2111,f26]) ).
fof(f2178,plain,
multiply(one,sF0) = multiply(sF4,sF6),
inference(forward_demodulation,[],[f2164,f241]) ).
fof(f2189,plain,
sF0 = multiply(sF4,sF6),
inference(forward_demodulation,[],[f2178,f3]) ).
fof(f2209,plain,
one = multiply(sF6,sF0),
inference(superposition,[],[f74,f2189]) ).
fof(f2240,plain,
multiply(multiply(b,sF0),sF4) = multiply(sF0,multiply(sF1,a)),
inference(superposition,[],[f547,f16]) ).
fof(f2297,plain,
multiply(multiply(b,sF0),sF4) = multiply(sF0,sF2),
inference(forward_demodulation,[],[f2240,f18]) ).
fof(f2311,plain,
multiply(one,sF4) = multiply(sF0,sF2),
inference(forward_demodulation,[],[f2297,f240]) ).
fof(f2318,plain,
sF4 = multiply(sF0,sF2),
inference(forward_demodulation,[],[f2311,f3]) ).
fof(f2334,plain,
one = multiply(sF2,sF4),
inference(superposition,[],[f74,f2318]) ).
fof(f2355,plain,
multiply(sF2,sF2) = multiply(sF1,sF3),
inference(superposition,[],[f191,f20]) ).
fof(f2356,plain,
multiply(sF4,sF2) = multiply(sF1,sF5),
inference(superposition,[],[f191,f24]) ).
fof(f2407,plain,
one = multiply(sF1,sF3),
inference(forward_demodulation,[],[f2355,f9]) ).
fof(f2536,plain,
multiply(sF0,sF6) = multiply(sF5,sF1),
inference(superposition,[],[f199,f16]) ).
fof(f2647,plain,
multiply(multiply(b,sF5),sF4) = multiply(sF6,multiply(sF5,a)),
inference(superposition,[],[f87,f26]) ).
fof(f2735,plain,
( multiply(one,sF4) = multiply(sF6,multiply(sF5,a))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2647,f338]) ).
fof(f2754,plain,
( sF4 = multiply(sF6,multiply(sF5,a))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f2735,f3]) ).
fof(f2823,plain,
multiply(sF2,sF4) = multiply(b,sF3),
inference(superposition,[],[f133,f20]) ).
fof(f2876,plain,
one = multiply(b,sF3),
inference(forward_demodulation,[],[f2823,f2334]) ).
fof(f3023,plain,
! [X0] : one = multiply(multiply(sF3,X0),multiply(one,multiply(sF1,X0))),
inference(superposition,[],[f5,f2407]) ).
fof(f3044,plain,
! [X0] :
( one != multiply(multiply(multiply(X0,sF1),multiply(X0,sF3)),one)
| one = multiply(multiply(X0,sF1),multiply(X0,sF3)) ),
inference(superposition,[],[f328,f2407]) ).
fof(f3050,plain,
! [X0] : one = multiply(multiply(X0,sF1),multiply(X0,sF3)),
inference(forward_subsumption_resolution,[],[f3044,f2]) ).
fof(f3077,plain,
! [X0] : one = multiply(multiply(sF3,X0),multiply(sF1,X0)),
inference(forward_demodulation,[],[f3023,f3]) ).
fof(f3959,plain,
multiply(multiply(sF0,sF6),sF1) = multiply(multiply(sF6,sF0),sF7),
inference(superposition,[],[f103,f16]) ).
fof(f4040,plain,
multiply(multiply(sF0,sF6),sF1) = multiply(one,sF7),
inference(forward_demodulation,[],[f3959,f2209]) ).
fof(f4057,plain,
sF7 = multiply(multiply(sF0,sF6),sF1),
inference(forward_demodulation,[],[f4040,f3]) ).
fof(f4281,plain,
( ! [X0] : multiply(multiply(sF5,b),multiply(sF5,X0)) = multiply(one,multiply(b,X0))
| ~ spl8_2 ),
inference(superposition,[],[f11,f338]) ).
fof(f4322,plain,
( ! [X0] : multiply(b,X0) = multiply(multiply(sF5,b),multiply(sF5,X0))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f4281,f3]) ).
fof(f4343,plain,
( ! [X0] : multiply(b,X0) = multiply(sF6,multiply(sF5,X0))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f4322,f26]) ).
fof(f4358,plain,
multiply(multiply(sF2,sF4),sF3) = multiply(multiply(sF4,sF2),sF5),
inference(superposition,[],[f109,f24]) ).
fof(f4386,plain,
multiply(multiply(sF4,sF2),multiply(a,a)) = multiply(sF5,multiply(multiply(sF2,sF4),sF3)),
inference(superposition,[],[f1428,f109]) ).
fof(f4426,plain,
multiply(multiply(sF4,sF2),multiply(a,a)) = multiply(sF5,multiply(one,sF3)),
inference(forward_demodulation,[],[f4386,f2334]) ).
fof(f4440,plain,
multiply(multiply(sF2,sF4),sF3) = multiply(multiply(sF1,sF5),sF5),
inference(forward_demodulation,[],[f4358,f2356]) ).
fof(f4453,plain,
multiply(multiply(sF4,sF2),multiply(a,a)) = multiply(sF5,sF3),
inference(forward_demodulation,[],[f4426,f3]) ).
fof(f4460,plain,
multiply(one,sF3) = multiply(multiply(sF1,sF5),sF5),
inference(forward_demodulation,[],[f4440,f2334]) ).
fof(f4465,plain,
multiply(sF5,sF3) = multiply(multiply(sF4,sF2),one),
inference(forward_demodulation,[],[f4453,f9]) ).
fof(f4468,plain,
sF3 = multiply(multiply(sF1,sF5),sF5),
inference(forward_demodulation,[],[f4460,f3]) ).
fof(f4471,plain,
one = multiply(sF5,sF3),
inference(forward_demodulation,[],[f4465,f2]) ).
fof(f4499,plain,
! [X0] : multiply(sF3,multiply(multiply(sF1,sF5),X0)) = multiply(sF5,multiply(multiply(sF5,multiply(sF1,sF5)),X0)),
inference(superposition,[],[f164,f4468]) ).
fof(f4507,plain,
! [X0] : multiply(sF3,multiply(multiply(sF1,sF5),X0)) = multiply(sF5,multiply(one,X0)),
inference(forward_demodulation,[],[f4499,f74]) ).
fof(f4518,plain,
! [X0] : multiply(sF5,X0) = multiply(sF3,multiply(multiply(sF1,sF5),X0)),
inference(forward_demodulation,[],[f4507,f3]) ).
fof(f5669,plain,
! [X0] : multiply(sF2,multiply(multiply(sF2,sF4),X0)) = multiply(sF4,multiply(multiply(sF1,sF5),X0)),
inference(superposition,[],[f585,f2356]) ).
fof(f5887,plain,
! [X0] : multiply(sF2,multiply(one,X0)) = multiply(sF4,multiply(multiply(sF1,sF5),X0)),
inference(forward_demodulation,[],[f5669,f2334]) ).
fof(f5930,plain,
! [X0] : multiply(sF2,X0) = multiply(sF4,multiply(multiply(sF1,sF5),X0)),
inference(forward_demodulation,[],[f5887,f3]) ).
fof(f5950,plain,
! [X0] : one = multiply(multiply(sF3,X0),multiply(one,multiply(b,X0))),
inference(superposition,[],[f5,f2876]) ).
fof(f6020,plain,
! [X0] : one = multiply(multiply(sF3,X0),multiply(b,X0)),
inference(forward_demodulation,[],[f5950,f3]) ).
fof(f6992,plain,
! [X0] : multiply(sF0,multiply(multiply(sF0,b),X0)) = multiply(b,multiply(one,X0)),
inference(superposition,[],[f585,f240]) ).
fof(f7006,plain,
! [X0] : multiply(b,X0) = multiply(sF0,multiply(multiply(sF0,b),X0)),
inference(forward_demodulation,[],[f6992,f3]) ).
fof(f7042,plain,
! [X0] : multiply(b,X0) = multiply(sF0,multiply(sF1,X0)),
inference(forward_demodulation,[],[f7006,f16]) ).
fof(f10662,plain,
one = multiply(multiply(sF3,a),sF4),
inference(superposition,[],[f6020,f22]) ).
fof(f10878,plain,
! [X0] : multiply(one,multiply(sF6,X0)) = multiply(multiply(sF0,sF6),multiply(sF0,X0)),
inference(superposition,[],[f11,f2209]) ).
fof(f10949,plain,
! [X0] : multiply(sF6,X0) = multiply(multiply(sF0,sF6),multiply(sF0,X0)),
inference(forward_demodulation,[],[f10878,f3]) ).
fof(f11857,plain,
( one != multiply(multiply(sF3,sF5),multiply(sF1,sF5))
| multiply(sF1,sF5) = multiply(sF3,sF5) ),
inference(superposition,[],[f1054,f4468]) ).
fof(f11875,plain,
( one != multiply(multiply(sF1,b),sF0)
| sF0 = multiply(sF1,b) ),
inference(superposition,[],[f1054,f16]) ).
fof(f11893,plain,
( one != multiply(multiply(sF5,a),sF4)
| sF4 = multiply(sF5,a) ),
inference(superposition,[],[f1054,f24]) ).
fof(f11986,definition,
( spl8_64
<=> sF4 = multiply(sF5,a) ),
introduced(definition,[new_symbols(definition,[spl8_64])],[avatar_definition]) ).
fof(f11988,plain,
( sF4 = multiply(sF5,a)
| ~ spl8_64 ),
inference(avatar_component_clause,[],[f11986]) ).
fof(f11990,definition,
( spl8_65
<=> one = multiply(multiply(sF5,a),sF4) ),
introduced(definition,[new_symbols(definition,[spl8_65])],[avatar_definition]) ).
fof(f11992,plain,
( one != multiply(multiply(sF5,a),sF4)
| spl8_65 ),
inference(avatar_component_clause,[],[f11990]) ).
fof(f11993,plain,
( spl8_64
| ~ spl8_65 ),
inference(avatar_split_clause,[],[f11893,f11990,f11986]) ).
fof(f12019,definition,
( spl8_70
<=> sF0 = multiply(sF1,b) ),
introduced(definition,[new_symbols(definition,[spl8_70])],[avatar_definition]) ).
fof(f12021,plain,
( sF0 = multiply(sF1,b)
| ~ spl8_70 ),
inference(avatar_component_clause,[],[f12019]) ).
fof(f12023,definition,
( spl8_71
<=> one = multiply(multiply(sF1,b),sF0) ),
introduced(definition,[new_symbols(definition,[spl8_71])],[avatar_definition]) ).
fof(f12025,plain,
( one != multiply(multiply(sF1,b),sF0)
| spl8_71 ),
inference(avatar_component_clause,[],[f12023]) ).
fof(f12026,plain,
( spl8_70
| ~ spl8_71 ),
inference(avatar_split_clause,[],[f11875,f12023,f12019]) ).
fof(f12051,plain,
multiply(sF1,sF5) = multiply(sF3,sF5),
inference(forward_subsumption_resolution,[],[f11857,f3077]) ).
fof(f14045,plain,
( one = multiply(multiply(sF5,a),sF4)
| ~ spl8_2 ),
inference(superposition,[],[f74,f2754]) ).
fof(f14099,plain,
( $false
| ~ spl8_2
| spl8_65 ),
inference(forward_subsumption_resolution,[],[f14045,f11992]) ).
fof(f14100,plain,
( ~ spl8_2
| spl8_65 ),
inference(avatar_contradiction_clause,[],[f14099]) ).
fof(f14162,plain,
( ! [X0] : multiply(multiply(X0,sF5),multiply(X0,a)) = multiply(multiply(sF5,X0),sF4)
| ~ spl8_64 ),
inference(superposition,[],[f11,f11988]) ).
fof(f14171,plain,
( ! [X0,X1] : multiply(X1,multiply(multiply(X0,sF5),multiply(X0,a))) = multiply(multiply(sF5,X0),multiply(X1,sF4))
| ~ spl8_64 ),
inference(superposition,[],[f130,f11988]) ).
fof(f21013,plain,
one = multiply(multiply(sF1,b),multiply(one,sF0)),
inference(superposition,[],[f77,f231]) ).
fof(f21015,plain,
one = multiply(multiply(sF3,b),multiply(one,sF0)),
inference(superposition,[],[f77,f244]) ).
fof(f21201,plain,
one = multiply(multiply(sF3,b),sF0),
inference(forward_demodulation,[],[f21015,f3]) ).
fof(f21203,plain,
one = multiply(multiply(sF1,b),sF0),
inference(forward_demodulation,[],[f21013,f3]) ).
fof(f21248,plain,
( $false
| spl8_71 ),
inference(forward_subsumption_resolution,[],[f21203,f12025]) ).
fof(f21249,plain,
spl8_71,
inference(avatar_contradiction_clause,[],[f21248]) ).
fof(f21274,plain,
( multiply(a,b) = multiply(sF2,sF0)
| ~ spl8_70 ),
inference(superposition,[],[f645,f12021]) ).
fof(f21285,plain,
( multiply(multiply(sF5,sF1),sF6) = multiply(multiply(sF1,sF5),sF0)
| ~ spl8_70 ),
inference(superposition,[],[f201,f12021]) ).
fof(f21371,plain,
( multiply(multiply(sF0,sF6),sF6) = multiply(multiply(sF1,sF5),sF0)
| ~ spl8_70 ),
inference(forward_demodulation,[],[f21285,f2536]) ).
fof(f21378,plain,
( sF0 = multiply(sF2,sF0)
| ~ spl8_70 ),
inference(forward_demodulation,[],[f21274,f14]) ).
fof(f21461,plain,
( ! [X0] :
( one != multiply(multiply(multiply(sF2,X0),sF0),multiply(X0,sF0))
| multiply(X0,sF0) = multiply(multiply(sF2,X0),sF0) )
| ~ spl8_70 ),
inference(superposition,[],[f328,f21378]) ).
fof(f21496,plain,
( ! [X0] : multiply(X0,sF0) = multiply(multiply(sF2,X0),sF0)
| ~ spl8_70 ),
inference(forward_subsumption_resolution,[],[f21461,f278]) ).
fof(f21530,plain,
( multiply(one,sF0) = multiply(sF4,sF0)
| ~ spl8_70 ),
inference(superposition,[],[f21496,f2334]) ).
fof(f21661,plain,
( sF0 = multiply(sF4,sF0)
| ~ spl8_70 ),
inference(forward_demodulation,[],[f21530,f3]) ).
fof(f21723,plain,
( ! [X0] :
( one != multiply(multiply(multiply(sF4,X0),sF0),multiply(X0,sF0))
| multiply(X0,sF0) = multiply(multiply(sF4,X0),sF0) )
| ~ spl8_70 ),
inference(superposition,[],[f328,f21661]) ).
fof(f21757,plain,
( ! [X0] : multiply(X0,sF0) = multiply(multiply(sF4,X0),sF0)
| ~ spl8_70 ),
inference(forward_subsumption_resolution,[],[f21723,f278]) ).
fof(f21792,plain,
( multiply(sF2,sF0) = multiply(multiply(sF1,sF5),sF0)
| ~ spl8_70 ),
inference(superposition,[],[f21757,f2356]) ).
fof(f21941,plain,
( multiply(sF2,sF0) = multiply(multiply(sF0,sF6),sF6)
| ~ spl8_70 ),
inference(forward_demodulation,[],[f21792,f21371]) ).
fof(f21966,plain,
( sF0 = multiply(multiply(sF0,sF6),sF6)
| ~ spl8_70 ),
inference(forward_demodulation,[],[f21941,f21378]) ).
fof(f28228,plain,
! [X2,X0,X1] :
( one != one
| one != multiply(multiply(multiply(X1,X2),multiply(X0,X2)),multiply(X0,X1))
| multiply(X0,X1) = multiply(multiply(X1,X2),multiply(X0,X2)) ),
inference(superposition,[],[f7,f165]) ).
fof(f28288,plain,
! [X2,X0,X1] :
( one != multiply(multiply(multiply(X1,X2),multiply(X0,X2)),multiply(X0,X1))
| multiply(X0,X1) = multiply(multiply(X1,X2),multiply(X0,X2)) ),
inference(trivial_inequality_removal,[],[f28228]) ).
fof(f28345,plain,
! [X2,X0,X1] :
( one != multiply(X0,multiply(multiply(X0,multiply(multiply(X1,X2),X2)),X1))
| multiply(X0,X1) = multiply(multiply(X1,X2),multiply(X0,X2)) ),
inference(forward_demodulation,[],[f28288,f1818]) ).
fof(f28741,plain,
! [X2,X0,X1] :
( one != multiply(X0,multiply(multiply(X0,multiply(one,multiply(multiply(X1,X2),X2))),X1))
| multiply(X0,X1) = multiply(one,multiply(X0,multiply(multiply(X1,X2),X2))) ),
inference(superposition,[],[f28345,f215]) ).
fof(f29123,plain,
! [X2,X0,X1] :
( one != multiply(X0,multiply(multiply(X0,multiply(multiply(X1,X2),X2)),X1))
| multiply(X0,X1) = multiply(one,multiply(X0,multiply(multiply(X1,X2),X2))) ),
inference(forward_demodulation,[],[f28741,f3]) ).
fof(f29229,plain,
! [X2,X0,X1] :
( one != multiply(X0,multiply(multiply(X0,multiply(multiply(X1,X2),X2)),X1))
| multiply(X0,X1) = multiply(X0,multiply(multiply(X1,X2),X2)) ),
inference(forward_demodulation,[],[f29123,f3]) ).
fof(f32176,plain,
( ! [X0] :
( one != multiply(multiply(multiply(sF6,multiply(sF5,X0)),sF4),multiply(multiply(X0,sF5),multiply(X0,a)))
| multiply(multiply(X0,sF5),multiply(X0,a)) = multiply(multiply(sF6,multiply(sF5,X0)),sF4) )
| ~ spl8_2 ),
inference(superposition,[],[f460,f2754]) ).
fof(f32684,plain,
( ! [X0] :
( one != multiply(multiply(sF5,X0),multiply(multiply(multiply(sF6,multiply(sF5,X0)),sF4),sF4))
| multiply(multiply(X0,sF5),multiply(X0,a)) = multiply(multiply(sF6,multiply(sF5,X0)),sF4) )
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f32176,f14171]) ).
fof(f33185,plain,
( ! [X0] : multiply(multiply(X0,sF5),multiply(X0,a)) = multiply(multiply(sF6,multiply(sF5,X0)),sF4)
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_subsumption_resolution,[],[f32684,f744]) ).
fof(f33599,plain,
( ! [X0] : multiply(multiply(b,X0),sF4) = multiply(multiply(X0,sF5),multiply(X0,a))
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f33185,f4343]) ).
fof(f33865,plain,
( ! [X0] : multiply(multiply(b,X0),sF4) = multiply(multiply(sF5,X0),sF4)
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f33599,f14162]) ).
fof(f52778,plain,
! [X0] : multiply(multiply(sF3,a),multiply(one,X0)) = multiply(sF4,multiply(multiply(sF4,multiply(sF3,a)),X0)),
inference(superposition,[],[f585,f10662]) ).
fof(f52852,plain,
! [X0] : multiply(multiply(sF3,a),multiply(one,X0)) = multiply(sF4,multiply(multiply(sF3,sF5),X0)),
inference(forward_demodulation,[],[f52778,f183]) ).
fof(f52965,plain,
! [X0] : multiply(sF4,multiply(multiply(sF1,sF5),X0)) = multiply(multiply(sF3,a),multiply(one,X0)),
inference(forward_demodulation,[],[f52852,f12051]) ).
fof(f53036,plain,
! [X0] : multiply(sF4,multiply(multiply(sF1,sF5),X0)) = multiply(multiply(sF3,a),X0),
inference(forward_demodulation,[],[f52965,f3]) ).
fof(f53083,plain,
! [X0] : multiply(sF2,X0) = multiply(multiply(sF3,a),X0),
inference(forward_demodulation,[],[f53036,f5930]) ).
fof(f53408,plain,
! [X0,X1] : multiply(X0,multiply(multiply(X0,multiply(sF3,a)),X1)) = multiply(sF2,multiply(multiply(multiply(sF3,a),X0),X1)),
inference(superposition,[],[f585,f53083]) ).
fof(f53532,plain,
! [X0,X1] : multiply(sF2,multiply(multiply(sF2,X0),X1)) = multiply(X0,multiply(multiply(X0,multiply(sF3,a)),X1)),
inference(forward_demodulation,[],[f53408,f53083]) ).
fof(f63866,plain,
! [X0] :
( one != multiply(X0,multiply(multiply(X0,multiply(sF3,a)),sF2))
| multiply(X0,sF2) = multiply(X0,multiply(sF3,a)) ),
inference(superposition,[],[f29229,f20]) ).
fof(f64158,plain,
! [X0] :
( one != multiply(sF2,multiply(multiply(sF2,X0),sF2))
| multiply(X0,sF2) = multiply(X0,multiply(sF3,a)) ),
inference(forward_demodulation,[],[f63866,f53532]) ).
fof(f64313,plain,
! [X0] : multiply(X0,sF2) = multiply(X0,multiply(sF3,a)),
inference(forward_subsumption_resolution,[],[f64158,f74]) ).
fof(f64527,plain,
! [X0] : multiply(X0,sF2) = multiply(sF3,multiply(X0,a)),
inference(superposition,[],[f10,f64313]) ).
fof(f64703,plain,
multiply(multiply(b,sF3),sF4) = multiply(multiply(sF3,b),sF2),
inference(superposition,[],[f87,f64313]) ).
fof(f64911,plain,
( multiply(multiply(sF3,b),sF2) = multiply(multiply(sF5,sF3),sF4)
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f64703,f33865]) ).
fof(f65121,plain,
( multiply(one,sF4) = multiply(multiply(sF3,b),sF2)
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f64911,f4471]) ).
fof(f65226,plain,
( sF4 = multiply(multiply(sF3,b),sF2)
| ~ spl8_2
| ~ spl8_64 ),
inference(forward_demodulation,[],[f65121,f3]) ).
fof(f66382,plain,
multiply(sF5,multiply(multiply(multiply(sF1,sF5),sF0),b)) = multiply(sF3,multiply(multiply(sF0,multiply(sF1,sF5)),sF1)),
inference(superposition,[],[f4518,f548]) ).
fof(f66600,plain,
multiply(sF5,multiply(multiply(multiply(sF1,sF5),sF0),b)) = multiply(sF3,multiply(multiply(b,sF5),sF1)),
inference(forward_demodulation,[],[f66382,f7042]) ).
fof(f66644,plain,
( multiply(sF5,multiply(multiply(multiply(sF1,sF5),sF0),b)) = multiply(sF3,multiply(one,sF1))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f66600,f338]) ).
fof(f66659,plain,
( multiply(sF3,sF1) = multiply(sF5,multiply(multiply(multiply(sF1,sF5),sF0),b))
| ~ spl8_2 ),
inference(forward_demodulation,[],[f66644,f3]) ).
fof(f66669,plain,
( multiply(sF3,sF1) = multiply(multiply(multiply(sF1,sF5),sF0),sF6)
| ~ spl8_2 ),
inference(forward_demodulation,[],[f66659,f199]) ).
fof(f66672,plain,
( multiply(sF3,sF1) = multiply(multiply(multiply(sF0,sF6),sF6),sF6)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66669,f21371]) ).
fof(f66674,plain,
( multiply(sF0,sF6) = multiply(sF3,sF1)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66672,f21966]) ).
fof(f66683,plain,
( multiply(multiply(sF1,sF3),sF2) = multiply(multiply(sF0,sF6),multiply(sF3,a))
| ~ spl8_2
| ~ spl8_70 ),
inference(superposition,[],[f193,f66674]) ).
fof(f66763,plain,
( one != multiply(multiply(multiply(sF0,sF6),sF1),sF3)
| sF3 = multiply(multiply(sF0,sF6),sF1)
| ~ spl8_2
| ~ spl8_70 ),
inference(superposition,[],[f1054,f66674]) ).
fof(f66811,plain,
( one != multiply(sF7,sF3)
| sF3 = multiply(multiply(sF0,sF6),sF1)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66763,f4057]) ).
fof(f66837,plain,
( multiply(multiply(sF1,sF3),sF2) = multiply(multiply(sF0,sF6),sF2)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66683,f64313]) ).
fof(f66849,plain,
( sF3 = sF7
| one != multiply(sF7,sF3)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66811,f4057]) ).
fof(f66868,plain,
( multiply(one,sF2) = multiply(multiply(sF0,sF6),sF2)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66837,f2407]) ).
fof(f66879,plain,
( one != multiply(sF7,sF3)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_subsumption_resolution,[],[f66849,f29]) ).
fof(f66887,plain,
( sF2 = multiply(multiply(sF0,sF6),sF2)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f66868,f3]) ).
fof(f76521,plain,
! [X0,X1] : one = multiply(multiply(X0,multiply(multiply(X1,X0),X1)),multiply(X0,X1)),
inference(superposition,[],[f164,f776]) ).
fof(f79928,plain,
! [X0,X1] : multiply(X0,multiply(one,multiply(multiply(sF3,b),X1))) = multiply(multiply(sF0,multiply(sF3,b)),multiply(sF0,multiply(X0,X1))),
inference(superposition,[],[f1146,f21201]) ).
fof(f80004,plain,
! [X0,X1] : multiply(X0,multiply(one,multiply(multiply(sF3,b),X1))) = multiply(multiply(sF3,sF1),multiply(sF0,multiply(X0,X1))),
inference(forward_demodulation,[],[f79928,f175]) ).
fof(f80142,plain,
( ! [X0,X1] : multiply(multiply(sF0,sF6),multiply(sF0,multiply(X0,X1))) = multiply(X0,multiply(one,multiply(multiply(sF3,b),X1)))
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f80004,f66674]) ).
fof(f80229,plain,
( ! [X0,X1] : multiply(multiply(sF0,sF6),multiply(sF0,multiply(X0,X1))) = multiply(X0,multiply(multiply(sF3,b),X1))
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f80142,f3]) ).
fof(f80285,plain,
( ! [X0,X1] : multiply(sF6,multiply(X0,X1)) = multiply(X0,multiply(multiply(sF3,b),X1))
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f80229,f10949]) ).
fof(f80853,plain,
( multiply(sF6,multiply(sF3,a)) = multiply(multiply(sF3,b),sF2)
| ~ spl8_2
| ~ spl8_70 ),
inference(superposition,[],[f64527,f80285]) ).
fof(f80908,plain,
( sF4 = multiply(sF6,multiply(sF3,a))
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f80853,f65226]) ).
fof(f81371,plain,
( sF4 = multiply(sF6,sF2)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f80908,f64313]) ).
fof(f90782,plain,
! [X0,X1] :
( one != one
| one != multiply(multiply(X0,X1),multiply(X0,multiply(multiply(X1,X0),X1)))
| multiply(X0,X1) = multiply(X0,multiply(multiply(X1,X0),X1)) ),
inference(superposition,[],[f7,f76521]) ).
fof(f90912,plain,
! [X0,X1] :
( one != multiply(multiply(X0,X1),multiply(X0,multiply(multiply(X1,X0),X1)))
| multiply(X0,X1) = multiply(X0,multiply(multiply(X1,X0),X1)) ),
inference(trivial_inequality_removal,[],[f90782]) ).
fof(f91042,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,multiply(multiply(X1,X0),X1)),
inference(forward_subsumption_resolution,[],[f90912,f233]) ).
fof(f92329,plain,
( multiply(sF2,sF6) = multiply(sF2,multiply(sF4,sF6))
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(superposition,[],[f91042,f81371]) ).
fof(f92799,plain,
( multiply(sF2,sF0) = multiply(sF2,sF6)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f92329,f2189]) ).
fof(f92924,plain,
( sF0 = multiply(sF2,sF6)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f92799,f21378]) ).
fof(f92998,plain,
( ! [X0] : multiply(X0,sF0) = multiply(sF2,multiply(X0,sF6))
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(superposition,[],[f10,f92924]) ).
fof(f262235,plain,
( multiply(multiply(sF2,multiply(sF0,sF6)),sF3) = multiply(multiply(sF0,sF6),multiply(sF2,a))
| ~ spl8_2
| ~ spl8_70 ),
inference(superposition,[],[f550,f66887]) ).
fof(f262572,plain,
( multiply(multiply(sF0,sF6),sF3) = multiply(multiply(sF2,multiply(sF0,sF6)),sF3)
| ~ spl8_2
| ~ spl8_70 ),
inference(forward_demodulation,[],[f262235,f20]) ).
fof(f262690,plain,
( multiply(multiply(sF0,sF6),sF3) = multiply(multiply(sF0,sF0),sF3)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f262572,f92998]) ).
fof(f262772,plain,
( multiply(one,sF3) = multiply(multiply(sF0,sF6),sF3)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f262690,f9]) ).
fof(f262825,plain,
( sF3 = multiply(multiply(sF0,sF6),sF3)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f262772,f3]) ).
fof(f262959,plain,
( one = multiply(multiply(multiply(sF0,sF6),sF1),sF3)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(superposition,[],[f3050,f262825]) ).
fof(f263279,plain,
( one = multiply(sF7,sF3)
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_demodulation,[],[f262959,f4057]) ).
fof(f263378,plain,
( $false
| ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(forward_subsumption_resolution,[],[f263279,f66879]) ).
fof(f263379,plain,
( ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(avatar_contradiction_clause,[],[f263378]) ).
cnf(s9,plain,
spl8_2,
inference(sat_conversion,[],[f684]) ).
cnf(s31,plain,
( spl8_64
| ~ spl8_65 ),
inference(sat_conversion,[],[f11993]) ).
cnf(s34,plain,
( spl8_70
| ~ spl8_71 ),
inference(sat_conversion,[],[f12026]) ).
cnf(s43,plain,
( ~ spl8_2
| spl8_65 ),
inference(sat_conversion,[],[f14100]) ).
cnf(s47,plain,
spl8_71,
inference(sat_conversion,[],[f21249]) ).
cnf(s215,plain,
( ~ spl8_2
| ~ spl8_64
| ~ spl8_70 ),
inference(sat_conversion,[],[f263379]) ).
cnf(s217,plain,
spl8_70,
inference(rat,[],[s34,s47]) ).
cnf(s218,plain,
~ spl8_64,
inference(rat,[],[s215,s217,s9]) ).
cnf(s220,plain,
spl8_65,
inference(rat,[],[s43,s9]) ).
cnf(s221,plain,
$false,
inference(rat,[],[s31,s220,s218]) ).
fof(f263551,plain,
$false,
inference(avatar_sat_refutation,[],[s221]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG010-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.28 % Computer : n001.cluster.edu
% 0.13/0.28 % Model : x86_64 x86_64
% 0.13/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.28 % Memory : 8046.5625MB
% 0.13/0.28 % OS : Linux 6.8.0-71-generic
% 0.13/0.28 % CPULimit : 300
% 0.13/0.28 % WCLimit : 300
% 0.13/0.28 % DateTime : Mon Sep 28 19:23:04 UTC 2026
% 0.13/0.29 % CPUTime :
% 0.13/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.28/0.36 Running first-order theorem proving
% 0.28/0.36 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
% 21.18/3.96 % (643079)Input is clausal, will run a generic CNF schedule.
% 21.18/3.96 % (643090)dis-21_1_sil=8000:lcm=predicate:random_seed=986644142: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)
% 21.18/3.96 % (643086)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=598547013:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 21.18/3.96 % (643085)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1257702678:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 21.18/3.96 % (643084)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=880303888:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 21.18/3.96 % (643090)Instruction limit reached!
% 21.18/3.96 % (643090)------------------------------
% 21.18/3.96 % (643090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.96 % (643090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.96 % (643090)CaDiCaL version: 2.1.3
% 21.18/3.96 % (643090)Termination reason: Instruction limit
% 21.18/3.96 % (643090)Termination phase: Saturation
% 21.18/3.96 % (643090)Time elapsed: 0.048 s
% 21.18/3.96 % (643090)Peak memory usage: 88 MB
% 21.18/3.96 % (643090)Instructions burned: 118 (million)
% 21.18/3.96 % (643087)lrs+10_1_sil=8000:sp=occurrence:random_seed=2367724721:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 21.18/3.96 % (643088)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2232561643:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 21.18/3.96 % (643089)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3671001098:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 21.18/3.96 % (643087)Instruction limit reached!
% 21.18/3.96 % (643087)------------------------------
% 21.18/3.96 % (643087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.96 % (643087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.96 % (643087)CaDiCaL version: 2.1.3
% 21.18/3.96 % (643087)Termination reason: Instruction limit
% 21.18/3.96 % (643087)Termination phase: Saturation
% 21.18/3.96 % (643087)Time elapsed: 0.106 s
% 21.18/3.96 % (643087)Peak memory usage: 89 MB
% 21.18/3.96 % (643087)Instructions burned: 108 (million)
% 21.18/3.96 % (643088)Instruction limit reached!
% 21.18/3.96 % (643088)------------------------------
% 21.18/3.96 % (643088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.96 % (643088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.96 % (643088)CaDiCaL version: 2.1.3
% 21.18/3.96 % (643088)Termination reason: Instruction limit
% 21.18/3.96 % (643088)Termination phase: Saturation
% 21.18/3.96 % (643088)Time elapsed: 0.108 s
% 21.18/3.96 % (643088)Peak memory usage: 88 MB
% 21.18/3.96 % (643088)Instructions burned: 115 (million)
% 21.18/3.96 % (643089)Instruction limit reached!
% 21.18/3.96 % (643089)------------------------------
% 21.18/3.96 % (643089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.96 % (643089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.96 % (643089)CaDiCaL version: 2.1.3
% 21.18/3.96 % (643089)Termination reason: Instruction limit
% 21.18/3.96 % (643089)Termination phase: Saturation
% 21.18/3.96 % (643089)Time elapsed: 0.167 s
% 21.18/3.96 % (643089)Peak memory usage: 89 MB
% 21.18/3.96 % (643089)Instructions burned: 181 (million)
% 21.18/3.96 % (643096)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=1401018252:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 21.18/3.96 % (643096)Refutation not found, incomplete strategy
% 21.18/3.96 % (643096)------------------------------
% 21.18/3.96 % (643096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.18/3.96 % (643096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.18/3.96 % (643096)CaDiCaL version: 2.1.3
% 21.18/3.96 % (643096)Termination reason: Refutation not found, incomplete strategy
% 21.18/3.96 % (643096)Time elapsed: 0.001 s
% 21.18/3.96 % (643096)Peak memory usage: 88 MB
% 21.18/3.96 % (643100)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1219520512:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 39.28/6.49 % (643099)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1263050850:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 39.28/6.49 % (643100)Refutation not found, incomplete strategy
% 39.28/6.49 % (643100)------------------------------
% 39.28/6.49 % (643100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.28/6.49 % (643100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.49 % (643100)CaDiCaL version: 2.1.3
% 39.28/6.49 % (643100)Termination reason: Refutation not found, incomplete strategy
% 39.28/6.49 % (643100)Time elapsed: 0.002 s
% 39.28/6.49 % (643100)Peak memory usage: 87 MB
% 39.28/6.49 % (643099)Refutation not found, incomplete strategy
% 39.28/6.49 % (643099)------------------------------
% 39.28/6.49 % (643099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.28/6.49 % (643099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.49 % (643099)CaDiCaL version: 2.1.3
% 39.28/6.49 % (643099)Termination reason: Refutation not found, incomplete strategy
% 39.28/6.49 % (643099)Time elapsed: 0.002 s
% 39.28/6.49 % (643099)Peak memory usage: 88 MB
% 39.28/6.49 % (643099)Instructions burned: 1 (million)
% 39.28/6.49 % (643096)------------------------------
% 39.28/6.49 % (643096)------------------------------
% 39.28/6.49 % (643101)lrs+10_64_to=lpo:sil=8000:random_seed=404987665:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 39.28/6.49 % (643101)Instruction limit reached!
% 39.28/6.49 % (643101)------------------------------
% 39.28/6.49 % (643101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.28/6.49 % (643101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.49 % (643101)CaDiCaL version: 2.1.3
% 39.28/6.49 % (643101)Termination reason: Instruction limit
% 39.28/6.49 % (643101)Termination phase: Saturation
% 39.28/6.49 % (643101)Time elapsed: 0.116 s
% 39.28/6.49 % (643101)Peak memory usage: 88 MB
% 39.28/6.49 % (643101)Instructions burned: 126 (million)
% 39.28/6.49 % (643105)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2894512073:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 39.28/6.49 % (643100)------------------------------
% 39.28/6.49 % (643100)------------------------------
% 39.28/6.49 % (643099)------------------------------
% 39.28/6.49 % (643099)------------------------------
% 39.28/6.49 % (643105)Instruction limit reached!
% 39.28/6.49 % (643105)------------------------------
% 39.28/6.49 % (643105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.28/6.49 % (643105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.49 % (643105)CaDiCaL version: 2.1.3
% 39.28/6.49 % (643105)Termination reason: Instruction limit
% 39.28/6.49 % (643105)Termination phase: Saturation
% 39.28/6.49 % (643105)Time elapsed: 0.138 s
% 39.28/6.49 % (643105)Peak memory usage: 90 MB
% 39.28/6.49 % (643105)Instructions burned: 194 (million)
% 39.28/6.49 % (643107)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=488857575:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 39.28/6.49 % (643107)Instruction limit reached!
% 39.28/6.49 % (643107)------------------------------
% 39.28/6.49 % (643107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.28/6.49 % (643107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.28/6.49 % (643107)CaDiCaL version: 2.1.3
% 39.28/6.49 % (643107)Termination reason: Instruction limit
% 39.28/6.49 % (643107)Termination phase: Saturation
% 39.28/6.49 % (643107)Time elapsed: 0.163 s
% 39.28/6.49 % (643107)Peak memory usage: 90 MB
% 39.28/6.49 % (643107)Instructions burned: 157 (million)
% 39.28/6.49 % (643110)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=4216466686:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 39.28/6.49 % (643109)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3120140022:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 39.28/6.49 % (643112)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3539165555:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 39.28/6.49 % (643112)Refutation not found, incomplete strategy
% 39.28/6.49 % (643112)------------------------------
% 39.28/6.49 % (643112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643112)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643112)Termination reason: Refutation not found, incomplete strategy
% 76.01/11.66 % (643112)Time elapsed: 0.002 s
% 76.01/11.66 % (643112)Peak memory usage: 87 MB
% 76.01/11.66 % (643110)Instruction limit reached!
% 76.01/11.66 % (643110)------------------------------
% 76.01/11.66 % (643110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643110)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643110)Termination reason: Instruction limit
% 76.01/11.66 % (643110)Termination phase: Saturation
% 76.01/11.66 % (643110)Time elapsed: 0.101 s
% 76.01/11.66 % (643110)Peak memory usage: 89 MB
% 76.01/11.66 % (643110)Instructions burned: 107 (million)
% 76.01/11.66 % (643113)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3014835367:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 76.01/11.66 % (643117)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=396218945:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 76.01/11.66 % (643112)------------------------------
% 76.01/11.66 % (643112)------------------------------
% 76.01/11.66 % (643113)Instruction limit reached!
% 76.01/11.66 % (643113)------------------------------
% 76.01/11.66 % (643113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643113)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643113)Termination reason: Instruction limit
% 76.01/11.66 % (643113)Termination phase: Saturation
% 76.01/11.66 % (643113)Time elapsed: 0.242 s
% 76.01/11.66 % (643113)Peak memory usage: 90 MB
% 76.01/11.66 % (643113)Instructions burned: 242 (million)
% 76.01/11.66 % (643120)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=860839526:i=134:sd=2:doe=on:ss=axioms:sgt=14_2981 on theBenchmark for (2981ds/134Mi)
% 76.01/11.66 % (643121)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=490950542:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 76.01/11.66 % (643120)Instruction limit reached!
% 76.01/11.66 % (643120)------------------------------
% 76.01/11.66 % (643120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643120)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643120)Termination reason: Instruction limit
% 76.01/11.66 % (643120)Termination phase: Saturation
% 76.01/11.66 % (643120)Time elapsed: 0.124 s
% 76.01/11.66 % (643120)Peak memory usage: 89 MB
% 76.01/11.66 % (643120)Instructions burned: 135 (million)
% 76.01/11.66 % (643124)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=48194725:i=191:fgj=on:bd=all_2977 on theBenchmark for (2977ds/191Mi)
% 76.01/11.66 % (643121)Instruction limit reached!
% 76.01/11.66 % (643121)------------------------------
% 76.01/11.66 % (643121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643121)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643121)Termination reason: Instruction limit
% 76.01/11.66 % (643121)Termination phase: Saturation
% 76.01/11.66 % (643121)Time elapsed: 0.497 s
% 76.01/11.66 % (643121)Peak memory usage: 93 MB
% 76.01/11.66 % (643121)Instructions burned: 499 (million)
% 76.01/11.66 % (643124)Instruction limit reached!
% 76.01/11.66 % (643124)------------------------------
% 76.01/11.66 % (643124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 76.01/11.66 % (643124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.01/11.66 % (643124)CaDiCaL version: 2.1.3
% 76.01/11.66 % (643124)Termination reason: Instruction limit
% 76.01/11.66 % (643124)Termination phase: Saturation
% 76.01/11.66 % (643124)Time elapsed: 0.190 s
% 76.01/11.66 % (643124)Peak memory usage: 91 MB
% 76.01/11.66 % (643124)Instructions burned: 191 (million)
% 76.01/11.66 % (643126)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2587408805:i=264:kws=precedence:fsr=off_2973 on theBenchmark for (2973ds/264Mi)
% 76.01/11.66 % (643127)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3096732352:cond=on:i=156:bs=on:gtg=exists_all:er=known_2972 on theBenchmark for (2972ds/156Mi)
% 110.81/16.54 % (643127)Instruction limit reached!
% 110.81/16.54 % (643127)------------------------------
% 110.81/16.54 % (643127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643127)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643127)Termination reason: Instruction limit
% 110.81/16.54 % (643127)Termination phase: Saturation
% 110.81/16.54 % (643127)Time elapsed: 0.155 s
% 110.81/16.54 % (643127)Peak memory usage: 90 MB
% 110.81/16.54 % (643127)Instructions burned: 156 (million)
% 110.81/16.54 % (643126)Instruction limit reached!
% 110.81/16.54 % (643126)------------------------------
% 110.81/16.54 % (643126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643126)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643126)Termination reason: Instruction limit
% 110.81/16.54 % (643126)Termination phase: Saturation
% 110.81/16.54 % (643126)Time elapsed: 0.284 s
% 110.81/16.54 % (643126)Peak memory usage: 91 MB
% 110.81/16.54 % (643126)Instructions burned: 264 (million)
% 110.81/16.54 % (643130)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=1305725381:i=3256:kws=precedence:bd=preordered:av=off_2967 on theBenchmark for (2967ds/3256Mi)
% 110.81/16.54 % (643131)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1185526908:i=537:av=off:ss=included_2966 on theBenchmark for (2966ds/537Mi)
% 110.81/16.54 % (643131)Instruction limit reached!
% 110.81/16.54 % (643131)------------------------------
% 110.81/16.54 % (643131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643131)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643131)Termination reason: Instruction limit
% 110.81/16.54 % (643131)Termination phase: Saturation
% 110.81/16.54 % (643131)Time elapsed: 0.462 s
% 110.81/16.54 % (643131)Peak memory usage: 92 MB
% 110.81/16.54 % (643131)Instructions burned: 538 (million)
% 110.81/16.54 % (643134)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3264121513:i=180:bd=preordered:av=off_2959 on theBenchmark for (2959ds/180Mi)
% 110.81/16.54 % (643134)Instruction limit reached!
% 110.81/16.54 % (643134)------------------------------
% 110.81/16.54 % (643134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643134)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643134)Termination reason: Instruction limit
% 110.81/16.54 % (643134)Termination phase: Saturation
% 110.81/16.54 % (643134)Time elapsed: 0.154 s
% 110.81/16.54 % (643134)Peak memory usage: 88 MB
% 110.81/16.54 % (643134)Instructions burned: 181 (million)
% 110.81/16.54 % (643109)Instruction limit reached!
% 110.81/16.54 % (643109)------------------------------
% 110.81/16.54 % (643109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643109)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643109)Termination reason: Instruction limit
% 110.81/16.54 % (643109)Termination phase: Saturation
% 110.81/16.54 % (643109)Time elapsed: 3.448 s
% 110.81/16.54 % (643109)Peak memory usage: 152 MB
% 110.81/16.54 % (643109)Instructions burned: 3395 (million)
% 110.81/16.54 % (643136)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=3291211647:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2954 on theBenchmark for (2954ds/10307Mi)
% 110.81/16.54 % (643138)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=670483065:i=412:gtgl=4:gtg=exists_all_2951 on theBenchmark for (2951ds/412Mi)
% 110.81/16.54 % (643138)Instruction limit reached!
% 110.81/16.54 % (643138)------------------------------
% 110.81/16.54 % (643138)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 110.81/16.54 % (643138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 110.81/16.54 % (643138)CaDiCaL version: 2.1.3
% 110.81/16.54 % (643138)Termination reason: Instruction limit
% 110.81/16.54 % (643138)Termination phase: Saturation
% 110.81/16.54 % (643138)Time elapsed: 0.399 s
% 110.81/16.54 % (643138)Peak memory usage: 95 MB
% 143.70/21.23 % (643138)Instructions burned: 412 (million)
% 143.70/21.23 % (643140)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=3102330613:s2pl=no:i=8478:s2at=4:nm=6_2943 on theBenchmark for (2943ds/8478Mi)
% 143.70/21.23 % (643130)Instruction limit reached!
% 143.70/21.23 % (643130)------------------------------
% 143.70/21.23 % (643130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.70/21.23 % (643130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.70/21.23 % (643130)CaDiCaL version: 2.1.3
% 143.70/21.23 % (643130)Termination reason: Instruction limit
% 143.70/21.23 % (643130)Termination phase: Saturation
% 143.70/21.23 % (643130)Time elapsed: 3.253 s
% 143.70/21.23 % (643130)Peak memory usage: 149 MB
% 143.70/21.23 % (643130)Instructions burned: 3257 (million)
% 143.70/21.23 % (643117)Instruction limit reached!
% 143.70/21.23 % (643117)------------------------------
% 143.70/21.23 % (643117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.70/21.23 % (643117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.70/21.23 % (643117)CaDiCaL version: 2.1.3
% 143.70/21.23 % (643117)Termination reason: Instruction limit
% 143.70/21.23 % (643117)Termination phase: Saturation
% 143.70/21.23 % (643117)Time elapsed: 5.094 s
% 143.70/21.23 % (643117)Peak memory usage: 167 MB
% 143.70/21.23 % (643117)Instructions burned: 5208 (million)
% 143.70/21.23 % (643142)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=3386725656:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2932 on theBenchmark for (2932ds/303Mi)
% 143.70/21.23 % (643142)Refutation not found, incomplete strategy
% 143.70/21.23 % (643142)------------------------------
% 143.70/21.23 % (643142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.70/21.23 % (643142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.70/21.23 % (643142)CaDiCaL version: 2.1.3
% 143.70/21.23 % (643142)Termination reason: Refutation not found, incomplete strategy
% 143.70/21.23 % (643142)Time elapsed: 0.003 s
% 143.70/21.23 % (643142)Peak memory usage: 88 MB
% 143.70/21.23 % (643142)Instructions burned: 1 (million)
% 143.70/21.23 % (643143)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=855439255:st=4:i=720:sd=3:fsr=off:ss=axioms_2930 on theBenchmark for (2930ds/720Mi)
% 143.70/21.23 % (643143)Refutation not found, incomplete strategy
% 143.70/21.23 % (643143)------------------------------
% 143.70/21.23 % (643143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.70/21.23 % (643143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.70/21.23 % (643143)CaDiCaL version: 2.1.3
% 143.70/21.23 % (643143)Termination reason: Refutation not found, incomplete strategy
% 143.70/21.23 % (643143)Time elapsed: 0.002 s
% 143.70/21.23 % (643143)Peak memory usage: 87 MB
% 143.70/21.23 % (643143)Instructions burned: 1 (million)
% 143.70/21.23 % (643142)------------------------------
% 143.70/21.23 % (643142)------------------------------
% 143.70/21.23 % (643143)------------------------------
% 143.70/21.23 % (643143)------------------------------
% 143.70/21.23 % (643146)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=593774770:i=598:bs=on:bd=preordered:av=off:ss=axioms_2924 on theBenchmark for (2924ds/598Mi)
% 143.70/21.23 % (643147)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3056438213:i=2989:sd=3:ss=axioms:sgt=60_2923 on theBenchmark for (2923ds/2989Mi)
% 143.70/21.23 % (643146)Instruction limit reached!
% 143.70/21.23 % (643146)------------------------------
% 143.70/21.23 % (643146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 143.70/21.23 % (643146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 143.70/21.23 % (643146)CaDiCaL version: 2.1.3
% 143.70/21.23 % (643146)Termination reason: Instruction limit
% 143.70/21.23 % (643146)Termination phase: Saturation
% 143.70/21.23 % (643146)Time elapsed: 0.654 s
% 143.70/21.23 % (643146)Peak memory usage: 95 MB
% 143.70/21.23 % (643146)Instructions burned: 598 (million)
% 143.70/21.23 % (643150)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=4292731520:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2914 on theBenchmark for (2914ds/1997Mi)
% 143.70/21.23 % (643147)Instruction limit reached!
% 196.78/28.74 % (643147)------------------------------
% 196.78/28.74 % (643147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643147)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643147)Termination reason: Instruction limit
% 196.78/28.74 % (643147)Termination phase: Saturation
% 196.78/28.74 % (643147)Time elapsed: 2.861 s
% 196.78/28.74 % (643147)Peak memory usage: 147 MB
% 196.78/28.74 % (643147)Instructions burned: 2989 (million)
% 196.78/28.74 % (643150)Instruction limit reached!
% 196.78/28.74 % (643150)------------------------------
% 196.78/28.74 % (643150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643150)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643150)Termination reason: Instruction limit
% 196.78/28.74 % (643150)Termination phase: Saturation
% 196.78/28.74 % (643150)Time elapsed: 2.076 s
% 196.78/28.74 % (643150)Peak memory usage: 138 MB
% 196.78/28.74 % (643150)Instructions burned: 1997 (million)
% 196.78/28.74 % (643152)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=1388958836:i=2088:bd=preordered:av=off_2892 on theBenchmark for (2892ds/2088Mi)
% 196.78/28.74 % (643153)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2202216658:i=1098:nicw=on_2890 on theBenchmark for (2890ds/1098Mi)
% 196.78/28.74 % (643153)Instruction limit reached!
% 196.78/28.74 % (643153)------------------------------
% 196.78/28.74 % (643153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643153)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643153)Termination reason: Instruction limit
% 196.78/28.74 % (643153)Termination phase: Saturation
% 196.78/28.74 % (643153)Time elapsed: 1.079 s
% 196.78/28.74 % (643153)Peak memory usage: 102 MB
% 196.78/28.74 % (643153)Instructions burned: 1098 (million)
% 196.78/28.74 % (643156)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3141450755:i=433:bd=preordered_2876 on theBenchmark for (2876ds/433Mi)
% 196.78/28.74 % (643156)Refutation not found, incomplete strategy
% 196.78/28.74 % (643156)------------------------------
% 196.78/28.74 % (643156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643156)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643156)Termination reason: Refutation not found, incomplete strategy
% 196.78/28.74 % (643156)Time elapsed: 0.003 s
% 196.78/28.74 % (643156)Peak memory usage: 88 MB
% 196.78/28.74 % (643156)Instructions burned: 1 (million)
% 196.78/28.74 % (643156)------------------------------
% 196.78/28.74 % (643156)------------------------------
% 196.78/28.74 % (643152)Instruction limit reached!
% 196.78/28.74 % (643152)------------------------------
% 196.78/28.74 % (643152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643152)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643152)Termination reason: Instruction limit
% 196.78/28.74 % (643152)Termination phase: Saturation
% 196.78/28.74 % (643152)Time elapsed: 2.114 s
% 196.78/28.74 % (643152)Peak memory usage: 139 MB
% 196.78/28.74 % (643152)Instructions burned: 2089 (million)
% 196.78/28.74 % (643158)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=851707317:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2869 on theBenchmark for (2869ds/2942Mi)
% 196.78/28.74 % (643159)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3368466554:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2867 on theBenchmark for (2867ds/6922Mi)
% 196.78/28.74 % (643140)Instruction limit reached!
% 196.78/28.74 % (643140)------------------------------
% 196.78/28.74 % (643140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.78/28.74 % (643140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.78/28.74 % (643140)CaDiCaL version: 2.1.3
% 196.78/28.74 % (643140)Termination reason: Instruction limit
% 196.78/28.74 % (643140)Termination phase: Saturation
% 196.78/28.74 % (643140)Time elapsed: 9.752 s
% 196.78/28.74 % (643140)Peak memory usage: 168 MB
% 233.37/33.93 % (643140)Instructions burned: 8478 (million)
% 233.37/33.93 % (643163)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=3569460085:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2843 on theBenchmark for (2843ds/596Mi)
% 233.37/33.93 % (643163)Refutation not found, incomplete strategy
% 233.37/33.93 % (643163)------------------------------
% 233.37/33.93 % (643163)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.37/33.93 % (643163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.37/33.93 % (643163)CaDiCaL version: 2.1.3
% 233.37/33.93 % (643163)Termination reason: Refutation not found, incomplete strategy
% 233.37/33.93 % (643163)Time elapsed: 0.003 s
% 233.37/33.93 % (643163)Peak memory usage: 88 MB
% 233.37/33.93 % (643163)Instructions burned: 1 (million)
% 233.37/33.93 % (643136)Instruction limit reached!
% 233.37/33.93 % (643136)------------------------------
% 233.37/33.93 % (643136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.37/33.93 % (643136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.37/33.93 % (643136)CaDiCaL version: 2.1.3
% 233.37/33.93 % (643136)Termination reason: Instruction limit
% 233.37/33.93 % (643136)Termination phase: Saturation
% 233.37/33.93 % (643136)Time elapsed: 11.289 s
% 233.37/33.93 % (643136)Peak memory usage: 193 MB
% 233.37/33.93 % (643136)Instructions burned: 10307 (million)
% 233.37/33.93 % (643158)Instruction limit reached!
% 233.37/33.93 % (643158)------------------------------
% 233.37/33.93 % (643158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.37/33.93 % (643158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.37/33.93 % (643158)CaDiCaL version: 2.1.3
% 233.37/33.93 % (643158)Termination reason: Instruction limit
% 233.37/33.93 % (643158)Termination phase: Saturation
% 233.37/33.93 % (643158)Time elapsed: 3.005 s
% 233.37/33.93 % (643158)Peak memory usage: 148 MB
% 233.37/33.93 % (643158)Instructions burned: 2942 (million)
% 233.37/33.93 % (643163)------------------------------
% 233.37/33.93 % (643163)------------------------------
% 233.37/33.93 % (643165)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=82780572:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2838 on theBenchmark for (2838ds/4123Mi)
% 233.37/33.93 % (643166)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1703516712:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2836 on theBenchmark for (2836ds/16411Mi)
% 233.37/33.93 % (643167)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=705386238:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2836 on theBenchmark for (2836ds/1670Mi)
% 233.37/33.93 % (643167)Instruction limit reached!
% 233.37/33.93 % (643167)------------------------------
% 233.37/33.93 % (643167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.37/33.93 % (643167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.37/33.93 % (643167)CaDiCaL version: 2.1.3
% 233.37/33.93 % (643167)Termination reason: Instruction limit
% 233.37/33.93 % (643167)Termination phase: Saturation
% 233.37/33.93 % (643167)Time elapsed: 1.740 s
% 233.37/33.93 % (643167)Peak memory usage: 136 MB
% 233.37/33.93 % (643167)Instructions burned: 1670 (million)
% 233.37/33.93 % (643171)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=110429351:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2815 on theBenchmark for (2815ds/1722Mi)
% 233.37/33.93 % (643159)Instruction limit reached!
% 233.37/33.93 % (643159)------------------------------
% 233.37/33.93 % (643159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 233.37/33.93 % (643159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.37/33.93 % (643159)CaDiCaL version: 2.1.3
% 233.37/33.93 % (643159)Termination reason: Instruction limit
% 233.37/33.93 % (643159)Termination phase: Saturation
% 233.37/33.93 % (643159)Time elapsed: 6.511 s
% 233.37/33.93 % (643159)Peak memory usage: 153 MB
% 233.37/33.93 % (643159)Instructions burned: 6922 (million)
% 233.37/33.93 % (643173)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=2466042413:cts=off:cond=on:i=9530:bs=on:fsd=on_2799 on theBenchmark for (2799ds/9530Mi)
% 179.13/38.28 % (643171)Instruction limit reached!
% 179.13/38.28 % (643171)------------------------------
% 179.13/38.28 % (643171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643171)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643171)Termination reason: Instruction limit
% 179.13/38.28 % (643171)Termination phase: Saturation
% 179.13/38.28 % (643171)Time elapsed: 1.812 s
% 179.13/38.28 % (643171)Peak memory usage: 136 MB
% 179.13/38.28 % (643171)Instructions burned: 1723 (million)
% 179.13/38.28 % (643165)Instruction limit reached!
% 179.13/38.28 % (643165)------------------------------
% 179.13/38.28 % (643165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643165)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643165)Termination reason: Instruction limit
% 179.13/38.28 % (643165)Termination phase: Saturation
% 179.13/38.28 % (643165)Time elapsed: 4.186 s
% 179.13/38.28 % (643165)Peak memory usage: 157 MB
% 179.13/38.28 % (643165)Instructions burned: 4123 (million)
% 179.13/38.28 % (643175)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2089538891:st=2:i=4495:sd=10:ss=included_2794 on theBenchmark for (2794ds/4495Mi)
% 179.13/38.28 % (643176)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2186516495:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2793 on theBenchmark for (2793ds/4920Mi)
% 179.13/38.28 % (643175)Instruction limit reached!
% 179.13/38.28 % (643175)------------------------------
% 179.13/38.28 % (643175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643175)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643175)Termination reason: Instruction limit
% 179.13/38.28 % (643175)Termination phase: Saturation
% 179.13/38.28 % (643175)Time elapsed: 4.361 s
% 179.13/38.28 % (643175)Peak memory usage: 162 MB
% 179.13/38.28 % (643175)Instructions burned: 4496 (million)
% 179.13/38.28 % (643179)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1313042331:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2747 on theBenchmark for (2747ds/2083Mi)
% 179.13/38.28 % (643176)Instruction limit reached!
% 179.13/38.28 % (643176)------------------------------
% 179.13/38.28 % (643176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643176)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643176)Termination reason: Instruction limit
% 179.13/38.28 % (643176)Termination phase: Saturation
% 179.13/38.28 % (643176)Time elapsed: 4.796 s
% 179.13/38.28 % (643176)Peak memory usage: 158 MB
% 179.13/38.28 % (643176)Instructions burned: 4921 (million)
% 179.13/38.28 % (643181)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1957880655:i=4629:av=off:gsp=on_2742 on theBenchmark for (2742ds/4629Mi)
% 179.13/38.28 % (643181)Refutation not found, incomplete strategy
% 179.13/38.28 % (643181)------------------------------
% 179.13/38.28 % (643181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643181)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643181)Termination reason: Refutation not found, incomplete strategy
% 179.13/38.28 % (643181)Time elapsed: 0.884 s
% 179.13/38.28 % (643181)Peak memory usage: 127 MB
% 179.13/38.28 % (643181)Instructions burned: 858 (million)
% 179.13/38.28 % (643181)------------------------------
% 179.13/38.28 % (643181)------------------------------
% 179.13/38.28 % (643183)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=956683230:i=1258:av=off_2726 on theBenchmark for (2726ds/1258Mi)
% 179.13/38.28 % (643179)Instruction limit reached!
% 179.13/38.28 % (643179)------------------------------
% 179.13/38.28 % (643179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643179)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643179)Termination reason: Instruction limit
% 179.13/38.28 % (643179)Termination phase: Saturation
% 179.13/38.28 % (643179)Time elapsed: 2.266 s
% 179.13/38.28 % (643179)Peak memory usage: 138 MB
% 179.13/38.28 % (643179)Instructions burned: 2083 (million)
% 179.13/38.28 % (643185)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3502813633:i=7343:av=off:ss=included_2721 on theBenchmark for (2721ds/7343Mi)
% 179.13/38.28 % (643183)Instruction limit reached!
% 179.13/38.28 % (643183)------------------------------
% 179.13/38.28 % (643183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643183)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643183)Termination reason: Instruction limit
% 179.13/38.28 % (643183)Termination phase: Saturation
% 179.13/38.28 % (643183)Time elapsed: 1.231 s
% 179.13/38.28 % (643183)Peak memory usage: 102 MB
% 179.13/38.28 % (643183)Instructions burned: 1258 (million)
% 179.13/38.28 % (643187)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1217330697:i=1325:sd=2:ss=axioms:sgt=16_2711 on theBenchmark for (2711ds/1325Mi)
% 179.13/38.28 % (643187)Refutation not found, incomplete strategy
% 179.13/38.28 % (643187)------------------------------
% 179.13/38.28 % (643187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643187)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643187)Termination reason: Refutation not found, incomplete strategy
% 179.13/38.28 % (643187)Time elapsed: 0.002 s
% 179.13/38.28 % (643187)Peak memory usage: 87 MB
% 179.13/38.28 % (643187)------------------------------
% 179.13/38.28 % (643187)------------------------------
% 179.13/38.28 % (643198)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=982631614:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2704 on theBenchmark for (2704ds/2646Mi)
% 179.13/38.28 % (643173)Instruction limit reached!
% 179.13/38.28 % (643173)------------------------------
% 179.13/38.28 % (643173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643173)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643173)Termination reason: Instruction limit
% 179.13/38.28 % (643173)Termination phase: Saturation
% 179.13/38.28 % (643173)Time elapsed: 9.589 s
% 179.13/38.28 % (643173)Peak memory usage: 196 MB
% 179.13/38.28 % (643173)Instructions burned: 9530 (million)
% 179.13/38.28 % (643208)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1410464089:i=1489:sd=2:ep=R:ss=axioms_2700 on theBenchmark for (2700ds/1489Mi)
% 179.13/38.28 % (643208)Refutation not found, incomplete strategy
% 179.13/38.28 % (643208)------------------------------
% 179.13/38.28 % (643208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643208)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643208)Termination reason: Refutation not found, incomplete strategy
% 179.13/38.28 % (643208)Time elapsed: 1.154 s
% 179.13/38.28 % (643208)Peak memory usage: 127 MB
% 179.13/38.28 % (643208)Instructions burned: 851 (million)
% 179.13/38.28 % (643208)------------------------------
% 179.13/38.28 % (643208)------------------------------
% 179.13/38.28 % (643210)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3241677115:i=1503_2681 on theBenchmark for (2681ds/1503Mi)
% 179.13/38.28 % (643198)Instruction limit reached!
% 179.13/38.28 % (643198)------------------------------
% 179.13/38.28 % (643198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643198)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643198)Termination reason: Instruction limit
% 179.13/38.28 % (643198)Termination phase: Saturation
% 179.13/38.28 % (643198)Time elapsed: 2.801 s
% 179.13/38.28 % (643198)Peak memory usage: 145 MB
% 179.13/38.28 % (643198)Instructions burned: 2646 (million)
% 179.13/38.28 % (643212)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3344656688:i=13942:kws=frequency_2673 on theBenchmark for (2673ds/13942Mi)
% 179.13/38.28 % (643210)Refutation not found, incomplete strategy
% 179.13/38.28 % (643210)------------------------------
% 179.13/38.28 % (643210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643210)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643210)Termination reason: Refutation not found, incomplete strategy
% 179.13/38.28 % (643210)Time elapsed: 0.954 s
% 179.13/38.28 % (643210)Peak memory usage: 127 MB
% 179.13/38.28 % (643210)Instructions burned: 852 (million)
% 179.13/38.28 % (643210)------------------------------
% 179.13/38.28 % (643210)------------------------------
% 179.13/38.28 % (643214)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=435365599:i=3604:fsr=off:er=filter_2665 on theBenchmark for (2665ds/3604Mi)
% 179.13/38.28 % (643166)Instruction limit reached!
% 179.13/38.28 % (643166)------------------------------
% 179.13/38.28 % (643166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643166)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643166)Termination reason: Instruction limit
% 179.13/38.28 % (643166)Termination phase: Saturation
% 179.13/38.28 % (643166)Time elapsed: 17.754 s
% 179.13/38.28 % (643166)Peak memory usage: 230 MB
% 179.13/38.28 % (643166)Instructions burned: 16411 (million)
% 179.13/38.28 % (643216)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=3275542877:i=1876:sd=1:ss=included:sgt=32_2655 on theBenchmark for (2655ds/1876Mi)
% 179.13/38.28 % (643185)Instruction limit reached!
% 179.13/38.28 % (643185)------------------------------
% 179.13/38.28 % (643185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643185)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643185)Termination reason: Instruction limit
% 179.13/38.28 % (643185)Termination phase: Saturation
% 179.13/38.28 % (643185)Time elapsed: 7.387 s
% 179.13/38.28 % (643185)Peak memory usage: 189 MB
% 179.13/38.28 % (643185)Instructions burned: 7344 (million)
% 179.13/38.28 % (643218)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1518901637:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2643 on theBenchmark for (2643ds/1932Mi)
% 179.13/38.28 % (643216)Instruction limit reached!
% 179.13/38.28 % (643216)------------------------------
% 179.13/38.28 % (643216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643216)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643216)Termination reason: Instruction limit
% 179.13/38.28 % (643216)Termination phase: Saturation
% 179.13/38.28 % (643216)Time elapsed: 1.958 s
% 179.13/38.28 % (643216)Peak memory usage: 138 MB
% 179.13/38.28 % (643216)Instructions burned: 1877 (million)
% 179.13/38.28 % (643218)Refutation not found, incomplete strategy
% 179.13/38.28 % (643218)------------------------------
% 179.13/38.28 % (643218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 179.13/38.28 % (643218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 179.13/38.28 % (643218)CaDiCaL version: 2.1.3
% 179.13/38.28 % (643218)Termination reason: Refutation not found, incomplete strategy
% 179.13/38.28 % (643218)Time elapsed: 0.885 s
% 179.13/38.28 % (643218)Peak memory usage: 127 MB
% 179.13/38.28 % (643218)Instructions burned: 866 (million)
% 179.13/38.28 % (643084)First to succeed.
% 179.13/38.28 % (643084)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-643079"
% 179.13/38.28 % (643225)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=268530833:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2632 on theBenchmark for (2632ds/1980Mi)
% 179.13/38.28 % (643218)------------------------------
% 179.13/38.28 % (643218)------------------------------
% 179.13/38.28 % (643227)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=1859169720:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2629 on theBenchmark for (2629ds/3902Mi)
% 179.13/38.28 % (643084)Refutation found. Thanks to Tanya!
% 179.13/38.28 % SZS status Unsatisfiable for theBenchmark
% 179.13/38.28 % SZS output start Proof for theBenchmark
% See solution above
% 264.62/38.38 % (643084)------------------------------
% 264.62/38.38 % (643084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.62/38.38 % (643084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.62/38.38 % (643084)CaDiCaL version: 2.1.3
% 264.62/38.38 % (643084)Termination reason: Refutation
% 264.62/38.38 % (643084)Time elapsed: 36.610 s
% 264.62/38.38 % (643084)Peak memory usage: 431 MB
% 264.62/38.38 % (643084)Instructions burned: 35436 (million)
% 264.62/38.38 % (643084)------------------------------
% 264.62/38.38 % (643084)------------------------------
% 264.62/38.38 % (643079)Success in time 37.386 s
% 264.62/38.38 % Vampire exiting
%------------------------------------------------------------------------------