%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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 10:19:10 AM UTC 2026
% Result : Unsatisfiable 41.51s 6.79s
% Output : Refutation 42.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 19
% Syntax : Number of formulae : 217 ( 136 unt; 3 def)
% Number of atoms : 329 ( 115 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 224 ( 112 ~; 109 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 4 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% Number of variables : 217 ( 0 sgn 217 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_less_equal) ).
fof(f2,axiom,
! [X0,X1] :
( ~ quotient(X0,X1,zero)
| less_equal(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_quotient) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ quotient(X0,X1,X2)
| less_equal(X2,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',divisor_existence) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ quotient(X5,X4,X6)
| ~ quotient(X1,X3,X4)
| ~ quotient(X0,X3,X5)
| ~ quotient(X0,X1,X2)
| ~ quotient(X2,X3,X7)
| less_equal(X6,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quotient_property) ).
fof(f5,axiom,
! [X0] : less_equal(zero,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_is_smallest) ).
fof(f6,axiom,
! [X0,X1] :
( ~ less_equal(X1,X0)
| ~ less_equal(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_equal_and_equal) ).
fof(f7,axiom,
! [X0] : less_equal(X0,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_is_largest) ).
fof(f8,axiom,
! [X0,X1] : quotient(X0,X1,divide(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure) ).
fof(f9,axiom,
! [X2,X3,X0,X1] :
( ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_defined) ).
fof(f10,axiom,
quotient(identity,a,idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f11,axiom,
quotient(identity,b,idQb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_b) ).
fof(f12,axiom,
quotient(identity,idQb,idQ_idQb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_idQb) ).
fof(f13,axiom,
quotient(idQa,idQ_idQb,idQa_Q__idQ_idQb),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idQa_divide_idQ_idQb) ).
fof(f14,axiom,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_divide_idQa) ).
fof(f15,axiom,
quotient(idQb,idQ_idQa,idQb_Q__idQ_idQa),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idQb_divide_idQ_idQa) ).
fof(f16,negated_conjecture,
idQa_Q__idQ_idQb != idQb_Q__idQ_idQa,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_idQa_Q__idQ_idQb_equals_idQb_Q__idQ_idQa) ).
fof(f21,plain,
! [X2,X0,X1] :
( ~ quotient(X0,X1,X2)
| divide(X0,X1) = X2 ),
inference(resolution,[],[f8,f9]) ).
fof(f22,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ quotient(X5,X1,X6)
| ~ quotient(X3,X1,X4)
| ~ quotient(X3,X0,X5)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X4,X2),X6) ),
inference(resolution,[],[f4,f8]) ).
fof(f27,plain,
! [X0,X1] : less_equal(divide(X0,X1),X0),
inference(resolution,[],[f3,f8]) ).
fof(f32,plain,
! [X0,X1] :
( ~ less_equal(X0,divide(X0,X1))
| divide(X0,X1) = X0 ),
inference(resolution,[],[f27,f6]) ).
fof(f57,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ quotient(X3,X1,X5)
| ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X2,X5),divide(X4,X1)) ),
inference(resolution,[],[f22,f8]) ).
fof(f58,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ quotient(X3,X1,X5)
| ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X2,X5),zero)
| ~ less_equal(X4,X1) ),
inference(resolution,[],[f22,f1]) ).
fof(f63,plain,
! [X2,X3,X0,X1,X4] :
( ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X4,divide(X1,X3)),divide(X2,X3)) ),
inference(resolution,[],[f57,f8]) ).
fof(f64,plain,
! [X2,X3,X0,X1,X4] :
( ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X4,zero),divide(X2,X3))
| ~ less_equal(X1,X3) ),
inference(resolution,[],[f57,f1]) ).
fof(f69,plain,
! [X2,X3,X0,X1] :
( less_equal(divide(divide(X0,X3),divide(X1,X3)),divide(X2,X3))
| ~ quotient(X0,X1,X2) ),
inference(resolution,[],[f63,f8]) ).
fof(f90,plain,
! [X0,X1] :
( ~ less_equal(X0,X1)
| zero = divide(X0,X1) ),
inference(resolution,[],[f21,f1]) ).
fof(f91,plain,
idQa = divide(identity,a),
inference(resolution,[],[f21,f10]) ).
fof(f92,plain,
idQ_idQa = divide(identity,idQa),
inference(resolution,[],[f21,f14]) ).
fof(f93,plain,
idQb = divide(identity,b),
inference(resolution,[],[f21,f11]) ).
fof(f94,plain,
idQ_idQb = divide(identity,idQb),
inference(resolution,[],[f21,f12]) ).
fof(f95,plain,
idQa_Q__idQ_idQb = divide(idQa,idQ_idQb),
inference(resolution,[],[f21,f13]) ).
fof(f96,plain,
idQb_Q__idQ_idQa = divide(idQb,idQ_idQa),
inference(resolution,[],[f21,f15]) ).
fof(f110,plain,
! [X2,X3,X0,X1] :
( ~ quotient(X0,X1,X2)
| less_equal(divide(divide(X0,X3),zero),divide(X2,X3))
| ~ less_equal(X1,X3) ),
inference(resolution,[],[f64,f8]) ).
fof(f118,plain,
! [X2,X0,X1] :
( less_equal(divide(divide(X0,X1),zero),divide(divide(X0,X2),X1))
| ~ less_equal(X2,X1) ),
inference(resolution,[],[f110,f8]) ).
fof(f124,plain,
! [X0] :
( less_equal(divide(divide(idQa,X0),zero),divide(idQa_Q__idQ_idQb,X0))
| ~ less_equal(idQ_idQb,X0) ),
inference(resolution,[],[f110,f13]) ).
fof(f125,plain,
! [X0] :
( less_equal(divide(divide(idQb,X0),zero),divide(idQb_Q__idQ_idQa,X0))
| ~ less_equal(idQ_idQa,X0) ),
inference(resolution,[],[f110,f15]) ).
fof(f213,plain,
! [X0] :
( ~ less_equal(X0,zero)
| zero = X0 ),
inference(resolution,[],[f5,f6]) ).
fof(f214,plain,
! [X0] : zero = divide(zero,X0),
inference(resolution,[],[f5,f32]) ).
fof(f361,plain,
! [X0] : zero = divide(X0,identity),
inference(resolution,[],[f90,f7]) ).
fof(f363,plain,
! [X0,X1] : zero = divide(divide(X0,X1),X0),
inference(resolution,[],[f90,f27]) ).
fof(f364,plain,
! [X2,X3,X0,X1] :
( ~ quotient(X0,X2,X3)
| zero = divide(divide(divide(X0,X1),divide(X2,X1)),divide(X3,X1)) ),
inference(resolution,[],[f90,f69]) ).
fof(f368,plain,
! [X0] :
( ~ less_equal(idQ_idQb,X0)
| zero = divide(divide(divide(idQa,X0),zero),divide(idQa_Q__idQ_idQb,X0)) ),
inference(resolution,[],[f90,f124]) ).
fof(f370,plain,
! [X0] :
( ~ less_equal(idQ_idQa,X0)
| zero = divide(divide(divide(idQb,X0),zero),divide(idQb_Q__idQ_idQa,X0)) ),
inference(resolution,[],[f90,f125]) ).
fof(f466,plain,
! [X2,X3,X0,X1,X4] :
( ~ quotient(X0,X3,X4)
| ~ quotient(X0,X1,X2)
| less_equal(divide(X4,divide(X1,X3)),zero)
| ~ less_equal(X2,X3) ),
inference(resolution,[],[f58,f8]) ).
fof(f476,plain,
! [X2,X3,X0,X1] :
( ~ quotient(X0,X1,X2)
| less_equal(divide(divide(X0,X3),divide(X1,X3)),zero)
| ~ less_equal(X2,X3) ),
inference(resolution,[],[f466,f8]) ).
fof(f486,plain,
! [X2,X0,X1] :
( less_equal(divide(divide(X0,X1),divide(X2,X1)),zero)
| ~ less_equal(divide(X0,X2),X1) ),
inference(resolution,[],[f476,f8]) ).
fof(f489,plain,
! [X0] :
( less_equal(divide(divide(identity,X0),divide(a,X0)),zero)
| ~ less_equal(idQa,X0) ),
inference(resolution,[],[f476,f10]) ).
fof(f500,plain,
! [X2,X0,X1] :
( ~ less_equal(divide(X0,X1),X2)
| zero = divide(divide(X0,X2),divide(X1,X2)) ),
inference(resolution,[],[f486,f213]) ).
fof(f525,plain,
! [X0,X1] : zero = divide(divide(X0,X0),divide(X1,X0)),
inference(resolution,[],[f500,f27]) ).
fof(f540,plain,
! [X2,X0,X1] :
( ~ less_equal(zero,X2)
| zero = divide(divide(divide(X0,X1),X2),divide(X0,X2)) ),
inference(superposition,[],[f500,f363]) ).
fof(f543,plain,
! [X2,X0,X1] : zero = divide(divide(divide(X0,X1),X2),divide(X0,X2)),
inference(forward_subsumption_resolution,[],[f540,f5]) ).
fof(f568,plain,
! [X0,X1] : quotient(divide(X0,X0),divide(X1,X0),zero),
inference(superposition,[],[f8,f525]) ).
fof(f627,definition,
( spl0_51
<=> less_equal(idQ_idQb,b) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f628,plain,
( less_equal(idQ_idQb,b)
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( ~ less_equal(idQ_idQb,b)
| spl0_51 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f722,plain,
! [X0] :
( ~ less_equal(idQa,X0)
| zero = divide(divide(identity,X0),divide(a,X0)) ),
inference(resolution,[],[f489,f213]) ).
fof(f766,plain,
! [X0] : quotient(divide(X0,X0),zero,zero),
inference(superposition,[],[f568,f363]) ).
fof(f775,plain,
! [X0] : less_equal(divide(X0,X0),zero),
inference(resolution,[],[f766,f2]) ).
fof(f797,plain,
! [X0] : zero = divide(X0,X0),
inference(resolution,[],[f775,f213]) ).
fof(f803,plain,
! [X0] : quotient(X0,X0,zero),
inference(superposition,[],[f8,f797]) ).
fof(f909,plain,
! [X0] : less_equal(X0,X0),
inference(resolution,[],[f803,f2]) ).
fof(f930,plain,
! [X0,X1] : zero = divide(divide(X0,divide(X0,X1)),divide(X1,divide(X0,X1))),
inference(resolution,[],[f909,f500]) ).
fof(f931,plain,
zero = divide(divide(identity,idQa),divide(a,idQa)),
inference(resolution,[],[f909,f722]) ).
fof(f932,plain,
zero = divide(idQ_idQa,divide(a,idQa)),
inference(forward_demodulation,[],[f931,f92]) ).
fof(f935,plain,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(superposition,[],[f8,f932]) ).
fof(f1029,plain,
! [X2,X0,X1] : quotient(divide(divide(X0,X1),X2),divide(X0,X2),zero),
inference(superposition,[],[f8,f543]) ).
fof(f1149,plain,
! [X0,X1] :
( ~ less_equal(zero,X1)
| zero = divide(divide(X0,X1),divide(identity,X1)) ),
inference(superposition,[],[f500,f361]) ).
fof(f1199,plain,
! [X0,X1] : zero = divide(divide(X0,X1),divide(identity,X1)),
inference(forward_subsumption_resolution,[],[f1149,f5]) ).
fof(f1247,plain,
! [X0,X1] : quotient(divide(X0,X1),divide(identity,X1),zero),
inference(superposition,[],[f8,f1199]) ).
fof(f1279,plain,
! [X0,X1] : less_equal(divide(X0,X1),divide(identity,X1)),
inference(resolution,[],[f1247,f2]) ).
fof(f1366,plain,
! [X0] : less_equal(divide(X0,idQa),idQ_idQa),
inference(superposition,[],[f1279,f92]) ).
fof(f1368,plain,
! [X0] : less_equal(divide(X0,idQb),idQ_idQb),
inference(superposition,[],[f1279,f94]) ).
fof(f1549,plain,
less_equal(idQ_idQa,divide(a,idQa)),
inference(resolution,[],[f935,f2]) ).
fof(f1569,plain,
( ~ less_equal(divide(a,idQa),idQ_idQa)
| idQ_idQa = divide(a,idQa) ),
inference(resolution,[],[f1549,f6]) ).
fof(f1570,plain,
idQ_idQa = divide(a,idQa),
inference(forward_subsumption_resolution,[],[f1569,f1366]) ).
fof(f1583,plain,
zero = divide(idQ_idQa,a),
inference(superposition,[],[f363,f1570]) ).
fof(f3237,plain,
! [X2,X0,X1] : less_equal(divide(divide(X0,X1),X2),divide(X0,X2)),
inference(resolution,[],[f1029,f2]) ).
fof(f4202,plain,
! [X0] : less_equal(divide(idQa_Q__idQ_idQb,X0),divide(idQa,X0)),
inference(superposition,[],[f3237,f95]) ).
fof(f4753,plain,
zero = divide(divide(divide(idQb,idQ_idQa),zero),divide(idQb_Q__idQ_idQa,idQ_idQa)),
inference(resolution,[],[f370,f909]) ).
fof(f4754,plain,
zero = divide(divide(idQb_Q__idQ_idQa,zero),divide(idQb_Q__idQ_idQa,idQ_idQa)),
inference(forward_demodulation,[],[f4753,f96]) ).
fof(f4764,plain,
( less_equal(divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),zero),zero)
| ~ less_equal(zero,divide(idQb_Q__idQ_idQa,idQ_idQa)) ),
inference(superposition,[],[f118,f4754]) ).
fof(f4809,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),zero),zero),
inference(forward_subsumption_resolution,[],[f4764,f5]) ).
fof(f4813,plain,
zero = divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),zero),
inference(resolution,[],[f4809,f213]) ).
fof(f4838,plain,
quotient(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),zero,zero),
inference(superposition,[],[f8,f4813]) ).
fof(f4893,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),zero),
inference(resolution,[],[f4838,f2]) ).
fof(f4926,plain,
zero = divide(divide(idQb_Q__idQ_idQa,zero),divide(divide(idQb_Q__idQ_idQa,idQ_idQa),zero)),
inference(resolution,[],[f4893,f500]) ).
fof(f4927,plain,
zero = divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),
inference(resolution,[],[f4893,f213]) ).
fof(f4944,plain,
quotient(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa),zero),
inference(superposition,[],[f8,f4927]) ).
fof(f5061,plain,
less_equal(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,idQ_idQa)),
inference(resolution,[],[f4944,f2]) ).
fof(f5091,plain,
idQb_Q__idQ_idQa = divide(idQb_Q__idQ_idQa,idQ_idQa),
inference(resolution,[],[f5061,f32]) ).
fof(f6697,plain,
! [X2,X0,X1] : zero = divide(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1)),
inference(resolution,[],[f364,f8]) ).
fof(f6703,plain,
! [X0] : zero = divide(divide(divide(identity,X0),divide(idQa,X0)),divide(idQ_idQa,X0)),
inference(resolution,[],[f364,f14]) ).
fof(f6704,plain,
! [X0] : zero = divide(divide(divide(identity,X0),divide(b,X0)),divide(idQb,X0)),
inference(resolution,[],[f364,f11]) ).
fof(f6705,plain,
! [X0] : zero = divide(divide(divide(identity,X0),divide(idQb,X0)),divide(idQ_idQb,X0)),
inference(resolution,[],[f364,f12]) ).
fof(f6723,plain,
! [X0] : zero = divide(divide(divide(idQb,X0),divide(idQ_idQa,X0)),divide(idQb_Q__idQ_idQa,X0)),
inference(resolution,[],[f364,f15]) ).
fof(f6948,plain,
! [X2,X0,X1] : quotient(divide(divide(X0,X1),divide(X2,X1)),divide(divide(X0,X2),X1),zero),
inference(superposition,[],[f8,f6697]) ).
fof(f7151,plain,
zero = divide(divide(divide(identity,idQb),divide(b,idQb)),zero),
inference(superposition,[],[f6704,f797]) ).
fof(f7212,plain,
zero = divide(divide(idQ_idQb,divide(b,idQb)),zero),
inference(forward_demodulation,[],[f7151,f94]) ).
fof(f7753,plain,
quotient(divide(divide(idQb_Q__idQ_idQa,divide(divide(idQb_Q__idQ_idQa,idQ_idQa),zero)),divide(zero,divide(divide(idQb_Q__idQ_idQa,idQ_idQa),zero))),zero,zero),
inference(superposition,[],[f6948,f4926]) ).
fof(f7764,plain,
quotient(divide(divide(idQb_Q__idQ_idQa,divide(divide(idQb_Q__idQ_idQa,idQ_idQa),zero)),zero),zero,zero),
inference(forward_demodulation,[],[f7753,f214]) ).
fof(f7884,plain,
quotient(divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),zero),zero,zero),
inference(forward_demodulation,[],[f7764,f5091]) ).
fof(f7962,plain,
quotient(divide(idQ_idQb,divide(b,idQb)),zero,zero),
inference(superposition,[],[f8,f7212]) ).
fof(f8031,plain,
less_equal(divide(idQ_idQb,divide(b,idQb)),zero),
inference(resolution,[],[f7962,f2]) ).
fof(f8071,plain,
zero = divide(idQ_idQb,divide(b,idQb)),
inference(resolution,[],[f8031,f213]) ).
fof(f8090,plain,
quotient(idQ_idQb,divide(b,idQb),zero),
inference(superposition,[],[f8,f8071]) ).
fof(f8241,plain,
less_equal(idQ_idQb,divide(b,idQb)),
inference(resolution,[],[f8090,f2]) ).
fof(f8278,plain,
( ~ less_equal(divide(b,idQb),idQ_idQb)
| idQ_idQb = divide(b,idQb) ),
inference(resolution,[],[f8241,f6]) ).
fof(f8287,plain,
idQ_idQb = divide(b,idQb),
inference(forward_subsumption_resolution,[],[f8278,f1368]) ).
fof(f8309,plain,
less_equal(idQ_idQb,b),
inference(superposition,[],[f27,f8287]) ).
fof(f8365,plain,
( $false
| spl0_51 ),
inference(forward_subsumption_resolution,[],[f8309,f629]) ).
fof(f8366,plain,
spl0_51,
inference(avatar_contradiction_clause,[],[f8365]) ).
fof(f8598,plain,
( zero = divide(divide(divide(idQa,b),zero),divide(idQa_Q__idQ_idQb,b))
| ~ spl0_51 ),
inference(resolution,[],[f628,f368]) ).
fof(f8753,plain,
less_equal(divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),zero),zero),
inference(resolution,[],[f7884,f2]) ).
fof(f8794,plain,
zero = divide(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),zero),
inference(resolution,[],[f8753,f213]) ).
fof(f8824,plain,
quotient(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),zero,zero),
inference(superposition,[],[f8,f8794]) ).
fof(f8884,plain,
less_equal(divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),zero),
inference(resolution,[],[f8824,f2]) ).
fof(f8924,plain,
zero = divide(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),
inference(resolution,[],[f8884,f213]) ).
fof(f8947,plain,
quotient(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero),zero),
inference(superposition,[],[f8,f8924]) ).
fof(f9109,plain,
less_equal(idQb_Q__idQ_idQa,divide(idQb_Q__idQ_idQa,zero)),
inference(resolution,[],[f8947,f2]) ).
fof(f9146,plain,
idQb_Q__idQ_idQa = divide(idQb_Q__idQ_idQa,zero),
inference(resolution,[],[f9109,f32]) ).
fof(f18955,plain,
! [X0,X1] : quotient(divide(X0,divide(X0,X1)),divide(X1,divide(X0,X1)),zero),
inference(superposition,[],[f8,f930]) ).
fof(f19062,plain,
! [X0,X1] : less_equal(divide(X0,divide(X0,X1)),divide(X1,divide(X0,X1))),
inference(resolution,[],[f18955,f2]) ).
fof(f19339,plain,
! [X0,X1] :
( ~ less_equal(divide(X0,divide(X1,X0)),divide(X1,divide(X1,X0)))
| divide(X0,divide(X1,X0)) = divide(X1,divide(X1,X0)) ),
inference(resolution,[],[f19062,f6]) ).
fof(f19476,plain,
! [X0] : less_equal(divide(X0,divide(X0,zero)),zero),
inference(superposition,[],[f19062,f214]) ).
fof(f19568,plain,
! [X0] : zero = divide(X0,divide(X0,zero)),
inference(resolution,[],[f19476,f213]) ).
fof(f19670,plain,
! [X0] : quotient(X0,divide(X0,zero),zero),
inference(superposition,[],[f8,f19568]) ).
fof(f21513,plain,
! [X0] : less_equal(X0,divide(X0,zero)),
inference(resolution,[],[f19670,f2]) ).
fof(f21627,plain,
! [X0] : divide(X0,zero) = X0,
inference(resolution,[],[f21513,f32]) ).
fof(f21857,plain,
! [X2,X0,X1] :
( less_equal(divide(X0,X1),divide(divide(X0,X2),X1))
| ~ less_equal(X2,X1) ),
inference(superposition,[],[f118,f21627]) ).
fof(f31893,plain,
( zero = divide(divide(idQa,b),divide(idQa_Q__idQ_idQb,b))
| ~ spl0_51 ),
inference(forward_demodulation,[],[f8598,f21627]) ).
fof(f66008,plain,
( ~ less_equal(divide(divide(idQa_Q__idQ_idQb,b),zero),divide(divide(idQa,b),zero))
| divide(divide(idQa,b),zero) = divide(divide(idQa_Q__idQ_idQb,b),zero)
| ~ spl0_51 ),
inference(superposition,[],[f19339,f31893]) ).
fof(f66243,plain,
( ~ less_equal(divide(divide(idQa_Q__idQ_idQb,b),zero),divide(idQa,b))
| divide(divide(idQa,b),zero) = divide(divide(idQa_Q__idQ_idQb,b),zero)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f66008,f21627]) ).
fof(f66399,plain,
( ~ less_equal(divide(idQa_Q__idQ_idQb,b),divide(idQa,b))
| divide(divide(idQa,b),zero) = divide(divide(idQa_Q__idQ_idQb,b),zero)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f66243,f21627]) ).
fof(f66529,plain,
( divide(divide(idQa,b),zero) = divide(divide(idQa_Q__idQ_idQb,b),zero)
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f66399,f4202]) ).
fof(f66625,plain,
( divide(divide(idQa,b),zero) = divide(idQa_Q__idQ_idQb,b)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f66529,f21627]) ).
fof(f66702,plain,
( divide(idQa,b) = divide(idQa_Q__idQ_idQb,b)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f66625,f21627]) ).
fof(f68394,plain,
( less_equal(divide(idQa,b),idQa_Q__idQ_idQb)
| ~ spl0_51 ),
inference(superposition,[],[f27,f66702]) ).
fof(f71004,definition,
( spl0_400
<=> less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb) ),
introduced(definition,[new_symbols(definition,[spl0_400])],[avatar_definition]) ).
fof(f71005,plain,
( less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| ~ spl0_400 ),
inference(avatar_component_clause,[],[f71004]) ).
fof(f71006,plain,
( ~ less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| spl0_400 ),
inference(avatar_component_clause,[],[f71004]) ).
fof(f78244,plain,
! [X2,X0,X1] :
( ~ less_equal(X0,X1)
| ~ less_equal(divide(divide(X2,X0),X1),divide(X2,X1))
| divide(X2,X1) = divide(divide(X2,X0),X1) ),
inference(resolution,[],[f21857,f6]) ).
fof(f79003,plain,
! [X2,X0,X1] :
( ~ less_equal(X0,X1)
| divide(X2,X1) = divide(divide(X2,X0),X1) ),
inference(forward_subsumption_resolution,[],[f78244,f3237]) ).
fof(f79798,plain,
! [X2,X0,X1] : divide(X0,X1) = divide(divide(X0,divide(X1,X2)),X1),
inference(resolution,[],[f79003,f27]) ).
fof(f80207,plain,
! [X0,X1] : divide(zero,X1) = divide(divide(X0,divide(X0,X1)),X1),
inference(superposition,[],[f79798,f930]) ).
fof(f80216,plain,
! [X2,X0,X1] : divide(zero,X0) = divide(divide(divide(X0,X1),X2),X0),
inference(superposition,[],[f79798,f543]) ).
fof(f80223,plain,
! [X0] : divide(zero,idQ_idQb) = divide(divide(divide(identity,X0),divide(idQb,X0)),idQ_idQb),
inference(superposition,[],[f79798,f6705]) ).
fof(f80224,plain,
! [X0] : divide(zero,idQ_idQa) = divide(divide(divide(identity,X0),divide(idQa,X0)),idQ_idQa),
inference(superposition,[],[f79798,f6703]) ).
fof(f80232,plain,
! [X0] : divide(zero,idQb_Q__idQ_idQa) = divide(divide(divide(idQb,X0),divide(idQ_idQa,X0)),idQb_Q__idQ_idQa),
inference(superposition,[],[f79798,f6723]) ).
fof(f80731,plain,
! [X0] : zero = divide(divide(divide(idQb,X0),divide(idQ_idQa,X0)),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f80232,f214]) ).
fof(f80739,plain,
! [X0] : zero = divide(divide(divide(identity,X0),divide(idQa,X0)),idQ_idQa),
inference(forward_demodulation,[],[f80224,f214]) ).
fof(f80740,plain,
! [X0] : zero = divide(divide(divide(identity,X0),divide(idQb,X0)),idQ_idQb),
inference(forward_demodulation,[],[f80223,f214]) ).
fof(f80747,plain,
! [X2,X0,X1] : zero = divide(divide(divide(X0,X1),X2),X0),
inference(forward_demodulation,[],[f80216,f214]) ).
fof(f80756,plain,
! [X0,X1] : zero = divide(divide(X0,divide(X0,X1)),X1),
inference(forward_demodulation,[],[f80207,f214]) ).
fof(f81720,plain,
! [X2,X0,X1] :
( ~ less_equal(zero,X2)
| zero = divide(divide(divide(X0,divide(X0,X1)),X2),divide(X1,X2)) ),
inference(superposition,[],[f500,f80756]) ).
fof(f81747,plain,
! [X0,X1] : less_equal(divide(divide(X0,divide(X0,X1)),zero),divide(X1,zero)),
inference(superposition,[],[f19062,f80756]) ).
fof(f81885,plain,
! [X0,X1] : less_equal(divide(divide(X0,divide(X0,X1)),zero),X1),
inference(forward_demodulation,[],[f81747,f21627]) ).
fof(f81904,plain,
! [X2,X0,X1] : zero = divide(divide(divide(X0,divide(X0,X1)),X2),divide(X1,X2)),
inference(forward_subsumption_resolution,[],[f81720,f5]) ).
fof(f82028,plain,
! [X0,X1] : less_equal(divide(X0,divide(X0,X1)),X1),
inference(forward_demodulation,[],[f81885,f21627]) ).
fof(f82095,plain,
! [X2,X0,X1] : divide(X0,X1) = divide(divide(X0,divide(X2,divide(X2,X1))),X1),
inference(resolution,[],[f82028,f79003]) ).
fof(f102361,plain,
zero = divide(divide(divide(idQb,a),zero),idQb_Q__idQ_idQa),
inference(superposition,[],[f80731,f1583]) ).
fof(f102547,plain,
zero = divide(divide(idQb,a),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f102361,f21627]) ).
fof(f102706,plain,
! [X0] : divide(X0,idQb_Q__idQ_idQa) = divide(divide(X0,divide(divide(idQb,a),zero)),idQb_Q__idQ_idQa),
inference(superposition,[],[f82095,f102547]) ).
fof(f102716,plain,
! [X0] : divide(X0,idQb_Q__idQ_idQa) = divide(divide(X0,divide(idQb,a)),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f102706,f21627]) ).
fof(f106762,plain,
zero = divide(divide(idQb,divide(idQa,b)),idQ_idQa),
inference(superposition,[],[f80739,f93]) ).
fof(f106972,plain,
zero = divide(divide(idQa,divide(idQb,a)),idQ_idQb),
inference(superposition,[],[f80740,f91]) ).
fof(f107185,plain,
zero = divide(divide(divide(idQa,idQ_idQb),divide(divide(idQb,a),idQ_idQb)),zero),
inference(superposition,[],[f6697,f106972]) ).
fof(f107319,plain,
zero = divide(divide(idQa,idQ_idQb),divide(divide(idQb,a),idQ_idQb)),
inference(forward_demodulation,[],[f107185,f21627]) ).
fof(f107338,plain,
zero = divide(idQa_Q__idQ_idQb,divide(divide(idQb,a),idQ_idQb)),
inference(forward_demodulation,[],[f107319,f95]) ).
fof(f107376,plain,
divide(zero,divide(idQb,a)) = divide(idQa_Q__idQ_idQb,divide(idQb,a)),
inference(superposition,[],[f79798,f107338]) ).
fof(f107494,plain,
zero = divide(idQa_Q__idQ_idQb,divide(idQb,a)),
inference(forward_demodulation,[],[f107376,f214]) ).
fof(f107565,plain,
divide(zero,idQb_Q__idQ_idQa) = divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(superposition,[],[f102716,f107494]) ).
fof(f107686,plain,
zero = divide(idQa_Q__idQ_idQb,idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f107565,f214]) ).
fof(f107815,plain,
! [X0] : zero = divide(divide(divide(idQa_Q__idQ_idQb,X0),idQb_Q__idQ_idQa),zero),
inference(superposition,[],[f543,f107686]) ).
fof(f107839,plain,
( ~ less_equal(divide(idQb_Q__idQ_idQa,zero),divide(idQa_Q__idQ_idQb,zero))
| divide(idQa_Q__idQ_idQb,zero) = divide(idQb_Q__idQ_idQa,zero) ),
inference(superposition,[],[f19339,f107686]) ).
fof(f107858,plain,
! [X0] : zero = divide(divide(divide(X0,divide(X0,idQa_Q__idQ_idQb)),idQb_Q__idQ_idQa),zero),
inference(superposition,[],[f81904,f107686]) ).
fof(f107872,plain,
! [X0] : zero = divide(divide(X0,divide(X0,idQa_Q__idQ_idQb)),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f107858,f21627]) ).
fof(f107879,plain,
( ~ less_equal(divide(idQb_Q__idQ_idQa,zero),idQa_Q__idQ_idQb)
| divide(idQa_Q__idQ_idQb,zero) = divide(idQb_Q__idQ_idQa,zero) ),
inference(forward_demodulation,[],[f107839,f21627]) ).
fof(f107896,plain,
! [X0] : zero = divide(divide(idQa_Q__idQ_idQb,X0),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f107815,f21627]) ).
fof(f107943,plain,
( ~ less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| divide(idQa_Q__idQ_idQb,zero) = divide(idQb_Q__idQ_idQa,zero) ),
inference(forward_demodulation,[],[f107879,f9146]) ).
fof(f108147,plain,
! [X0] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),zero),idQb_Q__idQ_idQa),
inference(superposition,[],[f82028,f107896]) ).
fof(f108159,plain,
! [X0] : less_equal(divide(idQa_Q__idQ_idQb,X0),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f108147,f21627]) ).
fof(f108258,plain,
( less_equal(divide(idQa,b),idQb_Q__idQ_idQa)
| ~ spl0_51 ),
inference(superposition,[],[f108159,f66702]) ).
fof(f110708,plain,
! [X0] : less_equal(divide(divide(X0,divide(X0,idQa_Q__idQ_idQb)),zero),idQb_Q__idQ_idQa),
inference(superposition,[],[f82028,f107872]) ).
fof(f110720,plain,
! [X0] : less_equal(divide(X0,divide(X0,idQa_Q__idQ_idQb)),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f110708,f21627]) ).
fof(f110894,plain,
! [X0,X1] : less_equal(divide(divide(divide(idQa_Q__idQ_idQb,X0),X1),zero),idQb_Q__idQ_idQa),
inference(superposition,[],[f110720,f80747]) ).
fof(f110910,plain,
! [X0,X1] : less_equal(divide(divide(idQa_Q__idQ_idQb,X0),X1),idQb_Q__idQ_idQa),
inference(forward_demodulation,[],[f110894,f21627]) ).
fof(f111270,plain,
( ! [X0] : less_equal(divide(divide(idQa,b),X0),idQb_Q__idQ_idQa)
| ~ spl0_51 ),
inference(superposition,[],[f110910,f66702]) ).
fof(f117435,definition,
( spl0_553
<=> idQb_Q__idQ_idQa = divide(idQa,b) ),
introduced(definition,[new_symbols(definition,[spl0_553])],[avatar_definition]) ).
fof(f117437,plain,
( idQb_Q__idQ_idQa = divide(idQa,b)
| ~ spl0_553 ),
inference(avatar_component_clause,[],[f117435]) ).
fof(f118738,plain,
zero = divide(divide(divide(idQb,idQ_idQa),divide(divide(idQa,b),idQ_idQa)),zero),
inference(superposition,[],[f6697,f106762]) ).
fof(f118874,plain,
zero = divide(divide(idQb,idQ_idQa),divide(divide(idQa,b),idQ_idQa)),
inference(forward_demodulation,[],[f118738,f21627]) ).
fof(f118893,plain,
zero = divide(idQb_Q__idQ_idQa,divide(divide(idQa,b),idQ_idQa)),
inference(forward_demodulation,[],[f118874,f96]) ).
fof(f119021,plain,
( ~ less_equal(divide(divide(divide(idQa,b),idQ_idQa),zero),divide(idQb_Q__idQ_idQa,zero))
| divide(idQb_Q__idQ_idQa,zero) = divide(divide(divide(idQa,b),idQ_idQa),zero) ),
inference(superposition,[],[f19339,f118893]) ).
fof(f119062,plain,
( ~ less_equal(divide(divide(divide(idQa,b),idQ_idQa),zero),idQb_Q__idQ_idQa)
| divide(idQb_Q__idQ_idQa,zero) = divide(divide(divide(idQa,b),idQ_idQa),zero) ),
inference(forward_demodulation,[],[f119021,f9146]) ).
fof(f119122,plain,
( ~ less_equal(divide(divide(idQa,b),idQ_idQa),idQb_Q__idQ_idQa)
| divide(idQb_Q__idQ_idQa,zero) = divide(divide(divide(idQa,b),idQ_idQa),zero) ),
inference(forward_demodulation,[],[f119062,f21627]) ).
fof(f119156,plain,
( divide(idQb_Q__idQ_idQa,zero) = divide(divide(divide(idQa,b),idQ_idQa),zero)
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f119122,f111270]) ).
fof(f119160,plain,
( divide(idQb_Q__idQ_idQa,zero) = divide(divide(idQa,b),idQ_idQa)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f119156,f21627]) ).
fof(f119162,plain,
( idQb_Q__idQ_idQa = divide(divide(idQa,b),idQ_idQa)
| ~ spl0_51 ),
inference(forward_demodulation,[],[f119160,f9146]) ).
fof(f119187,plain,
( ~ less_equal(divide(idQa,b),idQb_Q__idQ_idQa)
| idQb_Q__idQ_idQa = divide(idQa,b)
| ~ spl0_51 ),
inference(superposition,[],[f32,f119162]) ).
fof(f119278,plain,
( idQb_Q__idQ_idQa = divide(idQa,b)
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f119187,f108258]) ).
fof(f119292,plain,
( spl0_553
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f119278,f627,f117435]) ).
fof(f119295,plain,
( less_equal(idQb_Q__idQ_idQa,idQa_Q__idQ_idQb)
| ~ spl0_51
| ~ spl0_553 ),
inference(superposition,[],[f68394,f117437]) ).
fof(f119421,plain,
( $false
| ~ spl0_51
| spl0_400
| ~ spl0_553 ),
inference(forward_subsumption_resolution,[],[f119295,f71006]) ).
fof(f119422,plain,
( ~ spl0_51
| spl0_400
| ~ spl0_553 ),
inference(avatar_contradiction_clause,[],[f119421]) ).
fof(f119431,plain,
( divide(idQa_Q__idQ_idQb,zero) = divide(idQb_Q__idQ_idQa,zero)
| ~ spl0_400 ),
inference(forward_subsumption_resolution,[],[f107943,f71005]) ).
fof(f119435,plain,
( idQb_Q__idQ_idQa = divide(idQa_Q__idQ_idQb,zero)
| ~ spl0_400 ),
inference(forward_demodulation,[],[f119431,f9146]) ).
fof(f119440,plain,
( idQa_Q__idQ_idQb = idQb_Q__idQ_idQa
| ~ spl0_400 ),
inference(forward_demodulation,[],[f119435,f21627]) ).
fof(f119441,plain,
( $false
| ~ spl0_400 ),
inference(forward_subsumption_resolution,[],[f119440,f16]) ).
fof(f119442,plain,
~ spl0_400,
inference(avatar_contradiction_clause,[],[f119441]) ).
cnf(s119,plain,
spl0_51,
inference(sat_conversion,[],[f8366]) ).
cnf(s423,plain,
( ~ spl0_51
| spl0_553 ),
inference(sat_conversion,[],[f119292]) ).
cnf(s424,plain,
( ~ spl0_51
| spl0_400
| ~ spl0_553 ),
inference(sat_conversion,[],[f119422]) ).
cnf(s428,plain,
~ spl0_400,
inference(sat_conversion,[],[f119442]) ).
cnf(s429,plain,
( ~ spl0_51
| ~ spl0_553 ),
inference(rat,[],[s424,s428]) ).
cnf(s434,plain,
~ spl0_553,
inference(rat,[],[s429,s119]) ).
cnf(s436,plain,
$false,
inference(rat,[],[s423,s434,s119]) ).
fof(f119443,plain,
$false,
inference(avatar_sat_refutation,[],[s436]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HEN011-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n004.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 10:51:22 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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
% 10.01/2.38 % (3338519)Input is clausal, will run a generic CNF schedule.
% 10.01/2.38 % (3338606)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3787475160:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.01/2.38 % (3338606)Refutation not found, incomplete strategy
% 10.01/2.38 % (3338606)------------------------------
% 10.01/2.38 % (3338606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.38 % (3338606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.38 % (3338606)CaDiCaL version: 2.1.3
% 10.01/2.38 % (3338606)Termination reason: Refutation not found, incomplete strategy
% 10.01/2.38 % (3338606)Time elapsed: 0.013 s
% 10.01/2.38 % (3338606)Peak memory usage: 88 MB
% 10.01/2.38 % (3338606)Instructions burned: 31 (million)
% 10.01/2.38 % (3338603)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1862627216:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.01/2.38 % (3338599)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=1596166760:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.01/2.38 % (3338604)lrs+10_1_sil=8000:sp=occurrence:random_seed=803243115:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.01/2.38 % (3338601)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=662647888:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.01/2.38 % (3338608)dis-21_1_sil=8000:lcm=predicate:random_seed=1528688568:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.01/2.38 % (3338604)Refutation not found, incomplete strategy
% 10.01/2.38 % (3338604)------------------------------
% 10.01/2.38 % (3338604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.38 % (3338604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.38 % (3338604)CaDiCaL version: 2.1.3
% 10.01/2.38 % (3338604)Termination reason: Refutation not found, incomplete strategy
% 10.01/2.38 % (3338604)Time elapsed: 0.009 s
% 10.01/2.38 % (3338604)Peak memory usage: 88 MB
% 10.01/2.38 % (3338604)Instructions burned: 12 (million)
% 10.01/2.38 % (3338607)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3061012363:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.01/2.38 % (3338608)Instruction limit reached!
% 10.01/2.38 % (3338608)------------------------------
% 10.01/2.38 % (3338608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.38 % (3338608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.38 % (3338608)CaDiCaL version: 2.1.3
% 10.01/2.38 % (3338608)Termination reason: Instruction limit
% 10.01/2.38 % (3338608)Termination phase: Saturation
% 10.01/2.38 % (3338608)Time elapsed: 0.060 s
% 10.01/2.38 % (3338608)Peak memory usage: 88 MB
% 10.01/2.38 % (3338608)Instructions burned: 117 (million)
% 10.01/2.38 % (3338607)Instruction limit reached!
% 10.01/2.38 % (3338607)------------------------------
% 10.01/2.38 % (3338607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.38 % (3338607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.38 % (3338607)CaDiCaL version: 2.1.3
% 10.01/2.38 % (3338607)Termination reason: Instruction limit
% 10.01/2.38 % (3338607)Termination phase: Saturation
% 10.01/2.38 % (3338607)Time elapsed: 0.098 s
% 10.01/2.38 % (3338607)Peak memory usage: 89 MB
% 10.01/2.38 % (3338607)Instructions burned: 181 (million)
% 10.01/2.38 % (3338606)------------------------------
% 10.01/2.38 % (3338606)------------------------------
% 10.01/2.38 % (3338686)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3884618056:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.01/2.38 % (3338686)Refutation not found, incomplete strategy
% 10.01/2.38 % (3338686)------------------------------
% 10.01/2.38 % (3338686)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.01/2.38 % (3338686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.01/2.38 % (3338686)CaDiCaL version: 2.1.3
% 10.01/2.38 % (3338686)Termination reason: Refutation not found, incomplete strategy
% 10.01/2.38 % (3338686)Time elapsed: 0.016 s
% 10.01/2.38 % (3338686)Peak memory usage: 88 MB
% 20.46/3.81 % (3338686)Instructions burned: 21 (million)
% 20.46/3.81 % (3338703)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3408175206:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 20.46/3.81 % (3338702)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=515751645:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 20.46/3.81 % (3338703)Refutation not found, incomplete strategy
% 20.46/3.81 % (3338703)------------------------------
% 20.46/3.81 % (3338703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/3.81 % (3338703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/3.81 % (3338703)CaDiCaL version: 2.1.3
% 20.46/3.81 % (3338703)Termination reason: Refutation not found, incomplete strategy
% 20.46/3.81 % (3338703)Time elapsed: 0.006 s
% 20.46/3.81 % (3338703)Peak memory usage: 88 MB
% 20.46/3.81 % (3338703)Instructions burned: 16 (million)
% 20.46/3.81 % (3338604)------------------------------
% 20.46/3.81 % (3338604)------------------------------
% 20.46/3.81 % (3338702)Instruction limit reached!
% 20.46/3.81 % (3338702)------------------------------
% 20.46/3.81 % (3338702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/3.81 % (3338702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/3.81 % (3338702)CaDiCaL version: 2.1.3
% 20.46/3.81 % (3338702)Termination reason: Instruction limit
% 20.46/3.81 % (3338702)Termination phase: Saturation
% 20.46/3.81 % (3338702)Time elapsed: 0.108 s
% 20.46/3.81 % (3338702)Peak memory usage: 89 MB
% 20.46/3.81 % (3338702)Instructions burned: 190 (million)
% 20.46/3.81 % (3338703)------------------------------
% 20.46/3.81 % (3338703)------------------------------
% 20.46/3.81 % (3338707)lrs+10_64_to=lpo:sil=8000:random_seed=2511197317:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 20.46/3.81 % (3338686)------------------------------
% 20.46/3.81 % (3338686)------------------------------
% 20.46/3.81 % (3338707)Instruction limit reached!
% 20.46/3.81 % (3338707)------------------------------
% 20.46/3.81 % (3338707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/3.81 % (3338707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/3.82 % (3338707)CaDiCaL version: 2.1.3
% 20.46/3.82 % (3338707)Termination reason: Instruction limit
% 20.46/3.82 % (3338707)Termination phase: Saturation
% 20.46/3.82 % (3338707)Time elapsed: 0.078 s
% 20.46/3.82 % (3338707)Peak memory usage: 88 MB
% 20.46/3.82 % (3338707)Instructions burned: 126 (million)
% 20.46/3.82 % (3338708)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2603898073:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 20.46/3.82 % (3338709)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1586179168:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 20.46/3.82 % (3338709)Instruction limit reached!
% 20.46/3.82 % (3338709)------------------------------
% 20.46/3.82 % (3338709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/3.82 % (3338709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/3.82 % (3338709)CaDiCaL version: 2.1.3
% 20.46/3.82 % (3338709)Termination reason: Instruction limit
% 20.46/3.82 % (3338709)Termination phase: Saturation
% 20.46/3.82 % (3338709)Time elapsed: 0.057 s
% 20.46/3.82 % (3338709)Peak memory usage: 90 MB
% 20.46/3.82 % (3338709)Instructions burned: 157 (million)
% 20.46/3.82 % (3338711)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3593746450:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 20.46/3.82 % (3338708)Instruction limit reached!
% 20.46/3.82 % (3338708)------------------------------
% 20.46/3.82 % (3338708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.46/3.82 % (3338708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.46/3.82 % (3338708)CaDiCaL version: 2.1.3
% 20.46/3.82 % (3338708)Termination reason: Instruction limit
% 20.46/3.82 % (3338708)Termination phase: Saturation
% 20.46/3.82 % (3338708)Time elapsed: 0.119 s
% 20.46/3.82 % (3338708)Peak memory usage: 88 MB
% 20.46/3.82 % (3338708)Instructions burned: 195 (million)
% 20.46/3.82 % (3338712)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=782458126:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 30.90/5.23 % (3338715)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=789483551:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 30.90/5.23 % (3338712)Instruction limit reached!
% 30.90/5.23 % (3338712)------------------------------
% 30.90/5.23 % (3338712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.90/5.23 % (3338712)CaDiCaL version: 2.1.3
% 30.90/5.23 % (3338712)Termination reason: Instruction limit
% 30.90/5.23 % (3338712)Termination phase: Saturation
% 30.90/5.23 % (3338712)Time elapsed: 0.067 s
% 30.90/5.23 % (3338712)Peak memory usage: 89 MB
% 30.90/5.23 % (3338712)Instructions burned: 107 (million)
% 30.90/5.23 % (3338715)Refutation not found, incomplete strategy
% 30.90/5.23 % (3338715)------------------------------
% 30.90/5.23 % (3338715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.90/5.23 % (3338715)CaDiCaL version: 2.1.3
% 30.90/5.23 % (3338715)Termination reason: Refutation not found, incomplete strategy
% 30.90/5.23 % (3338715)Time elapsed: 0.015 s
% 30.90/5.23 % (3338715)Peak memory usage: 88 MB
% 30.90/5.23 % (3338715)Instructions burned: 44 (million)
% 30.90/5.23 % (3338717)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=289108603:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 30.90/5.23 % (3338717)Refutation not found, incomplete strategy
% 30.90/5.23 % (3338717)------------------------------
% 30.90/5.23 % (3338717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.90/5.23 % (3338717)CaDiCaL version: 2.1.3
% 30.90/5.23 % (3338717)Termination reason: Refutation not found, incomplete strategy
% 30.90/5.23 % (3338717)Time elapsed: 0.017 s
% 30.90/5.23 % (3338717)Peak memory usage: 87 MB
% 30.90/5.23 % (3338717)Instructions burned: 29 (million)
% 30.90/5.23 % (3338720)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3548038051:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 30.90/5.23 % (3338715)------------------------------
% 30.90/5.23 % (3338715)------------------------------
% 30.90/5.23 % (3338723)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1405489869:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 30.90/5.23 % (3338717)------------------------------
% 30.90/5.23 % (3338717)------------------------------
% 30.90/5.23 % (3338723)Instruction limit reached!
% 30.90/5.23 % (3338723)------------------------------
% 30.90/5.23 % (3338723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.90/5.23 % (3338723)CaDiCaL version: 2.1.3
% 30.90/5.23 % (3338723)Termination reason: Instruction limit
% 30.90/5.23 % (3338723)Termination phase: Saturation
% 30.90/5.23 % (3338723)Time elapsed: 0.045 s
% 30.90/5.23 % (3338723)Peak memory usage: 89 MB
% 30.90/5.23 % (3338723)Instructions burned: 136 (million)
% 30.90/5.23 % (3338725)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=767167370:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 30.90/5.23 % (3338726)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1171004884:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 30.90/5.23 % (3338725)Instruction limit reached!
% 30.90/5.23 % (3338725)------------------------------
% 30.90/5.23 % (3338725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.90/5.23 % (3338725)CaDiCaL version: 2.1.3
% 30.90/5.23 % (3338725)Termination reason: Instruction limit
% 30.90/5.23 % (3338725)Termination phase: Saturation
% 30.90/5.23 % (3338725)Time elapsed: 0.143 s
% 30.90/5.23 % (3338725)Peak memory usage: 91 MB
% 30.90/5.23 % (3338725)Instructions burned: 502 (million)
% 30.90/5.23 % (3338726)Instruction limit reached!
% 30.90/5.23 % (3338726)------------------------------
% 30.90/5.23 % (3338726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.90/5.23 % (3338726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338726)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338726)Termination reason: Instruction limit
% 41.51/6.79 % (3338726)Termination phase: Saturation
% 41.51/6.79 % (3338726)Time elapsed: 0.113 s
% 41.51/6.79 % (3338726)Peak memory usage: 89 MB
% 41.51/6.79 % (3338726)Instructions burned: 191 (million)
% 41.51/6.79 % (3338730)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1633736897:cond=on:i=156:bs=on:gtg=exists_all:er=known_2985 on theBenchmark for (2985ds/156Mi)
% 41.51/6.79 % (3338729)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2614534453:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 41.51/6.79 % (3338730)Instruction limit reached!
% 41.51/6.79 % (3338730)------------------------------
% 41.51/6.79 % (3338730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338730)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338730)Termination reason: Instruction limit
% 41.51/6.79 % (3338730)Termination phase: Saturation
% 41.51/6.79 % (3338730)Time elapsed: 0.049 s
% 41.51/6.79 % (3338730)Peak memory usage: 88 MB
% 41.51/6.79 % (3338730)Instructions burned: 159 (million)
% 41.51/6.79 % (3338729)Instruction limit reached!
% 41.51/6.79 % (3338729)------------------------------
% 41.51/6.79 % (3338729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338729)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338729)Termination reason: Instruction limit
% 41.51/6.79 % (3338729)Termination phase: Saturation
% 41.51/6.79 % (3338729)Time elapsed: 0.159 s
% 41.51/6.79 % (3338729)Peak memory usage: 90 MB
% 41.51/6.79 % (3338729)Instructions burned: 265 (million)
% 41.51/6.79 % (3338733)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=636115955:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 41.51/6.79 % (3338734)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=964629930:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 41.51/6.79 % (3338734)Refutation not found, incomplete strategy
% 41.51/6.79 % (3338734)------------------------------
% 41.51/6.79 % (3338734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338734)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338734)Termination reason: Refutation not found, incomplete strategy
% 41.51/6.79 % (3338734)Time elapsed: 0.005 s
% 41.51/6.79 % (3338734)Peak memory usage: 87 MB
% 41.51/6.79 % (3338734)Instructions burned: 8 (million)
% 41.51/6.79 % (3338734)------------------------------
% 41.51/6.79 % (3338734)------------------------------
% 41.51/6.79 % (3338737)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=376115407:i=180:bd=preordered:av=off_2977 on theBenchmark for (2977ds/180Mi)
% 41.51/6.79 % (3338737)Instruction limit reached!
% 41.51/6.79 % (3338737)------------------------------
% 41.51/6.79 % (3338737)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338737)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338737)Termination reason: Instruction limit
% 41.51/6.79 % (3338737)Termination phase: Saturation
% 41.51/6.79 % (3338737)Time elapsed: 0.092 s
% 41.51/6.79 % (3338737)Peak memory usage: 88 MB
% 41.51/6.79 % (3338737)Instructions burned: 180 (million)
% 41.51/6.79 % (3338739)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=3844279990:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 41.51/6.79 % (3338733)Instruction limit reached!
% 41.51/6.79 % (3338733)------------------------------
% 41.51/6.79 % (3338733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338733)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338733)Termination reason: Instruction limit
% 41.51/6.79 % (3338733)Termination phase: Saturation
% 41.51/6.79 % (3338733)Time elapsed: 0.987 s
% 41.51/6.79 % (3338733)Peak memory usage: 139 MB
% 41.51/6.79 % (3338733)Instructions burned: 3259 (million)
% 41.51/6.79 % (3338741)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3755665657:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 41.51/6.79 % (3338711)Instruction limit reached!
% 41.51/6.79 % (3338711)------------------------------
% 41.51/6.79 % (3338711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338711)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338711)Termination reason: Instruction limit
% 41.51/6.79 % (3338711)Termination phase: Saturation
% 41.51/6.79 % (3338711)Time elapsed: 2.179 s
% 41.51/6.79 % (3338711)Peak memory usage: 150 MB
% 41.51/6.79 % (3338711)Instructions burned: 3394 (million)
% 41.51/6.79 % (3338741)Instruction limit reached!
% 41.51/6.79 % (3338741)------------------------------
% 41.51/6.79 % (3338741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338741)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338741)Termination reason: Instruction limit
% 41.51/6.79 % (3338741)Termination phase: Saturation
% 41.51/6.79 % (3338741)Time elapsed: 0.130 s
% 41.51/6.79 % (3338741)Peak memory usage: 91 MB
% 41.51/6.79 % (3338741)Instructions burned: 415 (million)
% 41.51/6.79 % (3338743)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=452423571:s2pl=no:i=8478:s2at=4:nm=6_2970 on theBenchmark for (2970ds/8478Mi)
% 41.51/6.79 % (3338744)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=4066870394:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2969 on theBenchmark for (2969ds/303Mi)
% 41.51/6.79 % (3338744)Refutation not found, incomplete strategy
% 41.51/6.79 % (3338744)------------------------------
% 41.51/6.79 % (3338744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338744)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338744)Termination reason: Refutation not found, incomplete strategy
% 41.51/6.79 % (3338744)Time elapsed: 0.001 s
% 41.51/6.79 % (3338744)Peak memory usage: 88 MB
% 41.51/6.79 % (3338744)Instructions burned: 1 (million)
% 41.51/6.79 % (3338744)------------------------------
% 41.51/6.79 % (3338744)------------------------------
% 41.51/6.79 % (3338747)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3770285682:st=4:i=720:sd=3:fsr=off:ss=axioms_2966 on theBenchmark for (2966ds/720Mi)
% 41.51/6.79 % (3338747)Refutation not found, incomplete strategy
% 41.51/6.79 % (3338747)------------------------------
% 41.51/6.79 % (3338747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338747)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338747)Termination reason: Refutation not found, incomplete strategy
% 41.51/6.79 % (3338747)Time elapsed: 0.037 s
% 41.51/6.79 % (3338747)Peak memory usage: 89 MB
% 41.51/6.79 % (3338747)Instructions burned: 122 (million)
% 41.51/6.79 % (3338747)------------------------------
% 41.51/6.79 % (3338747)------------------------------
% 41.51/6.79 % (3338749)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2058906573:i=598:bs=on:bd=preordered:av=off:ss=axioms_2963 on theBenchmark for (2963ds/598Mi)
% 41.51/6.79 % (3338749)Refutation not found, incomplete strategy
% 41.51/6.79 % (3338749)------------------------------
% 41.51/6.79 % (3338749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338749)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338749)Termination reason: Refutation not found, incomplete strategy
% 41.51/6.79 % (3338749)Time elapsed: 0.026 s
% 41.51/6.79 % (3338749)Peak memory usage: 88 MB
% 41.51/6.79 % (3338749)Instructions burned: 87 (million)
% 41.51/6.79 % (3338749)------------------------------
% 41.51/6.79 % (3338749)------------------------------
% 41.51/6.79 % (3338751)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1474004186:i=2989:sd=3:ss=axioms:sgt=60_2960 on theBenchmark for (2960ds/2989Mi)
% 41.51/6.79 % (3338720)Instruction limit reached!
% 41.51/6.79 % (3338720)------------------------------
% 41.51/6.79 % (3338720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338720)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338720)Termination reason: Instruction limit
% 41.51/6.79 % (3338720)Termination phase: Saturation
% 41.51/6.79 % (3338720)Time elapsed: 3.301 s
% 41.51/6.79 % (3338720)Peak memory usage: 145 MB
% 41.51/6.79 % (3338720)Instructions burned: 5209 (million)
% 41.51/6.79 % (3338754)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3238734709:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2956 on theBenchmark for (2956ds/1997Mi)
% 41.51/6.79 % (3338751)Instruction limit reached!
% 41.51/6.79 % (3338751)------------------------------
% 41.51/6.79 % (3338751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338751)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338751)Termination reason: Instruction limit
% 41.51/6.79 % (3338751)Termination phase: Saturation
% 41.51/6.79 % (3338751)Time elapsed: 0.940 s
% 41.51/6.79 % (3338751)Peak memory usage: 135 MB
% 41.51/6.79 % (3338751)Instructions burned: 2990 (million)
% 41.51/6.79 % (3338756)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3125978346:i=2088:bd=preordered:av=off_2949 on theBenchmark for (2949ds/2088Mi)
% 41.51/6.79 % (3338599)First to succeed.
% 41.51/6.79 % (3338599)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3338519"
% 41.51/6.79 % (3338756)Instruction limit reached!
% 41.51/6.79 % (3338756)------------------------------
% 41.51/6.79 % (3338756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.51/6.79 % (3338756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.51/6.79 % (3338756)CaDiCaL version: 2.1.3
% 41.51/6.79 % (3338756)Termination reason: Instruction limit
% 41.51/6.79 % (3338756)Termination phase: Saturation
% 41.51/6.79 % (3338756)Time elapsed: 0.712 s
% 41.51/6.79 % (3338756)Peak memory usage: 134 MB
% 41.51/6.79 % (3338756)Instructions burned: 2088 (million)
% 41.51/6.79 % (3338599)Refutation found. Thanks to Tanya!
% 41.51/6.79 % SZS status Unsatisfiable for theBenchmark
% 41.51/6.79 % SZS output start Proof for theBenchmark
% See solution above
% 42.29/6.99 % (3338599)------------------------------
% 42.29/6.99 % (3338599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.29/6.99 % (3338599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.29/6.99 % (3338599)CaDiCaL version: 2.1.3
% 42.29/6.99 % (3338599)Termination reason: Refutation
% 42.29/6.99 % (3338599)Time elapsed: 5.460 s
% 42.29/6.99 % (3338599)Peak memory usage: 197 MB
% 42.29/6.99 % (3338599)Instructions burned: 8579 (million)
% 42.29/6.99 % (3338599)------------------------------
% 42.29/6.99 % (3338599)------------------------------
% 42.29/6.99 % (3338519)Success in time 5.9 s
% 42.29/6.99 % Vampire exiting
%------------------------------------------------------------------------------