%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : KLE044-10 : TPTP v9.3.1. Released v7.3.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 11:40:44 AM UTC 2026
% Result : Unsatisfiable 33.99s 5.23s
% Output : Refutation 33.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 18
% Syntax : Number of formulae : 91 ( 91 unt; 0 def)
% Number of atoms : 91 ( 90 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-4 aty)
% Number of variables : 157 ( 157 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : ifeq3(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom) ).
fof(f2,axiom,
! [X2,X0,X1] : ifeq2(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_001) ).
fof(f3,axiom,
! [X2,X0,X1] : ifeq(X0,X0,X1,X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ifeq_axiom_002) ).
fof(f4,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f5,axiom,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
fof(f7,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f8,axiom,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f9,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f10,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f11,axiom,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
fof(f12,axiom,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
fof(f17,axiom,
! [X0,X1] : ifeq2(leq(X0,X1),true,addition(X0,X1),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order_1) ).
fof(f18,axiom,
! [X0,X1] : ifeq3(addition(X0,X1),X1,leq(X0,X1),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order) ).
fof(f19,plain,
! [X0,X1] : true = ifeq3(addition(X0,X1),X1,leq(X0,X1),true),
inference(reorient_equations,[],[f18]) ).
fof(f20,axiom,
! [X0] : leq(addition(one,multiplication(X0,star(X0))),star(X0)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold_right) ).
fof(f21,plain,
! [X0] : true = leq(addition(one,multiplication(X0,star(X0))),star(X0)),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0] : leq(addition(one,multiplication(star(X0),X0)),star(X0)) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_unfold_left) ).
fof(f23,plain,
! [X0] : true = leq(addition(one,multiplication(star(X0),X0)),star(X0)),
inference(reorient_equations,[],[f22]) ).
fof(f24,axiom,
! [X2,X0,X1] : ifeq(leq(addition(multiplication(X0,X1),X2),X1),true,leq(multiplication(star(X0),X2),X1),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_induction_left) ).
fof(f25,plain,
! [X2,X0,X1] : true = ifeq(leq(addition(multiplication(X0,X1),X2),X1),true,leq(multiplication(star(X0),X2),X1),true),
inference(reorient_equations,[],[f24]) ).
fof(f26,axiom,
! [X2,X0,X1] : ifeq(leq(addition(multiplication(X0,X1),X2),X0),true,leq(multiplication(X2,star(X1)),X0),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',star_induction_right) ).
fof(f27,plain,
! [X2,X0,X1] : true = ifeq(leq(addition(multiplication(X0,X1),X2),X0),true,leq(multiplication(X2,star(X1)),X0),true),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
tuple(leq(star(addition(one,sK2_goals_X0)),star(sK2_goals_X0)),leq(star(sK1_goals_X0),star(addition(one,sK1_goals_X0)))) != tuple(true,true),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f38,plain,
! [X0,X1] : addition(X0,X1) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f5,f7]) ).
fof(f39,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f5,f4]) ).
fof(f45,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X1,addition(X2,X0)),
inference(superposition,[],[f5,f4]) ).
fof(f54,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,addition(X0,X1)),
inference(superposition,[],[f38,f4]) ).
fof(f96,plain,
! [X0,X1] : ifeq2(leq(X1,X0),true,addition(X0,X1),X0) = X0,
inference(superposition,[],[f17,f4]) ).
fof(f103,plain,
! [X0] : true = ifeq3(X0,X0,leq(X0,X0),true),
inference(superposition,[],[f19,f7]) ).
fof(f107,plain,
! [X0,X1] : true = ifeq3(addition(X0,X1),addition(X0,X1),leq(X1,addition(X0,X1)),true),
inference(superposition,[],[f19,f54]) ).
fof(f112,plain,
! [X0,X1] : true = leq(X1,addition(X0,X1)),
inference(forward_demodulation,[],[f107,f1]) ).
fof(f114,plain,
! [X0] : true = leq(X0,X0),
inference(forward_demodulation,[],[f103,f1]) ).
fof(f149,plain,
! [X2,X0,X1] : true = leq(X2,addition(X0,addition(X1,X2))),
inference(superposition,[],[f112,f5]) ).
fof(f205,plain,
! [X0] : star(X0) = ifeq2(true,true,addition(addition(one,multiplication(X0,star(X0))),star(X0)),star(X0)),
inference(superposition,[],[f17,f21]) ).
fof(f206,plain,
! [X0] : star(X0) = addition(addition(one,multiplication(X0,star(X0))),star(X0)),
inference(forward_demodulation,[],[f205,f2]) ).
fof(f209,plain,
! [X0] : star(X0) = addition(star(X0),addition(one,multiplication(X0,star(X0)))),
inference(forward_demodulation,[],[f206,f4]) ).
fof(f357,plain,
! [X0] : star(X0) = ifeq2(true,true,addition(addition(one,multiplication(star(X0),X0)),star(X0)),star(X0)),
inference(superposition,[],[f17,f23]) ).
fof(f358,plain,
! [X0] : star(X0) = addition(addition(one,multiplication(star(X0),X0)),star(X0)),
inference(forward_demodulation,[],[f357,f2]) ).
fof(f361,plain,
! [X0] : star(X0) = addition(star(X0),addition(one,multiplication(star(X0),X0))),
inference(forward_demodulation,[],[f358,f4]) ).
fof(f373,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(superposition,[],[f39,f5]) ).
fof(f430,plain,
! [X0,X1] : addition(X1,X0) = addition(X0,addition(X0,X1)),
inference(superposition,[],[f45,f7]) ).
fof(f469,plain,
! [X2,X0,X1] : addition(addition(X0,X1),X2) = addition(X1,addition(X2,X0)),
inference(superposition,[],[f45,f4]) ).
fof(f972,plain,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(X0,addition(X2,X1)),
inference(superposition,[],[f373,f45]) ).
fof(f1419,plain,
! [X2,X3,X0,X1] : true = leq(X1,addition(X3,addition(X0,addition(X1,X2)))),
inference(superposition,[],[f149,f469]) ).
fof(f4882,plain,
! [X0] : star(X0) = addition(one,addition(multiplication(X0,star(X0)),star(X0))),
inference(forward_demodulation,[],[f209,f45]) ).
fof(f4883,plain,
! [X0] : star(X0) = addition(one,addition(star(X0),multiplication(X0,star(X0)))),
inference(forward_demodulation,[],[f4882,f972]) ).
fof(f4884,plain,
! [X0] : star(X0) = addition(one,addition(multiplication(star(X0),X0),star(X0))),
inference(forward_demodulation,[],[f361,f45]) ).
fof(f4885,plain,
! [X0] : star(X0) = addition(one,addition(star(X0),multiplication(star(X0),X0))),
inference(forward_demodulation,[],[f4884,f972]) ).
fof(f4915,plain,
! [X0] : star(X0) = addition(one,star(X0)),
inference(superposition,[],[f38,f4883]) ).
fof(f4919,plain,
! [X0] : star(X0) = addition(addition(star(X0),multiplication(X0,star(X0))),star(X0)),
inference(superposition,[],[f54,f4883]) ).
fof(f4969,plain,
! [X0] : star(X0) = addition(star(X0),addition(star(X0),multiplication(X0,star(X0)))),
inference(forward_demodulation,[],[f4919,f4]) ).
fof(f4999,plain,
! [X0] : star(X0) = addition(star(X0),multiplication(X0,star(X0))),
inference(forward_demodulation,[],[f4969,f38]) ).
fof(f5033,plain,
! [X0,X1] : addition(star(X0),X1) = addition(one,addition(star(X0),X1)),
inference(superposition,[],[f5,f4915]) ).
fof(f6297,plain,
! [X0] : star(X0) = addition(star(X0),multiplication(star(X0),X0)),
inference(forward_demodulation,[],[f4885,f5033]) ).
fof(f8876,plain,
! [X0,X1] : multiplication(X0,addition(one,X1)) = addition(X0,multiplication(X0,X1)),
inference(superposition,[],[f11,f9]) ).
fof(f8980,plain,
! [X0,X1] : multiplication(X1,star(X0)) = addition(X1,multiplication(X1,addition(star(X0),multiplication(X0,star(X0))))),
inference(superposition,[],[f8876,f4883]) ).
fof(f9015,plain,
! [X0] : star(X0) = multiplication(star(X0),addition(one,X0)),
inference(superposition,[],[f8876,f6297]) ).
fof(f9140,plain,
! [X0,X1] : multiplication(X1,star(X0)) = addition(X1,multiplication(X1,star(X0))),
inference(forward_demodulation,[],[f8980,f4999]) ).
fof(f9174,plain,
! [X0] : star(addition(one,X0)) = multiplication(star(addition(one,X0)),addition(X0,one)),
inference(superposition,[],[f9015,f430]) ).
fof(f10065,plain,
! [X2,X3,X0,X1] : true = leq(X0,addition(X2,addition(X3,multiplication(X0,star(X1))))),
inference(superposition,[],[f1419,f9140]) ).
fof(f13316,plain,
! [X0,X1] : multiplication(addition(one,X1),X0) = addition(X0,multiplication(X1,X0)),
inference(superposition,[],[f12,f10]) ).
fof(f13341,plain,
! [X2,X0,X1] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X2,X0),X1),
inference(superposition,[],[f12,f4]) ).
fof(f13635,plain,
! [X0] : star(X0) = multiplication(addition(one,X0),star(X0)),
inference(superposition,[],[f13316,f4999]) ).
fof(f15234,plain,
! [X0,X1] : true = ifeq(leq(multiplication(X0,X1),X1),true,leq(multiplication(star(X0),multiplication(X0,X1)),X1),true),
inference(superposition,[],[f25,f7]) ).
fof(f15265,plain,
! [X0,X1] : true = ifeq(leq(addition(multiplication(X0,X1),one),X1),true,leq(star(X0),X1),true),
inference(superposition,[],[f25,f9]) ).
fof(f15440,plain,
! [X0,X1] : true = ifeq(leq(addition(one,multiplication(X0,X1)),X1),true,leq(star(X0),X1),true),
inference(forward_demodulation,[],[f15265,f4]) ).
fof(f19265,plain,
! [X2,X0,X1] : true = ifeq(leq(multiplication(X0,addition(X1,X2)),X0),true,leq(multiplication(multiplication(X0,X2),star(X1)),X0),true),
inference(superposition,[],[f27,f11]) ).
fof(f19576,plain,
! [X2,X0,X1] : true = ifeq(leq(multiplication(X0,addition(X1,X2)),X0),true,leq(multiplication(X0,multiplication(X2,star(X1))),X0),true),
inference(forward_demodulation,[],[f19265,f8]) ).
fof(f47266,plain,
! [X2,X3,X0,X1] : true = leq(X0,addition(X3,multiplication(addition(X0,X1),star(X2)))),
inference(superposition,[],[f10065,f13341]) ).
fof(f52129,plain,
! [X0,X1] : true = leq(X0,star(addition(X0,X1))),
inference(superposition,[],[f47266,f4999]) ).
fof(f52231,plain,
! [X0,X1] : star(addition(X0,X1)) = ifeq2(true,true,addition(X0,star(addition(X0,X1))),star(addition(X0,X1))),
inference(superposition,[],[f17,f52129]) ).
fof(f52237,plain,
! [X0,X1] : star(addition(X0,X1)) = addition(X0,star(addition(X0,X1))),
inference(forward_demodulation,[],[f52231,f2]) ).
fof(f113551,plain,
! [X0] : true = ifeq(leq(addition(one,star(X0)),star(X0)),true,leq(star(addition(one,X0)),star(X0)),true),
inference(superposition,[],[f15440,f13635]) ).
fof(f114405,plain,
! [X0] : true = ifeq(leq(star(X0),star(X0)),true,leq(star(addition(one,X0)),star(X0)),true),
inference(forward_demodulation,[],[f113551,f4915]) ).
fof(f114573,plain,
! [X0] : true = ifeq(true,true,leq(star(addition(one,X0)),star(X0)),true),
inference(forward_demodulation,[],[f114405,f114]) ).
fof(f114623,plain,
! [X0] : true = leq(star(addition(one,X0)),star(X0)),
inference(forward_demodulation,[],[f114573,f3]) ).
fof(f114689,plain,
tuple(true,true) != tuple(true,leq(star(sK1_goals_X0),star(addition(one,sK1_goals_X0)))),
inference(superposition,[],[f28,f114623]) ).
fof(f138858,plain,
! [X0] : true = ifeq(leq(star(X0),star(X0)),true,leq(multiplication(star(addition(one,X0)),star(X0)),star(X0)),true),
inference(superposition,[],[f15234,f13635]) ).
fof(f138901,plain,
! [X0] : true = ifeq(true,true,leq(multiplication(star(addition(one,X0)),star(X0)),star(X0)),true),
inference(forward_demodulation,[],[f138858,f114]) ).
fof(f138917,plain,
! [X0] : true = leq(multiplication(star(addition(one,X0)),star(X0)),star(X0)),
inference(forward_demodulation,[],[f138901,f3]) ).
fof(f138983,plain,
! [X0] : star(X0) = ifeq2(true,true,addition(star(X0),multiplication(star(addition(one,X0)),star(X0))),star(X0)),
inference(superposition,[],[f96,f138917]) ).
fof(f138991,plain,
! [X0] : star(X0) = addition(star(X0),multiplication(star(addition(one,X0)),star(X0))),
inference(forward_demodulation,[],[f138983,f2]) ).
fof(f139026,plain,
! [X0] : star(X0) = multiplication(addition(one,star(addition(one,X0))),star(X0)),
inference(forward_demodulation,[],[f138991,f13316]) ).
fof(f139045,plain,
! [X0] : star(X0) = multiplication(star(addition(one,X0)),star(X0)),
inference(forward_demodulation,[],[f139026,f52237]) ).
fof(f222864,plain,
! [X0] : true = ifeq(leq(star(addition(one,X0)),star(addition(one,X0))),true,leq(multiplication(star(addition(one,X0)),multiplication(one,star(X0))),star(addition(one,X0))),true),
inference(superposition,[],[f19576,f9174]) ).
fof(f223006,plain,
! [X0] : true = ifeq(leq(star(addition(one,X0)),star(addition(one,X0))),true,leq(multiplication(star(addition(one,X0)),star(X0)),star(addition(one,X0))),true),
inference(forward_demodulation,[],[f222864,f10]) ).
fof(f223092,plain,
! [X0] : true = ifeq(leq(star(addition(one,X0)),star(addition(one,X0))),true,leq(star(X0),star(addition(one,X0))),true),
inference(forward_demodulation,[],[f223006,f139045]) ).
fof(f223140,plain,
! [X0] : true = ifeq(true,true,leq(star(X0),star(addition(one,X0))),true),
inference(forward_demodulation,[],[f223092,f114]) ).
fof(f223156,plain,
! [X0] : true = leq(star(X0),star(addition(one,X0))),
inference(forward_demodulation,[],[f223140,f3]) ).
fof(f223240,plain,
tuple(true,true) != tuple(true,true),
inference(superposition,[],[f114689,f223156]) ).
fof(f223252,plain,
$false,
inference(trivial_inequality_removal,[],[f223240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE044-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.37 % Computer : n008.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 13:07:40 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 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
% 14.85/2.60 % (1208741)Will run a generic schedule for satisfiability detection.
% 14.85/2.60 % (1208748)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2637592982:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.85/2.60 % (1208747)% WARNING: option uhcvi not known.
% 14.85/2.60 % (1208751)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=35150119:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.85/2.60 % (1208746)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2615638318_2999 on theBenchmark for (2999ds/0Mi)
% 14.85/2.60 % (1208749)dis+10_1_sil=32000:sp=arity:random_seed=1721780732:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.85/2.60 % (1208750)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3803825221:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.85/2.60 % (1208752)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1316423665:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.85/2.60 % (1208747)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=241429334:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.85/2.60 % TRYING [1]
% 14.85/2.60 % TRYING [2]
% 14.85/2.60 % TRYING [3]
% 14.85/2.60 % TRYING [4]
% 14.85/2.60 % (1208749)Instruction limit reached!
% 14.85/2.60 % (1208749)------------------------------
% 14.85/2.60 % (1208749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.60 % (1208749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.60 % (1208749)CaDiCaL version: 2.1.3
% 14.85/2.60 % (1208749)Termination reason: Instruction limit
% 14.85/2.60 % (1208749)Termination phase: Saturation
% 14.85/2.60 % (1208749)Time elapsed: 0.060 s
% 14.85/2.60 % (1208749)Peak memory usage: 12 MB
% 14.85/2.60 % (1208749)Instructions burned: 104 (million)
% 14.85/2.60 % (1208750)Instruction limit reached!
% 14.85/2.60 % (1208750)------------------------------
% 14.85/2.60 % (1208750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.60 % (1208750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.60 % (1208750)CaDiCaL version: 2.1.3
% 14.85/2.60 % (1208750)Termination reason: Instruction limit
% 14.85/2.60 % (1208750)Termination phase: Saturation
% 14.85/2.60 % (1208750)Time elapsed: 0.069 s
% 14.85/2.60 % (1208750)Peak memory usage: 12 MB
% 14.85/2.60 % (1208750)Instructions burned: 116 (million)
% 14.85/2.60 % (1208751)Instruction limit reached!
% 14.85/2.60 % (1208751)------------------------------
% 14.85/2.60 % (1208751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.60 % (1208751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.60 % (1208751)CaDiCaL version: 2.1.3
% 14.85/2.60 % (1208751)Termination reason: Instruction limit
% 14.85/2.60 % (1208751)Termination phase: Saturation
% 14.85/2.60 % (1208751)Time elapsed: 0.074 s
% 14.85/2.60 % (1208751)Peak memory usage: 12 MB
% 14.85/2.60 % (1208751)Instructions burned: 131 (million)
% 14.85/2.60 % (1208760)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1133406023:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.85/2.60 % TRYING [1]
% 14.85/2.60 % TRYING [2]
% 14.85/2.60 % TRYING [3]
% 14.85/2.60 % (1208761)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=824729860:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.85/2.60 % (1208762)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=3171012624:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.85/2.60 % (1208752)Instruction limit reached!
% 14.85/2.60 % (1208752)------------------------------
% 14.85/2.60 % (1208752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.85/2.60 % (1208752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.85/2.60 % (1208752)CaDiCaL version: 2.1.3
% 14.85/2.60 % (1208752)Termination reason: Instruction limit
% 14.85/2.60 % (1208752)Termination phase: Saturation
% 14.85/2.60 % (1208752)Time elapsed: 0.093 s
% 14.85/2.60 % (1208752)Peak memory usage: 11 MB
% 14.85/2.60 % (1208752)Instructions burned: 159 (million)
% 14.85/2.60 % TRYING [4]
% 14.85/2.60 % TRYING [5]
% 14.85/2.60 % (1208766)ott-21_1_sil=16000:fs=off:random_seed=1435434577:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.85/2.60 % (1208761)Instruction limit reached!
% 14.85/2.60 % (1208761)------------------------------
% 14.85/2.60 % (1208761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208761)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208761)Termination reason: Instruction limit
% 33.99/5.22 % (1208761)Termination phase: Saturation
% 33.99/5.22 % (1208761)Time elapsed: 0.084 s
% 33.99/5.22 % (1208761)Peak memory usage: 12 MB
% 33.99/5.22 % (1208761)Instructions burned: 132 (million)
% 33.99/5.22 % TRYING [5]
% 33.99/5.22 % (1208766)Instruction limit reached!
% 33.99/5.22 % (1208766)------------------------------
% 33.99/5.22 % (1208766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208766)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208766)Termination reason: Instruction limit
% 33.99/5.22 % (1208766)Termination phase: Saturation
% 33.99/5.22 % (1208766)Time elapsed: 0.076 s
% 33.99/5.22 % (1208766)Peak memory usage: 11 MB
% 33.99/5.22 % (1208766)Instructions burned: 181 (million)
% 33.99/5.22 % (1208768)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2657988956:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 33.99/5.22 % (1208769)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1080794526:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 33.99/5.22 % TRYING [1]
% 33.99/5.22 % TRYING [2]
% 33.99/5.22 % TRYING [3]
% 33.99/5.22 % TRYING [4]
% 33.99/5.22 % TRYING [5]
% 33.99/5.22 % TRYING [6]
% 33.99/5.22 % (1208760)Instruction limit reached!
% 33.99/5.22 % (1208760)------------------------------
% 33.99/5.22 % (1208760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208760)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208760)Termination reason: Instruction limit
% 33.99/5.22 % (1208760)Termination phase: Finite model building SAT solving
% 33.99/5.22 % (1208760)Time elapsed: 0.348 s
% 33.99/5.22 % (1208760)Peak memory usage: 33 MB
% 33.99/5.22 % (1208760)Instructions burned: 714 (million)
% 33.99/5.22 % (1208762)Instruction limit reached!
% 33.99/5.22 % (1208762)------------------------------
% 33.99/5.22 % (1208762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208762)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208762)Termination reason: Instruction limit
% 33.99/5.22 % (1208762)Termination phase: Saturation
% 33.99/5.22 % (1208762)Time elapsed: 0.350 s
% 33.99/5.22 % (1208762)Peak memory usage: 19 MB
% 33.99/5.22 % (1208762)Instructions burned: 684 (million)
% 33.99/5.22 % (1208772)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=524996991:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 33.99/5.22 % (1208768)Instruction limit reached!
% 33.99/5.22 % (1208768)------------------------------
% 33.99/5.22 % (1208768)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208768)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208768)Termination reason: Instruction limit
% 33.99/5.22 % (1208768)Termination phase: Saturation
% 33.99/5.22 % (1208768)Time elapsed: 0.262 s
% 33.99/5.22 % (1208768)Peak memory usage: 15 MB
% 33.99/5.22 % (1208768)Instructions burned: 479 (million)
% 33.99/5.22 % (1208773)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3445397315:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 33.99/5.22 % (1208775)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=605940252:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 33.99/5.22 % TRYING [6]
% 33.99/5.22 % (1208769)Instruction limit reached!
% 33.99/5.22 % (1208769)------------------------------
% 33.99/5.22 % (1208769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208769)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208769)Termination reason: Instruction limit
% 33.99/5.22 % (1208769)Termination phase: Finite model building constraint generation
% 33.99/5.22 % (1208769)Time elapsed: 0.347 s
% 33.99/5.22 % (1208769)Peak memory usage: 25 MB
% 33.99/5.22 % (1208769)Instructions burned: 866 (million)
% 33.99/5.22 % (1208778)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2333443045:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 33.99/5.22 % (1208775)Instruction limit reached!
% 33.99/5.22 % (1208775)------------------------------
% 33.99/5.22 % (1208775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208775)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208775)Termination reason: Instruction limit
% 33.99/5.22 % (1208775)Termination phase: Saturation
% 33.99/5.22 % (1208775)Time elapsed: 0.382 s
% 33.99/5.22 % (1208775)Peak memory usage: 17 MB
% 33.99/5.22 % (1208775)Instructions burned: 693 (million)
% 33.99/5.22 % (1208773)Instruction limit reached!
% 33.99/5.22 % (1208773)------------------------------
% 33.99/5.22 % (1208773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.22 % (1208773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.22 % (1208773)CaDiCaL version: 2.1.3
% 33.99/5.22 % (1208773)Termination reason: Instruction limit
% 33.99/5.22 % (1208773)Termination phase: Finite model building constraint generation
% 33.99/5.22 % (1208773)Time elapsed: 0.399 s
% 33.99/5.22 % (1208773)Peak memory usage: 107 MB
% 33.99/5.22 % (1208773)Instructions burned: 890 (million)
% 33.99/5.23 % (1208780)fmb+10_1_sil=64000:random_seed=2385600023:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 33.99/5.23 % TRYING [1]
% 33.99/5.23 % TRYING [2]
% 33.99/5.23 % TRYING [3]
% 33.99/5.23 % (1208781)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1189583154:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 33.99/5.23 % TRYING [20]
% 33.99/5.23 % TRYING [4]
% 33.99/5.23 % TRYING [5]
% 33.99/5.23 % (1208778)Instruction limit reached!
% 33.99/5.23 % (1208778)------------------------------
% 33.99/5.23 % (1208778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208778)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208778)Termination reason: Instruction limit
% 33.99/5.23 % (1208778)Termination phase: Saturation
% 33.99/5.23 % (1208778)Time elapsed: 0.448 s
% 33.99/5.23 % (1208778)Peak memory usage: 18 MB
% 33.99/5.23 % (1208778)Instructions burned: 881 (million)
% 33.99/5.23 % (1208784)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1130572788:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 33.99/5.23 % TRYING [8]
% 33.99/5.23 % TRYING [7]
% 33.99/5.23 % (1208772)Instruction limit reached!
% 33.99/5.23 % (1208772)------------------------------
% 33.99/5.23 % (1208772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208772)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208772)Termination reason: Instruction limit
% 33.99/5.23 % (1208772)Termination phase: Saturation
% 33.99/5.23 % (1208772)Time elapsed: 0.674 s
% 33.99/5.23 % (1208772)Peak memory usage: 24 MB
% 33.99/5.23 % (1208772)Instructions burned: 1181 (million)
% 33.99/5.23 % (1208786)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2522107296:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 33.99/5.23 % TRYING [6]
% 33.99/5.23 % (1208784)Instruction limit reached!
% 33.99/5.23 % (1208784)------------------------------
% 33.99/5.23 % (1208784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208784)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208784)Termination reason: Instruction limit
% 33.99/5.23 % (1208784)Termination phase: Finite model building constraint generation
% 33.99/5.23 % (1208784)Time elapsed: 0.395 s
% 33.99/5.23 % (1208784)Peak memory usage: 98 MB
% 33.99/5.23 % (1208784)Instructions burned: 920 (million)
% 33.99/5.23 % (1208788)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1639426118:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 33.99/5.23 % TRYING [7]
% 33.99/5.23 % (1208788)Instruction limit reached!
% 33.99/5.23 % (1208788)------------------------------
% 33.99/5.23 % (1208788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208788)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208788)Termination reason: Instruction limit
% 33.99/5.23 % (1208788)Termination phase: Saturation
% 33.99/5.23 % (1208788)Time elapsed: 0.664 s
% 33.99/5.23 % (1208788)Peak memory usage: 21 MB
% 33.99/5.23 % (1208788)Instructions burned: 1472 (million)
% 33.99/5.23 % (1208790)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2160489958:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 33.99/5.23 % (1208790)Cannot represent all propositional literals internally
% 33.99/5.23 % (1208790)Refutation not found, incomplete strategy
% 33.99/5.23 % (1208790)------------------------------
% 33.99/5.23 % (1208790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208790)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208790)Termination reason: Refutation not found, incomplete strategy
% 33.99/5.23 % (1208790)Time elapsed: 0.002 s
% 33.99/5.23 % (1208790)Peak memory usage: 10 MB
% 33.99/5.23 % (1208790)Instructions burned: 4 (million)
% 33.99/5.23 % (1208790)------------------------------
% 33.99/5.23 % (1208790)------------------------------
% 33.99/5.23 % (1208792)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4125503291:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 33.99/5.23 % TRYING [16]
% 33.99/5.23 % (1208792)Instruction limit reached!
% 33.99/5.23 % (1208792)------------------------------
% 33.99/5.23 % (1208792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208792)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208792)Termination reason: Instruction limit
% 33.99/5.23 % (1208792)Termination phase: Finite model building constraint generation
% 33.99/5.23 % (1208792)Time elapsed: 0.736 s
% 33.99/5.23 % (1208792)Peak memory usage: 134 MB
% 33.99/5.23 % (1208792)Instructions burned: 2177 (million)
% 33.99/5.23 % (1208794)ott-2_1_sil=16000:newcnf=on:random_seed=1972677212:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2970 on theBenchmark for (2970ds/869Mi)
% 33.99/5.23 % (1208794)Instruction limit reached!
% 33.99/5.23 % (1208794)------------------------------
% 33.99/5.23 % (1208794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208794)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208794)Termination reason: Instruction limit
% 33.99/5.23 % (1208794)Termination phase: Saturation
% 33.99/5.23 % (1208794)Time elapsed: 0.501 s
% 33.99/5.23 % (1208794)Peak memory usage: 21 MB
% 33.99/5.23 % (1208794)Instructions burned: 871 (million)
% 33.99/5.23 % (1208796)ott+10_1_sil=32000:tgt=ground:random_seed=78577273:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 33.99/5.23 % (1208786)Instruction limit reached!
% 33.99/5.23 % (1208786)------------------------------
% 33.99/5.23 % (1208786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208786)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208786)Termination reason: Instruction limit
% 33.99/5.23 % (1208786)Termination phase: Saturation
% 33.99/5.23 % (1208786)Time elapsed: 2.651 s
% 33.99/5.23 % (1208786)Peak memory usage: 46 MB
% 33.99/5.23 % (1208786)Instructions burned: 5133 (million)
% 33.99/5.23 % (1208798)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2747645122:i=54282_2961 on theBenchmark for (2961ds/54282Mi)
% 33.99/5.23 % TRYING [1]
% 33.99/5.23 % TRYING [2]
% 33.99/5.23 % TRYING [3]
% 33.99/5.23 % TRYING [4]
% 33.99/5.23 % TRYING [5]
% 33.99/5.23 % TRYING [6]
% 33.99/5.23 % (1208781)Instruction limit reached!
% 33.99/5.23 % (1208781)------------------------------
% 33.99/5.23 % (1208781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208781)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208781)Termination reason: Instruction limit
% 33.99/5.23 % (1208781)Termination phase: Finite model building constraint generation
% 33.99/5.23 % (1208781)Time elapsed: 3.380 s
% 33.99/5.23 % (1208781)Peak memory usage: 624 MB
% 33.99/5.23 % (1208781)Instructions burned: 9516 (million)
% 33.99/5.23 % (1208800)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2802665583:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 33.99/5.23 % TRYING [8]
% 33.99/5.23 % (1208748) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1208741-1208748"...
% 33.99/5.23 % (1208748)...printing done.
% 33.99/5.23 % (1208748)Refutation found. Thanks to Tanya!
% 33.99/5.23 % SZS status Unsatisfiable for theBenchmark
% 33.99/5.23 % SZS output start Proof for theBenchmark
% See solution above
% 33.99/5.23 % (1208748)------------------------------
% 33.99/5.23 % (1208748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.99/5.23 % (1208748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.99/5.23 % (1208748)CaDiCaL version: 2.1.3
% 33.99/5.23 % (1208748)Termination reason: Refutation
% 33.99/5.23 % (1208748)Time elapsed: 4.774 s
% 33.99/5.23 % (1208748)Peak memory usage: 94 MB
% 33.99/5.23 % (1208748)Instructions burned: 23023 (million)
% 33.99/5.23 % (1208741)Success in time 4.818 s
% 33.99/5.23 % Vampire exiting
%------------------------------------------------------------------------------