%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM339+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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 12:12:12 PM UTC 2026
% Result : Theorem 8.64s 2.70s
% Output : Refutation 12.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 19
% Syntax : Number of formulae : 77 ( 29 unt; 0 def)
% Number of atoms : 240 ( 0 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 337 ( 174 ~; 145 |; 11 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 210 ( 208 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
rdn_translate(n1,rdn_pos(rdnn(n1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn1) ).
fof(f255,axiom,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdnn127) ).
fof(f256,axiom,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdnn128) ).
fof(f257,axiom,
rdn_non_zero_digit(rdnn(n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit1) ).
fof(f278,axiom,
! [X0,X1,X2] :
( rdn_non_zero(X2)
=> rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_extra_digits_positive_less) ).
fof(f279,axiom,
! [X0] :
( rdn_non_zero_digit(rdnn(X0))
=> rdn_non_zero(rdnn(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_non_zero_by_digit) ).
fof(f280,axiom,
! [X0,X1] :
( rdn_non_zero(X1)
=> rdn_non_zero(rdn(rdnn(X0),X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_non_zero_by_structure) ).
fof(f289,axiom,
! [X0,X1,X2,X3,X4,X5] :
( ( rdn_translate(X0,rdn_pos(X3))
& rdn_translate(X1,rdn_neg(X4))
& rdn_positive_less(X3,X4)
& rdn_add_with_carry(rdnn(n0),X3,X5,X4)
& rdn_translate(X2,rdn_neg(X5)) )
=> sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_entry_point_pos_neg_1) ).
fof(f296,axiom,
! [X0,X1,X2] :
( sum(X1,X2,X0)
<=> difference(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',minus_entry_point) ).
fof(f297,axiom,
! [X0,X1,X2,X3,X4] :
( ( rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
& rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) )
=> rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_digit_digit_digit) ).
fof(f299,axiom,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ( rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X6),rdnn(X7))
& rdn_digit_add(rdnn(X6),rdnn(X0),rdnn(X4),rdnn(X8))
& rdn_digit_add(rdnn(X7),rdnn(X8),rdnn(X9),rdnn(n0))
& rdn_add_with_carry(rdnn(X9),rdnn(n0),X3,X5)
& rdn_non_zero(X3)
& rdn_non_zero(X5) )
=> rdn_add_with_carry(rdnn(X0),rdnn(X1),rdn(rdnn(X2),X3),rdn(rdnn(X4),X5)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_digit_rdn_rdn) ).
fof(f302,axiom,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n0_n0_n0_n0) ).
fof(f303,axiom,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n0_n1_n1_n0) ).
fof(f304,axiom,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n0_n2_n2_n0) ).
fof(f312,axiom,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n1_n0_n1_n0) ).
fof(f319,axiom,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n1_n7_n8_n0) ).
fof(f322,axiom,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n2_n0_n2_n0) ).
fof(f382,axiom,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdn_digit_add_n8_n0_n8_n0) ).
fof(f402,conjecture,
? [X0] : difference(nn127,n1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',show_lower_boundary) ).
fof(f403,negated_conjecture,
~ ? [X0] : difference(nn127,n1,X0),
inference(negated_conjecture,[status(cth)],[f402]) ).
fof(f410,plain,
! [X0,X1,X2] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(ennf_transformation,[],[f278]) ).
fof(f411,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(ennf_transformation,[],[f279]) ).
fof(f412,plain,
! [X0,X1] :
( rdn_non_zero(rdn(rdnn(X0),X1))
| ~ rdn_non_zero(X1) ),
inference(ennf_transformation,[],[f280]) ).
fof(f427,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X0,X1,X2)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_neg(X4))
| ~ rdn_positive_less(X3,X4)
| ~ rdn_add_with_carry(rdnn(n0),X3,X5,X4)
| ~ rdn_translate(X2,rdn_neg(X5)) ),
inference(ennf_transformation,[],[f289]) ).
fof(f428,plain,
! [X0,X1,X2,X3,X4,X5] :
( sum(X0,X1,X2)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_neg(X4))
| ~ rdn_positive_less(X3,X4)
| ~ rdn_add_with_carry(rdnn(n0),X3,X5,X4)
| ~ rdn_translate(X2,rdn_neg(X5)) ),
inference(flattening,[],[f427]) ).
fof(f441,plain,
! [X0,X1,X2,X3,X4] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) ),
inference(ennf_transformation,[],[f297]) ).
fof(f442,plain,
! [X0,X1,X2,X3,X4] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) ),
inference(flattening,[],[f441]) ).
fof(f445,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdn(rdnn(X2),X3),rdn(rdnn(X4),X5))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X6),rdnn(X7))
| ~ rdn_digit_add(rdnn(X6),rdnn(X0),rdnn(X4),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X8),rdnn(X9),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X9),rdnn(n0),X3,X5)
| ~ rdn_non_zero(X3)
| ~ rdn_non_zero(X5) ),
inference(ennf_transformation,[],[f299]) ).
fof(f446,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdn(rdnn(X2),X3),rdn(rdnn(X4),X5))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X6),rdnn(X7))
| ~ rdn_digit_add(rdnn(X6),rdnn(X0),rdnn(X4),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X8),rdnn(X9),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X9),rdnn(n0),X3,X5)
| ~ rdn_non_zero(X3)
| ~ rdn_non_zero(X5) ),
inference(flattening,[],[f445]) ).
fof(f450,plain,
! [X0] : ~ difference(nn127,n1,X0),
inference(ennf_transformation,[],[f403]) ).
fof(f453,plain,
! [X0,X1,X2] :
( ( sum(X1,X2,X0)
| ~ difference(X0,X1,X2) )
& ( difference(X0,X1,X2)
| ~ sum(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f296]) ).
fof(f455,plain,
rdn_translate(n1,rdn_pos(rdnn(n1))),
inference(cnf_transformation,[],[f2]) ).
fof(f708,plain,
rdn_translate(nn127,rdn_neg(rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))))),
inference(cnf_transformation,[],[f255]) ).
fof(f709,plain,
rdn_translate(nn128,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(cnf_transformation,[],[f256]) ).
fof(f710,plain,
rdn_non_zero_digit(rdnn(n1)),
inference(cnf_transformation,[],[f257]) ).
fof(f731,plain,
! [X2,X0,X1] :
( rdn_positive_less(rdnn(X0),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2) ),
inference(cnf_transformation,[],[f410]) ).
fof(f732,plain,
! [X0] :
( rdn_non_zero(rdnn(X0))
| ~ rdn_non_zero_digit(rdnn(X0)) ),
inference(cnf_transformation,[],[f411]) ).
fof(f733,plain,
! [X0,X1] :
( rdn_non_zero(rdn(rdnn(X0),X1))
| ~ rdn_non_zero(X1) ),
inference(cnf_transformation,[],[f412]) ).
fof(f744,plain,
! [X2,X3,X0,X1,X4,X5] :
( sum(X0,X1,X2)
| ~ rdn_translate(X0,rdn_pos(X3))
| ~ rdn_translate(X1,rdn_neg(X4))
| ~ rdn_positive_less(X3,X4)
| ~ rdn_add_with_carry(rdnn(n0),X3,X5,X4)
| ~ rdn_translate(X2,rdn_neg(X5)) ),
inference(cnf_transformation,[],[f428]) ).
fof(f751,plain,
! [X2,X0,X1] :
( difference(X0,X1,X2)
| ~ sum(X1,X2,X0) ),
inference(cnf_transformation,[],[f453]) ).
fof(f753,plain,
! [X2,X3,X0,X1,X4] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_digit_add(rdnn(X4),rdnn(X0),rdnn(X3),rdnn(n0)) ),
inference(cnf_transformation,[],[f442]) ).
fof(f755,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( rdn_add_with_carry(rdnn(X0),rdnn(X1),rdn(rdnn(X2),X3),rdn(rdnn(X4),X5))
| ~ rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(X6),rdnn(X7))
| ~ rdn_digit_add(rdnn(X6),rdnn(X0),rdnn(X4),rdnn(X8))
| ~ rdn_digit_add(rdnn(X7),rdnn(X8),rdnn(X9),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X9),rdnn(n0),X3,X5)
| ~ rdn_non_zero(X3)
| ~ rdn_non_zero(X5) ),
inference(cnf_transformation,[],[f446]) ).
fof(f758,plain,
rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),
inference(cnf_transformation,[],[f302]) ).
fof(f759,plain,
rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(n1),rdnn(n0)),
inference(cnf_transformation,[],[f303]) ).
fof(f760,plain,
rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(n2),rdnn(n0)),
inference(cnf_transformation,[],[f304]) ).
fof(f768,plain,
rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(n1),rdnn(n0)),
inference(cnf_transformation,[],[f312]) ).
fof(f775,plain,
rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(n8),rdnn(n0)),
inference(cnf_transformation,[],[f319]) ).
fof(f778,plain,
rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(n2),rdnn(n0)),
inference(cnf_transformation,[],[f322]) ).
fof(f838,plain,
rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(n8),rdnn(n0)),
inference(cnf_transformation,[],[f382]) ).
fof(f858,plain,
! [X0] : ~ difference(nn127,n1,X0),
inference(cnf_transformation,[],[f450]) ).
fof(f859,plain,
! [X0] : ~ sum(n1,X0,nn127),
inference(resolution,[],[f858,f751]) ).
fof(f862,plain,
! [X2,X3,X0,X1] :
( ~ rdn_translate(nn127,rdn_neg(X3))
| ~ rdn_translate(X1,rdn_neg(X2))
| ~ rdn_positive_less(X0,X2)
| ~ rdn_add_with_carry(rdnn(n0),X0,X3,X2)
| ~ rdn_translate(n1,rdn_pos(X0)) ),
inference(resolution,[],[f859,f744]) ).
fof(f869,plain,
! [X2,X0,X1] :
( ~ rdn_translate(n1,rdn_pos(X2))
| ~ rdn_positive_less(X2,X1)
| ~ rdn_add_with_carry(rdnn(n0),X2,rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))),X1)
| ~ rdn_translate(X0,rdn_neg(X1)) ),
inference(resolution,[],[f862,f708]) ).
fof(f873,plain,
! [X0,X1] :
( ~ rdn_add_with_carry(rdnn(n0),rdnn(n1),rdn(rdnn(n7),rdn(rdnn(n2),rdnn(n1))),X0)
| ~ rdn_positive_less(rdnn(n1),X0)
| ~ rdn_translate(X1,rdn_neg(X0)) ),
inference(resolution,[],[f869,f455]) ).
fof(f874,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_non_zero(rdn(rdnn(n2),rdnn(n1)))
| ~ rdn_translate(X2,rdn_neg(rdn(rdnn(X0),X1)))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X0),rdnn(X5))
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X1)
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X0),X1))
| ~ rdn_non_zero(X1) ),
inference(resolution,[],[f873,f755]) ).
fof(f878,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_non_zero(rdnn(n1))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X3),rdnn(X4))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X1),X2))
| ~ rdn_non_zero(X2)
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(X1),X2))) ),
inference(resolution,[],[f874,f733]) ).
fof(f880,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_non_zero_digit(rdnn(n1))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X4),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X4),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X5)
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X2),X5))
| ~ rdn_non_zero(X5)
| ~ rdn_translate(X6,rdn_neg(rdn(rdnn(X2),X5)))
| ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X0),rdnn(X1)) ),
inference(resolution,[],[f878,f732]) ).
fof(f887,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_digit_add(rdnn(n1),rdnn(n7),rdnn(X0),rdnn(X3))
| ~ rdn_digit_add(rdnn(X3),rdnn(X2),rdnn(X4),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X4),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X5)
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X1),X5))
| ~ rdn_non_zero(X5)
| ~ rdn_translate(X6,rdn_neg(rdn(rdnn(X1),X5)))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(X1),rdnn(X2)) ),
inference(resolution,[],[f880,f710]) ).
fof(f893,plain,
! [X2,X3,X0,X1,X4] :
( ~ rdn_digit_add(rdnn(n8),rdnn(n0),rdnn(X3),rdnn(X0))
| ~ rdn_add_with_carry(rdnn(X1),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X2)
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(X3),X2))
| ~ rdn_non_zero(X2)
| ~ rdn_translate(X4,rdn_neg(rdn(rdnn(X3),X2)))
| ~ rdn_digit_add(rdnn(n0),rdnn(X0),rdnn(X1),rdnn(n0)) ),
inference(resolution,[],[f887,f775]) ).
fof(f895,plain,
! [X2,X0,X1] :
( ~ rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(X0),rdnn(n0))
| ~ rdn_positive_less(rdnn(n1),rdn(rdnn(n8),X1))
| ~ rdn_non_zero(X1)
| ~ rdn_translate(X2,rdn_neg(rdn(rdnn(n8),X1)))
| ~ rdn_add_with_carry(rdnn(X0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X1) ),
inference(resolution,[],[f893,f838]) ).
fof(f897,plain,
! [X0,X1] :
( ~ rdn_positive_less(rdnn(n1),rdn(rdnn(n8),X0))
| ~ rdn_non_zero(X0)
| ~ rdn_translate(X1,rdn_neg(rdn(rdnn(n8),X0)))
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X0) ),
inference(resolution,[],[f895,f758]) ).
fof(f898,plain,
! [X0,X1] :
( ~ rdn_non_zero(X0)
| ~ rdn_translate(X1,rdn_neg(rdn(rdnn(n8),X0)))
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X0)
| ~ rdn_non_zero(X0) ),
inference(resolution,[],[f897,f731]) ).
fof(f899,plain,
! [X0,X1] :
( ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdn(rdnn(n2),rdnn(n1)),X0)
| ~ rdn_translate(X1,rdn_neg(rdn(rdnn(n8),X0)))
| ~ rdn_non_zero(X0) ),
inference(duplicate_literal_removal,[],[f898]) ).
fof(f902,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_non_zero(rdnn(n1))
| ~ rdn_non_zero(rdn(rdnn(X1),X2))
| ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X3),rdnn(X4))
| ~ rdn_digit_add(rdnn(X3),rdnn(n0),rdnn(X1),rdnn(X5))
| ~ rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(X6),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X6),rdnn(n0),rdnn(n1),X2)
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(X1),X2))))
| ~ rdn_non_zero(X2) ),
inference(resolution,[],[f899,f755]) ).
fof(f904,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_non_zero_digit(rdnn(n1))
| ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X2),rdnn(n0),rdnn(X0),rdnn(X4))
| ~ rdn_digit_add(rdnn(X3),rdnn(X4),rdnn(X5),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X5),rdnn(n0),rdnn(n1),X1)
| ~ rdn_translate(X6,rdn_neg(rdn(rdnn(n8),rdn(rdnn(X0),X1))))
| ~ rdn_non_zero(X1)
| ~ rdn_non_zero(rdn(rdnn(X0),X1)) ),
inference(resolution,[],[f902,f732]) ).
fof(f907,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ rdn_digit_add(rdnn(n0),rdnn(n2),rdnn(X0),rdnn(X1))
| ~ rdn_digit_add(rdnn(X0),rdnn(n0),rdnn(X2),rdnn(X3))
| ~ rdn_digit_add(rdnn(X1),rdnn(X3),rdnn(X4),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X4),rdnn(n0),rdnn(n1),X5)
| ~ rdn_translate(X6,rdn_neg(rdn(rdnn(n8),rdn(rdnn(X2),X5))))
| ~ rdn_non_zero(X5)
| ~ rdn_non_zero(rdn(rdnn(X2),X5)) ),
inference(resolution,[],[f904,f710]) ).
fof(f909,plain,
! [X2,X3,X0,X1,X4] :
( ~ rdn_digit_add(rdnn(n2),rdnn(n0),rdnn(X0),rdnn(X1))
| ~ rdn_digit_add(rdnn(n0),rdnn(X1),rdnn(X2),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X2),rdnn(n0),rdnn(n1),X3)
| ~ rdn_translate(X4,rdn_neg(rdn(rdnn(n8),rdn(rdnn(X0),X3))))
| ~ rdn_non_zero(X3)
| ~ rdn_non_zero(rdn(rdnn(X0),X3)) ),
inference(resolution,[],[f907,f760]) ).
fof(f912,plain,
! [X2,X0,X1] :
( ~ rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(X0),rdnn(n0))
| ~ rdn_add_with_carry(rdnn(X0),rdnn(n0),rdnn(n1),X1)
| ~ rdn_translate(X2,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),X1))))
| ~ rdn_non_zero(X1)
| ~ rdn_non_zero(rdn(rdnn(n2),X1)) ),
inference(resolution,[],[f909,f778]) ).
fof(f914,plain,
! [X0,X1] :
( ~ rdn_non_zero(rdn(rdnn(n2),X0))
| ~ rdn_translate(X1,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),X0))))
| ~ rdn_non_zero(X0)
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdnn(n1),X0) ),
inference(resolution,[],[f912,f758]) ).
fof(f916,plain,
! [X0,X1] :
( ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),X1))))
| ~ rdn_non_zero(X1)
| ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdnn(n1),X1)
| ~ rdn_non_zero(X1) ),
inference(resolution,[],[f914,f733]) ).
fof(f917,plain,
! [X0,X1] :
( ~ rdn_add_with_carry(rdnn(n0),rdnn(n0),rdnn(n1),X1)
| ~ rdn_non_zero(X1)
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),X1)))) ),
inference(duplicate_literal_removal,[],[f916]) ).
fof(f919,plain,
! [X2,X0,X1] :
( ~ rdn_digit_add(rdnn(n0),rdnn(n1),rdnn(X2),rdnn(n0))
| ~ rdn_translate(X1,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(X0)))))
| ~ rdn_non_zero(rdnn(X0))
| ~ rdn_digit_add(rdnn(X2),rdnn(n0),rdnn(X0),rdnn(n0)) ),
inference(resolution,[],[f917,f753]) ).
fof(f922,plain,
! [X0,X1] :
( ~ rdn_digit_add(rdnn(n1),rdnn(n0),rdnn(X1),rdnn(n0))
| ~ rdn_non_zero(rdnn(X1))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(X1))))) ),
inference(resolution,[],[f919,f759]) ).
fof(f927,plain,
! [X0] :
( ~ rdn_non_zero(rdnn(n1))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))) ),
inference(resolution,[],[f922,f768]) ).
fof(f929,plain,
! [X0] :
( ~ rdn_non_zero_digit(rdnn(n1))
| ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))) ),
inference(resolution,[],[f927,f732]) ).
fof(f931,plain,
! [X0] : ~ rdn_translate(X0,rdn_neg(rdn(rdnn(n8),rdn(rdnn(n2),rdnn(n1))))),
inference(resolution,[],[f929,f710]) ).
fof(f936,plain,
$false,
inference(resolution,[],[f931,f709]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM339+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.44 % Computer : n016.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 27 19:40:03 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 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
% 7.94/2.27 % (2948881)Detected formulas, will run a generic FOF schedule.
% 7.94/2.27 % (2948895)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=185578322:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.94/2.27 % (2948898)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3964943688:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.94/2.27 % (2948898)Refutation not found, incomplete strategy
% 7.94/2.27 % (2948898)------------------------------
% 7.94/2.27 % (2948898)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.27 % (2948898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.27 % (2948898)CaDiCaL version: 2.1.3
% 7.94/2.27 % (2948898)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.27 % (2948898)Time elapsed: 0.004 s
% 7.94/2.27 % (2948898)Peak memory usage: 88 MB
% 7.94/2.27 % (2948898)Instructions burned: 2 (million)
% 7.94/2.27 % (2948894)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=2046368355:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.94/2.27 % (2948899)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=204503940:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.94/2.27 % (2948900)dis-21_1_sil=8000:lcm=predicate:random_seed=545320001: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)
% 7.94/2.27 % (2948897)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3070906542:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.94/2.27 % (2948896)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=618854624:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.94/2.27 % (2948897)Refutation not found, incomplete strategy
% 7.94/2.27 % (2948897)------------------------------
% 7.94/2.27 % (2948897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.27 % (2948897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.27 % (2948897)CaDiCaL version: 2.1.3
% 7.94/2.27 % (2948897)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.27 % (2948897)Time elapsed: 0.002 s
% 7.94/2.27 % (2948897)Peak memory usage: 87 MB
% 7.94/2.27 % (2948897)Instructions burned: 1 (million)
% 7.94/2.27 % (2948900)Instruction limit reached!
% 7.94/2.27 % (2948900)------------------------------
% 7.94/2.27 % (2948900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.27 % (2948900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.27 % (2948900)CaDiCaL version: 2.1.3
% 7.94/2.27 % (2948900)Termination reason: Instruction limit
% 7.94/2.27 % (2948900)Termination phase: Saturation
% 7.94/2.27 % (2948900)Time elapsed: 0.094 s
% 7.94/2.27 % (2948900)Peak memory usage: 88 MB
% 7.94/2.27 % (2948900)Instructions burned: 129 (million)
% 7.94/2.27 % (2948899)Instruction limit reached!
% 7.94/2.27 % (2948899)------------------------------
% 7.94/2.27 % (2948899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.27 % (2948899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.27 % (2948899)CaDiCaL version: 2.1.3
% 7.94/2.27 % (2948899)Termination reason: Instruction limit
% 7.94/2.27 % (2948899)Termination phase: Saturation
% 7.94/2.27 % (2948899)Time elapsed: 0.129 s
% 7.94/2.27 % (2948899)Peak memory usage: 89 MB
% 7.94/2.27 % (2948899)Instructions burned: 139 (million)
% 7.94/2.27 % (2948909)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3276171252:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 7.94/2.27 % (2948909)Refutation not found, incomplete strategy
% 7.94/2.27 % (2948909)------------------------------
% 7.94/2.27 % (2948909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.94/2.27 % (2948909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/2.27 % (2948909)CaDiCaL version: 2.1.3
% 7.94/2.27 % (2948909)Termination reason: Refutation not found, incomplete strategy
% 7.94/2.27 % (2948909)Time elapsed: 0.003 s
% 7.94/2.27 % (2948909)Peak memory usage: 87 MB
% 7.94/2.27 % (2948909)Instructions burned: 5 (million)
% 8.64/2.70 % (2948908)lrs+10_1_sil=8000:sp=occurrence:random_seed=832625161:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 8.64/2.70 % (2948908)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948908)------------------------------
% 8.64/2.70 % (2948908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948908)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948908)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948908)Time elapsed: 0.004 s
% 8.64/2.70 % (2948908)Peak memory usage: 88 MB
% 8.64/2.70 % (2948908)Instructions burned: 2 (million)
% 8.64/2.70 % (2948898)------------------------------
% 8.64/2.70 % (2948898)------------------------------
% 8.64/2.70 % (2948897)------------------------------
% 8.64/2.70 % (2948897)------------------------------
% 8.64/2.70 % (2948895)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948895)------------------------------
% 8.64/2.70 % (2948895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948895)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948895)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948895)Time elapsed: 0.477 s
% 8.64/2.70 % (2948895)Peak memory usage: 129 MB
% 8.64/2.70 % (2948895)Instructions burned: 910 (million)
% 8.64/2.70 % (2948913)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=3834046535:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 8.64/2.70 % (2948912)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3589363828:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 8.64/2.70 % (2948912)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948912)------------------------------
% 8.64/2.70 % (2948912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948912)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948912)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948912)Time elapsed: 0.002 s
% 8.64/2.70 % (2948912)Peak memory usage: 87 MB
% 8.64/2.70 % (2948912)Instructions burned: 1 (million)
% 8.64/2.70 % (2948895)------------------------------
% 8.64/2.70 % (2948895)------------------------------
% 8.64/2.70 [W927 19:40:04.275320626 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275432676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275523696 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275571276 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275645940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275695830 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275795313 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275842223 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275913850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.275961493 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.276041443 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 [W927 19:40:04.276088494 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 8.64/2.70 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 8.64/2.70 % (2948909)------------------------------
% 8.64/2.70 % (2948909)------------------------------
% 8.64/2.70 % (2948908)------------------------------
% 8.64/2.70 % (2948908)------------------------------
% 8.64/2.70 % (2948913)Instruction limit reached!
% 8.64/2.70 % (2948913)------------------------------
% 8.64/2.70 % (2948913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948913)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948913)Termination reason: Instruction limit
% 8.64/2.70 % (2948913)Termination phase: Saturation
% 8.64/2.70 % (2948913)Time elapsed: 0.170 s
% 8.64/2.70 % (2948913)Peak memory usage: 90 MB
% 8.64/2.70 % (2948913)Instructions burned: 248 (million)
% 8.64/2.70 % (2948916)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1124381360:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 8.64/2.70 % (2948916)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948916)------------------------------
% 8.64/2.70 % (2948916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948916)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948916)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948916)Time elapsed: 0.002 s
% 8.64/2.70 % (2948916)Peak memory usage: 88 MB
% 8.64/2.70 % (2948916)Instructions burned: 3 (million)
% 8.64/2.70 % (2948896)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948896)------------------------------
% 8.64/2.70 % (2948896)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948896)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948896)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948896)Time elapsed: 0.888 s
% 8.64/2.70 % (2948896)Peak memory usage: 127 MB
% 8.64/2.70 % (2948896)Instructions burned: 831 (million)
% 8.64/2.70 % (2948917)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3749214444:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 8.64/2.70 % (2948919)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=546525355:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 8.64/2.70 % (2948918)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2078615774:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 8.64/2.70 % (2948912)------------------------------
% 8.64/2.70 % (2948912)------------------------------
% 8.64/2.70 % (2948918)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948918)------------------------------
% 8.64/2.70 % (2948918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948918)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948918)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948918)Time elapsed: 0.004 s
% 8.64/2.70 % (2948918)Peak memory usage: 89 MB
% 8.64/2.70 % (2948918)Instructions burned: 2 (million)
% 8.64/2.70 % (2948919)First to succeed.
% 8.64/2.70 % (2948919)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2948881"
% 8.64/2.70 % (2948916)------------------------------
% 8.64/2.70 % (2948916)------------------------------
% 8.64/2.70 % (2948924)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1653938117:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 8.64/2.70 % (2948924)Refutation not found, incomplete strategy
% 8.64/2.70 % (2948924)------------------------------
% 8.64/2.70 % (2948924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.64/2.70 % (2948924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.64/2.70 % (2948924)CaDiCaL version: 2.1.3
% 8.64/2.70 % (2948924)Termination reason: Refutation not found, incomplete strategy
% 8.64/2.70 % (2948924)Time elapsed: 0.005 s
% 8.64/2.70 % (2948924)Peak memory usage: 87 MB
% 8.64/2.70 % (2948924)Instructions burned: 10 (million)
% 8.64/2.70 % (2948896)------------------------------
% 8.64/2.70 % (2948896)------------------------------
% 8.64/2.70 % (2948926)lrs+10_1_sil=8000:sp=occurrence:random_seed=1480443398:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 8.64/2.70 % (2948918)------------------------------
% 8.64/2.70 % (2948918)------------------------------
% 8.64/2.70 % (2948919)Refutation found. Thanks to Tanya!
% 8.64/2.70 % SZS status Theorem for theBenchmark
% 8.64/2.70 % SZS output start Proof for theBenchmark
% See solution above
% 12.10/2.92 % (2948919)------------------------------
% 12.10/2.92 % (2948919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.10/2.92 % (2948919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.10/2.92 % (2948919)CaDiCaL version: 2.1.3
% 12.10/2.92 % (2948919)Termination reason: Refutation
% 12.10/2.92 % (2948919)Time elapsed: 0.019 s
% 12.10/2.92 % (2948919)Peak memory usage: 88 MB
% 12.10/2.92 % (2948919)Instructions burned: 21 (million)
% 12.10/2.92 % (2948919)------------------------------
% 12.10/2.92 % (2948919)------------------------------
% 12.10/2.92 % (2948881)Success in time 1.622 s
% 12.10/2.92 % Vampire exiting
%------------------------------------------------------------------------------