%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KLE016+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:03 AM UTC 2026
% Result : Theorem 12.59s 2.68s
% Output : Refutation 13.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 31
% Syntax : Number of formulae : 262 ( 138 unt; 16 def)
% Number of atoms : 462 ( 209 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 358 ( 158 ~; 158 |; 22 &)
% ( 16 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 12 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 151 ( 0 sgn 144 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_annihilation) ).
fof(f12,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> addition(X0,X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',order) ).
fof(f13,axiom,
! [X0] :
( test(X0)
<=> ? [X1] : complement(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_1) ).
fof(f14,axiom,
! [X0,X1] :
( complement(X1,X0)
<=> ( multiplication(X0,X1) = zero
& multiplication(X1,X0) = zero
& addition(X0,X1) = one ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_2) ).
fof(f15,axiom,
! [X0,X1] :
( test(X0)
=> ( c(X0) = X1
<=> complement(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',test_3) ).
fof(f17,conjecture,
! [X0,X1] :
( ( test(X1)
& test(X0) )
=> ( leq(c(multiplication(X0,X1)),addition(c(X0),c(X1)))
& leq(addition(c(X0),c(X1)),c(multiplication(X0,X1))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f18,negated_conjecture,
~ ! [X0,X1] :
( ( test(X1)
& test(X0) )
=> ( leq(c(multiplication(X0,X1)),addition(c(X0),c(X1)))
& leq(addition(c(X0),c(X1)),c(multiplication(X0,X1))) ) ),
inference(negated_conjecture,[status(cth)],[f17]) ).
fof(f19,plain,
! [X0,X1] :
( addition(X0,X1) = X1
=> leq(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f20,plain,
! [X0,X1] :
( leq(X0,X1)
| addition(X0,X1) != X1 ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,plain,
! [X0,X1] :
( ( c(X0) = X1
<=> complement(X0,X1) )
| ~ test(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f23,plain,
? [X0,X1] :
( ( ~ leq(c(multiplication(X0,X1)),addition(c(X0),c(X1)))
| ~ leq(addition(c(X0),c(X1)),c(multiplication(X0,X1))) )
& test(X1)
& test(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f24,plain,
? [X0,X1] :
( ( ~ leq(c(multiplication(X0,X1)),addition(c(X0),c(X1)))
| ~ leq(addition(c(X0),c(X1)),c(multiplication(X0,X1))) )
& test(X1)
& test(X0) ),
inference(flattening,[],[f23]) ).
fof(f25,plain,
! [X0] :
( ( test(X0)
| ! [X1] : ~ complement(X1,X0) )
& ( ? [X1] : complement(X1,X0)
| ~ test(X0) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f26,plain,
! [X0] :
( ( test(X0)
| ! [X1] : ~ complement(X1,X0) )
& ( ? [X2] : complement(X2,X0)
| ~ test(X0) ) ),
inference(rectify,[],[f25]) ).
fof(f27,plain,
! [X0] :
( ( test(X0)
| ! [X1] : ~ complement(X1,X0) )
& ( complement(sK0(X0),X0)
| ~ test(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0))],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( ( complement(X1,X0)
| zero != multiplication(X0,X1)
| zero != multiplication(X1,X0)
| addition(X0,X1) != one )
& ( ( multiplication(X0,X1) = zero
& multiplication(X1,X0) = zero
& addition(X0,X1) = one )
| ~ complement(X1,X0) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f29,plain,
! [X0,X1] :
( ( complement(X1,X0)
| zero != multiplication(X0,X1)
| zero != multiplication(X1,X0)
| addition(X0,X1) != one )
& ( ( multiplication(X0,X1) = zero
& multiplication(X1,X0) = zero
& addition(X0,X1) = one )
| ~ complement(X1,X0) ) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( ( ( c(X0) = X1
| ~ complement(X0,X1) )
& ( complement(X0,X1)
| c(X0) != X1 ) )
| ~ test(X0) ),
inference(nnf_transformation,[],[f21]) ).
fof(f31,plain,
( ( ~ leq(c(multiplication(sK1,sK2)),addition(c(sK1),c(sK2)))
| ~ leq(addition(c(sK1),c(sK2)),c(multiplication(sK1,sK2))) )
& test(sK2)
& test(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f24]) ).
fof(f32,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f33,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f34,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f35,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f36,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f38,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f39,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f40,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f41,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f43,plain,
! [X0,X1] :
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[],[f20]) ).
fof(f45,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| test(X0) ),
inference(cnf_transformation,[],[f27]) ).
fof(f46,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| addition(X0,X1) = one ),
inference(cnf_transformation,[],[f29]) ).
fof(f47,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| zero = multiplication(X1,X0) ),
inference(cnf_transformation,[],[f29]) ).
fof(f48,plain,
! [X0,X1] :
( ~ complement(X1,X0)
| zero = multiplication(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f49,plain,
! [X0,X1] :
( zero != multiplication(X1,X0)
| zero != multiplication(X0,X1)
| complement(X1,X0)
| addition(X0,X1) != one ),
inference(cnf_transformation,[],[f29]) ).
fof(f50,plain,
! [X0,X1] :
( complement(X0,X1)
| c(X0) != X1
| ~ test(X0) ),
inference(cnf_transformation,[],[f30]) ).
fof(f53,plain,
test(sK1),
inference(cnf_transformation,[],[f31]) ).
fof(f54,plain,
test(sK2),
inference(cnf_transformation,[],[f31]) ).
fof(f55,plain,
( ~ leq(c(multiplication(sK1,sK2)),addition(c(sK1),c(sK2)))
| ~ leq(addition(c(sK1),c(sK2)),c(multiplication(sK1,sK2))) ),
inference(cnf_transformation,[],[f31]) ).
fof(f56,plain,
! [X0] :
( complement(X0,c(X0))
| ~ test(X0) ),
inference(equality_resolution,[],[f50]) ).
fof(f57,definition,
sF3 = multiplication(sK1,sK2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f58,plain,
multiplication(sK1,sK2) = sF3,
inference(reorient_equations,[],[f57]) ).
fof(f59,definition,
sF4 = c(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f60,plain,
c(sF3) = sF4,
inference(reorient_equations,[],[f59]) ).
fof(f61,definition,
sF5 = c(sK1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f62,plain,
c(sK1) = sF5,
inference(reorient_equations,[],[f61]) ).
fof(f63,definition,
sF6 = c(sK2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f64,plain,
c(sK2) = sF6,
inference(reorient_equations,[],[f63]) ).
fof(f65,definition,
sF7 = addition(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f66,plain,
addition(sF5,sF6) = sF7,
inference(reorient_equations,[],[f65]) ).
fof(f67,plain,
( ~ leq(sF4,sF7)
| ~ leq(sF7,sF4) ),
inference(definition_folding,[],[f55,f60,f58,f66,f64,f62,f66,f64,f62,f60,f58]) ).
fof(f69,definition,
( spl8_1
<=> leq(sF7,sF4) ),
introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition]) ).
fof(f71,plain,
( ~ leq(sF7,sF4)
| spl8_1 ),
inference(avatar_component_clause,[],[f69]) ).
fof(f73,definition,
( spl8_2
<=> leq(sF4,sF7) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f76,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(avatar_split_clause,[],[f67,f73,f69]) ).
fof(f88,plain,
( complement(sK1,sF5)
| ~ test(sK1) ),
inference(superposition,[],[f56,f62]) ).
fof(f89,plain,
complement(sK1,sF5),
inference(forward_subsumption_resolution,[],[f88,f53]) ).
fof(f90,plain,
( complement(sK2,sF6)
| ~ test(sK2) ),
inference(superposition,[],[f56,f64]) ).
fof(f91,plain,
complement(sK2,sF6),
inference(forward_subsumption_resolution,[],[f90,f54]) ).
fof(f92,plain,
( complement(sF3,sF4)
| ~ test(sF3) ),
inference(superposition,[],[f56,f60]) ).
fof(f94,definition,
( spl8_5
<=> test(sF3) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f96,plain,
( ~ test(sF3)
| spl8_5 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f98,definition,
( spl8_6
<=> complement(sF3,sF4) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f100,plain,
( complement(sF3,sF4)
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f98]) ).
fof(f101,plain,
( ~ spl8_5
| spl8_6 ),
inference(avatar_split_clause,[],[f92,f98,f94]) ).
fof(f103,plain,
! [X0,X1] :
( addition(X0,X1) != X0
| leq(X1,X0) ),
inference(superposition,[],[f43,f32]) ).
fof(f119,plain,
one = addition(sF5,sK1),
inference(resolution,[],[f89,f46]) ).
fof(f130,plain,
one = addition(sF6,sK2),
inference(resolution,[],[f91,f46]) ).
fof(f161,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f40,f38]) ).
fof(f167,plain,
! [X0] : addition(zero,X0) = X0,
inference(superposition,[],[f32,f34]) ).
fof(f177,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f33,f35]) ).
fof(f182,plain,
! [X2,X3,X0,X1] : addition(multiplication(X0,X1),addition(multiplication(X0,X2),X3)) = addition(multiplication(X0,addition(X1,X2)),X3),
inference(superposition,[],[f33,f39]) ).
fof(f183,plain,
! [X0] : addition(sF5,addition(sF6,X0)) = addition(sF7,X0),
inference(superposition,[],[f33,f66]) ).
fof(f184,plain,
! [X0] : addition(sF5,addition(sK1,X0)) = addition(one,X0),
inference(superposition,[],[f33,f119]) ).
fof(f185,plain,
! [X0] : addition(one,X0) = addition(sF6,addition(sK2,X0)),
inference(superposition,[],[f33,f130]) ).
fof(f208,plain,
sF7 = addition(sF5,sF7),
inference(superposition,[],[f177,f66]) ).
fof(f209,plain,
one = addition(sF5,one),
inference(superposition,[],[f177,f119]) ).
fof(f210,plain,
one = addition(sF6,one),
inference(superposition,[],[f177,f130]) ).
fof(f235,plain,
one = addition(one,sF6),
inference(superposition,[],[f32,f210]) ).
fof(f263,plain,
zero = multiplication(sK1,sF5),
inference(resolution,[],[f47,f89]) ).
fof(f264,plain,
zero = multiplication(sK2,sF6),
inference(resolution,[],[f47,f91]) ).
fof(f268,plain,
! [X0] : multiplication(addition(sK1,X0),sF5) = addition(zero,multiplication(X0,sF5)),
inference(superposition,[],[f40,f263]) ).
fof(f269,plain,
! [X0] : multiplication(X0,sF5) = multiplication(addition(sK1,X0),sF5),
inference(forward_demodulation,[],[f268,f167]) ).
fof(f273,plain,
! [X0] : multiplication(sK2,addition(X0,sF6)) = addition(multiplication(sK2,X0),zero),
inference(superposition,[],[f39,f264]) ).
fof(f276,plain,
! [X0] : multiplication(addition(sK2,X0),sF6) = addition(zero,multiplication(X0,sF6)),
inference(superposition,[],[f40,f264]) ).
fof(f277,plain,
! [X0] : multiplication(X0,sF6) = multiplication(addition(sK2,X0),sF6),
inference(forward_demodulation,[],[f276,f167]) ).
fof(f280,plain,
! [X0] : multiplication(sK2,addition(X0,sF6)) = multiplication(sK2,X0),
inference(forward_demodulation,[],[f273,f34]) ).
fof(f282,plain,
zero = multiplication(sF5,sK1),
inference(resolution,[],[f48,f89]) ).
fof(f283,plain,
zero = multiplication(sF6,sK2),
inference(resolution,[],[f48,f91]) ).
fof(f284,plain,
! [X0] : multiplication(sF5,addition(X0,sK1)) = addition(multiplication(sF5,X0),zero),
inference(superposition,[],[f39,f282]) ).
fof(f291,plain,
! [X0] : multiplication(sF5,addition(X0,sK1)) = multiplication(sF5,X0),
inference(forward_demodulation,[],[f284,f34]) ).
fof(f292,plain,
! [X0] : multiplication(sF6,addition(X0,sK2)) = addition(multiplication(sF6,X0),zero),
inference(superposition,[],[f39,f283]) ).
fof(f295,plain,
! [X0] : multiplication(addition(sF6,X0),sK2) = addition(zero,multiplication(X0,sK2)),
inference(superposition,[],[f40,f283]) ).
fof(f296,plain,
! [X0] : multiplication(X0,sK2) = multiplication(addition(sF6,X0),sK2),
inference(forward_demodulation,[],[f295,f167]) ).
fof(f299,plain,
! [X0] : multiplication(sF6,addition(X0,sK2)) = multiplication(sF6,X0),
inference(forward_demodulation,[],[f292,f34]) ).
fof(f301,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f39,f37]) ).
fof(f320,plain,
! [X0] : multiplication(sK1,multiplication(sK2,X0)) = multiplication(sF3,X0),
inference(superposition,[],[f36,f58]) ).
fof(f420,plain,
multiplication(sK1,addition(one,sK2)) = addition(sK1,sF3),
inference(superposition,[],[f301,f58]) ).
fof(f478,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,[],[f182,f40]) ).
fof(f561,plain,
! [X0,X1] : addition(multiplication(X0,sF5),multiplication(addition(X0,X1),sK1)) = addition(multiplication(X0,one),multiplication(X1,sK1)),
inference(superposition,[],[f478,f119]) ).
fof(f563,plain,
! [X0,X1] : addition(multiplication(X0,sF6),multiplication(addition(X0,X1),sK2)) = addition(multiplication(X0,one),multiplication(X1,sK2)),
inference(superposition,[],[f478,f130]) ).
fof(f649,plain,
! [X0,X1] : addition(multiplication(X0,sF6),multiplication(addition(X0,X1),sK2)) = addition(X0,multiplication(X1,sK2)),
inference(forward_demodulation,[],[f563,f37]) ).
fof(f651,plain,
! [X0,X1] : addition(multiplication(X0,sF5),multiplication(addition(X0,X1),sK1)) = addition(X0,multiplication(X1,sK1)),
inference(forward_demodulation,[],[f561,f37]) ).
fof(f714,plain,
! [X0] : addition(X0,multiplication(X0,sK1)) = addition(multiplication(X0,sF5),multiplication(X0,sK1)),
inference(superposition,[],[f651,f35]) ).
fof(f769,plain,
! [X0] : multiplication(X0,addition(sF5,sK1)) = addition(X0,multiplication(X0,sK1)),
inference(forward_demodulation,[],[f714,f39]) ).
fof(f786,plain,
! [X0] : multiplication(X0,addition(sF5,sK1)) = multiplication(X0,addition(one,sK1)),
inference(forward_demodulation,[],[f769,f301]) ).
fof(f797,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,addition(one,sK1)),
inference(forward_demodulation,[],[f786,f119]) ).
fof(f803,plain,
! [X0] : multiplication(X0,addition(one,sK1)) = X0,
inference(forward_demodulation,[],[f797,f37]) ).
fof(f808,plain,
! [X0] : addition(X0,multiplication(X0,sK2)) = addition(multiplication(X0,sF6),multiplication(X0,sK2)),
inference(superposition,[],[f649,f35]) ).
fof(f868,plain,
! [X0] : multiplication(X0,addition(sF6,sK2)) = addition(X0,multiplication(X0,sK2)),
inference(forward_demodulation,[],[f808,f39]) ).
fof(f888,plain,
! [X0] : multiplication(X0,addition(sF6,sK2)) = multiplication(X0,addition(one,sK2)),
inference(forward_demodulation,[],[f868,f301]) ).
fof(f902,plain,
! [X0] : multiplication(X0,one) = multiplication(X0,addition(one,sK2)),
inference(forward_demodulation,[],[f888,f130]) ).
fof(f909,plain,
! [X0] : multiplication(X0,addition(one,sK2)) = X0,
inference(forward_demodulation,[],[f902,f37]) ).
fof(f931,plain,
addition(sF5,one) = addition(sF7,sK2),
inference(superposition,[],[f183,f130]) ).
fof(f935,plain,
! [X0] : addition(sF7,X0) = addition(sF5,addition(X0,sF6)),
inference(superposition,[],[f183,f32]) ).
fof(f952,plain,
one = addition(sF7,sK2),
inference(forward_demodulation,[],[f931,f209]) ).
fof(f957,plain,
one = addition(sK2,sF7),
inference(superposition,[],[f32,f952]) ).
fof(f962,plain,
addition(sF7,multiplication(sK2,sK2)) = addition(multiplication(sF7,sF6),multiplication(one,sK2)),
inference(superposition,[],[f649,f952]) ).
fof(f965,plain,
addition(sF7,multiplication(sK2,sK2)) = addition(multiplication(sF7,sF6),sK2),
inference(forward_demodulation,[],[f962,f38]) ).
fof(f1069,plain,
multiplication(one,sF6) = multiplication(sF7,sF6),
inference(superposition,[],[f277,f957]) ).
fof(f1097,plain,
sF6 = multiplication(sF7,sF6),
inference(forward_demodulation,[],[f1069,f38]) ).
fof(f1212,plain,
one = addition(one,sK1),
inference(superposition,[],[f38,f803]) ).
fof(f1242,plain,
addition(multiplication(one,sF6),multiplication(one,sK2)) = addition(one,multiplication(sK1,sK2)),
inference(superposition,[],[f649,f1212]) ).
fof(f1245,plain,
addition(multiplication(one,sF6),multiplication(one,sK2)) = addition(one,sF3),
inference(forward_demodulation,[],[f1242,f58]) ).
fof(f1248,plain,
multiplication(one,addition(sF6,sK2)) = addition(one,sF3),
inference(forward_demodulation,[],[f1245,f39]) ).
fof(f1250,plain,
addition(sF6,sK2) = addition(one,sF3),
inference(forward_demodulation,[],[f1248,f38]) ).
fof(f1251,plain,
one = addition(one,sF3),
inference(forward_demodulation,[],[f1250,f130]) ).
fof(f1600,plain,
multiplication(one,sK2) = multiplication(sK2,sK2),
inference(superposition,[],[f296,f130]) ).
fof(f1631,plain,
sK2 = multiplication(sK2,sK2),
inference(forward_demodulation,[],[f1600,f38]) ).
fof(f1643,plain,
multiplication(sK1,sK2) = multiplication(sF3,sK2),
inference(superposition,[],[f320,f1631]) ).
fof(f1664,plain,
sF3 = multiplication(sF3,sK2),
inference(forward_demodulation,[],[f1643,f58]) ).
fof(f1676,plain,
addition(sK2,sF3) = multiplication(addition(one,sF3),sK2),
inference(superposition,[],[f161,f1664]) ).
fof(f1682,plain,
multiplication(one,sK2) = addition(sK2,sF3),
inference(forward_demodulation,[],[f1676,f1251]) ).
fof(f1688,plain,
sK2 = addition(sK2,sF3),
inference(forward_demodulation,[],[f1682,f38]) ).
fof(f1694,plain,
sK2 = addition(sF3,sK2),
inference(superposition,[],[f32,f1688]) ).
fof(f1742,plain,
sK1 = addition(sK1,sF3),
inference(superposition,[],[f909,f420]) ).
fof(f1801,plain,
multiplication(sK1,sF5) = multiplication(sF3,sF5),
inference(superposition,[],[f269,f1742]) ).
fof(f1803,plain,
sK1 = addition(sF3,sK1),
inference(superposition,[],[f32,f1742]) ).
fof(f1823,plain,
zero = multiplication(sF3,sF5),
inference(forward_demodulation,[],[f1801,f263]) ).
fof(f2025,definition,
( spl8_31
<=> zero = multiplication(sF5,sF3) ),
introduced(definition,[new_symbols(definition,[spl8_31])],[avatar_definition]) ).
fof(f2026,plain,
( zero = multiplication(sF5,sF3)
| ~ spl8_31 ),
inference(avatar_component_clause,[],[f2025]) ).
fof(f2039,definition,
( spl8_34
<=> zero = multiplication(sF6,sF3) ),
introduced(definition,[new_symbols(definition,[spl8_34])],[avatar_definition]) ).
fof(f2040,plain,
( zero = multiplication(sF6,sF3)
| ~ spl8_34 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2041,plain,
( zero != multiplication(sF6,sF3)
| spl8_34 ),
inference(avatar_component_clause,[],[f2039]) ).
fof(f2063,definition,
( spl8_35
<=> one = addition(sK2,sF6) ),
introduced(definition,[new_symbols(definition,[spl8_35])],[avatar_definition]) ).
fof(f2064,plain,
( one = addition(sK2,sF6)
| ~ spl8_35 ),
inference(avatar_component_clause,[],[f2063]) ).
fof(f2065,plain,
( one != addition(sK2,sF6)
| spl8_35 ),
inference(avatar_component_clause,[],[f2063]) ).
fof(f2323,plain,
multiplication(sF5,sK1) = multiplication(sF5,sF3),
inference(superposition,[],[f291,f1803]) ).
fof(f2351,plain,
zero = multiplication(sF5,sF3),
inference(forward_demodulation,[],[f2323,f282]) ).
fof(f2358,plain,
spl8_31,
inference(avatar_split_clause,[],[f2351,f2025]) ).
fof(f2471,plain,
multiplication(sF6,sK2) = multiplication(sF6,sF3),
inference(superposition,[],[f299,f1694]) ).
fof(f2502,plain,
zero = multiplication(sF6,sF3),
inference(forward_demodulation,[],[f2471,f283]) ).
fof(f2509,plain,
( $false
| spl8_34 ),
inference(forward_subsumption_resolution,[],[f2502,f2041]) ).
fof(f2510,plain,
spl8_34,
inference(avatar_contradiction_clause,[],[f2509]) ).
fof(f2753,plain,
addition(sF6,one) = addition(one,sF7),
inference(superposition,[],[f185,f957]) ).
fof(f2779,plain,
one = addition(one,sF7),
inference(forward_demodulation,[],[f2753,f210]) ).
fof(f3114,plain,
multiplication(sK2,sF5) = multiplication(sK2,sF7),
inference(superposition,[],[f280,f66]) ).
fof(f3153,plain,
multiplication(sF3,sF7) = multiplication(sK1,multiplication(sK2,sF5)),
inference(superposition,[],[f320,f3114]) ).
fof(f3177,plain,
multiplication(sF3,sF5) = multiplication(sF3,sF7),
inference(forward_demodulation,[],[f3153,f320]) ).
fof(f3195,plain,
zero = multiplication(sF3,sF7),
inference(forward_demodulation,[],[f3177,f1823]) ).
fof(f3201,plain,
! [X0] : multiplication(addition(X0,sF3),sF7) = addition(multiplication(X0,sF7),zero),
inference(superposition,[],[f40,f3195]) ).
fof(f3220,definition,
( spl8_50
<=> one = addition(sF7,sF3) ),
introduced(definition,[new_symbols(definition,[spl8_50])],[avatar_definition]) ).
fof(f3221,plain,
( one = addition(sF7,sF3)
| ~ spl8_50 ),
inference(avatar_component_clause,[],[f3220]) ).
fof(f3222,plain,
( one != addition(sF7,sF3)
| spl8_50 ),
inference(avatar_component_clause,[],[f3220]) ).
fof(f3228,definition,
( spl8_52
<=> zero = multiplication(sF7,sF3) ),
introduced(definition,[new_symbols(definition,[spl8_52])],[avatar_definition]) ).
fof(f3229,plain,
( zero = multiplication(sF7,sF3)
| ~ spl8_52 ),
inference(avatar_component_clause,[],[f3228]) ).
fof(f3230,plain,
( zero != multiplication(sF7,sF3)
| spl8_52 ),
inference(avatar_component_clause,[],[f3228]) ).
fof(f3233,plain,
! [X0] : multiplication(X0,sF7) = multiplication(addition(X0,sF3),sF7),
inference(forward_demodulation,[],[f3201,f34]) ).
fof(f3427,definition,
( spl8_53
<=> one = addition(sF7,sK1) ),
introduced(definition,[new_symbols(definition,[spl8_53])],[avatar_definition]) ).
fof(f3428,plain,
( one = addition(sF7,sK1)
| ~ spl8_53 ),
inference(avatar_component_clause,[],[f3427]) ).
fof(f3429,plain,
( one != addition(sF7,sK1)
| spl8_53 ),
inference(avatar_component_clause,[],[f3427]) ).
fof(f4053,plain,
addition(one,sF6) = addition(sF7,sK1),
inference(superposition,[],[f184,f935]) ).
fof(f4078,plain,
one = addition(sF7,sK1),
inference(forward_demodulation,[],[f4053,f235]) ).
fof(f4087,plain,
( $false
| spl8_53 ),
inference(forward_subsumption_resolution,[],[f4078,f3429]) ).
fof(f4088,plain,
spl8_53,
inference(avatar_contradiction_clause,[],[f4087]) ).
fof(f4103,plain,
( addition(multiplication(sF7,sF6),multiplication(one,sK2)) = addition(sF7,multiplication(sK1,sK2))
| ~ spl8_53 ),
inference(superposition,[],[f649,f3428]) ).
fof(f4106,plain,
( addition(multiplication(sF7,sF6),multiplication(one,sK2)) = addition(sF7,sF3)
| ~ spl8_53 ),
inference(forward_demodulation,[],[f4103,f58]) ).
fof(f4112,plain,
( addition(multiplication(sF7,sF6),sK2) = addition(sF7,sF3)
| ~ spl8_53 ),
inference(forward_demodulation,[],[f4106,f38]) ).
fof(f4114,plain,
( addition(sF7,multiplication(sK2,sK2)) = addition(sF7,sF3)
| ~ spl8_53 ),
inference(forward_demodulation,[],[f4112,f965]) ).
fof(f4116,plain,
( addition(sF7,sK2) = addition(sF7,sF3)
| ~ spl8_53 ),
inference(forward_demodulation,[],[f4114,f1631]) ).
fof(f4118,plain,
( one = addition(sF7,sF3)
| ~ spl8_53 ),
inference(forward_demodulation,[],[f4116,f952]) ).
fof(f4120,plain,
( $false
| spl8_50
| ~ spl8_53 ),
inference(forward_subsumption_resolution,[],[f4118,f3222]) ).
fof(f4121,plain,
( spl8_50
| ~ spl8_53 ),
inference(avatar_contradiction_clause,[],[f4120]) ).
fof(f5558,plain,
( one = addition(sF3,sF7)
| ~ spl8_50 ),
inference(superposition,[],[f32,f3221]) ).
fof(f7248,plain,
( one != addition(sF6,sK2)
| spl8_35 ),
inference(superposition,[],[f2065,f32]) ).
fof(f7252,plain,
( $false
| spl8_35 ),
inference(forward_subsumption_resolution,[],[f7248,f130]) ).
fof(f7253,plain,
spl8_35,
inference(avatar_contradiction_clause,[],[f7252]) ).
fof(f7273,plain,
( ! [X0,X1] : addition(multiplication(X0,one),multiplication(X1,sF6)) = addition(multiplication(X0,sK2),multiplication(addition(X0,X1),sF6))
| ~ spl8_35 ),
inference(superposition,[],[f478,f2064]) ).
fof(f7281,plain,
( ! [X0,X1] : addition(X0,multiplication(X1,sF6)) = addition(multiplication(X0,sK2),multiplication(addition(X0,X1),sF6))
| ~ spl8_35 ),
inference(forward_demodulation,[],[f7273,f37]) ).
fof(f8189,plain,
( addition(multiplication(sF5,sK2),multiplication(one,sF6)) = addition(sF5,multiplication(sK1,sF6))
| ~ spl8_35 ),
inference(superposition,[],[f7281,f119]) ).
fof(f8192,plain,
( addition(multiplication(sF5,sK2),multiplication(sF7,sF6)) = addition(sF5,multiplication(sF7,sF6))
| ~ spl8_35 ),
inference(superposition,[],[f7281,f208]) ).
fof(f8269,plain,
( addition(sF5,sF6) = addition(multiplication(sF5,sK2),sF6)
| ~ spl8_35 ),
inference(forward_demodulation,[],[f8192,f1097]) ).
fof(f8272,plain,
( addition(multiplication(sF5,sK2),sF6) = addition(sF5,multiplication(sK1,sF6))
| ~ spl8_35 ),
inference(forward_demodulation,[],[f8189,f38]) ).
fof(f8366,plain,
( sF7 = addition(multiplication(sF5,sK2),sF6)
| ~ spl8_35 ),
inference(forward_demodulation,[],[f8269,f66]) ).
fof(f8452,plain,
( sF7 = addition(sF5,multiplication(sK1,sF6))
| ~ spl8_35 ),
inference(forward_demodulation,[],[f8366,f8272]) ).
fof(f9060,plain,
( ! [X0] : multiplication(addition(sF5,X0),sF3) = addition(zero,multiplication(X0,sF3))
| ~ spl8_31 ),
inference(superposition,[],[f40,f2026]) ).
fof(f9082,plain,
( ! [X0] : multiplication(X0,sF3) = multiplication(addition(sF5,X0),sF3)
| ~ spl8_31 ),
inference(forward_demodulation,[],[f9060,f167]) ).
fof(f9105,plain,
( multiplication(sF7,sF3) = multiplication(multiplication(sK1,sF6),sF3)
| ~ spl8_31
| ~ spl8_35 ),
inference(superposition,[],[f9082,f8452]) ).
fof(f9152,plain,
( multiplication(sF7,sF3) = multiplication(sK1,multiplication(sF6,sF3))
| ~ spl8_31
| ~ spl8_35 ),
inference(forward_demodulation,[],[f9105,f36]) ).
fof(f9167,plain,
( multiplication(sK1,zero) = multiplication(sF7,sF3)
| ~ spl8_31
| ~ spl8_34
| ~ spl8_35 ),
inference(forward_demodulation,[],[f9152,f2040]) ).
fof(f9172,plain,
( zero = multiplication(sF7,sF3)
| ~ spl8_31
| ~ spl8_34
| ~ spl8_35 ),
inference(forward_demodulation,[],[f9167,f41]) ).
fof(f9176,plain,
( $false
| ~ spl8_31
| ~ spl8_34
| ~ spl8_35
| spl8_52 ),
inference(forward_subsumption_resolution,[],[f9172,f3230]) ).
fof(f9177,plain,
( ~ spl8_31
| ~ spl8_34
| ~ spl8_35
| spl8_52 ),
inference(avatar_contradiction_clause,[],[f9176]) ).
fof(f9184,plain,
( zero != zero
| zero != multiplication(sF3,sF7)
| complement(sF7,sF3)
| one != addition(sF3,sF7)
| ~ spl8_52 ),
inference(superposition,[],[f49,f3229]) ).
fof(f9194,plain,
( zero != multiplication(sF3,sF7)
| complement(sF7,sF3)
| one != addition(sF3,sF7)
| ~ spl8_52 ),
inference(trivial_inequality_removal,[],[f9184]) ).
fof(f9204,plain,
( complement(sF7,sF3)
| one != addition(sF3,sF7)
| ~ spl8_52 ),
inference(forward_subsumption_resolution,[],[f9194,f3195]) ).
fof(f9215,plain,
( complement(sF7,sF3)
| ~ spl8_50
| ~ spl8_52 ),
inference(forward_subsumption_resolution,[],[f9204,f5558]) ).
fof(f9361,plain,
( test(sF3)
| ~ spl8_50
| ~ spl8_52 ),
inference(resolution,[],[f9215,f45]) ).
fof(f9375,plain,
( $false
| spl8_5
| ~ spl8_50
| ~ spl8_52 ),
inference(forward_subsumption_resolution,[],[f9361,f96]) ).
fof(f9376,plain,
( spl8_5
| ~ spl8_50
| ~ spl8_52 ),
inference(avatar_contradiction_clause,[],[f9375]) ).
fof(f9379,plain,
( zero = multiplication(sF4,sF3)
| ~ spl8_6 ),
inference(resolution,[],[f100,f48]) ).
fof(f9381,plain,
( one = addition(sF4,sF3)
| ~ spl8_6 ),
inference(resolution,[],[f100,f46]) ).
fof(f9418,plain,
( multiplication(one,sF7) = multiplication(sF4,sF7)
| ~ spl8_6 ),
inference(superposition,[],[f3233,f9381]) ).
fof(f9454,plain,
( sF7 = multiplication(sF4,sF7)
| ~ spl8_6 ),
inference(forward_demodulation,[],[f9418,f38]) ).
fof(f9466,plain,
( ! [X0] : multiplication(sF4,addition(sF3,X0)) = addition(zero,multiplication(sF4,X0))
| ~ spl8_6 ),
inference(superposition,[],[f39,f9379]) ).
fof(f9494,plain,
( ! [X0] : multiplication(sF4,X0) = multiplication(sF4,addition(sF3,X0))
| ~ spl8_6 ),
inference(forward_demodulation,[],[f9466,f167]) ).
fof(f9584,plain,
( multiplication(sF4,addition(one,sF7)) = addition(sF4,sF7)
| ~ spl8_6 ),
inference(superposition,[],[f301,f9454]) ).
fof(f9586,plain,
( multiplication(sF4,one) = addition(sF4,sF7)
| ~ spl8_6 ),
inference(forward_demodulation,[],[f9584,f2779]) ).
fof(f9592,plain,
( sF4 = addition(sF4,sF7)
| ~ spl8_6 ),
inference(forward_demodulation,[],[f9586,f37]) ).
fof(f10047,plain,
( sF4 != sF7
| leq(sF4,sF7)
| ~ spl8_6 ),
inference(superposition,[],[f43,f9592]) ).
fof(f10048,plain,
( sF4 != sF4
| leq(sF7,sF4)
| ~ spl8_6 ),
inference(superposition,[],[f103,f9592]) ).
fof(f10062,plain,
( leq(sF7,sF4)
| ~ spl8_6 ),
inference(trivial_inequality_removal,[],[f10048]) ).
fof(f10069,plain,
( $false
| spl8_1
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f10062,f71]) ).
fof(f10070,plain,
( spl8_1
| ~ spl8_6 ),
inference(avatar_contradiction_clause,[],[f10069]) ).
fof(f10072,definition,
( spl8_123
<=> sF4 = sF7 ),
introduced(definition,[new_symbols(definition,[spl8_123])],[avatar_definition]) ).
fof(f10074,plain,
( sF4 != sF7
| spl8_123 ),
inference(avatar_component_clause,[],[f10072]) ).
fof(f10075,plain,
( spl8_2
| ~ spl8_123
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f10047,f98,f10072,f73]) ).
fof(f10402,plain,
( multiplication(sF4,sF7) = multiplication(sF4,one)
| ~ spl8_6
| ~ spl8_50 ),
inference(superposition,[],[f9494,f5558]) ).
fof(f10442,plain,
( sF4 = multiplication(sF4,sF7)
| ~ spl8_6
| ~ spl8_50 ),
inference(forward_demodulation,[],[f10402,f37]) ).
fof(f10456,plain,
( sF4 = sF7
| ~ spl8_6
| ~ spl8_50 ),
inference(forward_demodulation,[],[f10442,f9454]) ).
fof(f10459,plain,
( $false
| ~ spl8_6
| ~ spl8_50
| spl8_123 ),
inference(forward_subsumption_resolution,[],[f10456,f10074]) ).
fof(f10460,plain,
( ~ spl8_6
| ~ spl8_50
| spl8_123 ),
inference(avatar_contradiction_clause,[],[f10459]) ).
cnf(s1,plain,
( ~ spl8_1
| ~ spl8_2 ),
inference(sat_conversion,[],[f76]) ).
cnf(s3,plain,
( ~ spl8_5
| spl8_6 ),
inference(sat_conversion,[],[f101]) ).
cnf(s21,plain,
spl8_31,
inference(sat_conversion,[],[f2358]) ).
cnf(s22,plain,
spl8_34,
inference(sat_conversion,[],[f2510]) ).
cnf(s30,plain,
spl8_53,
inference(sat_conversion,[],[f4088]) ).
cnf(s31,plain,
( spl8_50
| ~ spl8_53 ),
inference(sat_conversion,[],[f4121]) ).
cnf(s54,plain,
spl8_35,
inference(sat_conversion,[],[f7253]) ).
cnf(s63,plain,
( ~ spl8_31
| ~ spl8_34
| ~ spl8_35
| spl8_52 ),
inference(sat_conversion,[],[f9177]) ).
cnf(s65,plain,
( spl8_5
| ~ spl8_50
| ~ spl8_52 ),
inference(sat_conversion,[],[f9376]) ).
cnf(s70,plain,
( spl8_1
| ~ spl8_6 ),
inference(sat_conversion,[],[f10070]) ).
cnf(s71,plain,
( spl8_2
| ~ spl8_6
| ~ spl8_123 ),
inference(sat_conversion,[],[f10075]) ).
cnf(s74,plain,
( ~ spl8_6
| ~ spl8_50
| spl8_123 ),
inference(sat_conversion,[],[f10460]) ).
cnf(s75,plain,
spl8_50,
inference(rat,[],[s31,s30]) ).
cnf(s78,plain,
spl8_52,
inference(rat,[],[s63,s22,s54,s21]) ).
cnf(s79,plain,
spl8_5,
inference(rat,[],[s65,s75,s78]) ).
cnf(s85,plain,
spl8_6,
inference(rat,[],[s3,s79]) ).
cnf(s86,plain,
spl8_123,
inference(rat,[],[s74,s75,s85]) ).
cnf(s87,plain,
spl8_2,
inference(rat,[],[s71,s86,s85]) ).
cnf(s88,plain,
spl8_1,
inference(rat,[],[s70,s85]) ).
cnf(s89,plain,
$false,
inference(rat,[],[s1,s87,s88]) ).
fof(f10462,plain,
$false,
inference(avatar_sat_refutation,[],[s89]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE016+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.35 % Computer : n017.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 27 12:54:50 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.59/2.63 % (2529156)Detected formulas, will run a generic FOF schedule.
% 12.59/2.63 % (2529162)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=2464427973:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.59/2.63 % (2529163)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=3060928325:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.59/2.63 % (2529161)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=3590364059:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.59/2.63 % (2529165)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1510915877:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.59/2.63 % (2529164)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3137886587:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.59/2.63 % (2529164)Refutation not found, incomplete strategy
% 12.59/2.63 % (2529164)------------------------------
% 12.59/2.63 % (2529164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.63 % (2529164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.63 % (2529164)CaDiCaL version: 2.1.3
% 12.59/2.63 % (2529164)Termination reason: Refutation not found, incomplete strategy
% 12.59/2.63 % (2529164)Time elapsed: 0.002 s
% 12.59/2.63 % (2529164)Peak memory usage: 88 MB
% 12.59/2.63 % (2529167)dis-21_1_sil=8000:lcm=predicate:random_seed=3916338748:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.59/2.63 % (2529166)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2021606490:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.59/2.63 % (2529167)Refutation not found, incomplete strategy
% 12.59/2.63 % (2529167)------------------------------
% 12.59/2.63 % (2529167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.63 % (2529167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.63 % (2529167)CaDiCaL version: 2.1.3
% 12.59/2.63 % (2529167)Termination reason: Refutation not found, incomplete strategy
% 12.59/2.63 % (2529167)Time elapsed: 0.003 s
% 12.59/2.63 % (2529167)Peak memory usage: 88 MB
% 12.59/2.63 % (2529167)Instructions burned: 2 (million)
% 12.59/2.63 % (2529165)Instruction limit reached!
% 12.59/2.63 % (2529165)------------------------------
% 12.59/2.63 % (2529165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.63 % (2529165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.63 % (2529165)CaDiCaL version: 2.1.3
% 12.59/2.63 % (2529165)Termination reason: Instruction limit
% 12.59/2.63 % (2529165)Termination phase: Saturation
% 12.59/2.63 % (2529165)Time elapsed: 0.072 s
% 12.59/2.63 % (2529165)Peak memory usage: 88 MB
% 12.59/2.63 % (2529165)Instructions burned: 119 (million)
% 12.59/2.63 % (2529166)Instruction limit reached!
% 12.59/2.63 % (2529166)------------------------------
% 12.59/2.63 % (2529166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.63 % (2529166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.63 % (2529166)CaDiCaL version: 2.1.3
% 12.59/2.63 % (2529166)Termination reason: Instruction limit
% 12.59/2.63 % (2529166)Termination phase: Saturation
% 12.59/2.63 % (2529166)Time elapsed: 0.081 s
% 12.59/2.63 % (2529166)Peak memory usage: 90 MB
% 12.59/2.63 % (2529166)Instructions burned: 140 (million)
% 12.59/2.63 % (2529175)lrs+10_1_sil=8000:sp=occurrence:random_seed=3595817019:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.59/2.63 % (2529164)------------------------------
% 12.59/2.63 % (2529164)------------------------------
% 12.59/2.63 % (2529176)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2392949045:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.59/2.63 % (2529167)------------------------------
% 12.59/2.63 % (2529167)------------------------------
% 12.59/2.63 % (2529176)Instruction limit reached!
% 12.59/2.63 % (2529176)------------------------------
% 12.59/2.63 % (2529176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.63 % (2529176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529176)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529176)Termination reason: Instruction limit
% 12.59/2.68 % (2529176)Termination phase: Saturation
% 12.59/2.68 % (2529176)Time elapsed: 0.091 s
% 12.59/2.68 % (2529176)Peak memory usage: 90 MB
% 12.59/2.68 % (2529176)Instructions burned: 158 (million)
% 12.59/2.68 % (2529179)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3977568712:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.59/2.68 % (2529175)Instruction limit reached!
% 12.59/2.68 % (2529175)------------------------------
% 12.59/2.68 % (2529175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529175)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529175)Termination reason: Instruction limit
% 12.59/2.68 % (2529175)Termination phase: Saturation
% 12.59/2.68 % (2529175)Time elapsed: 0.178 s
% 12.59/2.68 % (2529175)Peak memory usage: 91 MB
% 12.59/2.68 % (2529175)Instructions burned: 286 (million)
% 12.59/2.68 % (2529180)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=2363855395:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 12.59/2.68 % (2529181)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4243518825:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.59/2.68 % (2529183)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3597468609:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 12.59/2.68 % (2529180)Instruction limit reached!
% 12.59/2.68 % (2529180)------------------------------
% 12.59/2.68 % (2529180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529180)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529180)Termination reason: Instruction limit
% 12.59/2.68 % (2529180)Termination phase: Saturation
% 12.59/2.68 % (2529180)Time elapsed: 0.151 s
% 12.59/2.68 % (2529180)Peak memory usage: 91 MB
% 12.59/2.68 % (2529180)Instructions burned: 248 (million)
% 12.59/2.68 % (2529179)Instruction limit reached!
% 12.59/2.68 % (2529179)------------------------------
% 12.59/2.68 % (2529179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529179)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529179)Termination reason: Instruction limit
% 12.59/2.68 % (2529179)Termination phase: Saturation
% 12.59/2.68 % (2529179)Time elapsed: 0.189 s
% 12.59/2.68 % (2529179)Peak memory usage: 91 MB
% 12.59/2.68 % (2529179)Instructions burned: 325 (million)
% 12.59/2.68 % (2529181)Instruction limit reached!
% 12.59/2.68 % (2529181)------------------------------
% 12.59/2.68 % (2529181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529181)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529181)Termination reason: Instruction limit
% 12.59/2.68 % (2529181)Termination phase: Saturation
% 12.59/2.68 % (2529181)Time elapsed: 0.170 s
% 12.59/2.68 % (2529181)Peak memory usage: 89 MB
% 12.59/2.68 % (2529181)Instructions burned: 294 (million)
% 12.59/2.68 % (2529187)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1667353419:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 12.59/2.68 % (2529188)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2025922021:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 12.59/2.68 % (2529187)Instruction limit reached!
% 12.59/2.68 % (2529187)------------------------------
% 12.59/2.68 % (2529187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529187)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529187)Termination reason: Instruction limit
% 12.59/2.68 % (2529187)Termination phase: Saturation
% 12.59/2.68 % (2529187)Time elapsed: 0.079 s
% 12.59/2.68 % (2529187)Peak memory usage: 90 MB
% 12.59/2.68 % (2529187)Instructions burned: 113 (million)
% 12.59/2.68 % (2529188)Instruction limit reached!
% 12.59/2.68 % (2529188)------------------------------
% 12.59/2.68 % (2529188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529188)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529188)Termination reason: Instruction limit
% 12.59/2.68 % (2529188)Termination phase: Saturation
% 12.59/2.68 % (2529188)Time elapsed: 0.063 s
% 12.59/2.68 % (2529188)Peak memory usage: 89 MB
% 12.59/2.68 % (2529188)Instructions burned: 128 (million)
% 12.59/2.68 % (2529189)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3229723504:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 12.59/2.68 % (2529189)Instruction limit reached!
% 12.59/2.68 % (2529189)------------------------------
% 12.59/2.68 % (2529189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529189)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529189)Termination reason: Instruction limit
% 12.59/2.68 % (2529189)Termination phase: Saturation
% 12.59/2.68 % (2529189)Time elapsed: 0.071 s
% 12.59/2.68 % (2529189)Peak memory usage: 89 MB
% 12.59/2.68 % (2529189)Instructions burned: 114 (million)
% 12.59/2.68 % (2529192)lrs+10_1_sil=8000:sp=occurrence:random_seed=4261494494:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 12.59/2.68 % (2529194)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3286828027:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 12.59/2.68 % (2529195)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2527837431:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 12.59/2.68 % (2529194)Instruction limit reached!
% 12.59/2.68 % (2529194)------------------------------
% 12.59/2.68 % (2529194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529194)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529194)Termination reason: Instruction limit
% 12.59/2.68 % (2529194)Termination phase: Saturation
% 12.59/2.68 % (2529194)Time elapsed: 0.255 s
% 12.59/2.68 % (2529194)Peak memory usage: 91 MB
% 12.59/2.68 % (2529194)Instructions burned: 438 (million)
% 12.59/2.68 % (2529199)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2304221559:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 12.59/2.68 % (2529161)First to succeed.
% 12.59/2.68 % (2529161)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2529156"
% 12.59/2.68 % (2529199)Instruction limit reached!
% 12.59/2.68 % (2529199)------------------------------
% 12.59/2.68 % (2529199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529199)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529199)Termination reason: Instruction limit
% 12.59/2.68 % (2529199)Termination phase: Saturation
% 12.59/2.68 % (2529199)Time elapsed: 0.073 s
% 12.59/2.68 % (2529199)Peak memory usage: 90 MB
% 12.59/2.68 % (2529199)Instructions burned: 136 (million)
% 12.59/2.68 % (2529192)Instruction limit reached!
% 12.59/2.68 % (2529192)------------------------------
% 12.59/2.68 % (2529192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529192)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529192)Termination reason: Instruction limit
% 12.59/2.68 % (2529192)Termination phase: Saturation
% 12.59/2.68 % (2529192)Time elapsed: 0.509 s
% 12.59/2.68 % (2529192)Peak memory usage: 95 MB
% 12.59/2.68 % (2529192)Instructions burned: 908 (million)
% 12.59/2.68 % (2529201)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1591839231:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 12.59/2.68 % (2529201)Refutation not found, incomplete strategy
% 12.59/2.68 % (2529201)------------------------------
% 12.59/2.68 % (2529201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.68 % (2529201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.68 % (2529201)CaDiCaL version: 2.1.3
% 12.59/2.68 % (2529201)Termination reason: Refutation not found, incomplete strategy
% 12.59/2.68 % (2529201)Time elapsed: 0.002 s
% 12.59/2.68 % (2529201)Peak memory usage: 88 MB
% 12.59/2.68 % (2529201)Instructions burned: 1 (million)
% 12.59/2.68 % (2529202)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=693806285:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 12.59/2.68 % (2529161)Refutation found. Thanks to Tanya!
% 12.59/2.68 % SZS status Theorem for theBenchmark
% 12.59/2.68 % SZS output start Proof for theBenchmark
% See solution above
% 13.41/2.79 % (2529161)------------------------------
% 13.41/2.79 % (2529161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.41/2.79 % (2529161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.41/2.79 % (2529161)CaDiCaL version: 2.1.3
% 13.41/2.79 % (2529161)Termination reason: Refutation
% 13.41/2.79 % (2529161)Time elapsed: 1.398 s
% 13.41/2.79 % (2529161)Peak memory usage: 141 MB
% 13.41/2.79 % (2529161)Instructions burned: 2185 (million)
% 13.41/2.79 % (2529161)------------------------------
% 13.41/2.79 % (2529161)------------------------------
% 13.41/2.79 % (2529156)Success in time 1.834 s
% 13.41/2.79 % Vampire exiting
%------------------------------------------------------------------------------