%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE149+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:40:29 AM UTC 2026
% Result : Theorem 252.41s 42.86s
% Output : Refutation 297.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 29
% Syntax : Number of formulae : 751 ( 647 unt; 10 def)
% Number of atoms : 871 ( 700 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 237 ( 117 ~; 112 |; 1 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 769 ( 0 sgn 767 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity1) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity2) ).
fof(f10,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_annihilation) ).
fof(f11,axiom,
! [X0] : addition(one,multiplication(X0,star(X0))) = star(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold1) ).
fof(f12,axiom,
! [X0] : addition(one,multiplication(star(X0),X0)) = star(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold2) ).
fof(f13,axiom,
! [X0,X1,X2] :
( leq(addition(multiplication(X0,X2),X1),X2)
=> leq(multiplication(star(X0),X1),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_induction1) ).
fof(f14,axiom,
! [X0,X1,X2] :
( leq(addition(multiplication(X2,X0),X1),X2)
=> leq(multiplication(X1,star(X0)),X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_induction2) ).
fof(f15,axiom,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infty_unfold1) ).
fof(f16,axiom,
! [X0,X1,X2] :
( leq(X2,addition(multiplication(X0,X2),X1))
=> leq(X2,multiplication(strong_iteration(X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',infty_coinduction) ).
fof(f17,axiom,
! [X0] : strong_iteration(X0) = addition(star(X0),multiplication(strong_iteration(X0),zero)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',isolation) ).
fof(f18,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> addition(X0,X1) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order) ).
fof(f19,conjecture,
! [X0,X1] : strong_iteration(addition(X0,X1)) = addition(multiplication(multiplication(star(X1),X0),strong_iteration(addition(X0,X1))),strong_iteration(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f20,negated_conjecture,
~ ! [X0,X1] : strong_iteration(addition(X0,X1)) = addition(multiplication(multiplication(star(X1),X0),strong_iteration(addition(X0,X1))),strong_iteration(X1)),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [X0,X1,X2] :
( leq(multiplication(star(X0),X1),X2)
| ~ leq(addition(multiplication(X0,X2),X1),X2) ),
inference(ennf_transformation,[],[f13]) ).
fof(f22,plain,
! [X0,X1,X2] :
( leq(multiplication(X1,star(X0)),X2)
| ~ leq(addition(multiplication(X2,X0),X1),X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f23,plain,
! [X0,X1,X2] :
( leq(X2,multiplication(strong_iteration(X0),X1))
| ~ leq(X2,addition(multiplication(X0,X2),X1)) ),
inference(ennf_transformation,[],[f16]) ).
fof(f24,plain,
? [X0,X1] : strong_iteration(addition(X0,X1)) != addition(multiplication(multiplication(star(X1),X0),strong_iteration(addition(X0,X1))),strong_iteration(X1)),
inference(ennf_transformation,[],[f20]) ).
fof(f25,plain,
! [X0,X1] :
( ( leq(X0,X1)
| addition(X0,X1) != X1 )
& ( addition(X0,X1) = X1
| ~ leq(X0,X1) ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f26,plain,
strong_iteration(addition(sK0,sK1)) != addition(multiplication(multiplication(star(sK1),sK0),strong_iteration(addition(sK0,sK1))),strong_iteration(sK1)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f24]) ).
fof(f27,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f28,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f29,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f30,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f31,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f33,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f34,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f35,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f36,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f10]) ).
fof(f37,plain,
! [X0] : star(X0) = addition(one,multiplication(X0,star(X0))),
inference(cnf_transformation,[],[f11]) ).
fof(f38,plain,
! [X0] : star(X0) = addition(one,multiplication(star(X0),X0)),
inference(cnf_transformation,[],[f12]) ).
fof(f39,plain,
! [X2,X0,X1] :
( ~ leq(addition(multiplication(X0,X2),X1),X2)
| leq(multiplication(star(X0),X1),X2) ),
inference(cnf_transformation,[],[f21]) ).
fof(f40,plain,
! [X2,X0,X1] :
( ~ leq(addition(multiplication(X2,X0),X1),X2)
| leq(multiplication(X1,star(X0)),X2) ),
inference(cnf_transformation,[],[f22]) ).
fof(f41,plain,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),one),
inference(cnf_transformation,[],[f15]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ leq(X2,addition(multiplication(X0,X2),X1))
| leq(X2,multiplication(strong_iteration(X0),X1)) ),
inference(cnf_transformation,[],[f23]) ).
fof(f43,plain,
! [X0] : strong_iteration(X0) = addition(star(X0),multiplication(strong_iteration(X0),zero)),
inference(cnf_transformation,[],[f17]) ).
fof(f44,plain,
! [X0,X1] :
( ~ leq(X0,X1)
| addition(X0,X1) = X1 ),
inference(cnf_transformation,[],[f25]) ).
fof(f45,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f46,plain,
strong_iteration(addition(sK0,sK1)) != addition(multiplication(multiplication(star(sK1),sK0),strong_iteration(addition(sK0,sK1))),strong_iteration(sK1)),
inference(cnf_transformation,[],[f26]) ).
fof(f47,definition,
sF2 = addition(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f48,plain,
addition(sK0,sK1) = sF2,
inference(reorient_equations,[],[f47]) ).
fof(f49,definition,
sF3 = strong_iteration(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f50,plain,
strong_iteration(sF2) = sF3,
inference(reorient_equations,[],[f49]) ).
fof(f51,definition,
sF4 = star(sK1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f52,plain,
star(sK1) = sF4,
inference(reorient_equations,[],[f51]) ).
fof(f53,definition,
sF5 = multiplication(sF4,sK0),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f54,plain,
multiplication(sF4,sK0) = sF5,
inference(reorient_equations,[],[f53]) ).
fof(f55,definition,
sF6 = multiplication(sF5,sF3),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f56,plain,
multiplication(sF5,sF3) = sF6,
inference(reorient_equations,[],[f55]) ).
fof(f57,definition,
sF7 = strong_iteration(sK1),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f58,plain,
strong_iteration(sK1) = sF7,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF8 = addition(sF6,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f60,plain,
addition(sF6,sF7) = sF8,
inference(reorient_equations,[],[f59]) ).
fof(f61,plain,
sF3 != sF8,
inference(definition_folding,[],[f46,f60,f58,f56,f50,f48,f54,f52,f50,f48]) ).
fof(f62,plain,
sF4 = addition(one,multiplication(sK1,sF4)),
inference(superposition,[],[f37,f52]) ).
fof(f66,plain,
sF2 = addition(sK1,sK0),
inference(superposition,[],[f48,f27]) ).
fof(f68,plain,
sF7 = addition(star(sK1),multiplication(sF7,zero)),
inference(superposition,[],[f43,f58]) ).
fof(f70,plain,
sF7 = addition(sF4,multiplication(sF7,zero)),
inference(forward_demodulation,[],[f68,f52]) ).
fof(f73,plain,
sF3 = addition(multiplication(sF2,sF3),one),
inference(superposition,[],[f41,f50]) ).
fof(f79,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f28,f27]) ).
fof(f81,plain,
! [X0,X1] : addition(multiplication(X0,strong_iteration(X0)),addition(one,X1)) = addition(strong_iteration(X0),X1),
inference(superposition,[],[f28,f41]) ).
fof(f82,plain,
! [X0,X1] : addition(one,addition(multiplication(X0,star(X0)),X1)) = addition(star(X0),X1),
inference(superposition,[],[f28,f37]) ).
fof(f83,plain,
! [X0,X1] : addition(strong_iteration(X0),X1) = addition(star(X0),addition(multiplication(strong_iteration(X0),zero),X1)),
inference(superposition,[],[f28,f43]) ).
fof(f84,plain,
! [X0] : addition(sK0,addition(sK1,X0)) = addition(sF2,X0),
inference(superposition,[],[f28,f48]) ).
fof(f86,plain,
! [X0] : addition(sF6,addition(sF7,X0)) = addition(sF8,X0),
inference(superposition,[],[f28,f60]) ).
fof(f90,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X2,addition(X0,X1)),
inference(superposition,[],[f27,f28]) ).
fof(f92,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(forward_demodulation,[],[f79,f28]) ).
fof(f99,plain,
! [X2,X0,X1] :
( ~ leq(X2,addition(X0,multiplication(X1,X2)))
| leq(X2,multiplication(strong_iteration(X1),X0)) ),
inference(superposition,[],[f42,f27]) ).
fof(f102,plain,
! [X0] : multiplication(addition(sF5,X0),sF3) = addition(sF6,multiplication(X0,sF3)),
inference(superposition,[],[f35,f56]) ).
fof(f108,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X2),addition(multiplication(X1,X2),X3)) = addition(multiplication(addition(X0,X1),X2),X3),
inference(superposition,[],[f28,f35]) ).
fof(f115,plain,
! [X0] : multiplication(sF4,multiplication(sK0,X0)) = multiplication(sF5,X0),
inference(superposition,[],[f31,f54]) ).
fof(f116,plain,
! [X0] : multiplication(sF5,multiplication(sF3,X0)) = multiplication(sF6,X0),
inference(superposition,[],[f31,f56]) ).
fof(f120,plain,
! [X2,X3,X0,X1] : multiplication(addition(X3,multiplication(X0,X1)),X2) = addition(multiplication(X3,X2),multiplication(X0,multiplication(X1,X2))),
inference(superposition,[],[f35,f31]) ).
fof(f121,plain,
! [X2,X3,X0,X1] : multiplication(addition(multiplication(X0,X1),X3),X2) = addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)),
inference(superposition,[],[f35,f31]) ).
fof(f133,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f34,f32]) ).
fof(f137,plain,
! [X0,X1] : multiplication(X0,addition(X1,one)) = addition(multiplication(X0,X1),X0),
inference(superposition,[],[f34,f32]) ).
fof(f139,plain,
! [X0] : multiplication(sF4,addition(X0,sK0)) = addition(multiplication(sF4,X0),sF5),
inference(superposition,[],[f34,f54]) ).
fof(f146,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3),
inference(superposition,[],[f28,f34]) ).
fof(f148,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X2),multiplication(X0,X1)),
inference(superposition,[],[f27,f34]) ).
fof(f149,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = multiplication(X0,addition(X2,X1)),
inference(forward_demodulation,[],[f148,f34]) ).
fof(f164,plain,
multiplication(sF5,addition(one,sF3)) = addition(sF5,sF6),
inference(superposition,[],[f133,f56]) ).
fof(f168,plain,
! [X2,X0,X1] : addition(X0,addition(multiplication(X0,X1),X2)) = addition(multiplication(X0,addition(one,X1)),X2),
inference(superposition,[],[f28,f133]) ).
fof(f187,plain,
sF4 = addition(one,multiplication(sF4,sK1)),
inference(superposition,[],[f38,f52]) ).
fof(f189,plain,
! [X0,X1] : addition(star(X0),X1) = addition(one,addition(multiplication(star(X0),X0),X1)),
inference(superposition,[],[f28,f38]) ).
fof(f193,plain,
! [X0,X1] : multiplication(addition(X1,one),X0) = addition(multiplication(X1,X0),X0),
inference(superposition,[],[f35,f33]) ).
fof(f194,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f35,f33]) ).
fof(f202,plain,
! [X2,X0,X1] : multiplication(addition(one,multiplication(X0,X1)),X2) = addition(X2,multiplication(X0,multiplication(X1,X2))),
inference(superposition,[],[f194,f31]) ).
fof(f205,plain,
multiplication(addition(one,sF5),sF3) = addition(sF3,sF6),
inference(superposition,[],[f194,f56]) ).
fof(f210,plain,
! [X0] : multiplication(X0,addition(one,X0)) = multiplication(addition(one,X0),X0),
inference(superposition,[],[f133,f194]) ).
fof(f228,plain,
! [X2,X0,X1] :
( leq(multiplication(star(X0),multiplication(X1,X2)),X2)
| ~ leq(multiplication(addition(X0,X1),X2),X2) ),
inference(superposition,[],[f39,f35]) ).
fof(f343,plain,
! [X0] :
( X0 != X0
| leq(X0,X0) ),
inference(superposition,[],[f45,f30]) ).
fof(f344,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f28,f30]) ).
fof(f345,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X1,addition(X0,X1))),
inference(superposition,[],[f28,f30]) ).
fof(f348,plain,
! [X0,X1] :
( leq(multiplication(star(X0),multiplication(X0,X1)),X1)
| ~ leq(multiplication(X0,X1),X1) ),
inference(superposition,[],[f39,f30]) ).
fof(f352,plain,
! [X0] : leq(X0,X0),
inference(trivial_inequality_removal,[],[f343]) ).
fof(f363,plain,
! [X0] : strong_iteration(X0) = addition(multiplication(X0,strong_iteration(X0)),strong_iteration(X0)),
inference(superposition,[],[f344,f41]) ).
fof(f367,plain,
! [X0] : star(X0) = addition(one,star(X0)),
inference(superposition,[],[f344,f38]) ).
fof(f368,plain,
! [X0] : strong_iteration(X0) = addition(star(X0),strong_iteration(X0)),
inference(superposition,[],[f344,f43]) ).
fof(f371,plain,
sF2 = addition(sK1,sF2),
inference(superposition,[],[f344,f66]) ).
fof(f375,plain,
sF8 = addition(sF6,sF8),
inference(superposition,[],[f344,f60]) ).
fof(f377,plain,
! [X0,X1] :
( addition(X0,X1) != addition(X0,X1)
| leq(X0,addition(X0,X1)) ),
inference(superposition,[],[f45,f344]) ).
fof(f384,plain,
! [X0,X1] : leq(X0,addition(X0,X1)),
inference(trivial_inequality_removal,[],[f377]) ).
fof(f394,plain,
! [X0] : strong_iteration(X0) = multiplication(addition(X0,one),strong_iteration(X0)),
inference(forward_demodulation,[],[f363,f193]) ).
fof(f399,plain,
multiplication(addition(sF5,one),sF3) = addition(sF6,sF3),
inference(superposition,[],[f102,f33]) ).
fof(f412,plain,
! [X0,X1] : leq(X1,addition(X0,X1)),
inference(superposition,[],[f384,f27]) ).
fof(f444,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,addition(X3,X2)),multiplication(X1,X2)) = addition(multiplication(X0,X3),multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f146,f35]) ).
fof(f449,plain,
! [X2,X3,X0,X1] : addition(multiplication(X1,addition(X3,X2)),X0) = addition(multiplication(X1,X3),addition(X0,multiplication(X1,X2))),
inference(superposition,[],[f146,f27]) ).
fof(f503,plain,
! [X2,X3,X0,X1] : addition(multiplication(X2,X1),multiplication(addition(X2,X3),X0)) = addition(multiplication(X2,addition(X0,X1)),multiplication(X3,X0)),
inference(superposition,[],[f444,f27]) ).
fof(f508,plain,
! [X2,X0,X1] : addition(multiplication(X1,multiplication(X0,strong_iteration(X0))),multiplication(addition(X1,X2),one)) = addition(multiplication(X1,strong_iteration(X0)),multiplication(X2,one)),
inference(superposition,[],[f444,f41]) ).
fof(f514,plain,
! [X2,X0,X1] : addition(multiplication(X1,one),multiplication(addition(X1,X2),multiplication(X0,star(X0)))) = addition(multiplication(X1,star(X0)),multiplication(X2,multiplication(X0,star(X0)))),
inference(superposition,[],[f444,f37]) ).
fof(f519,plain,
! [X0,X1] : addition(multiplication(X0,sK1),multiplication(addition(X0,X1),sK0)) = addition(multiplication(X0,sF2),multiplication(X1,sK0)),
inference(superposition,[],[f444,f66]) ).
fof(f530,plain,
! [X0,X1] : addition(multiplication(X0,X1),multiplication(addition(X0,sF4),sK0)) = addition(multiplication(X0,addition(X1,sK0)),sF5),
inference(superposition,[],[f444,f54]) ).
fof(f532,plain,
! [X0,X1] : addition(multiplication(X0,X1),multiplication(addition(X0,sF5),sF3)) = addition(multiplication(X0,addition(X1,sF3)),sF6),
inference(superposition,[],[f444,f56]) ).
fof(f610,plain,
! [X2,X0,X1] : addition(multiplication(X1,one),multiplication(addition(X1,X2),multiplication(X0,star(X0)))) = multiplication(addition(X1,multiplication(X2,X0)),star(X0)),
inference(forward_demodulation,[],[f514,f120]) ).
fof(f611,plain,
! [X2,X0,X1] : addition(multiplication(X1,multiplication(X0,strong_iteration(X0))),multiplication(addition(X1,X2),one)) = addition(multiplication(X1,strong_iteration(X0)),X2),
inference(forward_demodulation,[],[f508,f32]) ).
fof(f635,plain,
! [X2,X0,X1] : multiplication(addition(X1,multiplication(X2,X0)),star(X0)) = addition(X1,multiplication(addition(X1,X2),multiplication(X0,star(X0)))),
inference(forward_demodulation,[],[f610,f32]) ).
fof(f636,plain,
! [X2,X0,X1] : addition(multiplication(X1,strong_iteration(X0)),X2) = addition(multiplication(X1,multiplication(X0,strong_iteration(X0))),addition(X1,X2)),
inference(forward_demodulation,[],[f611,f32]) ).
fof(f664,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f27,f29]) ).
fof(f692,plain,
! [X2,X0,X1] : addition(multiplication(X1,X0),multiplication(X2,X0)) = addition(multiplication(X1,zero),multiplication(addition(X1,X2),X0)),
inference(superposition,[],[f444,f664]) ).
fof(f697,plain,
! [X2,X0,X1] : multiplication(addition(X1,X2),X0) = addition(multiplication(X1,zero),multiplication(addition(X1,X2),X0)),
inference(forward_demodulation,[],[f692,f35]) ).
fof(f701,plain,
! [X0,X1] : addition(star(X0),multiplication(X1,X0)) = addition(one,multiplication(addition(star(X0),X1),X0)),
inference(superposition,[],[f189,f35]) ).
fof(f702,plain,
! [X0,X1] : addition(star(X0),multiplication(star(X0),X1)) = addition(one,multiplication(star(X0),addition(X0,X1))),
inference(superposition,[],[f189,f34]) ).
fof(f724,plain,
! [X0,X1] : addition(one,multiplication(star(X0),addition(X0,X1))) = multiplication(star(X0),addition(one,X1)),
inference(forward_demodulation,[],[f702,f133]) ).
fof(f729,plain,
! [X0,X1] : leq(X0,multiplication(strong_iteration(X1),X0)),
inference(resolution,[],[f99,f384]) ).
fof(f840,plain,
! [X2,X0,X1] : multiplication(addition(multiplication(X0,X1),one),X2) = addition(multiplication(X0,multiplication(X1,X2)),X2),
inference(superposition,[],[f193,f31]) ).
fof(f853,plain,
! [X0] : multiplication(X0,addition(X0,one)) = multiplication(addition(X0,one),X0),
inference(superposition,[],[f137,f193]) ).
fof(f855,plain,
! [X0,X1] :
( ~ leq(multiplication(addition(X0,one),X1),X1)
| leq(multiplication(star(X0),X1),X1) ),
inference(superposition,[],[f39,f193]) ).
fof(f899,plain,
sF4 = addition(one,sF4),
inference(superposition,[],[f344,f62]) ).
fof(f1106,plain,
! [X0,X1] : multiplication(strong_iteration(X1),X0) = addition(X0,multiplication(strong_iteration(X1),X0)),
inference(resolution,[],[f729,f44]) ).
fof(f1110,plain,
! [X0,X1] : multiplication(strong_iteration(X1),X0) = multiplication(addition(one,strong_iteration(X1)),X0),
inference(forward_demodulation,[],[f1106,f194]) ).
fof(f1119,plain,
! [X0,X1] : addition(multiplication(X0,strong_iteration(X1)),X0) = addition(multiplication(X0,multiplication(X1,strong_iteration(X1))),X0),
inference(superposition,[],[f636,f30]) ).
fof(f1138,plain,
! [X0,X1] : addition(multiplication(one,strong_iteration(X1)),multiplication(X0,star(X0))) = addition(multiplication(one,multiplication(X1,strong_iteration(X1))),star(X0)),
inference(superposition,[],[f636,f37]) ).
fof(f1139,plain,
! [X0,X1] : addition(multiplication(one,multiplication(X1,strong_iteration(X1))),star(X0)) = addition(multiplication(one,strong_iteration(X1)),multiplication(star(X0),X0)),
inference(superposition,[],[f636,f38]) ).
fof(f1141,plain,
! [X0] : addition(multiplication(one,multiplication(X0,strong_iteration(X0))),sF4) = addition(multiplication(one,strong_iteration(X0)),multiplication(sF4,sK1)),
inference(superposition,[],[f636,f187]) ).
fof(f1185,plain,
! [X0] : addition(multiplication(one,multiplication(X0,strong_iteration(X0))),sF4) = addition(strong_iteration(X0),multiplication(sF4,sK1)),
inference(forward_demodulation,[],[f1141,f33]) ).
fof(f1187,plain,
! [X0,X1] : addition(multiplication(one,multiplication(X1,strong_iteration(X1))),star(X0)) = addition(strong_iteration(X1),multiplication(star(X0),X0)),
inference(forward_demodulation,[],[f1139,f33]) ).
fof(f1188,plain,
! [X0,X1] : addition(multiplication(one,strong_iteration(X1)),multiplication(X0,star(X0))) = addition(multiplication(X1,strong_iteration(X1)),star(X0)),
inference(forward_demodulation,[],[f1138,f33]) ).
fof(f1203,plain,
! [X0,X1] : addition(multiplication(X0,strong_iteration(X1)),X0) = multiplication(X0,addition(multiplication(X1,strong_iteration(X1)),one)),
inference(forward_demodulation,[],[f1119,f137]) ).
fof(f1215,plain,
! [X0] : addition(strong_iteration(X0),multiplication(sF4,sK1)) = addition(multiplication(X0,strong_iteration(X0)),sF4),
inference(forward_demodulation,[],[f1185,f33]) ).
fof(f1217,plain,
! [X0,X1] : addition(strong_iteration(X1),multiplication(star(X0),X0)) = addition(multiplication(X1,strong_iteration(X1)),star(X0)),
inference(forward_demodulation,[],[f1187,f33]) ).
fof(f1218,plain,
! [X0,X1] : addition(multiplication(X1,strong_iteration(X1)),star(X0)) = addition(strong_iteration(X1),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f1188,f33]) ).
fof(f1231,plain,
! [X0,X1] : multiplication(X0,strong_iteration(X1)) = addition(multiplication(X0,strong_iteration(X1)),X0),
inference(forward_demodulation,[],[f1203,f41]) ).
fof(f1245,plain,
! [X0,X1] : multiplication(X0,strong_iteration(X1)) = multiplication(X0,addition(strong_iteration(X1),one)),
inference(forward_demodulation,[],[f1231,f137]) ).
fof(f1265,plain,
! [X0] : multiplication(X0,sF3) = multiplication(X0,addition(sF3,one)),
inference(superposition,[],[f1245,f50]) ).
fof(f1267,plain,
! [X0,X1] : multiplication(X1,strong_iteration(X0)) = multiplication(X1,addition(one,strong_iteration(X0))),
inference(superposition,[],[f1245,f27]) ).
fof(f1289,plain,
! [X0] : multiplication(one,strong_iteration(X0)) = addition(strong_iteration(X0),one),
inference(superposition,[],[f33,f1245]) ).
fof(f1299,plain,
! [X0] : strong_iteration(X0) = addition(strong_iteration(X0),one),
inference(forward_demodulation,[],[f1289,f33]) ).
fof(f1356,plain,
! [X0] : multiplication(strong_iteration(X0),addition(one,star(strong_iteration(X0)))) = addition(multiplication(X0,strong_iteration(X0)),star(strong_iteration(X0))),
inference(superposition,[],[f133,f1218]) ).
fof(f1371,plain,
! [X0] : addition(multiplication(X0,strong_iteration(X0)),star(strong_iteration(X0))) = multiplication(strong_iteration(X0),star(strong_iteration(X0))),
inference(forward_demodulation,[],[f1356,f367]) ).
fof(f1400,plain,
! [X2,X3,X0,X1] : addition(multiplication(X1,X2),addition(X3,multiplication(X0,X2))) = addition(X3,multiplication(addition(X0,X1),X2)),
inference(superposition,[],[f90,f35]) ).
fof(f1406,plain,
! [X0,X1] : addition(multiplication(X0,star(X0)),addition(X1,one)) = addition(X1,star(X0)),
inference(superposition,[],[f90,f37]) ).
fof(f1419,plain,
! [X0] : addition(sF7,addition(X0,sF6)) = addition(X0,sF8),
inference(superposition,[],[f90,f60]) ).
fof(f1664,plain,
sF7 = addition(sF7,one),
inference(superposition,[],[f1299,f58]) ).
fof(f1665,plain,
sF3 = addition(sF3,one),
inference(superposition,[],[f1299,f50]) ).
fof(f1669,plain,
! [X0] : strong_iteration(X0) = addition(one,strong_iteration(X0)),
inference(superposition,[],[f27,f1299]) ).
fof(f1689,plain,
sF3 = addition(one,sF3),
inference(superposition,[],[f1669,f50]) ).
fof(f1693,plain,
! [X0,X1] : addition(X1,strong_iteration(X0)) = addition(strong_iteration(X0),addition(X1,one)),
inference(superposition,[],[f90,f1669]) ).
fof(f1698,plain,
! [X0,X1] : addition(multiplication(one,strong_iteration(X1)),strong_iteration(X0)) = addition(multiplication(one,multiplication(X1,strong_iteration(X1))),strong_iteration(X0)),
inference(superposition,[],[f636,f1669]) ).
fof(f1700,plain,
! [X0,X1] : addition(multiplication(one,strong_iteration(X1)),strong_iteration(X0)) = addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X0)),
inference(forward_demodulation,[],[f1698,f33]) ).
fof(f1704,plain,
! [X0,X1] : addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X0)) = addition(strong_iteration(X1),strong_iteration(X0)),
inference(forward_demodulation,[],[f1700,f33]) ).
fof(f1708,plain,
! [X0] : addition(X0,sF3) = addition(one,addition(sF3,X0)),
inference(superposition,[],[f90,f1689]) ).
fof(f1709,plain,
! [X0] : addition(X0,sF3) = addition(sF3,addition(X0,one)),
inference(superposition,[],[f90,f1689]) ).
fof(f1735,plain,
! [X2,X0,X1] :
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| leq(multiplication(multiplication(X0,X2),star(X1)),X0) ),
inference(superposition,[],[f40,f34]) ).
fof(f1758,plain,
! [X2,X0,X1] :
( leq(multiplication(X0,multiplication(X2,star(X1))),X0)
| ~ leq(multiplication(X0,addition(X1,X2)),X0) ),
inference(forward_demodulation,[],[f1735,f31]) ).
fof(f1766,plain,
! [X0] : addition(sF8,X0) = addition(sF6,addition(X0,sF7)),
inference(superposition,[],[f86,f27]) ).
fof(f1776,plain,
addition(sF7,sF6) = addition(sF7,addition(sF8,sF6)),
inference(superposition,[],[f345,f86]) ).
fof(f1794,plain,
addition(sF7,sF6) = addition(sF8,sF8),
inference(forward_demodulation,[],[f1776,f1419]) ).
fof(f1804,plain,
sF8 = addition(sF7,sF6),
inference(forward_demodulation,[],[f1794,f30]) ).
fof(f1814,plain,
! [X0] : addition(multiplication(one,multiplication(X0,strong_iteration(X0))),sF4) = addition(multiplication(one,strong_iteration(X0)),sF4),
inference(superposition,[],[f636,f899]) ).
fof(f1816,plain,
! [X0] : addition(multiplication(one,multiplication(X0,strong_iteration(X0))),sF4) = addition(strong_iteration(X0),sF4),
inference(forward_demodulation,[],[f1814,f33]) ).
fof(f1820,plain,
! [X0] : addition(multiplication(X0,strong_iteration(X0)),sF4) = addition(strong_iteration(X0),sF4),
inference(forward_demodulation,[],[f1816,f33]) ).
fof(f1822,plain,
! [X0] : addition(strong_iteration(X0),multiplication(sF4,sK1)) = addition(strong_iteration(X0),sF4),
inference(forward_demodulation,[],[f1820,f1215]) ).
fof(f1936,plain,
! [X0] : multiplication(addition(X0,one),addition(strong_iteration(X0),one)) = addition(strong_iteration(X0),addition(X0,one)),
inference(superposition,[],[f137,f394]) ).
fof(f1947,plain,
! [X0] : multiplication(addition(X0,one),addition(strong_iteration(X0),one)) = addition(X0,strong_iteration(X0)),
inference(forward_demodulation,[],[f1936,f1693]) ).
fof(f1958,plain,
! [X0] : multiplication(addition(X0,one),strong_iteration(X0)) = addition(X0,strong_iteration(X0)),
inference(forward_demodulation,[],[f1947,f1245]) ).
fof(f1965,plain,
! [X0] : strong_iteration(X0) = addition(X0,strong_iteration(X0)),
inference(forward_demodulation,[],[f1958,f394]) ).
fof(f1969,plain,
sF7 = addition(sK1,sF7),
inference(superposition,[],[f1965,f58]) ).
fof(f1970,plain,
sF3 = addition(sF2,sF3),
inference(superposition,[],[f1965,f50]) ).
fof(f2001,plain,
sF7 = addition(sF7,sK1),
inference(superposition,[],[f27,f1969]) ).
fof(f2015,plain,
addition(sF6,sF7) = addition(sF8,sK1),
inference(superposition,[],[f86,f2001]) ).
fof(f2037,plain,
sF8 = addition(sF8,sK1),
inference(forward_demodulation,[],[f2015,f60]) ).
fof(f2052,plain,
! [X0] : addition(multiplication(X0,strong_iteration(X0)),star(strong_iteration(X0))) = multiplication(addition(one,star(strong_iteration(X0))),strong_iteration(X0)),
inference(superposition,[],[f194,f1217]) ).
fof(f2090,plain,
! [X0] : addition(multiplication(X0,strong_iteration(X0)),star(strong_iteration(X0))) = multiplication(star(strong_iteration(X0)),strong_iteration(X0)),
inference(forward_demodulation,[],[f2052,f367]) ).
fof(f2099,plain,
! [X0] : multiplication(strong_iteration(X0),star(strong_iteration(X0))) = multiplication(star(strong_iteration(X0)),strong_iteration(X0)),
inference(forward_demodulation,[],[f2090,f1371]) ).
fof(f2137,plain,
! [X0] :
( leq(multiplication(star(one),X0),X0)
| ~ leq(X0,X0) ),
inference(superposition,[],[f348,f33]) ).
fof(f2160,plain,
! [X0] : leq(multiplication(star(one),X0),X0),
inference(forward_subsumption_resolution,[],[f2137,f352]) ).
fof(f2415,plain,
! [X0,X1] : multiplication(addition(strong_iteration(X0),multiplication(one,X1)),star(X1)) = addition(strong_iteration(X0),multiplication(strong_iteration(X0),multiplication(X1,star(X1)))),
inference(superposition,[],[f635,f1299]) ).
fof(f2489,plain,
! [X0,X1] : multiplication(addition(strong_iteration(X0),multiplication(one,X1)),star(X1)) = multiplication(strong_iteration(X0),addition(one,multiplication(X1,star(X1)))),
inference(forward_demodulation,[],[f2415,f133]) ).
fof(f2527,plain,
! [X0,X1] : multiplication(strong_iteration(X0),star(X1)) = multiplication(addition(strong_iteration(X0),multiplication(one,X1)),star(X1)),
inference(forward_demodulation,[],[f2489,f37]) ).
fof(f2550,plain,
! [X0,X1] : multiplication(strong_iteration(X0),star(X1)) = multiplication(addition(strong_iteration(X0),X1),star(X1)),
inference(forward_demodulation,[],[f2527,f33]) ).
fof(f2573,plain,
! [X0] : addition(star(X0),multiplication(multiplication(strong_iteration(X0),zero),X0)) = addition(one,multiplication(strong_iteration(X0),X0)),
inference(superposition,[],[f701,f43]) ).
fof(f2621,plain,
! [X0] : addition(one,multiplication(strong_iteration(X0),X0)) = addition(star(X0),multiplication(strong_iteration(X0),multiplication(zero,X0))),
inference(forward_demodulation,[],[f2573,f31]) ).
fof(f2633,plain,
! [X0] : addition(star(X0),multiplication(strong_iteration(X0),zero)) = addition(one,multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f2621,f36]) ).
fof(f2637,plain,
! [X0] : strong_iteration(X0) = addition(one,multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f2633,f43]) ).
fof(f2656,plain,
! [X0,X1] : addition(multiplication(one,multiplication(X1,strong_iteration(X1))),strong_iteration(X0)) = addition(multiplication(one,strong_iteration(X1)),multiplication(strong_iteration(X0),X0)),
inference(superposition,[],[f636,f2637]) ).
fof(f2657,plain,
! [X0,X1] : addition(multiplication(one,multiplication(X1,strong_iteration(X1))),strong_iteration(X0)) = addition(strong_iteration(X1),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f2656,f33]) ).
fof(f2667,plain,
! [X0,X1] : addition(multiplication(X1,strong_iteration(X1)),strong_iteration(X0)) = addition(strong_iteration(X1),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f2657,f33]) ).
fof(f2671,plain,
! [X0,X1] : addition(strong_iteration(X1),strong_iteration(X0)) = addition(strong_iteration(X1),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f2667,f1704]) ).
fof(f2674,plain,
! [X0] : addition(strong_iteration(X0),sF7) = addition(strong_iteration(X0),multiplication(sF7,sK1)),
inference(superposition,[],[f2671,f58]) ).
fof(f2686,plain,
! [X0,X1] : addition(strong_iteration(X0),strong_iteration(X1)) = addition(multiplication(strong_iteration(X1),X1),strong_iteration(X0)),
inference(superposition,[],[f27,f2671]) ).
fof(f3118,plain,
sF8 = addition(sK1,sF8),
inference(superposition,[],[f27,f2037]) ).
fof(f3164,plain,
sF7 = addition(star(sK1),sF7),
inference(superposition,[],[f368,f58]) ).
fof(f3166,plain,
! [X0] : addition(one,multiplication(strong_iteration(X0),X0)) = addition(star(X0),multiplication(strong_iteration(X0),X0)),
inference(superposition,[],[f701,f368]) ).
fof(f3186,plain,
! [X0] : strong_iteration(X0) = addition(star(X0),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f3166,f2637]) ).
fof(f3187,plain,
sF7 = addition(sF4,sF7),
inference(forward_demodulation,[],[f3164,f52]) ).
fof(f3231,plain,
addition(one,zero) = star(zero),
inference(superposition,[],[f37,f36]) ).
fof(f3235,plain,
strong_iteration(zero) = addition(zero,one),
inference(superposition,[],[f41,f36]) ).
fof(f3242,plain,
one = strong_iteration(zero),
inference(forward_demodulation,[],[f3235,f664]) ).
fof(f3245,plain,
one = star(zero),
inference(forward_demodulation,[],[f3231,f29]) ).
fof(f3457,plain,
! [X0,X1] : addition(star(X0),multiplication(X1,star(X0))) = addition(one,multiplication(addition(X0,X1),star(X0))),
inference(superposition,[],[f82,f35]) ).
fof(f3458,plain,
! [X0,X1] : addition(star(X0),multiplication(X0,X1)) = addition(one,multiplication(X0,addition(star(X0),X1))),
inference(superposition,[],[f82,f34]) ).
fof(f3461,plain,
! [X0] : addition(one,multiplication(X0,star(X0))) = addition(star(X0),multiplication(X0,star(X0))),
inference(superposition,[],[f82,f30]) ).
fof(f3478,plain,
! [X0] : addition(multiplication(X0,star(X0)),one) = addition(multiplication(X0,star(X0)),addition(star(X0),one)),
inference(superposition,[],[f345,f82]) ).
fof(f3501,plain,
! [X0] : addition(multiplication(X0,star(X0)),one) = addition(star(X0),star(X0)),
inference(forward_demodulation,[],[f3478,f1406]) ).
fof(f3511,plain,
! [X0] : addition(one,multiplication(X0,star(X0))) = multiplication(addition(one,X0),star(X0)),
inference(forward_demodulation,[],[f3461,f194]) ).
fof(f3512,plain,
! [X0,X1] : addition(one,multiplication(addition(X0,X1),star(X0))) = multiplication(addition(one,X1),star(X0)),
inference(forward_demodulation,[],[f3457,f194]) ).
fof(f3521,plain,
! [X0] : star(X0) = addition(multiplication(X0,star(X0)),one),
inference(forward_demodulation,[],[f3501,f30]) ).
fof(f3524,plain,
! [X0] : star(X0) = multiplication(addition(one,X0),star(X0)),
inference(forward_demodulation,[],[f3511,f37]) ).
fof(f3701,plain,
! [X2,X0,X1] :
( ~ leq(multiplication(addition(X0,X1),X2),X2)
| addition(multiplication(star(X0),multiplication(X1,X2)),X2) = X2 ),
inference(resolution,[],[f228,f44]) ).
fof(f3717,plain,
! [X2,X0,X1] :
( ~ leq(multiplication(addition(X0,X1),X2),X2)
| multiplication(addition(multiplication(star(X0),X1),one),X2) = X2 ),
inference(forward_demodulation,[],[f3701,f840]) ).
fof(f3721,plain,
addition(sF6,sF7) = addition(sF8,one),
inference(superposition,[],[f86,f1664]) ).
fof(f3753,plain,
sF8 = addition(sF8,one),
inference(forward_demodulation,[],[f3721,f60]) ).
fof(f3806,plain,
addition(multiplication(one,sK1),multiplication(sF4,sK0)) = addition(multiplication(one,sF2),multiplication(sF4,sK0)),
inference(superposition,[],[f519,f899]) ).
fof(f3890,plain,
addition(multiplication(one,sK1),sF5) = addition(multiplication(one,sF2),sF5),
inference(forward_demodulation,[],[f3806,f54]) ).
fof(f3950,plain,
addition(multiplication(one,sK1),sF5) = addition(sF2,sF5),
inference(forward_demodulation,[],[f3890,f33]) ).
fof(f3998,plain,
addition(sF2,sF5) = addition(sK1,sF5),
inference(forward_demodulation,[],[f3950,f33]) ).
fof(f4372,plain,
sF8 = addition(sF7,sF8),
inference(superposition,[],[f344,f1804]) ).
fof(f4437,plain,
! [X0,X1] : leq(X1,multiplication(addition(X0,one),X1)),
inference(superposition,[],[f412,f193]) ).
fof(f4456,plain,
! [X0] : leq(multiplication(star(X0),X0),star(X0)),
inference(superposition,[],[f412,f38]) ).
fof(f4511,plain,
! [X0] : star(X0) = addition(multiplication(star(X0),X0),star(X0)),
inference(resolution,[],[f4456,f44]) ).
fof(f4516,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(X0,one)),
inference(forward_demodulation,[],[f4511,f137]) ).
fof(f5237,plain,
addition(sF6,sF7) = addition(sF8,sF6),
inference(superposition,[],[f344,f1766]) ).
fof(f5266,plain,
sF8 = addition(sF8,sF6),
inference(forward_demodulation,[],[f5237,f60]) ).
fof(f5435,plain,
! [X0,X1] : addition(strong_iteration(X0),multiplication(strong_iteration(X0),X1)) = addition(star(X0),multiplication(strong_iteration(X0),addition(zero,X1))),
inference(superposition,[],[f83,f34]) ).
fof(f5492,plain,
! [X0,X1] : addition(star(X0),multiplication(strong_iteration(X0),X1)) = addition(strong_iteration(X0),multiplication(strong_iteration(X0),X1)),
inference(forward_demodulation,[],[f5435,f664]) ).
fof(f5507,plain,
! [X0,X1] : addition(star(X0),multiplication(strong_iteration(X0),X1)) = multiplication(strong_iteration(X0),addition(one,X1)),
inference(forward_demodulation,[],[f5492,f133]) ).
fof(f5516,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = addition(star(sK1),multiplication(sF7,X0)),
inference(superposition,[],[f5507,f58]) ).
fof(f5517,plain,
! [X0] : multiplication(sF3,addition(one,X0)) = addition(star(sF2),multiplication(sF3,X0)),
inference(superposition,[],[f5507,f50]) ).
fof(f5562,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = addition(sF4,multiplication(sF7,X0)),
inference(forward_demodulation,[],[f5516,f52]) ).
fof(f6824,plain,
! [X2,X3,X0,X1] : addition(multiplication(addition(X3,X0),X1),multiplication(X0,X2)) = addition(multiplication(X3,X1),multiplication(X0,addition(X1,X2))),
inference(superposition,[],[f108,f34]) ).
fof(f6831,plain,
! [X0,X1] : addition(multiplication(X1,strong_iteration(X0)),strong_iteration(X0)) = addition(multiplication(addition(X1,X0),strong_iteration(X0)),one),
inference(superposition,[],[f108,f41]) ).
fof(f6936,plain,
! [X0,X1] : multiplication(addition(X1,one),strong_iteration(X0)) = addition(multiplication(addition(X1,X0),strong_iteration(X0)),one),
inference(forward_demodulation,[],[f6831,f193]) ).
fof(f7098,plain,
addition(multiplication(sF2,strong_iteration(sF2)),one) = multiplication(addition(sK1,one),strong_iteration(sF2)),
inference(superposition,[],[f6936,f371]) ).
fof(f7139,plain,
! [X0,X1] :
( ~ leq(strong_iteration(X1),multiplication(addition(X0,one),strong_iteration(X1)))
| leq(strong_iteration(X1),multiplication(strong_iteration(addition(X0,X1)),one)) ),
inference(superposition,[],[f42,f6936]) ).
fof(f7180,plain,
! [X0,X1] : leq(strong_iteration(X1),multiplication(strong_iteration(addition(X0,X1)),one)),
inference(forward_subsumption_resolution,[],[f7139,f4437]) ).
fof(f7207,plain,
addition(multiplication(sF2,sF3),one) = multiplication(addition(sK1,one),sF3),
inference(forward_demodulation,[],[f7098,f50]) ).
fof(f7267,plain,
! [X0,X1] : leq(strong_iteration(X1),strong_iteration(addition(X0,X1))),
inference(forward_demodulation,[],[f7180,f32]) ).
fof(f7273,plain,
sF3 = multiplication(addition(sK1,one),sF3),
inference(forward_demodulation,[],[f7207,f73]) ).
fof(f7331,plain,
( ~ leq(sF3,sF3)
| leq(multiplication(star(sK1),sF3),sF3) ),
inference(superposition,[],[f855,f7273]) ).
fof(f7345,plain,
multiplication(addition(sK1,one),addition(sF3,one)) = addition(sF3,addition(sK1,one)),
inference(superposition,[],[f137,f7273]) ).
fof(f7366,plain,
multiplication(addition(sK1,one),addition(sF3,one)) = addition(sK1,sF3),
inference(forward_demodulation,[],[f7345,f1709]) ).
fof(f7374,plain,
leq(multiplication(star(sK1),sF3),sF3),
inference(forward_subsumption_resolution,[],[f7331,f352]) ).
fof(f7378,plain,
multiplication(addition(sK1,one),sF3) = addition(sK1,sF3),
inference(forward_demodulation,[],[f7366,f1265]) ).
fof(f7381,plain,
leq(multiplication(sF4,sF3),sF3),
inference(forward_demodulation,[],[f7374,f52]) ).
fof(f7383,plain,
sF3 = addition(sK1,sF3),
inference(forward_demodulation,[],[f7378,f7273]) ).
fof(f7385,plain,
addition(sF2,sF3) = addition(sK0,sF3),
inference(superposition,[],[f84,f7383]) ).
fof(f7412,plain,
sF3 = addition(sK0,sF3),
inference(forward_demodulation,[],[f7385,f1970]) ).
fof(f7425,plain,
! [X0] : multiplication(X0,sF3) = multiplication(X0,addition(sF3,sK0)),
inference(superposition,[],[f149,f7412]) ).
fof(f7491,plain,
sF3 = addition(multiplication(sF4,sF3),sF3),
inference(resolution,[],[f7381,f44]) ).
fof(f7492,plain,
sF3 = multiplication(addition(sF4,one),sF3),
inference(forward_demodulation,[],[f7491,f193]) ).
fof(f7494,plain,
sF3 = multiplication(addition(one,sF4),sF3),
inference(superposition,[],[f7492,f27]) ).
fof(f7509,plain,
multiplication(addition(sF4,one),addition(sF3,one)) = addition(sF3,addition(sF4,one)),
inference(superposition,[],[f137,f7492]) ).
fof(f7530,plain,
multiplication(addition(sF4,one),addition(sF3,one)) = addition(sF4,sF3),
inference(forward_demodulation,[],[f7509,f1709]) ).
fof(f7538,plain,
sF3 = multiplication(sF4,sF3),
inference(forward_demodulation,[],[f7494,f899]) ).
fof(f7543,plain,
multiplication(addition(sF4,one),sF3) = addition(sF4,sF3),
inference(forward_demodulation,[],[f7530,f1265]) ).
fof(f7548,plain,
sF3 = addition(sF4,sF3),
inference(forward_demodulation,[],[f7543,f7492]) ).
fof(f7552,plain,
multiplication(sF4,addition(sF3,sK0)) = addition(sF3,sF5),
inference(superposition,[],[f139,f7538]) ).
fof(f7556,plain,
! [X0] : multiplication(sF4,addition(sF3,X0)) = addition(sF3,multiplication(sF4,X0)),
inference(superposition,[],[f34,f7538]) ).
fof(f7567,plain,
multiplication(sF4,addition(sF3,one)) = addition(sF3,sF4),
inference(superposition,[],[f137,f7538]) ).
fof(f7583,plain,
multiplication(sF4,sF3) = addition(sF3,sF4),
inference(forward_demodulation,[],[f7567,f1265]) ).
fof(f7590,plain,
multiplication(sF4,sF3) = addition(sF3,sF5),
inference(forward_demodulation,[],[f7552,f7425]) ).
fof(f7592,plain,
sF3 = addition(sF3,sF4),
inference(forward_demodulation,[],[f7583,f7538]) ).
fof(f7595,plain,
sF3 = addition(sF3,sF5),
inference(forward_demodulation,[],[f7590,f7538]) ).
fof(f7659,plain,
! [X0] : addition(X0,sF3) = addition(sF5,addition(X0,sF3)),
inference(superposition,[],[f90,f7595]) ).
fof(f7715,plain,
addition(multiplication(sF3,sK1),multiplication(sF3,sK0)) = addition(multiplication(sF3,sF2),multiplication(sF4,sK0)),
inference(superposition,[],[f519,f7592]) ).
fof(f7719,plain,
addition(one,multiplication(star(sF3),sF3)) = multiplication(star(sF3),addition(one,sF4)),
inference(superposition,[],[f724,f7592]) ).
fof(f7724,plain,
addition(one,multiplication(star(sF3),sF3)) = multiplication(star(sF3),sF4),
inference(forward_demodulation,[],[f7719,f899]) ).
fof(f7727,plain,
addition(multiplication(sF3,sK1),multiplication(sF3,sK0)) = addition(multiplication(sF3,sF2),sF5),
inference(forward_demodulation,[],[f7715,f54]) ).
fof(f7741,plain,
star(sF3) = multiplication(star(sF3),sF4),
inference(forward_demodulation,[],[f7724,f38]) ).
fof(f7744,plain,
multiplication(sF3,addition(sK1,sK0)) = addition(multiplication(sF3,sF2),sF5),
inference(forward_demodulation,[],[f7727,f34]) ).
fof(f7747,plain,
multiplication(sF3,sF2) = addition(multiplication(sF3,sF2),sF5),
inference(forward_demodulation,[],[f7744,f66]) ).
fof(f8076,plain,
! [X0] : star(strong_iteration(X0)) = multiplication(star(strong_iteration(X0)),strong_iteration(X0)),
inference(superposition,[],[f1245,f4516]) ).
fof(f8093,plain,
! [X0] : multiplication(addition(one,star(X0)),addition(X0,one)) = addition(addition(X0,one),star(X0)),
inference(superposition,[],[f194,f4516]) ).
fof(f8106,plain,
! [X0] : multiplication(addition(one,star(X0)),addition(X0,one)) = addition(X0,addition(one,star(X0))),
inference(forward_demodulation,[],[f8093,f28]) ).
fof(f8113,plain,
! [X0] : star(strong_iteration(X0)) = multiplication(strong_iteration(X0),star(strong_iteration(X0))),
inference(forward_demodulation,[],[f8076,f2099]) ).
fof(f8121,plain,
! [X0] : multiplication(star(X0),addition(X0,one)) = addition(X0,star(X0)),
inference(forward_demodulation,[],[f8106,f367]) ).
fof(f8128,plain,
! [X0] : star(X0) = addition(X0,star(X0)),
inference(forward_demodulation,[],[f8121,f4516]) ).
fof(f8167,plain,
addition(sF2,star(sK1)) = addition(sK0,star(sK1)),
inference(superposition,[],[f84,f8128]) ).
fof(f8170,plain,
addition(sF2,sF4) = addition(sK0,sF4),
inference(forward_demodulation,[],[f8167,f52]) ).
fof(f8269,plain,
! [X0] : multiplication(X0,addition(sF4,sK0)) = multiplication(X0,addition(sF2,sF4)),
inference(superposition,[],[f149,f8170]) ).
fof(f8734,plain,
! [X0] : star(star(X0)) = multiplication(star(X0),star(star(X0))),
inference(superposition,[],[f3524,f367]) ).
fof(f8736,plain,
star(sF3) = multiplication(sF3,star(sF3)),
inference(superposition,[],[f3524,f1689]) ).
fof(f8742,plain,
! [X0] : star(X0) = multiplication(addition(X0,one),star(X0)),
inference(superposition,[],[f3524,f27]) ).
fof(f8834,plain,
sF3 = addition(one,multiplication(sF2,sF3)),
inference(superposition,[],[f27,f73]) ).
fof(f8844,plain,
leq(multiplication(sF2,sF3),sF3),
inference(superposition,[],[f384,f73]) ).
fof(f9000,plain,
! [X0] : star(multiplication(X0,strong_iteration(X0))) = multiplication(strong_iteration(X0),star(multiplication(X0,strong_iteration(X0)))),
inference(superposition,[],[f8742,f41]) ).
fof(f9294,plain,
! [X2,X0,X1] : addition(multiplication(one,X1),multiplication(multiplication(X0,star(X0)),addition(X1,X2))) = addition(multiplication(star(X0),X1),multiplication(multiplication(X0,star(X0)),X2)),
inference(superposition,[],[f6824,f37]) ).
fof(f9297,plain,
! [X2,X0,X1] : addition(multiplication(one,X1),multiplication(multiplication(star(X0),X0),addition(X1,X2))) = addition(multiplication(star(X0),X1),multiplication(multiplication(star(X0),X0),X2)),
inference(superposition,[],[f6824,f38]) ).
fof(f9309,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),addition(X1,X2))) = addition(multiplication(strong_iteration(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),X2)),
inference(superposition,[],[f6824,f43]) ).
fof(f9344,plain,
! [X0,X1] : addition(multiplication(sF4,X0),multiplication(multiplication(sF7,zero),addition(X0,X1))) = addition(multiplication(sF7,X0),multiplication(multiplication(sF7,zero),X1)),
inference(superposition,[],[f6824,f70]) ).
fof(f9360,plain,
! [X0,X1] : addition(multiplication(sF7,X0),multiplication(one,X1)) = addition(multiplication(sF7,X0),multiplication(one,addition(X0,X1))),
inference(superposition,[],[f6824,f1664]) ).
fof(f9369,plain,
! [X2,X0,X1] : addition(multiplication(strong_iteration(X0),X1),multiplication(strong_iteration(X0),X2)) = addition(multiplication(one,X1),multiplication(strong_iteration(X0),addition(X1,X2))),
inference(superposition,[],[f6824,f1110]) ).
fof(f9464,plain,
! [X2,X0,X1] : addition(multiplication(addition(X1,X2),multiplication(X0,strong_iteration(X0))),multiplication(X2,one)) = addition(multiplication(X1,multiplication(X0,strong_iteration(X0))),multiplication(X2,strong_iteration(X0))),
inference(superposition,[],[f6824,f41]) ).
fof(f9627,plain,
! [X2,X0,X1] : addition(multiplication(addition(X1,X2),multiplication(X0,strong_iteration(X0))),multiplication(X2,one)) = multiplication(addition(multiplication(X1,X0),X2),strong_iteration(X0)),
inference(forward_demodulation,[],[f9464,f121]) ).
fof(f9672,plain,
! [X2,X0,X1] : addition(multiplication(strong_iteration(X0),X1),multiplication(strong_iteration(X0),X2)) = addition(X1,multiplication(strong_iteration(X0),addition(X1,X2))),
inference(forward_demodulation,[],[f9369,f33]) ).
fof(f9674,plain,
! [X0,X1] : addition(multiplication(sF7,X0),multiplication(one,X1)) = addition(multiplication(sF7,X0),addition(X0,X1)),
inference(forward_demodulation,[],[f9360,f33]) ).
fof(f9683,plain,
! [X0,X1] : addition(multiplication(sF4,X0),multiplication(multiplication(sF7,zero),addition(X0,X1))) = addition(multiplication(sF7,X0),multiplication(sF7,multiplication(zero,X1))),
inference(forward_demodulation,[],[f9344,f31]) ).
fof(f9703,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),addition(X1,X2))) = addition(multiplication(strong_iteration(X0),X1),multiplication(strong_iteration(X0),multiplication(zero,X2))),
inference(forward_demodulation,[],[f9309,f31]) ).
fof(f9715,plain,
! [X2,X0,X1] : addition(multiplication(one,X1),multiplication(multiplication(star(X0),X0),addition(X1,X2))) = addition(multiplication(star(X0),X1),multiplication(star(X0),multiplication(X0,X2))),
inference(forward_demodulation,[],[f9297,f31]) ).
fof(f9718,plain,
! [X2,X0,X1] : addition(multiplication(one,X1),multiplication(multiplication(X0,star(X0)),addition(X1,X2))) = addition(multiplication(star(X0),X1),multiplication(X0,multiplication(star(X0),X2))),
inference(forward_demodulation,[],[f9294,f31]) ).
fof(f9792,plain,
! [X2,X0,X1] : multiplication(addition(multiplication(X1,X0),X2),strong_iteration(X0)) = addition(multiplication(addition(X1,X2),multiplication(X0,strong_iteration(X0))),X2),
inference(forward_demodulation,[],[f9627,f32]) ).
fof(f9823,plain,
! [X2,X0,X1] : multiplication(strong_iteration(X0),addition(X1,X2)) = addition(X1,multiplication(strong_iteration(X0),addition(X1,X2))),
inference(forward_demodulation,[],[f9672,f34]) ).
fof(f9825,plain,
! [X0,X1] : addition(multiplication(sF7,X0),X1) = addition(multiplication(sF7,X0),addition(X0,X1)),
inference(forward_demodulation,[],[f9674,f33]) ).
fof(f9830,plain,
! [X0,X1] : addition(multiplication(sF4,X0),multiplication(multiplication(sF7,zero),addition(X0,X1))) = multiplication(sF7,addition(X0,multiplication(zero,X1))),
inference(forward_demodulation,[],[f9683,f34]) ).
fof(f9840,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),addition(X1,X2))) = multiplication(strong_iteration(X0),addition(X1,multiplication(zero,X2))),
inference(forward_demodulation,[],[f9703,f34]) ).
fof(f9852,plain,
! [X2,X0,X1] : addition(multiplication(one,X1),multiplication(multiplication(star(X0),X0),addition(X1,X2))) = multiplication(star(X0),addition(X1,multiplication(X0,X2))),
inference(forward_demodulation,[],[f9715,f34]) ).
fof(f9855,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(X0,multiplication(star(X0),X2))) = addition(multiplication(one,X1),multiplication(X0,multiplication(star(X0),addition(X1,X2)))),
inference(forward_demodulation,[],[f9718,f31]) ).
fof(f9927,plain,
! [X0,X1] : addition(multiplication(sF4,X0),multiplication(multiplication(sF7,zero),addition(X0,X1))) = multiplication(sF7,addition(X0,zero)),
inference(forward_demodulation,[],[f9830,f36]) ).
fof(f9933,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),addition(X1,X2))) = multiplication(strong_iteration(X0),addition(X1,zero)),
inference(forward_demodulation,[],[f9840,f36]) ).
fof(f9939,plain,
! [X2,X0,X1] : multiplication(star(X0),addition(X1,multiplication(X0,X2))) = addition(multiplication(one,X1),multiplication(star(X0),multiplication(X0,addition(X1,X2)))),
inference(forward_demodulation,[],[f9852,f31]) ).
fof(f9942,plain,
! [X2,X0,X1] : addition(multiplication(star(X0),X1),multiplication(X0,multiplication(star(X0),X2))) = addition(X1,multiplication(X0,multiplication(star(X0),addition(X1,X2)))),
inference(forward_demodulation,[],[f9855,f33]) ).
fof(f9980,plain,
! [X0,X1] : multiplication(sF7,X0) = addition(multiplication(sF4,X0),multiplication(multiplication(sF7,zero),addition(X0,X1))),
inference(forward_demodulation,[],[f9927,f29]) ).
fof(f9983,plain,
! [X2,X0,X1] : multiplication(strong_iteration(X0),X1) = addition(multiplication(star(X0),X1),multiplication(multiplication(strong_iteration(X0),zero),addition(X1,X2))),
inference(forward_demodulation,[],[f9933,f29]) ).
fof(f9988,plain,
! [X2,X0,X1] : multiplication(star(X0),addition(X1,multiplication(X0,X2))) = addition(X1,multiplication(star(X0),multiplication(X0,addition(X1,X2)))),
inference(forward_demodulation,[],[f9939,f33]) ).
fof(f10007,plain,
! [X0,X1] : multiplication(sF7,X0) = addition(multiplication(sF4,X0),multiplication(sF7,multiplication(zero,addition(X0,X1)))),
inference(forward_demodulation,[],[f9980,f31]) ).
fof(f10008,plain,
! [X2,X0,X1] : multiplication(strong_iteration(X0),X1) = addition(multiplication(star(X0),X1),multiplication(strong_iteration(X0),multiplication(zero,addition(X1,X2)))),
inference(forward_demodulation,[],[f9983,f31]) ).
fof(f10014,plain,
! [X0] : multiplication(sF7,X0) = addition(multiplication(sF4,X0),multiplication(sF7,zero)),
inference(forward_demodulation,[],[f10007,f36]) ).
fof(f10015,plain,
! [X0,X1] : multiplication(strong_iteration(X0),X1) = addition(multiplication(star(X0),X1),multiplication(strong_iteration(X0),zero)),
inference(forward_demodulation,[],[f10008,f36]) ).
fof(f10891,plain,
! [X0,X1] : multiplication(strong_iteration(X1),strong_iteration(X0)) = addition(one,multiplication(strong_iteration(X1),strong_iteration(X0))),
inference(superposition,[],[f9823,f1669]) ).
fof(f11097,plain,
multiplication(sF7,sK0) = addition(sF5,multiplication(sF7,zero)),
inference(superposition,[],[f10014,f54]) ).
fof(f11098,plain,
multiplication(sF7,sF3) = addition(sF3,multiplication(sF7,zero)),
inference(superposition,[],[f10014,f7538]) ).
fof(f11117,plain,
! [X0,X1] : addition(multiplication(sF4,addition(X1,X0)),multiplication(sF7,zero)) = addition(multiplication(sF4,X1),multiplication(sF7,X0)),
inference(superposition,[],[f146,f10014]) ).
fof(f11133,plain,
! [X0] : multiplication(sF7,X0) = addition(multiplication(sF4,X0),addition(multiplication(sF7,zero),multiplication(sF7,X0))),
inference(superposition,[],[f345,f10014]) ).
fof(f11163,plain,
! [X0] : multiplication(sF7,X0) = addition(multiplication(sF7,zero),multiplication(addition(sF7,sF4),X0)),
inference(forward_demodulation,[],[f11133,f1400]) ).
fof(f11168,plain,
! [X0,X1] : multiplication(sF7,addition(X1,X0)) = addition(multiplication(sF4,X1),multiplication(sF7,X0)),
inference(forward_demodulation,[],[f11117,f10014]) ).
fof(f11191,plain,
! [X0] : multiplication(sF7,X0) = multiplication(addition(sF7,sF4),X0),
inference(forward_demodulation,[],[f11163,f697]) ).
fof(f11668,plain,
! [X0,X1] : multiplication(addition(multiplication(X0,zero),X1),strong_iteration(zero)) = addition(multiplication(addition(X0,X1),zero),X1),
inference(superposition,[],[f9792,f36]) ).
fof(f11682,plain,
! [X0,X1] : multiplication(addition(addition(X0,multiplication(X1,strong_iteration(X1))),one),multiplication(X1,strong_iteration(X1))) = multiplication(addition(multiplication(X0,X1),multiplication(X1,strong_iteration(X1))),strong_iteration(X1)),
inference(superposition,[],[f193,f9792]) ).
fof(f11754,plain,
! [X0,X1] : multiplication(addition(multiplication(X0,X1),multiplication(X1,strong_iteration(X1))),strong_iteration(X1)) = multiplication(addition(X0,addition(multiplication(X1,strong_iteration(X1)),one)),multiplication(X1,strong_iteration(X1))),
inference(forward_demodulation,[],[f11682,f28]) ).
fof(f11762,plain,
! [X0,X1] : addition(multiplication(addition(X0,X1),zero),X1) = multiplication(addition(multiplication(X0,zero),X1),one),
inference(forward_demodulation,[],[f11668,f3242]) ).
fof(f11875,plain,
! [X0,X1] : multiplication(addition(multiplication(X0,X1),multiplication(X1,strong_iteration(X1))),strong_iteration(X1)) = multiplication(addition(X0,strong_iteration(X1)),multiplication(X1,strong_iteration(X1))),
inference(forward_demodulation,[],[f11754,f41]) ).
fof(f11882,plain,
! [X0,X1] : addition(multiplication(X0,zero),X1) = addition(multiplication(addition(X0,X1),zero),X1),
inference(forward_demodulation,[],[f11762,f32]) ).
fof(f12288,plain,
! [X0] : addition(X0,sF7) = addition(sF4,addition(X0,multiplication(sF7,zero))),
inference(superposition,[],[f92,f70]) ).
fof(f12312,plain,
! [X0] : addition(X0,sF8) = addition(sF8,addition(X0,sF6)),
inference(superposition,[],[f92,f5266]) ).
fof(f12442,plain,
! [X0,X1] : addition(strong_iteration(X0),X1) = addition(one,addition(multiplication(X0,strong_iteration(X0)),X1)),
inference(superposition,[],[f81,f92]) ).
fof(f12999,plain,
addition(sF3,sF4) = addition(sF3,multiplication(sF4,sK1)),
inference(superposition,[],[f1822,f50]) ).
fof(f13054,plain,
addition(sF3,sF4) = multiplication(sF4,addition(sF3,sK1)),
inference(forward_demodulation,[],[f12999,f7556]) ).
fof(f13064,plain,
sF3 = multiplication(sF4,addition(sF3,sK1)),
inference(forward_demodulation,[],[f13054,f7592]) ).
fof(f13308,plain,
! [X0] :
( ~ leq(multiplication(sF2,X0),X0)
| multiplication(addition(multiplication(star(sK1),sK0),one),X0) = X0 ),
inference(superposition,[],[f3717,f66]) ).
fof(f13310,plain,
! [X0] :
( ~ leq(multiplication(sF3,X0),X0)
| multiplication(addition(multiplication(star(sK1),sF3),one),X0) = X0 ),
inference(superposition,[],[f3717,f7383]) ).
fof(f13355,plain,
! [X0] :
( ~ leq(star(X0),star(X0))
| star(X0) = multiplication(addition(multiplication(star(X0),one),one),star(X0)) ),
inference(superposition,[],[f3717,f8742]) ).
fof(f13356,plain,
! [X0] :
( ~ leq(strong_iteration(X0),strong_iteration(X0))
| strong_iteration(X0) = multiplication(addition(multiplication(star(X0),one),one),strong_iteration(X0)) ),
inference(superposition,[],[f3717,f394]) ).
fof(f13378,plain,
! [X0] : strong_iteration(X0) = multiplication(addition(multiplication(star(X0),one),one),strong_iteration(X0)),
inference(forward_subsumption_resolution,[],[f13356,f352]) ).
fof(f13379,plain,
! [X0] : star(X0) = multiplication(addition(multiplication(star(X0),one),one),star(X0)),
inference(forward_subsumption_resolution,[],[f13355,f352]) ).
fof(f13398,plain,
! [X0] :
( multiplication(addition(multiplication(sF4,sF3),one),X0) = X0
| ~ leq(multiplication(sF3,X0),X0) ),
inference(forward_demodulation,[],[f13310,f52]) ).
fof(f13400,plain,
! [X0] :
( multiplication(addition(multiplication(sF4,sK0),one),X0) = X0
| ~ leq(multiplication(sF2,X0),X0) ),
inference(forward_demodulation,[],[f13308,f52]) ).
fof(f13440,plain,
! [X0] : strong_iteration(X0) = multiplication(multiplication(addition(star(X0),one),one),strong_iteration(X0)),
inference(forward_demodulation,[],[f13378,f193]) ).
fof(f13441,plain,
! [X0] : star(X0) = multiplication(multiplication(addition(star(X0),one),one),star(X0)),
inference(forward_demodulation,[],[f13379,f193]) ).
fof(f13446,plain,
! [X0] :
( multiplication(addition(sF3,one),X0) = X0
| ~ leq(multiplication(sF3,X0),X0) ),
inference(forward_demodulation,[],[f13398,f7538]) ).
fof(f13447,plain,
! [X0] :
( ~ leq(multiplication(sF2,X0),X0)
| multiplication(addition(sF5,one),X0) = X0 ),
inference(forward_demodulation,[],[f13400,f54]) ).
fof(f13462,plain,
! [X0] : strong_iteration(X0) = multiplication(addition(star(X0),one),multiplication(one,strong_iteration(X0))),
inference(forward_demodulation,[],[f13440,f31]) ).
fof(f13463,plain,
! [X0] : star(X0) = multiplication(addition(star(X0),one),multiplication(one,star(X0))),
inference(forward_demodulation,[],[f13441,f31]) ).
fof(f13468,plain,
! [X0] :
( ~ leq(multiplication(sF3,X0),X0)
| multiplication(sF3,X0) = X0 ),
inference(forward_demodulation,[],[f13446,f1665]) ).
fof(f13478,plain,
! [X0] : strong_iteration(X0) = multiplication(addition(star(X0),one),strong_iteration(X0)),
inference(forward_demodulation,[],[f13462,f33]) ).
fof(f13479,plain,
! [X0] : star(X0) = multiplication(addition(star(X0),one),star(X0)),
inference(forward_demodulation,[],[f13463,f33]) ).
fof(f13483,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(star(X0),one)),
inference(forward_demodulation,[],[f13479,f853]) ).
fof(f13491,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(one,star(X0))),
inference(superposition,[],[f149,f13483]) ).
fof(f13535,plain,
! [X0] : star(X0) = multiplication(star(X0),star(X0)),
inference(forward_demodulation,[],[f13491,f367]) ).
fof(f13554,plain,
sF4 = multiplication(sF4,sF4),
inference(superposition,[],[f13535,f52]) ).
fof(f13556,plain,
! [X0,X1] : multiplication(star(X0),X1) = multiplication(star(X0),multiplication(star(X0),X1)),
inference(superposition,[],[f31,f13535]) ).
fof(f13710,plain,
! [X0] : multiplication(sF4,X0) = multiplication(sF4,multiplication(sF4,X0)),
inference(superposition,[],[f31,f13554]) ).
fof(f13781,plain,
sF7 = addition(star(sK1),multiplication(sF7,sK1)),
inference(superposition,[],[f3186,f58]) ).
fof(f13782,plain,
sF3 = addition(star(sF2),multiplication(sF3,sF2)),
inference(superposition,[],[f3186,f50]) ).
fof(f13853,plain,
sF3 = multiplication(sF3,addition(one,sF2)),
inference(forward_demodulation,[],[f13782,f5517]) ).
fof(f13854,plain,
sF7 = addition(sF4,multiplication(sF7,sK1)),
inference(forward_demodulation,[],[f13781,f52]) ).
fof(f13873,plain,
sF7 = multiplication(sF7,addition(one,sK1)),
inference(forward_demodulation,[],[f13854,f5562]) ).
fof(f14465,plain,
! [X0] : addition(sF3,multiplication(X0,sK1)) = addition(multiplication(sF4,sF3),multiplication(addition(sF4,X0),sK1)),
inference(superposition,[],[f444,f13064]) ).
fof(f14517,plain,
! [X0] : addition(sF3,multiplication(X0,sK1)) = addition(sF3,multiplication(addition(sF4,X0),sK1)),
inference(forward_demodulation,[],[f14465,f7538]) ).
fof(f14978,plain,
sF3 = multiplication(addition(sF5,one),sF3),
inference(resolution,[],[f8844,f13447]) ).
fof(f14981,plain,
sF3 = addition(sF6,sF3),
inference(forward_demodulation,[],[f14978,f399]) ).
fof(f17791,plain,
addition(sF3,sF7) = addition(sF3,multiplication(sF7,sK1)),
inference(superposition,[],[f2674,f50]) ).
fof(f17887,plain,
multiplication(addition(one,sF5),addition(one,sF3)) = addition(addition(one,sF3),addition(sF5,sF6)),
inference(superposition,[],[f194,f164]) ).
fof(f17910,plain,
multiplication(addition(one,sF5),addition(one,sF3)) = addition(one,addition(sF3,addition(sF5,sF6))),
inference(forward_demodulation,[],[f17887,f28]) ).
fof(f17944,plain,
multiplication(addition(one,sF5),addition(one,sF3)) = addition(addition(sF5,sF6),sF3),
inference(forward_demodulation,[],[f17910,f1708]) ).
fof(f17971,plain,
multiplication(addition(one,sF5),addition(one,sF3)) = addition(sF5,addition(sF6,sF3)),
inference(forward_demodulation,[],[f17944,f28]) ).
fof(f17990,plain,
addition(sF6,sF3) = multiplication(addition(one,sF5),addition(one,sF3)),
inference(forward_demodulation,[],[f17971,f7659]) ).
fof(f18001,plain,
multiplication(addition(one,sF5),sF3) = addition(sF6,sF3),
inference(forward_demodulation,[],[f17990,f1689]) ).
fof(f18007,plain,
sF3 = multiplication(addition(one,sF5),sF3),
inference(forward_demodulation,[],[f18001,f14981]) ).
fof(f18009,plain,
sF3 = addition(sF3,sF6),
inference(forward_demodulation,[],[f18007,f205]) ).
fof(f20666,plain,
! [X0] : strong_iteration(X0) = multiplication(addition(one,star(X0)),strong_iteration(X0)),
inference(superposition,[],[f13478,f27]) ).
fof(f20725,plain,
! [X0] : strong_iteration(X0) = multiplication(star(X0),strong_iteration(X0)),
inference(forward_demodulation,[],[f20666,f367]) ).
fof(f20746,plain,
sF7 = multiplication(star(sK1),sF7),
inference(superposition,[],[f20725,f58]) ).
fof(f20749,plain,
! [X0] : addition(strong_iteration(X0),multiplication(strong_iteration(X0),zero)) = multiplication(strong_iteration(X0),strong_iteration(X0)),
inference(superposition,[],[f10015,f20725]) ).
fof(f20791,plain,
! [X0] : multiplication(strong_iteration(X0),addition(one,zero)) = multiplication(strong_iteration(X0),strong_iteration(X0)),
inference(forward_demodulation,[],[f20749,f133]) ).
fof(f20793,plain,
sF7 = multiplication(sF4,sF7),
inference(forward_demodulation,[],[f20746,f52]) ).
fof(f20798,plain,
! [X0] : multiplication(strong_iteration(X0),one) = multiplication(strong_iteration(X0),strong_iteration(X0)),
inference(forward_demodulation,[],[f20791,f29]) ).
fof(f20799,plain,
! [X0] : strong_iteration(X0) = multiplication(strong_iteration(X0),strong_iteration(X0)),
inference(forward_demodulation,[],[f20798,f32]) ).
fof(f20801,plain,
multiplication(sF7,sF7) = addition(sF7,multiplication(sF7,zero)),
inference(superposition,[],[f10014,f20793]) ).
fof(f20806,plain,
! [X0] : addition(multiplication(sF4,X0),sF7) = multiplication(sF4,addition(X0,sF7)),
inference(superposition,[],[f34,f20793]) ).
fof(f20844,plain,
multiplication(sF7,addition(one,zero)) = multiplication(sF7,sF7),
inference(forward_demodulation,[],[f20801,f133]) ).
fof(f20849,plain,
multiplication(sF7,one) = multiplication(sF7,sF7),
inference(forward_demodulation,[],[f20844,f29]) ).
fof(f20850,plain,
sF7 = multiplication(sF7,sF7),
inference(forward_demodulation,[],[f20849,f32]) ).
fof(f20854,plain,
! [X0] : addition(sF7,multiplication(sF7,X0)) = multiplication(sF7,addition(sF7,X0)),
inference(superposition,[],[f34,f20850]) ).
fof(f20891,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = multiplication(sF7,addition(sF7,X0)),
inference(forward_demodulation,[],[f20854,f133]) ).
fof(f20902,plain,
sF3 = multiplication(sF3,sF3),
inference(superposition,[],[f20799,f50]) ).
fof(f20908,plain,
! [X0,X1] : multiplication(strong_iteration(X0),X1) = multiplication(strong_iteration(X0),multiplication(strong_iteration(X0),X1)),
inference(superposition,[],[f31,f20799]) ).
fof(f20909,plain,
! [X0,X1] : addition(strong_iteration(X0),multiplication(strong_iteration(X0),X1)) = multiplication(strong_iteration(X0),addition(strong_iteration(X0),X1)),
inference(superposition,[],[f34,f20799]) ).
fof(f20952,plain,
! [X0,X1] : multiplication(strong_iteration(X0),addition(one,X1)) = multiplication(strong_iteration(X0),addition(strong_iteration(X0),X1)),
inference(forward_demodulation,[],[f20909,f133]) ).
fof(f20966,plain,
multiplication(sF5,sF3) = multiplication(sF6,sF3),
inference(superposition,[],[f116,f20902]) ).
fof(f21010,plain,
sF6 = multiplication(sF6,sF3),
inference(forward_demodulation,[],[f20966,f56]) ).
fof(f21488,plain,
addition(sF3,multiplication(sF7,sK1)) = addition(sF3,multiplication(multiplication(sF7,zero),sK1)),
inference(superposition,[],[f14517,f70]) ).
fof(f21565,plain,
addition(sF3,multiplication(sF7,sK1)) = addition(sF3,multiplication(sF7,multiplication(zero,sK1))),
inference(forward_demodulation,[],[f21488,f31]) ).
fof(f21583,plain,
addition(sF3,multiplication(sF7,zero)) = addition(sF3,multiplication(sF7,sK1)),
inference(forward_demodulation,[],[f21565,f36]) ).
fof(f21593,plain,
addition(sF3,sF7) = addition(sF3,multiplication(sF7,zero)),
inference(forward_demodulation,[],[f21583,f17791]) ).
fof(f21595,plain,
multiplication(sF7,sF3) = addition(sF3,sF7),
inference(forward_demodulation,[],[f21593,f11098]) ).
fof(f21603,plain,
multiplication(sF7,sF3) = addition(sF7,sF3),
inference(superposition,[],[f27,f21595]) ).
fof(f21731,definition,
( spl9_162
<=> sF3 = multiplication(sF7,sF3) ),
introduced(definition,[new_symbols(definition,[spl9_162])],[avatar_definition]) ).
fof(f21732,plain,
( sF3 = multiplication(sF7,sF3)
| ~ spl9_162 ),
inference(avatar_component_clause,[],[f21731]) ).
fof(f21733,plain,
( sF3 != multiplication(sF7,sF3)
| spl9_162 ),
inference(avatar_component_clause,[],[f21731]) ).
fof(f22845,plain,
! [X0] : multiplication(addition(one,multiplication(X0,sF5)),sF3) = addition(sF3,multiplication(X0,sF6)),
inference(superposition,[],[f202,f56]) ).
fof(f24376,plain,
! [X0] : addition(multiplication(star(one),X0),X0) = X0,
inference(resolution,[],[f2160,f44]) ).
fof(f24395,plain,
! [X0] : multiplication(addition(star(one),one),X0) = X0,
inference(forward_demodulation,[],[f24376,f193]) ).
fof(f25267,plain,
! [X0] : addition(X0,multiplication(sF3,sF2)) = addition(multiplication(sF3,sF2),addition(X0,sF5)),
inference(superposition,[],[f92,f7747]) ).
fof(f27136,plain,
! [X2,X0,X1] : addition(multiplication(X1,star(X0)),multiplication(X2,one)) = addition(multiplication(X1,multiplication(star(X0),X0)),multiplication(addition(X1,X2),one)),
inference(superposition,[],[f503,f38]) ).
fof(f27138,plain,
! [X2,X0,X1] : addition(multiplication(X1,strong_iteration(X0)),multiplication(X2,one)) = addition(multiplication(X1,multiplication(strong_iteration(X0),X0)),multiplication(addition(X1,X2),one)),
inference(superposition,[],[f503,f2637]) ).
fof(f27272,plain,
! [X0] : addition(multiplication(sF7,sK1),multiplication(addition(sF7,X0),one)) = addition(sF7,multiplication(X0,one)),
inference(superposition,[],[f503,f13873]) ).
fof(f27601,plain,
! [X0] : addition(sF7,X0) = addition(multiplication(sF7,sK1),multiplication(addition(sF7,X0),one)),
inference(forward_demodulation,[],[f27272,f32]) ).
fof(f27677,plain,
! [X2,X0,X1] : addition(multiplication(X1,strong_iteration(X0)),multiplication(X2,one)) = addition(multiplication(X1,multiplication(strong_iteration(X0),X0)),addition(X1,X2)),
inference(forward_demodulation,[],[f27138,f32]) ).
fof(f27679,plain,
! [X2,X0,X1] : addition(multiplication(X1,star(X0)),multiplication(X2,one)) = addition(multiplication(X1,multiplication(star(X0),X0)),addition(X1,X2)),
inference(forward_demodulation,[],[f27136,f32]) ).
fof(f27907,plain,
! [X0] : addition(sF7,X0) = addition(multiplication(sF7,sK1),addition(sF7,X0)),
inference(forward_demodulation,[],[f27601,f32]) ).
fof(f27940,plain,
! [X2,X0,X1] : addition(multiplication(X1,strong_iteration(X0)),X2) = addition(multiplication(X1,multiplication(strong_iteration(X0),X0)),addition(X1,X2)),
inference(forward_demodulation,[],[f27677,f32]) ).
fof(f27942,plain,
! [X2,X0,X1] : addition(multiplication(X1,star(X0)),X2) = addition(multiplication(X1,multiplication(star(X0),X0)),addition(X1,X2)),
inference(forward_demodulation,[],[f27679,f32]) ).
fof(f28304,plain,
! [X0,X1] : addition(multiplication(X0,star(X1)),X0) = addition(multiplication(X0,multiplication(star(X1),X1)),X0),
inference(superposition,[],[f27942,f30]) ).
fof(f28314,plain,
! [X0,X1] : addition(multiplication(X0,star(X1)),zero) = addition(multiplication(X0,multiplication(star(X1),X1)),X0),
inference(superposition,[],[f27942,f29]) ).
fof(f28386,plain,
! [X0,X1] : addition(multiplication(one,star(X1)),multiplication(X0,star(X0))) = addition(multiplication(one,multiplication(star(X1),X1)),star(X0)),
inference(superposition,[],[f27942,f37]) ).
fof(f28392,plain,
! [X0,X1] : addition(multiplication(one,star(X1)),multiplication(strong_iteration(X0),X0)) = addition(multiplication(one,multiplication(star(X1),X1)),strong_iteration(X0)),
inference(superposition,[],[f27942,f2637]) ).
fof(f28399,plain,
! [X0,X1] : addition(multiplication(one,multiplication(star(X1),X1)),star(X0)) = addition(multiplication(one,star(X1)),star(X0)),
inference(superposition,[],[f27942,f367]) ).
fof(f28400,plain,
! [X0,X1] : addition(multiplication(one,multiplication(star(X1),X1)),strong_iteration(X0)) = addition(multiplication(one,star(X1)),strong_iteration(X0)),
inference(superposition,[],[f27942,f1669]) ).
fof(f28466,plain,
! [X0] : addition(multiplication(sF4,star(X0)),multiplication(sF7,zero)) = addition(multiplication(sF4,multiplication(star(X0),X0)),sF7),
inference(superposition,[],[f27942,f70]) ).
fof(f28470,plain,
! [X0] : addition(multiplication(sF4,multiplication(star(X0),X0)),sF7) = addition(multiplication(sF4,star(X0)),sF7),
inference(superposition,[],[f27942,f3187]) ).
fof(f28632,plain,
! [X0] : addition(multiplication(sF4,multiplication(star(X0),X0)),sF7) = multiplication(sF4,addition(star(X0),sF7)),
inference(forward_demodulation,[],[f28470,f20806]) ).
fof(f28635,plain,
! [X0] : addition(multiplication(sF4,star(X0)),multiplication(sF7,zero)) = multiplication(sF4,addition(multiplication(star(X0),X0),sF7)),
inference(forward_demodulation,[],[f28466,f20806]) ).
fof(f28684,plain,
! [X0,X1] : addition(multiplication(one,multiplication(star(X1),X1)),strong_iteration(X0)) = addition(star(X1),strong_iteration(X0)),
inference(forward_demodulation,[],[f28400,f33]) ).
fof(f28685,plain,
! [X0,X1] : addition(multiplication(one,multiplication(star(X1),X1)),star(X0)) = addition(star(X1),star(X0)),
inference(forward_demodulation,[],[f28399,f33]) ).
fof(f28692,plain,
! [X0,X1] : addition(multiplication(star(X1),X1),strong_iteration(X0)) = addition(multiplication(one,star(X1)),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f28392,f33]) ).
fof(f28698,plain,
! [X0,X1] : addition(multiplication(one,star(X1)),multiplication(X0,star(X0))) = addition(multiplication(star(X1),X1),star(X0)),
inference(forward_demodulation,[],[f28386,f33]) ).
fof(f28761,plain,
! [X0,X1] : addition(multiplication(X0,star(X1)),zero) = multiplication(X0,addition(multiplication(star(X1),X1),one)),
inference(forward_demodulation,[],[f28314,f137]) ).
fof(f28768,plain,
! [X0,X1] : addition(multiplication(X0,star(X1)),X0) = multiplication(X0,addition(multiplication(star(X1),X1),one)),
inference(forward_demodulation,[],[f28304,f137]) ).
fof(f28816,plain,
! [X0] : multiplication(sF4,addition(star(X0),sF7)) = multiplication(sF4,addition(multiplication(star(X0),X0),sF7)),
inference(forward_demodulation,[],[f28632,f20806]) ).
fof(f28818,plain,
! [X0] : multiplication(sF7,star(X0)) = multiplication(sF4,addition(multiplication(star(X0),X0),sF7)),
inference(forward_demodulation,[],[f28635,f10014]) ).
fof(f28851,plain,
! [X0,X1] : addition(multiplication(star(X1),X1),strong_iteration(X0)) = addition(star(X1),strong_iteration(X0)),
inference(forward_demodulation,[],[f28684,f33]) ).
fof(f28852,plain,
! [X0,X1] : addition(star(X1),star(X0)) = addition(multiplication(star(X1),X1),star(X0)),
inference(forward_demodulation,[],[f28685,f33]) ).
fof(f28859,plain,
! [X0,X1] : addition(multiplication(star(X1),X1),strong_iteration(X0)) = addition(star(X1),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f28692,f33]) ).
fof(f28865,plain,
! [X0,X1] : addition(multiplication(star(X1),X1),star(X0)) = addition(star(X1),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f28698,f33]) ).
fof(f28925,plain,
! [X0,X1] : multiplication(X0,star(X1)) = multiplication(X0,addition(multiplication(star(X1),X1),one)),
inference(forward_demodulation,[],[f28761,f29]) ).
fof(f28927,plain,
! [X0,X1] : multiplication(X0,addition(star(X1),one)) = multiplication(X0,addition(multiplication(star(X1),X1),one)),
inference(forward_demodulation,[],[f28768,f137]) ).
fof(f28953,plain,
! [X0] : multiplication(sF7,star(X0)) = multiplication(sF4,addition(star(X0),sF7)),
inference(forward_demodulation,[],[f28818,f28816]) ).
fof(f28979,plain,
! [X0,X1] : addition(star(X1),strong_iteration(X0)) = addition(star(X1),multiplication(strong_iteration(X0),X0)),
inference(forward_demodulation,[],[f28859,f28851]) ).
fof(f28981,plain,
! [X0,X1] : addition(star(X1),star(X0)) = addition(star(X1),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f28865,f28852]) ).
fof(f29024,plain,
! [X0,X1] : multiplication(X0,star(X1)) = multiplication(X0,addition(star(X1),one)),
inference(forward_demodulation,[],[f28927,f28925]) ).
fof(f29153,plain,
! [X0] : addition(star(X0),zero) = addition(star(X0),star(zero)),
inference(superposition,[],[f28981,f36]) ).
fof(f29243,plain,
! [X0] : addition(star(X0),zero) = addition(star(X0),one),
inference(forward_demodulation,[],[f29153,f3245]) ).
fof(f29261,plain,
! [X0] : star(X0) = addition(star(X0),one),
inference(forward_demodulation,[],[f29243,f29]) ).
fof(f29279,plain,
! [X0] : addition(one,multiplication(X0,star(X0))) = addition(star(X0),multiplication(X0,one)),
inference(superposition,[],[f3458,f29024]) ).
fof(f29287,plain,
! [X2,X0,X1] : addition(multiplication(addition(X2,X0),star(X1)),multiplication(X0,one)) = addition(multiplication(X2,star(X1)),multiplication(X0,star(X1))),
inference(superposition,[],[f6824,f29024]) ).
fof(f29466,plain,
! [X2,X0,X1] : multiplication(addition(X2,X0),star(X1)) = addition(multiplication(addition(X2,X0),star(X1)),multiplication(X0,one)),
inference(forward_demodulation,[],[f29287,f35]) ).
fof(f29472,plain,
! [X0] : addition(one,multiplication(X0,star(X0))) = addition(star(X0),X0),
inference(forward_demodulation,[],[f29279,f32]) ).
fof(f29527,plain,
! [X2,X0,X1] : multiplication(addition(X2,X0),star(X1)) = addition(multiplication(addition(X2,X0),star(X1)),X0),
inference(forward_demodulation,[],[f29466,f32]) ).
fof(f29531,plain,
! [X0] : star(X0) = addition(star(X0),X0),
inference(forward_demodulation,[],[f29472,f37]) ).
fof(f29784,plain,
sF4 = addition(sF4,one),
inference(superposition,[],[f29261,f52]) ).
fof(f29941,plain,
! [X0,X1] : addition(multiplication(sF4,X0),multiplication(one,addition(X0,X1))) = addition(multiplication(sF4,X0),multiplication(one,X1)),
inference(superposition,[],[f6824,f29784]) ).
fof(f29954,plain,
! [X0,X1] : addition(multiplication(sF4,X0),X1) = addition(multiplication(sF4,X0),multiplication(one,addition(X0,X1))),
inference(forward_demodulation,[],[f29941,f33]) ).
fof(f29985,plain,
! [X0,X1] : addition(multiplication(sF4,X0),X1) = addition(multiplication(sF4,X0),addition(X0,X1)),
inference(forward_demodulation,[],[f29954,f33]) ).
fof(f31052,plain,
! [X0,X1] : addition(star(X0),strong_iteration(X1)) = addition(multiplication(strong_iteration(X1),X1),star(X0)),
inference(superposition,[],[f27,f28979]) ).
fof(f31256,plain,
! [X0] : multiplication(X0,star(one)) = multiplication(X0,multiplication(addition(star(one),one),one)),
inference(superposition,[],[f28925,f193]) ).
fof(f31443,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,star(one)),
inference(forward_demodulation,[],[f31256,f24395]) ).
fof(f31501,plain,
! [X0] : multiplication(X0,star(one)) = X0,
inference(forward_demodulation,[],[f31443,f32]) ).
fof(f34507,plain,
addition(multiplication(sF4,sF6),sF7) = addition(multiplication(sF4,sF6),sF8),
inference(superposition,[],[f29985,f60]) ).
fof(f34638,plain,
addition(multiplication(sF4,sF6),sF8) = multiplication(sF4,addition(sF6,sF7)),
inference(forward_demodulation,[],[f34507,f20806]) ).
fof(f34809,plain,
multiplication(sF4,sF8) = addition(multiplication(sF4,sF6),sF8),
inference(forward_demodulation,[],[f34638,f60]) ).
fof(f35018,plain,
multiplication(sF4,sF8) = addition(sF8,multiplication(sF4,sF6)),
inference(superposition,[],[f27,f34809]) ).
fof(f35098,definition,
( spl9_189
<=> sF8 = multiplication(sF4,sF8) ),
introduced(definition,[new_symbols(definition,[spl9_189])],[avatar_definition]) ).
fof(f35099,plain,
( sF8 = multiplication(sF4,sF8)
| ~ spl9_189 ),
inference(avatar_component_clause,[],[f35098]) ).
fof(f35100,plain,
( sF8 != multiplication(sF4,sF8)
| spl9_189 ),
inference(avatar_component_clause,[],[f35098]) ).
fof(f36110,plain,
sF8 = addition(multiplication(sF7,sK1),sF8),
inference(superposition,[],[f27907,f4372]) ).
fof(f36260,plain,
sF8 = addition(sF8,multiplication(sF7,sK1)),
inference(superposition,[],[f27,f36110]) ).
fof(f36748,plain,
! [X0,X1] : multiplication(star(X0),star(X1)) = addition(multiplication(star(X0),star(X1)),multiplication(star(X0),X0)),
inference(superposition,[],[f29527,f38]) ).
fof(f36902,plain,
! [X0,X1] : addition(star(addition(X0,X1)),X1) = addition(one,multiplication(addition(X0,X1),star(addition(X0,X1)))),
inference(superposition,[],[f82,f29527]) ).
fof(f37025,plain,
! [X0,X1] : star(addition(X0,X1)) = addition(star(addition(X0,X1)),X1),
inference(forward_demodulation,[],[f36902,f37]) ).
fof(f37128,plain,
! [X0,X1] : multiplication(star(X0),star(X1)) = multiplication(star(X0),addition(star(X1),X0)),
inference(forward_demodulation,[],[f36748,f34]) ).
fof(f37483,plain,
star(sF3) = addition(star(sF3),sF4),
inference(superposition,[],[f37025,f7592]) ).
fof(f38107,plain,
! [X0] : multiplication(star(X0),sF4) = multiplication(star(X0),addition(sF4,X0)),
inference(superposition,[],[f37128,f52]) ).
fof(f42852,plain,
! [X0] : multiplication(star(X0),multiplication(X0,star(X0))) = multiplication(multiplication(X0,star(X0)),star(X0)),
inference(superposition,[],[f210,f37]) ).
fof(f42856,plain,
! [X0] : multiplication(multiplication(star(X0),X0),star(X0)) = multiplication(star(X0),multiplication(star(X0),X0)),
inference(superposition,[],[f210,f38]) ).
fof(f42858,plain,
! [X0] : multiplication(multiplication(strong_iteration(X0),X0),strong_iteration(X0)) = multiplication(strong_iteration(X0),multiplication(strong_iteration(X0),X0)),
inference(superposition,[],[f210,f2637]) ).
fof(f42906,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = addition(multiplication(multiplication(X0,strong_iteration(X0)),addition(one,multiplication(X0,strong_iteration(X0)))),multiplication(X0,strong_iteration(X0))),
inference(superposition,[],[f9792,f210]) ).
fof(f43022,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = multiplication(multiplication(X0,strong_iteration(X0)),addition(addition(one,multiplication(X0,strong_iteration(X0))),one)),
inference(forward_demodulation,[],[f42906,f137]) ).
fof(f43054,plain,
! [X0] : multiplication(strong_iteration(X0),X0) = multiplication(multiplication(strong_iteration(X0),X0),strong_iteration(X0)),
inference(forward_demodulation,[],[f42858,f20908]) ).
fof(f43056,plain,
! [X0] : multiplication(star(X0),X0) = multiplication(multiplication(star(X0),X0),star(X0)),
inference(forward_demodulation,[],[f42856,f13556]) ).
fof(f43060,plain,
! [X0] : multiplication(star(X0),multiplication(X0,star(X0))) = multiplication(X0,multiplication(star(X0),star(X0))),
inference(forward_demodulation,[],[f42852,f31]) ).
fof(f43086,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = multiplication(X0,multiplication(strong_iteration(X0),addition(addition(one,multiplication(X0,strong_iteration(X0))),one))),
inference(forward_demodulation,[],[f43022,f31]) ).
fof(f43110,plain,
! [X0] : multiplication(strong_iteration(X0),X0) = multiplication(strong_iteration(X0),multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[],[f43054,f31]) ).
fof(f43112,plain,
! [X0] : multiplication(star(X0),X0) = multiplication(star(X0),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f43056,f31]) ).
fof(f43114,plain,
! [X0] : multiplication(X0,star(X0)) = multiplication(star(X0),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f43060,f13535]) ).
fof(f43130,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = multiplication(X0,multiplication(strong_iteration(X0),addition(one,addition(multiplication(X0,strong_iteration(X0)),one)))),
inference(forward_demodulation,[],[f43086,f28]) ).
fof(f43147,plain,
! [X0] : multiplication(X0,star(X0)) = multiplication(star(X0),X0),
inference(forward_demodulation,[],[f43114,f43112]) ).
fof(f43158,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = multiplication(X0,multiplication(strong_iteration(X0),addition(strong_iteration(X0),one))),
inference(forward_demodulation,[],[f43130,f12442]) ).
fof(f43177,plain,
! [X0] : multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)) = multiplication(X0,multiplication(strong_iteration(X0),addition(one,one))),
inference(forward_demodulation,[],[f43158,f20952]) ).
fof(f43189,plain,
! [X0] : multiplication(X0,multiplication(strong_iteration(X0),one)) = multiplication(addition(multiplication(one,X0),multiplication(X0,strong_iteration(X0))),strong_iteration(X0)),
inference(forward_demodulation,[],[f43177,f30]) ).
fof(f43195,plain,
! [X0] : multiplication(X0,multiplication(strong_iteration(X0),one)) = multiplication(addition(one,strong_iteration(X0)),multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[],[f43189,f11875]) ).
fof(f43200,plain,
! [X0] : multiplication(X0,multiplication(strong_iteration(X0),one)) = multiplication(strong_iteration(X0),multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[],[f43195,f1110]) ).
fof(f43203,plain,
! [X0] : multiplication(strong_iteration(X0),X0) = multiplication(X0,multiplication(strong_iteration(X0),one)),
inference(forward_demodulation,[],[f43200,f43110]) ).
fof(f43204,plain,
! [X0] : multiplication(X0,strong_iteration(X0)) = multiplication(strong_iteration(X0),X0),
inference(forward_demodulation,[],[f43203,f32]) ).
fof(f43206,plain,
multiplication(sF2,sF3) = multiplication(sF3,sF2),
inference(superposition,[],[f43204,f50]) ).
fof(f43426,plain,
! [X0,X1] : multiplication(star(X0),multiplication(X0,X1)) = multiplication(multiplication(X0,star(X0)),X1),
inference(superposition,[],[f31,f43147]) ).
fof(f43520,plain,
! [X0,X1] : multiplication(star(X0),multiplication(X0,X1)) = multiplication(X0,multiplication(star(X0),X1)),
inference(forward_demodulation,[],[f43426,f31]) ).
fof(f48597,plain,
addition(multiplication(sF4,one),sF3) = addition(multiplication(sF4,one),multiplication(sF2,sF3)),
inference(superposition,[],[f29985,f8834]) ).
fof(f48603,plain,
addition(sF4,sF3) = addition(sF4,multiplication(sF2,sF3)),
inference(forward_demodulation,[],[f48597,f32]) ).
fof(f48638,plain,
sF3 = addition(sF4,multiplication(sF2,sF3)),
inference(forward_demodulation,[],[f48603,f7548]) ).
fof(f50761,plain,
! [X0] : addition(strong_iteration(X0),sF3) = addition(multiplication(sF3,sF2),strong_iteration(X0)),
inference(superposition,[],[f2686,f50]) ).
fof(f50933,plain,
! [X0] : addition(strong_iteration(X0),sF3) = addition(multiplication(sF2,sF3),strong_iteration(X0)),
inference(forward_demodulation,[],[f50761,f43206]) ).
fof(f53161,plain,
addition(multiplication(sF4,sF8),sF8) = addition(multiplication(sF4,sF8),multiplication(sF7,sK1)),
inference(superposition,[],[f29985,f36260]) ).
fof(f53170,plain,
addition(multiplication(sF4,sF8),sF8) = multiplication(sF7,addition(sF8,sK1)),
inference(forward_demodulation,[],[f53161,f11168]) ).
fof(f53197,plain,
multiplication(sF7,sF8) = addition(multiplication(sF4,sF8),sF8),
inference(forward_demodulation,[],[f53170,f2037]) ).
fof(f53215,plain,
multiplication(sF7,sF8) = multiplication(addition(sF4,one),sF8),
inference(forward_demodulation,[],[f53197,f193]) ).
fof(f53220,plain,
multiplication(sF4,sF8) = multiplication(sF7,sF8),
inference(forward_demodulation,[],[f53215,f29784]) ).
fof(f53226,plain,
! [X0] : addition(multiplication(X0,sF8),multiplication(sF4,sF8)) = multiplication(addition(X0,sF7),sF8),
inference(superposition,[],[f35,f53220]) ).
fof(f53267,plain,
! [X0] : multiplication(addition(X0,sF4),sF8) = multiplication(addition(X0,sF7),sF8),
inference(forward_demodulation,[],[f53226,f35]) ).
fof(f55518,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = addition(sF4,addition(multiplication(sF4,X0),multiplication(sF7,zero))),
inference(superposition,[],[f10014,f168]) ).
fof(f55666,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = addition(multiplication(sF4,X0),sF7),
inference(forward_demodulation,[],[f55518,f12288]) ).
fof(f55921,plain,
! [X0] : multiplication(sF7,addition(one,X0)) = multiplication(sF4,addition(X0,sF7)),
inference(forward_demodulation,[],[f55666,f20806]) ).
fof(f59839,plain,
! [X2,X0,X1] :
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| addition(multiplication(X0,multiplication(X2,star(X1))),X0) = X0 ),
inference(resolution,[],[f1758,f44]) ).
fof(f59909,plain,
! [X2,X0,X1] :
( ~ leq(multiplication(X0,addition(X1,X2)),X0)
| multiplication(X0,addition(multiplication(X2,star(X1)),one)) = X0 ),
inference(forward_demodulation,[],[f59839,f137]) ).
fof(f59920,plain,
! [X0,X1] :
( ~ leq(multiplication(X1,X0),X1)
| multiplication(X1,addition(multiplication(X0,star(X0)),one)) = X1 ),
inference(superposition,[],[f59909,f30]) ).
fof(f59983,plain,
! [X0,X1] :
( ~ leq(multiplication(X1,strong_iteration(X0)),X1)
| multiplication(X1,addition(multiplication(one,star(multiplication(X0,strong_iteration(X0)))),one)) = X1 ),
inference(superposition,[],[f59909,f41]) ).
fof(f60232,plain,
! [X0] :
( ~ leq(star(X0),star(X0))
| star(X0) = multiplication(star(X0),addition(multiplication(one,star(star(X0))),one)) ),
inference(superposition,[],[f59909,f13483]) ).
fof(f60266,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(multiplication(one,star(star(X0))),one)),
inference(forward_subsumption_resolution,[],[f60232,f352]) ).
fof(f60447,plain,
! [X0,X1] :
( multiplication(X1,multiplication(one,addition(star(multiplication(X0,strong_iteration(X0))),one))) = X1
| ~ leq(multiplication(X1,strong_iteration(X0)),X1) ),
inference(forward_demodulation,[],[f59983,f137]) ).
fof(f60490,plain,
! [X0,X1] :
( ~ leq(multiplication(X1,X0),X1)
| multiplication(X1,star(X0)) = X1 ),
inference(forward_demodulation,[],[f59920,f3521]) ).
fof(f60500,plain,
! [X0] : star(X0) = multiplication(star(X0),multiplication(one,addition(star(star(X0)),one))),
inference(forward_demodulation,[],[f60266,f137]) ).
fof(f60602,plain,
! [X0,X1] :
( multiplication(X1,addition(star(multiplication(X0,strong_iteration(X0))),one)) = X1
| ~ leq(multiplication(X1,strong_iteration(X0)),X1) ),
inference(forward_demodulation,[],[f60447,f33]) ).
fof(f60632,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(star(star(X0)),one)),
inference(forward_demodulation,[],[f60500,f33]) ).
fof(f60677,plain,
! [X0,X1] :
( ~ leq(multiplication(X1,strong_iteration(X0)),X1)
| multiplication(X1,star(multiplication(X0,strong_iteration(X0)))) = X1 ),
inference(forward_demodulation,[],[f60602,f29024]) ).
fof(f60688,plain,
! [X0] : star(X0) = multiplication(star(X0),star(star(X0))),
inference(forward_demodulation,[],[f60632,f29024]) ).
fof(f60710,plain,
! [X0] : star(X0) = star(star(X0)),
inference(forward_demodulation,[],[f60688,f8734]) ).
fof(f60718,plain,
sF4 = star(sF4),
inference(superposition,[],[f60710,f52]) ).
fof(f61323,plain,
! [X0] :
( ~ leq(strong_iteration(X0),strong_iteration(X0))
| strong_iteration(X0) = multiplication(strong_iteration(X0),star(strong_iteration(X0))) ),
inference(superposition,[],[f60490,f20799]) ).
fof(f61331,plain,
( ~ leq(sF3,sF3)
| sF3 = multiplication(sF3,star(sF3)) ),
inference(superposition,[],[f60490,f20902]) ).
fof(f61377,plain,
sF3 = multiplication(sF3,star(sF3)),
inference(forward_subsumption_resolution,[],[f61331,f352]) ).
fof(f61390,plain,
! [X0] : strong_iteration(X0) = multiplication(strong_iteration(X0),star(strong_iteration(X0))),
inference(forward_subsumption_resolution,[],[f61323,f352]) ).
fof(f61484,plain,
sF3 = star(sF3),
inference(forward_demodulation,[],[f61377,f8736]) ).
fof(f61487,plain,
! [X0] : strong_iteration(X0) = star(strong_iteration(X0)),
inference(forward_demodulation,[],[f61390,f8113]) ).
fof(f62868,plain,
! [X0] :
( ~ leq(strong_iteration(X0),strong_iteration(X0))
| strong_iteration(X0) = multiplication(strong_iteration(X0),star(multiplication(X0,strong_iteration(X0)))) ),
inference(superposition,[],[f60677,f20799]) ).
fof(f62874,plain,
! [X0] : strong_iteration(X0) = multiplication(strong_iteration(X0),star(multiplication(X0,strong_iteration(X0)))),
inference(forward_subsumption_resolution,[],[f62868,f352]) ).
fof(f62887,plain,
! [X0] : strong_iteration(X0) = star(multiplication(X0,strong_iteration(X0))),
inference(forward_demodulation,[],[f62874,f9000]) ).
fof(f62911,plain,
sF3 = star(multiplication(sF2,sF3)),
inference(superposition,[],[f62887,f50]) ).
fof(f63263,plain,
multiplication(sF3,sF4) = multiplication(sF3,addition(sF4,multiplication(sF2,sF3))),
inference(superposition,[],[f38107,f62911]) ).
fof(f63286,plain,
multiplication(sF3,sF4) = multiplication(sF3,sF3),
inference(forward_demodulation,[],[f63263,f48638]) ).
fof(f63351,plain,
sF3 = multiplication(sF3,sF4),
inference(forward_demodulation,[],[f63286,f20902]) ).
fof(f63407,plain,
multiplication(sF5,sF3) = multiplication(sF6,sF4),
inference(superposition,[],[f116,f63351]) ).
fof(f63425,plain,
! [X0,X1] : addition(multiplication(sF3,X0),addition(sF3,X1)) = addition(multiplication(sF3,addition(X0,sF4)),X1),
inference(superposition,[],[f146,f63351]) ).
fof(f63456,plain,
sF6 = multiplication(sF6,sF4),
inference(forward_demodulation,[],[f63407,f56]) ).
fof(f63464,plain,
! [X0] : multiplication(sF6,X0) = multiplication(sF6,multiplication(sF4,X0)),
inference(superposition,[],[f31,f63456]) ).
fof(f72963,plain,
multiplication(sF6,sK0) = multiplication(sF6,sF5),
inference(superposition,[],[f63464,f54]) ).
fof(f84969,definition,
( spl9_389
<=> leq(sF3,sF8) ),
introduced(definition,[new_symbols(definition,[spl9_389])],[avatar_definition]) ).
fof(f84970,plain,
( ~ leq(sF3,sF8)
| spl9_389 ),
inference(avatar_component_clause,[],[f84969]) ).
fof(f94086,plain,
! [X0] : multiplication(star(sF4),multiplication(sF5,X0)) = multiplication(sF4,multiplication(star(sF4),multiplication(sK0,X0))),
inference(superposition,[],[f43520,f115]) ).
fof(f94090,plain,
multiplication(star(sF4),sF5) = multiplication(sF4,multiplication(star(sF4),sK0)),
inference(superposition,[],[f43520,f54]) ).
fof(f94227,plain,
multiplication(sF4,sF5) = multiplication(sF4,multiplication(sF4,sK0)),
inference(forward_demodulation,[],[f94090,f60718]) ).
fof(f94231,plain,
! [X0] : multiplication(sF4,multiplication(sF5,X0)) = multiplication(sF4,multiplication(sF4,multiplication(sK0,X0))),
inference(forward_demodulation,[],[f94086,f60718]) ).
fof(f94347,plain,
multiplication(sF4,sK0) = multiplication(sF4,sF5),
inference(forward_demodulation,[],[f94227,f13710]) ).
fof(f94349,plain,
! [X0] : multiplication(sF4,multiplication(sK0,X0)) = multiplication(sF4,multiplication(sF5,X0)),
inference(forward_demodulation,[],[f94231,f13710]) ).
fof(f94408,plain,
sF5 = multiplication(sF4,sF5),
inference(forward_demodulation,[],[f94347,f54]) ).
fof(f94409,plain,
! [X0] : multiplication(sF5,X0) = multiplication(sF4,multiplication(sF5,X0)),
inference(forward_demodulation,[],[f94349,f115]) ).
fof(f94464,plain,
addition(sF5,multiplication(sF7,zero)) = multiplication(sF7,sF5),
inference(superposition,[],[f10014,f94408]) ).
fof(f94529,plain,
multiplication(sF7,sK0) = multiplication(sF7,sF5),
inference(forward_demodulation,[],[f94464,f11097]) ).
fof(f99333,plain,
! [X2,X0,X1] : multiplication(star(X0),addition(X1,multiplication(X0,X2))) = addition(X1,multiplication(X0,multiplication(star(X0),addition(X1,X2)))),
inference(superposition,[],[f9988,f43520]) ).
fof(f103174,plain,
sF6 = multiplication(sF4,sF6),
inference(superposition,[],[f94409,f56]) ).
fof(f103332,plain,
addition(sF8,sF6) = multiplication(sF4,sF8),
inference(superposition,[],[f35018,f103174]) ).
fof(f103409,plain,
sF8 = multiplication(sF4,sF8),
inference(forward_demodulation,[],[f103332,f5266]) ).
fof(f103420,plain,
( $false
| spl9_189 ),
inference(forward_subsumption_resolution,[],[f103409,f35100]) ).
fof(f103421,plain,
spl9_189,
inference(avatar_contradiction_clause,[],[f103420]) ).
fof(f103861,plain,
( ! [X0] : multiplication(addition(X0,sF4),sF8) = addition(multiplication(X0,sF8),sF8)
| ~ spl9_189 ),
inference(superposition,[],[f35,f35099]) ).
fof(f103920,plain,
( ! [X0] : multiplication(addition(X0,sF4),sF8) = multiplication(addition(X0,one),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f103861,f193]) ).
fof(f130398,plain,
addition(multiplication(star(sF3),addition(sF4,sK0)),sF5) = addition(star(sF3),multiplication(addition(star(sF3),sF4),sK0)),
inference(superposition,[],[f530,f7741]) ).
fof(f130931,plain,
addition(multiplication(star(sF3),addition(sF4,sK0)),sF5) = addition(star(sF3),multiplication(star(sF3),sK0)),
inference(forward_demodulation,[],[f130398,f37483]) ).
fof(f131203,plain,
multiplication(star(sF3),addition(one,sK0)) = addition(multiplication(star(sF3),addition(sF4,sK0)),sF5),
inference(forward_demodulation,[],[f130931,f133]) ).
fof(f131408,plain,
multiplication(star(sF3),addition(one,sK0)) = addition(multiplication(star(sF3),addition(sF2,sF4)),sF5),
inference(forward_demodulation,[],[f131203,f8269]) ).
fof(f131571,plain,
multiplication(sF3,addition(one,sK0)) = addition(multiplication(sF3,addition(sF2,sF4)),sF5),
inference(forward_demodulation,[],[f131408,f61484]) ).
fof(f131701,plain,
multiplication(sF3,addition(one,sK0)) = addition(multiplication(sF3,sF2),addition(sF3,sF5)),
inference(forward_demodulation,[],[f131571,f63425]) ).
fof(f131795,plain,
addition(sF3,multiplication(sF3,sF2)) = multiplication(sF3,addition(one,sK0)),
inference(forward_demodulation,[],[f131701,f25267]) ).
fof(f131866,plain,
multiplication(sF3,addition(one,sF2)) = multiplication(sF3,addition(one,sK0)),
inference(forward_demodulation,[],[f131795,f133]) ).
fof(f131922,plain,
sF3 = multiplication(sF3,addition(one,sK0)),
inference(forward_demodulation,[],[f131866,f13853]) ).
fof(f132416,plain,
! [X0] : addition(sF3,multiplication(X0,sK0)) = addition(multiplication(sF3,one),multiplication(addition(sF3,X0),sK0)),
inference(superposition,[],[f444,f131922]) ).
fof(f132491,plain,
! [X0] : addition(sF3,multiplication(X0,sK0)) = addition(sF3,multiplication(addition(sF3,X0),sK0)),
inference(forward_demodulation,[],[f132416,f32]) ).
fof(f132886,plain,
addition(sF3,multiplication(sF3,sK0)) = addition(sF3,multiplication(sF6,sK0)),
inference(superposition,[],[f132491,f18009]) ).
fof(f133051,plain,
addition(sF3,multiplication(sF3,sK0)) = addition(sF3,multiplication(sF6,sF5)),
inference(forward_demodulation,[],[f132886,f72963]) ).
fof(f133116,plain,
multiplication(sF3,addition(one,sK0)) = addition(sF3,multiplication(sF6,sF5)),
inference(forward_demodulation,[],[f133051,f133]) ).
fof(f133165,plain,
sF3 = addition(sF3,multiplication(sF6,sF5)),
inference(forward_demodulation,[],[f133116,f131922]) ).
fof(f133450,plain,
addition(one,multiplication(sF3,star(sF3))) = multiplication(addition(one,multiplication(sF6,sF5)),star(sF3)),
inference(superposition,[],[f3512,f133165]) ).
fof(f133514,plain,
addition(one,multiplication(sF3,sF3)) = multiplication(addition(one,multiplication(sF6,sF5)),sF3),
inference(forward_demodulation,[],[f133450,f61484]) ).
fof(f133570,plain,
addition(one,multiplication(sF3,sF3)) = addition(sF3,multiplication(sF6,sF6)),
inference(forward_demodulation,[],[f133514,f22845]) ).
fof(f133589,plain,
addition(one,sF3) = addition(sF3,multiplication(sF6,sF6)),
inference(forward_demodulation,[],[f133570,f20902]) ).
fof(f133601,plain,
sF3 = addition(sF3,multiplication(sF6,sF6)),
inference(forward_demodulation,[],[f133589,f1689]) ).
fof(f135520,plain,
! [X0,X1] : strong_iteration(addition(X1,X0)) = addition(strong_iteration(X0),strong_iteration(addition(X1,X0))),
inference(resolution,[],[f7267,f44]) ).
fof(f136355,plain,
strong_iteration(sF2) = addition(strong_iteration(sK1),strong_iteration(sF2)),
inference(superposition,[],[f135520,f48]) ).
fof(f136512,plain,
! [X0,X1] : multiplication(strong_iteration(addition(X0,X1)),star(strong_iteration(addition(X0,X1)))) = multiplication(strong_iteration(X1),star(strong_iteration(addition(X0,X1)))),
inference(superposition,[],[f2550,f135520]) ).
fof(f136633,plain,
! [X0,X1] : multiplication(strong_iteration(addition(X0,X1)),strong_iteration(addition(X0,X1))) = multiplication(strong_iteration(X1),strong_iteration(addition(X0,X1))),
inference(forward_demodulation,[],[f136512,f61487]) ).
fof(f136664,plain,
sF3 = addition(strong_iteration(sK1),sF3),
inference(forward_demodulation,[],[f136355,f50]) ).
fof(f136738,plain,
! [X0,X1] : strong_iteration(addition(X0,X1)) = multiplication(strong_iteration(X1),strong_iteration(addition(X0,X1))),
inference(forward_demodulation,[],[f136633,f20799]) ).
fof(f136753,plain,
sF3 = addition(sF7,sF3),
inference(forward_demodulation,[],[f136664,f58]) ).
fof(f136781,plain,
sF3 = multiplication(sF7,sF3),
inference(forward_demodulation,[],[f136753,f21603]) ).
fof(f136790,plain,
( $false
| spl9_162 ),
inference(forward_subsumption_resolution,[],[f136781,f21733]) ).
fof(f136791,plain,
spl9_162,
inference(avatar_contradiction_clause,[],[f136790]) ).
fof(f137086,plain,
! [X0,X1] : strong_iteration(addition(X0,X1)) = multiplication(strong_iteration(X0),strong_iteration(addition(X0,X1))),
inference(superposition,[],[f136738,f27]) ).
fof(f139155,plain,
! [X0,X1] : multiplication(strong_iteration(X0),addition(strong_iteration(addition(X0,X1)),one)) = addition(strong_iteration(addition(X0,X1)),strong_iteration(X0)),
inference(superposition,[],[f137,f137086]) ).
fof(f139206,plain,
! [X0,X1] : multiplication(strong_iteration(X0),strong_iteration(addition(X0,X1))) = addition(strong_iteration(addition(X0,X1)),strong_iteration(X0)),
inference(forward_demodulation,[],[f139155,f1245]) ).
fof(f139385,plain,
! [X0,X1] : strong_iteration(addition(X0,X1)) = addition(strong_iteration(addition(X0,X1)),strong_iteration(X0)),
inference(forward_demodulation,[],[f139206,f137086]) ).
fof(f149411,plain,
! [X0,X1] : addition(one,multiplication(star(strong_iteration(addition(X0,X1))),strong_iteration(addition(X0,X1)))) = multiplication(star(strong_iteration(addition(X0,X1))),addition(one,strong_iteration(X0))),
inference(superposition,[],[f724,f139385]) ).
fof(f149499,plain,
! [X0,X1] : addition(one,multiplication(star(strong_iteration(addition(X0,X1))),strong_iteration(addition(X0,X1)))) = multiplication(star(strong_iteration(addition(X0,X1))),strong_iteration(X0)),
inference(forward_demodulation,[],[f149411,f1267]) ).
fof(f149674,plain,
! [X0,X1] : multiplication(strong_iteration(addition(X0,X1)),strong_iteration(X0)) = addition(one,multiplication(strong_iteration(addition(X0,X1)),strong_iteration(addition(X0,X1)))),
inference(forward_demodulation,[],[f149499,f61487]) ).
fof(f149741,plain,
! [X0,X1] : multiplication(strong_iteration(addition(X0,X1)),strong_iteration(X0)) = multiplication(strong_iteration(addition(X0,X1)),strong_iteration(addition(X0,X1))),
inference(forward_demodulation,[],[f149674,f10891]) ).
fof(f149767,plain,
! [X0,X1] : strong_iteration(addition(X0,X1)) = multiplication(strong_iteration(addition(X0,X1)),strong_iteration(X0)),
inference(forward_demodulation,[],[f149741,f20799]) ).
fof(f150080,plain,
strong_iteration(sF2) = multiplication(strong_iteration(sF2),strong_iteration(sK1)),
inference(superposition,[],[f149767,f371]) ).
fof(f150413,plain,
strong_iteration(sF2) = multiplication(strong_iteration(sF2),sF7),
inference(forward_demodulation,[],[f150080,f58]) ).
fof(f150594,plain,
sF3 = multiplication(sF3,sF7),
inference(forward_demodulation,[],[f150413,f50]) ).
fof(f150689,plain,
multiplication(sF5,sF3) = multiplication(sF6,sF7),
inference(superposition,[],[f116,f150594]) ).
fof(f150692,plain,
! [X0] : multiplication(sF3,X0) = multiplication(sF3,multiplication(sF7,X0)),
inference(superposition,[],[f31,f150594]) ).
fof(f150759,plain,
sF6 = multiplication(sF6,sF7),
inference(forward_demodulation,[],[f150689,f56]) ).
fof(f150800,plain,
addition(sF7,sF6) = multiplication(addition(one,sF6),sF7),
inference(superposition,[],[f194,f150759]) ).
fof(f150846,plain,
sF8 = multiplication(addition(one,sF6),sF7),
inference(forward_demodulation,[],[f150800,f1804]) ).
fof(f151173,plain,
multiplication(sF3,sK0) = multiplication(sF3,multiplication(sF7,sF5)),
inference(superposition,[],[f150692,f94529]) ).
fof(f151301,plain,
multiplication(sF3,sK0) = multiplication(sF3,sF5),
inference(forward_demodulation,[],[f151173,f150692]) ).
fof(f151363,plain,
multiplication(sF3,addition(one,sK0)) = addition(sF3,multiplication(sF3,sF5)),
inference(superposition,[],[f133,f151301]) ).
fof(f151407,plain,
multiplication(sF3,addition(one,sK0)) = multiplication(sF3,addition(one,sF5)),
inference(forward_demodulation,[],[f151363,f133]) ).
fof(f151439,plain,
sF3 = multiplication(sF3,addition(one,sF5)),
inference(forward_demodulation,[],[f151407,f131922]) ).
fof(f151461,plain,
! [X0] : addition(sF3,multiplication(X0,sF5)) = addition(multiplication(sF3,one),multiplication(addition(sF3,X0),sF5)),
inference(superposition,[],[f444,f151439]) ).
fof(f151538,plain,
! [X0] : addition(sF3,multiplication(X0,sF5)) = addition(sF3,multiplication(addition(sF3,X0),sF5)),
inference(forward_demodulation,[],[f151461,f32]) ).
fof(f154130,plain,
! [X0] : multiplication(addition(one,multiplication(addition(sF3,X0),sF5)),star(sF3)) = addition(one,multiplication(addition(sF3,multiplication(X0,sF5)),star(sF3))),
inference(superposition,[],[f3512,f151538]) ).
fof(f154219,plain,
! [X0] : multiplication(addition(one,multiplication(addition(sF3,X0),sF5)),star(sF3)) = multiplication(addition(one,multiplication(X0,sF5)),star(sF3)),
inference(forward_demodulation,[],[f154130,f3512]) ).
fof(f154306,plain,
! [X0] : multiplication(addition(one,multiplication(X0,sF5)),sF3) = multiplication(addition(one,multiplication(addition(sF3,X0),sF5)),sF3),
inference(forward_demodulation,[],[f154219,f61484]) ).
fof(f154380,plain,
! [X0] : multiplication(addition(one,multiplication(X0,sF5)),sF3) = addition(sF3,multiplication(addition(sF3,X0),sF6)),
inference(forward_demodulation,[],[f154306,f22845]) ).
fof(f154431,plain,
! [X0] : addition(sF3,multiplication(X0,sF6)) = addition(sF3,multiplication(addition(sF3,X0),sF6)),
inference(forward_demodulation,[],[f154380,f22845]) ).
fof(f156389,plain,
addition(sF3,multiplication(sF6,sF6)) = addition(sF3,multiplication(sF3,sF6)),
inference(superposition,[],[f154431,f18009]) ).
fof(f156579,plain,
addition(sF3,multiplication(sF6,sF6)) = multiplication(sF3,addition(one,sF6)),
inference(forward_demodulation,[],[f156389,f133]) ).
fof(f156668,plain,
sF3 = multiplication(sF3,addition(one,sF6)),
inference(forward_demodulation,[],[f156579,f133601]) ).
fof(f156845,plain,
( ~ leq(sF3,sF3)
| sF3 = multiplication(sF3,addition(multiplication(sF6,star(one)),one)) ),
inference(superposition,[],[f59909,f156668]) ).
fof(f156913,plain,
sF3 = multiplication(sF3,addition(multiplication(sF6,star(one)),one)),
inference(forward_subsumption_resolution,[],[f156845,f352]) ).
fof(f156933,plain,
sF3 = multiplication(sF3,addition(sF6,one)),
inference(forward_demodulation,[],[f156913,f31501]) ).
fof(f156984,plain,
( ~ leq(sF3,sF3)
| sF3 = multiplication(sF3,addition(multiplication(one,star(sF6)),one)) ),
inference(superposition,[],[f59909,f156933]) ).
fof(f157052,plain,
sF3 = multiplication(sF3,addition(multiplication(one,star(sF6)),one)),
inference(forward_subsumption_resolution,[],[f156984,f352]) ).
fof(f157072,plain,
sF3 = multiplication(sF3,multiplication(one,addition(star(sF6),one))),
inference(forward_demodulation,[],[f157052,f137]) ).
fof(f157086,plain,
sF3 = multiplication(sF3,addition(star(sF6),one)),
inference(forward_demodulation,[],[f157072,f33]) ).
fof(f157091,plain,
sF3 = multiplication(sF3,star(sF6)),
inference(forward_demodulation,[],[f157086,f29024]) ).
fof(f157103,plain,
multiplication(sF5,sF3) = multiplication(sF6,star(sF6)),
inference(superposition,[],[f116,f157091]) ).
fof(f157128,plain,
multiplication(addition(one,sF3),star(sF6)) = addition(star(sF6),sF3),
inference(superposition,[],[f194,f157091]) ).
fof(f157167,plain,
multiplication(sF3,star(sF6)) = addition(star(sF6),sF3),
inference(forward_demodulation,[],[f157128,f1689]) ).
fof(f157180,plain,
sF6 = multiplication(sF6,star(sF6)),
inference(forward_demodulation,[],[f157103,f56]) ).
fof(f157200,plain,
sF3 = addition(star(sF6),sF3),
inference(forward_demodulation,[],[f157167,f157091]) ).
fof(f157220,plain,
addition(one,multiplication(sF6,sF3)) = addition(star(sF6),multiplication(sF6,sF3)),
inference(superposition,[],[f3458,f157200]) ).
fof(f157370,plain,
addition(one,sF6) = addition(star(sF6),sF6),
inference(forward_demodulation,[],[f157220,f21010]) ).
fof(f157398,plain,
star(sF6) = addition(one,sF6),
inference(forward_demodulation,[],[f157370,f29531]) ).
fof(f157767,plain,
sF8 = multiplication(star(sF6),sF7),
inference(superposition,[],[f150846,f157398]) ).
fof(f157834,plain,
addition(multiplication(sF7,one),sF6) = addition(multiplication(sF7,one),star(sF6)),
inference(superposition,[],[f9825,f157398]) ).
fof(f157841,plain,
! [X0] : addition(multiplication(one,strong_iteration(X0)),sF6) = addition(multiplication(one,multiplication(strong_iteration(X0),X0)),star(sF6)),
inference(superposition,[],[f27940,f157398]) ).
fof(f157890,plain,
! [X0] : addition(multiplication(one,strong_iteration(X0)),sF6) = addition(multiplication(strong_iteration(X0),X0),star(sF6)),
inference(forward_demodulation,[],[f157841,f33]) ).
fof(f157896,plain,
addition(sF7,sF6) = addition(sF7,star(sF6)),
inference(forward_demodulation,[],[f157834,f32]) ).
fof(f157932,plain,
! [X0] : addition(multiplication(one,strong_iteration(X0)),sF6) = addition(star(sF6),strong_iteration(X0)),
inference(forward_demodulation,[],[f157890,f31052]) ).
fof(f157936,plain,
sF8 = addition(sF7,star(sF6)),
inference(forward_demodulation,[],[f157896,f1804]) ).
fof(f157954,plain,
! [X0] : addition(strong_iteration(X0),sF6) = addition(star(sF6),strong_iteration(X0)),
inference(forward_demodulation,[],[f157932,f33]) ).
fof(f157974,plain,
! [X0] : addition(X0,multiplication(sF6,multiplication(star(sF6),addition(X0,sF7)))) = addition(multiplication(star(sF6),X0),multiplication(sF6,sF8)),
inference(superposition,[],[f9942,f157767]) ).
fof(f158065,plain,
! [X0] : addition(multiplication(star(sF6),X0),multiplication(sF6,sF8)) = multiplication(star(sF6),addition(X0,multiplication(sF6,sF7))),
inference(forward_demodulation,[],[f157974,f99333]) ).
fof(f158080,plain,
! [X0] : multiplication(star(sF6),addition(X0,sF6)) = addition(multiplication(star(sF6),X0),multiplication(sF6,sF8)),
inference(forward_demodulation,[],[f158065,f150759]) ).
fof(f158584,plain,
multiplication(sF7,sF8) = multiplication(sF7,addition(one,star(sF6))),
inference(superposition,[],[f20891,f157936]) ).
fof(f158741,plain,
multiplication(sF7,sF8) = multiplication(sF4,addition(star(sF6),sF7)),
inference(forward_demodulation,[],[f158584,f55921]) ).
fof(f158763,plain,
multiplication(sF7,star(sF6)) = multiplication(sF7,sF8),
inference(forward_demodulation,[],[f158741,f28953]) ).
fof(f158772,plain,
multiplication(sF7,star(sF6)) = multiplication(sF4,sF8),
inference(forward_demodulation,[],[f158763,f53220]) ).
fof(f158774,plain,
( sF8 = multiplication(sF7,star(sF6))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f158772,f35099]) ).
fof(f159531,plain,
addition(sF7,sF6) = addition(star(sF6),sF7),
inference(superposition,[],[f157954,f58]) ).
fof(f159716,plain,
sF8 = addition(star(sF6),sF7),
inference(forward_demodulation,[],[f159531,f1804]) ).
fof(f159752,plain,
addition(one,multiplication(sF6,sF8)) = addition(star(sF6),multiplication(sF6,sF7)),
inference(superposition,[],[f3458,f159716]) ).
fof(f159917,plain,
addition(star(sF6),sF6) = addition(one,multiplication(sF6,sF8)),
inference(forward_demodulation,[],[f159752,f150759]) ).
fof(f159947,plain,
star(sF6) = addition(one,multiplication(sF6,sF8)),
inference(forward_demodulation,[],[f159917,f29531]) ).
fof(f160043,plain,
addition(multiplication(one,zero),multiplication(sF6,sF8)) = addition(multiplication(star(sF6),zero),multiplication(sF6,sF8)),
inference(superposition,[],[f11882,f159947]) ).
fof(f160105,plain,
multiplication(star(sF6),addition(zero,sF6)) = addition(multiplication(one,zero),multiplication(sF6,sF8)),
inference(forward_demodulation,[],[f160043,f158080]) ).
fof(f160166,plain,
multiplication(star(sF6),addition(zero,sF6)) = addition(zero,multiplication(sF6,sF8)),
inference(forward_demodulation,[],[f160105,f33]) ).
fof(f160197,plain,
multiplication(sF6,sF8) = multiplication(star(sF6),addition(zero,sF6)),
inference(forward_demodulation,[],[f160166,f664]) ).
fof(f160218,plain,
multiplication(star(sF6),sF6) = multiplication(sF6,sF8),
inference(forward_demodulation,[],[f160197,f664]) ).
fof(f160227,plain,
multiplication(sF6,star(sF6)) = multiplication(sF6,sF8),
inference(forward_demodulation,[],[f160218,f43147]) ).
fof(f160232,plain,
sF6 = multiplication(sF6,sF8),
inference(forward_demodulation,[],[f160227,f157180]) ).
fof(f160244,plain,
! [X0] : addition(sF6,multiplication(X0,sF8)) = multiplication(addition(sF6,X0),sF8),
inference(superposition,[],[f35,f160232]) ).
fof(f160259,plain,
addition(sF6,sF8) = multiplication(addition(sF6,one),sF8),
inference(superposition,[],[f193,f160232]) ).
fof(f160295,plain,
sF8 = multiplication(addition(sF6,one),sF8),
inference(forward_demodulation,[],[f160259,f375]) ).
fof(f161720,plain,
addition(sF6,multiplication(sF7,sF8)) = multiplication(addition(sF6,addition(sF7,sF4)),sF8),
inference(superposition,[],[f160244,f11191]) ).
fof(f161899,plain,
addition(sF6,multiplication(sF7,sF8)) = multiplication(addition(sF8,sF4),sF8),
inference(forward_demodulation,[],[f161720,f86]) ).
fof(f161941,plain,
( addition(sF6,multiplication(sF7,sF8)) = multiplication(addition(sF8,one),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161899,f103920]) ).
fof(f161961,plain,
( addition(sF6,multiplication(sF7,sF8)) = multiplication(sF8,addition(sF8,one))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161941,f853]) ).
fof(f161970,plain,
( multiplication(sF8,sF8) = addition(sF6,multiplication(sF7,sF8))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161961,f3753]) ).
fof(f161975,plain,
( multiplication(sF8,sF8) = multiplication(addition(sF6,sF7),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161970,f160244]) ).
fof(f161977,plain,
( multiplication(sF8,sF8) = multiplication(addition(sF6,sF4),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161975,f53267]) ).
fof(f161978,plain,
( multiplication(sF8,sF8) = multiplication(addition(sF6,one),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161977,f103920]) ).
fof(f161979,plain,
( sF8 = multiplication(sF8,sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161978,f160295]) ).
fof(f161988,plain,
( ! [X0] : addition(multiplication(X0,sF8),sF8) = multiplication(addition(X0,sF8),sF8)
| ~ spl9_189 ),
inference(superposition,[],[f35,f161979]) ).
fof(f162050,plain,
( ! [X0] : multiplication(addition(X0,one),sF8) = multiplication(addition(X0,sF8),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f161988,f193]) ).
fof(f162903,plain,
( multiplication(sF8,sF8) = multiplication(addition(sK1,one),sF8)
| ~ spl9_189 ),
inference(superposition,[],[f162050,f3118]) ).
fof(f163045,plain,
( sF8 = multiplication(addition(sK1,one),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f162903,f161979]) ).
fof(f163596,plain,
( ! [X0] : addition(sF8,multiplication(one,X0)) = addition(multiplication(sK1,sF8),multiplication(one,addition(sF8,X0)))
| ~ spl9_189 ),
inference(superposition,[],[f6824,f163045]) ).
fof(f163688,plain,
( ! [X0] : addition(sF8,multiplication(one,X0)) = addition(multiplication(sK1,sF8),addition(sF8,X0))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f163596,f33]) ).
fof(f163711,plain,
( ! [X0] : addition(sF8,X0) = addition(multiplication(sK1,sF8),addition(sF8,X0))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f163688,f33]) ).
fof(f169033,plain,
( multiplication(sF3,star(sF6)) = multiplication(sF3,sF8)
| ~ spl9_189 ),
inference(superposition,[],[f150692,f158774]) ).
fof(f169116,plain,
( sF3 = multiplication(sF3,sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f169033,f157091]) ).
fof(f169143,plain,
( ~ leq(sF3,sF8)
| sF3 = sF8
| ~ spl9_189 ),
inference(superposition,[],[f13468,f169116]) ).
fof(f169220,plain,
( ~ leq(sF3,sF8)
| ~ spl9_189 ),
inference(forward_subsumption_resolution,[],[f169143,f61]) ).
fof(f169237,plain,
( ~ spl9_389
| ~ spl9_189 ),
inference(avatar_split_clause,[],[f169220,f35098,f84969]) ).
fof(f171929,plain,
( ! [X0] : addition(sF8,X0) = addition(sF8,addition(multiplication(sK1,sF8),X0))
| ~ spl9_189 ),
inference(superposition,[],[f92,f163711]) ).
fof(f223222,plain,
addition(sF7,sF3) = addition(multiplication(sF2,sF3),sF7),
inference(superposition,[],[f50933,f58]) ).
fof(f223426,plain,
multiplication(sF7,sF3) = addition(multiplication(sF2,sF3),sF7),
inference(forward_demodulation,[],[f223222,f21603]) ).
fof(f223455,plain,
( sF3 = addition(multiplication(sF2,sF3),sF7)
| ~ spl9_162 ),
inference(forward_demodulation,[],[f223426,f21732]) ).
fof(f223476,plain,
( addition(sF6,sF3) = addition(sF8,multiplication(sF2,sF3))
| ~ spl9_162 ),
inference(superposition,[],[f1766,f223455]) ).
fof(f223670,plain,
( sF3 = addition(sF8,multiplication(sF2,sF3))
| ~ spl9_162 ),
inference(forward_demodulation,[],[f223476,f14981]) ).
fof(f891470,plain,
( ! [X0] : addition(multiplication(X0,sF3),sF3) = addition(sF8,multiplication(addition(sF2,X0),sF3))
| ~ spl9_162 ),
inference(superposition,[],[f1400,f223670]) ).
fof(f892044,plain,
( ! [X0] : multiplication(addition(X0,one),sF3) = addition(sF8,multiplication(addition(sF2,X0),sF3))
| ~ spl9_162 ),
inference(forward_demodulation,[],[f891470,f193]) ).
fof(f987151,plain,
( ! [X0] : addition(sF8,multiplication(sK1,X0)) = addition(multiplication(sK1,addition(sF8,X0)),sF8)
| ~ spl9_189 ),
inference(superposition,[],[f163711,f449]) ).
fof(f1025248,plain,
( addition(sF8,multiplication(addition(sK1,sF5),sF3)) = addition(sF8,addition(multiplication(sK1,addition(sF8,sF3)),sF6))
| ~ spl9_189 ),
inference(superposition,[],[f171929,f532]) ).
fof(f1025678,plain,
( addition(sF8,multiplication(addition(sK1,sF5),sF3)) = addition(multiplication(sK1,addition(sF8,sF3)),sF8)
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025248,f12312]) ).
fof(f1025782,plain,
( addition(sF8,multiplication(sK1,sF3)) = addition(sF8,multiplication(addition(sK1,sF5),sF3))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025678,f987151]) ).
fof(f1025830,plain,
( addition(sF8,multiplication(sK1,sF3)) = addition(sF8,multiplication(addition(sF2,sF5),sF3))
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025782,f3998]) ).
fof(f1025853,plain,
( multiplication(addition(sF5,one),sF3) = addition(sF8,multiplication(sK1,sF3))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025830,f892044]) ).
fof(f1025869,plain,
( addition(sF6,sF3) = addition(sF8,multiplication(sK1,sF3))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025853,f399]) ).
fof(f1025876,plain,
( sF3 = addition(sF8,multiplication(sK1,sF3))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1025869,f14981]) ).
fof(f1025906,plain,
( ~ leq(sF3,sF3)
| leq(sF3,multiplication(strong_iteration(sK1),sF8))
| ~ spl9_162
| ~ spl9_189 ),
inference(superposition,[],[f99,f1025876]) ).
fof(f1026243,plain,
( leq(sF3,multiplication(strong_iteration(sK1),sF8))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_subsumption_resolution,[],[f1025906,f352]) ).
fof(f1026344,plain,
( leq(sF3,multiplication(sF7,sF8))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1026243,f58]) ).
fof(f1026401,plain,
( leq(sF3,multiplication(sF4,sF8))
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1026344,f53220]) ).
fof(f1026438,plain,
( leq(sF3,sF8)
| ~ spl9_162
| ~ spl9_189 ),
inference(forward_demodulation,[],[f1026401,f35099]) ).
fof(f1026460,plain,
( $false
| ~ spl9_162
| ~ spl9_189
| spl9_389 ),
inference(forward_subsumption_resolution,[],[f1026438,f84970]) ).
fof(f1026461,plain,
( ~ spl9_162
| ~ spl9_189
| spl9_389 ),
inference(avatar_contradiction_clause,[],[f1026460]) ).
cnf(s289,plain,
spl9_189,
inference(sat_conversion,[],[f103421]) ).
cnf(s374,plain,
spl9_162,
inference(sat_conversion,[],[f136791]) ).
cnf(s460,plain,
( ~ spl9_189
| ~ spl9_389 ),
inference(sat_conversion,[],[f169237]) ).
cnf(s1249,plain,
( ~ spl9_162
| ~ spl9_189
| spl9_389 ),
inference(sat_conversion,[],[f1026461]) ).
cnf(s1254,plain,
spl9_389,
inference(rat,[],[s1249,s374,s289]) ).
cnf(s1257,plain,
$false,
inference(rat,[],[s460,s1254,s289]) ).
fof(f1026489,plain,
$false,
inference(avatar_sat_refutation,[],[s1257]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE149+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.30 % Computer : n012.cluster.edu
% 0.05/0.30 % Model : x86_64 x86_64
% 0.05/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.30 % Memory : 8046.5625MB
% 0.05/0.30 % OS : Linux 6.8.0-71-generic
% 0.05/0.30 % CPULimit : 300
% 0.05/0.30 % WCLimit : 300
% 0.05/0.30 % DateTime : Sun Sep 27 13:12:04 UTC 2026
% 0.05/0.30 % CPUTime :
% 0.05/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.32 Running first-order theorem proving
% 0.05/0.32 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
% 11.70/2.20 % (2380436)Detected formulas, will run a generic FOF schedule.
% 11.70/2.20 % (2380450)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3681393421:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_3000 on theBenchmark for (3000ds/134677Mi)
% 11.70/2.20 % (2380454)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1103795163:s2a=on:i=139:gtg=position_3000 on theBenchmark for (3000ds/139Mi)
% 11.70/2.20 % (2380455)dis-21_1_sil=8000:lcm=predicate:random_seed=2825649791:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/129Mi)
% 11.70/2.20 % (2380449)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=3942574446:i=141193_3000 on theBenchmark for (3000ds/141193Mi)
% 11.70/2.20 % (2380453)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3321575506:i=119:av=off:ss=axioms_3000 on theBenchmark for (3000ds/119Mi)
% 11.70/2.20 % (2380452)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4029048806:i=109:sd=1:ins=1:gsp=on:ss=axioms_3000 on theBenchmark for (3000ds/109Mi)
% 11.70/2.20 % (2380451)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3943716437:i=141695:sd=1:nm=32:gsp=on:ss=included_3000 on theBenchmark for (3000ds/141695Mi)
% 11.70/2.20 % (2380452)Refutation not found, incomplete strategy
% 11.70/2.20 % (2380452)------------------------------
% 11.70/2.20 % (2380452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.20 % (2380455)Refutation not found, incomplete strategy
% 11.70/2.20 % (2380455)------------------------------
% 11.70/2.20 % (2380455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.20 % (2380452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.20 % (2380455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.20 % (2380452)CaDiCaL version: 2.1.3
% 11.70/2.20 % (2380455)CaDiCaL version: 2.1.3
% 11.70/2.20 % (2380452)Termination reason: Refutation not found, incomplete strategy
% 11.70/2.20 % (2380452)Time elapsed: 0.001 s
% 11.70/2.20 % (2380455)Termination reason: Refutation not found, incomplete strategy
% 11.70/2.20 % (2380455)Time elapsed: 0.001 s
% 11.70/2.20 % (2380452)Peak memory usage: 88 MB
% 11.70/2.20 % (2380455)Peak memory usage: 88 MB
% 11.70/2.20 % (2380452)Instructions burned: 1 (million)
% 11.70/2.20 % (2380455)Instructions burned: 1 (million)
% 11.70/2.20 % (2380454)Instruction limit reached!
% 11.70/2.20 % (2380454)------------------------------
% 11.70/2.20 % (2380454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.20 % (2380454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.20 % (2380454)CaDiCaL version: 2.1.3
% 11.70/2.20 % (2380454)Termination reason: Instruction limit
% 11.70/2.20 % (2380454)Termination phase: Saturation
% 11.70/2.20 % (2380454)Time elapsed: 0.045 s
% 11.70/2.20 % (2380454)Peak memory usage: 89 MB
% 11.70/2.20 % (2380454)Instructions burned: 139 (million)
% 11.70/2.20 % (2380453)Instruction limit reached!
% 11.70/2.20 % (2380453)------------------------------
% 11.70/2.20 % (2380453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.20 % (2380453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.70/2.20 % (2380453)CaDiCaL version: 2.1.3
% 11.70/2.20 % (2380453)Termination reason: Instruction limit
% 11.70/2.20 % (2380453)Termination phase: Saturation
% 11.70/2.20 % (2380453)Time elapsed: 0.063 s
% 11.70/2.20 % (2380453)Peak memory usage: 89 MB
% 11.70/2.20 % (2380453)Instructions burned: 119 (million)
% 11.70/2.20 % (2380475)lrs+10_1_sil=32000:urr=on:br=off:random_seed=162134115:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 11.70/2.20 % (2380473)lrs+10_1_sil=8000:sp=occurrence:random_seed=1547303179:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 11.70/2.20 % (2380455)------------------------------
% 11.70/2.20 % (2380455)------------------------------
% 11.70/2.20 % (2380452)------------------------------
% 11.70/2.20 % (2380452)------------------------------
% 11.70/2.20 % (2380475)Instruction limit reached!
% 11.70/2.20 % (2380475)------------------------------
% 11.70/2.20 % (2380475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.70/2.20 % (2380475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380475)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380475)Termination reason: Instruction limit
% 14.49/2.71 % (2380475)Termination phase: Saturation
% 14.49/2.71 % (2380475)Time elapsed: 0.066 s
% 14.49/2.71 % (2380475)Peak memory usage: 89 MB
% 14.49/2.71 % (2380475)Instructions burned: 160 (million)
% 14.49/2.71 % (2380473)Instruction limit reached!
% 14.49/2.71 % (2380473)------------------------------
% 14.49/2.71 % (2380473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380473)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380473)Termination reason: Instruction limit
% 14.49/2.71 % (2380473)Termination phase: Saturation
% 14.49/2.71 % (2380473)Time elapsed: 0.164 s
% 14.49/2.71 % (2380473)Peak memory usage: 91 MB
% 14.49/2.71 % (2380473)Instructions burned: 287 (million)
% 14.49/2.71 % (2380481)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2734473990:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 14.49/2.71 % (2380480)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3222520227:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 14.49/2.71 % (2380482)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=322855562:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 14.49/2.71 % (2380482)Refutation not found, incomplete strategy
% 14.49/2.71 % (2380482)------------------------------
% 14.49/2.71 % (2380482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380482)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380482)Termination reason: Refutation not found, incomplete strategy
% 14.49/2.71 % (2380482)Time elapsed: 0.001 s
% 14.49/2.71 % (2380482)Peak memory usage: 88 MB
% 14.49/2.71 % (2380482)Instructions burned: 2 (million)
% 14.49/2.71 % (2380481)Instruction limit reached!
% 14.49/2.71 % (2380481)------------------------------
% 14.49/2.71 % (2380481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380481)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380481)Termination reason: Instruction limit
% 14.49/2.71 % (2380481)Termination phase: Saturation
% 14.49/2.71 % (2380481)Time elapsed: 0.117 s
% 14.49/2.71 % (2380481)Peak memory usage: 92 MB
% 14.49/2.71 % (2380481)Instructions burned: 249 (million)
% 14.49/2.71 % (2380451)Refutation not found, incomplete strategy
% 14.49/2.71 % (2380451)------------------------------
% 14.49/2.71 % (2380451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380451)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380451)Termination reason: Refutation not found, incomplete strategy
% 14.49/2.71 % (2380451)Time elapsed: 0.503 s
% 14.49/2.71 % (2380451)Peak memory usage: 127 MB
% 14.49/2.71 % (2380451)Instructions burned: 890 (million)
% 14.49/2.71 % (2380480)Instruction limit reached!
% 14.49/2.71 % (2380480)------------------------------
% 14.49/2.71 % (2380480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380480)CaDiCaL version: 2.1.3
% 14.49/2.71 % (2380480)Termination reason: Instruction limit
% 14.49/2.71 % (2380480)Termination phase: Saturation
% 14.49/2.71 % (2380480)Time elapsed: 0.175 s
% 14.49/2.71 % (2380480)Peak memory usage: 92 MB
% 14.49/2.71 % (2380480)Instructions burned: 327 (million)
% 14.49/2.71 % (2380484)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2816534522:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 14.49/2.71 % (2380482)------------------------------
% 14.49/2.71 % (2380482)------------------------------
% 14.49/2.71 % (2380490)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1071083377:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 14.49/2.71 % (2380490)Refutation not found, incomplete strategy
% 14.49/2.71 % (2380490)------------------------------
% 14.49/2.71 % (2380490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.49/2.71 % (2380490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.49/2.71 % (2380490)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380490)Termination reason: Refutation not found, incomplete strategy
% 22.85/3.80 % (2380490)Time elapsed: 0.006 s
% 22.85/3.80 % (2380490)Peak memory usage: 88 MB
% 22.85/3.80 % (2380490)Instructions burned: 7 (million)
% 22.85/3.80 % (2380451)------------------------------
% 22.85/3.80 % (2380451)------------------------------
% 22.85/3.80 % (2380492)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1095490598:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 22.85/3.80 % (2380492)Refutation not found, incomplete strategy
% 22.85/3.80 % (2380492)------------------------------
% 22.85/3.80 % (2380492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/3.80 % (2380492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/3.80 % (2380492)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380492)Termination reason: Refutation not found, incomplete strategy
% 22.85/3.80 % (2380492)Time elapsed: 0.001 s
% 22.85/3.80 % (2380492)Peak memory usage: 88 MB
% 22.85/3.80 % (2380495)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4255539990:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 22.85/3.80 % (2380495)Refutation not found, incomplete strategy
% 22.85/3.80 % (2380495)------------------------------
% 22.85/3.80 % (2380495)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/3.80 % (2380495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/3.80 % (2380495)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380495)Termination reason: Refutation not found, incomplete strategy
% 22.85/3.80 % (2380495)Time elapsed: 0.001 s
% 22.85/3.80 % (2380495)Peak memory usage: 89 MB
% 22.85/3.80 % (2380495)Instructions burned: 1 (million)
% 22.85/3.80 % (2380490)------------------------------
% 22.85/3.80 % (2380490)------------------------------
% 22.85/3.80 % (2380497)lrs+10_1_sil=8000:sp=occurrence:random_seed=1260612305:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 22.85/3.80 % (2380492)------------------------------
% 22.85/3.80 % (2380492)------------------------------
% 22.85/3.80 % (2380495)------------------------------
% 22.85/3.80 % (2380495)------------------------------
% 22.85/3.80 % (2380501)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2393733972:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 22.85/3.80 % (2380501)Refutation not found, incomplete strategy
% 22.85/3.80 % (2380501)------------------------------
% 22.85/3.80 % (2380501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/3.80 % (2380501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/3.80 % (2380501)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380501)Termination reason: Refutation not found, incomplete strategy
% 22.85/3.80 % (2380501)Time elapsed: 0.001 s
% 22.85/3.80 % (2380501)Peak memory usage: 88 MB
% 22.85/3.80 % (2380504)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1633095092:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 22.85/3.80 % (2380503)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3960416177:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 22.85/3.80 % (2380504)Refutation not found, incomplete strategy
% 22.85/3.80 % (2380504)------------------------------
% 22.85/3.80 % (2380504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/3.80 % (2380504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/3.80 % (2380504)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380504)Termination reason: Refutation not found, incomplete strategy
% 22.85/3.80 % (2380504)Time elapsed: 0.002 s
% 22.85/3.80 % (2380504)Peak memory usage: 88 MB
% 22.85/3.80 % (2380504)Instructions burned: 1 (million)
% 22.85/3.80 % (2380501)------------------------------
% 22.85/3.80 % (2380501)------------------------------
% 22.85/3.80 % (2380504)------------------------------
% 22.85/3.80 % (2380504)------------------------------
% 22.85/3.80 % (2380497)Instruction limit reached!
% 22.85/3.80 % (2380497)------------------------------
% 22.85/3.80 % (2380497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.85/3.80 % (2380497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.85/3.80 % (2380497)CaDiCaL version: 2.1.3
% 22.85/3.80 % (2380497)Termination reason: Instruction limit
% 22.85/3.80 % (2380497)Termination phase: Saturation
% 22.85/3.80 % (2380497)Time elapsed: 0.485 s
% 39.88/6.25 % (2380497)Peak memory usage: 96 MB
% 39.88/6.25 % (2380497)Instructions burned: 907 (million)
% 39.88/6.25 % (2380510)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3662337090:st=8:i=592:sd=3:ep=RST:ss=axioms_2984 on theBenchmark for (2984ds/592Mi)
% 39.88/6.25 % (2380511)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=573924985:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 39.88/6.25 % (2380512)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=355837620:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 39.88/6.25 % (2380512)Instruction limit reached!
% 39.88/6.25 % (2380512)------------------------------
% 39.88/6.25 % (2380512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380512)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380512)Termination reason: Instruction limit
% 39.88/6.25 % (2380512)Termination phase: Saturation
% 39.88/6.25 % (2380512)Time elapsed: 0.070 s
% 39.88/6.25 % (2380512)Peak memory usage: 90 MB
% 39.88/6.25 % (2380512)Instructions burned: 126 (million)
% 39.88/6.25 % (2380484)Instruction limit reached!
% 39.88/6.25 % (2380484)------------------------------
% 39.88/6.25 % (2380484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380484)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380484)Termination reason: Instruction limit
% 39.88/6.25 % (2380484)Termination phase: Saturation
% 39.88/6.25 % (2380484)Time elapsed: 1.217 s
% 39.88/6.25 % (2380484)Peak memory usage: 144 MB
% 39.88/6.25 % (2380484)Instructions burned: 2350 (million)
% 39.88/6.25 % (2380510)Instruction limit reached!
% 39.88/6.25 % (2380510)------------------------------
% 39.88/6.25 % (2380510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380510)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380510)Termination reason: Instruction limit
% 39.88/6.25 % (2380510)Termination phase: Saturation
% 39.88/6.25 % (2380510)Time elapsed: 0.232 s
% 39.88/6.25 % (2380510)Peak memory usage: 98 MB
% 39.88/6.25 % (2380510)Instructions burned: 594 (million)
% 39.88/6.25 % (2380516)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3896041446:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 39.88/6.25 % (2380516)Instruction limit reached!
% 39.88/6.25 % (2380516)------------------------------
% 39.88/6.25 % (2380516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380516)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380516)Termination reason: Instruction limit
% 39.88/6.25 % (2380516)Termination phase: Saturation
% 39.88/6.25 % (2380516)Time elapsed: 0.047 s
% 39.88/6.25 % (2380516)Peak memory usage: 90 MB
% 39.88/6.25 % (2380516)Instructions burned: 136 (million)
% 39.88/6.25 % (2380517)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=387646261:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 39.88/6.25 % (2380517)Refutation not found, incomplete strategy
% 39.88/6.25 % (2380517)------------------------------
% 39.88/6.25 % (2380517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380517)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380517)Termination reason: Refutation not found, incomplete strategy
% 39.88/6.25 % (2380517)Time elapsed: 0.0000 s
% 39.88/6.25 % (2380517)Peak memory usage: 88 MB
% 39.88/6.25 % (2380519)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2870686207:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2979 on theBenchmark for (2979ds/431Mi)
% 39.88/6.25 % (2380519)Refutation not found, incomplete strategy
% 39.88/6.25 % (2380519)------------------------------
% 39.88/6.25 % (2380519)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.88/6.25 % (2380519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.88/6.25 % (2380519)CaDiCaL version: 2.1.3
% 39.88/6.25 % (2380519)Termination reason: Refutation not found, incomplete strategy
% 50.01/7.86 % (2380519)Time elapsed: 0.001 s
% 50.01/7.86 % (2380519)Peak memory usage: 88 MB
% 50.01/7.86 % (2380519)Instructions burned: 1 (million)
% 50.01/7.86 % (2380522)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=4178058705:i=6060:aac=none:ins=25_2978 on theBenchmark for (2978ds/6060Mi)
% 50.01/7.86 % (2380517)------------------------------
% 50.01/7.86 % (2380517)------------------------------
% 50.01/7.86 % (2380519)------------------------------
% 50.01/7.86 % (2380519)------------------------------
% 50.01/7.86 % (2380570)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2101518715:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2977 on theBenchmark for (2977ds/150Mi)
% 50.01/7.86 % (2380593)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2260555552:i=14155:bd=all_2976 on theBenchmark for (2976ds/14155Mi)
% 50.01/7.86 % (2380570)Instruction limit reached!
% 50.01/7.86 % (2380570)------------------------------
% 50.01/7.86 % (2380570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.01/7.86 % (2380570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.86 % (2380570)CaDiCaL version: 2.1.3
% 50.01/7.86 % (2380570)Termination reason: Instruction limit
% 50.01/7.86 % (2380570)Termination phase: Saturation
% 50.01/7.86 % (2380570)Time elapsed: 0.056 s
% 50.01/7.86 % (2380570)Peak memory usage: 91 MB
% 50.01/7.86 % (2380570)Instructions burned: 156 (million)
% 50.01/7.86 % (2380634)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=472991193:i=667:av=off:fsr=off_2975 on theBenchmark for (2975ds/667Mi)
% 50.01/7.86 % (2380634)Refutation not found, incomplete strategy
% 50.01/7.86 % (2380634)------------------------------
% 50.01/7.86 % (2380634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.01/7.86 % (2380634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.86 % (2380634)CaDiCaL version: 2.1.3
% 50.01/7.86 % (2380634)Termination reason: Refutation not found, incomplete strategy
% 50.01/7.86 % (2380634)Time elapsed: 0.001 s
% 50.01/7.86 % (2380634)Peak memory usage: 88 MB
% 50.01/7.86 % (2380634)Instructions burned: 1 (million)
% 50.01/7.86 % (2380634)------------------------------
% 50.01/7.86 % (2380634)------------------------------
% 50.01/7.86 % (2380641)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=134093431:s2a=on:i=185:s2at=1.8:fdi=4_2972 on theBenchmark for (2972ds/185Mi)
% 50.01/7.86 % (2380641)Instruction limit reached!
% 50.01/7.86 % (2380641)------------------------------
% 50.01/7.86 % (2380641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.01/7.86 % (2380641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.86 % (2380641)CaDiCaL version: 2.1.3
% 50.01/7.86 % (2380641)Termination reason: Instruction limit
% 50.01/7.86 % (2380641)Termination phase: Saturation
% 50.01/7.86 % (2380641)Time elapsed: 0.062 s
% 50.01/7.86 % (2380641)Peak memory usage: 90 MB
% 50.01/7.86 % (2380641)Instructions burned: 186 (million)
% 50.01/7.86 % (2380656)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1252678228:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2970 on theBenchmark for (2970ds/193Mi)
% 50.01/7.86 % (2380656)Instruction limit reached!
% 50.01/7.86 % (2380656)------------------------------
% 50.01/7.86 % (2380656)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.01/7.86 % (2380656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.86 % (2380656)CaDiCaL version: 2.1.3
% 50.01/7.86 % (2380656)Termination reason: Instruction limit
% 50.01/7.86 % (2380656)Termination phase: Saturation
% 50.01/7.86 % (2380656)Time elapsed: 0.069 s
% 50.01/7.86 % (2380656)Peak memory usage: 92 MB
% 50.01/7.86 % (2380656)Instructions burned: 196 (million)
% 50.01/7.86 % (2380503)Instruction limit reached!
% 50.01/7.86 % (2380503)------------------------------
% 50.01/7.86 % (2380503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.01/7.86 % (2380503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.01/7.86 % (2380503)CaDiCaL version: 2.1.3
% 50.01/7.86 % (2380503)Termination reason: Instruction limit
% 50.01/7.86 % (2380503)Termination phase: Saturation
% 68.05/10.22 % (2380503)Time elapsed: 1.866 s
% 68.05/10.22 % (2380503)Peak memory usage: 170 MB
% 68.05/10.22 % (2380503)Instructions burned: 5204 (million)
% 68.05/10.22 % (2380687)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3140864470:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2968 on theBenchmark for (2968ds/4850Mi)
% 68.05/10.22 % (2380687)Refutation not found, incomplete strategy
% 68.05/10.22 % (2380687)------------------------------
% 68.05/10.22 % (2380687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.05/10.22 % (2380687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.05/10.22 % (2380687)CaDiCaL version: 2.1.3
% 68.05/10.22 % (2380687)Termination reason: Refutation not found, incomplete strategy
% 68.05/10.22 % (2380687)Time elapsed: 0.0000 s
% 68.05/10.22 % (2380687)Peak memory usage: 88 MB
% 68.05/10.22 % (2380689)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1545787682:i=12111:sd=1:ss=included_2967 on theBenchmark for (2967ds/12111Mi)
% 68.05/10.22 % (2380687)------------------------------
% 68.05/10.22 % (2380687)------------------------------
% 68.05/10.22 % (2380691)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=606355894:i=319:kws=precedence:fsr=off_2965 on theBenchmark for (2965ds/319Mi)
% 68.05/10.22 % (2380691)Instruction limit reached!
% 68.05/10.22 % (2380691)------------------------------
% 68.05/10.22 % (2380691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.05/10.22 % (2380691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.05/10.22 % (2380691)CaDiCaL version: 2.1.3
% 68.05/10.22 % (2380691)Termination reason: Instruction limit
% 68.05/10.22 % (2380691)Termination phase: Saturation
% 68.05/10.22 % (2380691)Time elapsed: 0.104 s
% 68.05/10.22 % (2380691)Peak memory usage: 93 MB
% 68.05/10.22 % (2380691)Instructions burned: 322 (million)
% 68.05/10.22 % (2380693)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3339716844:i=2064:ep=RST_2963 on theBenchmark for (2963ds/2064Mi)
% 68.05/10.22 % (2380522)Instruction limit reached!
% 68.05/10.22 % (2380522)------------------------------
% 68.05/10.22 % (2380522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.05/10.22 % (2380522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.05/10.22 % (2380522)CaDiCaL version: 2.1.3
% 68.05/10.22 % (2380522)Termination reason: Instruction limit
% 68.05/10.22 % (2380522)Termination phase: Saturation
% 68.05/10.22 % (2380522)Time elapsed: 2.135 s
% 68.05/10.22 % (2380522)Peak memory usage: 184 MB
% 68.05/10.22 % (2380522)Instructions burned: 6061 (million)
% 68.05/10.22 % (2380693)Instruction limit reached!
% 68.05/10.22 % (2380693)------------------------------
% 68.05/10.22 % (2380693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.05/10.22 % (2380693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.05/10.22 % (2380693)CaDiCaL version: 2.1.3
% 68.05/10.22 % (2380693)Termination reason: Instruction limit
% 68.05/10.22 % (2380693)Termination phase: Saturation
% 68.05/10.22 % (2380693)Time elapsed: 0.727 s
% 68.05/10.22 % (2380693)Peak memory usage: 115 MB
% 68.05/10.22 % (2380693)Instructions burned: 2066 (million)
% 68.05/10.22 % (2380695)dis-1011_128_sil=32000:random_seed=1475483907:i=3706:ep=RST:av=off_2955 on theBenchmark for (2955ds/3706Mi)
% 68.05/10.22 % (2380696)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4055262030:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2954 on theBenchmark for (2954ds/757Mi)
% 68.05/10.22 % (2380696)Refutation not found, incomplete strategy
% 68.05/10.22 % (2380696)------------------------------
% 68.05/10.22 % (2380696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.05/10.22 % (2380696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.05/10.22 % (2380696)CaDiCaL version: 2.1.3
% 68.05/10.22 % (2380696)Termination reason: Refutation not found, incomplete strategy
% 68.05/10.22 % (2380696)Time elapsed: 0.001 s
% 68.05/10.22 % (2380696)Peak memory usage: 89 MB
% 68.05/10.22 % (2380696)Instructions burned: 1 (million)
% 68.05/10.22 % (2380696)------------------------------
% 68.05/10.22 % (2380696)------------------------------
% 68.05/10.22 % (2380699)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1418562215:i=13913:ss=axioms:sgt=8_2952 on theBenchmark for (2952ds/13913Mi)
% 68.05/10.22 % (2380695)Instruction limit reached!
% 68.05/10.22 % (2380695)------------------------------
% 72.30/11.01 % (2380695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380695)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380695)Termination reason: Instruction limit
% 72.30/11.01 % (2380695)Termination phase: Saturation
% 72.30/11.01 % (2380695)Time elapsed: 1.183 s
% 72.30/11.01 % (2380695)Peak memory usage: 115 MB
% 72.30/11.01 % (2380695)Instructions burned: 3706 (million)
% 72.30/11.01 % (2380701)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2981042178:i=9925:aac=none_2942 on theBenchmark for (2942ds/9925Mi)
% 72.30/11.01 % (2380701)Refutation not found, incomplete strategy
% 72.30/11.01 % (2380701)------------------------------
% 72.30/11.01 % (2380701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380701)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380701)Termination reason: Refutation not found, incomplete strategy
% 72.30/11.01 % (2380701)Time elapsed: 0.336 s
% 72.30/11.01 % (2380701)Peak memory usage: 128 MB
% 72.30/11.01 % (2380701)Instructions burned: 902 (million)
% 72.30/11.01 % (2380701)------------------------------
% 72.30/11.01 % (2380701)------------------------------
% 72.30/11.01 % (2380511)Instruction limit reached!
% 72.30/11.01 % (2380511)------------------------------
% 72.30/11.01 % (2380511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380511)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380511)Termination reason: Instruction limit
% 72.30/11.01 % (2380511)Termination phase: Saturation
% 72.30/11.01 % (2380511)Time elapsed: 4.563 s
% 72.30/11.01 % (2380511)Peak memory usage: 242 MB
% 72.30/11.01 % (2380511)Instructions burned: 13194 (million)
% 72.30/11.01 % (2380703)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=1618738856:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2936 on theBenchmark for (2936ds/2479Mi)
% 72.30/11.01 % (2380703)Refutation not found, incomplete strategy
% 72.30/11.01 % (2380703)------------------------------
% 72.30/11.01 % (2380703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380703)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380703)Termination reason: Refutation not found, incomplete strategy
% 72.30/11.01 % (2380703)Time elapsed: 0.001 s
% 72.30/11.01 % (2380703)Peak memory usage: 89 MB
% 72.30/11.01 % (2380703)Instructions burned: 2 (million)
% 72.30/11.01 % (2380704)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1138739094:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2935 on theBenchmark for (2935ds/440Mi)
% 72.30/11.01 % (2380703)------------------------------
% 72.30/11.01 % (2380703)------------------------------
% 72.30/11.01 % (2380704)Instruction limit reached!
% 72.30/11.01 % (2380704)------------------------------
% 72.30/11.01 % (2380704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380704)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380704)Termination reason: Instruction limit
% 72.30/11.01 % (2380704)Termination phase: Saturation
% 72.30/11.01 % (2380704)Time elapsed: 0.131 s
% 72.30/11.01 % (2380704)Peak memory usage: 94 MB
% 72.30/11.01 % (2380704)Instructions burned: 443 (million)
% 72.30/11.01 % (2380707)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=2049629153:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2933 on theBenchmark for (2933ds/11145Mi)
% 72.30/11.01 % (2380708)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=972626110:cts=off:i=3034:av=off:er=known:fsd=on_2933 on theBenchmark for (2933ds/3034Mi)
% 72.30/11.01 % (2380689)Instruction limit reached!
% 72.30/11.01 % (2380689)------------------------------
% 72.30/11.01 % (2380689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.01 % (2380689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.01 % (2380689)CaDiCaL version: 2.1.3
% 72.30/11.01 % (2380689)Termination reason: Instruction limit
% 72.30/11.01 % (2380689)Termination phase: Saturation
% 72.30/11.01 % (2380689)Time elapsed: 3.927 s
% 79.09/11.92 % (2380689)Peak memory usage: 244 MB
% 79.09/11.92 % (2380689)Instructions burned: 12114 (million)
% 79.09/11.92 % (2380711)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=372522597:st=2:s2a=on:i=524:s2at=2:ss=axioms_2926 on theBenchmark for (2926ds/524Mi)
% 79.09/11.92 % (2380593)Instruction limit reached!
% 79.09/11.92 % (2380593)------------------------------
% 79.09/11.92 % (2380593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.09/11.92 % (2380593)CaDiCaL version: 2.1.3
% 79.09/11.92 % (2380593)Termination reason: Instruction limit
% 79.09/11.92 % (2380593)Termination phase: Saturation
% 79.09/11.92 % (2380593)Time elapsed: 5.087 s
% 79.09/11.92 % (2380593)Peak memory usage: 239 MB
% 79.09/11.92 % (2380593)Instructions burned: 14155 (million)
% 79.09/11.92 % (2380711)Instruction limit reached!
% 79.09/11.92 % (2380711)------------------------------
% 79.09/11.92 % (2380711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.09/11.92 % (2380711)CaDiCaL version: 2.1.3
% 79.09/11.92 % (2380711)Termination reason: Instruction limit
% 79.09/11.92 % (2380711)Termination phase: Saturation
% 79.09/11.92 % (2380711)Time elapsed: 0.156 s
% 79.09/11.92 % (2380711)Peak memory usage: 92 MB
% 79.09/11.92 % (2380711)Instructions burned: 527 (million)
% 79.09/11.92 % (2380713)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3269988206:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2924 on theBenchmark for (2924ds/1016Mi)
% 79.09/11.92 % (2380714)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3911342565:i=14123:bd=preordered:ins=4_2923 on theBenchmark for (2923ds/14123Mi)
% 79.09/11.92 % (2380708)Instruction limit reached!
% 79.09/11.92 % (2380708)------------------------------
% 79.09/11.92 % (2380708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.09/11.92 % (2380708)CaDiCaL version: 2.1.3
% 79.09/11.92 % (2380708)Termination reason: Instruction limit
% 79.09/11.92 % (2380708)Termination phase: Saturation
% 79.09/11.92 % (2380708)Time elapsed: 1.025 s
% 79.09/11.92 % (2380708)Peak memory usage: 142 MB
% 79.09/11.92 % (2380708)Instructions burned: 3035 (million)
% 79.09/11.92 % (2380713)Instruction limit reached!
% 79.09/11.92 % (2380713)------------------------------
% 79.09/11.92 % (2380713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.09/11.92 % (2380713)CaDiCaL version: 2.1.3
% 79.09/11.92 % (2380713)Termination reason: Instruction limit
% 79.09/11.92 % (2380713)Termination phase: Saturation
% 79.09/11.92 % (2380713)Time elapsed: 0.299 s
% 79.09/11.92 % (2380713)Peak memory usage: 96 MB
% 79.09/11.92 % (2380713)Instructions burned: 1018 (million)
% 79.09/11.92 % (2380717)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=928963837:i=5781:kws=precedence:bd=all:rawr=on_2921 on theBenchmark for (2921ds/5781Mi)
% 79.09/11.92 % (2380718)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=382183396:i=2448:gtgl=5:bd=preordered:gtg=all_2920 on theBenchmark for (2920ds/2448Mi)
% 79.09/11.92 % (2380718)Instruction limit reached!
% 79.09/11.92 % (2380718)------------------------------
% 79.09/11.92 % (2380718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.09/11.92 % (2380718)CaDiCaL version: 2.1.3
% 79.09/11.92 % (2380718)Termination reason: Instruction limit
% 79.09/11.92 % (2380718)Termination phase: Saturation
% 79.09/11.92 % (2380718)Time elapsed: 0.857 s
% 79.09/11.92 % (2380718)Peak memory usage: 143 MB
% 79.09/11.92 % (2380718)Instructions burned: 2450 (million)
% 79.09/11.92 % (2380721)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3572618587:i=3223:kws=precedence:fgj=on:av=off_2910 on theBenchmark for (2910ds/3223Mi)
% 79.09/11.92 % (2380699)Instruction limit reached!
% 79.09/11.92 % (2380699)------------------------------
% 79.09/11.92 % (2380699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.09/11.92 % (2380699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380699)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380699)Termination reason: Instruction limit
% 100.40/14.86 % (2380699)Termination phase: Saturation
% 100.40/14.86 % (2380699)Time elapsed: 4.744 s
% 100.40/14.86 % (2380699)Peak memory usage: 250 MB
% 100.40/14.86 % (2380699)Instructions burned: 13915 (million)
% 100.40/14.86 % (2380723)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2548271679:st=5.6:i=2033:sd=3:ss=axioms_2903 on theBenchmark for (2903ds/2033Mi)
% 100.40/14.86 % (2380717)Instruction limit reached!
% 100.40/14.86 % (2380717)------------------------------
% 100.40/14.86 % (2380717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.40/14.86 % (2380717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380717)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380717)Termination reason: Instruction limit
% 100.40/14.86 % (2380717)Termination phase: Saturation
% 100.40/14.86 % (2380717)Time elapsed: 1.873 s
% 100.40/14.86 % (2380717)Peak memory usage: 133 MB
% 100.40/14.86 % (2380717)Instructions burned: 5782 (million)
% 100.40/14.86 % (2380725)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=389492641:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2901 on theBenchmark for (2901ds/2055Mi)
% 100.40/14.86 % (2380721)Instruction limit reached!
% 100.40/14.86 % (2380721)------------------------------
% 100.40/14.86 % (2380721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.40/14.86 % (2380721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380721)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380721)Termination reason: Instruction limit
% 100.40/14.86 % (2380721)Termination phase: Saturation
% 100.40/14.86 % (2380721)Time elapsed: 1.064 s
% 100.40/14.86 % (2380721)Peak memory usage: 153 MB
% 100.40/14.86 % (2380721)Instructions burned: 3223 (million)
% 100.40/14.86 % (2380723)Refutation not found, incomplete strategy
% 100.40/14.86 % (2380723)------------------------------
% 100.40/14.86 % (2380723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.40/14.86 % (2380723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380723)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380723)Termination reason: Refutation not found, incomplete strategy
% 100.40/14.86 % (2380723)Time elapsed: 0.332 s
% 100.40/14.86 % (2380723)Peak memory usage: 128 MB
% 100.40/14.86 % (2380723)Instructions burned: 898 (million)
% 100.40/14.86 % (2380707)Instruction limit reached!
% 100.40/14.86 % (2380707)------------------------------
% 100.40/14.86 % (2380707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.40/14.86 % (2380707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380707)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380707)Termination reason: Instruction limit
% 100.40/14.86 % (2380707)Termination phase: Saturation
% 100.40/14.86 % (2380707)Time elapsed: 3.497 s
% 100.40/14.86 % (2380707)Peak memory usage: 225 MB
% 100.40/14.86 % (2380707)Instructions burned: 11145 (million)
% 100.40/14.86 % (2380727)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=302937659:i=21611:sd=3:ss=axioms_2898 on theBenchmark for (2898ds/21611Mi)
% 100.40/14.86 % (2380723)------------------------------
% 100.40/14.86 % (2380723)------------------------------
% 100.40/14.86 % (2380728)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=2930885904:i=4835:sd=13:ss=axioms:sgt=23_2897 on theBenchmark for (2897ds/4835Mi)
% 100.40/14.86 % (2380728)Refutation not found, incomplete strategy
% 100.40/14.86 % (2380728)------------------------------
% 100.40/14.86 % (2380728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 100.40/14.86 % (2380728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.86 % (2380728)CaDiCaL version: 2.1.3
% 100.40/14.86 % (2380728)Termination reason: Refutation not found, incomplete strategy
% 100.40/14.86 % (2380728)Time elapsed: 0.001 s
% 100.40/14.86 % (2380728)Peak memory usage: 88 MB
% 100.40/14.86 % (2380728)Instructions burned: 2 (million)
% 100.40/14.86 % (2380730)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=2788775165:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2896 on theBenchmark for (2896ds/797Mi)
% 100.40/14.86 % (2380730)Refutation not found, incomplete strategy
% 100.40/14.86 % (2380730)------------------------------
% 100.40/14.86 % (2380730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.14/20.88 % (2380730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.14/20.88 % (2380730)CaDiCaL version: 2.1.3
% 142.14/20.88 % (2380730)Termination reason: Refutation not found, incomplete strategy
% 142.14/20.88 % (2380730)Time elapsed: 0.001 s
% 142.14/20.88 % (2380730)Peak memory usage: 88 MB
% 142.14/20.88 % (2380730)Instructions burned: 1 (million)
% 142.14/20.88 % (2380728)------------------------------
% 142.14/20.88 % (2380728)------------------------------
% 142.14/20.88 % (2380730)------------------------------
% 142.14/20.88 % (2380730)------------------------------
% 142.14/20.88 % (2380733)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=568332036:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2894 on theBenchmark for (2894ds/2326Mi)
% 142.14/20.88 % (2380733)Refutation not found, incomplete strategy
% 142.14/20.88 % (2380733)------------------------------
% 142.14/20.88 % (2380733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.14/20.88 % (2380733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.14/20.88 % (2380733)CaDiCaL version: 2.1.3
% 142.14/20.88 % (2380733)Termination reason: Refutation not found, incomplete strategy
% 142.14/20.88 % (2380733)Time elapsed: 0.001 s
% 142.14/20.88 % (2380733)Peak memory usage: 89 MB
% 142.14/20.88 % (2380733)Instructions burned: 2 (million)
% 142.14/20.88 % (2380725)Instruction limit reached!
% 142.14/20.88 % (2380725)------------------------------
% 142.14/20.88 % (2380725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.14/20.88 % (2380725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.14/20.88 % (2380725)CaDiCaL version: 2.1.3
% 142.14/20.88 % (2380725)Termination reason: Instruction limit
% 142.14/20.88 % (2380725)Termination phase: Saturation
% 142.14/20.88 % (2380725)Time elapsed: 0.706 s
% 142.14/20.88 % (2380725)Peak memory usage: 137 MB
% 142.14/20.88 % (2380725)Instructions burned: 2057 (million)
% 142.14/20.88 % (2380734)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1727342105:i=6038:nm=6_2893 on theBenchmark for (2893ds/6038Mi)
% 142.14/20.88 % (2380733)------------------------------
% 142.14/20.88 % (2380733)------------------------------
% 142.14/20.88 % (2380736)lrs+10_1_sil=32000:sp=occurrence:random_seed=2207519073:st=2:i=33334:sd=3:ss=included:sgt=32_2892 on theBenchmark for (2892ds/33334Mi)
% 142.14/20.88 % (2380738)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1133031054:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2891 on theBenchmark for (2891ds/1008Mi)
% 142.14/20.88 % (2380738)Refutation not found, incomplete strategy
% 142.14/20.88 % (2380738)------------------------------
% 142.14/20.88 % (2380738)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.14/20.88 % (2380738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.14/20.88 % (2380738)CaDiCaL version: 2.1.3
% 142.14/20.88 % (2380738)Termination reason: Refutation not found, incomplete strategy
% 142.14/20.88 % (2380738)Time elapsed: 0.003 s
% 142.14/20.88 % (2380738)Peak memory usage: 88 MB
% 142.14/20.88 % (2380738)Instructions burned: 6 (million)
% 142.14/20.88 % (2380734)Refutation not found, incomplete strategy
% 142.14/20.88 % (2380734)------------------------------
% 142.14/20.88 % (2380734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.14/20.88 % (2380734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.14/20.88 % (2380734)CaDiCaL version: 2.1.3
% 142.14/20.88 % (2380734)Termination reason: Refutation not found, incomplete strategy
% 142.14/20.88 % (2380734)Time elapsed: 0.330 s
% 142.14/20.88 % (2380734)Peak memory usage: 128 MB
% 142.14/20.88 % (2380734)Instructions burned: 868 (million)
% 142.14/20.88 % (2380738)------------------------------
% 142.14/20.88 % (2380738)------------------------------
% 142.14/20.88 % (2380734)------------------------------
% 142.14/20.88 % (2380734)------------------------------
% 142.14/20.88 % (2380741)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2134084774:i=8327:s2at=5:bd=preordered_2888 on theBenchmark for (2888ds/8327Mi)
% 142.14/20.88 % (2380742)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=3440279745:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2887 on theBenchmark for (2887ds/1083Mi)
% 180.85/26.22 % (2380742)Instruction limit reached!
% 180.85/26.22 % (2380742)------------------------------
% 180.85/26.22 % (2380742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380742)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380742)Termination reason: Instruction limit
% 180.85/26.22 % (2380742)Termination phase: Saturation
% 180.85/26.22 % (2380742)Time elapsed: 0.267 s
% 180.85/26.22 % (2380742)Peak memory usage: 97 MB
% 180.85/26.22 % (2380742)Instructions burned: 1088 (million)
% 180.85/26.22 % (2380745)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=1857262086:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2883 on theBenchmark for (2883ds/1084Mi)
% 180.85/26.22 % (2380745)Instruction limit reached!
% 180.85/26.22 % (2380745)------------------------------
% 180.85/26.22 % (2380745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380745)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380745)Termination reason: Instruction limit
% 180.85/26.22 % (2380745)Termination phase: Saturation
% 180.85/26.22 % (2380745)Time elapsed: 0.358 s
% 180.85/26.22 % (2380745)Peak memory usage: 97 MB
% 180.85/26.22 % (2380745)Instructions burned: 1084 (million)
% 180.85/26.22 % (2380747)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=1870346877:i=6995:s2at=5:gtg=all_2878 on theBenchmark for (2878ds/6995Mi)
% 180.85/26.22 % (2380714)Instruction limit reached!
% 180.85/26.22 % (2380714)------------------------------
% 180.85/26.22 % (2380714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380714)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380714)Termination reason: Instruction limit
% 180.85/26.22 % (2380714)Termination phase: Saturation
% 180.85/26.22 % (2380714)Time elapsed: 5.018 s
% 180.85/26.22 % (2380714)Peak memory usage: 241 MB
% 180.85/26.22 % (2380714)Instructions burned: 14125 (million)
% 180.85/26.22 % (2380749)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=401207464:st=2:i=6225:sd=15:ss=axioms_2871 on theBenchmark for (2871ds/6225Mi)
% 180.85/26.22 % (2380749)Refutation not found, incomplete strategy
% 180.85/26.22 % (2380749)------------------------------
% 180.85/26.22 % (2380749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380749)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380749)Termination reason: Refutation not found, incomplete strategy
% 180.85/26.22 % (2380749)Time elapsed: 0.001 s
% 180.85/26.22 % (2380749)Peak memory usage: 88 MB
% 180.85/26.22 % (2380749)Instructions burned: 1 (million)
% 180.85/26.22 % (2380749)------------------------------
% 180.85/26.22 % (2380749)------------------------------
% 180.85/26.22 % (2380751)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3471256654:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2869 on theBenchmark for (2869ds/3372Mi)
% 180.85/26.22 % (2380741)Instruction limit reached!
% 180.85/26.22 % (2380741)------------------------------
% 180.85/26.22 % (2380741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380741)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380741)Termination reason: Instruction limit
% 180.85/26.22 % (2380741)Termination phase: Saturation
% 180.85/26.22 % (2380741)Time elapsed: 2.906 s
% 180.85/26.22 % (2380741)Peak memory usage: 201 MB
% 180.85/26.22 % (2380741)Instructions burned: 8330 (million)
% 180.85/26.22 % (2380751)Instruction limit reached!
% 180.85/26.22 % (2380751)------------------------------
% 180.85/26.22 % (2380751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 180.85/26.22 % (2380751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.85/26.22 % (2380751)CaDiCaL version: 2.1.3
% 180.85/26.22 % (2380751)Termination reason: Instruction limit
% 180.85/26.22 % (2380751)Termination phase: Saturation
% 180.85/26.22 % (2380751)Time elapsed: 1.041 s
% 180.85/26.22 % (2380751)Peak memory usage: 152 MB
% 180.85/26.22 % (2380751)Instructions burned: 3373 (million)
% 180.85/26.22 % (2380965)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=1733325625:st=2.3:i=26457:sd=10:ss=included:sgt=8_2858 on theBenchmark for (2858ds/26457Mi)
% 203.48/29.56 % (2380966)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=488632246:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2857 on theBenchmark for (2857ds/13494Mi)
% 203.48/29.56 % (2380747)Instruction limit reached!
% 203.48/29.56 % (2380747)------------------------------
% 203.48/29.56 % (2380747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.48/29.56 % (2380747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.48/29.56 % (2380747)CaDiCaL version: 2.1.3
% 203.48/29.56 % (2380747)Termination reason: Instruction limit
% 203.48/29.56 % (2380747)Termination phase: Saturation
% 203.48/29.56 % (2380747)Time elapsed: 2.469 s
% 203.48/29.56 % (2380747)Peak memory usage: 190 MB
% 203.48/29.56 % (2380747)Instructions burned: 6996 (million)
% 203.48/29.56 % (2380965)Refutation not found, incomplete strategy
% 203.48/29.56 % (2380965)------------------------------
% 203.48/29.56 % (2380965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.48/29.56 % (2380965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.48/29.56 % (2380965)CaDiCaL version: 2.1.3
% 203.48/29.56 % (2380965)Termination reason: Refutation not found, incomplete strategy
% 203.48/29.56 % (2380965)Time elapsed: 0.478 s
% 203.48/29.56 % (2380965)Peak memory usage: 128 MB
% 203.48/29.56 % (2380965)Instructions burned: 898 (million)
% 203.48/29.56 % (2381000)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=2942358565:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2852 on theBenchmark for (2852ds/2503Mi)
% 203.48/29.56 % (2380965)------------------------------
% 203.48/29.56 % (2380965)------------------------------
% 203.48/29.56 % (2381002)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=2266812959:i=2559:sd=1:ep=RSTC:ss=axioms_2849 on theBenchmark for (2849ds/2559Mi)
% 203.48/29.56 % (2381002)Refutation not found, incomplete strategy
% 203.48/29.56 % (2381002)------------------------------
% 203.48/29.56 % (2381002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.48/29.56 % (2381002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.48/29.56 % (2381002)CaDiCaL version: 2.1.3
% 203.48/29.56 % (2381002)Termination reason: Refutation not found, incomplete strategy
% 203.48/29.56 % (2381002)Time elapsed: 0.534 s
% 203.48/29.56 % (2381002)Peak memory usage: 127 MB
% 203.48/29.56 % (2381002)Instructions burned: 859 (million)
% 203.48/29.56 % (2381002)------------------------------
% 203.48/29.56 % (2381002)------------------------------
% 203.48/29.56 % (2381004)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=890727817:i=30753:av=off:ss=included_2838 on theBenchmark for (2838ds/30753Mi)
% 203.48/29.56 % (2381000)Instruction limit reached!
% 203.48/29.56 % (2381000)------------------------------
% 203.48/29.56 % (2381000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.48/29.56 % (2381000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.48/29.56 % (2381000)CaDiCaL version: 2.1.3
% 203.48/29.56 % (2381000)Termination reason: Instruction limit
% 203.48/29.56 % (2381000)Termination phase: Saturation
% 203.48/29.56 % (2381000)Time elapsed: 1.419 s
% 203.48/29.56 % (2381000)Peak memory usage: 144 MB
% 203.48/29.56 % (2381000)Instructions burned: 2505 (million)
% 203.48/29.56 % (2381006)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=674480417:i=26473:ep=RSTC_2835 on theBenchmark for (2835ds/26473Mi)
% 203.48/29.56 % (2380727)Instruction limit reached!
% 203.48/29.56 % (2380727)------------------------------
% 203.48/29.56 % (2380727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.48/29.56 % (2380727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.48/29.56 % (2380727)CaDiCaL version: 2.1.3
% 203.48/29.56 % (2380727)Termination reason: Instruction limit
% 203.48/29.56 % (2380727)Termination phase: Saturation
% 203.48/29.56 % (2380727)Time elapsed: 9.249 s
% 203.48/29.56 % (2380727)Peak memory usage: 318 MB
% 203.48/29.56 % (2380727)Instructions burned: 21612 (million)
% 203.48/29.56 % (2381008)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=735982027:cts=off:i=2759:kws=inv_arity:fgj=on_2804 on theBenchmark for (2804ds/2759Mi)
% 203.48/29.56 % (2381008)Refutation not found, incomplete strategy
% 226.89/32.95 % (2381008)------------------------------
% 226.89/32.95 % (2381008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2381008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.89/32.95 % (2381008)CaDiCaL version: 2.1.3
% 226.89/32.95 % (2381008)Termination reason: Refutation not found, incomplete strategy
% 226.89/32.95 % (2381008)Time elapsed: 0.516 s
% 226.89/32.95 % (2381008)Peak memory usage: 128 MB
% 226.89/32.95 % (2381008)Instructions burned: 861 (million)
% 226.89/32.95 % (2381008)------------------------------
% 226.89/32.95 % (2381008)------------------------------
% 226.89/32.95 % (2381010)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=806511368:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2793 on theBenchmark for (2793ds/5665Mi)
% 226.89/32.95 % (2380966)Instruction limit reached!
% 226.89/32.95 % (2380966)------------------------------
% 226.89/32.95 % (2380966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2380966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.89/32.95 % (2380966)CaDiCaL version: 2.1.3
% 226.89/32.95 % (2380966)Termination reason: Instruction limit
% 226.89/32.95 % (2380966)Termination phase: Saturation
% 226.89/32.95 % (2380966)Time elapsed: 8.411 s
% 226.89/32.95 % (2380966)Peak memory usage: 264 MB
% 226.89/32.95 % (2380966)Instructions burned: 13495 (million)
% 226.89/32.95 % (2381012)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=4094476415:i=1532:ep=RS:ss=axioms_2771 on theBenchmark for (2771ds/1532Mi)
% 226.89/32.95 % (2381012)Refutation not found, incomplete strategy
% 226.89/32.95 % (2381012)------------------------------
% 226.89/32.95 % (2381012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2381012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.89/32.95 % (2381012)CaDiCaL version: 2.1.3
% 226.89/32.95 % (2381012)Termination reason: Refutation not found, incomplete strategy
% 226.89/32.95 % (2381012)Time elapsed: 0.547 s
% 226.89/32.95 % (2381012)Peak memory usage: 128 MB
% 226.89/32.95 % (2381012)Instructions burned: 890 (million)
% 226.89/32.95 % (2381012)------------------------------
% 226.89/32.95 % (2381012)------------------------------
% 226.89/32.95 % (2381014)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=1039624077:i=1565:sd=2:ss=axioms:sgt=32_2761 on theBenchmark for (2761ds/1565Mi)
% 226.89/32.95 % (2381010)Instruction limit reached!
% 226.89/32.95 % (2381010)------------------------------
% 226.89/32.95 % (2381010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2381010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.89/32.95 % (2381010)CaDiCaL version: 2.1.3
% 226.89/32.95 % (2381010)Termination reason: Instruction limit
% 226.89/32.95 % (2381010)Termination phase: Saturation
% 226.89/32.95 % (2381010)Time elapsed: 3.599 s
% 226.89/32.95 % (2381010)Peak memory usage: 158 MB
% 226.89/32.95 % (2381010)Instructions burned: 5666 (million)
% 226.89/32.95 % (2381016)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=3463857170:i=1572:fgj=on:gsp=on_2755 on theBenchmark for (2755ds/1572Mi)
% 226.89/32.95 % (2381014)Instruction limit reached!
% 226.89/32.95 % (2381014)------------------------------
% 226.89/32.95 % (2381014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2381014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 226.89/32.95 % (2381014)CaDiCaL version: 2.1.3
% 226.89/32.95 % (2381014)Termination reason: Instruction limit
% 226.89/32.95 % (2381014)Termination phase: Saturation
% 226.89/32.95 % (2381014)Time elapsed: 0.936 s
% 226.89/32.95 % (2381014)Peak memory usage: 135 MB
% 226.89/32.95 % (2381014)Instructions burned: 1565 (million)
% 226.89/32.95 % (2381018)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=2356195348:i=6052:sd=4:ss=axioms:sgt=24_2749 on theBenchmark for (2749ds/6052Mi)
% 226.89/32.95 % (2381016)Instruction limit reached!
% 226.89/32.95 % (2381016)------------------------------
% 226.89/32.95 % (2381016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 226.89/32.95 % (2381016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2381016)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2381016)Termination reason: Instruction limit
% 261.21/37.65 % (2381016)Termination phase: Saturation
% 261.21/37.65 % (2381016)Time elapsed: 0.980 s
% 261.21/37.65 % (2381016)Peak memory usage: 136 MB
% 261.21/37.65 % (2381016)Instructions burned: 1572 (million)
% 261.21/37.65 % (2381018)Refutation not found, incomplete strategy
% 261.21/37.65 % (2381018)------------------------------
% 261.21/37.65 % (2381018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 261.21/37.65 % (2381018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2381018)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2381018)Termination reason: Refutation not found, incomplete strategy
% 261.21/37.65 % (2381018)Time elapsed: 0.539 s
% 261.21/37.65 % (2381018)Peak memory usage: 128 MB
% 261.21/37.65 % (2381018)Instructions burned: 899 (million)
% 261.21/37.65 % (2381020)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=3333538461:i=3500:sd=1:bd=preordered:sup=off:ss=included_2743 on theBenchmark for (2743ds/3500Mi)
% 261.21/37.65 % (2381018)------------------------------
% 261.21/37.65 % (2381018)------------------------------
% 261.21/37.65 % (2381022)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=1663648563:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2739 on theBenchmark for (2739ds/1842Mi)
% 261.21/37.65 % (2381020)Refutation not found, incomplete strategy
% 261.21/37.65 % (2381020)------------------------------
% 261.21/37.65 % (2381020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 261.21/37.65 % (2381020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2381020)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2381020)Termination reason: Refutation not found, incomplete strategy
% 261.21/37.65 % (2381020)Time elapsed: 0.516 s
% 261.21/37.65 % (2381020)Peak memory usage: 127 MB
% 261.21/37.65 % (2381020)Instructions burned: 867 (million)
% 261.21/37.65 % (2381020)------------------------------
% 261.21/37.65 % (2381020)------------------------------
% 261.21/37.65 % (2381024)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2350354357:i=66096:add=on_2732 on theBenchmark for (2732ds/66096Mi)
% 261.21/37.65 % (2381022)Instruction limit reached!
% 261.21/37.65 % (2381022)------------------------------
% 261.21/37.65 % (2381022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 261.21/37.65 % (2381022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2381022)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2381022)Termination reason: Instruction limit
% 261.21/37.65 % (2381022)Termination phase: Saturation
% 261.21/37.65 % (2381022)Time elapsed: 1.076 s
% 261.21/37.65 % (2381022)Peak memory usage: 138 MB
% 261.21/37.65 % (2381022)Instructions burned: 1842 (million)
% 261.21/37.65 % (2381026)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3539024685:i=1884:sd=1:nm=60:ss=axioms_2725 on theBenchmark for (2725ds/1884Mi)
% 261.21/37.65 % (2380736)Instruction limit reached!
% 261.21/37.65 % (2380736)------------------------------
% 261.21/37.65 % (2380736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 261.21/37.65 % (2380736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2380736)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2380736)Termination reason: Instruction limit
% 261.21/37.65 % (2380736)Termination phase: Saturation
% 261.21/37.65 % (2380736)Time elapsed: 17.622 s
% 261.21/37.65 % (2380736)Peak memory usage: 294 MB
% 261.21/37.65 % (2380736)Instructions burned: 33335 (million)
% 261.21/37.65 % (2381028)lrs-1011_4:1_sil=16000:bsr=on:random_seed=1592523999:cts=off:i=5469:bs=on:fsr=off_2714 on theBenchmark for (2714ds/5469Mi)
% 261.21/37.65 % (2381026)Instruction limit reached!
% 261.21/37.65 % (2381026)------------------------------
% 261.21/37.65 % (2381026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 261.21/37.65 % (2381026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 261.21/37.65 % (2381026)CaDiCaL version: 2.1.3
% 261.21/37.65 % (2381026)Termination reason: Instruction limit
% 261.21/37.65 % (2381026)Termination phase: Saturation
% 261.21/37.65 % (2381026)Time elapsed: 1.136 s
% 261.21/37.65 % (2381026)Peak memory usage: 135 MB
% 261.21/37.65 % (2381026)Instructions burned: 1885 (million)
% 261.21/37.65 % (2381030)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=914885640:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2712 on theBenchmark for (2712ds/2037Mi)
% 276.31/39.96 % (2381006)Instruction limit reached!
% 276.31/39.96 % (2381006)------------------------------
% 276.31/39.96 % (2381006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.31/39.96 % (2381006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.31/39.96 % (2381006)CaDiCaL version: 2.1.3
% 276.31/39.96 % (2381006)Termination reason: Instruction limit
% 276.31/39.96 % (2381006)Termination phase: Saturation
% 276.31/39.96 % (2381006)Time elapsed: 12.940 s
% 276.31/39.96 % (2381006)Peak memory usage: 442 MB
% 276.31/39.96 % (2381006)Instructions burned: 26474 (million)
% 276.31/39.96 % (2381032)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2910157929:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2703 on theBenchmark for (2703ds/2110Mi)
% 276.31/39.96 % (2381030)Instruction limit reached!
% 276.31/39.96 % (2381030)------------------------------
% 276.31/39.96 % (2381030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.31/39.96 % (2381030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.31/39.96 % (2381030)CaDiCaL version: 2.1.3
% 276.31/39.96 % (2381030)Termination reason: Instruction limit
% 276.31/39.96 % (2381030)Termination phase: Saturation
% 276.31/39.96 % (2381030)Time elapsed: 1.220 s
% 276.31/39.96 % (2381030)Peak memory usage: 140 MB
% 276.31/39.96 % (2381030)Instructions burned: 2038 (million)
% 276.31/39.96 % (2381034)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=1724238023:i=2430:add=off:aac=none:nm=16_2697 on theBenchmark for (2697ds/2430Mi)
% 276.31/39.96 % (2381032)Instruction limit reached!
% 276.31/39.96 % (2381032)------------------------------
% 276.31/39.96 % (2381032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.31/39.96 % (2381032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.31/39.96 % (2381032)CaDiCaL version: 2.1.3
% 276.31/39.96 % (2381032)Termination reason: Instruction limit
% 276.31/39.96 % (2381032)Termination phase: Saturation
% 276.31/39.96 % (2381032)Time elapsed: 1.207 s
% 276.31/39.96 % (2381032)Peak memory usage: 140 MB
% 276.31/39.96 % (2381032)Instructions burned: 2111 (million)
% 276.31/39.96 % (2381036)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=438202523:cond=fast:i=4891_2689 on theBenchmark for (2689ds/4891Mi)
% 276.31/39.96 % (2381028)Instruction limit reached!
% 276.31/39.96 % (2381028)------------------------------
% 276.31/39.96 % (2381028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.31/39.96 % (2381028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.31/39.96 % (2381028)CaDiCaL version: 2.1.3
% 276.31/39.96 % (2381028)Termination reason: Instruction limit
% 276.31/39.96 % (2381028)Termination phase: Saturation
% 276.31/39.96 % (2381028)Time elapsed: 2.906 s
% 276.31/39.96 % (2381028)Peak memory usage: 112 MB
% 276.31/39.96 % (2381028)Instructions burned: 5470 (million)
% 276.31/39.96 % (2381034)Instruction limit reached!
% 276.31/39.96 % (2381034)------------------------------
% 276.31/39.96 % (2381034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.31/39.96 % (2381034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.31/39.96 % (2381034)CaDiCaL version: 2.1.3
% 276.31/39.96 % (2381034)Termination reason: Instruction limit
% 276.31/39.96 % (2381034)Termination phase: Saturation
% 276.31/39.96 % (2381034)Time elapsed: 1.338 s
% 276.31/39.96 % (2381034)Peak memory usage: 144 MB
% 276.31/39.96 % (2381034)Instructions burned: 2431 (million)
% 276.31/39.96 % (2381038)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=2246152052:st=2:i=14845:sd=2:ss=included:fsd=on_2683 on theBenchmark for (2683ds/14845Mi)
% 276.31/39.96 % (2381039)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3126374215:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2681 on theBenchmark for (2681ds/7534Mi)
% 276.31/39.96 % (2381038)Refutation not found, incomplete strategy
% 276.31/39.96 % (2381038)------------------------------
% 276.31/39.96 % (2381038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381038)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381038)Termination reason: Refutation not found, incomplete strategy
% 252.41/42.86 % (2381038)Time elapsed: 0.518 s
% 252.41/42.86 % (2381038)Peak memory usage: 128 MB
% 252.41/42.86 % (2381038)Instructions burned: 885 (million)
% 252.41/42.86 % (2381038)------------------------------
% 252.41/42.86 % (2381038)------------------------------
% 252.41/42.86 % (2381042)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=1822758994:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2673 on theBenchmark for (2673ds/10353Mi)
% 252.41/42.86 % (2381004)Instruction limit reached!
% 252.41/42.86 % (2381004)------------------------------
% 252.41/42.86 % (2381004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381004)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381004)Termination reason: Instruction limit
% 252.41/42.86 % (2381004)Termination phase: Saturation
% 252.41/42.86 % (2381004)Time elapsed: 17.462 s
% 252.41/42.86 % (2381004)Peak memory usage: 434 MB
% 252.41/42.86 % (2381004)Instructions burned: 30753 (million)
% 252.41/42.86 % (2381044)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=859092525:i=7860_2661 on theBenchmark for (2661ds/7860Mi)
% 252.41/42.86 % (2381036)Instruction limit reached!
% 252.41/42.86 % (2381036)------------------------------
% 252.41/42.86 % (2381036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381036)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381036)Termination reason: Instruction limit
% 252.41/42.86 % (2381036)Termination phase: Saturation
% 252.41/42.86 % (2381036)Time elapsed: 2.791 s
% 252.41/42.86 % (2381036)Peak memory usage: 169 MB
% 252.41/42.86 % (2381036)Instructions burned: 4893 (million)
% 252.41/42.86 % (2381044)Refutation not found, incomplete strategy
% 252.41/42.86 % (2381044)------------------------------
% 252.41/42.86 % (2381044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381044)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381044)Termination reason: Refutation not found, incomplete strategy
% 252.41/42.86 % (2381044)Time elapsed: 0.001 s
% 252.41/42.86 % (2381044)Peak memory usage: 88 MB
% 252.41/42.86 % (2381044)Instructions burned: 1 (million)
% 252.41/42.86 % (2381044)------------------------------
% 252.41/42.86 % (2381044)------------------------------
% 252.41/42.86 % (2381046)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=1129866456:i=7896:sd=2:bs=on:ss=included:sgt=20_2658 on theBenchmark for (2658ds/7896Mi)
% 252.41/42.86 % (2381048)lrs+10_1_ncem=casc2026/models/loop2.pt:sil=16000:tgt=ground:npcc=on:prc=on:random_seed=2596191885:i=5812:gtgl=2:gtg=all_2656 on theBenchmark for (2656ds/5812Mi)
% 252.41/42.86 % (2381039)Instruction limit reached!
% 252.41/42.86 % (2381039)------------------------------
% 252.41/42.86 % (2381039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381039)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381039)Termination reason: Instruction limit
% 252.41/42.86 % (2381039)Termination phase: Saturation
% 252.41/42.86 % (2381039)Time elapsed: 4.300 s
% 252.41/42.86 % (2381039)Peak memory usage: 183 MB
% 252.41/42.86 % (2381039)Instructions burned: 7534 (million)
% 252.41/42.86 % (2381050)ott-1011_1_anc=none:ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:prc=on:sp=const_frequency:sos=on:lsd=100:random_seed=1831773575:i=2965:s2at=3.7:aac=none:fgj=on:fdi=2:er=known_2636 on theBenchmark for (2636ds/2965Mi)
% 252.41/42.86 % (2381050)Aborted by signal SIGSEGV on /export/starexec/sandbox2/benchmark/theBenchmark.p
% 252.41/42.86 % (2381050)------------------------------
% 252.41/42.86 % (2381050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381050)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381050)Termination reason: Unknown
% 252.41/42.86 % (2381050)Termination phase: Saturation
% 252.41/42.86 % (2381050)Time elapsed: 0.514 s
% 252.41/42.86 % (2381050)Peak memory usage: 127 MB
% 252.41/42.86 % (2381050)Instructions burned: 851 (million)
% 252.41/42.86 % (2381052)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=1495501658:i=2967:kws=precedence:bd=preordered:av=off_2628 on theBenchmark for (2628ds/2967Mi)
% 252.41/42.86 % (2381048)Instruction limit reached!
% 252.41/42.86 % (2381048)------------------------------
% 252.41/42.86 % (2381048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381048)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381048)Termination reason: Instruction limit
% 252.41/42.86 % (2381048)Termination phase: Saturation
% 252.41/42.86 % (2381048)Time elapsed: 3.564 s
% 252.41/42.86 % (2381048)Peak memory usage: 189 MB
% 252.41/42.86 % (2381048)Instructions burned: 5814 (million)
% 252.41/42.86 % (2381042)Instruction limit reached!
% 252.41/42.86 % (2381042)------------------------------
% 252.41/42.86 % (2381042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381042)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381042)Termination reason: Instruction limit
% 252.41/42.86 % (2381042)Termination phase: Saturation
% 252.41/42.86 % (2381042)Time elapsed: 5.429 s
% 252.41/42.86 % (2381042)Peak memory usage: 192 MB
% 252.41/42.86 % (2381042)Instructions burned: 10353 (million)
% 252.41/42.86 % (2381054)ott+1002_1_anc=all:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:sos=on:spb=goal_then_units:alpa=false:sac=on:random_seed=3669762834:i=3022:sd=1:kws=frequency:aac=none:ep=RST:nm=16:ss=axioms:er=known_2618 on theBenchmark for (2618ds/3022Mi)
% 252.41/42.86 % (2381055)lrs-1010_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=const_frequency:sos=all:lcm=predicate:acc=on:bsr=unit_only:gs=on:sac=on:newcnf=on:random_seed=2395519453:prac=on:i=3207:kws=frequency:fgj=on:ss=axioms:er=filter:sgt=8_2616 on theBenchmark for (2616ds/3207Mi)
% 252.41/42.86 % (2381046)Instruction limit reached!
% 252.41/42.86 % (2381046)------------------------------
% 252.41/42.86 % (2381046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381046)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381046)Termination reason: Instruction limit
% 252.41/42.86 % (2381046)Termination phase: Saturation
% 252.41/42.86 % (2381046)Time elapsed: 4.331 s
% 252.41/42.86 % (2381046)Peak memory usage: 188 MB
% 252.41/42.86 % (2381046)Instructions burned: 7897 (million)
% 252.41/42.86 % (2381058)lrs+1011_1_anc=all:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:sos=on:lcm=predicate:random_seed=1560379738:st=4.2:i=3289:sd=5:aac=none:ss=included:sgt=10_2613 on theBenchmark for (2613ds/3289Mi)
% 252.41/42.86 % (2381052)Instruction limit reached!
% 252.41/42.86 % (2381052)------------------------------
% 252.41/42.86 % (2381052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381052)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381052)Termination reason: Instruction limit
% 252.41/42.86 % (2381052)Termination phase: Saturation
% 252.41/42.86 % (2381052)Time elapsed: 1.745 s
% 252.41/42.86 % (2381052)Peak memory usage: 148 MB
% 252.41/42.86 % (2381052)Instructions burned: 2968 (million)
% 252.41/42.86 % (2381055)Refutation not found, incomplete strategy
% 252.41/42.86 % (2381055)------------------------------
% 252.41/42.86 % (2381055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381055)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381055)Termination reason: Refutation not found, incomplete strategy
% 252.41/42.86 % (2381055)Time elapsed: 0.533 s
% 252.41/42.86 % (2381055)Peak memory usage: 128 MB
% 252.41/42.86 % (2381055)Instructions burned: 886 (million)
% 252.41/42.86 % (2381060)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:random_seed=2289074089:i=38569:sd=3:ss=axioms:sgt=32_2609 on theBenchmark for (2609ds/38569Mi)
% 252.41/42.86 % (2381055)------------------------------
% 252.41/42.86 % (2381055)------------------------------
% 252.41/42.86 % (2381058)Refutation not found, incomplete strategy
% 252.41/42.86 % (2381058)------------------------------
% 252.41/42.86 % (2381058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381058)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381058)Termination reason: Refutation not found, incomplete strategy
% 252.41/42.86 % (2381058)Time elapsed: 0.498 s
% 252.41/42.86 % (2381058)Peak memory usage: 128 MB
% 252.41/42.86 % (2381058)Instructions burned: 867 (million)
% 252.41/42.86 % (2381062)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=16000:npcc=on:bsr=on:random_seed=2671712287:cts=off:i=3394_2606 on theBenchmark for (2606ds/3394Mi)
% 252.41/42.86 % (2381058)------------------------------
% 252.41/42.86 % (2381058)------------------------------
% 252.41/42.86 % (2381064)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=arity:spb=intro:lcm=reverse:urr=ec_only:fd=preordered:gs=on:sac=on:random_seed=2143176744:i=33824:bd=preordered_2603 on theBenchmark for (2603ds/33824Mi)
% 252.41/42.86 % (2381054)Instruction limit reached!
% 252.41/42.86 % (2381054)------------------------------
% 252.41/42.86 % (2381054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381054)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381054)Termination reason: Instruction limit
% 252.41/42.86 % (2381054)Termination phase: Saturation
% 252.41/42.86 % (2381054)Time elapsed: 2.066 s
% 252.41/42.86 % (2381054)Peak memory usage: 144 MB
% 252.41/42.86 % (2381054)Instructions burned: 3023 (million)
% 252.41/42.86 % (2381066)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=64000:tgt=ground:npcc=on:random_seed=548338068:i=20684:bd=all:gtg=exists_sym_2595 on theBenchmark for (2595ds/20684Mi)
% 252.41/42.86 % (2381062)Instruction limit reached!
% 252.41/42.86 % (2381062)------------------------------
% 252.41/42.86 % (2381062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381062)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381062)Termination reason: Instruction limit
% 252.41/42.86 % (2381062)Termination phase: Saturation
% 252.41/42.86 % (2381062)Time elapsed: 1.918 s
% 252.41/42.86 % (2381062)Peak memory usage: 152 MB
% 252.41/42.86 % (2381062)Instructions burned: 3395 (million)
% 252.41/42.86 % (2381068)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:irw=on:npcc=on:prc=on:bsd=on:sp=reverse_frequency:sos=on:erd=off:spb=goal:lcm=reverse:urr=full:bsr=on:s2agt=32:alpa=random:kmz=on:random_seed=1950039530:st=3:prac=on:i=7222:kws=arity_squared:add=on:fgj=on:bd=preordered:gtg=exists_top:gsp=on:ss=axioms:er=known:sgt=8:proc=on_2584 on theBenchmark for (2584ds/7222Mi)
% 252.41/42.86 % (2380449)First to succeed.
% 252.41/42.86 % (2380449)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2380436"
% 252.41/42.86 % (2381068)Refutation not found, incomplete strategy
% 252.41/42.86 % (2381068)------------------------------
% 252.41/42.86 % (2381068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 252.41/42.86 % (2381068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 252.41/42.86 % (2381068)CaDiCaL version: 2.1.3
% 252.41/42.86 % (2381068)Termination reason: Refutation not found, incomplete strategy
% 252.41/42.86 % (2381068)Time elapsed: 0.408 s
% 252.41/42.86 % (2381068)Peak memory usage: 128 MB
% 252.41/42.86 % (2381068)Instructions burned: 856 (million)
% 252.41/42.86 % (2380449)Refutation found. Thanks to Tanya!
% 252.41/42.86 % SZS status Theorem for theBenchmark
% 252.41/42.86 % SZS output start Proof for theBenchmark
% See solution above
% 297.59/43.06 % (2380449)------------------------------
% 297.59/43.06 % (2380449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 297.59/43.06 % (2380449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 297.59/43.06 % (2380449)CaDiCaL version: 2.1.3
% 297.59/43.06 % (2380449)Termination reason: Refutation
% 297.59/43.06 % (2380449)Time elapsed: 41.623 s
% 297.59/43.06 % (2380449)Peak memory usage: 961 MB
% 297.59/43.06 % (2380449)Instructions burned: 82504 (million)
% 297.59/43.06 % (2380449)------------------------------
% 297.59/43.06 % (2380449)------------------------------
% 297.59/43.06 % (2380436)Success in time 42.31 s
% 297.59/43.06 % Vampire exiting
%------------------------------------------------------------------------------