efsmt_coverts> run -ptaDir imitator_examples/Imitator/FMS1 -imFile imitator_examples/interactionModels/FMS1.im 
[warn] Scala version was updated by one of library dependencies:
[warn]  * org.scala-lang:scala-library:(2.10.4, 2.10.0, 2.9.1) -> 2.10.6
[warn] To force scalaVersion, add the following:
[warn]  ivyScala := ivyScala.value map { _.copy(overrideScalaVersion = true) }
[warn] Run 'evicted' to see detailed eviction warnings

Multiple main classes detected, select one to run:

 [1] org.TCH2Z3
 [2] org.GenPhilos
 [3] org.HA2Z3
 [4] org.Thermostat2Z3
 [5] org.RunEFTests
 [6] org.TestAssemblyZ3
 [7] org.TestPPL
 [8] org.PTA2EF
 [9] org.GenUppaal
 [10] org.PTAG2EF
 [11] org.TestAssembly

Enter number: 10

[info] Running org.PTAG2EF -ptaDir imitator_examples/Imitator/FMS1 -imFile imitator_examples/interactionModels/FMS1.im
[info] Debug: java.library.path= /usr/java/packages/lib/amd64:/usr/lib/x86_64-linux-gnu/jni:/lib/x86_64-linux-gnu:/usr/lib/x86_64-linux-gnu:/usr/lib/jni:/lib:/usr/lib
[info] 1.1
[info] im = Set(Set(Mill_O_B3_M, Robot1_O_B3_M), Set(Conveyor_B1_in, Spec1_B1_in), Set(Mill_O_B3_R2, Robot2_O_B3_R2), Set(Assembly_product), Set(Mill_B3_out_M), Set(Assembly_O_B5_A, Robot2_O_B5_A), Set(Mill_I_B3_R1, Robot1_I_B3_R1), Set(Robot1_B3_in_R1), Set(Robot1_B1_out, Spec1_B1_out), Set(Assembly_B5_out_A), Set(Robot2_B3_out_R2), Set(Conveyor_O_B1_R1, Robot1_O_B1_R1), Set(Mill_I_B3_M, Robot2_I_B3_M), Set(Robot2_B5_in_R2), Set(Assembly_I_B5_R2, Robot2_I_B5_R2), Set(Conveyor_I_B1_C1, Robot1_I_B1_C1), Set(Mill_B3_in_M))
[info] clks: List(clk_I_B3_R1,  clk_B3_in_M,  clk_B3_out_M,  clk_O_B3_M,  clk_I_B3_M,  clk_O_B3_R2 )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/mill.imi ta = (Mill,M0,Set(M2, M4, M0, M1, M3),Set((M1,Mill_B3_out_M,true,Set(),Set((C,0)),Set(),M2), (M0,Mill_I_B3_R1,true,Set(),Set((A,0)),Set(),M1), (M2,Mill_O_B3_M,true,Set(),Set((D,0)),Set(),M0), (M4,Mill_O_B3_R2,true,Set(),Set((F,0)),Set(),M0), (M0,Mill_B3_in_M,true,Set(),Set((B,0)),Set(),M3), (M3,Mill_I_B3_M,true,Set(),Set((E,0)),Set(),M4)),Map(D -> clk_O_B3_M, A -> clk_I_B3_R1, E -> clk_I_B3_M, A -> p_B3_out_M, B -> clk_B3_in_M, C -> clk_B3_out_M, F -> clk_O_B3_R2),Map(M2 -> true, M4 -> true, M0 -> true, M1 -> true, M3 -> true),Map())
[info] ptaH: (Millh,M0,Set(M2, M4, M0, M1, M3),Set((M2,Mill_O_B3_M,true,Set(),Set((D,0), (K,0)),Set(),M0), (M0,Mill_I_B3_R1,true,Set(),Set((A,0), (M,0)),Set(),M1), (M0,Mill_B3_in_M,true,Set(),Set((B,0), (H,0)),Set(),M3), (M1,Mill_B3_out_M,true,Set(),Set((C,0), (I,0)),Set(),M2), (M3,Mill_I_B3_M,true,Set(),Set((E,0), (L,0)),Set(),M4), (M4,Mill_O_B3_R2,true,Set(),Set((F,0), (J,0)),Set(),M0)),Map(K -> hMill_O_B3_M, J -> hMill_O_B3_R2, D -> clk_O_B3_M, A -> clk_I_B3_R1, H -> hMill_B3_in_M, E -> clk_I_B3_M, L -> hMill_I_B3_M, I -> hMill_B3_out_M, M -> hMill_I_B3_R1, A -> p_B3_out_M, B -> clk_B3_in_M, C -> clk_B3_out_M, F -> clk_O_B3_R2),Map(M2 -> true, M4 -> true, M0 -> true, M1 -> true, M3 -> true),Map(),Set(p_B3_out_M))
[info] locsI = Map(M2 -> 0, M4 -> 1, M0 -> 2, M1 -> 3, M3 -> 4)
[info] iniL = M0
[info] clks: List(clk_I_B1_C1,  clk_B1_out,  clk_O_B1_R1,  clk_B3_in_R1,  clk_I_B3_R1,  clk_O_B3_M)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/robot1.imi ta = (Robot1,R1_0,Set(R1_4, R1_1, R1_5, R1_2, R1_3, R1_0),Set((R1_5,Robot1_O_B3_M,true,Set(),Set((F,0)),Set(),R1_0), (R1_3,Robot1_B3_in_R1,true,Set(),Set((D,0)),Set(),R1_4), (R1_0,Robot1_I_B1_C1,true,Set(),Set((A,0)),Set(),R1_1), (R1_1,Robot1_B1_out,-A >= -1,Set(),Set((B,0)),Set(),R1_2), (R1_4,Robot1_I_B3_R1,true,Set(),Set((E,0)),Set(),R1_5), (R1_2,Robot1_O_B1_R1,true,Set(),Set((C,0)),Set(),R1_3)),Map(A -> clk_I_B1_C1, B -> clk_B1_out, C -> clk_O_B1_R1, E -> clk_I_B3_R1, F -> clk_O_B3_M, D -> clk_B3_in_R1),Map(R1_4 -> true, R1_1 -> true, R1_5 -> true, R1_2 -> true, R1_3 -> true, R1_0 -> true),Map())
[info] ptaH: (Robot1h,R1_0,Set(R1_4, R1_1, R1_5, R1_2, R1_3, R1_0),Set((R1_1,Robot1_B1_out,-A >= -1,Set(),Set((B,0), (J,0)),Set(),R1_2), (R1_3,Robot1_B3_in_R1,true,Set(),Set((D,0), (L,0)),Set(),R1_4), (R1_0,Robot1_I_B1_C1,true,Set(),Set((A,0), (G,0)),Set(),R1_1), (R1_2,Robot1_O_B1_R1,true,Set(),Set((C,0), (H,0)),Set(),R1_3), (R1_4,Robot1_I_B3_R1,true,Set(),Set((E,0), (I,0)),Set(),R1_5), (R1_5,Robot1_O_B3_M,true,Set(),Set((F,0), (K,0)),Set(),R1_0)),Map(G -> hRobot1_I_B1_C1, L -> hRobot1_B3_in_R1, A -> clk_I_B1_C1, K -> hRobot1_O_B3_M, I -> hRobot1_I_B3_R1, J -> hRobot1_B1_out, H -> hRobot1_O_B1_R1, B -> clk_B1_out, C -> clk_O_B1_R1, E -> clk_I_B3_R1, F -> clk_O_B3_M, D -> clk_B3_in_R1),Map(R1_4 -> true, R1_1 -> true, R1_5 -> true, R1_2 -> true, R1_3 -> true, R1_0 -> true),Map(),Set())
[info] locsI = Map(R1_4 -> 0, R1_1 -> 1, R1_5 -> 2, R1_2 -> 3, R1_3 -> 4, R1_0 -> 5)
[info] iniL = R1_0
[info] clks: List(clk_I_B3_M,  clk_B3_out_R2,  clk_O_B3_R2,  clk_B5_in_R2,  clk_I_B5_R2,  clk_O_B5_A )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/robot2.imi ta = (Robot2,R2_0,Set(R2_2, R2_5, R2_1, R2_4, R2_0, R2_3),Set((R2_4,Robot2_I_B5_R2,true,Set(),Set((E,0)),Set(),R2_5), (R2_0,Robot2_I_B3_M,true,Set(),Set((A,0)),Set(),R2_1), (R2_2,Robot2_O_B3_R2,true,Set(),Set((C,0)),Set(),R2_3), (R2_3,Robot2_B5_in_R2,true,Set(),Set((D,0)),Set(),R2_4), (R2_5,Robot2_O_B5_A,true,Set(),Set((F,0)),Set(),R2_0), (R2_1,Robot2_B3_out_R2,true,Set(),Set((B,0)),Set(),R2_2)),Map(C -> clk_O_B3_R2, E -> clk_I_B5_R2, F -> clk_O_B5_A, A -> clk_I_B3_M, D -> clk_B5_in_R2, B -> clk_B3_out_R2),Map(R2_2 -> true, R2_5 -> true, R2_1 -> true, R2_4 -> true, R2_0 -> true, R2_3 -> true),Map())
[info] ptaH: (Robot2h,R2_0,Set(R2_2, R2_5, R2_1, R2_4, R2_0, R2_3),Set((R2_2,Robot2_O_B3_R2,true,Set(),Set((C,0), (J,0)),Set(),R2_3), (R2_0,Robot2_I_B3_M,true,Set(),Set((A,0), (K,0)),Set(),R2_1), (R2_1,Robot2_B3_out_R2,true,Set(),Set((B,0), (L,0)),Set(),R2_2), (R2_5,Robot2_O_B5_A,true,Set(),Set((F,0), (I,0)),Set(),R2_0), (R2_4,Robot2_I_B5_R2,true,Set(),Set((E,0), (H,0)),Set(),R2_5), (R2_3,Robot2_B5_in_R2,true,Set(),Set((D,0), (G,0)),Set(),R2_4)),Map(G -> hRobot2_B5_in_R2, K -> hRobot2_I_B3_M, J -> hRobot2_O_B3_R2, C -> clk_O_B3_R2, E -> clk_I_B5_R2, F -> clk_O_B5_A, I -> hRobot2_O_B5_A, A -> clk_I_B3_M, L -> hRobot2_B3_out_R2, H -> hRobot2_I_B5_R2, D -> clk_B5_in_R2, B -> clk_B3_out_R2),Map(R2_2 -> true, R2_5 -> true, R2_1 -> true, R2_4 -> true, R2_0 -> true, R2_3 -> true),Map(),Set())
[info] locsI = Map(R2_2 -> 0, R2_5 -> 1, R2_1 -> 2, R2_4 -> 3, R2_0 -> 4, R2_3 -> 5)
[info] iniL = R2_0
[info] clks: List(clk_B1_in,  clk_I_B1_C1,  clk_B1_R1 )
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/conveyor.imi ta = (Conveyor1,C0,Set(C0, C1, C2),Set((C0,Conveyor_B1_in,true,Set(),Set((A,0)),Set(),C1), (C1,Conveyor_I_B1_C1,true,Set(),Set((B,0)),Set(),C2), (C2,Conveyor_O_B1_R1,true,Set(),Set((C,0)),Set(),C0)),Map(A -> clk_B1_in, B -> clk_I_B1_C1, C -> clk_B1_R1, A -> p_I_B1_C1),Map(C0 -> true, C1 -> true, C2 -> true),Map())
[info] ptaH: (Conveyor1h,C0,Set(C0, C1, C2),Set((C0,Conveyor_B1_in,true,Set(),Set((A,0), (E,0)),Set(),C1), (C1,Conveyor_I_B1_C1,true,Set(),Set((B,0), (F,0)),Set(),C2), (C2,Conveyor_O_B1_R1,true,Set(),Set((C,0), (G,0)),Set(),C0)),Map(C -> clk_B1_R1, G -> hConveyor_O_B1_R1, E -> hConveyor_B1_in, A -> p_I_B1_C1, F -> hConveyor_I_B1_C1, B -> clk_I_B1_C1, A -> clk_B1_in),Map(C0 -> true, C1 -> true, C2 -> true),Map(),Set(p_I_B1_C1))
[info] locsI = Map(C0 -> 0, C1 -> 1, C2 -> 2)
[info] iniL = C0
[info] clks: List(clk_I_B5_R2,  clk_B5_out_A,  clk_O_B5_A,  clk_product)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/assembly.imi ta = (AssemblyStation,A0,Set(A0, A1, A2, A3),Set((A0,Assembly_I_B5_R2,true,Set(),Set((A,0)),Set(),A1), (A1,Assembly_B5_out_A,true,Set(),Set((B,0)),Set(),A2), (A2,Assembly_O_B5_A,true,Set(),Set((C,0)),Set(),A3), (A3,Assembly_product,true,Set(),Set((D,0)),Set(),A0)),Map(A -> clk_I_B5_R2, B -> clk_B5_out_A, C -> clk_O_B5_A, D -> clk_product),Map(A0 -> true, A1 -> true, A2 -> true, A3 -> true),Map())
[info] ptaH: (AssemblyStationh,A0,Set(A0, A1, A2, A3),Set((A0,Assembly_I_B5_R2,true,Set(),Set((A,0), (E,0)),Set(),A1), (A1,Assembly_B5_out_A,true,Set(),Set((B,0), (F,0)),Set(),A2), (A2,Assembly_O_B5_A,true,Set(),Set((C,0), (G,0)),Set(),A3), (A3,Assembly_product,true,Set(),Set((D,0), (H,0)),Set(),A0)),Map(H -> hAssembly_product, E -> hAssembly_I_B5_R2, A -> clk_I_B5_R2, D -> clk_product, F -> hAssembly_B5_out_A, B -> clk_B5_out_A, C -> clk_O_B5_A, G -> hAssembly_O_B5_A),Map(A0 -> true, A1 -> true, A2 -> true, A3 -> true),Map(),Set())
[info] locsI = Map(A0 -> 0, A1 -> 1, A2 -> 2, A3 -> 3)
[info] iniL = A0
[info] clks: List(clk_B1_in,  clk_B1_out)
[info] ptag2ef for file /home/etienne/git/efsmt_coverts/imitator_examples/Imitator/FMS1/spec1.imi ta = (Spec1,S0,Set(S0, S1, ERROR),Set((S1,Spec1_B1_out,A > 3,Set(),Set((B,0)),Set(),ERROR), (S0,Spec1_B1_out,true,Set(),Set((B,0)),Set(),ERROR), (S1,Spec1_B1_out,-A >= -3,Set(),Set((B,0)),Set(),S0), (S0,Spec1_B1_in,true,Set(),Set((A,0)),Set(),S1), (ERROR,Spec1_B1_out,A > 3,Set(),Set((B,0)),Set(),ERROR)),Map(A -> clk_B1_in, B -> clk_B1_out),Map(S0 -> true, S1 -> true, ERROR -> true),Map())
[info] ptaH: (Spec1h,S0,Set(S0, S1, ERROR),Set((S0,Spec1_B1_in,true,Set(),Set((A,0), (D,0)),Set(),S1), (ERROR,Spec1_B1_out,A > 3,Set(),Set((B,0), (C,0)),Set(),ERROR), (S1,Spec1_B1_out,-A >= -3,Set(),Set((B,0), (C,0)),Set(),S0), (S1,Spec1_B1_out,A > 3,Set(),Set((B,0), (C,0)),Set(),ERROR), (S0,Spec1_B1_out,true,Set(),Set((B,0), (C,0)),Set(),ERROR)),Map(A -> clk_B1_in, B -> clk_B1_out, C -> hSpec1_B1_out, D -> hSpec1_B1_in),Map(S0 -> true, S1 -> true, ERROR -> true),Map(),Set())
[info] locsI = Map(S0 -> 0, S1 -> 1, ERROR -> 2)
[info] iniL = S0
[info] outz3=
[info] ciMillhh = Or(And(M0,  clk_O_B3_M >= 0,  clk_B3_in_M == clk_O_B3_M,  clk_I_B3_M == clk_O_B3_M,  clk_B3_out_M == clk_O_B3_M,  hMill_B3_in_M == clk_O_B3_M,  clk_O_B3_R2 == clk_O_B3_M,  hMill_I_B3_R1 == clk_O_B3_M,  hMill_O_B3_R2 == clk_O_B3_M,  hMill_I_B3_M == clk_O_B3_M,  clk_I_B3_R1 == clk_O_B3_M,  hMill_O_B3_M == clk_O_B3_M,  hMill_B3_out_M == clk_O_B3_M), And(M3,  clk_I_B3_M >= hMill_B3_in_M,  hMill_B3_in_M >= 0,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == clk_O_B3_M,  clk_I_B3_M == hMill_B3_out_M,  clk_I_B3_M == hMill_O_B3_M,  clk_I_B3_M == clk_I_B3_R1,  clk_I_B3_M == hMill_I_B3_M,  clk_I_B3_M == hMill_O_B3_R2,  clk_I_B3_M == hMill_I_B3_R1,  clk_I_B3_M == clk_O_B3_R2,  clk_I_B3_M == clk_B3_out_M), And(M1,  clk_B3_in_M >= clk_I_B3_R1,  clk_I_B3_R1 >= 0,  clk_B3_in_M == clk_O_B3_M,  clk_B3_in_M == hMill_B3_out_M,  clk_B3_in_M == hMill_O_B3_M,  clk_B3_in_M == hMill_I_B3_M,  clk_B3_in_M == hMill_O_B3_R2,  clk_B3_in_M == clk_O_B3_R2,  clk_B3_in_M == hMill_B3_in_M,  clk_B3_in_M == clk_B3_out_M,  clk_B3_in_M == clk_I_B3_M,  hMill_I_B3_R1 == clk_I_B3_R1), And(M4,  clk_B3_in_M >= hMill_I_B3_M,  hMill_I_B3_M >= 0,  clk_B3_out_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == clk_O_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_B3_out_M == hMill_O_B3_M,  clk_B3_out_M == clk_I_B3_R1,  clk_B3_out_M == hMill_O_B3_R2,  clk_B3_out_M == hMill_I_B3_R1,  clk_B3_out_M == clk_O_B3_R2), And(M2,  clk_B3_in_M >= hMill_I_B3_R1,  hMill_I_B3_R1 >= hMill_B3_out_M,  hMill_B3_out_M >= 0,  clk_B3_in_M == clk_O_B3_M,  clk_B3_in_M == hMill_O_B3_M,  clk_B3_in_M == hMill_I_B3_M,  clk_B3_in_M == hMill_O_B3_R2,  clk_B3_in_M == clk_O_B3_R2,  clk_B3_in_M == hMill_B3_in_M,  clk_B3_in_M == clk_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  hMill_I_B3_R1 == clk_I_B3_R1), And(M0,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= hMill_O_B3_R2,  hMill_O_B3_R2 >= 0,  clk_B3_out_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == clk_O_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_B3_out_M == hMill_O_B3_M,  clk_B3_out_M == clk_I_B3_R1,  clk_B3_out_M == hMill_I_B3_R1,  clk_O_B3_R2 == hMill_O_B3_R2), And(M0,  clk_B3_in_M >= hMill_I_B3_R1,  clk_B3_out_M >= clk_O_B3_M,  clk_O_B3_M >= 0,  hMill_I_B3_R1 >= clk_B3_out_M,  clk_B3_in_M == hMill_I_B3_M,  clk_B3_in_M == hMill_O_B3_R2,  clk_B3_in_M == clk_O_B3_R2,  clk_B3_in_M == hMill_B3_in_M,  clk_B3_in_M == clk_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M3,  clk_I_B3_M >= clk_O_B3_R2,  hMill_B3_in_M >= 0,  clk_O_B3_R2 >= hMill_B3_in_M,  clk_B3_out_M >= clk_I_B3_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == clk_O_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_B3_out_M == hMill_O_B3_M,  clk_B3_out_M == clk_I_B3_R1,  clk_B3_out_M == hMill_I_B3_R1,  clk_O_B3_R2 == hMill_O_B3_R2), And(M1,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_O_B3_R2 >= clk_I_B3_R1,  clk_I_B3_R1 >= 0,  clk_B3_out_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == clk_O_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_B3_out_M == hMill_O_B3_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1), And(M3,  clk_I_B3_M >= hMill_I_B3_R1,  clk_B3_out_M >= hMill_O_B3_M,  hMill_B3_in_M >= 0,  hMill_O_B3_M >= hMill_B3_in_M,  hMill_I_B3_R1 >= clk_B3_out_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_I_B3_M == hMill_O_B3_R2,  clk_I_B3_M == clk_O_B3_R2,  clk_B3_out_M == hMill_B3_out_M,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M1,  clk_B3_in_M >= clk_B3_out_M,  clk_B3_out_M >= hMill_O_B3_M,  clk_I_B3_R1 >= 0,  hMill_O_B3_M >= clk_I_B3_R1,  clk_B3_in_M == hMill_I_B3_M,  clk_B3_in_M == hMill_O_B3_R2,  clk_B3_in_M == clk_O_B3_R2,  clk_B3_in_M == hMill_B3_in_M,  clk_B3_in_M == clk_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M2,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_O_B3_R2 >= hMill_I_B3_R1,  hMill_I_B3_R1 >= hMill_B3_out_M,  hMill_B3_out_M >= 0,  hMill_O_B3_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M4,  clk_B3_in_M >= hMill_I_B3_M,  clk_B3_out_M >= clk_O_B3_R2,  hMill_I_B3_M >= 0,  clk_O_B3_R2 >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == clk_O_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_B3_out_M == hMill_O_B3_M,  clk_B3_out_M == clk_I_B3_R1,  clk_B3_out_M == hMill_I_B3_R1,  clk_O_B3_R2 == hMill_O_B3_R2), And(M4,  clk_B3_in_M >= hMill_I_B3_M,  clk_B3_out_M >= hMill_O_B3_M,  clk_O_B3_R2 >= hMill_I_B3_R1,  hMill_I_B3_M >= 0,  hMill_I_B3_R1 >= clk_B3_out_M,  hMill_O_B3_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M2,  clk_B3_in_M >= hMill_O_B3_M,  hMill_I_B3_R1 >= hMill_B3_out_M,  hMill_B3_out_M >= 0,  hMill_O_B3_M >= hMill_I_B3_R1,  clk_B3_in_M == hMill_I_B3_M,  clk_B3_in_M == hMill_O_B3_R2,  clk_B3_in_M == clk_O_B3_R2,  clk_B3_in_M == hMill_B3_in_M,  clk_B3_in_M == clk_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M0,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= hMill_O_B3_R2,  clk_B3_out_M >= hMill_O_B3_M,  hMill_O_B3_R2 >= 0,  hMill_I_B3_R1 >= clk_B3_out_M,  hMill_O_B3_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M0,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_B3_out_M >= clk_O_B3_M,  clk_O_B3_R2 >= hMill_I_B3_R1,  clk_O_B3_M >= 0,  hMill_I_B3_R1 >= clk_B3_out_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M3,  clk_I_B3_M >= clk_O_B3_R2,  clk_B3_out_M >= hMill_O_B3_M,  hMill_B3_in_M >= 0,  clk_O_B3_R2 >= hMill_B3_in_M,  hMill_I_B3_R1 >= clk_B3_out_M,  hMill_O_B3_M >= clk_I_B3_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M1,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_B3_out_M >= hMill_O_B3_M,  clk_O_B3_R2 >= clk_I_B3_R1,  clk_I_B3_R1 >= 0,  hMill_O_B3_M >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M3,  clk_I_B3_M >= clk_O_B3_R2,  clk_B3_out_M >= hMill_O_B3_M,  hMill_B3_in_M >= 0,  clk_O_B3_R2 >= hMill_I_B3_R1,  hMill_O_B3_M >= hMill_B3_in_M,  hMill_I_B3_R1 >= clk_B3_out_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M1,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_B3_out_M >= hMill_O_B3_M,  clk_I_B3_R1 >= 0,  hMill_O_B3_M >= clk_I_B3_R1,  clk_O_B3_R2 >= clk_B3_out_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M4,  clk_B3_in_M >= hMill_I_B3_M,  clk_B3_out_M >= hMill_O_B3_M,  hMill_I_B3_M >= 0,  hMill_O_B3_M >= clk_O_B3_R2,  hMill_I_B3_R1 >= clk_B3_out_M,  clk_O_B3_R2 >= clk_B3_in_M,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M), And(M2,  clk_B3_in_M >= clk_I_B3_M,  clk_I_B3_M >= clk_O_B3_R2,  clk_O_B3_R2 >= hMill_O_B3_M,  hMill_I_B3_R1 >= hMill_B3_out_M,  hMill_B3_out_M >= 0,  hMill_O_B3_M >= hMill_I_B3_R1,  clk_B3_in_M == hMill_B3_in_M,  clk_I_B3_M == hMill_I_B3_M,  clk_B3_out_M == hMill_B3_out_M,  clk_O_B3_R2 == hMill_O_B3_R2,  hMill_I_B3_R1 == clk_I_B3_R1,  hMill_O_B3_M == clk_O_B3_M))
[info] 
[info] NotAt2Locs_Millhh  = Not(Or(And(M2, M4), And(M2, M0), And(M2, M1), And(M2, M3), And(M4, M0), And(M4, M1), And(M4, M3), And(M0, M1), And(M0, M3), And(M1, M3)))
[info] 
[info] Kp_Millhh = And(Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_O_B3_M >= 0, clk_B3_in_M == clk_O_B3_M, clk_I_B3_M == clk_O_B3_M, clk_B3_out_M == clk_O_B3_M, hMill_B3_in_M == clk_O_B3_M, clk_O_B3_R2 == clk_O_B3_M, hMill_I_B3_R1 == clk_O_B3_M, hMill_O_B3_R2 == clk_O_B3_M, hMill_I_B3_M == clk_O_B3_M, clk_I_B3_R1 == clk_O_B3_M, hMill_O_B3_M == clk_O_B3_M, hMill_B3_out_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_I_B3_M >= hMill_B3_in_M, hMill_B3_in_M >= 0, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == clk_O_B3_M, clk_I_B3_M == hMill_B3_out_M, clk_I_B3_M == hMill_O_B3_M, clk_I_B3_M == clk_I_B3_R1, clk_I_B3_M == hMill_I_B3_M, clk_I_B3_M == hMill_O_B3_R2, clk_I_B3_M == hMill_I_B3_R1, clk_I_B3_M == clk_O_B3_R2, clk_I_B3_M == clk_B3_out_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_R1, clk_I_B3_R1 >= 0, clk_B3_in_M == clk_O_B3_M, clk_B3_in_M == hMill_B3_out_M, clk_B3_in_M == hMill_O_B3_M, clk_B3_in_M == hMill_I_B3_M, clk_B3_in_M == hMill_O_B3_R2, clk_B3_in_M == clk_O_B3_R2, clk_B3_in_M == hMill_B3_in_M, clk_B3_in_M == clk_B3_out_M, clk_B3_in_M == clk_I_B3_M, hMill_I_B3_R1 == clk_I_B3_R1))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_M, hMill_I_B3_M >= 0, clk_B3_out_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == clk_O_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_B3_out_M == hMill_O_B3_M, clk_B3_out_M == clk_I_B3_R1, clk_B3_out_M == hMill_O_B3_R2, clk_B3_out_M == hMill_I_B3_R1, clk_B3_out_M == clk_O_B3_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_R1, hMill_I_B3_R1 >= hMill_B3_out_M, hMill_B3_out_M >= 0, clk_B3_in_M == clk_O_B3_M, clk_B3_in_M == hMill_O_B3_M, clk_B3_in_M == hMill_I_B3_M, clk_B3_in_M == hMill_O_B3_R2, clk_B3_in_M == clk_O_B3_R2, clk_B3_in_M == hMill_B3_in_M, clk_B3_in_M == clk_I_B3_M, clk_B3_out_M == hMill_B3_out_M, hMill_I_B3_R1 == clk_I_B3_R1))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= hMill_O_B3_R2, hMill_O_B3_R2 >= 0, clk_B3_out_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == clk_O_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_B3_out_M == hMill_O_B3_M, clk_B3_out_M == clk_I_B3_R1, clk_B3_out_M == hMill_I_B3_R1, clk_O_B3_R2 == hMill_O_B3_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_R1, clk_B3_out_M >= clk_O_B3_M, clk_O_B3_M >= 0, hMill_I_B3_R1 >= clk_B3_out_M, clk_B3_in_M == hMill_I_B3_M, clk_B3_in_M == hMill_O_B3_R2, clk_B3_in_M == clk_O_B3_R2, clk_B3_in_M == hMill_B3_in_M, clk_B3_in_M == clk_I_B3_M, clk_B3_out_M == hMill_B3_out_M, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_I_B3_M >= clk_O_B3_R2, hMill_B3_in_M >= 0, clk_O_B3_R2 >= hMill_B3_in_M, clk_B3_out_M >= clk_I_B3_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == clk_O_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_B3_out_M == hMill_O_B3_M, clk_B3_out_M == clk_I_B3_R1, clk_B3_out_M == hMill_I_B3_R1, clk_O_B3_R2 == hMill_O_B3_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= clk_O_B3_R2, clk_O_B3_R2 >= clk_I_B3_R1, clk_I_B3_R1 >= 0, clk_B3_out_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == clk_O_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_B3_out_M == hMill_O_B3_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_I_B3_M >= hMill_I_B3_R1, clk_B3_out_M >= hMill_O_B3_M, hMill_B3_in_M >= 0, hMill_O_B3_M >= hMill_B3_in_M, hMill_I_B3_R1 >= clk_B3_out_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_I_B3_M == hMill_O_B3_R2, clk_I_B3_M == clk_O_B3_R2, clk_B3_out_M == hMill_B3_out_M, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_B3_out_M, clk_B3_out_M >= hMill_O_B3_M, clk_I_B3_R1 >= 0, hMill_O_B3_M >= clk_I_B3_R1, clk_B3_in_M == hMill_I_B3_M, clk_B3_in_M == hMill_O_B3_R2, clk_B3_in_M == clk_O_B3_R2, clk_B3_in_M == hMill_B3_in_M, clk_B3_in_M == clk_I_B3_M, clk_B3_out_M == hMill_B3_out_M, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= clk_O_B3_R2, clk_O_B3_R2 >= hMill_I_B3_R1, hMill_I_B3_R1 >= hMill_B3_out_M, hMill_B3_out_M >= 0, hMill_O_B3_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_M, clk_B3_out_M >= clk_O_B3_R2, hMill_I_B3_M >= 0, clk_O_B3_R2 >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == clk_O_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_B3_out_M == hMill_O_B3_M, clk_B3_out_M == clk_I_B3_R1, clk_B3_out_M == hMill_I_B3_R1, clk_O_B3_R2 == hMill_O_B3_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_M, clk_B3_out_M >= hMill_O_B3_M, clk_O_B3_R2 >= hMill_I_B3_R1, hMill_I_B3_M >= 0, hMill_I_B3_R1 >= clk_B3_out_M, hMill_O_B3_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_O_B3_M, hMill_I_B3_R1 >= hMill_B3_out_M, hMill_B3_out_M >= 0, hMill_O_B3_M >= hMill_I_B3_R1, clk_B3_in_M == hMill_I_B3_M, clk_B3_in_M == hMill_O_B3_R2, clk_B3_in_M == clk_O_B3_R2, clk_B3_in_M == hMill_B3_in_M, clk_B3_in_M == clk_I_B3_M, clk_B3_out_M == hMill_B3_out_M, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= hMill_O_B3_R2, clk_B3_out_M >= hMill_O_B3_M, hMill_O_B3_R2 >= 0, hMill_I_B3_R1 >= clk_B3_out_M, hMill_O_B3_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= clk_O_B3_R2, clk_B3_out_M >= clk_O_B3_M, clk_O_B3_R2 >= hMill_I_B3_R1, clk_O_B3_M >= 0, hMill_I_B3_R1 >= clk_B3_out_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_I_B3_M >= clk_O_B3_R2, clk_B3_out_M >= hMill_O_B3_M, hMill_B3_in_M >= 0, clk_O_B3_R2 >= hMill_B3_in_M, hMill_I_B3_R1 >= clk_B3_out_M, hMill_O_B3_M >= clk_I_B3_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= clk_O_B3_R2, clk_B3_out_M >= hMill_O_B3_M, clk_O_B3_R2 >= clk_I_B3_R1, clk_I_B3_R1 >= 0, hMill_O_B3_M >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_I_B3_M >= clk_O_B3_R2, clk_B3_out_M >= hMill_O_B3_M, hMill_B3_in_M >= 0, clk_O_B3_R2 >= hMill_I_B3_R1, hMill_O_B3_M >= hMill_B3_in_M, hMill_I_B3_R1 >= clk_B3_out_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= clk_I_B3_M, clk_I_B3_M >= clk_O_B3_R2, clk_B3_out_M >= hMill_O_B3_M, clk_I_B3_R1 >= 0, hMill_O_B3_M >= clk_I_B3_R1, clk_O_B3_R2 >= clk_B3_out_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B3_in_M,clk_I_B3_M,clk_B3_out_M,hMill_B3_in_M,clk_O_B3_R2,hMill_I_B3_R1,hMill_O_B3_R2,hMill_I_B3_M,clk_I_B3_R1,hMill_O_B3_M,hMill_B3_out_M,clk_O_B3_M], And( clk_B3_in_M >= hMill_I_B3_M, clk_B3_out_M >= hMill_O_B3_M, hMill_I_B3_M >= 0, hMill_O_B3_M >= clk_O_B3_R2, hMill_I_B3_R1 >= clk_B3_out_M, clk_O_B3_R2 >= clk_B3_in_M, clk_B3_in_M == hMill_B3_in_M, clk_I_B3_M == hMill_I_B3_M, clk_B3_out_M == hMill_B3_out_M, clk_O_B3_R2 == hMill_O_B3_R2, hMill_I_B3_R1 == clk_I_B3_R1, hMill_O_B3_M == clk_O_B3_M))).as_expr())
[info] 
[info] ciRobot1hh = Or(And(R1_0,  hRobot1_I_B3_R1 >= 0,  clk_I_B1_C1 == hRobot1_I_B3_R1,  clk_O_B1_R1 == hRobot1_I_B3_R1,  clk_B1_out == hRobot1_I_B3_R1,  hRobot1_O_B1_R1 == hRobot1_I_B3_R1,  hRobot1_B3_in_R1 == hRobot1_I_B3_R1,  hRobot1_I_B1_C1 == hRobot1_I_B3_R1,  hRobot1_B1_out == hRobot1_I_B3_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  clk_B3_in_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == hRobot1_I_B3_R1,  clk_O_B3_M == hRobot1_I_B3_R1), And(R1_1,  clk_O_B1_R1 >= hRobot1_I_B1_C1,  hRobot1_I_B1_C1 >= 0,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_I_B3_R1,  clk_O_B1_R1 == clk_O_B3_M,  clk_O_B1_R1 == hRobot1_O_B3_M,  clk_O_B1_R1 == clk_B3_in_R1,  clk_O_B1_R1 == clk_I_B3_R1,  clk_O_B1_R1 == hRobot1_B1_out,  clk_O_B1_R1 == hRobot1_B3_in_R1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_O_B1_R1 == clk_B1_out), And(R1_2,  clk_I_B1_C1 >= hRobot1_B1_out,  hRobot1_B1_out >= 0,  clk_O_B1_R1 >= clk_I_B1_C1,  hRobot1_B1_out + 1 >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_I_B3_R1,  clk_O_B1_R1 == clk_O_B3_M,  clk_O_B1_R1 == hRobot1_O_B3_M,  clk_O_B1_R1 == clk_B3_in_R1,  clk_O_B1_R1 == clk_I_B3_R1,  clk_O_B1_R1 == hRobot1_B3_in_R1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out), And(R1_3,  clk_I_B1_C1 >= clk_B1_out,  clk_B1_out >= hRobot1_O_B1_R1,  hRobot1_O_B1_R1 >= 0,  clk_B1_out + 1 >= clk_I_B1_C1,  hRobot1_B3_in_R1 >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == hRobot1_I_B3_R1,  hRobot1_B3_in_R1 == clk_O_B3_M,  hRobot1_B3_in_R1 == hRobot1_O_B3_M,  hRobot1_B3_in_R1 == clk_B3_in_R1,  hRobot1_B3_in_R1 == clk_I_B3_R1), And(R1_4,  clk_I_B1_C1 >= clk_B1_out,  clk_O_B1_R1 >= clk_B3_in_R1,  clk_B3_in_R1 >= 0,  clk_B1_out >= clk_O_B1_R1,  clk_B1_out + 1 >= clk_I_B1_C1,  clk_I_B3_R1 >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  clk_I_B3_R1 == clk_O_B3_M,  clk_I_B3_R1 == hRobot1_O_B3_M), And(R1_5,  clk_I_B1_C1 >= clk_B1_out,  clk_O_B1_R1 >= hRobot1_B3_in_R1,  hRobot1_B3_in_R1 >= hRobot1_I_B3_R1,  hRobot1_I_B3_R1 >= 0,  clk_B1_out >= clk_O_B1_R1,  clk_B1_out + 1 >= clk_I_B1_C1,  hRobot1_O_B3_M >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M), And(R1_0,  clk_I_B1_C1 >= clk_B1_out,  clk_O_B1_R1 >= hRobot1_B3_in_R1,  hRobot1_B3_in_R1 >= clk_I_B3_R1,  clk_I_B3_R1 >= clk_O_B3_M,  clk_O_B3_M >= 0,  clk_B1_out >= clk_O_B1_R1,  clk_B1_out + 1 >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M), And(R1_1,  clk_O_B1_R1 >= hRobot1_B3_in_R1,  hRobot1_B3_in_R1 >= clk_I_B3_R1,  hRobot1_I_B1_C1 >= 0,  clk_I_B3_R1 >= hRobot1_O_B3_M,  hRobot1_O_B3_M >= hRobot1_I_B1_C1,  clk_B1_out >= clk_O_B1_R1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M), And(R1_2,  clk_I_B1_C1 >= hRobot1_B1_out,  clk_O_B1_R1 >= hRobot1_B3_in_R1,  hRobot1_B3_in_R1 >= clk_I_B3_R1,  hRobot1_B1_out >= 0,  clk_I_B3_R1 >= hRobot1_O_B3_M,  hRobot1_B1_out + 1 >= clk_I_B1_C1,  hRobot1_O_B3_M >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M), And(R1_3,  clk_I_B1_C1 >= clk_B1_out,  clk_B1_out >= hRobot1_O_B1_R1,  hRobot1_O_B1_R1 >= 0,  hRobot1_B3_in_R1 >= clk_I_B3_R1,  clk_I_B3_R1 >= hRobot1_O_B3_M,  clk_B1_out + 1 >= clk_I_B1_C1,  hRobot1_O_B3_M >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M), And(R1_4,  clk_I_B1_C1 >= clk_B1_out,  clk_O_B1_R1 >= clk_B3_in_R1,  clk_I_B3_R1 >= hRobot1_O_B3_M,  clk_B3_in_R1 >= 0,  clk_B1_out >= clk_O_B1_R1,  clk_B1_out + 1 >= clk_I_B1_C1,  hRobot1_O_B3_M >= clk_I_B1_C1,  clk_I_B1_C1 == hRobot1_I_B1_C1,  clk_O_B1_R1 == hRobot1_O_B1_R1,  clk_B1_out == hRobot1_B1_out,  hRobot1_B3_in_R1 == clk_B3_in_R1,  clk_I_B3_R1 == hRobot1_I_B3_R1,  hRobot1_O_B3_M == clk_O_B3_M))
[info] 
[info] NotAt2Locs_Robot1hh  = Not(Or(And(R1_4, R1_1), And(R1_4, R1_5), And(R1_4, R1_2), And(R1_4, R1_3), And(R1_4, R1_0), And(R1_1, R1_5), And(R1_1, R1_2), And(R1_1, R1_3), And(R1_1, R1_0), And(R1_5, R1_2), And(R1_5, R1_3), And(R1_5, R1_0), And(R1_2, R1_3), And(R1_2, R1_0), And(R1_3, R1_0)))
[info] 
[info] Kp_Robot1hh = And(Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( hRobot1_I_B3_R1 >= 0, clk_I_B1_C1 == hRobot1_I_B3_R1, clk_O_B1_R1 == hRobot1_I_B3_R1, clk_B1_out == hRobot1_I_B3_R1, hRobot1_O_B1_R1 == hRobot1_I_B3_R1, hRobot1_B3_in_R1 == hRobot1_I_B3_R1, hRobot1_I_B1_C1 == hRobot1_I_B3_R1, hRobot1_B1_out == hRobot1_I_B3_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, clk_B3_in_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == hRobot1_I_B3_R1, clk_O_B3_M == hRobot1_I_B3_R1))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_O_B1_R1 >= hRobot1_I_B1_C1, hRobot1_I_B1_C1 >= 0, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_I_B3_R1, clk_O_B1_R1 == clk_O_B3_M, clk_O_B1_R1 == hRobot1_O_B3_M, clk_O_B1_R1 == clk_B3_in_R1, clk_O_B1_R1 == clk_I_B3_R1, clk_O_B1_R1 == hRobot1_B1_out, clk_O_B1_R1 == hRobot1_B3_in_R1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_O_B1_R1 == clk_B1_out))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= hRobot1_B1_out, hRobot1_B1_out >= 0, clk_O_B1_R1 >= clk_I_B1_C1, hRobot1_B1_out + 1 >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_I_B3_R1, clk_O_B1_R1 == clk_O_B3_M, clk_O_B1_R1 == hRobot1_O_B3_M, clk_O_B1_R1 == clk_B3_in_R1, clk_O_B1_R1 == clk_I_B3_R1, clk_O_B1_R1 == hRobot1_B3_in_R1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= clk_B1_out, clk_B1_out >= hRobot1_O_B1_R1, hRobot1_O_B1_R1 >= 0, clk_B1_out + 1 >= clk_I_B1_C1, hRobot1_B3_in_R1 >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == hRobot1_I_B3_R1, hRobot1_B3_in_R1 == clk_O_B3_M, hRobot1_B3_in_R1 == hRobot1_O_B3_M, hRobot1_B3_in_R1 == clk_B3_in_R1, hRobot1_B3_in_R1 == clk_I_B3_R1))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= clk_B1_out, clk_O_B1_R1 >= clk_B3_in_R1, clk_B3_in_R1 >= 0, clk_B1_out >= clk_O_B1_R1, clk_B1_out + 1 >= clk_I_B1_C1, clk_I_B3_R1 >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, clk_I_B3_R1 == clk_O_B3_M, clk_I_B3_R1 == hRobot1_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= clk_B1_out, clk_O_B1_R1 >= hRobot1_B3_in_R1, hRobot1_B3_in_R1 >= hRobot1_I_B3_R1, hRobot1_I_B3_R1 >= 0, clk_B1_out >= clk_O_B1_R1, clk_B1_out + 1 >= clk_I_B1_C1, hRobot1_O_B3_M >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= clk_B1_out, clk_O_B1_R1 >= hRobot1_B3_in_R1, hRobot1_B3_in_R1 >= clk_I_B3_R1, clk_I_B3_R1 >= clk_O_B3_M, clk_O_B3_M >= 0, clk_B1_out >= clk_O_B1_R1, clk_B1_out + 1 >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_O_B1_R1 >= hRobot1_B3_in_R1, hRobot1_B3_in_R1 >= clk_I_B3_R1, hRobot1_I_B1_C1 >= 0, clk_I_B3_R1 >= hRobot1_O_B3_M, hRobot1_O_B3_M >= hRobot1_I_B1_C1, clk_B1_out >= clk_O_B1_R1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= hRobot1_B1_out, clk_O_B1_R1 >= hRobot1_B3_in_R1, hRobot1_B3_in_R1 >= clk_I_B3_R1, hRobot1_B1_out >= 0, clk_I_B3_R1 >= hRobot1_O_B3_M, hRobot1_B1_out + 1 >= clk_I_B1_C1, hRobot1_O_B3_M >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == clk_O_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,clk_O_B1_R1,clk_B1_out,hRobot1_O_B1_R1,hRobot1_B3_in_R1,hRobot1_I_B1_C1,hRobot1_B1_out,clk_I_B3_R1,clk_B3_in_R1,hRobot1_O_B3_M,clk_O_B3_M,hRobot1_I_B3_R1], And( clk_I_B1_C1 >= clk_B1_out, clk_B1_out >= hRobot1_O_B1_R1, hRobot1_O_B1_R1 >= 0, hRobot1_B3_in_R1 >= clk_I_B3_R1, clk_I_B3_R1 >= hRobot1_O_B3_M, clk_B1_out + 1 >= clk_I_B1_C1, hRobot1_O_B3_M >= clk_I_B1_C1, clk_I_B1_C1 == hRobot1_I_B1_C1, clk_O_B1_R1 == hRobot1_O_B1_R1, clk_B1_out == hRobot1_B1_out, hRobot1_B3_in_R1 == clk_B3_in_R1, clk_I_B3_R1 == hRobot1_I_B3_R1, hRobot1_O_B3_M == clk_O_B3_M))).as_expr())
[info] 
[info] ciRobot2hh = Or(And(R2_0,  clk_B3_out_R2 >= 0,  clk_B5_in_R2 == clk_B3_out_R2,  hRobot2_O_B5_A == clk_B3_out_R2,  hRobot2_O_B3_R2 == clk_B3_out_R2,  clk_O_B5_A == clk_B3_out_R2,  hRobot2_I_B5_R2 == clk_B3_out_R2,  hRobot2_B5_in_R2 == clk_B3_out_R2,  clk_I_B3_M == clk_B3_out_R2,  clk_O_B3_R2 == clk_B3_out_R2,  clk_I_B5_R2 == clk_B3_out_R2,  hRobot2_B3_out_R2 == clk_B3_out_R2,  hRobot2_I_B3_M == clk_B3_out_R2), And(R2_1,  clk_B5_in_R2 >= hRobot2_I_B3_M,  hRobot2_I_B3_M >= 0,  clk_B5_in_R2 == clk_B3_out_R2,  clk_B5_in_R2 == hRobot2_B3_out_R2,  clk_B5_in_R2 == clk_I_B5_R2,  clk_B5_in_R2 == clk_O_B3_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  clk_B5_in_R2 == hRobot2_I_B5_R2,  clk_B5_in_R2 == clk_O_B5_A,  clk_B5_in_R2 == hRobot2_O_B3_R2,  clk_B5_in_R2 == hRobot2_O_B5_A,  clk_I_B3_M == hRobot2_I_B3_M), And(R2_2,  clk_B5_in_R2 >= clk_I_B3_M,  clk_I_B3_M >= clk_B3_out_R2,  clk_B3_out_R2 >= 0,  clk_B5_in_R2 == clk_I_B5_R2,  clk_B5_in_R2 == clk_O_B3_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  clk_B5_in_R2 == hRobot2_I_B5_R2,  clk_B5_in_R2 == clk_O_B5_A,  clk_B5_in_R2 == hRobot2_O_B3_R2,  clk_B5_in_R2 == hRobot2_O_B5_A,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_3,  clk_B5_in_R2 >= clk_I_B3_M,  clk_I_B3_M >= hRobot2_B3_out_R2,  clk_O_B3_R2 >= 0,  hRobot2_B3_out_R2 >= clk_O_B3_R2,  clk_B5_in_R2 == clk_I_B5_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  clk_B5_in_R2 == hRobot2_I_B5_R2,  clk_B5_in_R2 == clk_O_B5_A,  clk_B5_in_R2 == hRobot2_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_4,  hRobot2_O_B5_A >= clk_I_B3_M,  hRobot2_O_B3_R2 >= hRobot2_B5_in_R2,  hRobot2_B5_in_R2 >= 0,  clk_I_B3_M >= hRobot2_B3_out_R2,  hRobot2_B3_out_R2 >= hRobot2_O_B3_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_I_B5_R2,  hRobot2_O_B5_A == hRobot2_I_B5_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_5,  clk_B5_in_R2 >= clk_I_B5_R2,  hRobot2_O_B5_A >= clk_I_B3_M,  clk_I_B3_M >= hRobot2_B3_out_R2,  clk_I_B5_R2 >= 0,  hRobot2_B3_out_R2 >= hRobot2_O_B3_R2,  hRobot2_O_B3_R2 >= clk_B5_in_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_0,  clk_B5_in_R2 >= hRobot2_I_B5_R2,  clk_O_B5_A >= 0,  clk_I_B3_M >= hRobot2_B3_out_R2,  hRobot2_I_B5_R2 >= clk_O_B5_A,  hRobot2_B3_out_R2 >= hRobot2_O_B3_R2,  hRobot2_O_B3_R2 >= clk_B5_in_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_1,  clk_B5_in_R2 >= hRobot2_I_B5_R2,  hRobot2_O_B5_A >= hRobot2_I_B3_M,  hRobot2_I_B3_M >= 0,  hRobot2_B3_out_R2 >= hRobot2_O_B3_R2,  hRobot2_I_B5_R2 >= hRobot2_O_B5_A,  hRobot2_O_B3_R2 >= clk_B5_in_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_2,  clk_B5_in_R2 >= hRobot2_I_B5_R2,  hRobot2_O_B5_A >= clk_I_B3_M,  clk_I_B3_M >= clk_B3_out_R2,  clk_B3_out_R2 >= 0,  hRobot2_I_B5_R2 >= hRobot2_O_B5_A,  hRobot2_O_B3_R2 >= clk_B5_in_R2,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_3,  clk_B5_in_R2 >= hRobot2_I_B5_R2,  hRobot2_O_B5_A >= clk_I_B3_M,  clk_I_B3_M >= hRobot2_B3_out_R2,  clk_O_B3_R2 >= 0,  hRobot2_B3_out_R2 >= clk_O_B3_R2,  hRobot2_I_B5_R2 >= hRobot2_O_B5_A,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2), And(R2_4,  hRobot2_O_B5_A >= clk_I_B3_M,  hRobot2_O_B3_R2 >= hRobot2_B5_in_R2,  hRobot2_B5_in_R2 >= 0,  clk_I_B3_M >= hRobot2_B3_out_R2,  hRobot2_B3_out_R2 >= hRobot2_O_B3_R2,  hRobot2_I_B5_R2 >= hRobot2_O_B5_A,  clk_B5_in_R2 == hRobot2_B5_in_R2,  hRobot2_O_B5_A == clk_O_B5_A,  hRobot2_O_B3_R2 == clk_O_B3_R2,  hRobot2_I_B5_R2 == clk_I_B5_R2,  clk_I_B3_M == hRobot2_I_B3_M,  hRobot2_B3_out_R2 == clk_B3_out_R2))
[info] 
[info] NotAt2Locs_Robot2hh  = Not(Or(And(R2_2, R2_5), And(R2_2, R2_1), And(R2_2, R2_4), And(R2_2, R2_0), And(R2_2, R2_3), And(R2_5, R2_1), And(R2_5, R2_4), And(R2_5, R2_0), And(R2_5, R2_3), And(R2_1, R2_4), And(R2_1, R2_0), And(R2_1, R2_3), And(R2_4, R2_0), And(R2_4, R2_3), And(R2_0, R2_3)))
[info] 
[info] Kp_Robot2hh = And(Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B3_out_R2 >= 0, clk_B5_in_R2 == clk_B3_out_R2, hRobot2_O_B5_A == clk_B3_out_R2, hRobot2_O_B3_R2 == clk_B3_out_R2, clk_O_B5_A == clk_B3_out_R2, hRobot2_I_B5_R2 == clk_B3_out_R2, hRobot2_B5_in_R2 == clk_B3_out_R2, clk_I_B3_M == clk_B3_out_R2, clk_O_B3_R2 == clk_B3_out_R2, clk_I_B5_R2 == clk_B3_out_R2, hRobot2_B3_out_R2 == clk_B3_out_R2, hRobot2_I_B3_M == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= hRobot2_I_B3_M, hRobot2_I_B3_M >= 0, clk_B5_in_R2 == clk_B3_out_R2, clk_B5_in_R2 == hRobot2_B3_out_R2, clk_B5_in_R2 == clk_I_B5_R2, clk_B5_in_R2 == clk_O_B3_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, clk_B5_in_R2 == hRobot2_I_B5_R2, clk_B5_in_R2 == clk_O_B5_A, clk_B5_in_R2 == hRobot2_O_B3_R2, clk_B5_in_R2 == hRobot2_O_B5_A, clk_I_B3_M == hRobot2_I_B3_M))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= clk_I_B3_M, clk_I_B3_M >= clk_B3_out_R2, clk_B3_out_R2 >= 0, clk_B5_in_R2 == clk_I_B5_R2, clk_B5_in_R2 == clk_O_B3_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, clk_B5_in_R2 == hRobot2_I_B5_R2, clk_B5_in_R2 == clk_O_B5_A, clk_B5_in_R2 == hRobot2_O_B3_R2, clk_B5_in_R2 == hRobot2_O_B5_A, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= clk_I_B3_M, clk_I_B3_M >= hRobot2_B3_out_R2, clk_O_B3_R2 >= 0, hRobot2_B3_out_R2 >= clk_O_B3_R2, clk_B5_in_R2 == clk_I_B5_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, clk_B5_in_R2 == hRobot2_I_B5_R2, clk_B5_in_R2 == clk_O_B5_A, clk_B5_in_R2 == hRobot2_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( hRobot2_O_B5_A >= clk_I_B3_M, hRobot2_O_B3_R2 >= hRobot2_B5_in_R2, hRobot2_B5_in_R2 >= 0, clk_I_B3_M >= hRobot2_B3_out_R2, hRobot2_B3_out_R2 >= hRobot2_O_B3_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_I_B5_R2, hRobot2_O_B5_A == hRobot2_I_B5_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= clk_I_B5_R2, hRobot2_O_B5_A >= clk_I_B3_M, clk_I_B3_M >= hRobot2_B3_out_R2, clk_I_B5_R2 >= 0, hRobot2_B3_out_R2 >= hRobot2_O_B3_R2, hRobot2_O_B3_R2 >= clk_B5_in_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, hRobot2_I_B5_R2 == clk_I_B5_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= hRobot2_I_B5_R2, clk_O_B5_A >= 0, clk_I_B3_M >= hRobot2_B3_out_R2, hRobot2_I_B5_R2 >= clk_O_B5_A, hRobot2_B3_out_R2 >= hRobot2_O_B3_R2, hRobot2_O_B3_R2 >= clk_B5_in_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, hRobot2_I_B5_R2 == clk_I_B5_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= hRobot2_I_B5_R2, hRobot2_O_B5_A >= hRobot2_I_B3_M, hRobot2_I_B3_M >= 0, hRobot2_B3_out_R2 >= hRobot2_O_B3_R2, hRobot2_I_B5_R2 >= hRobot2_O_B5_A, hRobot2_O_B3_R2 >= clk_B5_in_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, hRobot2_I_B5_R2 == clk_I_B5_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= hRobot2_I_B5_R2, hRobot2_O_B5_A >= clk_I_B3_M, clk_I_B3_M >= clk_B3_out_R2, clk_B3_out_R2 >= 0, hRobot2_I_B5_R2 >= hRobot2_O_B5_A, hRobot2_O_B3_R2 >= clk_B5_in_R2, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, hRobot2_I_B5_R2 == clk_I_B5_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_B5_in_R2,hRobot2_O_B5_A,hRobot2_O_B3_R2,clk_O_B5_A,hRobot2_I_B5_R2,hRobot2_B5_in_R2,clk_I_B3_M,clk_O_B3_R2,clk_I_B5_R2,hRobot2_B3_out_R2,hRobot2_I_B3_M,clk_B3_out_R2], And( clk_B5_in_R2 >= hRobot2_I_B5_R2, hRobot2_O_B5_A >= clk_I_B3_M, clk_I_B3_M >= hRobot2_B3_out_R2, clk_O_B3_R2 >= 0, hRobot2_B3_out_R2 >= clk_O_B3_R2, hRobot2_I_B5_R2 >= hRobot2_O_B5_A, clk_B5_in_R2 == hRobot2_B5_in_R2, hRobot2_O_B5_A == clk_O_B5_A, hRobot2_O_B3_R2 == clk_O_B3_R2, hRobot2_I_B5_R2 == clk_I_B5_R2, clk_I_B3_M == hRobot2_I_B3_M, hRobot2_B3_out_R2 == clk_B3_out_R2))).as_expr())
[info] 
[info] ciConveyor1hh = Or(And(C0,  hConveyor_B1_in >= 0,  clk_I_B1_C1 == hConveyor_B1_in,  hConveyor_O_B1_R1 == hConveyor_B1_in,  hConveyor_I_B1_C1 == hConveyor_B1_in,  clk_B1_R1 == hConveyor_B1_in,  clk_B1_in == hConveyor_B1_in), And(C1,  clk_I_B1_C1 >= hConveyor_B1_in,  hConveyor_B1_in >= 0,  clk_I_B1_C1 == clk_B1_R1,  clk_I_B1_C1 == hConveyor_I_B1_C1,  clk_I_B1_C1 == hConveyor_O_B1_R1,  clk_B1_in == hConveyor_B1_in), And(C2,  hConveyor_O_B1_R1 >= clk_B1_in,  hConveyor_I_B1_C1 >= 0,  clk_B1_in >= hConveyor_I_B1_C1,  clk_I_B1_C1 == hConveyor_I_B1_C1,  hConveyor_O_B1_R1 == clk_B1_R1,  clk_B1_in == hConveyor_B1_in), And(C0,  clk_I_B1_C1 >= clk_B1_R1,  clk_B1_R1 >= 0,  clk_B1_in >= clk_I_B1_C1,  clk_I_B1_C1 == hConveyor_I_B1_C1,  hConveyor_O_B1_R1 == clk_B1_R1,  clk_B1_in == hConveyor_B1_in), And(C1,  clk_I_B1_C1 >= hConveyor_O_B1_R1,  hConveyor_O_B1_R1 >= hConveyor_B1_in,  hConveyor_B1_in >= 0,  clk_I_B1_C1 == hConveyor_I_B1_C1,  hConveyor_O_B1_R1 == clk_B1_R1,  clk_B1_in == hConveyor_B1_in))
[info] 
[info] NotAt2Locs_Conveyor1hh  = Not(Or(And(C0, C1), And(C0, C2), And(C1, C2)))
[info] 
[info] Kp_Conveyor1hh = And(Tactic('qe2').apply(Exists([clk_I_B1_C1,hConveyor_O_B1_R1,hConveyor_I_B1_C1,clk_B1_R1,clk_B1_in,hConveyor_B1_in], And( hConveyor_B1_in >= 0, clk_I_B1_C1 == hConveyor_B1_in, hConveyor_O_B1_R1 == hConveyor_B1_in, hConveyor_I_B1_C1 == hConveyor_B1_in, clk_B1_R1 == hConveyor_B1_in, clk_B1_in == hConveyor_B1_in))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,hConveyor_O_B1_R1,hConveyor_I_B1_C1,clk_B1_R1,clk_B1_in,hConveyor_B1_in], And( clk_I_B1_C1 >= hConveyor_B1_in, hConveyor_B1_in >= 0, clk_I_B1_C1 == clk_B1_R1, clk_I_B1_C1 == hConveyor_I_B1_C1, clk_I_B1_C1 == hConveyor_O_B1_R1, clk_B1_in == hConveyor_B1_in))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,hConveyor_O_B1_R1,hConveyor_I_B1_C1,clk_B1_R1,clk_B1_in,hConveyor_B1_in], And( hConveyor_O_B1_R1 >= clk_B1_in, hConveyor_I_B1_C1 >= 0, clk_B1_in >= hConveyor_I_B1_C1, clk_I_B1_C1 == hConveyor_I_B1_C1, hConveyor_O_B1_R1 == clk_B1_R1, clk_B1_in == hConveyor_B1_in))).as_expr(), Tactic('qe2').apply(Exists([clk_I_B1_C1,hConveyor_O_B1_R1,hConveyor_I_B1_C1,clk_B1_R1,clk_B1_in,hConveyor_B1_in], And( clk_I_B1_C1 >= clk_B1_R1, clk_B1_R1 >= 0, clk_B1_in >= clk_I_B1_C1, clk_I_B1_C1 == hConveyor_I_B1_C1, hConveyor_O_B1_R1 == clk_B1_R1, clk_B1_in == hConveyor_B1_in))).as_expr())
[info] 
[info] ciAssemblyStationhh = Or(And(A0,  hAssembly_product >= 0,  clk_product == hAssembly_product,  hAssembly_B5_out_A == hAssembly_product,  clk_B5_out_A == hAssembly_product,  clk_O_B5_A == hAssembly_product,  hAssembly_O_B5_A == hAssembly_product,  clk_I_B5_R2 == hAssembly_product,  hAssembly_I_B5_R2 == hAssembly_product), And(A1,  clk_product >= hAssembly_I_B5_R2,  hAssembly_I_B5_R2 >= 0,  clk_product == hAssembly_product,  clk_product == hAssembly_O_B5_A,  clk_product == clk_O_B5_A,  clk_product == clk_B5_out_A,  clk_product == hAssembly_B5_out_A,  clk_I_B5_R2 == hAssembly_I_B5_R2), And(A2,  clk_product >= clk_I_B5_R2,  clk_B5_out_A >= 0,  clk_I_B5_R2 >= clk_B5_out_A,  clk_product == hAssembly_product,  clk_product == hAssembly_O_B5_A,  clk_product == clk_O_B5_A,  hAssembly_B5_out_A == clk_B5_out_A,  clk_I_B5_R2 == hAssembly_I_B5_R2), And(A3,  clk_product >= clk_I_B5_R2,  hAssembly_B5_out_A >= hAssembly_O_B5_A,  hAssembly_O_B5_A >= 0,  clk_I_B5_R2 >= hAssembly_B5_out_A,  clk_product == hAssembly_product,  hAssembly_B5_out_A == clk_B5_out_A,  clk_O_B5_A == hAssembly_O_B5_A,  clk_I_B5_R2 == hAssembly_I_B5_R2), And(A0,  hAssembly_B5_out_A >= clk_O_B5_A,  clk_O_B5_A >= hAssembly_product,  hAssembly_product >= 0,  clk_I_B5_R2 >= hAssembly_B5_out_A,  clk_product == hAssembly_product,  hAssembly_B5_out_A == clk_B5_out_A,  clk_O_B5_A == hAssembly_O_B5_A,  clk_I_B5_R2 == hAssembly_I_B5_R2), And(A1,  clk_product >= hAssembly_I_B5_R2,  hAssembly_B5_out_A >= clk_O_B5_A,  hAssembly_I_B5_R2 >= 0,  clk_O_B5_A >= clk_product,  clk_product == hAssembly_product,  hAssembly_B5_out_A == clk_B5_out_A,  clk_O_B5_A == hAssembly_O_B5_A,  clk_I_B5_R2 == hAssembly_I_B5_R2), And(A2,  clk_product >= clk_I_B5_R2,  clk_B5_out_A >= 0,  clk_I_B5_R2 >= clk_B5_out_A,  clk_O_B5_A >= clk_product,  clk_product == hAssembly_product,  hAssembly_B5_out_A == clk_B5_out_A,  clk_O_B5_A == hAssembly_O_B5_A,  clk_I_B5_R2 == hAssembly_I_B5_R2))
[info] 
[info] NotAt2Locs_AssemblyStationhh  = Not(Or(And(A0, A1), And(A0, A2), And(A0, A3), And(A1, A2), And(A1, A3), And(A2, A3)))
[info] 
[info] Kp_AssemblyStationhh = And(Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( hAssembly_product >= 0, clk_product == hAssembly_product, hAssembly_B5_out_A == hAssembly_product, clk_B5_out_A == hAssembly_product, clk_O_B5_A == hAssembly_product, hAssembly_O_B5_A == hAssembly_product, clk_I_B5_R2 == hAssembly_product, hAssembly_I_B5_R2 == hAssembly_product))).as_expr(), Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( clk_product >= hAssembly_I_B5_R2, hAssembly_I_B5_R2 >= 0, clk_product == hAssembly_product, clk_product == hAssembly_O_B5_A, clk_product == clk_O_B5_A, clk_product == clk_B5_out_A, clk_product == hAssembly_B5_out_A, clk_I_B5_R2 == hAssembly_I_B5_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( clk_product >= clk_I_B5_R2, clk_B5_out_A >= 0, clk_I_B5_R2 >= clk_B5_out_A, clk_product == hAssembly_product, clk_product == hAssembly_O_B5_A, clk_product == clk_O_B5_A, hAssembly_B5_out_A == clk_B5_out_A, clk_I_B5_R2 == hAssembly_I_B5_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( clk_product >= clk_I_B5_R2, hAssembly_B5_out_A >= hAssembly_O_B5_A, hAssembly_O_B5_A >= 0, clk_I_B5_R2 >= hAssembly_B5_out_A, clk_product == hAssembly_product, hAssembly_B5_out_A == clk_B5_out_A, clk_O_B5_A == hAssembly_O_B5_A, clk_I_B5_R2 == hAssembly_I_B5_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( hAssembly_B5_out_A >= clk_O_B5_A, clk_O_B5_A >= hAssembly_product, hAssembly_product >= 0, clk_I_B5_R2 >= hAssembly_B5_out_A, clk_product == hAssembly_product, hAssembly_B5_out_A == clk_B5_out_A, clk_O_B5_A == hAssembly_O_B5_A, clk_I_B5_R2 == hAssembly_I_B5_R2))).as_expr(), Tactic('qe2').apply(Exists([clk_product,hAssembly_B5_out_A,clk_B5_out_A,clk_O_B5_A,hAssembly_O_B5_A,clk_I_B5_R2,hAssembly_I_B5_R2,hAssembly_product], And( clk_product >= hAssembly_I_B5_R2, hAssembly_B5_out_A >= clk_O_B5_A, hAssembly_I_B5_R2 >= 0, clk_O_B5_A >= clk_product, clk_product == hAssembly_product, hAssembly_B5_out_A == clk_B5_out_A, clk_O_B5_A == hAssembly_O_B5_A, clk_I_B5_R2 == hAssembly_I_B5_R2))).as_expr())
[info] 
[info] ciSpec1hh = Or(And(S0,  hSpec1_B1_in >= 0,  clk_B1_in == hSpec1_B1_in,  clk_B1_out == hSpec1_B1_in,  hSpec1_B1_out == hSpec1_B1_in), And(S1,  clk_B1_out >= hSpec1_B1_in,  hSpec1_B1_in >= 0,  clk_B1_in == hSpec1_B1_in,  clk_B1_out == hSpec1_B1_out), And(ERROR,  clk_B1_in >= hSpec1_B1_out,  hSpec1_B1_out >= 0,  clk_B1_in == hSpec1_B1_in,  clk_B1_out == hSpec1_B1_out), And(S0,  clk_B1_in >= hSpec1_B1_out,  hSpec1_B1_out >= 0,  hSpec1_B1_out + 3 >= clk_B1_in,  clk_B1_in == hSpec1_B1_in,  clk_B1_out == hSpec1_B1_out), And(ERROR,  clk_B1_in > 3 + hSpec1_B1_out,  hSpec1_B1_out >= 0,  clk_B1_in == hSpec1_B1_in,  clk_B1_out == hSpec1_B1_out))
[info] 
[info] NotAt2Locs_Spec1hh  = Not(Or(And(S0, S1), And(S0, ERROR), And(S1, ERROR)))
[info] 
[info] Kp_Spec1hh = And(Tactic('qe2').apply(Exists([clk_B1_in,clk_B1_out,hSpec1_B1_out,hSpec1_B1_in], And( hSpec1_B1_in >= 0, clk_B1_in == hSpec1_B1_in, clk_B1_out == hSpec1_B1_in, hSpec1_B1_out == hSpec1_B1_in))).as_expr(), Tactic('qe2').apply(Exists([clk_B1_in,clk_B1_out,hSpec1_B1_out,hSpec1_B1_in], And( clk_B1_out >= hSpec1_B1_in, hSpec1_B1_in >= 0, clk_B1_in == hSpec1_B1_in, clk_B1_out == hSpec1_B1_out))).as_expr(), Tactic('qe2').apply(Exists([clk_B1_in,clk_B1_out,hSpec1_B1_out,hSpec1_B1_in], And( clk_B1_in >= hSpec1_B1_out, hSpec1_B1_out >= 0, clk_B1_in == hSpec1_B1_in, clk_B1_out == hSpec1_B1_out))).as_expr(), Tactic('qe2').apply(Exists([clk_B1_in,clk_B1_out,hSpec1_B1_out,hSpec1_B1_in], And( clk_B1_in >= hSpec1_B1_out, hSpec1_B1_out >= 0, hSpec1_B1_out + 3 >= clk_B1_in, clk_B1_in == hSpec1_B1_in, clk_B1_out == hSpec1_B1_out))).as_expr())
[info] 
[info] 
[info] #abstract reach
[info] absReachII = Or(*(And(M0, R1_3, R2_4, C0, A3, S0), And(M3, R1_3, R2_0, C0, A0, S0), And(M0, R1_4, R2_5, C0, A1, S0), And(M0, R1_4, R2_3, C0, A0, S0), And(M4, R1_0, R2_2, C1, A0, S1), And(M1, R1_5, R2_5, C1, A1, S1), And(M3, R1_3, R2_3, C1, A0, S1), And(M0, R1_1, R2_3, C2, A3, S1), And(M3, R1_3, R2_3, C0, A3, S0), And(M3, R1_3, R2_3, C1, A3, S1), And(M0, R1_0, R2_3, C1, A0, S1), And(M4, R1_0, R2_2, C0, A3, S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M3, R1_0, R2_0, C1, A3, S1), And(M3, R1_1, R2_4, C2, A0, S1), And(M4, R1_2, R2_2, C2, A3, S0), And(M0, R1_4, R2_3, C1, A0, S1), And(M1, R1_5, R2_0, C0, A3, S0), And(M0, R1_3, R2_5, C1, A1, S1), And(M2, R1_5, R2_4, C0, A3, S0), And(M0, R1_2, R2_5, C2, A2, S0), And(M3, R1_4, R2_5, C0, A1, S0), And(M0, R1_3, R2_0, C0, A3, S0), And(M0, R1_3, R2_4, C0, A0, S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M1, R1_5, R2_4, C0, A0, S0), And(M0, R1_0, R2_4, C1, A3, S1), And(M0, R1_4, R2_4, C1, A0, S1), And(M3, R1_2, R2_3, C2, A0, S0), And(M3, R1_4, R2_0, C0, A0, S0), And(M0, R1_4, R2_4, C0, A3, S0), And(M3, R1_0, R2_0, C0, A3, S0), And(M4, R1_4, R2_1, C1, A3, S1), And(M1, R1_5, R2_3, C0, A3, S0), And(M4, R1_3, R2_1, C1, A3, S1), And(M3, R1_4, R2_0, C0, A0, S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M3, R1_4, R2_5, C1, A2, S1), And(M0, R1_1, R2_4, C2, A0, S1), And(M4, R1_0, R2_1, C1, A3, S1), And(M4, R1_0, R2_1, C0, A0, S0), And(M1, R1_5, R2_4, C0, A0, S0), And(M0, R1_3, R2_5, C0, A2, S0), And(M0, R1_3, R2_3, C0, A0, S0), And(M0, R1_4, R2_0, C1, A3, S1), And(M3, R1_0, R2_0, C0, A3, S0), And(M2, R1_5, R2_3, C0, A0, S0), And(M2, R1_5, R2_5, C0, A2, S0), And(M3, R1_0, R2_0, C1, A0, S1), And(M0, R1_0, R2_5, C0, A1, S0), And(M4, R1_0, R2_2, C1, A3, S1), And(M0, R1_3, R2_0, C0, A3, S0), And(M1, R1_5, R2_0, C0, A3, S0), And(M0, R1_0, R2_0, C0, A0, S0), And(M1, R1_5, R2_3, C0, A3, S0), And(M3, R1_2, R2_5, C2, A2, S0), And(M3, R1_3, R2_4, C1, A0, S1), And(M3, R1_0, R2_0, C0, A0, S0), And(M2, R1_5, R2_0, C0, A3, S0), And(M1, R1_5, R2_5, C0, A2, S0), And(M0, R1_4, R2_5, C1, A2, S1), And(M0, R1_4, R2_0, C0, A3, S0), And(M0, R1_1, R2_0, C2, A0, S1), And(M0, R1_1, R2_4, C2, A0, S1), And(M3, R1_4, R2_0, C1, A0, S1), And(M0, R1_0, R2_4, C0, A3, S0), And(M0, R1_4, R2_5, C0, A1, S0), And(M3, R1_4, R2_3, C0, A3, S0), And(M2, R1_5, R2_4, C0, A0, S0), And(M0, R1_1, R2_4, C2, A3, S1), And(M4, R1_0, R2_1, C0, A3, S0), And(M3, R1_0, R2_5, C1, A1, S1), And(M3, R1_0, R2_0, C1, A3, S1), And(M3, R1_1, R2_3, C2, A0, S1), And(M0, R1_0, R2_5, C0, A2, S0), And(M4, R1_2, R2_2, C2, A0, S0), And(M0, R1_0, R2_4, C1, A3, S1), And(M3, R1_2, R2_5, C2, A2, S0), And(M1, R1_5, R2_4, C1, A3, S1), And(M3, R1_2, R2_3, C2, A3, S0), And(M4, R1_0, R2_1, C0, A3, S0), And(M0, R1_0, R2_3, C0, A3, S0), And(M0, R1_4, R2_3, C1, A3, S1), And(M0, R1_2, R2_4, C2, A0, S0), And(M3, R1_0, R2_3, C0, A3, S0), And(M4, R1_4, R2_2, C1, A3, S1), And(M0, R1_0, R2_3, C1, A3, S1), And(M3, R1_3, R2_0, C0, A0, S0), And(M2, R1_5, R2_3, C1, A0, S1), And(M0, R1_4, R2_5, C0, A1, S0), And(M0, R1_3, R2_0, C1, A3, S1), And(M1, R1_5, R2_3, C1, A0, S1), And(M3, R1_0, R2_3, C0, A3, S0), And(M2, R1_5, R2_5, C0, A1, S0), And(M1, R1_5, R2_3, C1, A0, S1), And(M0, R1_4, R2_0, C1, A3, S1), And(M3, R1_1, R2_5, C2, A1, S1), And(M4, R1_2, R2_1, C2, A0, S0), And(M3, R1_0, R2_0, C0, A0, S0), And(M0, R1_0, R2_3, C0, A0, S0), And(M0, R1_0, R2_4, C0, A0, S0), And(M0, R1_3, R2_3, C1, A0, S1), And(M3, R1_3, R2_3, C1, A3, S1), And(M4, R1_4, R2_1, C0, A3, S0), And(M0, R1_0, R2_3, C1, A0, S1), And(M2, R1_5, R2_5, C1, A1, S1), And(M3, R1_1, R2_0, C2, A0, S1), And(M0, R1_4, R2_5, C0, A2, S0), And(M3, R1_4, R2_3, C1, A0, S1), And(M0, R1_0, R2_5, C1, A1, S1), And(M3, R1_3, R2_3, C0, A0, S0), And(M0, R1_2, R2_3, C2, A0, S0), And(M3, R1_3, R2_5, C1, A1, S1), And(M1, R1_5, R2_3, C0, A0, S0), And(M3, R1_1, R2_3, C2, A3, S1), And(M3, R1_2, R2_4, C2, A0, S0), And(M0, R1_0, R2_0, C1, A3, S1), And(M4, R1_4, R2_1, C0, A3, S0), And(M0, R1_4, R2_3, C1, A3, S1), And(M3, R1_4, R2_4, C0, A3, S0), And(M4, R1_3, R2_1, C1, A3, S1), And(M3, R1_3, R2_0, C0, A0, S0), And(M4, R1_2, R2_2, C2, A3, S0), And(M0, R1_2, R2_5, C2, A1, S0), And(M0, R1_3, R2_3, C1, A3, S1), And(M0, R1_0, R2_4, C1, A0, S1), And(M2, R1_5, R2_3, C0, A0, S0), And(M1, R1_5, R2_4, C0, A3, S0), And(M0, R1_3, R2_3, C0, A0, S0), And(M3, R1_2, R2_3, C2, A0, S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M4, R1_1, R2_2, C2, A0, S1), And(M3, R1_3, R2_4, C1, A0, S1), And(M3, R1_4, R2_3, C0, A0, S0), And(M0, R1_0, R2_5, C1, A2, S1), And(M0, R1_3, R2_3, C0, A3, S0), And(M2, R1_5, R2_0, C1, A3, S1), And(M0, R1_3, R2_3, C0, A0, S0), And(M0, R1_4, R2_5, C0, A2, S0), And(M0, R1_2, R2_4, C2, A3, S0), And(M3, R1_0, R2_5, C1, A1, S1), And(M0, R1_1, R2_5, C2, A2, S1), And(M4, R1_4, R2_2, C0, A3, S0), And(M2, R1_5, R2_5, C1, A1, S1), And(M4, R1_3, R2_1, C0, A0, S0), And(M0, R1_2, R2_5, C2, A2, S0), And(M1, R1_5, R2_5, C0, A1, S0), And(M0, R1_2, R2_0, C2, A0, S0), And(M0, R1_4, R2_3, C1, A0, S1), And(M0, R1_4, R2_4, C0, A3, S0), And(M0, R1_2, R2_0, C2, A3, S0), And(M3, R1_0, R2_4, C0, A0, S0), And(M4, R1_4, R2_2, C0, A3, S0), And(M0, R1_3, R2_4, C1, A3, S1), And(M3, R1_4, R2_4, C1, A0, S1), And(M0, R1_1, R2_5, C2, A2, S1), And(M0, R1_0, R2_5, C1, A2, S1), And(M0, R1_3, R2_3, C1, A0, S1), And(M2, R1_5, R2_3, C1, A0, S1), And(M0, R1_3, R2_0, C0, A0, S0), And(M0, R1_3, R2_0, C0, A3, S0), And(M2, R1_5, R2_3, C0, A3, S0), And(M4, R1_2, R2_1, C2, A0, S0), And(M4, R1_4, R2_1, C1, A0, S1), And(M0, R1_4, R2_4, C1, A3, S1), And(M3, R1_0, R2_4, C1, A0, S1), And(M2, R1_5, R2_4, C0, A0, S0), And(M4, R1_1, R2_1, C2, A3, S1), And(M0, R1_1, R2_5, C2, A1, S1), And(M2, R1_5, R2_4, C1, A0, S1), And(M0, R1_4, R2_3, C1, A3, S1), And(M1, R1_5, R2_4, C1, A3, S1), And(M3, R1_2, R2_3, C2, A3, S0), And(M0, R1_4, R2_5, C0, A1, S0), And(M3, R1_0, R2_5, C1, A2, S1), And(M3, R1_3, R2_5, C0, A1, S0), And(M3, R1_3, R2_4, C1, A3, S1), And(M3, R1_1, R2_0, C2, A3, S1), And(M0, R1_3, R2_0, C0, A0, S0), And(M3, R1_2, R2_0, C2, A0, S0), And(M3, R1_2, R2_0, C2, A3, S0), And(M0, R1_0, R2_3, C1, A3, S1), And(M0, R1_4, R2_3, C0, A0, S0), And(M3, R1_3, R2_3, C0, A0, S0), And(M3, R1_0, R2_5, C1, A2, S1), And(M3, R1_3, R2_4, C0, A3, S0), And(M1, R1_5, R2_0, C1, A3, S1), And(M2, R1_5, R2_0, C0, A3, S0), And(M0, R1_4, R2_0, C1, A0, S1), And(M0, R1_1, R2_5, C2, A2, S1), And(M0, R1_3, R2_3, C1, A3, S1), And(M3, R1_3, R2_5, C0, A1, S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M0, R1_3, R2_3, C1, A0, S1), And(M0, R1_0, R2_5, C1, A2, S1), And(M0, R1_2, R2_3, C2, A3, S0), And(M0, R1_1, R2_0, C2, A3, S1), And(M0, R1_2, R2_3, C2, A0, S0), And(M0, R1_3, R2_4, C0, A0, S0), And(M0, R1_2, R2_4, C2, A3, S0), And(M4, R1_0, R2_1, C1, A0, S1), And(M0, R1_1, R2_3, C2, A0, S1), And(M0, R1_3, R2_4, C1, A3, S1), And(M2, R1_5, R2_5, C0, A1, S0), And(M3, R1_3, R2_0, C0, A3, S0), And(M2, R1_5, R2_3, C1, A3, S1), And(M0, R1_4, R2_0, C0, A3, S0), And(M1, R1_5, R2_5, C1, A2, S1), And(M1, R1_5, R2_3, C1, A3, S1), And(M1, R1_5, R2_5, C1, A2, S1), And(M1, R1_5, R2_4, C0, A0, S0), And(M1, R1_5, R2_3, C0, A0, S0), And(M2, R1_5, R2_4, C1, A3, S1), And(M0, R1_1, R2_0, C2, A0, S1), And(M3, R1_3, R2_0, C0, A3, S0), And(M3, R1_4, R2_3, C0, A0, S0), And(M4, R1_0, R2_2, C0, A3, S0), And(M2, R1_5, R2_3, C0, A3, S0), And(M2, R1_5, R2_0, C0, A3, S0), And(M0, R1_1, R2_3, C2, A3, S1), And(M3, R1_3, R2_5, C0, A2, S0), And(M4, R1_0, R2_1, C0, A0, S0), And(M3, R1_1, R2_4, C2, A0, S1), And(M3, R1_1, R2_3, C2, A3, S1), And(M0, R1_3, R2_5, C0, A2, S0), And(M3, R1_4, R2_5, C1, A1, S1), And(M3, R1_0, R2_0, C1, A0, S1), And(M4, R1_4, R2_1, C0, A0, S0), And(M0, R1_0, R2_4, C1, A3, S1), And(M0, R1_4, R2_5, C0, A2, S0), And(M3, R1_3, R2_3, C1, A3, S1), And(M4, R1_3, R2_1, C0, A3, S0), And(M3, R1_3, R2_5, C0, A1, S0), And(M0, R1_4, R2_0, C0, A0, S0), And(M3, R1_0, R2_3, C0, A0, S0), And(M0, R1_3, R2_4, C1, A0, S1), And(M0, R1_1, R2_3, C2, A3, S1), And(M0, R1_0, R2_0, C1, A3, S1), And(M3, R1_3, R2_3, C0, A0, S0), And(M4, R1_3, R2_1, C1, A3, S1), And(M3, R1_4, R2_0, C1, A3, S1), And(M4, R1_0, R2_1, C1, A3, S1), And(M0, R1_3, R2_4, C1, A3, S1), And(M4, R1_3, R2_2, C0, A0, S0), And(M0, R1_4, R2_0, C0, A3, S0), And(M3, R1_0, R2_5, C0, A2, S0), And(M1, R1_5, R2_4, C0, A3, S0), And(M0, R1_3, R2_5, C0, A1, S0), And(M1, R1_5, R2_3, C0, A3, S0), And(M0, R1_0, R2_3, C1, A3, S1), And(M3, R1_0, R2_5, C0, A1, S0), And(M3, R1_1, R2_4, C2, A3, S1), And(M3, R1_3, R2_0, C1, A0, S1), And(M2, R1_5, R2_0, C0, A0, S0), And(M0, R1_4, R2_0, C0, A0, S0), And(M0, R1_1, R2_3, C2, A3, S1), And(M3, R1_4, R2_5, C0, A2, S0), And(M0, R1_4, R2_4, C1, A0, S1), And(M0, R1_3, R2_0, C1, A3, S1), And(M0, R1_2, R2_0, C2, A3, S0), And(M0, R1_2, R2_3, C2, A3, S0), And(M3, R1_1, R2_5, C2, A1, S1), And(M3, R1_3, R2_4, C0, A0, S0), And(M4, R1_0, R2_1, C1, A0, S1), And(M3, R1_4, R2_3, C0, A3, S0), And(M0, R1_0, R2_0, C0, A3, S0), And(M0, R1_1, R2_4, C2, A3, S1), And(M3, R1_3, R2_5, C0, A2, S0), And(M0, R1_3, R2_3, C0, A3, S0), And(M0, R1_1, R2_0, C2, A3, S1), And(M0, R1_4, R2_3, C1, A3, S1), And(M4, R1_4, R2_1, C0, A3, S0), And(M2, R1_5, R2_4, C1, A0, S1), And(M3, R1_2, R2_3, C2, A3, S0), And(M0, R1_4, R2_4, C1, A3, S1), And(M0, R1_4, R2_5, C1, A1, S1), And(M4, R1_2, R2_1, C2, A3, S0), And(M3, R1_1, R2_5, C2, A2, S1), And(M3, R1_1, R2_3, C2, A3, S1), And(M4, R1_4, R2_1, C0, A0, S0), And(M3, R1_3, R2_0, C1, A0, S1), And(M0, R1_4, R2_0, C0, A0, S0), And(M3, R1_4, R2_4, C1, A3, S1), And(M2, R1_5, R2_5, C0, A2, S0), And(M0, R1_0, R2_0, C0, A3, S0), And(M0, R1_4, R2_0, C1, A3, S1), And(M2, R1_5, R2_5, C0, A1, S0), And(M0, R1_3, R2_3, C1, A3, S1), And(M0, R1_4, R2_5, C1, A1, S1), And(M3, R1_0, R2_3, C1, A0, S1), And(M0, R1_4, R2_4, C1, A0, S1), And(M4, R1_4, R2_2, C1, A3, S1), And(M4, R1_1, R2_2, C2, A0, S1), And(M3, R1_0, R2_3, C0, A3, S0), And(M3, R1_2, R2_5, C2, A1, S0), And(M0, R1_0, R2_5, C0, A1, S0), And(M0, R1_3, R2_3, C1, A3, S1), And(M0, R1_0, R2_3, C0, A0, S0), And(M2, R1_5, R2_5, C0, A2, S0), And(M0, R1_1, R2_5, C2, A1, S1), And(M0, R1_2, R2_0, C2, A0, S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M1, R1_5, R2_5, C1, A1, S1), And(M2, R1_5, R2_3, C0, A3, S0), And(M3, R1_0, R2_0, C1, A3, S1), And(M3, R1_4, R2_0, C0, A3, S0), And(M0, R1_3, R2_4, C0, A3, S0), And(M3, R1_2, R2_0, C2, A0, S0), And(M0, R1_0, R2_5, C0, A2, S0), And(M4, R1_3, R2_2, C1, A3, S1), And(M3, R1_0, R2_4, C1, A0, S1), And(M0, R1_3, R2_5, C0, A2, S0), And(M0, R1_3, R2_4, C0, A3, S0), And(M0, R1_4, R2_5, C1, A2, S1), And(M4, R1_3, R2_1, C0, A0, S0), And(M0, R1_2, R2_5, C2, A1, S0), And(M0, R1_3, R2_5, C1, A1, S1), And(M4, R1_2, R2_2, C2, A0, S0), And(M0, R1_3, R2_3, C0, A3, S0), And(M3, R1_4, R2_3, C1, A3, S1), And(M0, R1_4, R2_3, C0, A0, S0), And(M0, R1_2, R2_3, C2, A3, S0), And(M3, R1_3, R2_0, C1, A3, S1), And(M0, R1_0, R2_5, C0, A1, S0), And(M4, R1_0, R2_2, C1, A3, S1), And(M0, R1_1, R2_0, C2, A3, S1), And(M4, R1_2, R2_1, C2, A3, S0), And(M2, R1_5, R2_4, C1, A3, S1), And(M3, R1_3, R2_3, C0, A3, S0), And(M1, R1_5, R2_5, C0, A2, S0), And(M0, R1_3, R2_0, C1, A0, S1), And(M0, R1_3, R2_0, C0, A3, S0), And(M0, R1_4, R2_4, C0, A0, S0), And(M4, R1_1, R2_2, C2, A3, S1), And(M1, R1_5, R2_4, C1, A0, S1), And(M3, R1_1, R2_0, C2, A3, S1), And(M4, R1_3, R2_2, C1, A0, S1), And(M4, R1_0, R2_1, C1, A3, S1), And(M0, R1_4, R2_4, C0, A0, S0), And(M0, R1_0, R2_4, C0, A0, S0), And(M2, R1_5, R2_5, C1, A2, S1), And(M0, R1_0, R2_3, C0, A3, S0), And(M0, R1_0, R2_0, C0, A3, S0), And(M4, R1_0, R2_2, C1, A3, S1), And(M0, R1_4, R2_4, C1, A3, S1), And(M0, R1_0, R2_5, C1, A1, S1), And(M4, R1_4, R2_1, C1, A3, S1), And(M3, R1_2, R2_0, C2, A3, S0), And(M0, R1_3, R2_5, C1, A2, S1), And(M4, R1_3, R2_2, C1, A0, S1), And(M4, R1_1, R2_1, C2, A0, S1), And(M3, R1_4, R2_3, C0, A3, S0), And(M0, R1_0, R2_4, C0, A3, S0), And(M2, R1_5, R2_3, C0, A3, S0), And(M0, R1_0, R2_3, C1, A0, S1), And(M3, R1_3, R2_4, C0, A0, S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M0, R1_4, R2_5, C1, A1, S1), And(M4, R1_0, R2_1, C0, A3, S0), And(M3, R1_0, R2_5, C0, A1, S0), And(M0, R1_0, R2_3, C0, A0, S0), And(M0, R1_2, R2_5, C2, A2, S0), And(M0, R1_3, R2_3, C0, A3, S0), And(M0, R1_0, R2_0, C1, A0, S1), And(M3, R1_0, R2_4, C0, A3, S0), And(M3, R1_1, R2_0, C2, A3, S1), And(M4, R1_3, R2_1, C0, A3, S0), And(M1, R1_5, R2_4, C0, A3, S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M3, R1_4, R2_4, C0, A0, S0), And(M2, R1_5, R2_0, C0, A0, S0), And(M3, R1_3, R2_3, C0, A3, S0), And(M4, R1_3, R2_2, C1, A3, S1), And(M0, R1_0, R2_5, C0, A2, S0), And(M0, R1_4, R2_4, C0, A3, S0), And(M4, R1_1, R2_1, C2, A0, S1), And(M3, R1_0, R2_3, C0, A0, S0), And(M3, R1_0, R2_4, C1, A3, S1), And(M1, R1_5, R2_3, C0, A3, S0), And(M1, R1_5, R2_3, C0, A0, S0), And(M2, R1_5, R2_0, C1, A0, S1), And(M0, R1_1, R2_4, C2, A0, S1), And(M0, R1_4, R2_0, C0, A3, S0), And(M3, R1_2, R2_4, C2, A3, S0), And(M0, R1_2, R2_3, C2, A0, S0), And(M0, R1_2, R2_5, C2, A1, S0), And(M0, R1_3, R2_5, C0, A2, S0), And(M1, R1_5, R2_0, C0, A0, S0), And(M3, R1_1, R2_3, C2, A0, S1), And(M0, R1_0, R2_3, C1, A3, S1), And(M0, R1_2, R2_4, C2, A0, S0), And(M3, R1_3, R2_5, C1, A2, S1), And(M0, R1_4, R2_5, C0, A2, S0), And(M4, R1_3, R2_2, C0, A0, S0), And(M3, R1_4, R2_5, C0, A2, S0), And(M1, R1_5, R2_4, C1, A0, S1), And(M3, R1_3, R2_5, C0, A2, S0), And(M0, R1_3, R2_4, C1, A0, S1), And(M0, R1_0, R2_0, C1, A3, S1), And(M0, R1_0, R2_0, C1, A0, S1), And(M4, R1_3, R2_1, C0, A3, S0), And(M0, R1_2, R2_3, C2, A3, S0), And(M3, R1_3, R2_3, C0, A3, S0), And(M0, R1_0, R2_4, C0, A0, S0), And(M1, R1_5, R2_0, C0, A0, S0), And(M4, R1_3, R2_1, C1, A0, S1), And(M3, R1_0, R2_0, C0, A3, S0), And(M3, R1_4, R2_4, C0, A0, S0), And(M1, R1_5, R2_0, C1, A3, S1), And(M3, R1_2, R2_4, C2, A3, S0), And(M0, R1_2, R2_4, C2, A3, S0), And(M1, R1_5, R2_5, C0, A1, S0), And(M3, R1_1, R2_5, C2, A2, S1), And(M3, R1_0, R2_3, C1, A3, S1), And(M3, R1_2, R2_4, C2, A0, S0), And(M0, R1_0, R2_3, C0, A3, S0), And(M3, R1_0, R2_4, C1, A3, S1), And(M1, R1_5, R2_5, C0, A2, S0), And(M3, R1_3, R2_4, C0, A3, S0), And(M2, R1_5, R2_0, C1, A3, S1), And(M0, R1_4, R2_4, C0, A3, S0), And(M0, R1_2, R2_4, C2, A0, S0), And(M0, R1_1, R2_3, C2, A0, S1), And(M4, R1_2, R2_1, C2, A3, S0), And(M0, R1_3, R2_5, C1, A1, S1), And(M0, R1_0, R2_4, C0, A3, S0), And(M4, R1_3, R2_1, C0, A0, S0), And(M3, R1_2, R2_5, C2, A1, S0), And(M3, R1_0, R2_4, C0, A3, S0), And(M0, R1_4, R2_0, C1, A0, S1), And(M0, R1_3, R2_4, C0, A3, S0), And(M0, R1_4, R2_4, C0, A0, S0), And(M4, R1_0, R2_2, C0, A0, S0), And(M0, R1_3, R2_5, C1, A2, S1), And(M2, R1_5, R2_4, C0, A3, S0), And(M4, R1_0, R2_2, C0, A3, S0), And(M3, R1_4, R2_0, C0, A3, S0), And(M4, R1_1, R2_1, C2, A3, S1), And(M3, R1_0, R2_3, C1, A0, S1), And(M3, R1_4, R2_0, C0, A3, S0), And(M3, R1_4, R2_5, C0, A1, S0), And(M3, R1_3, R2_0, C1, A3, S1), And(M1, R1_5, R2_5, C0, A1, S0), And(M0, R1_3, R2_5, C0, A1, S0), And(M0, R1_3, R2_0, C1, A0, S1), And(M2, R1_5, R2_4, C0, A3, S0), And(M3, R1_3, R2_0, C1, A3, S1), And(M4, R1_4, R2_2, C0, A0, S0), And(M0, R1_4, R2_4, C0, A0, S0), And(M4, R1_3, R2_2, C1, A3, S1), And(M3, R1_2, R2_0, C2, A3, S0), And(M3, R1_4, R2_0, C1, A3, S1), And(M4, R1_2, R2_2, C2, A3, S0), And(M0, R1_3, R2_0, C0, A0, S0), And(M0, R1_4, R2_3, C1, A0, S1), And(M2, R1_5, R2_3, C1, A3, S1), And(M2, R1_5, R2_3, C0, A0, S0), And(M4, R1_3, R2_1, C0, A3, S0), And(M4, R1_4, R2_2, C1, A0, S1), And(M1, R1_5, R2_3, C1, A3, S1), And(M0, R1_3, R2_4, C0, A0, S0), And(M2, R1_5, R2_3, C1, A3, S1), And(M0, R1_1, R2_3, C2, A0, S1), And(M2, R1_5, R2_4, C0, A0, S0), And(M4, R1_1, R2_2, C2, A3, S1), And(M3, R1_0, R2_5, C0, A2, S0), And(M1, R1_5, R2_0, C1, A0, S1), And(M1, R1_5, R2_0, C0, A3, S0), And(M3, R1_3, R2_4, C0, A3, S0), And(M0, R1_3, R2_5, C0, A1, S0), And(M0, R1_4, R2_5, C1, A2, S1), And(M3, R1_3, R2_4, C0, A0, S0), And(M4, R1_1, R2_1, C2, A3, S1), And(M0, R1_3, R2_3, C0, A0, S0), And(M0, R1_3, R2_0, C1, A3, S1), And(M3, R1_3, R2_4, C1, A3, S1), And(M4, R1_4, R2_2, C0, A0, S0), And(M4, R1_0, R2_2, C0, A0, S0), And(M3, R1_4, R2_4, C0, A3, S0), And(M0, R1_3, R2_4, C1, A0, S1), And(M2, R1_5, R2_5, C1, A2, S1), And(M4, R1_0, R2_2, C1, A0, S1), And(M3, R1_3, R2_5, C1, A2, S1), And(M0, R1_2, R2_0, C2, A3, S0), And(M4, R1_3, R2_1, C1, A0, S1), And(M0, R1_3, R2_5, C0, A1, S0), And(M3, R1_4, R2_3, C1, A3, S1), And(M3, R1_0, R2_3, C1, A3, S1), And(M4, R1_3, R2_2, C0, A0, S0), And(M1, R1_5, R2_3, C1, A3, S1), And(M0, R1_0, R2_4, C1, A0, S1), And(M0, R1_1, R2_5, C2, A1, S1), And(M0, R1_3, R2_4, C0, A0, S0), And(M3, R1_0, R2_4, C0, A0, S0), And(M3, R1_0, R2_3, C1, A3, S1), And(M3, R1_3, R2_3, C1, A0, S1), And(M0, R1_0, R2_5, C1, A1, S1), And(M0, R1_4, R2_3, C0, A3, S0), And(M0, R1_3, R2_5, C1, A2, S1), And(M3, R1_3, R2_0, C0, A3, S0), And(M0, R1_3, R2_3, C0, A3, S0), And(M3, R1_1, R2_4, C2, A3, S1), And(M0, R1_0, R2_4, C1, A0, S1), And(M4, R1_4, R2_2, C0, A3, S0), And(M0, R1_0, R2_0, C0, A0, S0), And(M0, R1_1, R2_4, C2, A3, S1), And(M4, R1_1, R2_2, C2, A3, S1), And(M0, R1_0, R2_3, C0, A3, S0), And(M3, R1_3, R2_0, C0, A3, S0), And(M0, R1_4, R2_3, C0, A0, S0), And(M3, R1_1, R2_0, C2, A0, S1), And(M3, R1_3, R2_5, C1, A1, S1))) 
[info] 
[info] #Enabled guided by absReach
[info] En = Or(*(And(M0,R1_3,R2_4,C0,A3,S0), And(M3, R1_3, R2_0, C0, A0, S0), And(M0,R1_4,R2_5,C0,A1,S0), And(M0, R1_4, R2_3, C0, A0, S0), And(M4, R1_0, R2_2, C1, A0, S1), And(M1,R1_5,R2_5,C1,A1,S1), And(M3,R1_3,R2_3,C1,A0,S1), And(M0,R1_1,R2_3,C2,A3,S1), And(M3,R1_3,R2_3,C0,A3,S0), And(M3,R1_3,R2_3,C1,A3,S1), And(M0,R1_0,R2_3,C1,A0,S1), And(M4,R1_0,R2_2,C0,A3,S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M3, R1_0, R2_0, C1, A3, S1), And(M3, R1_1, R2_4, C2, A0, S1), And(M4, R1_2, R2_2, C2, A3, S0), And(M0, R1_4, R2_3, C1, A0, S1), And(M1, R1_5, R2_0, C0, A3, S0), And(M0,R1_3,R2_5,C1,A1,S1), And(M2,R1_5,R2_4,C0,A3,S0), And(M0, R1_2, R2_5, C2, A2, S0), And(M3, R1_4, R2_5, C0, A1, S0), And(M0,R1_3,R2_0,C0,A3,S0), And(M0, R1_3, R2_4, C0, A0, S0), And(M4,R1_3,R2_2,C0,A3,S0), And(M1,R1_5,R2_4,C0,A0,S0), And(M0,R1_0,R2_4,C1,A3,S1), And(M0, R1_4, R2_4, C1, A0, S1), And(M3, R1_2, R2_3, C2, A0, S0), And(M3, R1_4, R2_0, C0, A0, S0), And(M0, R1_4, R2_4, C0, A3, S0), And(M3,R1_0,R2_0,C0,A3,S0), And(M4,R1_4,R2_1,C1,A3,S1), And(M1,R1_5,R2_3,C0,A3,S0), And(M4,R1_3,R2_1,C1,A3,S1), And(M3, R1_4, R2_0, C0, A0, S0), And(M0,R1_4,R2_3,C0,A3,S0), And(M3, R1_4, R2_5, C1, A2, S1), And(M0,R1_1,R2_4,C2,A0,S1), And(M4,R1_0,R2_1,C1,A3,S1), And(M4, R1_0, R2_1, C0, A0, S0), And(M1, R1_5, R2_4, C0, A0, S0), And(M0,R1_3,R2_5,C0,A2,S0), And(M0,R1_3,R2_3,C0,A0,S0), And(M0,R1_4,R2_0,C1,A3,S1), And(M3, R1_0, R2_0, C0, A3, S0), And(M2, R1_5, R2_3, C0, A0, S0), And(M2, R1_5, R2_5, C0, A2, S0), And(M3, R1_0, R2_0, C1, A0, S1), And(M0, R1_0, R2_5, C0, A1, S0), And(M4, R1_0, R2_2, C1, A3, S1), And(M0,R1_3,R2_0,C0,A3,S0), And(M1,R1_5,R2_0,C0,A3,S0), And(M0,R1_0,R2_0,C0,A0,S0), And(M1,R1_5,R2_3,C0,A3,S0), And(M3, R1_2, R2_5, C2, A2, S0), And(M3, R1_3, R2_4, C1, A0, S1), And(M3, R1_0, R2_0, C0, A0, S0), And(M2, R1_5, R2_0, C0, A3, S0), And(M1, R1_5, R2_5, C0, A2, S0), And(M0, R1_4, R2_5, C1, A2, S1), And(M0,R1_4,R2_0,C0,A3,S0), And(M0,R1_1,R2_0,C2,A0,S1), And(M0, R1_1, R2_4, C2, A0, S1), And(M3, R1_4, R2_0, C1, A0, S1), And(M0,R1_0,R2_4,C0,A3,S0), And(M0, R1_4, R2_5, C0, A1, S0), And(M3, R1_4, R2_3, C0, A3, S0), And(M2, R1_5, R2_4, C0, A0, S0), And(And(M0, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M4, R1_0, R2_1, C0, A3, S0), And(M3,R1_0,R2_5,C1,A1,S1), And(M3,R1_0,R2_0,C1,A3,S1), And(And(M3, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M0,R1_0,R2_5,C0,A2,S0), And(M4, R1_2, R2_2, C2, A0, S0), And(M0, R1_0, R2_4, C1, A3, S1), And(M3, R1_2, R2_5, C2, A2, S0), And(M1,R1_5,R2_4,C1,A3,S1), And(M3, R1_2, R2_3, C2, A3, S0), And(M4,R1_0,R2_1,C0,A3,S0), And(M0,R1_0,R2_3,C0,A3,S0), And(M0, R1_4, R2_3, C1, A3, S1), And(M0, R1_2, R2_4, C2, A0, S0), And(M3,R1_0,R2_3,C0,A3,S0), And(M4,R1_4,R2_2,C1,A3,S1), And(M0, R1_0, R2_3, C1, A3, S1), And(M3, R1_3, R2_0, C0, A0, S0), And(M2, R1_5, R2_3, C1, A0, S1), And(M0,R1_4,R2_5,C0,A1,S0), And(M0,R1_3,R2_0,C1,A3,S1), And(M1,R1_5,R2_3,C1,A0,S1), And(M3,R1_0,R2_3,C0,A3,S0), And(M2, R1_5, R2_5, C0, A1, S0), And(M1,R1_5,R2_3,C1,A0,S1), And(M0,R1_4,R2_0,C1,A3,S1), And(And(M3, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1)), And(M4, R1_2, R2_1, C2, A0, S0), And(M3, R1_0, R2_0, C0, A0, S0), And(M0, R1_0, R2_3, C0, A0, S0), And(M0, R1_0, R2_4, C0, A0, S0), And(M0,R1_3,R2_3,C1,A0,S1), And(M3,R1_3,R2_3,C1,A3,S1), And(M4,R1_4,R2_1,C0,A3,S0), And(M0, R1_0, R2_3, C1, A0, S1), And(M2, R1_5, R2_5, C1, A1, S1), And(And(M3, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M0, R1_4, R2_5, C0, A2, S0), And(M3,R1_4,R2_3,C1,A0,S1), And(M0,R1_0,R2_5,C1,A1,S1), And(M3, R1_3, R2_3, C0, A0, S0), And(M0, R1_2, R2_3, C2, A0, S0), And(M3,R1_3,R2_5,C1,A1,S1), And(M1,R1_5,R2_3,C0,A0,S0), And(M3,R1_1,R2_3,C2,A3,S1), And(M3, R1_2, R2_4, C2, A0, S0), And(M0, R1_0, R2_0, C1, A3, S1), And(M4, R1_4, R2_1, C0, A3, S0), And(M0,R1_4,R2_3,C1,A3,S1), And(M3, R1_4, R2_4, C0, A3, S0), And(M4,R1_3,R2_1,C1,A3,S1), And(M3,R1_3,R2_0,C0,A0,S0), And(M4, R1_2, R2_2, C2, A3, S0), And(M0,R1_2,R2_5,C2,A1,S0), And(M0,R1_3,R2_3,C1,A3,S1), And(M0, R1_0, R2_4, C1, A0, S1), And(M2,R1_5,R2_3,C0,A0,S0), And(M1, R1_5, R2_4, C0, A3, S0), And(M0,R1_3,R2_3,C0,A0,S0), And(M3,R1_2,R2_3,C2,A0,S0), And(M0,R1_4,R2_3,C0,A3,S0), And(And(M4, R1_1, R2_2, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_2, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M4, R1_1, R2_2, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_2, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M3,R1_3,R2_4,C1,A0,S1), And(M3,R1_4,R2_3,C0,A0,S0), And(M0,R1_0,R2_5,C1,A2,S1), And(M0,R1_3,R2_3,C0,A3,S0), And(M2, R1_5, R2_0, C1, A3, S1), And(M0, R1_3, R2_3, C0, A0, S0), And(M0, R1_4, R2_5, C0, A2, S0), And(M0,R1_2,R2_4,C2,A3,S0), And(M3, R1_0, R2_5, C1, A1, S1), And(M0,R1_1,R2_5,C2,A2,S1), And(M4,R1_4,R2_2,C0,A3,S0), And(M2,R1_5,R2_5,C1,A1,S1), And(M4, R1_3, R2_1, C0, A0, S0), And(M0,R1_2,R2_5,C2,A2,S0), And(M1, R1_5, R2_5, C0, A1, S0), And(M0, R1_2, R2_0, C2, A0, S0), And(M0,R1_4,R2_3,C1,A0,S1), And(M0,R1_4,R2_4,C0,A3,S0), And(M0,R1_2,R2_0,C2,A3,S0), And(M3, R1_0, R2_4, C0, A0, S0), And(M4, R1_4, R2_2, C0, A3, S0), And(M0,R1_3,R2_4,C1,A3,S1), And(M3, R1_4, R2_4, C1, A0, S1), And(And(M0, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1)), And(M0, R1_0, R2_5, C1, A2, S1), And(M0,R1_3,R2_3,C1,A0,S1), And(M2,R1_5,R2_3,C1,A0,S1), And(M0,R1_3,R2_0,C0,A0,S0), And(M0,R1_3,R2_0,C0,A3,S0), And(M2, R1_5, R2_3, C0, A3, S0), And(M4,R1_2,R2_1,C2,A0,S0), And(M4,R1_4,R2_1,C1,A0,S1), And(M0,R1_4,R2_4,C1,A3,S1), And(M3, R1_0, R2_4, C1, A0, S1), And(M2, R1_5, R2_4, C0, A0, S0), And(M4,R1_1,R2_1,C2,A3,S1), And(And(M0, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_5, C2, A1, S1, -clk_I_B1_C1 >= -1)), And(M2, R1_5, R2_4, C1, A0, S1), And(M0,R1_4,R2_3,C1,A3,S1), And(M1,R1_5,R2_4,C1,A3,S1), And(M3,R1_2,R2_3,C2,A3,S0), And(M0, R1_4, R2_5, C0, A1, S0), And(M3, R1_0, R2_5, C1, A2, S1), And(M3,R1_3,R2_5,C0,A1,S0), And(M3,R1_3,R2_4,C1,A3,S1), And(M3,R1_1,R2_0,C2,A3,S1), And(M0,R1_3,R2_0,C0,A0,S0), And(M3, R1_2, R2_0, C2, A0, S0), And(M3, R1_2, R2_0, C2, A3, S0), And(M0,R1_0,R2_3,C1,A3,S1), And(M0,R1_4,R2_3,C0,A0,S0), And(M3,R1_3,R2_3,C0,A0,S0), And(M3, R1_0, R2_5, C1, A2, S1), And(M3,R1_3,R2_4,C0,A3,S0), And(M1,R1_5,R2_0,C1,A3,S1), And(M2,R1_5,R2_0,C0,A3,S0), And(M0, R1_4, R2_0, C1, A0, S1), And(M0, R1_1, R2_5, C2, A2, S1), And(M0,R1_3,R2_3,C1,A3,S1), And(M3, R1_3, R2_5, C0, A1, S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M0,R1_3,R2_3,C1,A0,S1), And(M0, R1_0, R2_5, C1, A2, S1), And(M0,R1_2,R2_3,C2,A3,S0), And(M0,R1_1,R2_0,C2,A3,S1), And(M0,R1_2,R2_3,C2,A0,S0), And(M0,R1_3,R2_4,C0,A0,S0), And(M0,R1_2,R2_4,C2,A3,S0), And(M4,R1_0,R2_1,C1,A0,S1), And(M0,R1_1,R2_3,C2,A0,S1), And(M0,R1_3,R2_4,C1,A3,S1), And(M2,R1_5,R2_5,C0,A1,S0), And(M3,R1_3,R2_0,C0,A3,S0), And(M2,R1_5,R2_3,C1,A3,S1), And(M0, R1_4, R2_0, C0, A3, S0), And(M1,R1_5,R2_5,C1,A2,S1), And(M1,R1_5,R2_3,C1,A3,S1), And(M1, R1_5, R2_5, C1, A2, S1), And(M1, R1_5, R2_4, C0, A0, S0), And(M1, R1_5, R2_3, C0, A0, S0), And(M2, R1_5, R2_4, C1, A3, S1), And(And(M0, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_0, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M3, R1_3, R2_0, C0, A3, S0), And(M3, R1_4, R2_3, C0, A0, S0), And(M4, R1_0, R2_2, C0, A3, S0), And(M2, R1_5, R2_3, C0, A3, S0), And(M2, R1_5, R2_0, C0, A3, S0), And(M0,R1_1,R2_3,C2,A3,S1), And(M3, R1_3, R2_5, C0, A2, S0), And(M4,R1_0,R2_1,C0,A0,S0), And(And(M3, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(And(M3, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M0, R1_3, R2_5, C0, A2, S0), And(M3,R1_4,R2_5,C1,A1,S1), And(M3, R1_0, R2_0, C1, A0, S1), And(M4, R1_4, R2_1, C0, A0, S0), And(M0,R1_0,R2_4,C1,A3,S1), And(M0,R1_4,R2_5,C0,A2,S0), And(M3,R1_3,R2_3,C1,A3,S1), And(M4,R1_3,R2_1,C0,A3,S0), And(M3,R1_3,R2_5,C0,A1,S0), And(M0, R1_4, R2_0, C0, A0, S0), And(M3, R1_0, R2_3, C0, A0, S0), And(M0,R1_3,R2_4,C1,A0,S1), And(And(M0, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_3, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M0,R1_0,R2_0,C1,A3,S1), And(M3,R1_3,R2_3,C0,A0,S0), And(M4,R1_3,R2_1,C1,A3,S1), And(M3,R1_4,R2_0,C1,A3,S1), And(M4, R1_0, R2_1, C1, A3, S1), And(M0,R1_3,R2_4,C1,A3,S1), And(M4, R1_3, R2_2, C0, A0, S0), And(M0,R1_4,R2_0,C0,A3,S0), And(M3, R1_0, R2_5, C0, A2, S0), And(M1,R1_5,R2_4,C0,A3,S0), And(M0, R1_3, R2_5, C0, A1, S0), And(M1,R1_5,R2_3,C0,A3,S0), And(M0,R1_0,R2_3,C1,A3,S1), And(M3, R1_0, R2_5, C0, A1, S0), And(And(M3, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_4, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M3, R1_3, R2_0, C1, A0, S1), And(M2, R1_5, R2_0, C0, A0, S0), And(M0, R1_4, R2_0, C0, A0, S0), And(M0,R1_1,R2_3,C2,A3,S1), And(M3, R1_4, R2_5, C0, A2, S0), And(M0,R1_4,R2_4,C1,A0,S1), And(M0,R1_3,R2_0,C1,A3,S1), And(M0, R1_2, R2_0, C2, A3, S0), And(M0, R1_2, R2_3, C2, A3, S0), And(M3,R1_1,R2_5,C2,A1,S1), And(M3, R1_3, R2_4, C0, A0, S0), And(M4, R1_0, R2_1, C1, A0, S1), And(M3,R1_4,R2_3,C0,A3,S0), And(M0,R1_0,R2_0,C0,A3,S0), And(M0,R1_1,R2_4,C2,A3,S1), And(M3,R1_3,R2_5,C0,A2,S0), And(M0,R1_3,R2_3,C0,A3,S0), And(M0,R1_1,R2_0,C2,A3,S1), And(M0,R1_4,R2_3,C1,A3,S1), And(M4,R1_4,R2_1,C0,A3,S0), And(M2, R1_5, R2_4, C1, A0, S1), And(M3,R1_2,R2_3,C2,A3,S0), And(M0, R1_4, R2_4, C1, A3, S1), And(M0,R1_4,R2_5,C1,A1,S1), And(M4, R1_2, R2_1, C2, A3, S0), And(M3, R1_1, R2_5, C2, A2, S1), And(M3,R1_1,R2_3,C2,A3,S1), And(M4,R1_4,R2_1,C0,A0,S0), And(M3,R1_3,R2_0,C1,A0,S1), And(M0,R1_4,R2_0,C0,A0,S0), And(M3,R1_4,R2_4,C1,A3,S1), And(M2, R1_5, R2_5, C0, A2, S0), And(M0,R1_0,R2_0,C0,A3,S0), And(M0, R1_4, R2_0, C1, A3, S1), And(M2, R1_5, R2_5, C0, A1, S0), And(M0,R1_3,R2_3,C1,A3,S1), And(M0, R1_4, R2_5, C1, A1, S1), And(M3, R1_0, R2_3, C1, A0, S1), And(M0, R1_4, R2_4, C1, A0, S1), And(M4, R1_4, R2_2, C1, A3, S1), And(M4, R1_1, R2_2, C2, A0, S1), And(M3, R1_0, R2_3, C0, A3, S0), And(M3,R1_2,R2_5,C2,A1,S0), And(M0,R1_0,R2_5,C0,A1,S0), And(M0,R1_3,R2_3,C1,A3,S1), And(M0,R1_0,R2_3,C0,A0,S0), And(M2, R1_5, R2_5, C0, A2, S0), And(M0,R1_1,R2_5,C2,A1,S1), And(M0,R1_2,R2_0,C2,A0,S0), And(M0, R1_4, R2_3, C0, A3, S0), And(M1,R1_5,R2_5,C1,A1,S1), And(M2,R1_5,R2_3,C0,A3,S0), And(M3, R1_0, R2_0, C1, A3, S1), And(M3,R1_4,R2_0,C0,A3,S0), And(M0,R1_3,R2_4,C0,A3,S0), And(M3, R1_2, R2_0, C2, A0, S0), And(M0, R1_0, R2_5, C0, A2, S0), And(M4,R1_3,R2_2,C1,A3,S1), And(M3, R1_0, R2_4, C1, A0, S1), And(M0,R1_3,R2_5,C0,A2,S0), And(M0,R1_3,R2_4,C0,A3,S0), And(M0, R1_4, R2_5, C1, A2, S1), And(M4,R1_3,R2_1,C0,A0,S0), And(M0,R1_2,R2_5,C2,A1,S0), And(M0,R1_3,R2_5,C1,A1,S1), And(M4, R1_2, R2_2, C2, A0, S0), And(M0,R1_3,R2_3,C0,A3,S0), And(M3,R1_4,R2_3,C1,A3,S1), And(M0, R1_4, R2_3, C0, A0, S0), And(M0,R1_2,R2_3,C2,A3,S0), And(M3,R1_3,R2_0,C1,A3,S1), And(M0,R1_0,R2_5,C0,A1,S0), And(M4,R1_0,R2_2,C1,A3,S1), And(And(M0, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M4,R1_2,R2_1,C2,A3,S0), And(M2,R1_5,R2_4,C1,A3,S1), And(M3, R1_3, R2_3, C0, A3, S0), And(M1,R1_5,R2_5,C0,A2,S0), And(M0,R1_3,R2_0,C1,A0,S1), And(M0, R1_3, R2_0, C0, A3, S0), And(M0,R1_4,R2_4,C0,A0,S0), And(M4,R1_1,R2_2,C2,A3,S1), And(M1, R1_5, R2_4, C1, A0, S1), And(And(M3, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_0, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M4, R1_3, R2_2, C1, A0, S1), And(M4,R1_0,R2_1,C1,A3,S1), And(M0, R1_4, R2_4, C0, A0, S0), And(M0, R1_0, R2_4, C0, A0, S0), And(M2, R1_5, R2_5, C1, A2, S1), And(M0,R1_0,R2_3,C0,A3,S0), And(M0, R1_0, R2_0, C0, A3, S0), And(M4, R1_0, R2_2, C1, A3, S1), And(M0,R1_4,R2_4,C1,A3,S1), And(M0, R1_0, R2_5, C1, A1, S1), And(M4,R1_4,R2_1,C1,A3,S1), And(M3, R1_2, R2_0, C2, A3, S0), And(M0,R1_3,R2_5,C1,A2,S1), And(M4,R1_3,R2_2,C1,A0,S1), And(And(M4, R1_1, R2_1, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_1, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M4, R1_1, R2_1, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_1, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M3,R1_4,R2_3,C0,A3,S0), And(M0, R1_0, R2_4, C0, A3, S0), And(M2,R1_5,R2_3,C0,A3,S0), And(M0,R1_0,R2_3,C1,A0,S1), And(M3, R1_3, R2_4, C0, A0, S0), And(M4, R1_3, R2_2, C0, A3, S0), And(M0,R1_4,R2_5,C1,A1,S1), And(M4,R1_0,R2_1,C0,A3,S0), And(M3,R1_0,R2_5,C0,A1,S0), And(M0,R1_0,R2_3,C0,A0,S0), And(M0, R1_2, R2_5, C2, A2, S0), And(M0,R1_3,R2_3,C0,A3,S0), And(M0,R1_0,R2_0,C1,A0,S1), And(M3,R1_0,R2_4,C0,A3,S0), And(M3, R1_1, R2_0, C2, A3, S1), And(M4,R1_3,R2_1,C0,A3,S0), And(M1,R1_5,R2_4,C0,A3,S0), And(M4,R1_3,R2_2,C0,A3,S0), And(M3, R1_4, R2_4, C0, A0, S0), And(M2, R1_5, R2_0, C0, A0, S0), And(M3,R1_3,R2_3,C0,A3,S0), And(M4,R1_3,R2_2,C1,A3,S1), And(M0, R1_0, R2_5, C0, A2, S0), And(M0, R1_4, R2_4, C0, A3, S0), And(M4,R1_1,R2_1,C2,A0,S1), And(M3,R1_0,R2_3,C0,A0,S0), And(M3, R1_0, R2_4, C1, A3, S1), And(M1, R1_5, R2_3, C0, A3, S0), And(M1,R1_5,R2_3,C0,A0,S0), And(M2, R1_5, R2_0, C1, A0, S1), And(And(M0, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_4, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M0, R1_4, R2_0, C0, A3, S0), And(M3, R1_2, R2_4, C2, A3, S0), And(M0,R1_2,R2_3,C2,A0,S0), And(M0, R1_2, R2_5, C2, A1, S0), And(M0, R1_3, R2_5, C0, A2, S0), And(M1,R1_5,R2_0,C0,A0,S0), And(M3,R1_1,R2_3,C2,A0,S1), And(M0,R1_0,R2_3,C1,A3,S1), And(M0, R1_2, R2_4, C2, A0, S0), And(M3, R1_3, R2_5, C1, A2, S1), And(M0, R1_4, R2_5, C0, A2, S0), And(M4,R1_3,R2_2,C0,A0,S0), And(M3, R1_4, R2_5, C0, A2, S0), And(M1,R1_5,R2_4,C1,A0,S1), And(M3, R1_3, R2_5, C0, A2, S0), And(M0, R1_3, R2_4, C1, A0, S1), And(M0,R1_0,R2_0,C1,A3,S1), And(M0, R1_0, R2_0, C1, A0, S1), And(M4,R1_3,R2_1,C0,A3,S0), And(M0,R1_2,R2_3,C2,A3,S0), And(M3,R1_3,R2_3,C0,A3,S0), And(M0,R1_0,R2_4,C0,A0,S0), And(M1, R1_5, R2_0, C0, A0, S0), And(M4,R1_3,R2_1,C1,A0,S1), And(M3, R1_0, R2_0, C0, A3, S0), And(M3, R1_4, R2_4, C0, A0, S0), And(M1,R1_5,R2_0,C1,A3,S1), And(M3,R1_2,R2_4,C2,A3,S0), And(M0, R1_2, R2_4, C2, A3, S0), And(M1,R1_5,R2_5,C0,A1,S0), And(And(M3, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M3, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M3, R1_1, R2_5, C2, A2, S1, -clk_I_B1_C1 >= -1)), And(M3,R1_0,R2_3,C1,A3,S1), And(M3, R1_2, R2_4, C2, A0, S0), And(M0,R1_0,R2_3,C0,A3,S0), And(M3,R1_0,R2_4,C1,A3,S1), And(M1, R1_5, R2_5, C0, A2, S0), And(M3, R1_3, R2_4, C0, A3, S0), And(M2,R1_5,R2_0,C1,A3,S1), And(M0,R1_4,R2_4,C0,A3,S0), And(M0,R1_2,R2_4,C2,A0,S0), And(M0,R1_1,R2_3,C2,A0,S1), And(M4,R1_2,R2_1,C2,A3,S0), And(M0,R1_3,R2_5,C1,A1,S1), And(M0,R1_0,R2_4,C0,A3,S0), And(M4,R1_3,R2_1,C0,A0,S0), And(M3, R1_2, R2_5, C2, A1, S0), And(M3, R1_0, R2_4, C0, A3, S0), And(M0,R1_4,R2_0,C1,A0,S1), And(M0, R1_3, R2_4, C0, A3, S0), And(M0, R1_4, R2_4, C0, A0, S0), And(M4, R1_0, R2_2, C0, A0, S0), And(M0,R1_3,R2_5,C1,A2,S1), And(M2, R1_5, R2_4, C0, A3, S0), And(M4, R1_0, R2_2, C0, A3, S0), And(M3, R1_4, R2_0, C0, A3, S0), And(M4,R1_1,R2_1,C2,A3,S1), And(M3,R1_0,R2_3,C1,A0,S1), And(M3, R1_4, R2_0, C0, A3, S0), And(M3,R1_4,R2_5,C0,A1,S0), And(M3, R1_3, R2_0, C1, A3, S1), And(M1,R1_5,R2_5,C0,A1,S0), And(M0,R1_3,R2_5,C0,A1,S0), And(M0,R1_3,R2_0,C1,A0,S1), And(M2, R1_5, R2_4, C0, A3, S0), And(M3,R1_3,R2_0,C1,A3,S1), And(M4, R1_4, R2_2, C0, A0, S0), And(M0, R1_4, R2_4, C0, A0, S0), And(M4, R1_3, R2_2, C1, A3, S1), And(M3,R1_2,R2_0,C2,A3,S0), And(M3, R1_4, R2_0, C1, A3, S1), And(M4,R1_2,R2_2,C2,A3,S0), And(M0, R1_3, R2_0, C0, A0, S0), And(M0,R1_4,R2_3,C1,A0,S1), And(M2,R1_5,R2_3,C1,A3,S1), And(M2, R1_5, R2_3, C0, A0, S0), And(M4, R1_3, R2_1, C0, A3, S0), And(M4, R1_4, R2_2, C1, A0, S1), And(M1,R1_5,R2_3,C1,A3,S1), And(M0, R1_3, R2_4, C0, A0, S0), And(M2, R1_5, R2_3, C1, A3, S1), And(And(M0, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M0, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M0, R1_1, R2_3, C2, A0, S1, -clk_I_B1_C1 >= -1)), And(M2, R1_5, R2_4, C0, A0, S0), And(M4, R1_1, R2_2, C2, A3, S1), And(M3, R1_0, R2_5, C0, A2, S0), And(M1,R1_5,R2_0,C1,A0,S1), And(M1,R1_5,R2_0,C0,A3,S0), And(M3,R1_3,R2_4,C0,A3,S0), And(M0,R1_3,R2_5,C0,A1,S0), And(M0,R1_4,R2_5,C1,A2,S1), And(M3,R1_3,R2_4,C0,A0,S0), And(And(M4, R1_1, R2_1, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_1, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M4, R1_1, R2_1, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_1, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M0,R1_3,R2_3,C0,A0,S0), And(M0,R1_3,R2_0,C1,A3,S1), And(M3,R1_3,R2_4,C1,A3,S1), And(M4, R1_4, R2_2, C0, A0, S0), And(M4, R1_0, R2_2, C0, A0, S0), And(M3,R1_4,R2_4,C0,A3,S0), And(M0,R1_3,R2_4,C1,A0,S1), And(M2, R1_5, R2_5, C1, A2, S1), And(M4, R1_0, R2_2, C1, A0, S1), And(M3,R1_3,R2_5,C1,A2,S1), And(M0,R1_2,R2_0,C2,A3,S0), And(M4,R1_3,R2_1,C1,A0,S1), And(M0,R1_3,R2_5,C0,A1,S0), And(M3,R1_4,R2_3,C1,A3,S1), And(M3,R1_0,R2_3,C1,A3,S1), And(M4, R1_3, R2_2, C0, A0, S0), And(M1,R1_5,R2_3,C1,A3,S1), And(M0, R1_0, R2_4, C1, A0, S1), And(M0,R1_1,R2_5,C2,A1,S1), And(M0,R1_3,R2_4,C0,A0,S0), And(M3, R1_0, R2_4, C0, A0, S0), And(M3, R1_0, R2_3, C1, A3, S1), And(M3,R1_3,R2_3,C1,A0,S1), And(M0,R1_0,R2_5,C1,A1,S1), And(M0,R1_4,R2_3,C0,A3,S0), And(M0, R1_3, R2_5, C1, A2, S1), And(M3, R1_3, R2_0, C0, A3, S0), And(M0, R1_3, R2_3, C0, A3, S0), And(M3,R1_1,R2_4,C2,A3,S1), And(M0,R1_0,R2_4,C1,A0,S1), And(M4, R1_4, R2_2, C0, A3, S0), And(M0, R1_0, R2_0, C0, A0, S0), And(M0,R1_1,R2_4,C2,A3,S1), And(And(M4, R1_1, R2_2, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_2, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_B1_in >= -3), And(M4, R1_1, R2_2, C2, A3, S1, -clk_I_B1_C1 >= -1, -clk_I_B1_C1 + clk_B1_in > 2), And(M4, R1_1, R2_2, C2, A3, S1, -clk_I_B1_C1 >= -1)), And(M0, R1_0, R2_3, C0, A3, S0), And(M3,R1_3,R2_0,C0,A3,S0), And(M0,R1_4,R2_3,C0,A0,S0), And(M3, R1_1, R2_0, C2, A0, S1), And(M3,R1_3,R2_5,C1,A1,S1)))
[info] 
[info] DisN = Not(En)
[info] 
[info] #deltas = Map()
[info] [getEqsC]: imClks = Map(Set(Mill_O_B3_M, Robot1_O_B3_M) -> hMill_O_B3_MRobot1_O_B3_M, Set(Conveyor_B1_in, Spec1_B1_in) -> hConveyor_B1_inSpec1_B1_in, Set(Mill_O_B3_R2, Robot2_O_B3_R2) -> hMill_O_B3_R2Robot2_O_B3_R2, Set(Assembly_product) -> hAssembly_product, Set(Mill_B3_out_M) -> hMill_B3_out_M, Set(Assembly_O_B5_A, Robot2_O_B5_A) -> hAssembly_O_B5_ARobot2_O_B5_A, Set(Mill_I_B3_R1, Robot1_I_B3_R1) -> hMill_I_B3_R1Robot1_I_B3_R1, Set(Robot1_B3_in_R1) -> hRobot1_B3_in_R1, Set(Robot1_B1_out, Spec1_B1_out) -> hRobot1_B1_outSpec1_B1_out, Set(Assembly_B5_out_A) -> hAssembly_B5_out_A, Set(Robot2_B3_out_R2) -> hRobot2_B3_out_R2, Set(Conveyor_O_B1_R1, Robot1_O_B1_R1) -> hConveyor_O_B1_R1Robot1_O_B1_R1, Set(Mill_I_B3_M, Robot2_I_B3_M) -> hMill_I_B3_MRobot2_I_B3_M, Set(Robot2_B5_in_R2) -> hRobot2_B5_in_R2, Set(Assembly_I_B5_R2, Robot2_I_B5_R2) -> hAssembly_I_B5_R2Robot2_I_B5_R2, Set(Conveyor_I_B1_C1, Robot1_I_B1_C1) -> hConveyor_I_B1_C1Robot1_I_B1_C1, Set(Mill_B3_in_M) -> hMill_B3_in_M)
[info] [getEqsC]: ports = Set(Mill_B3_in_M, Assembly_B5_out_A, Assembly_I_B5_R2, Robot1_I_B1_C1, Robot1_O_B1_R1, Conveyor_B1_in, Robot2_B5_in_R2, Robot1_I_B3_R1, Robot1_B1_out, Conveyor_I_B1_C1, Mill_B3_out_M, Mill_O_B3_R2, Assembly_O_B5_A, Robot1_O_B3_M, Spec1_B1_out, Mill_O_B3_M, Robot2_I_B5_R2, Conveyor_O_B1_R1, Mill_I_B3_M, Robot2_O_B5_A, Mill_I_B3_R1, Robot2_O_B3_R2, Robot2_I_B3_M, Robot1_B3_in_R1, Assembly_product, Robot2_B3_out_R2, Spec1_B1_in)
[info] resultZ3 = 
[info] (runEFSMT: cmd = dependencies/./test  /home/etienne/git/efsmt_coverts/examples/Imitator/FMS1-outEF-59_2_2017
[info] 
[info] ,2)
[info] [error while executing EFSMT]: terminate called after throwing an instance of 'std::bad_alloc'  what():  std::bad_alloc. No results can be returned.
[success] Total time: 35 s, completed 21/02/17 13:43
efsmt_coverts>