%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWX242-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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:46:50 PM UTC 2026
% Result : Unsatisfiable 8.99s 1.56s
% Output : Refutation 8.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 26
% Syntax : Number of formulae : 85 ( 77 unt; 0 def)
% Number of atoms : 93 ( 92 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 45 ( 37 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 4 con; 0-8 aty)
% Number of variables : 248 ( 248 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X2,X3,X0,X1,X6,X4,X5] : aux3(X0,X1,X2,X3,X4,X5,X6,btrue) = unifyloop(X0,append(X3,X1),append(X6,X4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_004) ).
fof(f9,axiom,
! [X2,X3,X0,X1,X4] : aux5(X0,X1,X2,X3,X4,btrue) = unifyloop(X0,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
fof(f13,axiom,
! [X2,X0,X1] : aux6(X0,X1,just(X2)) = eq3(subst(X2,X0),subst(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
fof(f20,axiom,
! [X2,X3,X0,X1,X4] : fail(X0,cons(var(X1),X2),X3,X4) = unifyvar(X0,X1,X3,X4,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
fof(f22,axiom,
! [X2,X0,X1] : subst(X0,app(X1,X2)) = app(X1,substList(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
fof(f23,axiom,
! [X0,X1] : subst(X0,var(X1)) = apply1(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_019) ).
fof(f24,axiom,
! [X0] : substList(X0,nil) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_020) ).
fof(f25,plain,
! [X0] : nil = substList(X0,nil),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
! [X2,X0,X1] : substList(X0,cons(X1,X2)) = cons(subst(X0,X1),substList(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
fof(f37,axiom,
! [X0,X1] : unifyoccurs(X0,var(X1)) = eq2(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
fof(f39,axiom,
! [X0] : unifyloop(X0,nil,nil) = just(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
fof(f43,axiom,
! [X2,X3,X0,X1,X6,X4,X5] : unifyloop(X0,cons(app(X1,X2),X3),cons(app(X4,X5),X6)) = aux3(X0,X3,X1,X2,X6,X4,X5,eq2(X1,X4)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_034) ).
fof(f46,axiom,
! [X2,X3,X0,X1,X4] : unifyloop(X0,cons(var(X1),X2),cons(X3,X4)) = unifyvar(X0,X1,X3,X2,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
fof(f48,axiom,
! [X2,X3,X0,X1,X4] : unifyvar(X0,X1,var(X2),X3,X4) = aux5(X0,X1,X3,X4,X2,eq2(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
fof(f50,axiom,
! [X0,X1] : unify2(X0,X1) = unifyloop(lam3,cons(X0,nil),cons(X1,nil)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
fof(f51,axiom,
! [X0,X1] : unificationOK(X0,X1) = aux6(X0,X1,unify2(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
fof(f52,axiom,
! [X0,X1] : prop_unify_makes_equal(X0,X1) = eq4(unificationOK(X0,X1),btrue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
fof(f57,axiom,
! [X0] : append(nil,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_046) ).
fof(f58,axiom,
! [X2,X0,X1] : append(cons(X0,X1),X2) = cons(X0,append(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
fof(f71,axiom,
eq4(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_054) ).
fof(f72,plain,
bfalse = eq4(bfalse,btrue),
inference(reorient_equations,[],[f71]) ).
fof(f75,axiom,
! [X0] : eq2(X0,X0) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
fof(f76,plain,
! [X0] : btrue = eq2(X0,X0),
inference(reorient_equations,[],[f75]) ).
fof(f79,axiom,
! [X0] : eq4(X0,X0) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_058) ).
fof(f80,plain,
! [X0] : btrue = eq4(X0,X0),
inference(reorient_equations,[],[f79]) ).
fof(f83,axiom,
! [X2,X3,X0,X1] :
( eq3(X0,X1) != bfalse
| eq(cons(X0,X2),cons(X1,X3)) = bfalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_060) ).
fof(f84,plain,
! [X2,X3,X0,X1] :
( bfalse != eq3(X0,X1)
| bfalse = eq(cons(X0,X2),cons(X1,X3)) ),
inference(reorient_equations,[],[f83]) ).
fof(f89,axiom,
! [X0,X1] : eq(cons(X0,X1),nil) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_063) ).
fof(f90,plain,
! [X0,X1] : bfalse = eq(cons(X0,X1),nil),
inference(reorient_equations,[],[f89]) ).
fof(f93,axiom,
! [X2,X3,X0,X1] :
( eq2(X0,X1) != btrue
| eq3(app(X0,X2),app(X1,X3)) = eq(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
fof(f94,plain,
! [X2,X3,X0,X1] :
( btrue != eq2(X0,X1)
| eq(X2,X3) = eq3(app(X0,X2),app(X1,X3)) ),
inference(reorient_equations,[],[f93]) ).
fof(f104,axiom,
! [X0] : apply1(lam3,X0) = var(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
fof(f105,plain,
! [X0] : var(X0) = apply1(lam3,X0),
inference(reorient_equations,[],[f104]) ).
fof(f106,negated_conjecture,
! [X0,X1] : eq4(prop_unify_makes_equal(X0,X1),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f107,plain,
! [X0,X1] : btrue != eq4(prop_unify_makes_equal(X0,X1),bfalse),
inference(reorient_equations,[],[f106]) ).
fof(f108,plain,
! [X0,X1] : eq2(X0,X1) = unifyoccurs(X0,apply1(lam3,X1)),
inference(definition_unfolding,[],[f37,f105]) ).
fof(f110,plain,
! [X0,X1] : unificationOK(X0,X1) = aux6(X0,X1,unifyloop(lam3,cons(X0,nil),cons(X1,nil))),
inference(definition_unfolding,[],[f51,f50]) ).
fof(f111,plain,
! [X0,X1] : prop_unify_makes_equal(X0,X1) = eq4(aux6(X0,X1,unifyloop(lam3,cons(X0,nil),cons(X1,nil))),btrue),
inference(definition_unfolding,[],[f52,f110]) ).
fof(f113,plain,
! [X2,X3,X0,X1,X4] : unifyvar(X0,X1,X3,X4,X2) = fail(X0,cons(apply1(lam3,X1),X2),X3,X4),
inference(definition_unfolding,[],[f20,f105]) ).
fof(f115,plain,
! [X0,X1] : apply1(X0,X1) = subst(X0,apply1(lam3,X1)),
inference(definition_unfolding,[],[f23,f105]) ).
fof(f119,plain,
! [X2,X0,X1] : eq3(subst(X2,X0),subst(X2,X1)) = aux6(X0,X1,unifyloop(X2,nil,nil)),
inference(definition_unfolding,[],[f13,f39]) ).
fof(f120,plain,
! [X2,X3,X0,X1,X6,X4,X5] : unifyloop(X0,cons(app(X1,X2),X3),cons(app(X4,X5),X6)) = aux3(X0,X3,X1,X2,X6,X4,X5,unifyoccurs(X1,apply1(lam3,X4))),
inference(definition_unfolding,[],[f43,f108]) ).
fof(f123,plain,
! [X2,X3,X0,X1,X4] : unifyloop(X0,cons(apply1(lam3,X1),X2),cons(X3,X4)) = fail(X0,cons(apply1(lam3,X1),X4),X3,X2),
inference(definition_unfolding,[],[f46,f105,f113]) ).
fof(f125,plain,
! [X2,X3,X0,X1,X4] : fail(X0,cons(apply1(lam3,X1),X4),apply1(lam3,X2),X3) = aux5(X0,X1,X3,X4,X2,unifyoccurs(X1,apply1(lam3,X2))),
inference(definition_unfolding,[],[f48,f113,f105,f108]) ).
fof(f133,plain,
! [X0] : btrue = unifyoccurs(X0,apply1(lam3,X0)),
inference(definition_unfolding,[],[f76,f108]) ).
fof(f135,plain,
! [X2,X3,X0,X1] :
( btrue != unifyoccurs(X0,apply1(lam3,X1))
| eq(X2,X3) = eq3(app(X0,X2),app(X1,X3)) ),
inference(definition_unfolding,[],[f94,f108]) ).
fof(f141,plain,
! [X0,X1] : btrue != eq4(eq4(aux6(X0,X1,unifyloop(lam3,cons(X0,nil),cons(X1,nil))),btrue),bfalse),
inference(definition_unfolding,[],[f107,f111]) ).
fof(f142,plain,
! [X2,X0,X1] : substList(X0,cons(apply1(lam3,X1),X2)) = cons(apply1(X0,X1),substList(X0,X2)),
inference(superposition,[],[f26,f115]) ).
fof(f144,plain,
! [X0,X1] : substList(X0,cons(X1,nil)) = cons(subst(X0,X1),nil),
inference(superposition,[],[f26,f25]) ).
fof(f248,plain,
! [X2,X0,X1] :
( btrue != btrue
| eq(X1,X2) = eq3(app(X0,X1),app(X0,X2)) ),
inference(superposition,[],[f135,f133]) ).
fof(f255,plain,
! [X2,X0,X1] : eq(X1,X2) = eq3(app(X0,X1),app(X0,X2)),
inference(trivial_inequality_removal,[],[f248]) ).
fof(f262,plain,
! [X2,X3,X0,X1] : fail(X0,cons(apply1(lam3,X1),X2),apply1(lam3,X1),X3) = aux5(X0,X1,X3,X2,X1,btrue),
inference(superposition,[],[f125,f133]) ).
fof(f269,plain,
! [X2,X3,X0,X1] : fail(X0,cons(apply1(lam3,X1),X2),apply1(lam3,X1),X3) = unifyloop(X0,X3,X2),
inference(forward_demodulation,[],[f262,f9]) ).
fof(f277,plain,
! [X2,X3,X0,X1,X4,X5] : unifyloop(X0,cons(app(X1,X2),X3),cons(app(X1,X4),X5)) = aux3(X0,X3,X1,X2,X5,X1,X4,btrue),
inference(superposition,[],[f120,f133]) ).
fof(f290,plain,
! [X2,X3,X0,X1,X4,X5] : unifyloop(X0,cons(app(X1,X2),X3),cons(app(X1,X4),X5)) = unifyloop(X0,append(X2,X3),append(X4,X5)),
inference(forward_demodulation,[],[f277,f5]) ).
fof(f400,plain,
! [X2,X3,X0,X1,X4] :
( bfalse = eq(cons(app(X2,X0),X3),cons(app(X2,X1),X4))
| bfalse != eq(X0,X1) ),
inference(superposition,[],[f84,f255]) ).
fof(f514,plain,
! [X0,X1] : substList(X0,cons(apply1(lam3,X1),nil)) = cons(apply1(X0,X1),nil),
inference(superposition,[],[f142,f25]) ).
fof(f770,plain,
! [X2,X0,X1] : btrue != eq4(eq4(aux6(app(X2,X0),app(X2,X1),unifyloop(lam3,append(X0,nil),append(X1,nil))),btrue),bfalse),
inference(superposition,[],[f141,f290]) ).
fof(f772,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X2,cons(X0,X1)),app(X2,X3),unifyloop(lam3,cons(X0,append(X1,nil)),append(X3,nil))),btrue),bfalse),
inference(superposition,[],[f770,f58]) ).
fof(f892,plain,
! [X2,X0,X1] : btrue != eq4(eq4(aux6(app(X0,cons(X1,nil)),app(X0,X2),unifyloop(lam3,cons(X1,nil),append(X2,nil))),btrue),bfalse),
inference(superposition,[],[f772,f57]) ).
fof(f900,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X2,cons(X3,nil)),app(X2,cons(X0,X1)),unifyloop(lam3,cons(X3,nil),cons(X0,append(X1,nil)))),btrue),bfalse),
inference(superposition,[],[f892,f58]) ).
fof(f976,plain,
! [X2,X3,X0,X1,X4] : btrue != eq4(eq4(aux6(app(X2,cons(X3,nil)),app(X2,cons(X4,cons(X0,X1))),unifyloop(lam3,cons(X3,nil),cons(X4,cons(X0,append(X1,nil))))),btrue),bfalse),
inference(superposition,[],[f900,f58]) ).
fof(f1466,plain,
! [X2,X0,X1] : substList(X0,cons(X2,cons(apply1(lam3,X1),nil))) = cons(subst(X0,X2),cons(apply1(X0,X1),nil)),
inference(superposition,[],[f26,f514]) ).
fof(f2558,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X0,cons(X1,nil)),app(X0,cons(X2,cons(X3,nil))),unifyloop(lam3,cons(X1,nil),cons(X2,cons(X3,nil)))),btrue),bfalse),
inference(superposition,[],[f976,f57]) ).
fof(f2605,plain,
! [X2,X3,X0,X1,X4] : btrue != eq4(eq4(aux6(app(X3,cons(app(X4,X0),nil)),app(X3,cons(app(X4,X1),cons(X2,nil))),unifyloop(lam3,append(X0,nil),append(X1,cons(X2,nil)))),btrue),bfalse),
inference(superposition,[],[f2558,f290]) ).
fof(f19868,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X1,cons(app(X2,X3),nil)),app(X1,cons(app(X2,nil),cons(X0,nil))),unifyloop(lam3,append(X3,nil),cons(X0,nil))),btrue),bfalse),
inference(superposition,[],[f2605,f57]) ).
fof(f19962,plain,
! [X2,X3,X0,X1,X4] : btrue != eq4(eq4(aux6(app(X2,cons(app(X3,cons(X0,X1)),nil)),app(X2,cons(app(X3,nil),cons(X4,nil))),unifyloop(lam3,cons(X0,append(X1,nil)),cons(X4,nil))),btrue),bfalse),
inference(superposition,[],[f19868,f58]) ).
fof(f43842,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X0,cons(app(X1,cons(X2,nil)),nil)),app(X0,cons(app(X1,nil),cons(X3,nil))),unifyloop(lam3,cons(X2,nil),cons(X3,nil))),btrue),bfalse),
inference(superposition,[],[f19962,f57]) ).
fof(f43908,plain,
! [X2,X3,X0,X1] : btrue != eq4(eq4(aux6(app(X2,cons(app(X3,cons(apply1(lam3,X0),nil)),nil)),app(X2,cons(app(X3,nil),cons(X1,nil))),fail(lam3,cons(apply1(lam3,X0),nil),X1,nil)),btrue),bfalse),
inference(superposition,[],[f43842,f123]) ).
fof(f64938,plain,
! [X2,X0,X1] : btrue != eq4(eq4(aux6(app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil)),app(X0,cons(app(X1,nil),cons(apply1(lam3,X2),nil))),unifyloop(lam3,nil,nil)),btrue),bfalse),
inference(superposition,[],[f43908,f269]) ).
fof(f64949,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(subst(lam3,app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),subst(lam3,app(X0,cons(app(X1,nil),cons(apply1(lam3,X2),nil))))),btrue),bfalse),
inference(forward_demodulation,[],[f64938,f119]) ).
fof(f64951,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(subst(lam3,app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),app(X0,substList(lam3,cons(app(X1,nil),cons(apply1(lam3,X2),nil))))),btrue),bfalse),
inference(forward_demodulation,[],[f64949,f22]) ).
fof(f64953,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(subst(lam3,app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),app(X0,cons(subst(lam3,app(X1,nil)),cons(apply1(lam3,X2),nil)))),btrue),bfalse),
inference(forward_demodulation,[],[f64951,f1466]) ).
fof(f64954,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(subst(lam3,app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),app(X0,cons(app(X1,substList(lam3,nil)),cons(apply1(lam3,X2),nil)))),btrue),bfalse),
inference(forward_demodulation,[],[f64953,f22]) ).
fof(f64955,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(subst(lam3,app(X0,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),app(X0,cons(app(X1,nil),cons(apply1(lam3,X2),nil)))),btrue),bfalse),
inference(forward_demodulation,[],[f64954,f25]) ).
fof(f64956,plain,
! [X2,X0,X1] : btrue != eq4(eq4(eq3(app(X0,substList(lam3,cons(app(X1,cons(apply1(lam3,X2),nil)),nil))),app(X0,cons(app(X1,nil),cons(apply1(lam3,X2),nil)))),btrue),bfalse),
inference(forward_demodulation,[],[f64955,f22]) ).
fof(f64957,plain,
! [X2,X1] : btrue != eq4(eq4(eq(substList(lam3,cons(app(X1,cons(apply1(lam3,X2),nil)),nil)),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse),
inference(forward_demodulation,[],[f64956,f255]) ).
fof(f64958,plain,
! [X2,X1] : btrue != eq4(eq4(eq(cons(subst(lam3,app(X1,cons(apply1(lam3,X2),nil))),nil),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse),
inference(forward_demodulation,[],[f64957,f144]) ).
fof(f64959,plain,
! [X2,X1] : btrue != eq4(eq4(eq(cons(app(X1,substList(lam3,cons(apply1(lam3,X2),nil))),nil),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse),
inference(forward_demodulation,[],[f64958,f22]) ).
fof(f64960,plain,
! [X2,X1] : btrue != eq4(eq4(eq(cons(app(X1,cons(subst(lam3,apply1(lam3,X2)),nil)),nil),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse),
inference(forward_demodulation,[],[f64959,f144]) ).
fof(f64961,plain,
! [X2,X1] : btrue != eq4(eq4(eq(cons(app(X1,cons(apply1(lam3,X2),nil)),nil),cons(app(X1,nil),cons(apply1(lam3,X2),nil))),btrue),bfalse),
inference(forward_demodulation,[],[f64960,f115]) ).
fof(f65637,plain,
! [X1] :
( btrue != eq4(eq4(bfalse,btrue),bfalse)
| bfalse != eq(cons(apply1(lam3,X1),nil),nil) ),
inference(superposition,[],[f64961,f400]) ).
fof(f65640,plain,
btrue != eq4(eq4(bfalse,btrue),bfalse),
inference(forward_subsumption_resolution,[],[f65637,f90]) ).
fof(f65642,plain,
btrue != eq4(bfalse,bfalse),
inference(forward_demodulation,[],[f65640,f72]) ).
fof(f65644,plain,
$false,
inference(forward_subsumption_resolution,[],[f65642,f80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWX242-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 15:18:04 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.12 Running first-order model finding
% 0.09/0.12 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
% 4.36/0.87 % (3450182)Will run a generic schedule for satisfiability detection.
% 4.36/0.87 % (3450188)% WARNING: option uhcvi not known.
% 4.36/0.87 % (3450189)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=63902434:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.36/0.87 % (3450187)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3334440772_2999 on theBenchmark for (2999ds/0Mi)
% 4.36/0.87 % (3450190)dis+10_1_sil=32000:sp=arity:random_seed=2373205957:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.36/0.87 % (3450191)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=219291810:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.36/0.87 % (3450188)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=704775694:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.36/0.87 % (3450192)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=354394779:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.36/0.87 % (3450193)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3141586879:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.36/0.87 % TRYING [1]
% 4.36/0.87 % TRYING [2]
% 4.36/0.87 % TRYING [3]
% 4.36/0.87 % (3450190)Instruction limit reached!
% 4.36/0.87 % (3450190)------------------------------
% 4.36/0.87 % (3450190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/0.87 % (3450190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/0.87 % (3450190)CaDiCaL version: 2.1.3
% 4.36/0.87 % (3450190)Termination reason: Instruction limit
% 4.36/0.87 % (3450190)Termination phase: Saturation
% 4.36/0.87 % (3450190)Time elapsed: 0.033 s
% 4.36/0.87 % (3450190)Peak memory usage: 12 MB
% 4.36/0.87 % (3450190)Instructions burned: 104 (million)
% 4.36/0.87 % (3450191)Instruction limit reached!
% 4.36/0.87 % (3450191)------------------------------
% 4.36/0.87 % (3450191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/0.87 % (3450191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/0.87 % (3450191)CaDiCaL version: 2.1.3
% 4.36/0.87 % (3450191)Termination reason: Instruction limit
% 4.36/0.87 % (3450191)Termination phase: Saturation
% 4.36/0.87 % (3450191)Time elapsed: 0.039 s
% 4.36/0.87 % (3450191)Peak memory usage: 13 MB
% 4.36/0.87 % (3450191)Instructions burned: 118 (million)
% 4.36/0.87 % (3450192)Instruction limit reached!
% 4.36/0.87 % (3450192)------------------------------
% 4.36/0.87 % (3450192)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/0.87 % (3450192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/0.87 % (3450192)CaDiCaL version: 2.1.3
% 4.36/0.87 % (3450192)Termination reason: Instruction limit
% 4.36/0.87 % (3450192)Termination phase: Saturation
% 4.36/0.87 % (3450192)Time elapsed: 0.044 s
% 4.36/0.87 % (3450192)Peak memory usage: 13 MB
% 4.36/0.87 % (3450192)Instructions burned: 134 (million)
% 4.36/0.87 % (3450201)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3455528941:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.36/0.87 % (3450202)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=611758033:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.36/0.87 % TRYING [1]
% 4.36/0.87 % (3450193)Instruction limit reached!
% 4.36/0.87 % (3450193)------------------------------
% 4.36/0.87 % (3450193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/0.87 % (3450193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/0.87 % (3450193)CaDiCaL version: 2.1.3
% 4.36/0.87 % (3450193)Termination reason: Instruction limit
% 4.36/0.87 % (3450193)Termination phase: Saturation
% 4.36/0.87 % (3450193)Time elapsed: 0.052 s
% 4.36/0.87 % (3450193)Peak memory usage: 13 MB
% 4.36/0.87 % (3450193)Instructions burned: 161 (million)
% 4.36/0.87 % TRYING [2]
% 4.36/0.87 % (3450203)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=3996901098:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.36/0.87 % TRYING [3]
% 4.36/0.87 % (3450206)ott-21_1_sil=16000:fs=off:random_seed=1340876399:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.36/0.87 % (3450202)Instruction limit reached!
% 4.36/0.87 % (3450202)------------------------------
% 4.36/0.87 % (3450202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/0.87 % (3450202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450202)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450202)Termination reason: Instruction limit
% 8.99/1.56 % (3450202)Termination phase: Saturation
% 8.99/1.56 % (3450202)Time elapsed: 0.047 s
% 8.99/1.56 % (3450202)Peak memory usage: 13 MB
% 8.99/1.56 % (3450202)Instructions burned: 132 (million)
% 8.99/1.56 % (3450209)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4265909267:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.99/1.56 % (3450206)Instruction limit reached!
% 8.99/1.56 % (3450206)------------------------------
% 8.99/1.56 % (3450206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450206)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450206)Termination reason: Instruction limit
% 8.99/1.56 % (3450206)Termination phase: Saturation
% 8.99/1.56 % (3450206)Time elapsed: 0.054 s
% 8.99/1.56 % (3450206)Peak memory usage: 12 MB
% 8.99/1.56 % (3450206)Instructions burned: 183 (million)
% 8.99/1.56 % (3450211)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1742822648:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 8.99/1.56 % TRYING [1]
% 8.99/1.56 % TRYING [2]
% 8.99/1.56 % TRYING [3]
% 8.99/1.56 % (3450201)Instruction limit reached!
% 8.99/1.56 % (3450201)------------------------------
% 8.99/1.56 % (3450201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450201)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450201)Termination reason: Instruction limit
% 8.99/1.56 % (3450201)Termination phase: Finite model building constraint generation
% 8.99/1.56 % (3450201)Time elapsed: 0.148 s
% 8.99/1.56 % (3450201)Peak memory usage: 45 MB
% 8.99/1.56 % (3450201)Instructions burned: 718 (million)
% 8.99/1.56 % (3450213)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=572903045:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.99/1.56 % TRYING [4]
% 8.99/1.56 % (3450203)Instruction limit reached!
% 8.99/1.56 % (3450203)------------------------------
% 8.99/1.56 % (3450203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450203)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450203)Termination reason: Instruction limit
% 8.99/1.56 % (3450203)Termination phase: Saturation
% 8.99/1.56 % (3450203)Time elapsed: 0.204 s
% 8.99/1.56 % (3450203)Peak memory usage: 19 MB
% 8.99/1.56 % (3450203)Instructions burned: 687 (million)
% 8.99/1.56 % (3450209)Instruction limit reached!
% 8.99/1.56 % (3450209)------------------------------
% 8.99/1.56 % (3450209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450209)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450209)Termination reason: Instruction limit
% 8.99/1.56 % (3450209)Termination phase: Saturation
% 8.99/1.56 % (3450209)Time elapsed: 0.153 s
% 8.99/1.56 % (3450209)Peak memory usage: 17 MB
% 8.99/1.56 % (3450209)Instructions burned: 477 (million)
% 8.99/1.56 % (3450215)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1090840964:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.99/1.56 % (3450216)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=239696599:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 8.99/1.56 % (3450215)Cannot represent all propositional literals internally
% 8.99/1.56 % (3450215)Refutation not found, incomplete strategy
% 8.99/1.56 % (3450215)------------------------------
% 8.99/1.56 % (3450215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450215)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450215)Termination reason: Refutation not found, incomplete strategy
% 8.99/1.56 % (3450215)Time elapsed: 0.005 s
% 8.99/1.56 % (3450215)Peak memory usage: 11 MB
% 8.99/1.56 % (3450215)Instructions burned: 19 (million)
% 8.99/1.56 % (3450215)------------------------------
% 8.99/1.56 % (3450215)------------------------------
% 8.99/1.56 % (3450219)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=221339609:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 8.99/1.56 % (3450211)Instruction limit reached!
% 8.99/1.56 % (3450211)------------------------------
% 8.99/1.56 % (3450211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450211)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450211)Termination reason: Instruction limit
% 8.99/1.56 % (3450211)Termination phase: Finite model building constraint generation
% 8.99/1.56 % (3450211)Time elapsed: 0.219 s
% 8.99/1.56 % (3450211)Peak memory usage: 52 MB
% 8.99/1.56 % (3450211)Instructions burned: 867 (million)
% 8.99/1.56 % (3450221)fmb+10_1_sil=64000:random_seed=370805464:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 8.99/1.56 % TRYING [1]
% 8.99/1.56 % TRYING [2]
% 8.99/1.56 % TRYING [3]
% 8.99/1.56 % (3450216)Instruction limit reached!
% 8.99/1.56 % (3450216)------------------------------
% 8.99/1.56 % (3450216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450216)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450216)Termination reason: Instruction limit
% 8.99/1.56 % (3450216)Termination phase: Saturation
% 8.99/1.56 % (3450216)Time elapsed: 0.201 s
% 8.99/1.56 % (3450216)Peak memory usage: 16 MB
% 8.99/1.56 % (3450216)Instructions burned: 696 (million)
% 8.99/1.56 % (3450223)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=278506915:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 8.99/1.56 % (3450223)Cannot represent all propositional literals internally
% 8.99/1.56 % (3450223)Refutation not found, incomplete strategy
% 8.99/1.56 % (3450223)------------------------------
% 8.99/1.56 % (3450223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450223)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450223)Termination reason: Refutation not found, incomplete strategy
% 8.99/1.56 % (3450223)Time elapsed: 0.005 s
% 8.99/1.56 % (3450223)Peak memory usage: 10 MB
% 8.99/1.56 % (3450223)Instructions burned: 19 (million)
% 8.99/1.56 % (3450223)------------------------------
% 8.99/1.56 % (3450223)------------------------------
% 8.99/1.56 % (3450225)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=304024728:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 8.99/1.56 % TRYING [8]
% 8.99/1.56 % (3450219)Instruction limit reached!
% 8.99/1.56 % (3450219)------------------------------
% 8.99/1.56 % (3450219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450219)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450219)Termination reason: Instruction limit
% 8.99/1.56 % (3450219)Termination phase: Saturation
% 8.99/1.56 % (3450219)Time elapsed: 0.270 s
% 8.99/1.56 % (3450219)Peak memory usage: 19 MB
% 8.99/1.56 % (3450219)Instructions burned: 880 (million)
% 8.99/1.56 % (3450227)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=141633009:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 8.99/1.56 % (3450213)Instruction limit reached!
% 8.99/1.56 % (3450213)------------------------------
% 8.99/1.56 % (3450213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450213)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450213)Termination reason: Instruction limit
% 8.99/1.56 % (3450213)Termination phase: Saturation
% 8.99/1.56 % (3450213)Time elapsed: 0.366 s
% 8.99/1.56 % (3450213)Peak memory usage: 27 MB
% 8.99/1.56 % (3450213)Instructions burned: 1180 (million)
% 8.99/1.56 % (3450229)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=108604828:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 8.99/1.56 % (3450225)Instruction limit reached!
% 8.99/1.56 % (3450225)------------------------------
% 8.99/1.56 % (3450225)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450225)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450225)Termination reason: Instruction limit
% 8.99/1.56 % (3450225)Termination phase: Finite model building constraint generation
% 8.99/1.56 % (3450225)Time elapsed: 0.180 s
% 8.99/1.56 % (3450225)Peak memory usage: 73 MB
% 8.99/1.56 % (3450225)Instructions burned: 921 (million)
% 8.99/1.56 % (3450231)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2423611933:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 8.99/1.56 % (3450231)Cannot represent all propositional literals internally
% 8.99/1.56 % (3450231)Refutation not found, incomplete strategy
% 8.99/1.56 % (3450231)------------------------------
% 8.99/1.56 % (3450231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450231)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450231)Termination reason: Refutation not found, incomplete strategy
% 8.99/1.56 % (3450231)Time elapsed: 0.005 s
% 8.99/1.56 % (3450231)Peak memory usage: 10 MB
% 8.99/1.56 % (3450231)Instructions burned: 19 (million)
% 8.99/1.56 % (3450231)------------------------------
% 8.99/1.56 % (3450231)------------------------------
% 8.99/1.56 % (3450233)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3151091965:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 8.99/1.56 % (3450233)Cannot represent all propositional literals internally
% 8.99/1.56 % (3450233)Refutation not found, incomplete strategy
% 8.99/1.56 % (3450233)------------------------------
% 8.99/1.56 % (3450233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450233)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450233)Termination reason: Refutation not found, incomplete strategy
% 8.99/1.56 % (3450233)Time elapsed: 0.021 s
% 8.99/1.56 % (3450233)Peak memory usage: 11 MB
% 8.99/1.56 % (3450233)Instructions burned: 77 (million)
% 8.99/1.56 % (3450233)------------------------------
% 8.99/1.56 % (3450233)------------------------------
% 8.99/1.56 % (3450235)ott-2_1_sil=16000:newcnf=on:random_seed=1440220876:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 8.99/1.56 % (3450235)Instruction limit reached!
% 8.99/1.56 % (3450235)------------------------------
% 8.99/1.56 % (3450235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450235)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450235)Termination reason: Instruction limit
% 8.99/1.56 % (3450235)Termination phase: Saturation
% 8.99/1.56 % (3450235)Time elapsed: 0.302 s
% 8.99/1.56 % (3450235)Peak memory usage: 24 MB
% 8.99/1.56 % (3450235)Instructions burned: 871 (million)
% 8.99/1.56 % (3450229)Instruction limit reached!
% 8.99/1.56 % (3450229)------------------------------
% 8.99/1.56 % (3450229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450229)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450229)Termination reason: Instruction limit
% 8.99/1.56 % (3450229)Termination phase: Saturation
% 8.99/1.56 % (3450229)Time elapsed: 0.478 s
% 8.99/1.56 % (3450229)Peak memory usage: 32 MB
% 8.99/1.56 % (3450229)Instructions burned: 1475 (million)
% 8.99/1.56 % (3450237)ott+10_1_sil=32000:tgt=ground:random_seed=1992647073:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 8.99/1.56 % (3450238)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2525934706:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 8.99/1.56 % TRYING [1]
% 8.99/1.56 % TRYING [2]
% 8.99/1.56 % TRYING [3]
% 8.99/1.56 % TRYING [4]
% 8.99/1.56 % (3450188) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3450182-3450188"...
% 8.99/1.56 % (3450188)...printing done.
% 8.99/1.56 % (3450188)Refutation found. Thanks to Tanya!
% 8.99/1.56 % SZS status Unsatisfiable for theBenchmark
% 8.99/1.56 % SZS output start Proof for theBenchmark
% See solution above
% 8.99/1.56 % (3450188)------------------------------
% 8.99/1.56 % (3450188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.56 % (3450188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.56 % (3450188)CaDiCaL version: 2.1.3
% 8.99/1.56 % (3450188)Termination reason: Refutation
% 8.99/1.56 % (3450188)Time elapsed: 1.367 s
% 8.99/1.56 % (3450188)Peak memory usage: 57 MB
% 8.99/1.56 % (3450188)Instructions burned: 4579 (million)
% 8.99/1.56 % (3450182)Success in time 1.429 s
% 8.99/1.56 % Vampire exiting
%------------------------------------------------------------------------------