# command line: # KaDE kin_phos_4.ka -print-efficiency -ode-backend DOTNET -with-symmetries Forward -dotnet-output network_kin_phos_4_with_fsym.net # THINGS THAT ARE KNOWN FROM KAPPA FILE AND KaSim OPTIONS: # # init - the initial abundances of each species and token # tinit - the initial simulation time (likely 0) # tend - the final simulation time # initialstep - initial time step at the beginning of numerical integration # maxstep - maximal time step for numerical integration # reltol - relative error tolerance; # abstol - absolute error tolerance; # period - the time period between points to return # # variables (init(i),y(i)) denote numbers of embeddings # rule rates are corrected by the number of automorphisms in the lhs of rules begin parameters 1 tinit 0 2 tend 1 3 period 0.01 4 Stot 100 5 kuS 0.01 6 kdPS 0.1 7 kPS 0.001 8 kpS 0.1 9 kdKS 1. 10 kKS 0.01 end parameters begin species 1 S(x1~u,x2~u,x3~u,x4~u) 100 2 P(s) 100 3 K(s) 100 4 K(s!1).S(x1~u,x2~u,x3~u,x4~u!1) 0 5 K(s!1).S(x1~u,x2~u,x3~u!2,x4~u!1).K(s!2) 0 6 S(x1~u,x2~u,x3~u,x4~p) 0 7 K(s!1).S(x1~u,x2~u,x3~u!1,x4~p) 0 8 S(x1~u,x2~u,x3~u,x4~p!1).P(s!1) 0 9 K(s!1).S(x1~u,x2~u,x3~u!1,x4~p!2).P(s!2) 0 10 K(s!1).S(x1~u,x2~u!2,x3~u!1,x4~p!3).P(s!3).K(s!2) 0 11 S(x1~u,x2~u,x3~p,x4~p!1).P(s!1) 0 12 K(s!1).S(x1~u,x2~u!1,x3~p,x4~p!2).P(s!2) 0 13 S(x1~u,x2~u,x3~p!1,x4~p!2).P(s!1).P(s!2) 0 14 S(x1~u,x2~u,x3~p,x4~p) 0 15 K(s!1).S(x1~u,x2~u!1,x3~p,x4~p) 0 16 K(s!1).S(x1~u!1,x2~u!2,x3~p,x4~p).K(s!2) 0 17 S(x1~u,x2~p,x3~p,x4~p) 0 18 K(s!1).S(x1~u!1,x2~p,x3~p,x4~p) 0 19 S(x1~u,x2~p,x3~p,x4~p!1).P(s!1) 0 20 K(s!1).S(x1~u!1,x2~p,x3~p,x4~p!2).P(s!2) 0 21 S(x1~u,x2~p,x3~p!1,x4~p!2).P(s!2).P(s!1) 0 22 K(s!1).S(x1~u!1,x2~p,x3~p!2,x4~p!3).P(s!3).P(s!2) 0 23 S(x1~u,x2~p!1,x3~p!2,x4~p!3).P(s!1).P(s!3).P(s!2) 0 24 K(s!1).S(x1~u!1,x2~p!2,x3~p!3,x4~p!4).P(s!4).P(s!3).P(s!2) 0 25 S(x1~p,x2~p!1,x3~p!2,x4~p!3).P(s!2).P(s!3).P(s!1) 0 26 K(s!1).S(x1~u,x2~u!1,x3~p!2,x4~p!3).P(s!3).P(s!2) 0 27 K(s!1).S(x1~u!1,x2~u!2,x3~p!3,x4~p!4).P(s!4).K(s!2).P(s!3) 0 28 K(s!1).S(x1~u!1,x2~u!2,x3~p,x4~p!3).P(s!3).K(s!2) 0 29 K(s!1).S(x1~u,x2~u!2,x3~u!1,x4~p).K(s!2) 0 30 K(s!1).S(x1~u!1,x2~u!2,x3~u!3,x4~p).K(s!3).K(s!2) 0 31 K(s!1).S(x1~u!1,x2~u!2,x3~u!3,x4~p!4).P(s!4).K(s!3).K(s!2) 0 32 K(s!1).S(x1~u,x2~u!2,x3~u!3,x4~u!1).K(s!3).K(s!2) 0 33 K(s!1).S(x1~u!1,x2~u!2,x3~u!3,x4~u!4).K(s!4).K(s!3).K(s!2) 0 34 S(x1~p!1,x2~p!2,x3~p!3,x4~p!4).P(s!1).P(s!4).P(s!3).P(s!2) 0 35 S(x1~p,x2~p,x3~p!1,x4~p!2).P(s!1).P(s!2) 0 36 S(x1~p,x2~p,x3~p,x4~p!1).P(s!1) 0 37 S(x1~p,x2~p,x3~p,x4~p) 0 end species begin reactions # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~p) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) 1 5 3,7 kpS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~u) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + K(s) 2 5 3,4 kdKS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) 3 5 3,7 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + K(s) 4 5 3,4 kdKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) 5 3,5 32 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) 6 3,5 32 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + P(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) 7 2,7 9 kPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) -> S(x1~u, x2~u, x3~p, x4~p) + K(s) 8 7 3,14 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) -> S(x1~u, x2~u, x3~u, x4~p) + K(s) 9 7 3,6 kdKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) 10 3,7 29 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) 11 3,7 29 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + P(s) 12 10 2,5 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + P(s) 13 10 2,29 kdPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + K(s) 14 10 3,12 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + K(s) 15 10 3,9 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + K(s) 16 10 3,12 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + K(s) 17 10 3,9 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) 18 3,10 31 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + P(s) 19 12 2,7 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + P(s) 20 12 2,15 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + P(s) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) 21 2,12 26 kPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + K(s) 22 12 3,19 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + K(s) 23 12 3,11 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) 24 3,12 28 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + P(s) 25 13 2,8 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + P(s) 26 13 2,11 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + P(s) 27 13 2,8 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + P(s) 28 13 2,11 kdPS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) 29 3,13 26 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) 30 3,13 26 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) 31 2,16 28 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) 32 2,16 28 kPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + K(s) 33 16 3,18 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + K(s) 34 16 3,15 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + K(s) 35 16 3,18 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + K(s) 36 16 3,15 kdKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + P(s) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) 37 2,18 20 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + P(s) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) 38 2,18 20 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + P(s) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) 39 2,18 20 kPS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) -> S(x1~p, x2~p, x3~p, x4~p) + K(s) 40 18 3,37 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) -> S(x1~u, x2~p, x3~p, x4~p) + K(s) 41 18 3,17 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + P(s) 42 20 2,15 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) + P(s) 43 20 2,18 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) 44 2,20 22 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) 45 2,20 22 kPS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + K(s) 46 20 3,36 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + K(s) 47 20 3,19 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + P(s) 48 22 2,12 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + P(s) 49 22 2,20 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + P(s) 50 22 2,12 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + P(s) 51 22 2,20 kdPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) 52 2,22 24 kPS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + K(s) 53 22 3,35 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + K(s) 54 22 3,21 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + P(s) 55 34 2,23 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + P(s) 56 34 2,25 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + P(s) 57 34 2,23 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + P(s) 58 34 2,25 kdPS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~u) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + P(s) 59 34 2,23 kuS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~p) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + P(s) 60 34 2,25 kdPS # rule : P(s!1), S(x1~p!1) -> P(s), S(x1~u) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + P(s) 61 34 2,23 kuS # rule : P(s!1), S(x1~p!1) -> P(s), S(x1~p) # S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + P(s) 62 34 2,25 kdPS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # S(x1~p, x2~p, x3~p, x4~p) + P(s) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) 63 2,37 36 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~p, x2~p, x3~p, x4~p) + P(s) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) 64 2,37 36 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~p, x2~p, x3~p, x4~p) + P(s) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) 65 2,37 36 kPS # rule : P(s), S(x1~p) -> P(s!1), S(x1~p!1) # S(x1~p, x2~p, x3~p, x4~p) + P(s) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) 66 2,37 36 kPS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) -> S(x1~u, x2~p, x3~p, x4~p) + P(s) 67 36 2,17 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) -> S(x1~p, x2~p, x3~p, x4~p) + P(s) 68 36 2,37 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) 69 2,36 35 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) 70 2,36 35 kPS # rule : P(s), S(x1~p) -> P(s!1), S(x1~p!1) # S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) 71 2,36 35 kPS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 72 35 2,19 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 73 35 2,36 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 74 35 2,19 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) -> S(x1~p, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 75 35 2,36 kdPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) 76 2,35 25 kPS # rule : P(s), S(x1~p) -> P(s!1), S(x1~p!1) # S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) 77 2,35 25 kPS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 78 25 2,21 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 79 25 2,35 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 80 25 2,21 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 81 25 2,35 kdPS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~u) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 82 25 2,21 kuS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~p) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) -> S(x1~p, x2~p, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 83 25 2,35 kdPS # rule : P(s), S(x1~p) -> P(s!1), S(x1~p!1) # S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + P(s) -> S(x1~p!1, x2~p!2, x3~p!3, x4~p!4), P(s!1), P(s!4), P(s!3), P(s!2) 84 2,25 34 kPS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + K(s) 85 33 3,30 kpS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + K(s) 86 33 3,32 kdKS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + K(s) 87 33 3,30 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + K(s) 88 33 3,32 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + K(s) 89 33 3,30 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + K(s) 90 33 3,32 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + K(s) 91 33 3,30 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + K(s) 92 33 3,32 kdKS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~p) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 93 32 3,29 kpS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~u) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + K(s) 94 32 3,5 kdKS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 95 32 3,29 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + K(s) 96 32 3,5 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 97 32 3,29 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) + K(s) 98 32 3,5 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~u!4), K(s!4), K(s!3), K(s!2) 99 3,32 33 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!3, x4~u!1), K(s!3), K(s!2) + P(s) 100 31 2,32 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + P(s) 101 31 2,30 kdPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + K(s) 102 31 3,28 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + K(s) 103 31 3,10 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + K(s) 104 31 3,28 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + K(s) 105 31 3,10 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + K(s) 106 31 3,28 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + K(s) 107 31 3,10 kdKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p!4), P(s!4), K(s!3), K(s!2) 108 2,30 31 kPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + K(s) 109 30 3,16 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 110 30 3,29 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + K(s) 111 30 3,16 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 112 30 3,29 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + K(s) 113 30 3,16 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) 114 30 3,29 kdKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + P(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) 115 2,29 10 kPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + K(s) 116 29 3,15 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) 117 29 3,7 kdKS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + K(s) 118 29 3,15 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + K(s) 119 29 3,7 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~u!3, x4~p), K(s!3), K(s!2) 120 3,29 30 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p), K(s!2) + P(s) 121 28 2,29 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) + P(s) 122 28 2,16 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + P(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) 123 2,28 27 kPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + K(s) 124 28 3,20 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + K(s) 125 28 3,12 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) + K(s) 126 28 3,20 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + K(s) 127 28 3,12 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + P(s) 128 27 2,10 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + P(s) 129 27 2,28 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) + P(s) 130 27 2,10 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p!3), P(s!3), K(s!2) + P(s) 131 27 2,28 kdPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + K(s) 132 27 3,22 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + K(s) 133 27 3,26 kdKS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + K(s) 134 27 3,22 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + K(s) 135 27 3,26 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + P(s) 136 26 2,9 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + P(s) 137 26 2,12 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + P(s) 138 26 2,9 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) + P(s) 139 26 2,12 kdPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + K(s) 140 26 3,21 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) -> S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + K(s) 141 26 3,13 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p!3, x4~p!4), P(s!4), K(s!2), P(s!3) 142 3,26 27 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 143 24 2,26 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 144 24 2,22 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 145 24 2,26 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 146 24 2,22 kdPS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~u) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u, x2~u!1, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 147 24 2,26 kuS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~p) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) + P(s) 148 24 2,22 kdPS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~p) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> S(x1~p, x2~p!1, x3~p!2, x4~p!3), P(s!2), P(s!3), P(s!1) + K(s) 149 24 3,25 kpS # rule : K(s!1), S(x1~u!1) -> K(s), S(x1~u) # K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + K(s) 150 24 3,23 kdKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 151 23 2,13 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 152 23 2,21 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 153 23 2,13 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 154 23 2,21 kdPS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~u) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) + P(s) 155 23 2,13 kuS # rule : P(s!1), S(x2~p!1) -> P(s), S(x2~p) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) 156 23 2,21 kdPS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) + K(s) -> K(s!1), S(x1~u!1, x2~p!2, x3~p!3, x4~p!4), P(s!4), P(s!3), P(s!2) 157 3,23 24 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + P(s) 158 21 2,11 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 159 21 2,19 kdPS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~u) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + P(s) 160 21 2,11 kuS # rule : P(s!1), S(x3~p!1) -> P(s), S(x3~p) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) 161 21 2,19 kdPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + P(s) -> S(x1~u, x2~p!1, x3~p!2, x4~p!3), P(s!1), P(s!3), P(s!2) 162 2,21 23 kPS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) + K(s) -> K(s!1), S(x1~u!1, x2~p, x3~p!2, x4~p!3), P(s!3), P(s!2) 163 3,21 22 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) -> S(x1~u, x2~u, x3~p, x4~p) + P(s) 164 19 2,14 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) -> S(x1~u, x2~p, x3~p, x4~p) + P(s) 165 19 2,17 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) 166 2,19 21 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~u, x2~p, x3~p!1, x4~p!2), P(s!2), P(s!1) 167 2,19 21 kPS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p!2), P(s!2) 168 3,19 20 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # S(x1~u, x2~p, x3~p, x4~p) + P(s) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) 169 2,17 19 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~u, x2~p, x3~p, x4~p) + P(s) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) 170 2,17 19 kPS # rule : P(s), S(x2~p) -> P(s!1), S(x2~p!1) # S(x1~u, x2~p, x3~p, x4~p) + P(s) -> S(x1~u, x2~p, x3~p, x4~p!1), P(s!1) 171 2,17 19 kPS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~p, x3~p, x4~p) + K(s) -> K(s!1), S(x1~u!1, x2~p, x3~p, x4~p) 172 3,17 18 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + P(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) 173 2,15 12 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + P(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) 174 2,15 12 kPS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~p) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) -> S(x1~u, x2~p, x3~p, x4~p) + K(s) 175 15 3,17 kpS # rule : K(s!1), S(x2~u!1) -> K(s), S(x2~u) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) -> S(x1~u, x2~u, x3~p, x4~p) + K(s) 176 15 3,14 kdKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) + K(s) -> K(s!1), S(x1~u!1, x2~u!2, x3~p, x4~p), K(s!2) 177 3,15 16 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # S(x1~u, x2~u, x3~p, x4~p) + P(s) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) 178 2,14 11 kPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~u, x2~u, x3~p, x4~p) + P(s) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) 179 2,14 11 kPS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~p, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) 180 3,14 15 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~p, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p) 181 3,14 15 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) -> S(x1~u, x2~u, x3~u, x4~p) + P(s) 182 11 2,6 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) -> S(x1~u, x2~u, x3~p, x4~p) + P(s) 183 11 2,14 kdPS # rule : P(s), S(x3~p) -> P(s!1), S(x3~p!1) # S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + P(s) -> S(x1~u, x2~u, x3~p!1, x4~p!2), P(s!1), P(s!2) 184 2,11 13 kPS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) 185 3,11 12 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u, x2~u!1, x3~p, x4~p!2), P(s!2) 186 3,11 12 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + P(s) 187 9 2,4 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) + P(s) 188 9 2,7 kdPS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~p) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) -> S(x1~u, x2~u, x3~p, x4~p!1), P(s!1) + K(s) 189 9 3,11 kpS # rule : K(s!1), S(x3~u!1) -> K(s), S(x3~u) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) -> S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + K(s) 190 9 3,8 kdKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) 191 3,9 10 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) + K(s) -> K(s!1), S(x1~u, x2~u!2, x3~u!1, x4~p!3), P(s!3), K(s!2) 192 3,9 10 kKS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~u) # S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) -> S(x1~u, x2~u, x3~u, x4~u) + P(s) 193 8 1,2 kuS # rule : P(s!1), S(x4~p!1) -> P(s), S(x4~p) # S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) -> S(x1~u, x2~u, x3~u, x4~p) + P(s) 194 8 2,6 kdPS # rule : K(s), S(x3~u) -> K(s!1), S(x3~u!1) # S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) 195 3,8 9 kKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) 196 3,8 9 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p!2), P(s!2) 197 3,8 9 kKS # rule : P(s), S(x4~p) -> P(s!1), S(x4~p!1) # S(x1~u, x2~u, x3~u, x4~p) + P(s) -> S(x1~u, x2~u, x3~u, x4~p!1), P(s!1) 198 2,6 8 kPS # rule : K(s), S(x3~u) -> K(s!1), S(x3~u!1) # S(x1~u, x2~u, x3~u, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) 199 3,6 7 kKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~u, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) 200 3,6 7 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~u, x4~p) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!1, x4~p) 201 3,6 7 kKS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~p) # K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) -> S(x1~u, x2~u, x3~u, x4~p) + K(s) 202 4 3,6 kpS # rule : K(s!1), S(x4~u!1) -> K(s), S(x4~u) # K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) -> S(x1~u, x2~u, x3~u, x4~u) + K(s) 203 4 1,3 kdKS # rule : K(s), S(x3~u) -> K(s!1), S(x3~u!1) # K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) 204 3,4 5 kKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) 205 3,4 5 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u!2, x4~u!1), K(s!2) 206 3,4 5 kKS # rule : K(s), S(x4~u) -> K(s!1), S(x4~u!1) # S(x1~u, x2~u, x3~u, x4~u) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) 207 1,3 4 kKS # rule : K(s), S(x3~u) -> K(s!1), S(x3~u!1) # S(x1~u, x2~u, x3~u, x4~u) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) 208 1,3 4 kKS # rule : K(s), S(x2~u) -> K(s!1), S(x2~u!1) # S(x1~u, x2~u, x3~u, x4~u) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) 209 1,3 4 kKS # rule : K(s), S(x1~u) -> K(s!1), S(x1~u!1) # S(x1~u, x2~u, x3~u, x4~u) + K(s) -> K(s!1), S(x1~u, x2~u, x3~u, x4~u!1) 210 1,3 4 kKS end reactions