%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : HEN010-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:09 AM UTC 2026
% Result : Unsatisfiable 11.00s 3.01s
% Output : Refutation 13.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 15
% Syntax : Number of formulae : 97 ( 36 unt; 2 def)
% Number of atoms : 199 ( 32 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 206 ( 104 ~; 100 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% Number of variables : 119 ( 0 sgn 119 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( quotient(X0,X1,zero)
| ~ less_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quotient_less_equal) ).
fof(f2,axiom,
! [X0,X1] :
( ~ quotient(X0,X1,zero)
| less_equal(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_equal_quotient) ).
fof(f3,axiom,
! [X2,X0,X1] :
( ~ quotient(X0,X1,X2)
| less_equal(X2,X0) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',quotient_property) ).
fof(f5,axiom,
! [X0] : less_equal(zero,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zero_is_smallest) ).
fof(f6,axiom,
! [X0,X1] :
( ~ less_equal(X1,X0)
| ~ less_equal(X0,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_equal_and_equal) ).
fof(f7,axiom,
! [X0] : less_equal(X0,identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_is_largest) ).
fof(f8,axiom,
! [X0,X1] : quotient(X0,X1,divide(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure) ).
fof(f9,axiom,
! [X2,X3,X0,X1] :
( ~ quotient(X0,X1,X3)
| ~ quotient(X0,X1,X2)
| X2 = X3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',well_defined) ).
fof(f10,axiom,
quotient(identity,a,idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_a) ).
fof(f11,axiom,
quotient(identity,idQa,idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQa) ).
fof(f12,axiom,
quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',identity_divide_idQ_idQa) ).
fof(f13,negated_conjecture,
idQa != idQa_Q__idQ_idQa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_idQa_equals_idQa_Q__idQ_idQa) ).
fof(f17,plain,
! [X2,X0,X1] :
( ~ quotient(X0,X1,X2)
| divide(X0,X1) = X2 ),
inference(resolution,[],[f8,f9]) ).
fof(f21,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(f23,plain,
less_equal(idQa_Q__idQ_idQa,idQa),
inference(resolution,[],[f3,f12]) ).
fof(f26,plain,
! [X0,X1] : less_equal(divide(X0,X1),X0),
inference(resolution,[],[f3,f8]) ).
fof(f27,plain,
( ~ less_equal(idQa,idQa_Q__idQ_idQa)
| idQa = idQa_Q__idQ_idQa ),
inference(resolution,[],[f23,f6]) ).
fof(f28,plain,
~ less_equal(idQa,idQa_Q__idQ_idQa),
inference(forward_subsumption_resolution,[],[f27,f13]) ).
fof(f33,plain,
! [X0,X1] :
( ~ less_equal(X0,divide(X0,X1))
| divide(X0,X1) = X0 ),
inference(resolution,[],[f26,f6]) ).
fof(f37,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,[],[f21,f8]) ).
fof(f38,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,[],[f21,f1]) ).
fof(f43,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,[],[f37,f1]) ).
fof(f52,plain,
idQ_idQa = divide(identity,idQa),
inference(resolution,[],[f17,f11]) ).
fof(f53,plain,
idQa = divide(identity,a),
inference(resolution,[],[f17,f10]) ).
fof(f55,plain,
! [X0,X1] :
( ~ less_equal(X0,X1)
| zero = divide(X0,X1) ),
inference(resolution,[],[f17,f1]) ).
fof(f77,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,[],[f43,f8]) ).
fof(f79,plain,
! [X0] :
( less_equal(divide(divide(idQa,X0),zero),divide(idQa_Q__idQ_idQa,X0))
| ~ less_equal(idQ_idQa,X0) ),
inference(resolution,[],[f77,f12]) ).
fof(f184,plain,
! [X0] :
( ~ less_equal(X0,zero)
| zero = X0 ),
inference(resolution,[],[f5,f6]) ).
fof(f185,plain,
! [X0] : zero = divide(zero,X0),
inference(resolution,[],[f5,f33]) ).
fof(f219,plain,
! [X0,X1] : zero = divide(divide(X0,X1),X0),
inference(resolution,[],[f55,f26]) ).
fof(f261,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,[],[f38,f8]) ).
fof(f267,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,[],[f261,f8]) ).
fof(f270,plain,
! [X0,X1] :
( ~ quotient(identity,X0,X1)
| less_equal(divide(idQ_idQa,divide(X0,idQa)),zero)
| ~ less_equal(X1,idQa) ),
inference(resolution,[],[f261,f11]) ).
fof(f273,plain,
! [X2,X0,X1] :
( less_equal(divide(divide(X0,X1),divide(X2,X1)),zero)
| ~ less_equal(divide(X0,X2),X1) ),
inference(resolution,[],[f267,f8]) ).
fof(f274,plain,
! [X2,X0,X1] :
( less_equal(divide(divide(X0,X1),divide(X2,X1)),zero)
| ~ less_equal(zero,X1)
| ~ less_equal(X0,X2) ),
inference(resolution,[],[f267,f1]) ).
fof(f276,plain,
! [X0] :
( less_equal(divide(divide(identity,X0),divide(idQa,X0)),zero)
| ~ less_equal(idQ_idQa,X0) ),
inference(resolution,[],[f267,f11]) ).
fof(f280,plain,
! [X2,X0,X1] :
( less_equal(divide(divide(X0,X1),divide(X2,X1)),zero)
| ~ less_equal(X0,X2) ),
inference(forward_subsumption_resolution,[],[f274,f5]) ).
fof(f283,plain,
! [X2,X0,X1] :
( ~ less_equal(divide(X0,X1),X2)
| ~ less_equal(zero,divide(divide(X0,X2),divide(X1,X2)))
| zero = divide(divide(X0,X2),divide(X1,X2)) ),
inference(resolution,[],[f273,f6]) ).
fof(f297,plain,
! [X2,X0,X1] :
( ~ less_equal(divide(X0,X1),X2)
| zero = divide(divide(X0,X2),divide(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f283,f5]) ).
fof(f300,plain,
! [X0,X1] : zero = divide(divide(X0,X0),divide(X1,X0)),
inference(resolution,[],[f297,f26]) ).
fof(f334,plain,
! [X0,X1] : quotient(divide(X0,X0),divide(X1,X0),zero),
inference(superposition,[],[f8,f300]) ).
fof(f448,plain,
! [X0,X1] : less_equal(divide(X0,X0),divide(X1,X0)),
inference(resolution,[],[f334,f2]) ).
fof(f478,plain,
! [X0] : divide(X0,X0) = divide(divide(X0,X0),X0),
inference(resolution,[],[f448,f33]) ).
fof(f491,plain,
! [X0] : zero = divide(X0,X0),
inference(forward_demodulation,[],[f478,f219]) ).
fof(f492,plain,
! [X0] : quotient(X0,X0,zero),
inference(superposition,[],[f8,f491]) ).
fof(f545,plain,
! [X0] : less_equal(X0,X0),
inference(resolution,[],[f492,f2]) ).
fof(f569,plain,
! [X2,X0,X1] :
( ~ less_equal(X0,X1)
| ~ less_equal(zero,divide(divide(X0,X2),divide(X1,X2)))
| zero = divide(divide(X0,X2),divide(X1,X2)) ),
inference(resolution,[],[f280,f6]) ).
fof(f594,plain,
! [X2,X0,X1] :
( ~ less_equal(X0,X1)
| zero = divide(divide(X0,X2),divide(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f569,f5]) ).
fof(f595,plain,
! [X0,X1] : zero = divide(divide(X0,X1),divide(identity,X1)),
inference(resolution,[],[f594,f7]) ).
fof(f630,plain,
! [X0,X1] : quotient(divide(X0,X1),divide(identity,X1),zero),
inference(superposition,[],[f8,f595]) ).
fof(f660,plain,
! [X0,X1] : less_equal(divide(X0,X1),divide(identity,X1)),
inference(resolution,[],[f630,f2]) ).
fof(f718,plain,
( less_equal(divide(idQa,divide(idQa,a)),zero)
| ~ less_equal(idQ_idQa,a) ),
inference(superposition,[],[f276,f53]) ).
fof(f727,definition,
( spl0_25
<=> less_equal(idQ_idQa,a) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f728,plain,
( less_equal(idQ_idQa,a)
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f729,plain,
( ~ less_equal(idQ_idQa,a)
| spl0_25 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f731,definition,
( spl0_26
<=> less_equal(divide(idQa,divide(idQa,a)),zero) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f733,plain,
( less_equal(divide(idQa,divide(idQa,a)),zero)
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,plain,
( ~ spl0_25
| spl0_26 ),
inference(avatar_split_clause,[],[f718,f731,f727]) ).
fof(f747,plain,
( less_equal(divide(idQ_idQa,divide(a,idQa)),zero)
| ~ less_equal(idQa,idQa) ),
inference(resolution,[],[f270,f10]) ).
fof(f778,plain,
! [X0] : less_equal(divide(X0,idQa),idQ_idQa),
inference(superposition,[],[f660,f52]) ).
fof(f1260,plain,
less_equal(divide(idQ_idQa,divide(a,idQa)),zero),
inference(forward_subsumption_resolution,[],[f747,f545]) ).
fof(f1263,plain,
zero = divide(idQ_idQa,divide(a,idQa)),
inference(resolution,[],[f1260,f184]) ).
fof(f1274,plain,
quotient(idQ_idQa,divide(a,idQa),zero),
inference(superposition,[],[f8,f1263]) ).
fof(f1403,plain,
less_equal(idQ_idQa,divide(a,idQa)),
inference(resolution,[],[f1274,f2]) ).
fof(f1426,plain,
( ~ less_equal(divide(a,idQa),idQ_idQa)
| idQ_idQa = divide(a,idQa) ),
inference(resolution,[],[f1403,f6]) ).
fof(f1427,plain,
idQ_idQa = divide(a,idQa),
inference(forward_subsumption_resolution,[],[f1426,f778]) ).
fof(f1439,plain,
less_equal(idQ_idQa,a),
inference(superposition,[],[f26,f1427]) ).
fof(f1465,plain,
( $false
| spl0_25 ),
inference(forward_subsumption_resolution,[],[f1439,f729]) ).
fof(f1466,plain,
spl0_25,
inference(avatar_contradiction_clause,[],[f1465]) ).
fof(f1591,plain,
( zero = divide(idQa,divide(idQa,a))
| ~ spl0_26 ),
inference(resolution,[],[f733,f184]) ).
fof(f1604,plain,
( quotient(idQa,divide(idQa,a),zero)
| ~ spl0_26 ),
inference(superposition,[],[f8,f1591]) ).
fof(f1921,plain,
( less_equal(idQa,divide(idQa,a))
| ~ spl0_26 ),
inference(resolution,[],[f1604,f2]) ).
fof(f1942,plain,
( idQa = divide(idQa,a)
| ~ spl0_26 ),
inference(resolution,[],[f1921,f33]) ).
fof(f1956,plain,
( less_equal(divide(idQa,zero),divide(idQa_Q__idQ_idQa,a))
| ~ less_equal(idQ_idQa,a)
| ~ spl0_26 ),
inference(superposition,[],[f79,f1942]) ).
fof(f1987,plain,
( less_equal(divide(idQa,zero),divide(idQa_Q__idQ_idQa,a))
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f1956,f728]) ).
fof(f1988,plain,
( zero = divide(divide(idQa,divide(idQa_Q__idQ_idQa,a)),divide(zero,divide(idQa_Q__idQ_idQa,a)))
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f1987,f297]) ).
fof(f2001,plain,
( zero = divide(divide(idQa,divide(idQa_Q__idQ_idQa,a)),zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_demodulation,[],[f1988,f185]) ).
fof(f2006,plain,
( quotient(divide(idQa,divide(idQa_Q__idQ_idQa,a)),zero,zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(superposition,[],[f8,f2001]) ).
fof(f3935,plain,
( less_equal(divide(idQa,divide(idQa_Q__idQ_idQa,a)),zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f2006,f2]) ).
fof(f3968,plain,
( zero = divide(idQa,divide(idQa_Q__idQ_idQa,a))
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f3935,f184]) ).
fof(f3999,plain,
( ! [X0] :
( ~ less_equal(zero,X0)
| zero = divide(divide(idQa,X0),divide(divide(idQa_Q__idQ_idQa,a),X0)) )
| ~ spl0_25
| ~ spl0_26 ),
inference(superposition,[],[f297,f3968]) ).
fof(f4015,plain,
( ! [X0] : zero = divide(divide(idQa,X0),divide(divide(idQa_Q__idQ_idQa,a),X0))
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f3999,f5]) ).
fof(f4040,plain,
( zero = divide(divide(idQa,idQa_Q__idQ_idQa),zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(superposition,[],[f4015,f219]) ).
fof(f4098,plain,
( quotient(divide(idQa,idQa_Q__idQ_idQa),zero,zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(superposition,[],[f8,f4040]) ).
fof(f4133,plain,
( less_equal(divide(idQa,idQa_Q__idQ_idQa),zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f4098,f2]) ).
fof(f4162,plain,
( zero = divide(idQa,idQa_Q__idQ_idQa)
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f4133,f184]) ).
fof(f4182,plain,
( quotient(idQa,idQa_Q__idQ_idQa,zero)
| ~ spl0_25
| ~ spl0_26 ),
inference(superposition,[],[f8,f4162]) ).
fof(f4281,plain,
( less_equal(idQa,idQa_Q__idQ_idQa)
| ~ spl0_25
| ~ spl0_26 ),
inference(resolution,[],[f4182,f2]) ).
fof(f4305,plain,
( $false
| ~ spl0_25
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f4281,f28]) ).
fof(f4306,plain,
( ~ spl0_25
| ~ spl0_26 ),
inference(avatar_contradiction_clause,[],[f4305]) ).
cnf(s14,plain,
( ~ spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f734]) ).
cnf(s22,plain,
spl0_25,
inference(sat_conversion,[],[f1466]) ).
cnf(s48,plain,
( ~ spl0_25
| ~ spl0_26 ),
inference(sat_conversion,[],[f4306]) ).
cnf(s51,plain,
~ spl0_26,
inference(rat,[],[s48,s22]) ).
cnf(s53,plain,
$false,
inference(rat,[],[s14,s51,s22]) ).
fof(f4308,plain,
$false,
inference(avatar_sat_refutation,[],[s53]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HEN010-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.48 % Computer : n006.cluster.edu
% 0.24/0.48 % Model : x86_64 x86_64
% 0.24/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.24/0.48 % Memory : 8046.5625MB
% 0.24/0.48 % OS : Linux 6.8.0-71-generic
% 0.24/0.48 % CPULimit : 300
% 0.24/0.48 % WCLimit : 300
% 0.24/0.48 % DateTime : Sun Sep 27 10:50:41 UTC 2026
% 0.24/0.49 % CPUTime :
% 0.24/0.49 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.27/0.54 Running first-order theorem proving
% 0.27/0.54 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.00/3.00 % (2800798)Input is clausal, will run a generic CNF schedule.
% 11.00/3.00 % (2800807)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1378370426:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.00/3.00 % (2800807)Refutation not found, incomplete strategy
% 11.00/3.00 % (2800807)------------------------------
% 11.00/3.00 % (2800807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800807)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800807)Termination reason: Refutation not found, incomplete strategy
% 11.00/3.00 % (2800807)Time elapsed: 0.013 s
% 11.00/3.00 % (2800807)Peak memory usage: 88 MB
% 11.00/3.00 % (2800807)Instructions burned: 20 (million)
% 11.00/3.00 % (2800803)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=2653442769:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.00/3.00 % (2800804)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1885715697:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.00/3.00 % (2800805)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1294734426:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.00/3.00 % (2800806)lrs+10_1_sil=8000:sp=occurrence:random_seed=683576213:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.00/3.00 % (2800806)Refutation not found, incomplete strategy
% 11.00/3.00 % (2800806)------------------------------
% 11.00/3.00 % (2800806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800806)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800806)Termination reason: Refutation not found, incomplete strategy
% 11.00/3.00 % (2800806)Time elapsed: 0.006 s
% 11.00/3.00 % (2800806)Peak memory usage: 88 MB
% 11.00/3.00 % (2800806)Instructions burned: 4 (million)
% 11.00/3.00 % (2800809)dis-21_1_sil=8000:lcm=predicate:random_seed=907304858: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)
% 11.00/3.00 % (2800808)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=892913514:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.00/3.00 % (2800809)Instruction limit reached!
% 11.00/3.00 % (2800809)------------------------------
% 11.00/3.00 % (2800809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800809)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800809)Termination reason: Instruction limit
% 11.00/3.00 % (2800809)Termination phase: Saturation
% 11.00/3.00 % (2800809)Time elapsed: 0.093 s
% 11.00/3.00 % (2800809)Peak memory usage: 88 MB
% 11.00/3.00 % (2800809)Instructions burned: 117 (million)
% 11.00/3.00 % (2800808)Instruction limit reached!
% 11.00/3.00 % (2800808)------------------------------
% 11.00/3.00 % (2800808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800808)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800808)Termination reason: Instruction limit
% 11.00/3.00 % (2800808)Termination phase: Saturation
% 11.00/3.00 % (2800808)Time elapsed: 0.153 s
% 11.00/3.00 % (2800808)Peak memory usage: 88 MB
% 11.00/3.00 % (2800808)Instructions burned: 181 (million)
% 11.00/3.00 % (2800807)------------------------------
% 11.00/3.00 % (2800807)------------------------------
% 11.00/3.00 % (2800817)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=3885941096:i=143:sd=2:aac=none:ss=axioms:sgt=16_2995 on theBenchmark for (2995ds/143Mi)
% 11.00/3.00 % (2800817)Refutation not found, incomplete strategy
% 11.00/3.00 % (2800817)------------------------------
% 11.00/3.00 % (2800817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800817)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800817)Termination reason: Refutation not found, incomplete strategy
% 11.00/3.00 % (2800817)Time elapsed: 0.010 s
% 11.00/3.00 % (2800817)Peak memory usage: 88 MB
% 11.00/3.00 % (2800817)Instructions burned: 7 (million)
% 11.00/3.00 % (2800806)------------------------------
% 11.00/3.00 % (2800806)------------------------------
% 11.00/3.00 % (2800818)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4005094819:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2995 on theBenchmark for (2995ds/189Mi)
% 11.00/3.00 % (2800818)Instruction limit reached!
% 11.00/3.00 % (2800818)------------------------------
% 11.00/3.00 % (2800818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800818)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800818)Termination reason: Instruction limit
% 11.00/3.00 % (2800818)Termination phase: Saturation
% 11.00/3.00 % (2800818)Time elapsed: 0.092 s
% 11.00/3.00 % (2800818)Peak memory usage: 89 MB
% 11.00/3.00 % (2800818)Instructions burned: 191 (million)
% 11.00/3.00 % (2800819)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1740300052:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 11.00/3.00 % (2800819)Refutation not found, incomplete strategy
% 11.00/3.00 % (2800819)------------------------------
% 11.00/3.00 % (2800819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.00 % (2800819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.00 % (2800819)CaDiCaL version: 2.1.3
% 11.00/3.00 % (2800819)Termination reason: Refutation not found, incomplete strategy
% 11.00/3.00 % (2800819)Time elapsed: 0.007 s
% 11.00/3.00 % (2800819)Peak memory usage: 88 MB
% 11.00/3.00 % (2800819)Instructions burned: 4 (million)
% 11.00/3.00 % (2800823)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3811090443:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 11.00/3.00 % (2800822)lrs+10_64_to=lpo:sil=8000:random_seed=180511261:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 11.00/3.00 % (2800817)------------------------------
% 11.00/3.00 % (2800817)------------------------------
% 11.00/3.00 % (2800823)Instruction limit reached!
% 11.00/3.00 % (2800823)------------------------------
% 11.00/3.00 % (2800823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.01 % (2800823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.01 % (2800823)CaDiCaL version: 2.1.3
% 11.00/3.01 % (2800823)Termination reason: Instruction limit
% 11.00/3.01 % (2800823)Termination phase: Saturation
% 11.00/3.01 % (2800823)Time elapsed: 0.099 s
% 11.00/3.01 % (2800823)Peak memory usage: 88 MB
% 11.00/3.01 % (2800823)Instructions burned: 196 (million)
% 11.00/3.01 % (2800822)Instruction limit reached!
% 11.00/3.01 % (2800822)------------------------------
% 11.00/3.01 % (2800822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.01 % (2800822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.01 % (2800822)CaDiCaL version: 2.1.3
% 11.00/3.01 % (2800822)Termination reason: Instruction limit
% 11.00/3.01 % (2800822)Termination phase: Saturation
% 11.00/3.01 % (2800822)Time elapsed: 0.132 s
% 11.00/3.01 % (2800822)Peak memory usage: 89 MB
% 11.00/3.01 % (2800822)Instructions burned: 126 (million)
% 11.00/3.01 % (2800819)------------------------------
% 11.00/3.01 % (2800819)------------------------------
% 11.00/3.01 % (2800827)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=992550973:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 11.00/3.01 % (2800828)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=33743311:i=3394:sd=4:ss=included:sgt=64_2988 on theBenchmark for (2988ds/3394Mi)
% 11.00/3.01 % (2800829)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=215324997:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 11.00/3.01 % (2800803)First to succeed.
% 11.00/3.01 % (2800803)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2800798"
% 11.00/3.01 % (2800827)Instruction limit reached!
% 11.00/3.01 % (2800827)------------------------------
% 11.00/3.01 % (2800827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.01 % (2800827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.01 % (2800827)CaDiCaL version: 2.1.3
% 11.00/3.01 % (2800827)Termination reason: Instruction limit
% 11.00/3.01 % (2800827)Termination phase: Saturation
% 11.00/3.01 % (2800827)Time elapsed: 0.166 s
% 11.00/3.01 % (2800827)Peak memory usage: 90 MB
% 11.00/3.01 % (2800827)Instructions burned: 157 (million)
% 11.00/3.01 % (2800830)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2252494094:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 11.00/3.01 % (2800830)Refutation not found, incomplete strategy
% 11.00/3.01 % (2800830)------------------------------
% 11.00/3.01 % (2800830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.01 % (2800830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.01 % (2800830)CaDiCaL version: 2.1.3
% 11.00/3.01 % (2800830)Termination reason: Refutation not found, incomplete strategy
% 11.00/3.01 % (2800830)Time elapsed: 0.027 s
% 11.00/3.01 % (2800830)Peak memory usage: 88 MB
% 11.00/3.01 % (2800830)Instructions burned: 25 (million)
% 11.00/3.01 % (2800829)Instruction limit reached!
% 11.00/3.01 % (2800829)------------------------------
% 11.00/3.01 % (2800829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.00/3.01 % (2800829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.00/3.01 % (2800829)CaDiCaL version: 2.1.3
% 11.00/3.01 % (2800829)Termination reason: Instruction limit
% 11.00/3.01 % (2800829)Termination phase: Saturation
% 11.00/3.01 % (2800829)Time elapsed: 0.109 s
% 11.00/3.01 % (2800829)Peak memory usage: 88 MB
% 11.00/3.01 % (2800829)Instructions burned: 107 (million)
% 11.00/3.01 % (2800803)Refutation found. Thanks to Tanya!
% 11.00/3.01 % SZS status Unsatisfiable for theBenchmark
% 11.00/3.01 % SZS output start Proof for theBenchmark
% See solution above
% 13.03/3.39 % (2800803)------------------------------
% 13.03/3.39 % (2800803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.03/3.39 % (2800803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.03/3.39 % (2800803)CaDiCaL version: 2.1.3
% 13.03/3.39 % (2800803)Termination reason: Refutation
% 13.03/3.39 % (2800803)Time elapsed: 1.168 s
% 13.03/3.39 % (2800803)Peak memory usage: 132 MB
% 13.03/3.39 % (2800803)Instructions burned: 1325 (million)
% 13.03/3.39 % (2800803)------------------------------
% 13.03/3.39 % (2800803)------------------------------
% 13.03/3.39 % (2800798)Success in time 1.703 s
% 13.03/3.39 % Vampire exiting
%------------------------------------------------------------------------------