%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV536-1.010 : 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 : n015.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:07 PM UTC 2026
% Result : Satisfiable 40.82s 7.26s
% Output : Saturation 40.82s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u97,axiom,
store(sF44,i5,sF45) = sF46 ).
cnf(u890,axiom,
( sF0 = sF74
| i8 = i6
| i6 = i5
| i6 = i4
| i6 = i9
| i6 = i1
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3 ) ).
cnf(u377,axiom,
( sF16 = select(sF11,i1)
| i4 = i1
| i9 = i1 ) ).
cnf(u177,axiom,
sF24 = select(sF26,i0) ).
cnf(u1009,negated_conjecture,
( i1 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u63,axiom,
select(sF26,i1) = sF29 ).
cnf(u877,axiom,
( sF77 = select(sF7,sF76)
| i8 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i7 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u1061,negated_conjecture,
( i6 = sF76
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u986,negated_conjecture,
( sF31 = sF77
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u886,axiom,
( sF27 = sF66
| i8 = i2
| i7 = i2
| i6 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u373,axiom,
( sF12 = select(sF7,i9)
| i8 = i9
| i5 = i9 ) ).
cnf(u1164,negated_conjecture,
( sF4 != sF72
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9
| i6 = i2
| i6 = i3 ) ).
cnf(u681,axiom,
( sF55 = select(a1,i1)
| i7 = i1
| i8 = i1
| i6 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u1005,negated_conjecture,
( i6 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u916,axiom,
( sF14 = sF72
| i9 = i1
| i7 = i9
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3
| i8 = i4
| i7 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u907,axiom,
( sF78 = select(sF44,sF76)
| i5 = sF76
| i8 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i7 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76
| i6 = sF76 ) ).
cnf(u751,axiom,
( sF73 = store(sF71,i6,sF51)
| i9 = i1
| i7 = i9
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3 ) ).
cnf(u1059,negated_conjecture,
( sF29 != sF53
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1 ) ).
cnf(u1116,negated_conjecture,
( sF72 = sF78
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u633,axiom,
( sF12 = sF49
| i8 = i9
| i7 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u503,axiom,
( sF33 = select(sF19,i3)
| i1 = i3
| i2 = i3
| i0 = i3
| i4 = i3
| i5 = i3 ) ).
cnf(u928,axiom,
( sF71 = store(sF69,i0,sF33)
| i8 = i3
| i7 = i3
| i6 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u1110,negated_conjecture,
( sF77 = select(sF19,i6)
| i6 = i0
| i6 = i2
| i6 = i3
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u731,axiom,
( sF27 = select(sF7,i2)
| i8 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u1109,negated_conjecture,
( sF77 = select(sF15,i6)
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u1011,negated_conjecture,
( i7 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u336,axiom,
( sF53 = select(sF56,i1)
| i7 = i1 ) ).
cnf(u489,axiom,
( sF49 = sF59
| i4 = i9
| i4 = i1
| i7 = i4 ) ).
cnf(u502,axiom,
( sF27 = select(sF19,i2)
| i0 = i2
| i4 = i2
| i5 = i2 ) ).
cnf(u443,axiom,
( select(sF56,X0) = select(sF63,X0)
| i0 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u781,axiom,
( sF2 = sF29
| i1 = i0
| i4 = i1
| i5 = i1
| i7 = i6
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u727,axiom,
( sF70 = select(sF48,i3)
| i4 = i3
| i9 = i3
| i1 = i3
| i7 = i3
| i2 = i3
| i0 = i3
| i5 = i3 ) ).
cnf(u962,negated_conjecture,
( i7 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u25,axiom,
select(sF7,i8) = sF10 ).
cnf(u141,axiom,
select(sF67,i0) = sF68 ).
cnf(u332,axiom,
( sF49 = select(sF52,i4)
| i4 = i9 ) ).
cnf(u135,axiom,
store(sF63,i2,sF64) = sF65 ).
cnf(u1007,negated_conjecture,
( i4 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u250,axiom,
sF43 = sF45 ).
cnf(u91,axiom,
select(sF40,i6) = sF43 ).
cnf(u282,axiom,
( select(sF11,X0) = select(sF15,X0)
| i4 = X0
| i9 = X0 ) ).
cnf(u440,axiom,
( sF59 = select(sF52,i4)
| i4 = i1
| i7 = i4 ) ).
cnf(u635,axiom,
( sF52 = store(sF50,i9,sF14)
| i8 = i4
| i7 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u313,axiom,
( select(a1,X0) = select(sF40,X0)
| i7 = X0
| i8 = X0 ) ).
cnf(u93,axiom,
store(sF42,i8,sF43) = sF44 ).
cnf(u434,axiom,
( sF55 = select(sF48,i1)
| i4 = i1
| i9 = i1 ) ).
cnf(u49,axiom,
select(sF19,i4) = sF22 ).
cnf(u828,axiom,
( sF62 = store(sF60,i0,sF24)
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0 ) ).
cnf(u87,axiom,
select(sF40,i8) = sF41 ).
cnf(u245,axiom,
sF11 = store(sF9,i5,sF6) ).
cnf(u414,axiom,
( sF43 = select(a1,i6)
| i7 = i6
| i8 = i6 ) ).
cnf(u436,axiom,
( sF24 = select(sF15,i0)
| i7 = i0
| i1 = i0
| i4 = i0
| i5 = i0 ) ).
cnf(u43,axiom,
store(sF17,i1,sF18) = sF19 ).
cnf(u232,axiom,
( select(sF54,X0) = select(sF56,X0)
| i7 = X0 ) ).
cnf(u73,axiom,
store(sF32,i0,sF33) = sF34 ).
cnf(u706,axiom,
( sF74 = select(sF52,i6)
| i6 = i1
| i7 = i6
| i6 = i0
| i6 = i4
| i6 = i5
| i6 = i2
| i6 = i3 ) ).
cnf(u264,axiom,
sF0 = select(sF42,i6) ).
cnf(u397,axiom,
( sF33 = select(sF26,i3)
| i1 = i3
| i2 = i3 ) ).
cnf(u430,axiom,
( sF12 = sF22
| i4 = i9
| i7 = i4
| i4 = i1 ) ).
cnf(u45,axiom,
select(sF19,i5) = sF20 ).
cnf(u226,axiom,
( select(sF42,X0) = select(sF44,X0)
| i8 = X0 ) ).
cnf(u67,axiom,
select(sF30,i0) = sF31 ).
cnf(u677,axiom,
( sF65 = store(sF63,i2,sF2)
| i7 = i1
| i1 = i0
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u416,axiom,
( sF16 = select(sF7,i1)
| i8 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u39,axiom,
store(sF15,i7,sF16) = sF17 ).
cnf(u228,axiom,
( select(sF46,X0) = select(sF48,X0)
| i8 = X0 ) ).
cnf(u69,axiom,
store(sF30,i3,sF31) = sF32 ).
cnf(u260,axiom,
( sF0 = sF4
| i8 = i7 ) ).
cnf(u219,axiom,
( select(sF28,X0) = select(sF30,X0)
| i2 = X0 ) ).
cnf(u184,axiom,
sF0 = select(sF40,i8) ).
cnf(u319,axiom,
( select(sF40,X0) = select(sF44,X0)
| i6 = X0
| i8 = X0 ) ).
cnf(u658,axiom,
( sF58 = store(sF56,i4,sF43)
| i8 = i5
| i5 = i4
| i5 = i9
| i5 = i1
| i7 = i5 ) ).
cnf(u349,axiom,
( select(sF63,X0) = select(sF67,X0)
| i2 = X0
| i1 = X0 ) ).
cnf(u983,negated_conjecture,
( sF68 != sF77
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u178,axiom,
sF27 = select(sF28,i1) ).
cnf(u981,negated_conjecture,
( sF68 = sF78
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u19,axiom,
store(sF5,i8,sF6) = sF7 ).
cnf(u629,axiom,
( sF14 = sF51
| i8 = i4
| i7 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u317,axiom,
( sF0 = select(sF44,i6)
| i8 = i6 ) ).
cnf(u959,negated_conjecture,
( sF78 = select(sF75,i3)
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u180,axiom,
sF31 = select(sF32,i3) ).
cnf(u21,axiom,
select(sF7,i5) = sF8 ).
cnf(u147,axiom,
store(sF69,i0,sF70) = sF71 ).
cnf(u495,axiom,
( sF72 = select(sF63,i9)
| i9 = i2
| i9 = i1
| i9 = i3
| i9 = i0 ) ).
cnf(u829,axiom,
( sF69 = store(sF67,i3,sF24)
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u1171,negated_conjecture,
( sF4 != sF14
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9
| i6 = i2
| i6 = i3
| i9 = i1
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3
| i8 = i4
| i5 = i4 ) ).
cnf(u15,axiom,
store(sF3,i6,sF4) = sF5 ).
cnf(u149,axiom,
select(sF71,i9) = sF72 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(u325,axiom,
( sF43 = select(sF48,i5)
| i8 = i5 ) ).
cnf(u904,axiom,
( sF24 = sF68
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u761,axiom,
( sF74 = select(sF48,i6)
| i6 = i4
| i6 = i9
| i6 = i1
| i7 = i6
| i6 = i0
| i6 = i5
| i6 = i2
| i6 = i3 ) ).
cnf(u281,axiom,
( sF12 = select(sF15,i4)
| i4 = i9 ) ).
cnf(u900,axiom,
( sF70 = select(a1,i3)
| i7 = i3
| i8 = i3
| i6 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u275,axiom,
( sF8 = select(sF11,i8)
| i8 = i5 ) ).
cnf(u1169,negated_conjecture,
( sF4 != sF51
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9
| i6 = i2
| i6 = i3
| i9 = i1
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3 ) ).
cnf(u519,axiom,
( sF60 = store(sF58,i5,sF49)
| i4 = i9
| i4 = i1
| i7 = i4 ) ).
cnf(u1008,negated_conjecture,
( i9 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u855,axiom,
( sF70 = select(sF40,i3)
| i6 = i3
| i8 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i7 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u309,axiom,
( select(sF34,X0) = select(sF38,X0)
| i9 = X0
| i5 = X0 ) ).
cnf(u648,axiom,
( sF27 = select(sF11,i2)
| i4 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i0 = i2
| i5 = i2 ) ).
cnf(u661,axiom,
( sF16 = select(a1,i1)
| i8 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u327,axiom,
( select(sF44,X0) = select(sF48,X0)
| i5 = X0
| i8 = X0 ) ).
cnf(u240,axiom,
( select(sF69,X0) = select(sF71,X0)
| i0 = X0 ) ).
cnf(u611,axiom,
( sF74 = select(sF56,i6)
| i6 = i0
| i6 = i4
| i6 = i5
| i6 = i2
| i6 = i1
| i6 = i3 ) ).
cnf(u832,axiom,
( sF77 = select(sF11,sF76)
| i4 = sF76
| i9 = sF76
| i7 = sF76
| i1 = sF76
| i0 = sF76
| i5 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u410,axiom,
( sF77 = select(sF34,sF76)
| i9 = sF76
| i5 = sF76 ) ).
cnf(u1076,negated_conjecture,
( i6 != i9
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u222,axiom,
( select(sF34,X0) = select(sF36,X0)
| i9 = X0 ) ).
cnf(u804,axiom,
( sF12 = sF35
| i5 = i0
| i5 = i1
| i5 = i2
| i5 = i3
| i4 = i9
| i7 = i4
| i4 = i1 ) ).
cnf(u221,axiom,
( select(sF32,X0) = select(sF34,X0)
| i0 = X0 ) ).
cnf(u412,axiom,
( sF18 = select(sF7,i7)
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u607,axiom,
( sF61 = select(sF48,i0)
| i4 = i0
| i9 = i0
| i1 = i0
| i7 = i0
| i5 = i0 ) ).
cnf(u208,axiom,
( select(sF7,X0) = select(sF9,X0)
| i8 = X0 ) ).
cnf(u95,axiom,
select(sF44,i8) = sF45 ).
cnf(u215,axiom,
( select(sF21,X0) = select(sF23,X0)
| i5 = X0 ) ).
cnf(u1151,negated_conjecture,
( sF4 = sF77
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u1100,negated_conjecture,
( sF77 = select(sF30,i6)
| i6 = i3
| i6 = i0
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u202,axiom,
sF74 = select(sF75,i9) ).
cnf(u784,axiom,
( sF66 = select(sF40,i2)
| i6 = i2
| i8 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i0 = i2 ) ).
cnf(u171,axiom,
sF14 = select(sF15,i9) ).
cnf(u866,axiom,
( sF27 = select(a1,i2)
| i8 = i2
| i7 = i2
| i6 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u201,axiom,
sF72 = select(sF73,i6) ).
cnf(u174,axiom,
sF20 = select(sF21,i4) ).
cnf(u587,axiom,
( sF37 = select(sF19,i9)
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i1
| i9 = i2
| i9 = i3 ) ).
cnf(u204,axiom,
( select(a1,X0) = select(sF39,X0)
| i7 = X0 ) ).
cnf(u173,axiom,
sF18 = select(sF19,i1) ).
cnf(u364,axiom,
( sF59 = select(sF63,i5)
| i5 = i0 ) ).
cnf(u195,axiom,
sF61 = select(sF62,i0) ).
cnf(u748,axiom,
( sF61 = select(sF40,i0)
| i6 = i0
| i8 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0
| i7 = i0 ) ).
cnf(u285,axiom,
( sF16 = select(sF19,i7)
| i7 = i1 ) ).
cnf(u198,axiom,
sF66 = select(sF67,i1) ).
cnf(u167,axiom,
sF6 = select(sF7,i8) ).
cnf(u963,negated_conjecture,
( i6 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u197,axiom,
sF64 = select(sF65,i2) ).
cnf(u388,axiom,
( select(sF19,X0) = select(sF26,X0)
| i0 = X0
| i4 = X0
| i5 = X0 ) ).
cnf(u862,axiom,
( sF78 = select(sF48,sF76)
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i7 = sF76
| i0 = sF76
| i5 = sF76
| i2 = sF76
| i3 = sF76
| i6 = sF76 ) ).
cnf(u123,axiom,
select(sF56,i4) = sF59 ).
cnf(u548,axiom,
( sF49 = select(a1,i9)
| i7 = i9
| i8 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u153,axiom,
select(sF71,i6) = sF74 ).
cnf(u344,axiom,
( select(sF60,X0) = select(sF63,X0)
| i0 = X0 ) ).
cnf(u615,axiom,
( sF72 = select(sF56,i9)
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i1
| i9 = i3 ) ).
cnf(u539,axiom,
( sF8 = sF47
| i8 = i5
| i7 = i5
| i6 = i5 ) ).
cnf(u946,axiom,
( sF77 = select(a1,sF76)
| i8 = sF76
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u1019,negated_conjecture,
( sF78 = select(sF67,i2)
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u125,axiom,
store(sF58,i5,sF59) = sF60 ).
cnf(u433,axiom,
( sF53 = select(sF48,i7)
| i7 = i4
| i7 = i9 ) ).
cnf(u757,axiom,
( sF77 = select(sF15,sF76)
| i7 = sF76
| i1 = sF76
| i0 = sF76
| i4 = sF76
| i5 = sF76
| i2 = sF76
| i3 = sF76
| i9 = sF76 ) ).
cnf(u819,axiom,
( sF24 = sF61
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0 ) ).
cnf(u119,axiom,
select(sF56,i5) = sF57 ).
cnf(u970,negated_conjecture,
( i8 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u427,axiom,
( sF51 = select(sF44,i4)
| i5 = i4
| i8 = i4 ) ).
cnf(u340,axiom,
( sF57 = select(sF60,i4)
| i5 = i4 ) ).
cnf(u457,axiom,
( sF72 = select(sF67,i9)
| i9 = i3
| i9 = i0 ) ).
cnf(u535,axiom,
( sF12 = select(a1,i9)
| i8 = i9
| i7 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u105,axiom,
store(sF48,i4,sF49) = sF50 ).
cnf(u296,axiom,
( select(sF23,X0) = select(sF26,X0)
| i0 = X0 ) ).
cnf(u143,axiom,
store(sF67,i3,sF68) = sF69 ).
cnf(u994,negated_conjecture,
( sF24 != sF61
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0 ) ).
cnf(u451,axiom,
( sF61 = sF68
| i0 = i2
| i1 = i0 ) ).
cnf(u582,axiom,
( sF22 = sF35
| i5 = i0
| i5 = i1
| i5 = i2
| i5 = i3 ) ).
cnf(u407,axiom,
( sF12 = select(sF3,i9)
| i6 = i9
| i8 = i9
| i5 = i9 ) ).
cnf(u99,axiom,
select(sF44,i5) = sF47 ).
cnf(u966,negated_conjecture,
( i9 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u129,axiom,
store(sF60,i0,sF61) = sF62 ).
cnf(u453,axiom,
( sF69 = store(sF67,i3,sF61)
| i0 = i2
| i1 = i0 ) ).
cnf(u922,axiom,
( sF77 = select(sF3,sF76)
| i6 = sF76
| i8 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i7 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u179,axiom,
sF29 = select(sF30,i2) ).
cnf(u101,axiom,
store(sF46,i8,sF47) = sF48 ).
cnf(u182,axiom,
sF35 = select(sF36,i9) ).
cnf(u292,axiom,
( sF20 = select(sF23,i4)
| i5 = i4 ) ).
cnf(u57,axiom,
store(sF25,i0,sF24) = sF26 ).
cnf(u381,axiom,
( sF22 = select(sF15,i4)
| i7 = i4
| i4 = i1 ) ).
cnf(u286,axiom,
( select(sF15,X0) = select(sF19,X0)
| i7 = X0
| i1 = X0 ) ).
cnf(u403,axiom,
( sF35 = select(sF30,i5)
| i5 = i3
| i5 = i0 ) ).
cnf(u51,axiom,
store(sF21,i5,sF22) = sF23 ).
cnf(u81,axiom,
store(sF36,i5,sF37) = sF38 ).
cnf(u175,axiom,
sF22 = select(sF23,i5) ).
cnf(u53,axiom,
select(sF23,i0) = sF24 ).
cnf(u361,axiom,
( sF20 = select(sF26,i4)
| i5 = i4
| i4 = i0 ) ).
cnf(u685,axiom,
( sF61 = select(sF44,i0)
| i5 = i0
| i8 = i0
| i4 = i0
| i9 = i0
| i1 = i0
| i7 = i0 ) ).
cnf(u514,axiom,
( sF70 = select(sF56,i3)
| i2 = i3
| i1 = i3
| i0 = i3
| i4 = i3
| i5 = i3 ) ).
cnf(u47,axiom,
store(sF19,i4,sF20) = sF21 ).
cnf(u513,axiom,
( sF66 = select(sF56,i2)
| i0 = i2
| i4 = i2
| i5 = i2 ) ).
cnf(u151,axiom,
store(sF71,i6,sF72) = sF73 ).
cnf(u870,axiom,
( sF2 = sF64
| i7 = i1
| i1 = i0
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u544,axiom,
( sF51 = select(a1,i4)
| i7 = i4
| i8 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u357,axiom,
( select(sF71,X0) = select(sF75,X0)
| i6 = X0
| i9 = X0 ) ).
cnf(u739,axiom,
( sF24 = select(sF3,i0)
| i6 = i0
| i8 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i0
| i1 = i0 ) ).
cnf(u1066,negated_conjecture,
( sF78 = select(sF75,i6)
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u989,negated_conjecture,
( sF31 != sF68
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u497,axiom,
( sF78 = select(sF67,sF76)
| i3 = sF76
| i0 = sF76
| i6 = sF76
| i9 = sF76 ) ).
cnf(u75,axiom,
select(sF34,i5) = sF35 ).
cnf(u553,axiom,
( sF53 = sF64
| i7 = i1
| i1 = i0
| i4 = i1
| i5 = i1 ) ).
cnf(u735,axiom,
( sF66 = select(sF44,i2)
| i5 = i2
| i8 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i0 = i2 ) ).
cnf(u700,axiom,
( sF58 = store(sF56,i4,sF6)
| i8 = i5
| i5 = i4
| i5 = i9
| i5 = i1
| i7 = i5
| i8 = i6
| i7 = i6 ) ).
cnf(u618,axiom,
( sF78 = select(sF63,sF76)
| i2 = sF76
| i1 = sF76
| i3 = sF76
| i0 = sF76
| i6 = sF76
| i9 = sF76 ) ).
cnf(u691,axiom,
( sF14 = sF37
| i7 = i9
| i9 = i1
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3 ) ).
cnf(u224,axiom,
( select(sF39,X0) = select(sF40,X0)
| i8 = X0 ) ).
cnf(u769,axiom,
( sF70 = select(sF44,i3)
| i5 = i3
| i8 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i7 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u715,axiom,
( sF51 = sF72
| i9 = i1
| i7 = i9
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3 ) ).
cnf(u487,axiom,
( sF57 = select(sF48,i5)
| i5 = i4
| i5 = i9
| i5 = i1
| i7 = i5 ) ).
cnf(u1065,negated_conjecture,
( sF77 = select(sF38,i6)
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u668,axiom,
( sF24 = select(sF7,i0)
| i8 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i0
| i1 = i0 ) ).
cnf(u515,axiom,
( sF23 = store(sF21,i5,sF12)
| i4 = i9
| i7 = i4
| i4 = i1 ) ).
cnf(u839,axiom,
( sF74 = select(sF44,i6)
| i6 = i5
| i8 = i6
| i6 = i4
| i6 = i9
| i6 = i1
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3 ) ).
cnf(u956,negated_conjecture,
( i3 = sF76
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u251,axiom,
sF46 = store(sF44,i5,sF43) ).
cnf(u341,axiom,
( select(sF56,X0) = select(sF60,X0)
| i4 = X0
| i5 = X0 ) ).
cnf(u1046,negated_conjecture,
( sF64 = sF78
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u472,axiom,
( sF47 = select(a1,i5)
| i7 = i5
| i8 = i5
| i6 = i5 ) ).
cnf(u253,axiom,
sF6 = select(sF11,i5) ).
cnf(u444,axiom,
( sF61 = select(sF56,i0)
| i4 = i0
| i5 = i0 ) ).
cnf(u639,axiom,
( sF60 = store(sF58,i5,sF12)
| i4 = i9
| i4 = i1
| i7 = i4
| i8 = i9
| i7 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u466,axiom,
( sF6 = sF43
| i8 = i6
| i7 = i6 ) ).
cnf(u276,axiom,
( select(sF7,X0) = select(sF11,X0)
| i8 = X0
| i5 = X0 ) ).
cnf(u272,axiom,
sF43 = select(sF46,i5) ).
cnf(u247,axiom,
sF0 = sF41 ).
cnf(u656,axiom,
( sF66 = select(sF48,i2)
| i4 = i2
| i9 = i2
| i1 = i2
| i7 = i2
| i0 = i2
| i5 = i2 ) ).
cnf(u468,axiom,
( sF46 = store(sF44,i5,sF6)
| i8 = i6
| i7 = i6 ) ).
cnf(u213,axiom,
( select(sF17,X0) = select(sF19,X0)
| i1 = X0 ) ).
cnf(u233,axiom,
( select(sF56,X0) = select(sF58,X0)
| i4 = X0 ) ).
cnf(u236,axiom,
( select(sF62,X0) = select(sF63,X0)
| i0 = X0 ) ).
cnf(u77,axiom,
store(sF34,i9,sF35) = sF36 ).
cnf(u813,axiom,
( sF73 = store(sF71,i6,sF14)
| i9 = i1
| i7 = i9
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3
| i8 = i4
| i7 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u268,axiom,
( select(sF3,X0) = select(sF7,X0)
| i6 = X0
| i8 = X0 ) ).
cnf(u227,axiom,
( select(sF44,X0) = select(sF46,X0)
| i5 = X0 ) ).
cnf(u418,axiom,
( sF47 = select(sF40,i5)
| i6 = i5
| i8 = i5 ) ).
cnf(u33,axiom,
select(sF11,i4) = sF14 ).
cnf(u230,axiom,
( select(sF50,X0) = select(sF52,X0)
| i9 = X0 ) ).
cnf(u71,axiom,
select(sF30,i3) = sF33 ).
cnf(u262,axiom,
( sF5 = store(sF3,i6,sF0)
| i8 = i7 ) ).
cnf(u229,axiom,
( select(sF48,X0) = select(sF50,X0)
| i4 = X0 ) ).
cnf(u404,axiom,
( sF37 = select(sF30,i9)
| i9 = i3
| i9 = i0 ) ).
cnf(u186,axiom,
sF43 = select(sF44,i8) ).
cnf(u1022,negated_conjecture,
( sF77 = select(sF34,i2)
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u27,axiom,
store(sF9,i5,sF10) = sF11 ).
cnf(u216,axiom,
( select(sF23,X0) = select(sF25,X0)
| i0 = X0 ) ).
cnf(u185,axiom,
sF41 = select(sF42,i6) ).
cnf(u376,axiom,
( sF18 = select(sF11,i7)
| i7 = i4
| i7 = i9 ) ).
cnf(u223,axiom,
( select(sF36,X0) = select(sF38,X0)
| i5 = X0 ) ).
cnf(u439,axiom,
( sF57 = select(sF52,i5)
| i5 = i1
| i7 = i5 ) ).
cnf(u188,axiom,
sF47 = select(sF48,i8) ).
cnf(u29,axiom,
select(sF11,i9) = sF12 ).
cnf(u210,axiom,
( select(sF11,X0) = select(sF13,X0)
| i4 = X0 ) ).
cnf(u337,axiom,
( select(sF52,X0) = select(sF56,X0)
| i1 = X0
| i7 = X0 ) ).
cnf(u209,axiom,
( select(sF9,X0) = select(sF11,X0)
| i5 = X0 ) ).
cnf(u400,axiom,
( sF32 = store(sF30,i3,sF24)
| i1 = i0
| i0 = i2 ) ).
cnf(u969,negated_conjecture,
( i2 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u23,axiom,
store(sF7,i8,sF8) = sF9 ).
cnf(u212,axiom,
( select(sF15,X0) = select(sF17,X0)
| i7 = X0 ) ).
cnf(u181,axiom,
sF33 = select(sF34,i0) ).
cnf(u372,axiom,
( sF14 = select(sF7,i4)
| i8 = i4
| i5 = i4 ) ).
cnf(u203,axiom,
( select(a1,X0) = select(sF1,X0)
| i8 = X0 ) ).
cnf(u531,axiom,
( sF14 = select(a1,i4)
| i8 = i4
| i7 = i4
| i6 = i4
| i5 = i4 ) ).
cnf(u168,axiom,
sF8 = select(sF9,i8) ).
cnf(u9,axiom,
select(a1,i8) = sF2 ).
cnf(u642,axiom,
( sF19 = store(sF17,i1,sF2)
| i7 = i6
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u333,axiom,
( select(sF48,X0) = select(sF52,X0)
| i4 = X0
| i9 = X0 ) ).
cnf(u483,axiom,
( sF53 = select(sF44,i7)
| i7 = i5
| i8 = i7
| i7 = i4
| i7 = i9 ) ).
cnf(u384,axiom,
( sF8 = select(a1,i5)
| i8 = i5
| i7 = i5
| i6 = i5 ) ).
cnf(u162,negated_conjecture,
sF77 != sF78 ).
cnf(u965,negated_conjecture,
( i4 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u161,axiom,
select(sF75,sF76) = sF78 ).
cnf(u485,axiom,
( sF55 = select(sF44,i1)
| i5 = i1
| i8 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u164,axiom,
sF2 = select(sF39,i7) ).
cnf(u5,axiom,
select(a1,i7) = sF0 ).
cnf(u520,axiom,
( sF30 = store(sF28,i2,sF18)
| i1 = i0
| i4 = i1
| i5 = i1 ) ).
cnf(u765,axiom,
( sF33 = select(sF7,i3)
| i8 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i7 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u827,axiom,
( sF63 = store(sF62,i0,sF24)
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0 ) ).
cnf(u127,axiom,
select(sF60,i0) = sF61 ).
cnf(u950,axiom,
( sF78 = select(a1,sF76)
| i7 = sF76
| i8 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u113,axiom,
store(sF52,i1,sF53) = sF54 ).
cnf(u873,axiom,
( sF66 = select(a1,i2)
| i7 = i2
| i8 = i2
| i6 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u745,axiom,
( sF56 = store(sF54,i7,sF16)
| i8 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u589,axiom,
( sF36 = store(sF34,i9,sF22)
| i5 = i0
| i5 = i1
| i5 = i2
| i5 = i3 ) ).
cnf(u897,axiom,
( sF75 = store(sF73,i9,sF0)
| i8 = i6
| i6 = i5
| i6 = i4
| i6 = i9
| i6 = i1
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3 ) ).
cnf(u259,axiom,
( select(a1,X0) = select(sF3,X0)
| i8 = X0
| i7 = X0 ) ).
cnf(u1012,negated_conjecture,
( i8 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u698,axiom,
( sF77 = select(sF19,sF76)
| i0 = sF76
| i4 = sF76
| i5 = sF76
| i1 = sF76
| i2 = sF76
| i3 = sF76
| i9 = sF76 ) ).
cnf(u967,negated_conjecture,
( i1 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u1021,negated_conjecture,
( sF78 = select(sF71,i2)
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u991,negated_conjecture,
( sF31 != sF61
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0 ) ).
cnf(u541,axiom,
( sF48 = store(sF46,i8,sF8)
| i8 = i5
| i7 = i5
| i6 = i5 ) ).
cnf(u836,axiom,
( sF6 = sF57
| i8 = i5
| i5 = i4
| i5 = i9
| i5 = i1
| i7 = i5
| i8 = i6
| i7 = i6 ) ).
cnf(u238,axiom,
( select(sF65,X0) = select(sF67,X0)
| i1 = X0 ) ).
cnf(u792,axiom,
( sF61 = select(a1,i0)
| i7 = i0
| i8 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0 ) ).
cnf(u604,axiom,
( sF43 = sF57
| i8 = i5
| i5 = i4
| i5 = i9
| i5 = i1
| i7 = i5 ) ).
cnf(u992,negated_conjecture,
( i2 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u895,axiom,
( sF33 = select(a1,i3)
| i8 = i3
| i7 = i3
| i6 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u1126,negated_conjecture,
( sF72 != sF77
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u206,axiom,
( select(sF3,X0) = select(sF5,X0)
| i6 = X0 ) ).
cnf(u788,axiom,
( sF24 = select(a1,i0)
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i1 = i0 ) ).
cnf(u584,axiom,
( sF65 = store(sF63,i2,sF53)
| i7 = i1
| i1 = i0
| i4 = i1
| i5 = i1 ) ).
cnf(u205,axiom,
( select(sF1,X0) = select(sF3,X0)
| i7 = X0 ) ).
cnf(u83,axiom,
store(a1,i7,sF2) = sF39 ).
cnf(u239,axiom,
( select(sF67,X0) = select(sF69,X0)
| i3 = X0 ) ).
cnf(u561,axiom,
( sF2 = sF18
| i7 = i6
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u591,axiom,
( sF77 = select(sF26,sF76)
| i1 = sF76
| i2 = sF76
| i3 = sF76
| i0 = sF76
| i9 = sF76
| i5 = sF76 ) ).
cnf(u192,axiom,
sF55 = select(sF56,i7) ).
cnf(u556,axiom,
( sF21 = store(sF19,i4,sF6)
| i5 = i4
| i5 = i9
| i7 = i5
| i5 = i1 ) ).
cnf(u352,axiom,
( sF68 = select(sF71,i3)
| i0 = i3 ) ).
cnf(u199,axiom,
sF68 = select(sF69,i3) ).
cnf(u641,axiom,
( sF30 = store(sF28,i2,sF2)
| i1 = i0
| i4 = i1
| i5 = i1
| i7 = i6
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u1075,negated_conjecture,
( i6 != i4
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u155,axiom,
store(sF73,i9,sF74) = sF75 ).
cnf(u504,axiom,
( sF18 = sF29
| i1 = i0
| i4 = i1
| i5 = i1 ) ).
cnf(u1023,negated_conjecture,
( sF29 = sF77
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u1108,negated_conjecture,
( sF77 = select(sF11,i6)
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u79,axiom,
select(sF34,i9) = sF37 ).
cnf(u1077,negated_conjecture,
( i6 != i1
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u157,axiom,
sk(sF38,sF75) = sF76 ).
cnf(u348,axiom,
( sF64 = select(sF67,i2)
| i1 = i2 ) ).
cnf(u1080,negated_conjecture,
( i8 != i6
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u423,axiom,
( sF6 = sF20
| i5 = i4
| i5 = i9
| i7 = i5
| i5 = i1 ) ).
cnf(u304,axiom,
( sF31 = select(sF34,i3)
| i0 = i3 ) ).
cnf(u723,axiom,
( sF33 = select(sF11,i3)
| i4 = i3
| i9 = i3
| i7 = i3
| i1 = i3
| i2 = i3
| i0 = i3
| i5 = i3 ) ).
cnf(u459,axiom,
( sF37 = select(sF26,i9)
| i9 = i1
| i9 = i2
| i9 = i3
| i9 = i0 ) ).
cnf(u267,axiom,
( sF4 = select(sF7,i6)
| i8 = i6 ) ).
cnf(u1074,negated_conjecture,
( i6 != i5
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u107,axiom,
select(sF48,i4) = sF51 ).
cnf(u974,negated_conjecture,
( sF77 = select(sF34,i3)
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u137,axiom,
select(sF63,i2) = sF66 ).
cnf(u461,axiom,
( sF78 = select(sF71,sF76)
| i6 = sF76
| i9 = sF76 ) ).
cnf(u109,axiom,
store(sF50,i9,sF51) = sF52 ).
cnf(u968,negated_conjecture,
( i0 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u300,axiom,
( sF27 = select(sF30,i1)
| i1 = i2 ) ).
cnf(u131,axiom,
store(sF62,i0,sF61) = sF63 ).
cnf(u207,axiom,
( select(sF5,X0) = select(sF7,X0)
| i8 = X0 ) ).
cnf(u480,axiom,
( sF49 = select(sF40,i9)
| i6 = i9
| i8 = i9
| i5 = i9 ) ).
cnf(u103,axiom,
select(sF48,i9) = sF49 ).
cnf(u512,axiom,
( sF64 = select(sF56,i1)
| i1 = i0
| i4 = i1
| i5 = i1 ) ).
cnf(u133,axiom,
select(sF63,i1) = sF64 ).
cnf(u59,axiom,
select(sF26,i2) = sF27 ).
cnf(u248,axiom,
sF42 = store(sF40,i6,sF0) ).
cnf(u89,axiom,
store(sF40,i6,sF41) = sF42 ).
cnf(u446,axiom,
( sF35 = select(sF26,i5)
| i5 = i1
| i5 = i2
| i5 = i3
| i5 = i0 ) ).
cnf(u61,axiom,
store(sF26,i1,sF27) = sF28 ).
cnf(u242,axiom,
( select(sF73,X0) = select(sF75,X0)
| i9 = X0 ) ).
cnf(u369,axiom,
( sF8 = select(sF3,i5)
| i6 = i5
| i8 = i5 ) ).
cnf(u241,axiom,
( select(sF71,X0) = select(sF73,X0)
| i6 = X0 ) ).
cnf(u55,axiom,
store(sF23,i0,sF24) = sF25 ).
cnf(u244,axiom,
sF6 = sF10 ).
cnf(u85,axiom,
store(sF39,i8,sF0) = sF40 ).
cnf(u172,axiom,
sF16 = select(sF17,i7) ).
cnf(u353,axiom,
( select(sF67,X0) = select(sF71,X0)
| i3 = X0
| i0 = X0 ) ).
cnf(u41,axiom,
select(sF15,i7) = sF18 ).
cnf(u365,axiom,
( sF57 = select(sF63,i4)
| i5 = i4
| i4 = i0 ) ).
cnf(u367,axiom,
( sF6 = select(a1,i6)
| i8 = i6
| i7 = i6 ) ).
cnf(u35,axiom,
store(sF13,i9,sF14) = sF15 ).
cnf(u65,axiom,
store(sF28,i2,sF29) = sF30 ).
cnf(u389,axiom,
( sF24 = select(sF19,i0)
| i4 = i0
| i5 = i0 ) ).
cnf(u37,axiom,
select(sF15,i1) = sF16 ).
cnf(u964,negated_conjecture,
( i5 != i3
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u31,axiom,
store(sF11,i4,sF12) = sF13 ).
cnf(u625,axiom,
( sF70 = select(sF52,i3)
| i1 = i3
| i7 = i3
| i2 = i3
| i0 = i3
| i4 = i3
| i5 = i3 ) ).
cnf(u17,axiom,
select(sF3,i6) = sF6 ).
cnf(u650,axiom,
( sF36 = store(sF34,i9,sF12)
| i5 = i0
| i5 = i1
| i5 = i2
| i5 = i3
| i4 = i9
| i7 = i4
| i4 = i1 ) ).
cnf(u777,axiom,
( sF27 = select(sF3,i2)
| i6 = i2
| i8 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i7 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u234,axiom,
( select(sF58,X0) = select(sF60,X0)
| i5 = X0 ) ).
cnf(u1101,negated_conjecture,
( sF77 = select(sF34,i6)
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u678,axiom,
( sF54 = store(sF52,i1,sF2)
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u621,axiom,
( sF33 = select(sF15,i3)
| i7 = i3
| i1 = i3
| i2 = i3
| i0 = i3
| i4 = i3
| i5 = i3 ) ).
cnf(u145,axiom,
select(sF67,i3) = sF70 ).
cnf(u1111,negated_conjecture,
( sF77 = select(sF7,i6)
| i7 = i6
| i6 = i0
| i6 = i2
| i6 = i3
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u773,axiom,
( sF78 = select(sF52,sF76)
| i1 = sF76
| i7 = sF76
| i0 = sF76
| i4 = sF76
| i5 = sF76
| i2 = sF76
| i3 = sF76
| i6 = sF76
| i9 = sF76 ) ).
cnf(u719,axiom,
( sF78 = select(sF56,sF76)
| i0 = sF76
| i4 = sF76
| i5 = sF76
| i2 = sF76
| i1 = sF76
| i3 = sF76
| i6 = sF76
| i9 = sF76 ) ).
cnf(u926,axiom,
( sF33 = sF70
| i8 = i3
| i7 = i3
| i6 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u293,axiom,
( select(sF19,X0) = select(sF23,X0)
| i4 = X0
| i5 = X0 ) ).
cnf(u675,axiom,
( sF2 = sF53
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u601,axiom,
( sF55 = select(sF40,i1)
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u999,negated_conjecture,
( sF77 = select(sF38,i2)
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u1056,negated_conjecture,
( sF29 != sF64
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u476,axiom,
( sF51 = select(sF40,i4)
| i6 = i4
| i8 = i4
| i5 = i4 ) ).
cnf(u1050,negated_conjecture,
( sF64 != sF77
| i2 = i3
| i0 = i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u973,negated_conjecture,
( sF78 = select(sF71,i3)
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u848,axiom,
( sF33 = select(sF3,i3)
| i6 = i3
| i8 = i3
| i5 = i3
| i4 = i3
| i9 = i3
| i7 = i3
| i1 = i3
| i2 = i3
| i0 = i3 ) ).
cnf(u235,axiom,
( select(sF60,X0) = select(sF62,X0)
| i0 = X0 ) ).
cnf(u305,axiom,
( select(sF30,X0) = select(sF34,X0)
| i3 = X0
| i0 = X0 ) ).
cnf(u456,axiom,
( sF74 = select(sF67,i6)
| i6 = i3
| i6 = i0 ) ).
cnf(u237,axiom,
( select(sF63,X0) = select(sF65,X0)
| i2 = X0 ) ).
cnf(u428,axiom,
( sF49 = select(sF44,i9)
| i5 = i9
| i8 = i9 ) ).
cnf(u450,axiom,
( sF70 = select(sF63,i3)
| i2 = i3
| i1 = i3 ) ).
cnf(u931,axiom,
( sF78 = select(sF40,sF76)
| i6 = sF76
| i8 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i7 = sF76
| i0 = sF76
| i2 = sF76
| i3 = sF76 ) ).
cnf(u231,axiom,
( select(sF52,X0) = select(sF54,X0)
| i1 = X0 ) ).
cnf(u640,axiom,
( sF50 = store(sF48,i4,sF12)
| i8 = i9
| i7 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u218,axiom,
( select(sF26,X0) = select(sF28,X0)
| i1 = X0 ) ).
cnf(u187,axiom,
sF45 = select(sF46,i5) ).
cnf(u301,axiom,
( select(sF26,X0) = select(sF30,X0)
| i1 = X0
| i2 = X0 ) ).
cnf(u217,axiom,
( select(sF25,X0) = select(sF26,X0)
| i0 = X0 ) ).
cnf(u190,axiom,
sF51 = select(sF52,i9) ).
cnf(u1000,negated_conjecture,
( sF78 = select(sF75,i2)
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u220,axiom,
( select(sF30,X0) = select(sF32,X0)
| i3 = X0 ) ).
cnf(u568,axiom,
( sF16 = select(sF3,i1)
| i6 = i1
| i8 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u189,axiom,
sF49 = select(sF50,i4) ).
cnf(u380,axiom,
( sF20 = select(sF15,i5)
| i7 = i5
| i5 = i1 ) ).
cnf(u211,axiom,
( select(sF13,X0) = select(sF15,X0)
| i9 = X0 ) ).
cnf(u575,axiom,
( sF24 = select(sF11,i0)
| i4 = i0
| i9 = i0
| i7 = i0
| i1 = i0
| i5 = i0 ) ).
cnf(u176,axiom,
sF24 = select(sF25,i0) ).
cnf(u392,axiom,
( sF14 = select(sF3,i4)
| i6 = i4
| i8 = i4
| i5 = i4 ) ).
cnf(u1106,negated_conjecture,
( sF77 = select(sF26,i6)
| i6 = i2
| i6 = i3
| i6 = i0
| i0 = i2
| i2 = i3
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i1 = i0
| i8 = i0
| i7 = i0
| i5 = i0
| i4 = i0
| i9 = i0
| i7 = i1
| i4 = i1
| i5 = i1
| i8 = i7
| i7 = i6
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u214,axiom,
( select(sF19,X0) = select(sF21,X0)
| i4 = X0 ) ).
cnf(u796,axiom,
( sF12 = sF59
| i4 = i9
| i4 = i1
| i7 = i4
| i8 = i9
| i7 = i9
| i6 = i9
| i5 = i9 ) ).
cnf(u183,axiom,
sF37 = select(sF38,i5) ).
cnf(u491,axiom,
( sF61 = select(sF52,i0)
| i1 = i0
| i7 = i0
| i4 = i0
| i5 = i0 ) ).
cnf(u170,axiom,
sF12 = select(sF13,i4) ).
cnf(u11,axiom,
store(sF1,i7,sF2) = sF3 ).
cnf(u200,axiom,
sF70 = select(sF71,i0) ).
cnf(u169,axiom,
sF10 = select(sF11,i5) ).
cnf(u360,axiom,
( sF22 = select(sF26,i5)
| i5 = i0 ) ).
cnf(u225,axiom,
( select(sF40,X0) = select(sF42,X0)
| i6 = X0 ) ).
cnf(u555,axiom,
( sF66 = select(sF52,i2)
| i1 = i2
| i7 = i2
| i0 = i2
| i4 = i2
| i5 = i2 ) ).
cnf(u398,axiom,
( sF24 = sF31
| i1 = i0
| i0 = i2 ) ).
cnf(u13,axiom,
select(sF3,i8) = sF4 ).
cnf(u194,axiom,
sF59 = select(sF60,i5) ).
cnf(u163,axiom,
sF0 = select(sF1,i8) ).
cnf(u193,axiom,
sF57 = select(sF58,i4) ).
cnf(u166,axiom,
sF4 = select(sF5,i6) ).
cnf(u7,axiom,
store(a1,i8,sF0) = sF1 ).
cnf(u196,axiom,
sF61 = select(sF63,i0) ).
cnf(u139,axiom,
store(sF65,i1,sF66) = sF67 ).
cnf(u165,axiom,
sF2 = select(sF3,i7) ).
cnf(u356,axiom,
( sF72 = select(sF75,i6)
| i6 = i9 ) ).
cnf(u551,axiom,
( sF27 = select(sF15,i2)
| i7 = i2
| i1 = i2
| i0 = i2
| i4 = i2
| i5 = i2 ) ).
cnf(u958,negated_conjecture,
( sF77 = select(sF38,i3)
| i7 = sF76
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i2 = sF76
| i8 = sF76 ) ).
cnf(u121,axiom,
store(sF56,i4,sF57) = sF58 ).
cnf(u1006,negated_conjecture,
( i5 != i2
| i6 = sF76
| i5 = sF76
| i4 = sF76
| i9 = sF76
| i1 = sF76
| i0 = sF76
| i7 = sF76
| i8 = sF76
| i0 = i2
| i1 = i0
| i8 = i0
| i7 = i0
| i6 = i0
| i5 = i0
| i4 = i0
| i9 = i0 ) ).
cnf(u312,axiom,
( sF2 = select(sF40,i7)
| i8 = i7 ) ).
cnf(u159,axiom,
select(sF38,sF76) = sF77 ).
cnf(u892,axiom,
( sF67 = store(sF65,i1,sF27)
| i8 = i2
| i7 = i2
| i6 = i2
| i5 = i2
| i4 = i2
| i9 = i2
| i1 = i2
| i0 = i2 ) ).
cnf(u743,axiom,
( sF16 = sF55
| i8 = i1
| i7 = i1
| i6 = i1
| i5 = i1
| i4 = i1
| i9 = i1 ) ).
cnf(u115,axiom,
select(sF52,i1) = sF55 ).
cnf(u493,axiom,
( sF74 = select(sF63,i6)
| i6 = i2
| i6 = i1
| i6 = i3
| i6 = i0 ) ).
cnf(u597,axiom,
( sF53 = select(sF40,i7)
| i7 = i6
| i8 = i7
| i7 = i5
| i7 = i4
| i7 = i9 ) ).
cnf(u469,axiom,
( sF44 = store(sF42,i8,sF6)
| i8 = i6
| i7 = i6 ) ).
cnf(u117,axiom,
store(sF54,i7,sF55) = sF56 ).
cnf(u750,axiom,
( sF38 = store(sF36,i5,sF14)
| i7 = i9
| i9 = i1
| i9 = i0
| i4 = i9
| i5 = i9
| i9 = i2
| i9 = i3 ) ).
cnf(u308,axiom,
( sF35 = select(sF38,i9)
| i5 = i9 ) ).
cnf(u463,axiom,
( sF77 = select(sF30,sF76)
| i3 = sF76
| i0 = sF76
| i9 = sF76
| i5 = sF76 ) ).
cnf(u191,axiom,
sF53 = select(sF54,i1) ).
cnf(u111,axiom,
select(sF52,i7) = sF53 ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV536-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n015.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 11:39:17 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.22/0.31 Running first-order model finding
% 0.22/0.31 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
% 31.75/5.94 % (2567571)Will run a generic schedule for satisfiability detection.
% 31.75/5.94 % (2567579)dis+10_1_sil=32000:sp=arity:random_seed=3366203454:i=103:fgj=on_2986 on theBenchmark for (2986ds/103Mi)
% 31.75/5.94 % (2567577)% WARNING: option uhcvi not known.
% 31.75/5.94 % (2567580)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=514995322:i=116_2986 on theBenchmark for (2986ds/116Mi)
% 31.75/5.94 % (2567581)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3999475109:i=131_2986 on theBenchmark for (2986ds/131Mi)
% 31.75/5.94 % (2567576)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2429907880_2986 on theBenchmark for (2986ds/0Mi)
% 31.75/5.94 % (2567578)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=219841414:i=88024:add=on:rawr=on_2986 on theBenchmark for (2986ds/88024Mi)
% 31.75/5.94 % (2567577)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4012811794:i=135531:add=off:rawr=on_2986 on theBenchmark for (2986ds/135531Mi)
% 31.75/5.94 % (2567582)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1121821491:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2986 on theBenchmark for (2986ds/159Mi)
% 31.75/5.94 % TRYING [1]
% 31.75/5.94 % TRYING [2]
% 31.75/5.94 % TRYING [3]
% 31.75/5.94 % TRYING [4]
% 31.75/5.94 % TRYING [5]
% 31.75/5.94 % (2567580)Instruction limit reached!
% 31.75/5.94 % (2567580)------------------------------
% 31.75/5.94 % (2567580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.75/5.94 % (2567580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.75/5.94 % (2567580)CaDiCaL version: 2.1.3
% 31.75/5.94 % (2567580)Termination reason: Instruction limit
% 31.75/5.94 % (2567580)Termination phase: Saturation
% 31.75/5.94 % (2567580)Time elapsed: 0.108 s
% 31.75/5.94 % (2567580)Peak memory usage: 42 MB
% 31.75/5.94 % (2567580)Instructions burned: 116 (million)
% 31.75/5.94 % (2567581)Instruction limit reached!
% 31.75/5.94 % (2567581)------------------------------
% 31.75/5.94 % (2567581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.75/5.94 % (2567581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.75/5.94 % (2567581)CaDiCaL version: 2.1.3
% 31.75/5.94 % (2567581)Termination reason: Instruction limit
% 31.75/5.94 % (2567581)Termination phase: Saturation
% 31.75/5.94 % (2567581)Time elapsed: 0.126 s
% 31.75/5.94 % (2567581)Peak memory usage: 43 MB
% 31.75/5.94 % (2567581)Instructions burned: 131 (million)
% 31.75/5.94 % (2567590)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=194878913:i=714:nm=2_2985 on theBenchmark for (2985ds/714Mi)
% 31.75/5.94 % TRYING [6]
% 31.75/5.94 % (2567591)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2867612798:i=131:bd=preordered:fsd=on_2985 on theBenchmark for (2985ds/131Mi)
% 31.75/5.94 % (2567579)Instruction limit reached!
% 31.75/5.94 % (2567579)------------------------------
% 31.75/5.94 % (2567579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.75/5.94 % (2567579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.75/5.94 % (2567579)CaDiCaL version: 2.1.3
% 31.75/5.94 % (2567579)Termination reason: Instruction limit
% 31.75/5.94 % (2567579)Termination phase: Saturation
% 31.75/5.94 % (2567579)Time elapsed: 0.175 s
% 31.75/5.94 % (2567579)Peak memory usage: 152 MB
% 31.75/5.94 % (2567579)Instructions burned: 105 (million)
% 31.75/5.94 % (2567594)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=1344873002:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2984 on theBenchmark for (2984ds/684Mi)
% 31.75/5.94 % (2567582)Instruction limit reached!
% 31.75/5.94 % (2567582)------------------------------
% 31.75/5.94 % (2567582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.75/5.94 % (2567582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.75/5.94 % (2567582)CaDiCaL version: 2.1.3
% 31.75/5.94 % (2567582)Termination reason: Instruction limit
% 31.75/5.94 % (2567582)Termination phase: Saturation
% 31.75/5.94 % (2567582)Time elapsed: 0.193 s
% 31.75/5.94 % (2567582)Peak memory usage: 64 MB
% 31.75/5.94 % (2567582)Instructions burned: 161 (million)
% 31.75/5.94 % (2567591)Instruction limit reached!
% 31.75/5.94 % (2567591)------------------------------
% 31.75/5.94 % (2567591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.75/5.94 % (2567591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.75/5.94 % (2567591)CaDiCaL version: 2.1.3
% 31.75/5.94 % (2567591)Termination reason: Instruction limit
% 40.82/7.26 % (2567591)Termination phase: Saturation
% 40.82/7.26 % (2567591)Time elapsed: 0.062 s
% 40.82/7.26 % (2567591)Peak memory usage: 23 MB
% 40.82/7.26 % (2567591)Instructions burned: 133 (million)
% 40.82/7.26 % (2567596)ott-21_1_sil=16000:fs=off:random_seed=1060193077:i=180:av=off:fsr=off_2984 on theBenchmark for (2984ds/180Mi)
% 40.82/7.26 % (2567597)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3349903978:i=477:bd=all_2984 on theBenchmark for (2984ds/477Mi)
% 40.82/7.26 % TRYING [7]
% 40.82/7.26 % (2567594)Instruction limit reached!
% 40.82/7.26 % (2567594)------------------------------
% 40.82/7.26 % (2567594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567594)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567594)Termination reason: Instruction limit
% 40.82/7.26 % (2567594)Termination phase: Property scanning
% 40.82/7.26 % (2567594)Time elapsed: 0.125 s
% 40.82/7.26 % (2567594)Peak memory usage: 9 MB
% 40.82/7.26 % (2567594)Instructions burned: 690 (million)
% 40.82/7.26 % (2567596)Instruction limit reached!
% 40.82/7.26 % (2567596)------------------------------
% 40.82/7.26 % (2567596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567596)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567596)Termination reason: Instruction limit
% 40.82/7.26 % (2567596)Termination phase: Saturation
% 40.82/7.26 % (2567596)Time elapsed: 0.083 s
% 40.82/7.26 % (2567596)Peak memory usage: 10 MB
% 40.82/7.26 % (2567596)Instructions burned: 181 (million)
% 40.82/7.26 % (2567600)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=99329763:fmbsr=1.3:i=865:ins=25_2983 on theBenchmark for (2983ds/865Mi)
% 40.82/7.26 % (2567601)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1230236187:i=1179_2983 on theBenchmark for (2983ds/1179Mi)
% 40.82/7.26 % (2567590)Instruction limit reached!
% 40.82/7.26 % (2567590)------------------------------
% 40.82/7.26 % (2567590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567590)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567590)Termination reason: Instruction limit
% 40.82/7.26 % (2567590)Termination phase: Finite model building preprocessing
% 40.82/7.26 % (2567590)Time elapsed: 0.241 s
% 40.82/7.26 % (2567590)Peak memory usage: 9 MB
% 40.82/7.26 % (2567590)Instructions burned: 716 (million)
% 40.82/7.26 % (2567604)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3682045910:i=889:ins=1_2982 on theBenchmark for (2982ds/889Mi)
% 40.82/7.26 % (2567600)Instruction limit reached!
% 40.82/7.26 % (2567600)------------------------------
% 40.82/7.26 % (2567600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567600)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567600)Termination reason: Instruction limit
% 40.82/7.26 % (2567600)Termination phase: Property scanning
% 40.82/7.26 % (2567600)Time elapsed: 0.159 s
% 40.82/7.26 % (2567600)Peak memory usage: 9 MB
% 40.82/7.26 % (2567600)Instructions burned: 876 (million)
% 40.82/7.26 % (2567606)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=3568976730:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2981 on theBenchmark for (2981ds/692Mi)
% 40.82/7.26 % (2567606)Instruction limit reached!
% 40.82/7.26 % (2567606)------------------------------
% 40.82/7.26 % (2567606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567606)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567606)Termination reason: Instruction limit
% 40.82/7.26 % (2567606)Termination phase: Property scanning
% 40.82/7.26 % (2567606)Time elapsed: 0.125 s
% 40.82/7.26 % (2567606)Peak memory usage: 9 MB
% 40.82/7.26 % (2567606)Instructions burned: 694 (million)
% 40.82/7.26 % TRYING [8]
% 40.82/7.26 % (2567608)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1726932060:i=879:kws=inv_precedence:fsr=off_2980 on theBenchmark for (2980ds/879Mi)
% 40.82/7.26 % (2567604)Instruction limit reached!
% 40.82/7.26 % (2567604)------------------------------
% 40.82/7.26 % (2567604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567604)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567604)Termination reason: Instruction limit
% 40.82/7.26 % (2567604)Termination phase: Property scanning
% 40.82/7.26 % (2567604)Time elapsed: 0.306 s
% 40.82/7.26 % (2567604)Peak memory usage: 9 MB
% 40.82/7.26 % (2567604)Instructions burned: 891 (million)
% 40.82/7.26 % (2567610)fmb+10_1_sil=64000:random_seed=664276962:i=22061:nm=2:gsp=on_2979 on theBenchmark for (2979ds/22061Mi)
% 40.82/7.26 % TRYING [1]
% 40.82/7.26 % TRYING [2]
% 40.82/7.26 % TRYING [3]
% 40.82/7.26 % TRYING [4]
% 40.82/7.26 % (2567601)Instruction limit reached!
% 40.82/7.26 % (2567601)------------------------------
% 40.82/7.26 % (2567601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567601)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567601)Termination reason: Instruction limit
% 40.82/7.26 % (2567601)Termination phase: Saturation
% 40.82/7.26 % (2567601)Time elapsed: 0.511 s
% 40.82/7.26 % (2567601)Peak memory usage: 25 MB
% 40.82/7.26 % (2567601)Instructions burned: 1180 (million)
% 40.82/7.26 % (2567612)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3700387219:i=9515:nm=5_2978 on theBenchmark for (2978ds/9515Mi)
% 40.82/7.26 % TRYING [5]
% 40.82/7.26 % TRYING [20]
% 40.82/7.26 % (2567608)Instruction limit reached!
% 40.82/7.26 % (2567608)------------------------------
% 40.82/7.26 % (2567608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567608)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567608)Termination reason: Instruction limit
% 40.82/7.26 % (2567608)Termination phase: Saturation
% 40.82/7.26 % (2567608)Time elapsed: 0.343 s
% 40.82/7.26 % (2567608)Peak memory usage: 88 MB
% 40.82/7.26 % (2567608)Instructions burned: 882 (million)
% 40.82/7.26 % (2567614)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2323608944:fmbsr=1.7:i=920_2976 on theBenchmark for (2976ds/920Mi)
% 40.82/7.26 % TRYING [8]
% 40.82/7.26 % TRYING [6]
% 40.82/7.26 % (2567614)Instruction limit reached!
% 40.82/7.26 % (2567614)------------------------------
% 40.82/7.26 % (2567614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567614)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567614)Termination reason: Instruction limit
% 40.82/7.26 % (2567614)Termination phase: Finite model building SAT solving
% 40.82/7.26 % (2567614)Time elapsed: 0.184 s
% 40.82/7.26 % (2567614)Peak memory usage: 41 MB
% 40.82/7.26 % (2567614)Instructions burned: 920 (million)
% 40.82/7.26 % (2567616)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=414882003:i=5131_2974 on theBenchmark for (2974ds/5131Mi)
% 40.82/7.26 % TRYING [9]
% 40.82/7.26 % TRYING [7]
% 40.82/7.26 % (2567597)Instruction limit reached!
% 40.82/7.26 % (2567597)------------------------------
% 40.82/7.26 % (2567597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567597)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567597)Termination reason: Instruction limit
% 40.82/7.26 % (2567597)Termination phase: Saturation
% 40.82/7.26 % (2567597)Time elapsed: 1.336 s
% 40.82/7.26 % (2567597)Peak memory usage: 153 MB
% 40.82/7.26 % (2567597)Instructions burned: 479 (million)
% 40.82/7.26 % (2567618)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2568802060:i=1472:ins=7:fdi=8:gsp=on_2970 on theBenchmark for (2970ds/1472Mi)
% 40.82/7.26 % (2567618)Instruction limit reached!
% 40.82/7.26 % (2567618)------------------------------
% 40.82/7.26 % (2567618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567618)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567618)Termination reason: Instruction limit
% 40.82/7.26 % (2567618)Termination phase: Property scanning
% 40.82/7.26 % (2567618)Time elapsed: 0.507 s
% 40.82/7.26 % (2567618)Peak memory usage: 10 MB
% 40.82/7.26 % (2567618)Instructions burned: 1473 (million)
% 40.82/7.26 % (2567620)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4232651323:i=6324_2965 on theBenchmark for (2965ds/6324Mi)
% 40.82/7.26 % TRYING [8]
% 40.82/7.26 % TRYING [77]
% 40.82/7.26 % TRYING [9]
% 40.82/7.26 % (2567620)Instruction limit reached!
% 40.82/7.26 % (2567620)------------------------------
% 40.82/7.26 % (2567620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567620)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567620)Termination reason: Instruction limit
% 40.82/7.26 % (2567620)Termination phase: Finite model building constraint generation
% 40.82/7.26 % (2567620)Time elapsed: 2.163 s
% 40.82/7.26 % (2567620)Peak memory usage: 374 MB
% 40.82/7.26 % (2567620)Instructions burned: 6325 (million)
% 40.82/7.26 % (2567622)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=638691742:fmbsr=2.30978:i=2174_2943 on theBenchmark for (2943ds/2174Mi)
% 40.82/7.26 % (2567612)Instruction limit reached!
% 40.82/7.26 % (2567612)------------------------------
% 40.82/7.26 % (2567612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567612)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567612)Termination reason: Instruction limit
% 40.82/7.26 % (2567612)Termination phase: Finite model building constraint generation
% 40.82/7.26 % (2567612)Time elapsed: 3.907 s
% 40.82/7.26 % (2567612)Peak memory usage: 642 MB
% 40.82/7.26 % (2567612)Instructions burned: 9515 (million)
% 40.82/7.26 % (2567624)ott-2_1_sil=16000:newcnf=on:random_seed=679739578:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2938 on theBenchmark for (2938ds/869Mi)
% 40.82/7.26 % TRYING [16]
% 40.82/7.26 % (2567622)Instruction limit reached!
% 40.82/7.26 % (2567622)------------------------------
% 40.82/7.26 % (2567622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567622)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567622)Termination reason: Instruction limit
% 40.82/7.26 % (2567622)Termination phase: Finite model building constraint generation
% 40.82/7.26 % (2567622)Time elapsed: 0.773 s
% 40.82/7.26 % (2567622)Peak memory usage: 17 MB
% 40.82/7.26 % (2567622)Instructions burned: 2175 (million)
% 40.82/7.26 % (2567626)ott+10_1_sil=32000:tgt=ground:random_seed=2762732639:i=5114:av=off_2935 on theBenchmark for (2935ds/5114Mi)
% 40.82/7.26 % (2567624)Instruction limit reached!
% 40.82/7.26 % (2567624)------------------------------
% 40.82/7.26 % (2567624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.26 % (2567624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.26 % (2567624)CaDiCaL version: 2.1.3
% 40.82/7.26 % (2567624)Termination reason: Instruction limit
% 40.82/7.26 % (2567624)Termination phase: Saturation
% 40.82/7.26 % (2567624)Time elapsed: 0.500 s
% 40.82/7.26 % (2567624)Peak memory usage: 71 MB
% 40.82/7.26 % (2567624)Instructions burned: 871 (million)
% 40.82/7.26 % (2567628)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1381957737:i=54282_2932 on theBenchmark for (2932ds/54282Mi)
% 40.82/7.26 % TRYING [1]
% 40.82/7.26 % TRYING [2]
% 40.82/7.26 % TRYING [3]
% 40.82/7.26 % TRYING [4]
% 40.82/7.26 % TRYING [5]
% 40.82/7.26 % TRYING [6]
% 40.82/7.26 % (2567626) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2567571-2567626"...
% 40.82/7.26 % (2567626)...printing done.
% 40.82/7.26 % SZS status Satisfiable for theBenchmark
% 40.82/7.26 % SZS output start Saturation.
% See solution above
% 40.82/7.27 % SZS output start Definitions and Model Updates.
% 40.82/7.27 % SZS output end Definitions and Model Updates.
% 40.82/7.27 % (2567626)------------------------------
% 40.82/7.27 % (2567626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.82/7.27 % (2567626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.82/7.27 % (2567626)CaDiCaL version: 2.1.3
% 40.82/7.27 % (2567626)Termination reason: Satisfiable
% 40.82/7.27 % (2567626)Time elapsed: 0.416 s
% 40.82/7.27 % (2567626)Peak memory usage: 23 MB
% 40.82/7.27 % (2567626)Instructions burned: 1034 (million)
% 40.82/7.27 % (2567571)Success in time 6.952 s
% 40.82/7.27 % Vampire exiting
%------------------------------------------------------------------------------