%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV556-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:25:56 PM UTC 2026
% Result : Satisfiable 0.44s 0.31s
% Output : Saturation 0.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u69,hypothesis,
i1 != i2 ).
cnf(u74,hypothesis,
e_37 = select(a1,i2) ).
cnf(u82,hypothesis,
e_35 = select(a2,i2) ).
cnf(u109,hypothesis,
i3 != i4 ).
cnf(u114,hypothesis,
e_45 = select(a_36,i4) ).
cnf(u122,hypothesis,
e_43 = select(a_38,i4) ).
cnf(u142,hypothesis,
i5 = i6 ).
cnf(u145,hypothesis,
e_53 != select(a_44,i6) ).
cnf(u169,hypothesis,
i1 != i7 ).
cnf(u174,hypothesis,
e_55 = select(a_54,i1) ).
cnf(u190,hypothesis,
i1 = i3 ).
cnf(u194,hypothesis,
e_41 = select(a_32,i3) ).
cnf(u201,hypothesis,
i2 != i3 ).
cnf(u210,hypothesis,
e_39 = select(a_34,i3) ).
cnf(u238,hypothesis,
e_57 != select(a_48,i1) ).
cnf(u243,hypothesis,
i1 = i5 ).
cnf(u248,hypothesis,
e_51 != select(a_46,i6) ).
cnf(u290,hypothesis,
e_55 != select(a_50,i1) ).
cnf(u305,hypothesis,
e_49 = select(a_40,i5) ).
cnf(u328,hypothesis,
i4 != i5 ).
cnf(u347,hypothesis,
e_47 = select(a_42,i1) ).
cnf(u350,hypothesis,
i1 != i4 ).
cnf(u357,hypothesis,
e_47 = select(a_42,i5) ).
cnf(u369,hypothesis,
i1 = i6 ).
cnf(u401,hypothesis,
i2 = i4 ).
cnf(u483,hypothesis,
e_53 != select(a_40,i6) ).
cnf(u494,hypothesis,
i4 != i6 ).
cnf(u583,hypothesis,
i2 != i6 ).
cnf(u638,hypothesis,
e_51 != e_53 ).
cnf(u1192,negated_conjecture,
i3 = i_59 ).
cnf(u1195,negated_conjecture,
i2 != i_59 ).
cnf(u1200,negated_conjecture,
i1 = i_59 ).
cnf(u1348,hypothesis,
e_35 = select(a_38,i2) ).
cnf(u1469,hypothesis,
e_51 != select(a_42,i1) ).
cnf(u1684,hypothesis,
e_35 = e_43 ).
cnf(u1690,hypothesis,
e_35 != select(a_42,i1) ).
cnf(u1706,hypothesis,
e_35 != e_47 ).
cnf(u1780,negated_conjecture,
e_31 != e_43 ).
cnf(u1817,negated_conjecture,
e_31 = e_47 ).
cnf(u1832,hypothesis,
e_51 != select(a_48,i1) ).
cnf(u2262,hypothesis,
e_51 = select(a_44,i1) ).
cnf(u2271,hypothesis,
e_35 = e_51 ).
cnf(u2283,hypothesis,
e_35 = e_37 ).
cnf(u2422,hypothesis,
e_57 = select(a_48,i7) ).
cnf(u2440,hypothesis,
e_55 = select(a_50,i7) ).
cnf(u2525,negated_conjecture,
e_31 = select(a_42,i7) ).
cnf(u2528,negated_conjecture,
i2 != i7 ).
cnf(u2967,negated_conjecture,
e_33 = select(a_44,i2) ).
cnf(u1273,negated_conjecture,
e_31 = e_61 ).
cnf(hyp0,hypothesis,
a_32 = store(a1,i1,e_31) ).
cnf(hyp19,hypothesis,
e_41 = select(a_36,i3) ).
cnf(u49,hypothesis,
e_53 = select(a_54,i6) ).
cnf(u2115,negated_conjecture,
e_31 != e_35 ).
cnf(u2246,hypothesis,
e_35 = select(a_40,i2) ).
cnf(u40,hypothesis,
e_35 = select(a_36,i2) ).
cnf(u2247,hypothesis,
e_35 = select(a_44,i2) ).
cnf(u163,hypothesis,
( select(a_52,X0) = select(a_54,X0)
| i7 = X0
| i1 = X0 ) ).
cnf(u2564,hypothesis,
( select(a_46,X0) = select(a_50,X0)
| i1 = X0 ) ).
cnf(u63,hypothesis,
( select(a_50,X0) = select(a_54,X0)
| i6 = X0 ) ).
cnf(hyp4,hypothesis,
a_40 = store(a_36,i3,e_39) ).
cnf(hyp7,hypothesis,
a_46 = store(a_42,i4,e_45) ).
cnf(u2380,hypothesis,
e_33 = select(a_50,i1) ).
cnf(hyp22,hypothesis,
e_47 = select(a_46,i5) ).
cnf(u2826,hypothesis,
( select(a_46,X0) = select(a_48,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(u1282,hypothesis,
e_33 = select(a_38,i1) ).
cnf(u2750,negated_conjecture,
e_31 = select(a_34,i7) ).
cnf(u44,hypothesis,
e_43 = select(a_44,i4) ).
cnf(hyp26,hypothesis,
e_55 = select(a_54,i7) ).
cnf(u2833,hypothesis,
a_36 = store(a_32,i2,e_33) ).
cnf(u336,hypothesis,
e_47 = select(a_48,i1) ).
cnf(u51,hypothesis,
( select(a1,X0) = select(a_32,X0)
| i1 = X0 ) ).
cnf(u2516,negated_conjecture,
e_31 = select(a_54,i1) ).
cnf(u1302,hypothesis,
a_40 = store(a_36,i1,e_33) ).
cnf(hyp11,hypothesis,
a_54 = store(a_50,i6,e_53) ).
cnf(u1285,hypothesis,
e_31 = select(a_42,i1) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u645,hypothesis,
e_53 = select(a_48,i1) ).
cnf(u1303,hypothesis,
a_42 = store(a_38,i1,e_31) ).
cnf(hyp29,hypothesis,
e_61 = select(a2,i_59) ).
cnf(u3027,negated_conjecture,
( select(a1,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u572,hypothesis,
e_35 = e_45 ).
cnf(u642,hypothesis,
a_52 = store(a_48,i1,e_51) ).
cnf(u55,hypothesis,
( select(a_34,X0) = select(a_38,X0)
| i2 = X0 ) ).
cnf(u1304,hypothesis,
( select(a_36,X0) = select(a_40,X0)
| i1 = X0 ) ).
cnf(u58,hypothesis,
( select(a_40,X0) = select(a_44,X0)
| i4 = X0 ) ).
cnf(u3009,negated_conjecture,
( select(a_34,X0) = select(a_36,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(hyp2,hypothesis,
a_36 = store(a_32,i2,e_35) ).
cnf(u2248,hypothesis,
e_35 = select(a_46,i2) ).
cnf(u2375,hypothesis,
e_33 = select(a_44,i1) ).
cnf(u2985,negated_conjecture,
( select(a_38,X0) = select(a_40,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(hyp5,hypothesis,
a_42 = store(a_38,i3,e_41) ).
cnf(u36,hypothesis,
store(a_52,i1,e_55) = a_58 ).
cnf(u2932,hypothesis,
e_33 = select(a_36,i2) ).
cnf(hyp28,hypothesis,
e_60 = select(a1,i_59) ).
cnf(u43,hypothesis,
e_41 = select(a_42,i3) ).
cnf(hyp16,hypothesis,
e_35 = select(a_34,i2) ).
cnf(u2117,hypothesis,
a_44 = store(a_40,i2,e_35) ).
cnf(u62,hypothesis,
( select(a_52,X0) = select(a_48,X0)
| i6 = X0 ) ).
cnf(u2836,hypothesis,
a_44 = store(a_40,i2,e_33) ).
cnf(u2870,negated_conjecture,
e_57 = select(a_40,i7) ).
cnf(u2341,hypothesis,
a_38 = store(a_34,i2,e_35) ).
cnf(u1274,negated_conjecture,
e_31 != e_60 ).
cnf(hyp9,hypothesis,
a_50 = store(a_46,i5,e_49) ).
cnf(u2138,hypothesis,
e_31 = e_41 ).
cnf(u2019,hypothesis,
a_46 = store(a_42,i2,e_35) ).
cnf(u2413,hypothesis,
e_47 = e_55 ).
cnf(u38,hypothesis,
e_33 = select(a_34,i1) ).
cnf(u2348,hypothesis,
e_33 = e_51 ).
cnf(u53,hypothesis,
( select(a_52,X0) = select(a_58,X0)
| i1 = X0 ) ).
cnf(u2406,hypothesis,
e_33 != e_55 ).
cnf(u2496,negated_conjecture,
e_31 = e_53 ).
cnf(u2288,hypothesis,
e_33 != e_53 ).
cnf(u1283,hypothesis,
e_31 = select(a_36,i1) ).
cnf(u56,hypothesis,
( select(a_36,X0) = select(a_40,X0)
| i3 = X0 ) ).
cnf(hyp20,hypothesis,
e_43 = select(a_42,i4) ).
cnf(u644,hypothesis,
e_51 = select(a_50,i1) ).
cnf(u2493,negated_conjecture,
( select(a_44,X0) = select(a_48,X0)
| i1 = X0 ) ).
cnf(u2722,negated_conjecture,
e_31 != e_57 ).
cnf(hyp23,hypothesis,
e_49 = select(a_44,i5) ).
cnf(u2476,hypothesis,
( select(a_52,X0) = select(a_50,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(u334,hypothesis,
e_47 = select(a_46,i1) ).
cnf(u41,hypothesis,
e_37 = select(a_38,i2) ).
cnf(u2463,hypothesis,
e_47 = select(a_50,i7) ).
cnf(u60,hypothesis,
( select(a_44,X0) = select(a_48,X0)
| i5 = X0 ) ).
cnf(hyp1,hypothesis,
a_34 = store(a2,i1,e_33) ).
cnf(u2349,hypothesis,
e_35 = select(a1,i2) ).
cnf(hyp8,hypothesis,
a_48 = store(a_44,i5,e_47) ).
cnf(u2832,hypothesis,
e_33 = e_35 ).
cnf(u1272,negated_conjecture,
e_33 = e_60 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(hyp27,hypothesis,
e_57 = select(a_52,i7) ).
cnf(u646,hypothesis,
e_51 = select(a_52,i1) ).
cnf(u2343,hypothesis,
a_50 = store(a_46,i1,e_33) ).
cnf(hyp14,hypothesis,
e_31 = select(a2,i1) ).
cnf(u45,hypothesis,
e_45 = select(a_46,i4) ).
cnf(u2905,negated_conjecture,
e_57 = select(a_36,i7) ).
cnf(u2999,negated_conjecture,
( select(a_36,X0) = select(a_38,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u2838,hypothesis,
e_33 = select(a_38,i2) ).
cnf(u48,hypothesis,
e_51 = select(a_52,i6) ).
cnf(u47,hypothesis,
e_49 = select(a_50,i5) ).
cnf(hyp18,hypothesis,
e_39 = select(a_38,i3) ).
cnf(hyp3,hypothesis,
a_38 = store(a_34,i2,e_37) ).
cnf(u2337,hypothesis,
e_33 = e_49 ).
cnf(hyp30,hypothesis,
i_59 = sk(a1,a2) ).
cnf(u2768,hypothesis,
e_33 = select(a_52,i1) ).
cnf(hyp21,hypothesis,
e_45 = select(a_40,i4) ).
cnf(u52,hypothesis,
( select(a2,X0) = select(a_34,X0)
| i1 = X0 ) ).
cnf(u2975,negated_conjecture,
e_57 = select(a1,i7) ).
cnf(u2656,negated_conjecture,
e_31 = e_55 ).
cnf(u2894,negated_conjecture,
( select(a_44,X0) = select(a_46,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(u2322,hypothesis,
( select(a_50,X0) = select(a_54,X0)
| i1 = X0 ) ).
cnf(u1275,negated_conjecture,
e_31 != e_33 ).
cnf(u59,hypothesis,
( select(a_42,X0) = select(a_46,X0)
| i4 = X0 ) ).
cnf(u2737,hypothesis,
( select(a_48,X0) = select(a_50,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(u50,hypothesis,
e_57 = select(a_58,i7) ).
cnf(u3023,negated_conjecture,
( select(a_32,X0) = select(a2,X0)
| i1 = X0
| i2 = X0
| i7 = X0 ) ).
cnf(u2492,negated_conjecture,
a_48 = store(a_44,i1,e_31) ).
cnf(hyp6,hypothesis,
a_44 = store(a_40,i4,e_43) ).
cnf(u2941,negated_conjecture,
e_57 = select(a_32,i7) ).
cnf(u2951,negated_conjecture,
( select(a_40,X0) = select(a_42,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(u2559,hypothesis,
( select(a_40,X0) = select(a_44,X0)
| i2 = X0 ) ).
cnf(u2910,negated_conjecture,
( select(a_42,X0) = select(a_44,X0)
| i1 = X0
| i7 = X0
| i2 = X0 ) ).
cnf(hyp25,hypothesis,
e_53 = select(a_48,i6) ).
cnf(u647,hypothesis,
e_53 = select(a_54,i1) ).
cnf(goal,negated_conjecture,
e_60 != e_61 ).
cnf(u2517,negated_conjecture,
e_31 = select(a_46,i7) ).
cnf(u2506,negated_conjecture,
a_54 = store(a_50,i1,e_31) ).
cnf(u54,hypothesis,
( select(a_32,X0) = select(a_36,X0)
| i2 = X0 ) ).
cnf(u2834,hypothesis,
a_46 = store(a_42,i2,e_33) ).
cnf(u2837,hypothesis,
a_38 = store(a_34,i2,e_33) ).
cnf(u2364,hypothesis,
a_52 = store(a_48,i1,e_33) ).
cnf(u2664,negated_conjecture,
a_58 = store(a_52,i1,e_31) ).
cnf(u1263,hypothesis,
e_33 = e_39 ).
cnf(hyp10,hypothesis,
a_52 = store(a_48,i6,e_51) ).
cnf(u757,hypothesis,
( select(a_52,X0) = select(a_48,X0)
| i1 = X0 ) ).
cnf(u2757,hypothesis,
( select(a_42,X0) = select(a_46,X0)
| i2 = X0 ) ).
cnf(u2934,hypothesis,
e_33 = select(a_46,i2) ).
cnf(hyp13,hypothesis,
a_58 = store(a_54,i7,e_57) ).
cnf(u2245,hypothesis,
e_35 = select(a_42,i2) ).
cnf(u2863,hypothesis,
e_33 = e_37 ).
cnf(u39,hypothesis,
e_55 = select(a_58,i1) ).
cnf(u3017,negated_conjecture,
( select(a_32,X0) = select(a_34,X0)
| i2 = X0
| i1 = X0
| i7 = X0 ) ).
cnf(u155,hypothesis,
e_47 = e_53 ).
cnf(u42,hypothesis,
e_39 = select(a_40,i3) ).
cnf(u2744,negated_conjecture,
e_31 = select(a_38,i7) ).
cnf(u2412,hypothesis,
e_47 != select(a_44,i1) ).
cnf(u57,hypothesis,
( select(a_38,X0) = select(a_42,X0)
| i3 = X0 ) ).
cnf(hyp17,hypothesis,
e_37 = select(a_32,i2) ).
cnf(u64,hypothesis,
( select(a_58,X0) = select(a_54,X0)
| i7 = X0 ) ).
cnf(u1306,hypothesis,
( select(a_38,X0) = select(a_42,X0)
| i1 = X0 ) ).
cnf(hyp24,hypothesis,
e_51 = select(a_50,i6) ).
cnf(hyp15,hypothesis,
e_33 = select(a1,i1) ).
cnf(u46,hypothesis,
e_47 = select(a_48,i5) ).
cnf(u61,hypothesis,
( select(a_46,X0) = select(a_50,X0)
| i5 = X0 ) ).
cnf(u37,hypothesis,
e_31 = select(a_32,i1) ).
cnf(u1284,hypothesis,
e_33 = select(a_40,i1) ).
cnf(u2760,negated_conjecture,
e_31 = select(a_58,i1) ).
cnf(u2854,negated_conjecture,
e_57 = select(a_44,i7) ).
cnf(u2401,hypothesis,
e_33 != e_47 ).
cnf(u2755,negated_conjecture,
e_31 = select(a2,i7) ).
cnf(u2494,negated_conjecture,
e_31 = select(a_48,i1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV556-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.16 % Computer : n002.cluster.edu
% 0.08/0.16 % Model : x86_64 x86_64
% 0.08/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.16 % Memory : 8046.5625MB
% 0.08/0.16 % OS : Linux 6.8.0-71-generic
% 0.08/0.16 % CPULimit : 300
% 0.08/0.16 % WCLimit : 300
% 0.08/0.16 % DateTime : Mon Sep 28 11:48:37 UTC 2026
% 0.08/0.16 % CPUTime :
% 0.08/0.16 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 Running first-order model finding
% 0.08/0.19 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
% 0.44/0.31 % (306704)Will run a generic schedule for satisfiability detection.
% 0.44/0.31 % (306713)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1096323882:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.44/0.31 % (306710)% WARNING: option uhcvi not known.
% 0.44/0.31 % (306709)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3337164079_2999 on theBenchmark for (2999ds/0Mi)
% 0.44/0.31 % (306714)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=798059098:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.44/0.31 % (306710)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3608899071:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.44/0.31 % (306715)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2362668846:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.44/0.31 % (306711)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2930362747:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.44/0.31 % (306712)dis+10_1_sil=32000:sp=arity:random_seed=507651560:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.44/0.31 % TRYING [1]
% 0.44/0.31 % TRYING [2]
% 0.44/0.31 % TRYING [3]
% 0.44/0.31 % TRYING [4]
% 0.44/0.31 % TRYING [5]
% 0.44/0.31 % (306713)Instruction limit reached!
% 0.44/0.31 % (306713)------------------------------
% 0.44/0.31 % (306713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.31 % (306713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.31 % (306713)CaDiCaL version: 2.1.3
% 0.44/0.31 % (306713)Termination reason: Instruction limit
% 0.44/0.31 % (306713)Termination phase: Saturation
% 0.44/0.31 % (306713)Time elapsed: 0.035 s
% 0.44/0.31 % (306713)Peak memory usage: 12 MB
% 0.44/0.31 % (306713)Instructions burned: 116 (million)
% 0.44/0.31 % (306723)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3109241386:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.44/0.31 % TRYING [1]
% 0.44/0.31 % TRYING [2]
% 0.44/0.31 % TRYING [6]
% 0.44/0.31 % TRYING [3]
% 0.44/0.31 % TRYING [4]
% 0.44/0.31 % TRYING [5]
% 0.44/0.31 % (306712)Instruction limit reached!
% 0.44/0.31 % (306712)------------------------------
% 0.44/0.31 % (306712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.31 % (306712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.31 % (306712)CaDiCaL version: 2.1.3
% 0.44/0.31 % (306712)Termination reason: Instruction limit
% 0.44/0.31 % (306712)Termination phase: Saturation
% 0.44/0.31 % (306712)Time elapsed: 0.058 s
% 0.44/0.31 % (306712)Peak memory usage: 12 MB
% 0.44/0.31 % (306712)Instructions burned: 105 (million)
% 0.44/0.31 % (306714)Instruction limit reached!
% 0.44/0.31 % (306714)------------------------------
% 0.44/0.31 % (306714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.31 % (306714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.31 % (306714)CaDiCaL version: 2.1.3
% 0.44/0.31 % (306714)Termination reason: Instruction limit
% 0.44/0.31 % (306714)Termination phase: Saturation
% 0.44/0.31 % (306714)Time elapsed: 0.064 s
% 0.44/0.31 % (306714)Peak memory usage: 12 MB
% 0.44/0.31 % (306714)Instructions burned: 132 (million)
% 0.44/0.31 % (306710) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-306704-306710"...
% 0.44/0.31 % (306710)...printing done.
% 0.44/0.31 % SZS status Satisfiable for theBenchmark
% 0.44/0.31 % SZS output start Saturation.
% See solution above
% 0.44/0.31 % SZS output start Definitions and Model Updates.
% 0.44/0.31 for all inputs,
% 0.44/0.31 define a_56 := a_58
% 0.44/0.31 % SZS output end Definitions and Model Updates.
% 0.44/0.31 % (306710)------------------------------
% 0.44/0.31 % (306710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.44/0.31 % (306710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.44/0.31 % (306710)CaDiCaL version: 2.1.3
% 0.44/0.31 % (306710)Termination reason: Satisfiable
% 0.44/0.31 % (306710)Time elapsed: 0.072 s
% 0.44/0.31 % (306710)Peak memory usage: 13 MB
% 0.44/0.31 % (306710)Instructions burned: 117 (million)
% 0.44/0.31 % (306704)Success in time 0.107 s
% 0.44/0.31 % Vampire exiting
%------------------------------------------------------------------------------