%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW225+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 01:39:39 PM UTC 2026
% Result : Theorem 12.17s 2.09s
% Output : Refutation 12.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of formulae : 44 ( 26 unt; 0 def)
% Number of atoms : 66 ( 13 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 43 ( 21 ~; 17 |; 0 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-3 aty)
% Number of variables : 41 ( 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096N1_A_L_AN2_A_060_061_Af_A_IN1_A_L_AN2_J_096) ).
fof(f19,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0)
=> ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)
=> X1 = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__antisym) ).
fof(f80,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__le__linear) ).
fof(f81,axiom,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__le__refl) ).
fof(f309,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X1),X0)
=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__le__lessD) ).
fof(f314,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,c_Nat_OSuc(X0))
<=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__Suc__eq__le) ).
fof(f323,axiom,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__eq__plus1__left) ).
fof(f366,axiom,
! [X0] : c_RComplete_Onatceiling(hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_natceiling__real__of__nat) ).
fof(f399,axiom,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0))
=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(X1),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_natceiling__le) ).
fof(f595,axiom,
c_RealDef_Oreal(tc_Nat_Onat) = c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__eq__of__nat) ).
fof(f1269,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1270,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
inference(negated_conjecture,[status(cth)],[f1269]) ).
fof(f1281,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
inference(flattening,[],[f1270]) ).
fof(f1299,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0) ),
inference(ennf_transformation,[],[f19]) ).
fof(f1300,plain,
! [X0,X1] :
( X1 = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0) ),
inference(flattening,[],[f1299]) ).
fof(f1602,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X1),X0) ),
inference(ennf_transformation,[],[f309]) ).
fof(f1684,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(X1),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0)) ),
inference(ennf_transformation,[],[f399]) ).
fof(f2336,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),
inference(cnf_transformation,[],[f3]) ).
fof(f2354,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f1300]) ).
fof(f2434,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
fof(f2435,plain,
! [X0] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X0),
inference(cnf_transformation,[],[f81]) ).
fof(f2755,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X1),X0)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[],[f1602]) ).
fof(f2763,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,c_Nat_OSuc(X0)) ),
inference(cnf_transformation,[],[f314]) ).
fof(f2777,plain,
! [X0] : c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0),
inference(cnf_transformation,[],[f323]) ).
fof(f2842,plain,
! [X0] : c_RComplete_Onatceiling(hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0)) = X0,
inference(cnf_transformation,[],[f366]) ).
fof(f2883,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0))
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(X1),X0) ),
inference(cnf_transformation,[],[f1684]) ).
fof(f3157,plain,
c_RealDef_Oreal(tc_Nat_Onat) = c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),
inference(cnf_transformation,[],[f595]) ).
fof(f4054,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
inference(cnf_transformation,[],[f1281]) ).
fof(f4134,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X1),X0)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(definition_unfolding,[],[f2755,f2777]) ).
fof(f4141,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),X0))
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0) ),
inference(definition_unfolding,[],[f2763,f2777]) ).
fof(f4245,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
inference(definition_unfolding,[],[f4054,f2777,f2777]) ).
fof(f4425,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
inference(superposition,[],[f4245,f3157]) ).
fof(f4439,plain,
! [X0] : c_RComplete_Onatceiling(hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),X0)) = X0,
inference(forward_demodulation,[],[f2842,f3157]) ).
fof(f4461,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(resolution,[],[f2434,f4245]) ).
fof(f4463,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(forward_demodulation,[],[f4461,f3157]) ).
fof(f7088,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X1,hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),X0))
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(X1),X0) ),
inference(forward_demodulation,[],[f2883,f3157]) ).
fof(f8327,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_RComplete_Onatceiling(hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),
inference(resolution,[],[f7088,f4463]) ).
fof(f8353,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),
inference(forward_demodulation,[],[f8327,f4439]) ).
fof(f8958,plain,
c_Orderings_Oord__class_Oless(tc_Nat_Onat,hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),
inference(resolution,[],[f8353,f4134]) ).
fof(f9049,plain,
c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),
inference(resolution,[],[f8958,f4141]) ).
fof(f9056,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))
| c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____) = hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)) ),
inference(resolution,[],[f9049,f2354]) ).
fof(f9065,plain,
c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____) = hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),
inference(forward_subsumption_resolution,[],[f9056,f2336]) ).
fof(f9071,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_Nat_Osemiring__1__class_Oof__nat(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
inference(superposition,[],[f4425,f9065]) ).
fof(f9081,plain,
$false,
inference(forward_subsumption_resolution,[],[f9071,f2435]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW225+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n008.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 13:19:39 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.24/0.28 Running first-order model finding
% 0.24/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.17/2.08 % (2245303)Will run a generic schedule for satisfiability detection.
% 12.17/2.08 % (2245313)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2891992025:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 12.17/2.08 % (2245310)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2745268802:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 12.17/2.08 % (2245309)% WARNING: option uhcvi not known.
% 12.17/2.08 % (2245314)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2801277532:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 12.17/2.08 % (2245308)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=35161142_2999 on theBenchmark for (2999ds/0Mi)
% 12.17/2.08 % (2245309)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2929843047:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 12.17/2.08 % (2245311)dis+10_1_sil=32000:sp=arity:random_seed=1413839692:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 12.17/2.08 % (2245312)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4011015451:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 12.17/2.08 % (2245313)Instruction limit reached!
% 12.17/2.08 % (2245313)------------------------------
% 12.17/2.08 % (2245313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245313)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245313)Termination reason: Instruction limit
% 12.17/2.08 % (2245313)Termination phase: Saturation
% 12.17/2.08 % (2245313)Time elapsed: 0.062 s
% 12.17/2.08 % (2245313)Peak memory usage: 15 MB
% 12.17/2.08 % (2245313)Instructions burned: 132 (million)
% 12.17/2.08 % (2245322)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2121827834:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 12.17/2.08 % (2245311)Instruction limit reached!
% 12.17/2.08 % (2245311)------------------------------
% 12.17/2.08 % (2245311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245311)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245311)Termination reason: Instruction limit
% 12.17/2.08 % (2245311)Termination phase: Saturation
% 12.17/2.08 % (2245311)Time elapsed: 0.084 s
% 12.17/2.08 % (2245311)Peak memory usage: 14 MB
% 12.17/2.08 % (2245311)Instructions burned: 103 (million)
% 12.17/2.08 % (2245312)Instruction limit reached!
% 12.17/2.08 % (2245312)------------------------------
% 12.17/2.08 % (2245312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245312)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245312)Termination reason: Instruction limit
% 12.17/2.08 % (2245312)Termination phase: Saturation
% 12.17/2.08 % (2245312)Time elapsed: 0.100 s
% 12.17/2.08 % (2245312)Peak memory usage: 14 MB
% 12.17/2.08 % (2245312)Instructions burned: 116 (million)
% 12.17/2.08 % (2245325)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2300689545:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 12.17/2.08 % (2245326)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2742661848:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 12.17/2.08 % (2245314)Instruction limit reached!
% 12.17/2.08 % (2245314)------------------------------
% 12.17/2.08 % (2245314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245314)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245314)Termination reason: Instruction limit
% 12.17/2.08 % (2245314)Termination phase: Saturation
% 12.17/2.08 % (2245314)Time elapsed: 0.153 s
% 12.17/2.08 % (2245314)Peak memory usage: 16 MB
% 12.17/2.08 % (2245314)Instructions burned: 159 (million)
% 12.17/2.08 % (2245330)ott-21_1_sil=16000:fs=off:random_seed=3448844621:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 12.17/2.08 % (2245325)Instruction limit reached!
% 12.17/2.08 % (2245325)------------------------------
% 12.17/2.08 % (2245325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245325)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245325)Termination reason: Instruction limit
% 12.17/2.08 % (2245325)Termination phase: Saturation
% 12.17/2.08 % (2245325)Time elapsed: 0.089 s
% 12.17/2.08 % (2245325)Peak memory usage: 15 MB
% 12.17/2.08 % (2245325)Instructions burned: 132 (million)
% 12.17/2.08 % (2245332)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=691995138:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 12.17/2.08 % (2245330)Instruction limit reached!
% 12.17/2.08 % (2245330)------------------------------
% 12.17/2.08 % (2245330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.08 % (2245330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.08 % (2245330)CaDiCaL version: 2.1.3
% 12.17/2.08 % (2245330)Termination reason: Instruction limit
% 12.17/2.08 % (2245330)Termination phase: Saturation
% 12.17/2.08 % (2245330)Time elapsed: 0.162 s
% 12.17/2.08 % (2245330)Peak memory usage: 14 MB
% 12.17/2.08 % (2245330)Instructions burned: 180 (million)
% 12.17/2.08 % (2245334)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3670901936:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 12.17/2.09 % TRYING [1]
% 12.17/2.09 % (2245322)Instruction limit reached!
% 12.17/2.09 % (2245322)------------------------------
% 12.17/2.09 % (2245322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245322)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245322)Termination reason: Instruction limit
% 12.17/2.09 % (2245322)Termination phase: Finite model building constraint generation
% 12.17/2.09 % (2245322)Time elapsed: 0.329 s
% 12.17/2.09 % (2245322)Peak memory usage: 23 MB
% 12.17/2.09 % (2245322)Instructions burned: 715 (million)
% 12.17/2.09 % (2245336)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1999501186:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 12.17/2.09 % TRYING [1]
% 12.17/2.09 % (2245326)Instruction limit reached!
% 12.17/2.09 % (2245326)------------------------------
% 12.17/2.09 % (2245326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245326)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245326)Termination reason: Instruction limit
% 12.17/2.09 % (2245326)Termination phase: Saturation
% 12.17/2.09 % (2245326)Time elapsed: 0.536 s
% 12.17/2.09 % (2245326)Peak memory usage: 16 MB
% 12.17/2.09 % (2245326)Instructions burned: 684 (million)
% 12.17/2.09 % (2245338)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1407418044:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 12.17/2.09 % TRYING [2]
% 12.17/2.09 % (2245332)Instruction limit reached!
% 12.17/2.09 % (2245332)------------------------------
% 12.17/2.09 % (2245332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245332)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245332)Termination reason: Instruction limit
% 12.17/2.09 % (2245332)Termination phase: Saturation
% 12.17/2.09 % (2245332)Time elapsed: 0.516 s
% 12.17/2.09 % (2245332)Peak memory usage: 17 MB
% 12.17/2.09 % (2245332)Instructions burned: 478 (million)
% 12.17/2.09 % (2245340)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3139483679:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 12.17/2.09 % TRYING [1]
% 12.17/2.09 % TRYING [3]
% 12.17/2.09 % (2245336)Instruction limit reached!
% 12.17/2.09 % (2245336)------------------------------
% 12.17/2.09 % (2245336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245336)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245336)Termination reason: Instruction limit
% 12.17/2.09 % (2245336)Termination phase: Saturation
% 12.17/2.09 % (2245336)Time elapsed: 0.643 s
% 12.17/2.09 % (2245336)Peak memory usage: 22 MB
% 12.17/2.09 % (2245336)Instructions burned: 1180 (million)
% 12.17/2.09 % (2245342)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2503943895:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 12.17/2.09 % TRYING [2]
% 12.17/2.09 % (2245334)Instruction limit reached!
% 12.17/2.09 % (2245334)------------------------------
% 12.17/2.09 % (2245334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245334)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245334)Termination reason: Instruction limit
% 12.17/2.09 % (2245334)Termination phase: Finite model building constraint generation
% 12.17/2.09 % (2245334)Time elapsed: 0.738 s
% 12.17/2.09 % (2245334)Peak memory usage: 32 MB
% 12.17/2.09 % (2245334)Instructions burned: 866 (million)
% 12.17/2.09 % (2245344)fmb+10_1_sil=64000:random_seed=3453823514:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 12.17/2.09 % (2245340)Instruction limit reached!
% 12.17/2.09 % (2245340)------------------------------
% 12.17/2.09 % (2245340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245340)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245340)Termination reason: Instruction limit
% 12.17/2.09 % (2245340)Termination phase: Saturation
% 12.17/2.09 % (2245340)Time elapsed: 0.615 s
% 12.17/2.09 % (2245340)Peak memory usage: 19 MB
% 12.17/2.09 % (2245340)Instructions burned: 692 (million)
% 12.17/2.09 % (2245346)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4229528230:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 12.17/2.09 % (2245338)Instruction limit reached!
% 12.17/2.09 % (2245338)------------------------------
% 12.17/2.09 % (2245338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245338)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245338)Termination reason: Instruction limit
% 12.17/2.09 % (2245338)Termination phase: Finite model building constraint generation
% 12.17/2.09 % (2245338)Time elapsed: 0.783 s
% 12.17/2.09 % (2245338)Peak memory usage: 49 MB
% 12.17/2.09 % (2245338)Instructions burned: 890 (million)
% 12.17/2.09 % (2245342)Instruction limit reached!
% 12.17/2.09 % (2245342)------------------------------
% 12.17/2.09 % (2245342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245342)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245342)Termination reason: Instruction limit
% 12.17/2.09 % (2245342)Termination phase: Saturation
% 12.17/2.09 % (2245342)Time elapsed: 0.417 s
% 12.17/2.09 % (2245342)Peak memory usage: 21 MB
% 12.17/2.09 % (2245342)Instructions burned: 881 (million)
% 12.17/2.09 % (2245348)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=396177876:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 12.17/2.09 % (2245349)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=624779009:i=5131_2983 on theBenchmark for (2983ds/5131Mi)
% 12.17/2.09 % (2245349) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2245303-2245349"...
% 12.17/2.09 % (2245349)...printing done.
% 12.17/2.09 % (2245349)Refutation found. Thanks to Tanya!
% 12.17/2.09 % SZS status Theorem for theBenchmark
% 12.17/2.09 % SZS output start Proof for theBenchmark
% See solution above
% 12.17/2.09 % (2245349)------------------------------
% 12.17/2.09 % (2245349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.17/2.09 % (2245349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.17/2.09 % (2245349)CaDiCaL version: 2.1.3
% 12.17/2.09 % (2245349)Termination reason: Refutation
% 12.17/2.09 % (2245349)Time elapsed: 0.136 s
% 12.17/2.09 % (2245349)Peak memory usage: 16 MB
% 12.17/2.09 % (2245349)Instructions burned: 261 (million)
% 12.17/2.09 % (2245303)Success in time 1.792 s
% 12.17/2.09 % Vampire exiting
%------------------------------------------------------------------------------