%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ARI698_1 : TPTP v9.3.1. Released v6.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:33:41 AM UTC 2026
% Result : Theorem 1.89s 0.75s
% Output : Refutation 2.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 24
% Syntax : Number of formulae : 98 ( 81 unt; 0 typ; 12 def)
% Number of atoms : 135 ( 110 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 56 ( 19 ~; 15 |; 10 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number arithmetic : 892 ( 0 atm; 642 fun; 240 num; 10 var)
% Number of types : 1 ( 0 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 14 ( 12 usr; 13 prp; 0-2 aty)
% Number of functors : 14 ( 7 usr; 10 con; 0-2 aty)
% Number of variables : 10 ( 10 !; 0 ?; 10 :)
% Comments :
%------------------------------------------------------------------------------
tff(func_def_0,type,
n: $int ).
tff(func_def_1,type,
x6: $int ).
tff(func_def_2,type,
x5: $int ).
tff(func_def_3,type,
x4: $int ).
tff(func_def_4,type,
x3: $int ).
tff(func_def_5,type,
x2: $int ).
tff(func_def_6,type,
x1: $int ).
tff(f1,axiom,
n = 1000,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq1) ).
tff(f2,axiom,
$sum($sum($sum($sum($sum($product(1,x6),$product(n,x5)),$product(n,x4)),$product(n,x3)),$product(n,x2)),$product(n,x1)) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq2) ).
tff(f3,axiom,
$difference($difference($difference($difference($difference($product(n,x6),x5),x4),x3),x2),x1) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq3) ).
tff(f4,axiom,
$difference($difference($difference($difference($sum($product(n,x6),$product(1,x5)),x4),x3),x2),x1) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq4) ).
tff(f7,axiom,
$difference($difference($difference($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),x3),x2),x1) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq7) ).
tff(f8,axiom,
$difference($difference($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),x2),x1) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq8) ).
tff(f10,axiom,
$sum($difference($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),x2),$product(1,x1)) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',eq10) ).
tff(f12,conjecture,
( ( x1 = 0 )
& ( x3 = 0 )
& ( x2 = 0 )
& ( x6 = 0 )
& ( x5 = 0 )
& ( x4 = 0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj) ).
tff(f13,negated_conjecture,
~ ( ( x1 = 0 )
& ( x3 = 0 )
& ( x2 = 0 )
& ( x6 = 0 )
& ( x5 = 0 )
& ( x4 = 0 ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
tff(f14,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(theory_normalization,[],[f7]) ).
tff(f15,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1)),
inference(theory_normalization,[],[f10]) ).
tff(f16,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(theory_normalization,[],[f4]) ).
tff(f18,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1)),
inference(theory_normalization,[],[f8]) ).
tff(f19,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$uminus(x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(theory_normalization,[],[f3]) ).
tff(f21,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f22,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum($sum(X0,X1),X2) = $sum(X0,$sum(X1,X2)) ),
introduced(definition,[],[tha_associativity]) ).
tff(f24,plain,
! [X0: $int,X1: $int] : ( $uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0)) ),
introduced(definition,[],[tha_inverse_op_op_inverses]) ).
tff(f36,plain,
! [X2: $int,X0: $int,X1: $int] : ( $sum($product(X0,X1),$product(X0,X2)) = $product(X0,$sum(X1,X2)) ),
introduced(definition,[],[tha_distributivity]) ).
tff(f39,plain,
( ( x2 != 0 )
| ( x3 != 0 )
| ( x1 != 0 )
| ( x4 != 0 )
| ( x6 != 0 )
| ( x5 != 0 ) ),
inference(ennf_transformation,[],[f13]) ).
tff(f40,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$uminus(x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(cnf_transformation,[],[f19]) ).
tff(f41,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(cnf_transformation,[],[f14]) ).
tff(f42,plain,
( ( x4 != 0 )
| ( x1 != 0 )
| ( x6 != 0 )
| ( x5 != 0 )
| ( x3 != 0 )
| ( x2 != 0 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f44,plain,
n = 1000,
inference(cnf_transformation,[],[f1]) ).
tff(f46,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(cnf_transformation,[],[f16]) ).
tff(f47,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1)),
inference(cnf_transformation,[],[f15]) ).
tff(f48,plain,
$sum($sum($sum($sum($sum($product(1,x6),$product(n,x5)),$product(n,x4)),$product(n,x3)),$product(n,x2)),$product(n,x1)) = 0,
inference(cnf_transformation,[],[f2]) ).
tff(f51,plain,
0 = $sum($sum($sum($sum($sum($product(n,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1)),
inference(cnf_transformation,[],[f18]) ).
tff(f52,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),$uminus(x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(definition_unfolding,[],[f40,f44]) ).
tff(f53,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(definition_unfolding,[],[f41,f44]) ).
tff(f56,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(1,x5)),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(definition_unfolding,[],[f46,f44]) ).
tff(f57,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(0,x3)),$uminus(x2)),$product(1,x1)),
inference(definition_unfolding,[],[f47,f44]) ).
tff(f58,plain,
0 = $sum($sum($sum($sum($sum($product(1,x6),$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$product(1000,x2)),$product(1000,x1)),
inference(definition_unfolding,[],[f48,f44,f44,f44,f44,f44]) ).
tff(f61,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),$product(0,x5)),$product(0,x4)),$product(1,x3)),$uminus(x2)),$uminus(x1)),
inference(definition_unfolding,[],[f51,f44]) ).
tff(f65,plain,
0 = $sum($sum($sum($product(1000,x6),x3),$uminus(x2)),$uminus(x1)),
inference(evaluation,[],[f61]) ).
tff(f66,plain,
0 = $sum($sum($product(1000,x6),$uminus(x2)),x1),
inference(evaluation,[],[f57]) ).
tff(f67,plain,
0 = $sum($sum($sum($product(1000,x6),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(evaluation,[],[f53]) ).
tff(f68,plain,
0 = $sum($sum($sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$product(1000,x2)),$product(1000,x1)),
inference(evaluation,[],[f58]) ).
tff(f71,plain,
0 = $sum($sum($sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3)),$uminus(x2)),$uminus(x1)),
inference(evaluation,[],[f56]) ).
tff(f74,plain,
0 = $sum($sum($product(1000,x6),x3),$sum($uminus(x2),$uminus(x1))),
inference(forward_demodulation,[],[f65,f22]) ).
tff(f75,plain,
0 = $sum($sum($sum($sum($product(1000,x6),$uminus(x5)),$uminus(x4)),$uminus(x3)),$sum($uminus(x2),$uminus(x1))),
inference(forward_demodulation,[],[f52,f22]) ).
tff(f76,plain,
0 = $sum($product(1000,x6),$sum($uminus(x2),x1)),
inference(forward_demodulation,[],[f66,f22]) ).
tff(f77,plain,
0 = $sum($sum($product(1000,x6),$uminus(x3)),$sum($uminus(x2),$uminus(x1))),
inference(forward_demodulation,[],[f67,f22]) ).
tff(f78,plain,
0 = $sum($sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$product(1000,x3)),$sum($product(1000,x2),$product(1000,x1))),
inference(forward_demodulation,[],[f68,f22]) ).
tff(f80,definition,
( spl0_1
<=> ( x1 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
tff(f84,definition,
( spl0_2
<=> ( x6 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
tff(f88,definition,
( spl0_3
<=> ( x5 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
tff(f92,definition,
( spl0_4
<=> ( x3 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
tff(f96,definition,
( spl0_5
<=> ( x2 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
tff(f100,definition,
( spl0_6
<=> ( x4 = 0 ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
tff(f103,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f42,f100,f96,f92,f88,f84,f80]) ).
tff(f106,plain,
0 = $sum($sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$uminus(x3)),$sum($uminus(x2),$uminus(x1))),
inference(forward_demodulation,[],[f71,f22]) ).
tff(f109,plain,
0 = $sum($product(1000,x6),$sum(x3,$sum($uminus(x2),$uminus(x1)))),
inference(forward_demodulation,[],[f74,f22]) ).
tff(f110,plain,
0 = $sum($sum($sum($product(1000,x6),$uminus(x5)),$uminus(x4)),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1)))),
inference(forward_demodulation,[],[f75,f22]) ).
tff(f111,plain,
0 = $sum($product(1000,x6),$sum(x1,$uminus(x2))),
inference(forward_demodulation,[],[f76,f21]) ).
tff(f112,plain,
0 = $sum($product(1000,x6),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1)))),
inference(forward_demodulation,[],[f77,f22]) ).
tff(f113,plain,
0 = $sum($sum($sum(x6,$product(1000,x5)),$product(1000,x4)),$sum($product(1000,x3),$sum($product(1000,x2),$product(1000,x1)))),
inference(forward_demodulation,[],[f78,f22]) ).
tff(f120,plain,
0 = $sum($sum($sum($product(1000,x6),x5),$uminus(x4)),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1)))),
inference(forward_demodulation,[],[f106,f22]) ).
tff(f123,plain,
0 = $sum($product(1000,x6),$sum(x3,$uminus($sum(x1,x2)))),
inference(forward_demodulation,[],[f109,f24]) ).
tff(f124,plain,
0 = $sum($sum($product(1000,x6),$uminus(x5)),$sum($uminus(x4),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1))))),
inference(forward_demodulation,[],[f110,f22]) ).
tff(f126,definition,
( spl0_8
<=> ( 0 = $sum($product(1000,x6),$sum(x1,$uminus(x2))) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
tff(f129,plain,
spl0_8,
inference(avatar_split_clause,[],[f111,f126]) ).
tff(f130,plain,
0 = $sum($product(1000,x6),$sum($uminus(x3),$uminus($sum(x1,x2)))),
inference(forward_demodulation,[],[f112,f24]) ).
tff(f131,plain,
0 = $sum($sum(x6,$product(1000,x5)),$sum($product(1000,x4),$sum($product(1000,x3),$sum($product(1000,x2),$product(1000,x1))))),
inference(forward_demodulation,[],[f113,f22]) ).
tff(f137,plain,
0 = $sum($sum($product(1000,x6),x5),$sum($uminus(x4),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1))))),
inference(forward_demodulation,[],[f120,f22]) ).
tff(f141,definition,
( spl0_10
<=> ( 0 = $sum($product(1000,x6),$sum(x3,$uminus($sum(x1,x2)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
tff(f144,plain,
spl0_10,
inference(avatar_split_clause,[],[f123,f141]) ).
tff(f145,plain,
0 = $sum($product(1000,x6),$sum($uminus(x5),$sum($uminus(x4),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1)))))),
inference(forward_demodulation,[],[f124,f22]) ).
tff(f146,plain,
0 = $sum($product(1000,x6),$uminus($sum($sum(x1,x2),x3))),
inference(forward_demodulation,[],[f130,f24]) ).
tff(f147,plain,
0 = $sum(x6,$sum($product(1000,x5),$sum($product(1000,x4),$sum($product(1000,x3),$sum($product(1000,x2),$product(1000,x1)))))),
inference(forward_demodulation,[],[f131,f22]) ).
tff(f148,plain,
0 = $sum($product(1000,x6),$sum(x5,$sum($uminus(x4),$sum($uminus(x3),$sum($uminus(x2),$uminus(x1)))))),
inference(forward_demodulation,[],[f137,f22]) ).
tff(f159,plain,
0 = $sum($product(1000,x6),$sum($uminus(x5),$sum($uminus(x4),$sum($uminus(x3),$uminus($sum(x1,x2)))))),
inference(forward_demodulation,[],[f145,f24]) ).
tff(f160,plain,
0 = $sum($product(1000,x6),$uminus($sum(x1,$sum(x2,x3)))),
inference(forward_demodulation,[],[f146,f22]) ).
tff(f161,plain,
0 = $sum(x6,$sum($product(1000,x5),$sum($product(1000,x4),$sum($product(1000,x3),$sum($product(1000,x1),$product(1000,x2)))))),
inference(forward_demodulation,[],[f147,f21]) ).
tff(f162,plain,
0 = $sum($product(1000,x6),$sum(x5,$sum($uminus(x4),$sum($uminus(x3),$uminus($sum(x1,x2)))))),
inference(forward_demodulation,[],[f148,f24]) ).
tff(f163,plain,
0 = $sum($product(1000,x6),$sum($uminus(x5),$sum($uminus(x4),$uminus($sum($sum(x1,x2),x3))))),
inference(forward_demodulation,[],[f159,f24]) ).
tff(f164,plain,
0 = $sum($product(1000,x6),$uminus($sum(x1,$sum(x3,x2)))),
inference(forward_demodulation,[],[f160,f21]) ).
tff(f165,plain,
0 = $sum(x6,$sum($product(1000,x5),$sum($product(1000,x4),$sum($product(1000,x3),$product(1000,$sum(x1,x2)))))),
inference(forward_demodulation,[],[f161,f36]) ).
tff(f166,plain,
0 = $sum($product(1000,x6),$sum(x5,$sum($uminus(x4),$uminus($sum($sum(x1,x2),x3))))),
inference(forward_demodulation,[],[f162,f24]) ).
tff(f167,plain,
0 = $sum($product(1000,x6),$sum($uminus(x5),$uminus($sum($sum($sum(x1,x2),x3),x4)))),
inference(forward_demodulation,[],[f163,f24]) ).
tff(f169,definition,
( spl0_13
<=> ( 0 = $sum($product(1000,x6),$uminus($sum(x1,$sum(x3,x2)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
tff(f172,plain,
spl0_13,
inference(avatar_split_clause,[],[f164,f169]) ).
tff(f173,plain,
0 = $sum(x6,$sum($product(1000,x5),$sum($product(1000,x4),$product(1000,$sum(x3,$sum(x1,x2)))))),
inference(forward_demodulation,[],[f165,f36]) ).
tff(f174,plain,
0 = $sum($product(1000,x6),$sum(x5,$uminus($sum($sum($sum(x1,x2),x3),x4)))),
inference(forward_demodulation,[],[f166,f24]) ).
tff(f175,plain,
0 = $sum($product(1000,x6),$uminus($sum($sum($sum($sum(x1,x2),x3),x4),x5))),
inference(forward_demodulation,[],[f167,f24]) ).
tff(f176,plain,
0 = $sum(x6,$sum($product(1000,x5),$product(1000,$sum(x4,$sum(x3,$sum(x1,x2)))))),
inference(forward_demodulation,[],[f173,f36]) ).
tff(f177,plain,
0 = $sum($product(1000,x6),$sum(x5,$uminus($sum($sum(x1,x2),$sum(x3,x4))))),
inference(forward_demodulation,[],[f174,f22]) ).
tff(f178,plain,
0 = $sum($product(1000,x6),$uminus($sum($sum($sum(x1,x2),x3),$sum(x4,x5)))),
inference(forward_demodulation,[],[f175,f22]) ).
tff(f179,plain,
0 = $sum(x6,$product(1000,$sum(x5,$sum(x4,$sum(x3,$sum(x1,x2)))))),
inference(forward_demodulation,[],[f176,f36]) ).
tff(f180,plain,
0 = $sum($product(1000,x6),$sum(x5,$uminus($sum(x1,$sum(x2,$sum(x3,x4)))))),
inference(forward_demodulation,[],[f177,f22]) ).
tff(f181,plain,
0 = $sum($product(1000,x6),$uminus($sum($sum(x1,x2),$sum(x3,$sum(x4,x5))))),
inference(forward_demodulation,[],[f178,f22]) ).
tff(f183,definition,
( spl0_14
<=> ( 0 = $sum(x6,$product(1000,$sum(x5,$sum(x4,$sum(x3,$sum(x1,x2)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
tff(f186,plain,
spl0_14,
inference(avatar_split_clause,[],[f179,f183]) ).
tff(f188,definition,
( spl0_15
<=> ( 0 = $sum($product(1000,x6),$sum(x5,$uminus($sum(x1,$sum(x2,$sum(x3,x4)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
tff(f191,plain,
spl0_15,
inference(avatar_split_clause,[],[f180,f188]) ).
tff(f192,plain,
0 = $sum($product(1000,x6),$uminus($sum(x1,$sum(x2,$sum(x3,$sum(x4,x5)))))),
inference(forward_demodulation,[],[f181,f22]) ).
tff(f194,definition,
( spl0_16
<=> ( 0 = $sum($product(1000,x6),$uminus($sum(x1,$sum(x2,$sum(x3,$sum(x4,x5)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
tff(f197,plain,
spl0_16,
inference(avatar_split_clause,[],[f192,f194]) ).
tff(f198,plain,
$false,
inference(avatar_smt_refutation,[],[f197,f191,f186,f172,f144,f129,f103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI698_1 : TPTP v9.3.1. Released v6.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 20:55:36 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 1.89/0.75 % (2813789)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 1.89/0.75 % (2813866)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3343722195:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 1.89/0.75 % (2813866)First to succeed.
% 1.89/0.75 % (2813866)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2813789"
% 1.89/0.75 % (2813863)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=4202955695:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 1.89/0.75 % (2813860)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1744567996:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 1.89/0.75 % (2813859)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3103861761:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 1.89/0.75 % (2813858)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=2055843404:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 1.89/0.75 % (2813863)Instruction limit reached!
% 1.89/0.75 % (2813863)------------------------------
% 1.89/0.75 % (2813863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/0.75 % (2813863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.75 % (2813863)CaDiCaL version: 2.1.3
% 1.89/0.75 % (2813863)Termination reason: Instruction limit
% 1.89/0.75 % (2813863)Termination phase: Saturation
% 1.89/0.75 % (2813863)Time elapsed: 0.005 s
% 1.89/0.75 % (2813863)Peak memory usage: 88 MB
% 1.89/0.75 % (2813863)Instructions burned: 5 (million)
% 1.89/0.75 % (2813864)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=264611180:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 1.89/0.75 % (2813862)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2046637358:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 1.89/0.75 % (2813862)Instruction limit reached!
% 1.89/0.75 % (2813862)------------------------------
% 1.89/0.75 % (2813862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/0.75 % (2813862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.75 % (2813862)CaDiCaL version: 2.1.3
% 1.89/0.75 % (2813862)Termination reason: Instruction limit
% 1.89/0.75 % (2813862)Termination phase: Saturation
% 1.89/0.75 % (2813862)Time elapsed: 0.005 s
% 1.89/0.75 % (2813862)Peak memory usage: 88 MB
% 1.89/0.75 % (2813862)Instructions burned: 8 (million)
% 1.89/0.75 % (2813859)Also succeeded, but the first one will report.
% 1.89/0.75 % (2813858)Refutation not found, incomplete strategy
% 1.89/0.75 % (2813858)------------------------------
% 1.89/0.75 % (2813858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/0.75 % (2813858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.75 % (2813858)CaDiCaL version: 2.1.3
% 1.89/0.75 % (2813858)Termination reason: Refutation not found, incomplete strategy
% 1.89/0.75 % (2813858)Time elapsed: 0.035 s
% 1.89/0.75 % (2813858)Peak memory usage: 115 MB
% 1.89/0.75 % (2813858)Instructions burned: 9 (million)
% 1.89/0.75 % (2813864)Also succeeded, but the first one will report.
% 1.89/0.75 % (2813860)Instruction limit reached!
% 1.89/0.75 % (2813860)------------------------------
% 1.89/0.75 % (2813860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.89/0.75 % (2813860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.75 % (2813860)CaDiCaL version: 2.1.3
% 1.89/0.75 % (2813860)Termination reason: Instruction limit
% 1.89/0.75 % (2813860)Termination phase: Saturation
% 1.89/0.75 % (2813860)Time elapsed: 0.154 s
% 1.89/0.75 % (2813860)Peak memory usage: 114 MB
% 1.89/0.75 % (2813860)Instructions burned: 202 (million)
% 1.89/0.75 % (2813866)Refutation found. Thanks to Tanya!
% 1.89/0.75 % SZS status Theorem for theBenchmark
% 1.89/0.75 % SZS output start Proof for theBenchmark
% See solution above
% 2.52/0.88 % (2813866)------------------------------
% 2.52/0.88 % (2813866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.52/0.88 % (2813866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.52/0.88 % (2813866)CaDiCaL version: 2.1.3
% 2.52/0.88 % (2813866)Termination reason: Refutation
% 2.52/0.88 % (2813866)Time elapsed: 0.025 s
% 2.52/0.88 % (2813866)Peak memory usage: 116 MB
% 2.52/0.88 % (2813866)Instructions burned: 24 (million)
% 2.52/0.88 % (2813866)------------------------------
% 2.52/0.88 % (2813866)------------------------------
% 2.52/0.88 % (2813789)Success in time 0.318 s
% 2.52/0.88 % Vampire exiting
%------------------------------------------------------------------------------