%------------------------------------------------------------------------------
% 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 : n026.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 : Theorem 1.68s 0.55s
% Output : Refutation 1.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 18
% Syntax : Number of formulae : 77 ( 46 unt; 0 def)
% Number of atoms : 112 ( 103 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 70 ( 35 ~; 30 |; 0 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 2 con; 0-5 aty)
% Number of variables : 262 ( 258 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] : proj2App(app(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_005) ).
fof(f9,axiom,
! [X0,X1] : tail(cons(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
fof(f10,axiom,
! [X0,X1] : nil != cons(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
fof(f15,axiom,
! [X0,X1,X2,X3,X4] : fail(X0,cons(var(X4),X3),X1,X2) = unifyvar(X0,X4,X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
fof(f21,axiom,
! [X0,X1,X2] : subst(X0,app(X1,X2)) = app(X1,substList(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
fof(f22,axiom,
! [X0,X1] : subst(X0,var(X1)) = apply1(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
fof(f23,axiom,
! [X0] : substList(X0,nil) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
fof(f24,axiom,
! [X0,X1,X2] : substList(X0,cons(X1,X2)) = cons(subst(X0,X1),substList(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_024) ).
fof(f30,axiom,
! [X0] : unifyloop(X0,nil,nil) = just(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
fof(f33,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( X2 = X5
=> unifyloop(X0,cons(app(X2,X3),X1),cons(app(X5,X6),X4)) = unifyloop(X0,append(X3,X1),append(X6,X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_033) ).
fof(f37,axiom,
! [X0,X1,X2,X3,X4] : unifyloop(X0,cons(var(X2),X1),cons(X3,X4)) = unifyvar(X0,X2,X3,X1,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
fof(f40,axiom,
! [X0,X1,X2,X3,X4] :
( X1 = X4
=> unifyvar(X0,X1,var(X4),X2,X3) = unifyloop(X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_040) ).
fof(f43,axiom,
! [X0,X1] : unify2(X0,X1) = unifyloop(lam3,cons(X0,nil),cons(X1,nil)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
fof(f45,axiom,
! [X0,X1,X2] :
( unify2(X0,X1) = just(X2)
=> ( unificationOK(X0,X1)
<=> subst(X2,X0) = subst(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_045) ).
fof(f48,axiom,
! [X0] : append(nil,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
fof(f49,axiom,
! [X0,X1,X2] : append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_049) ).
fof(f52,axiom,
! [X0] : apply1(lam3,X0) = var(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_052) ).
fof(f53,conjecture,
? [X0,X1] : ~ unificationOK(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_053) ).
fof(f54,negated_conjecture,
~ ? [X0,X1] : ~ unificationOK(X0,X1),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( unifyloop(X0,cons(app(X2,X3),X1),cons(app(X5,X6),X4)) = unifyloop(X0,append(X3,X1),append(X6,X4))
| X2 != X5 ),
inference(ennf_transformation,[],[f33]) ).
fof(f63,plain,
! [X0,X1,X2,X3,X4] :
( unifyvar(X0,X1,var(X4),X2,X3) = unifyloop(X0,X2,X3)
| X1 != X4 ),
inference(ennf_transformation,[],[f40]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ( unificationOK(X0,X1)
<=> subst(X2,X0) = subst(X2,X1) )
| unify2(X0,X1) != just(X2) ),
inference(ennf_transformation,[],[f45]) ).
fof(f67,plain,
! [X0,X1] : unificationOK(X0,X1),
inference(ennf_transformation,[],[f54]) ).
fof(f72,plain,
! [X0,X1] : proj2App(app(X0,X1)) = X1,
inference(cnf_transformation,[],[f5]) ).
fof(f76,plain,
! [X0,X1] : tail(cons(X0,X1)) = X1,
inference(cnf_transformation,[],[f9]) ).
fof(f77,plain,
! [X0,X1] : cons(X0,X1) != nil,
inference(cnf_transformation,[],[f10]) ).
fof(f82,plain,
! [X2,X3,X0,X1,X4] : fail(X0,cons(var(X4),X3),X1,X2) = unifyvar(X0,X4,X1,X2,X3),
inference(cnf_transformation,[],[f15]) ).
fof(f92,plain,
! [X2,X0,X1] : subst(X0,app(X1,X2)) = app(X1,substList(X0,X2)),
inference(cnf_transformation,[],[f21]) ).
fof(f93,plain,
! [X0,X1] : subst(X0,var(X1)) = apply1(X0,X1),
inference(cnf_transformation,[],[f22]) ).
fof(f94,plain,
! [X0] : nil = substList(X0,nil),
inference(cnf_transformation,[],[f23]) ).
fof(f95,plain,
! [X2,X0,X1] : substList(X0,cons(X1,X2)) = cons(subst(X0,X1),substList(X0,X2)),
inference(cnf_transformation,[],[f24]) ).
fof(f101,plain,
! [X0] : just(X0) = unifyloop(X0,nil,nil),
inference(cnf_transformation,[],[f30]) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X2 != X5
| unifyloop(X0,cons(app(X2,X3),X1),cons(app(X5,X6),X4)) = unifyloop(X0,append(X3,X1),append(X6,X4)) ),
inference(cnf_transformation,[],[f59]) ).
fof(f108,plain,
! [X2,X3,X0,X1,X4] : unifyloop(X0,cons(var(X2),X1),cons(X3,X4)) = unifyvar(X0,X2,X3,X1,X4),
inference(cnf_transformation,[],[f37]) ).
fof(f111,plain,
! [X2,X3,X0,X1,X4] :
( X1 != X4
| unifyvar(X0,X1,var(X4),X2,X3) = unifyloop(X0,X2,X3) ),
inference(cnf_transformation,[],[f63]) ).
fof(f114,plain,
! [X0,X1] : unify2(X0,X1) = unifyloop(lam3,cons(X0,nil),cons(X1,nil)),
inference(cnf_transformation,[],[f43]) ).
fof(f117,plain,
! [X2,X0,X1] :
( unify2(X0,X1) != just(X2)
| subst(X2,X0) = subst(X2,X1)
| ~ unificationOK(X0,X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f120,plain,
! [X0] : append(nil,X0) = X0,
inference(cnf_transformation,[],[f48]) ).
fof(f121,plain,
! [X2,X0,X1] : append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
inference(cnf_transformation,[],[f49]) ).
fof(f125,plain,
! [X0] : var(X0) = apply1(lam3,X0),
inference(cnf_transformation,[],[f52]) ).
fof(f126,plain,
! [X0,X1] : unificationOK(X0,X1),
inference(cnf_transformation,[],[f67]) ).
fof(f130,plain,
! [X0] : var(X0) = subst(lam3,var(X0)),
inference(definition_unfolding,[],[f125,f93]) ).
fof(f136,plain,
! [X2,X3,X0,X1,X4] : unifyloop(X0,cons(var(X2),X1),cons(X3,X4)) = fail(X0,cons(var(X2),X4),X3,X1),
inference(definition_unfolding,[],[f108,f82]) ).
fof(f139,plain,
! [X2,X3,X0,X1,X4] :
( X1 != X4
| unifyloop(X0,X2,X3) = fail(X0,cons(var(X1),X3),var(X4),X2) ),
inference(definition_unfolding,[],[f111,f82]) ).
fof(f142,plain,
! [X2,X0,X1] :
( unifyloop(lam3,cons(X0,nil),cons(X1,nil)) != unifyloop(X2,nil,nil)
| subst(X2,X0) = subst(X2,X1)
| ~ unificationOK(X0,X1) ),
inference(definition_unfolding,[],[f117,f114,f101]) ).
fof(f150,plain,
! [X3,X0,X1,X6,X4,X5] : unifyloop(X0,append(X3,X1),append(X6,X4)) = unifyloop(X0,cons(app(X5,X3),X1),cons(app(X5,X6),X4)),
inference(equality_resolution,[],[f104]) ).
fof(f151,plain,
! [X2,X3,X0,X4] : unifyloop(X0,X2,X3) = fail(X0,cons(var(X4),X3),var(X4),X2),
inference(equality_resolution,[],[f139]) ).
fof(f153,plain,
! [X2,X0,X1] :
( unifyloop(lam3,cons(X0,nil),cons(X1,nil)) != unifyloop(X2,nil,nil)
| subst(X2,X0) = subst(X2,X1) ),
inference(forward_subsumption_resolution,[],[f142,f126]) ).
fof(f163,plain,
! [X2,X3,X0,X1] : substList(X1,cons(app(X0,X2),X3)) = cons(app(X0,substList(X1,X2)),substList(X1,X3)),
inference(superposition,[],[f95,f92]) ).
fof(f164,plain,
! [X0,X1] : substList(X0,cons(X1,nil)) = cons(subst(X0,X1),nil),
inference(superposition,[],[f95,f94]) ).
fof(f331,plain,
! [X2,X0,X1] : substList(X0,cons(app(X1,nil),X2)) = cons(app(X1,nil),substList(X0,X2)),
inference(superposition,[],[f163,f94]) ).
fof(f714,plain,
! [X2,X3,X0,X1] :
( unifyloop(lam3,append(X0,nil),append(X1,nil)) != unifyloop(X3,nil,nil)
| subst(X3,app(X2,X0)) = subst(X3,app(X2,X1)) ),
inference(superposition,[],[f153,f150]) ).
fof(f715,plain,
! [X2,X3,X0,X1] :
( subst(X3,app(X2,X0)) = app(X2,substList(X3,X1))
| unifyloop(lam3,append(X0,nil),append(X1,nil)) != unifyloop(X3,nil,nil) ),
inference(forward_demodulation,[],[f714,f92]) ).
fof(f716,plain,
! [X2,X3,X0,X1] :
( unifyloop(lam3,append(X0,nil),append(X1,nil)) != unifyloop(X3,nil,nil)
| app(X2,substList(X3,X1)) = app(X2,substList(X3,X0)) ),
inference(forward_demodulation,[],[f715,f92]) ).
fof(f718,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X3,nil,nil) != unifyloop(lam3,cons(X0,append(X1,nil)),append(X2,nil))
| app(X4,substList(X3,X2)) = app(X4,substList(X3,cons(X0,X1))) ),
inference(superposition,[],[f716,f121]) ).
fof(f739,plain,
! [X2,X3,X0,X1] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,cons(X1,nil),append(X2,nil))
| app(X3,substList(X0,X2)) = app(X3,substList(X0,cons(X1,nil))) ),
inference(superposition,[],[f718,f120]) ).
fof(f746,plain,
! [X2,X3,X0,X1] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,cons(X1,nil),append(X2,nil))
| app(X3,substList(X0,X2)) = app(X3,cons(subst(X0,X1),nil)) ),
inference(forward_demodulation,[],[f739,f164]) ).
fof(f760,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X2,nil,nil) != unifyloop(lam3,cons(X3,nil),cons(X0,append(X1,nil)))
| app(X4,substList(X2,cons(X0,X1))) = app(X4,cons(subst(X2,X3),nil)) ),
inference(superposition,[],[f746,f121]) ).
fof(f806,plain,
! [X2,X3,X0,X1,X4,X5] :
( unifyloop(X2,nil,nil) != unifyloop(lam3,cons(X3,nil),cons(X4,cons(X0,append(X1,nil))))
| app(X5,substList(X2,cons(X4,cons(X0,X1)))) = app(X5,cons(subst(X2,X3),nil)) ),
inference(superposition,[],[f760,f121]) ).
fof(f999,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,cons(X1,nil),cons(X2,cons(X3,nil)))
| app(X4,cons(subst(X0,X1),nil)) = app(X4,substList(X0,cons(X2,cons(X3,nil)))) ),
inference(superposition,[],[f806,f120]) ).
fof(f1007,plain,
! [X2,X3,X0,X1,X4,X5] :
( unifyloop(X3,nil,nil) != unifyloop(lam3,append(X0,nil),append(X1,cons(X2,nil)))
| app(X5,cons(subst(X3,app(X4,X0)),nil)) = app(X5,substList(X3,cons(app(X4,X1),cons(X2,nil)))) ),
inference(superposition,[],[f999,f150]) ).
fof(f1008,plain,
! [X2,X3,X0,X1,X4,X5] :
( unifyloop(X3,nil,nil) != unifyloop(lam3,append(X0,nil),append(X1,cons(X2,nil)))
| app(X5,cons(app(X4,substList(X3,X0)),nil)) = app(X5,substList(X3,cons(app(X4,X1),cons(X2,nil)))) ),
inference(forward_demodulation,[],[f1007,f92]) ).
fof(f2137,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X1,nil,nil) != unifyloop(lam3,append(X2,nil),cons(X0,nil))
| app(X3,cons(app(X4,substList(X1,X2)),nil)) = app(X3,substList(X1,cons(app(X4,nil),cons(X0,nil)))) ),
inference(superposition,[],[f1008,f120]) ).
fof(f2139,plain,
! [X2,X3,X0,X1,X4] :
( app(X3,cons(app(X4,substList(X1,X2)),nil)) = app(X3,cons(app(X4,nil),substList(X1,cons(X0,nil))))
| unifyloop(X1,nil,nil) != unifyloop(lam3,append(X2,nil),cons(X0,nil)) ),
inference(forward_demodulation,[],[f2137,f331]) ).
fof(f2141,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X1,nil,nil) != unifyloop(lam3,append(X2,nil),cons(X0,nil))
| app(X3,cons(app(X4,substList(X1,X2)),nil)) = app(X3,cons(app(X4,nil),cons(subst(X1,X0),nil))) ),
inference(forward_demodulation,[],[f2139,f164]) ).
fof(f2143,plain,
! [X2,X3,X0,X1,X4,X5] :
( unifyloop(X2,nil,nil) != unifyloop(lam3,cons(X0,append(X1,nil)),cons(X3,nil))
| app(X4,cons(app(X5,substList(X2,cons(X0,X1))),nil)) = app(X4,cons(app(X5,nil),cons(subst(X2,X3),nil))) ),
inference(superposition,[],[f2141,f121]) ).
fof(f3759,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,cons(X1,nil),cons(X2,nil))
| app(X3,cons(app(X4,substList(X0,cons(X1,nil))),nil)) = app(X3,cons(app(X4,nil),cons(subst(X0,X2),nil))) ),
inference(superposition,[],[f2143,f120]) ).
fof(f3768,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,cons(X1,nil),cons(X2,nil))
| app(X3,cons(app(X4,cons(subst(X0,X1),nil)),nil)) = app(X3,cons(app(X4,nil),cons(subst(X0,X2),nil))) ),
inference(forward_demodulation,[],[f3759,f164]) ).
fof(f3885,plain,
! [X2,X3,X0,X1,X4] :
( unifyloop(X2,nil,nil) != fail(lam3,cons(var(X0),nil),X1,nil)
| app(X3,cons(app(X4,cons(subst(X2,var(X0)),nil)),nil)) = app(X3,cons(app(X4,nil),cons(subst(X2,X1),nil))) ),
inference(superposition,[],[f3768,f136]) ).
fof(f3892,plain,
! [X2,X3,X0,X1] :
( unifyloop(X0,nil,nil) != unifyloop(lam3,nil,nil)
| app(X2,cons(app(X3,cons(subst(X0,var(X1)),nil)),nil)) = app(X2,cons(app(X3,nil),cons(subst(X0,var(X1)),nil))) ),
inference(superposition,[],[f3885,f151]) ).
fof(f3895,plain,
! [X2,X0,X1] : app(X0,cons(app(X1,cons(subst(lam3,var(X2)),nil)),nil)) = app(X0,cons(app(X1,nil),cons(subst(lam3,var(X2)),nil))),
inference(equality_resolution,[],[f3892]) ).
fof(f3896,plain,
! [X2,X0,X1] : app(X0,cons(app(X1,cons(var(X2),nil)),nil)) = app(X0,cons(app(X1,nil),cons(var(X2),nil))),
inference(forward_demodulation,[],[f3895,f130]) ).
fof(f3898,plain,
! [X2,X0,X1] : cons(app(X1,cons(var(X2),nil)),nil) = proj2App(app(X0,cons(app(X1,nil),cons(var(X2),nil)))),
inference(superposition,[],[f72,f3896]) ).
fof(f3942,plain,
! [X2,X1] : cons(app(X1,cons(var(X2),nil)),nil) = cons(app(X1,nil),cons(var(X2),nil)),
inference(forward_demodulation,[],[f3898,f72]) ).
fof(f4123,plain,
! [X0,X1] : nil = tail(cons(app(X0,nil),cons(var(X1),nil))),
inference(superposition,[],[f76,f3942]) ).
fof(f4227,plain,
! [X1] : nil = cons(var(X1),nil),
inference(forward_demodulation,[],[f4123,f76]) ).
fof(f4307,plain,
$false,
inference(forward_subsumption_resolution,[],[f4227,f77]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX242_1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 15:21:12 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 1.68/0.55 % (3932953)Will run a generic schedule for satisfiability detection.
% 1.68/0.55 % (3932958)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=445655100_2999 on theBenchmark for (2999ds/0Mi)
% 1.68/0.55 % (3932959)% WARNING: option uhcvi not known.
% 1.68/0.55 % Detected minimum model sizes of [3]
% 1.68/0.55 % Detected maximum model sizes of [max]
% 1.68/0.55 % TRYING [3]
% 1.68/0.55 % (3932960)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1848470882:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.68/0.55 % (3932961)dis+10_1_sil=32000:sp=arity:random_seed=1590870249:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.68/0.55 % (3932959)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1256577740:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.68/0.55 % (3932963)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3538776442:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.68/0.55 % (3932962)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=894278355:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.68/0.55 % (3932964)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=419928248:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.68/0.55 % TRYING [4]
% 1.68/0.55 % (3932962)Instruction limit reached!
% 1.68/0.55 % (3932962)------------------------------
% 1.68/0.55 % (3932962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932962)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932962)Termination reason: Instruction limit
% 1.68/0.55 % (3932962)Termination phase: Saturation
% 1.68/0.55 % (3932962)Time elapsed: 0.047 s
% 1.68/0.55 % (3932962)Peak memory usage: 11 MB
% 1.68/0.55 % (3932962)Instructions burned: 118 (million)
% 1.68/0.55 % (3932961)Instruction limit reached!
% 1.68/0.55 % (3932961)------------------------------
% 1.68/0.55 % (3932961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932961)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932961)Termination reason: Instruction limit
% 1.68/0.55 % (3932961)Termination phase: Saturation
% 1.68/0.55 % (3932961)Time elapsed: 0.063 s
% 1.68/0.55 % (3932961)Peak memory usage: 12 MB
% 1.68/0.55 % (3932961)Instructions burned: 103 (million)
% 1.68/0.55 % (3932963)Instruction limit reached!
% 1.68/0.55 % (3932963)------------------------------
% 1.68/0.55 % (3932963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932963)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932963)Termination reason: Instruction limit
% 1.68/0.55 % (3932963)Termination phase: Saturation
% 1.68/0.55 % (3932963)Time elapsed: 0.069 s
% 1.68/0.55 % (3932963)Peak memory usage: 12 MB
% 1.68/0.55 % (3932963)Instructions burned: 131 (million)
% 1.68/0.55 % (3932973)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=223500468:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.68/0.55 % Detected minimum model sizes of [3]
% 1.68/0.55 % Detected maximum model sizes of [max]
% 1.68/0.55 % TRYING [3]
% 1.68/0.55 % (3932978)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2675889269:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.68/0.55 % (3932964)Instruction limit reached!
% 1.68/0.55 % (3932964)------------------------------
% 1.68/0.55 % (3932964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932964)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932964)Termination reason: Instruction limit
% 1.68/0.55 % (3932964)Termination phase: Saturation
% 1.68/0.55 % (3932964)Time elapsed: 0.091 s
% 1.68/0.55 % (3932964)Peak memory usage: 13 MB
% 1.68/0.55 % (3932964)Instructions burned: 160 (million)
% 1.68/0.55 % (3932982)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=207520204:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.68/0.55 % (3932994)ott-21_1_sil=16000:fs=off:random_seed=4076103177:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.68/0.55 % (3932978)Instruction limit reached!
% 1.68/0.55 % (3932978)------------------------------
% 1.68/0.55 % (3932978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932978)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932978)Termination reason: Instruction limit
% 1.68/0.55 % (3932978)Termination phase: Saturation
% 1.68/0.55 % (3932978)Time elapsed: 0.073 s
% 1.68/0.55 % (3932978)Peak memory usage: 12 MB
% 1.68/0.55 % (3932978)Instructions burned: 131 (million)
% 1.68/0.55 % (3933027)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=591495369:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.68/0.55 % TRYING [4]
% 1.68/0.55 % (3932994)Instruction limit reached!
% 1.68/0.55 % (3932994)------------------------------
% 1.68/0.55 % (3932994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932994)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932994)Termination reason: Instruction limit
% 1.68/0.55 % (3932994)Termination phase: Saturation
% 1.68/0.55 % (3932994)Time elapsed: 0.107 s
% 1.68/0.55 % (3932994)Peak memory usage: 13 MB
% 1.68/0.55 % (3932994)Instructions burned: 180 (million)
% 1.68/0.55 % (3933029)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2954139867:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.68/0.55 % Detected minimum model sizes of [3]
% 1.68/0.55 % Detected maximum model sizes of [max]
% 1.68/0.55 % TRYING [3]
% 1.68/0.55 % (3932982) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3932953-3932982"...
% 1.68/0.55 % (3932982)...printing done.
% 1.68/0.55 % (3932982)Refutation found. Thanks to Tanya!
% 1.68/0.55 % SZS status Theorem for theBenchmark
% 1.68/0.55 % SZS output start Proof for theBenchmark
% See solution above
% 1.68/0.55 % (3932982)------------------------------
% 1.68/0.55 % (3932982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.68/0.55 % (3932982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.68/0.55 % (3932982)CaDiCaL version: 2.1.3
% 1.68/0.55 % (3932982)Termination reason: Refutation
% 1.68/0.55 % (3932982)Time elapsed: 0.185 s
% 1.68/0.55 % (3932982)Peak memory usage: 15 MB
% 1.68/0.55 % (3932982)Instructions burned: 311 (million)
% 1.68/0.55 % (3932953)Success in time 0.308 s
% 1.68/0.55 % Vampire exiting
%------------------------------------------------------------------------------