dwolter_SparQ/Calculi/oprastar_1.lisp
(def-calculus "OPRA* mit m=1 (ostar_1)"
	:arity             :binary
	:identity-relation P_s_0
	:parametric?       nil
	:base-relations (P_s_0 O_0_0 +_0_1 P_0_2 -_0_3 +_s_1 -_1_0 +_1_1 -_1_1 O_1_1 +_1_2 +_1_3 -_1_3 P_1_3 O_s_2 P_2_0 -_2_1 O_2_2 +_2_3 -_s_3 +_3_0 +_3_1 -_3_1 P_3_1 -_3_2 +_3_3 -_3_3 O_3_3 )



	:converse-operation ( 
		( P_s_0 P_s_0 )
		( O_0_0 O_0_0 )
		( +_0_1 -_1_0 )
		( P_0_2 P_2_0 )
		( -_0_3 +_3_0 )
		( +_s_1 -_s_3 )
		( -_1_0 +_0_1 )
		( +_1_1 -_1_1 )
		( -_1_1 +_1_1 )
		( O_1_1 O_1_1 )
		( +_1_2 -_2_1 )
		( +_1_3 -_3_1 )
		( -_1_3 +_3_1 )
		( P_1_3 P_3_1 )
		( O_s_2 O_s_2 )
		( P_2_0 P_0_2 )
		( -_2_1 +_1_2 )
		( O_2_2 O_2_2 )
		( +_2_3 -_3_2 )
		( -_s_3 +_s_1 )
		( +_3_0 -_0_3 )
		( +_3_1 -_1_3 )
		( -_3_1 +_1_3 )
		( P_3_1 P_1_3 )
		( -_3_2 +_2_3 )
		( +_3_3 -_3_3 )
		( -_3_3 +_3_3 )
		( O_3_3 O_3_3 )
)



	:composition-operation (
(P_S_0 P_S_0 (P_S_0)) (P_S_0 O_0_0 (O_0_0)) (P_S_0 +_0_1 (+_0_1))
 (P_S_0 P_0_2 (P_0_2)) (P_S_0 -_0_3 (-_0_3)) (P_S_0 +_S_1 (+_S_1))
 (P_S_0 -_1_0 (-_1_0)) (P_S_0 +_1_1 (+_1_1)) (P_S_0 -_1_1 (-_1_1))
 (P_S_0 O_1_1 (O_1_1)) (P_S_0 +_1_2 (+_1_2)) (P_S_0 +_1_3 (+_1_3))
 (P_S_0 -_1_3 (-_1_3)) (P_S_0 P_1_3 (P_1_3)) (P_S_0 O_S_2 (O_S_2))
 (P_S_0 P_2_0 (P_2_0)) (P_S_0 -_2_1 (-_2_1)) (P_S_0 O_2_2 (O_2_2))
 (P_S_0 +_2_3 (+_2_3)) (P_S_0 -_S_3 (-_S_3)) (P_S_0 +_3_0 (+_3_0))
 (P_S_0 +_3_1 (+_3_1)) (P_S_0 -_3_1 (-_3_1)) (P_S_0 P_3_1 (P_3_1))
 (P_S_0 -_3_2 (-_3_2)) (P_S_0 +_3_3 (+_3_3)) (P_S_0 -_3_3 (-_3_3))
 (P_S_0 O_3_3 (O_3_3)) (O_0_0 P_S_0 (O_0_0))
 (O_0_0 O_0_0 (P_S_0 P_2_0 P_2_0 P_0_2 P_0_2))
 (O_0_0 +_0_1 (-_S_3 -_2_1 -_2_1 -_0_3 -_0_3))
 (O_0_0 P_0_2 (O_0_0 O_0_0 O_S_2 O_2_2 O_2_2))
 (O_0_0 -_0_3 (+_0_1 +_0_1 +_S_1 +_2_3 +_2_3))
 (O_0_0 +_S_1 (-_0_3)) (O_0_0 -_1_0 (+_3_1))
 (O_0_0 +_1_1 (-_3_1 -_3_2 -_3_3)) (O_0_0 -_1_1 (+_3_1))
 (O_0_0 O_1_1 (P_3_1)) (O_0_0 +_1_2 (-_3_3)) (O_0_0 +_1_3 (-_3_3))
 (O_0_0 -_1_3 (+_3_0 +_3_1 +_3_3)) (O_0_0 P_1_3 (O_3_3))
 (O_0_0 O_S_2 (P_0_2)) (O_0_0 P_2_0 (O_0_0 O_0_0))
 (O_0_0 -_2_1 (+_0_1 +_0_1)) (O_0_0 O_2_2 (P_0_2 P_0_2))
 (O_0_0 +_2_3 (-_0_3 -_0_3)) (O_0_0 -_S_3 (+_0_1))
 (O_0_0 +_3_0 (-_1_3)) (O_0_0 +_3_1 (-_1_0 -_1_1 -_1_3))
 (O_0_0 -_3_1 (+_1_1)) (O_0_0 P_3_1 (O_1_1)) (O_0_0 -_3_2 (+_1_1))
 (O_0_0 +_3_3 (-_1_3)) (O_0_0 -_3_3 (+_1_1 +_1_2 +_1_3))
 (O_0_0 O_3_3 (P_1_3)) (+_0_1 P_S_0 (+_0_1)) (+_0_1 O_0_0 (-_1_3))
 (+_0_1 +_0_1 (-_1_0 +_1_1 O_1_1 -_1_1 -_1_3))
 (+_0_1 P_0_2 (+_1_1))
 (+_0_1 -_0_3 (+_1_1 +_1_2 +_1_3 P_1_3 -_1_3))
 (+_0_1 +_S_1 (O_0_0 +_0_1 -_0_3))
 (+_0_1 -_1_0 (-_1_3 P_0_2 P_0_2 +_3_1 P_2_0 P_2_0 P_S_0))
 (+_0_1 +_1_1
  (-_1_0 -_S_3 +_1_1 O_1_1 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2
   -_0_3 -_0_3 -_1_3 -_3_3))
 (+_0_1 -_1_1
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_0_3 -_0_3 -_1_3 -_3_3))
 (+_0_1 O_1_1
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 -_3_3))
 (+_0_1 +_1_2 (-_3_3 O_2_2 O_2_2 O_S_2 +_1_1 O_0_0 O_0_0))
 (+_0_1 +_1_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (+_0_1 -_1_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_2_3 +_3_3))
 (+_0_1 P_1_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3))
 (+_0_1 O_S_2 (-_0_3)) (+_0_1 P_2_0 (+_3_1))
 (+_0_1 -_2_1 (+_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (+_0_1 O_2_2 (-_3_3))
 (+_0_1 +_2_3 (+_3_0 +_3_1 +_3_3 O_3_3 -_3_3))
 (+_0_1 -_S_3 (+_0_1 P_0_2 -_0_3))
 (+_0_1 +_3_0 (O_0_0 O_0_0 +_3_1 -_1_3))
 (+_0_1 +_3_1
  (-_1_0 +_0_1 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_1_3))
 (+_0_1 -_3_1
  (+_0_1 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (+_0_1 P_3_1 (+_3_1 +_1_1 +_0_1 +_0_1))
 (+_0_1 -_3_2 (+_1_1 P_0_2 P_0_2 -_3_3))
 (+_0_1 +_3_3
  (+_3_0 +_3_1 -_0_3 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (+_0_1 -_3_3
  (+_1_1 +_1_2 -_0_3 -_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (+_0_1 O_3_3 (-_3_3 -_1_3 -_0_3 -_0_3)) (P_0_2 P_S_0 (P_0_2))
 (P_0_2 O_0_0 (O_0_0 O_0_0)) (P_0_2 +_0_1 (+_0_1 +_0_1))
 (P_0_2 P_0_2 (P_0_2 P_0_2)) (P_0_2 -_0_3 (-_0_3 -_0_3))
 (P_0_2 +_S_1 (+_0_1)) (P_0_2 -_1_0 (-_1_3)) (P_0_2 +_1_1 (+_1_1))
 (P_0_2 -_1_1 (-_1_0 -_1_1 -_1_3)) (P_0_2 O_1_1 (O_1_1))
 (P_0_2 +_1_2 (+_1_1)) (P_0_2 +_1_3 (+_1_1 +_1_2 +_1_3))
 (P_0_2 -_1_3 (-_1_3)) (P_0_2 P_1_3 (P_1_3)) (P_0_2 O_S_2 (O_0_0))
 (P_0_2 P_2_0 (P_S_0 P_2_0 P_2_0 P_0_2 P_0_2))
 (P_0_2 -_2_1 (-_S_3 -_2_1 -_2_1 -_0_3 -_0_3))
 (P_0_2 O_2_2 (O_0_0 O_0_0 O_S_2 O_2_2 O_2_2))
 (P_0_2 +_2_3 (+_0_1 +_0_1 +_S_1 +_2_3 +_2_3))
 (P_0_2 -_S_3 (-_0_3)) (P_0_2 +_3_0 (+_3_1)) (P_0_2 +_3_1 (+_3_1))
 (P_0_2 -_3_1 (-_3_1 -_3_2 -_3_3)) (P_0_2 P_3_1 (P_3_1))
 (P_0_2 -_3_2 (-_3_3)) (P_0_2 +_3_3 (+_3_0 +_3_1 +_3_3))
 (P_0_2 -_3_3 (-_3_3)) (P_0_2 O_3_3 (O_3_3)) (-_0_3 P_S_0 (-_0_3))
 (-_0_3 O_0_0 (+_3_1))
 (-_0_3 +_0_1 (+_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (-_0_3 P_0_2 (-_3_3))
 (-_0_3 -_0_3 (+_3_0 +_3_1 +_3_3 O_3_3 -_3_3))
 (-_0_3 +_S_1 (+_0_1 P_0_2 -_0_3))
 (-_0_3 -_1_0 (O_0_0 O_0_0 +_3_1 -_1_3))
 (-_0_3 +_1_1
  (+_0_1 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (-_0_3 -_1_1
  (-_1_0 +_0_1 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_1_3))
 (-_0_3 O_1_1 (+_3_1 +_1_1 +_0_1 +_0_1))
 (-_0_3 +_1_2 (+_1_1 P_0_2 P_0_2 -_3_3))
 (-_0_3 +_1_3
  (+_1_1 +_1_2 -_0_3 -_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (-_0_3 -_1_3
  (+_3_0 +_3_1 -_0_3 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (-_0_3 P_1_3 (-_3_3 -_1_3 -_0_3 -_0_3)) (-_0_3 O_S_2 (+_0_1))
 (-_0_3 P_2_0 (-_1_3))
 (-_0_3 -_2_1 (-_1_0 +_1_1 O_1_1 -_1_1 -_1_3))
 (-_0_3 O_2_2 (+_1_1))
 (-_0_3 +_2_3 (+_1_1 +_1_2 +_1_3 P_1_3 -_1_3))
 (-_0_3 -_S_3 (O_0_0 +_0_1 -_0_3))
 (-_0_3 +_3_0 (-_1_3 P_0_2 P_0_2 +_3_1 P_2_0 P_2_0 P_S_0))
 (-_0_3 +_3_1
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_0_3 -_0_3 -_1_3 -_3_3))
 (-_0_3 -_3_1
  (-_1_0 -_S_3 +_1_1 O_1_1 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2
   -_0_3 -_0_3 -_1_3 -_3_3))
 (-_0_3 P_3_1
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 -_3_3))
 (-_0_3 -_3_2 (-_3_3 O_2_2 O_2_2 O_S_2 +_1_1 O_0_0 O_0_0))
 (-_0_3 +_3_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_2_3 +_3_3))
 (-_0_3 -_3_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (-_0_3 O_3_3
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3))
 (+_S_1 P_S_0 (+_S_1)) (+_S_1 O_0_0 (-_1_0))
 (+_S_1 +_0_1 (+_1_1 O_1_1 -_1_1)) (+_S_1 P_0_2 (+_1_2))
 (+_S_1 -_0_3 (+_1_3 P_1_3 -_1_3))
 (+_S_1 +_S_1 (-_S_3 O_S_2 +_S_1))
 (+_S_1 -_1_0 (-_1_0 P_2_0 +_3_0))
 (+_S_1 +_1_1 (-_3_1 -_2_1 -_1_1 O_1_1 +_1_1))
 (+_S_1 -_1_1 (-_3_1 P_3_1 +_3_1 -_2_1 -_1_1))
 (+_S_1 O_1_1 (-_1_1 -_2_1 -_3_1))
 (+_S_1 +_1_2 (+_1_2 O_2_2 -_3_2))
 (+_S_1 +_1_3 (-_3_3 O_3_3 +_3_3 +_2_3 +_1_3))
 (+_S_1 -_1_3 (+_3_3 +_2_3 -_1_3 P_1_3 +_1_3))
 (+_S_1 P_1_3 (+_1_3 +_2_3 +_3_3)) (+_S_1 O_S_2 (-_S_3))
 (+_S_1 P_2_0 (+_3_0)) (+_S_1 -_2_1 (+_3_1 P_3_1 -_3_1))
 (+_S_1 O_2_2 (-_3_2)) (+_S_1 +_2_3 (+_3_3 O_3_3 -_3_3))
 (+_S_1 -_S_3 (P_S_0 -_S_3 +_S_1))
 (+_S_1 +_3_0 (O_0_0 -_1_0 +_3_0))
 (+_S_1 +_3_1 (+_3_1 -_1_1 O_1_1 +_1_1 +_0_1))
 (+_S_1 -_3_1 (-_3_1 P_3_1 +_3_1 +_1_1 +_0_1))
 (+_S_1 P_3_1 (+_0_1 +_1_1 +_3_1))
 (+_S_1 -_3_2 (P_0_2 +_1_2 -_3_2))
 (+_S_1 +_3_3 (-_3_3 O_3_3 +_3_3 -_1_3 -_0_3))
 (+_S_1 -_3_3 (-_3_3 -_1_3 P_1_3 +_1_3 -_0_3))
 (+_S_1 O_3_3 (-_0_3 -_1_3 -_3_3)) (-_1_0 P_S_0 (-_1_0))
 (-_1_0 O_0_0 (+_3_0 +_3_0 +_1_2 +_1_2 +_S_1))
 (-_1_0 +_0_1
  (P_S_0 -_S_3 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 +_S_1 +_1_3
   P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (-_1_0 P_0_2 (-_1_0 -_1_0 -_S_3 -_3_2 -_3_2))
 (-_1_0 -_0_3
  (-_S_3 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 O_S_2 +_S_1 +_3_3
   O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_1_0 +_S_1 (+_1_3 P_1_3 -_1_3))
 (-_1_0 -_1_0 (+_0_1 +_1_1 O_1_1 -_1_1 +_3_1))
 (-_1_0 +_1_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (-_1_0 -_1_1 (+_0_1 +_1_1 O_1_1 -_1_1 +_3_1))
 (-_1_0 O_1_1 (+_3_1 +_1_1 +_0_1))
 (-_1_0 +_1_2 (-_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (-_1_0 +_1_3 (-_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (-_1_0 -_1_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (-_1_0 P_1_3 (-_3_3 -_1_3 -_0_3)) (-_1_0 O_S_2 (+_1_2))
 (-_1_0 P_2_0 (-_1_0 -_1_0))
 (-_1_0 -_2_1 (+_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1))
 (-_1_0 O_2_2 (+_1_2 +_1_2))
 (-_1_0 +_2_3 (+_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (-_1_0 -_S_3 (+_1_1 O_1_1 -_1_1))
 (-_1_0 +_3_0 (+_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (-_1_0 +_3_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (-_1_0 -_3_1 (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1))
 (-_1_0 P_3_1 (-_3_1 -_2_1 -_1_1))
 (-_1_0 -_3_2 (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1))
 (-_1_0 +_3_3 (+_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (-_1_0 -_3_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (-_1_0 O_3_3 (+_3_3 +_2_3 +_1_3)) (+_1_1 P_S_0 (+_1_1))
 (-_1_1 P_S_0 (-_1_1)) (O_1_1 P_S_0 (O_1_1)) (+_1_1 O_0_0 (-_1_3))
 (-_1_1 O_0_0 (+_1_3 +_2_3 +_3_3)) (O_1_1 O_0_0 (P_1_3))
 (+_1_1 +_0_1 (-_1_0 +_1_1 O_1_1 -_1_1 -_1_3))
 (-_1_1 +_0_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (O_1_1 +_0_1 (-_1_3 -_1_1 -_1_0)) (+_1_1 P_0_2 (+_1_1))
 (-_1_1 P_0_2 (-_1_1 -_2_1 -_3_1)) (O_1_1 P_0_2 (O_1_1))
 (+_1_1 -_0_3 (+_1_1 +_1_2 +_1_3 P_1_3 -_1_3))
 (-_1_1 -_0_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (O_1_1 -_0_3 (+_1_3 +_1_2 +_1_1))
 (+_1_1 +_S_1 (-_1_3 -_1_1 O_1_1 +_1_1 -_1_0))
 (-_1_1 +_S_1 (-_1_3 P_1_3 +_1_3 -_1_1 -_1_0))
 (O_1_1 +_S_1 (-_1_0 -_1_1 -_1_3))
 (+_1_1 -_1_0
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   P_1_3 -_1_3 +_2_3 +_3_3))
 (-_1_1 -_1_0
  (+_3_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_1_2 +_1_2
   +_S_1 +_1_3 +_2_3 +_3_3))
 (O_1_1 -_1_0
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3))
 (+_1_1 +_1_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   O_1_1 +_1_1 -_S_3 -_1_0))
 (+_1_1 -_1_1
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 +_1_1 -_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 -_3_3 +_3_3))
 (+_1_1 O_1_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (-_1_1 +_1_1
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 +_1_1 -_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 -_3_3 +_3_3))
 (-_1_1 -_1_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 -_1_1
   O_1_1 +_1_1 +_0_1 +_3_0))
 (-_1_1 O_1_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (O_1_1 +_1_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (O_1_1 -_1_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (O_1_1 O_1_1 (P_1_3 P_1_3 P_0_2 P_3_1 P_3_1 P_2_0 P_S_0))
 (+_1_1 +_1_2
  (-_1_0 -_1_0 -_S_3 +_1_1 O_1_1 -_1_1 -_2_1 -_3_1 -_3_2
   -_3_2 -_0_3 -_1_3 -_3_3))
 (-_1_1 +_1_2
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (O_1_1 +_1_2
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 -_3_3))
 (+_1_1 +_1_3
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 +_3_1 -_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   -_1_3 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_1_1 -_1_3
  (+_3_3 +_3_3 +_2_3 -_1_3 P_1_3 +_1_3 +_S_1 +_1_2 +_3_1
   +_1_1 +_1_1 +_0_1 +_3_0))
 (+_1_1 P_1_3
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (-_1_1 +_1_3
  (-_3_3 -_3_3 -_1_3 P_1_3 +_1_3 -_0_3 -_3_2 -_3_1 -_2_1
   -_1_1 -_1_1 -_S_3 -_1_0))
 (-_1_1 -_1_3
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 +_3_1 -_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   -_1_3 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_1_1 P_1_3
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (O_1_1 +_1_3
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (O_1_1 -_1_3
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (O_1_1 P_1_3 (O_3_3 O_3_3 O_2_2 O_S_2 O_1_1 O_1_1 O_0_0))
 (+_1_1 O_S_2 (-_1_3)) (-_1_1 O_S_2 (+_1_3)) (O_1_1 O_S_2 (P_1_3))
 (+_1_1 P_2_0 (+_0_1 +_1_1 +_3_1)) (-_1_1 P_2_0 (-_1_1))
 (O_1_1 P_2_0 (O_1_1))
 (+_1_1 -_2_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (-_1_1 -_2_1 (+_1_1 O_1_1 -_1_1 +_1_2 +_1_3))
 (O_1_1 -_2_1 (+_1_3 +_1_2 +_1_1))
 (+_1_1 O_2_2 (-_0_3 -_1_3 -_3_3)) (-_1_1 O_2_2 (+_1_3))
 (O_1_1 O_2_2 (P_1_3))
 (+_1_1 +_2_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (-_1_1 +_2_3 (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3))
 (O_1_1 +_2_3 (-_1_3 -_1_1 -_1_0))
 (+_1_1 -_S_3 (-_1_3 P_1_3 +_1_3 +_1_2 +_1_1))
 (-_1_1 -_S_3 (+_1_3 +_1_2 -_1_1 O_1_1 +_1_1))
 (O_1_1 -_S_3 (+_1_1 +_1_2 +_1_3))
 (+_1_1 +_3_0
  (-_1_0 -_1_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_1_3))
 (-_1_1 +_3_0
  (-_1_0 -_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (O_1_1 +_3_0 (-_1_0 -_1_0 -_1_1 -_1_3))
 (+_1_1 +_3_1
  (-_1_0 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 +_3_1
   -_1_3))
 (+_1_1 -_3_1
  (+_0_1 +_1_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (+_1_1 P_3_1 (+_0_1 +_1_1 +_1_1 +_3_1))
 (-_1_1 +_3_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3
   P_1_3 -_1_3 +_2_3 +_3_3))
 (-_1_1 -_3_1
  (+_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2
   +_1_3))
 (-_1_1 P_3_1 (-_1_1 -_1_1 -_2_1 -_3_1))
 (O_1_1 +_3_1 (-_1_0 -_1_1 -_1_1 -_1_3))
 (O_1_1 -_3_1 (+_1_1 +_1_1 +_1_2 +_1_3)) (O_1_1 P_3_1 (O_1_1 O_1_1))
 (+_1_1 -_3_2
  (+_1_1 +_1_2 +_1_2 -_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (-_1_1 -_3_2
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 +_1_2 +_1_3))
 (O_1_1 -_3_2 (+_1_1 +_1_2 +_1_2 +_1_3))
 (+_1_1 +_3_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (+_1_1 -_3_3
  (+_1_1 +_1_2 -_0_3 +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3
   -_3_3))
 (+_1_1 O_3_3 (-_0_3 -_1_3 -_1_3 -_3_3))
 (-_1_1 +_3_3
  (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3
   +_3_3))
 (-_1_1 -_3_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (-_1_1 O_3_3 (+_1_3 +_1_3 +_2_3 +_3_3))
 (O_1_1 +_3_3 (-_1_0 -_1_1 -_1_3 -_1_3))
 (O_1_1 -_3_3 (+_1_1 +_1_2 +_1_3 +_1_3)) (O_1_1 O_3_3 (P_1_3 P_1_3))
 (+_1_2 P_S_0 (+_1_2)) (+_1_2 O_0_0 (-_1_0 -_1_0))
 (+_1_2 +_0_1 (+_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1))
 (+_1_2 P_0_2 (+_1_2 +_1_2))
 (+_1_2 -_0_3 (+_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (+_1_2 +_S_1 (+_1_1 O_1_1 -_1_1))
 (+_1_2 -_1_0 (+_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (+_1_2 +_1_1 (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1))
 (+_1_2 -_1_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (+_1_2 O_1_1 (-_3_1 -_2_1 -_1_1))
 (+_1_2 +_1_2 (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1))
 (+_1_2 +_1_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (+_1_2 -_1_3 (+_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (+_1_2 P_1_3 (+_3_3 +_2_3 +_1_3)) (+_1_2 O_S_2 (-_1_0))
 (+_1_2 P_2_0 (+_3_0 +_3_0 +_1_2 +_1_2 +_S_1))
 (+_1_2 -_2_1
  (P_S_0 -_S_3 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 +_S_1 +_1_3
   P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (+_1_2 O_2_2 (-_1_0 -_1_0 -_S_3 -_3_2 -_3_2))
 (+_1_2 +_2_3
  (-_S_3 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 O_S_2 +_S_1 +_3_3
   O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_1_2 -_S_3 (+_1_3 P_1_3 -_1_3))
 (+_1_2 +_3_0 (+_0_1 +_1_1 O_1_1 -_1_1 +_3_1))
 (+_1_2 +_3_1 (+_0_1 +_1_1 O_1_1 -_1_1 +_3_1))
 (+_1_2 -_3_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (+_1_2 P_3_1 (+_3_1 +_1_1 +_0_1))
 (+_1_2 -_3_2 (-_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (+_1_2 +_3_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (+_1_2 -_3_3 (-_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (+_1_2 O_3_3 (-_3_3 -_1_3 -_0_3)) (+_1_3 P_S_0 (+_1_3))
 (-_1_3 P_S_0 (-_1_3)) (P_1_3 P_S_0 (P_1_3)) (+_1_3 O_0_0 (-_1_1))
 (-_1_3 O_0_0 (+_0_1 +_1_1 +_3_1)) (P_1_3 O_0_0 (O_1_1))
 (+_1_3 +_0_1 (+_1_1 O_1_1 -_1_1 +_1_2 +_1_3))
 (-_1_3 +_0_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (P_1_3 +_0_1 (+_1_3 +_1_2 +_1_1)) (+_1_3 P_0_2 (+_1_3))
 (-_1_3 P_0_2 (-_0_3 -_1_3 -_3_3)) (P_1_3 P_0_2 (P_1_3))
 (+_1_3 -_0_3 (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3))
 (-_1_3 -_0_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (P_1_3 -_0_3 (-_1_3 -_1_1 -_1_0))
 (+_1_3 +_S_1 (+_1_3 +_1_2 -_1_1 O_1_1 +_1_1))
 (-_1_3 +_S_1 (-_1_3 P_1_3 +_1_3 +_1_2 +_1_1))
 (P_1_3 +_S_1 (+_1_1 +_1_2 +_1_3))
 (+_1_3 -_1_0
  (-_1_0 -_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3))
 (-_1_3 -_1_0
  (-_1_0 -_1_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_1_3))
 (P_1_3 -_1_0 (-_1_0 -_1_0 -_1_1 -_1_3))
 (+_1_3 +_1_1
  (+_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2
   +_1_3))
 (+_1_3 -_1_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3
   P_1_3 -_1_3 +_2_3 +_3_3))
 (+_1_3 O_1_1 (-_1_1 -_1_1 -_2_1 -_3_1))
 (-_1_3 +_1_1
  (+_0_1 +_1_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (-_1_3 -_1_1
  (-_1_0 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 +_3_1
   -_1_3))
 (-_1_3 O_1_1 (+_0_1 +_1_1 +_1_1 +_3_1))
 (P_1_3 +_1_1 (+_1_1 +_1_1 +_1_2 +_1_3))
 (P_1_3 -_1_1 (-_1_0 -_1_1 -_1_1 -_1_3)) (P_1_3 O_1_1 (O_1_1 O_1_1))
 (+_1_3 +_1_2
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 +_1_2 +_1_3))
 (-_1_3 +_1_2
  (+_1_1 +_1_2 +_1_2 -_0_3 +_1_3 P_1_3 -_1_3 -_3_3))
 (P_1_3 +_1_2 (+_1_1 +_1_2 +_1_2 +_1_3))
 (+_1_3 +_1_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (+_1_3 -_1_3
  (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3
   +_3_3))
 (+_1_3 P_1_3 (+_1_3 +_1_3 +_2_3 +_3_3))
 (-_1_3 +_1_3
  (+_1_1 +_1_2 -_0_3 +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3
   -_3_3))
 (-_1_3 -_1_3
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (-_1_3 P_1_3 (-_0_3 -_1_3 -_1_3 -_3_3))
 (P_1_3 +_1_3 (+_1_1 +_1_2 +_1_3 +_1_3))
 (P_1_3 -_1_3 (-_1_0 -_1_1 -_1_3 -_1_3)) (P_1_3 P_1_3 (P_1_3 P_1_3))
 (+_1_3 O_S_2 (-_1_1)) (-_1_3 O_S_2 (+_1_1)) (P_1_3 O_S_2 (O_1_1))
 (+_1_3 P_2_0 (+_1_3 +_2_3 +_3_3)) (-_1_3 P_2_0 (-_1_3))
 (P_1_3 P_2_0 (P_1_3))
 (+_1_3 -_2_1
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (-_1_3 -_2_1 (-_1_0 +_1_1 O_1_1 -_1_1 -_1_3))
 (P_1_3 -_2_1 (-_1_3 -_1_1 -_1_0))
 (+_1_3 O_2_2 (-_1_1 -_2_1 -_3_1)) (-_1_3 O_2_2 (+_1_1))
 (P_1_3 O_2_2 (O_1_1))
 (+_1_3 +_2_3
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (-_1_3 +_2_3 (+_1_1 +_1_2 +_1_3 P_1_3 -_1_3))
 (P_1_3 +_2_3 (+_1_3 +_1_2 +_1_1))
 (+_1_3 -_S_3 (-_1_3 P_1_3 +_1_3 -_1_1 -_1_0))
 (-_1_3 -_S_3 (-_1_3 -_1_1 O_1_1 +_1_1 -_1_0))
 (P_1_3 -_S_3 (-_1_0 -_1_1 -_1_3))
 (+_1_3 +_3_0
  (+_3_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_1_2 +_1_2
   +_S_1 +_1_3 +_2_3 +_3_3))
 (-_1_3 +_3_0
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   P_1_3 -_1_3 +_2_3 +_3_3))
 (P_1_3 +_3_0
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3))
 (+_1_3 +_3_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 -_1_1
   O_1_1 +_1_1 +_0_1 +_3_0))
 (+_1_3 -_3_1
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 +_1_1 -_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 -_3_3 +_3_3))
 (+_1_3 P_3_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (-_1_3 +_3_1
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 +_1_1 -_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 -_3_3 +_3_3))
 (-_1_3 -_3_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   O_1_1 +_1_1 -_S_3 -_1_0))
 (-_1_3 P_3_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (P_1_3 +_3_1
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (P_1_3 -_3_1
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (P_1_3 P_3_1 (P_1_3 P_1_3 P_0_2 P_3_1 P_3_1 P_2_0 P_S_0))
 (+_1_3 -_3_2
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (-_1_3 -_3_2
  (-_1_0 -_1_0 -_S_3 +_1_1 O_1_1 -_1_1 -_2_1 -_3_1 -_3_2
   -_3_2 -_0_3 -_1_3 -_3_3))
 (P_1_3 -_3_2
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 -_3_3))
 (+_1_3 +_3_3
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 +_3_1 -_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   -_1_3 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_1_3 -_3_3
  (-_3_3 -_3_3 -_1_3 P_1_3 +_1_3 -_0_3 -_3_2 -_3_1 -_2_1
   -_1_1 -_1_1 -_S_3 -_1_0))
 (+_1_3 O_3_3
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (-_1_3 +_3_3
  (+_3_3 +_3_3 +_2_3 -_1_3 P_1_3 +_1_3 +_S_1 +_1_2 +_3_1
   +_1_1 +_1_1 +_0_1 +_3_0))
 (-_1_3 -_3_3
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 +_3_1 -_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   -_1_3 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_1_3 O_3_3
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (P_1_3 +_3_3
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (P_1_3 -_3_3
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (P_1_3 O_3_3 (O_3_3 O_3_3 O_2_2 O_S_2 O_1_1 O_1_1 O_0_0))
 (O_S_2 P_S_0 (O_S_2)) (O_S_2 O_0_0 (P_2_0)) (O_S_2 +_0_1 (-_2_1))
 (O_S_2 P_0_2 (O_2_2)) (O_S_2 -_0_3 (+_2_3)) (O_S_2 +_S_1 (-_S_3))
 (O_S_2 -_1_0 (+_3_0)) (O_S_2 +_1_1 (-_3_1)) (O_S_2 -_1_1 (+_3_1))
 (O_S_2 O_1_1 (P_3_1)) (O_S_2 +_1_2 (-_3_2)) (O_S_2 +_1_3 (-_3_3))
 (O_S_2 -_1_3 (+_3_3)) (O_S_2 P_1_3 (O_3_3)) (O_S_2 O_S_2 (P_S_0))
 (O_S_2 P_2_0 (O_0_0)) (O_S_2 -_2_1 (+_0_1)) (O_S_2 O_2_2 (P_0_2))
 (O_S_2 +_2_3 (-_0_3)) (O_S_2 -_S_3 (+_S_1)) (O_S_2 +_3_0 (-_1_0))
 (O_S_2 +_3_1 (-_1_1)) (O_S_2 -_3_1 (+_1_1)) (O_S_2 P_3_1 (O_1_1))
 (O_S_2 -_3_2 (+_1_2)) (O_S_2 +_3_3 (-_1_3)) (O_S_2 -_3_3 (+_1_3))
 (O_S_2 O_3_3 (P_1_3)) (P_2_0 P_S_0 (P_2_0))
 (P_2_0 O_0_0 (O_0_0 O_0_0 O_S_2 O_2_2 O_2_2))
 (P_2_0 +_0_1 (+_0_1 +_0_1 +_S_1 +_2_3 +_2_3))
 (P_2_0 P_0_2 (P_S_0 P_2_0 P_2_0 P_0_2 P_0_2))
 (P_2_0 -_0_3 (-_S_3 -_2_1 -_2_1 -_0_3 -_0_3))
 (P_2_0 +_S_1 (+_2_3)) (P_2_0 -_1_0 (-_1_1))
 (P_2_0 +_1_1 (+_1_1 +_1_2 +_1_3)) (P_2_0 -_1_1 (-_1_1))
 (P_2_0 O_1_1 (O_1_1)) (P_2_0 +_1_2 (+_1_3)) (P_2_0 +_1_3 (+_1_3))
 (P_2_0 -_1_3 (-_1_0 -_1_1 -_1_3)) (P_2_0 P_1_3 (P_1_3))
 (P_2_0 O_S_2 (O_2_2)) (P_2_0 P_2_0 (P_2_0 P_2_0))
 (P_2_0 -_2_1 (-_2_1 -_2_1)) (P_2_0 O_2_2 (O_2_2 O_2_2))
 (P_2_0 +_2_3 (+_2_3 +_2_3)) (P_2_0 -_S_3 (-_2_1))
 (P_2_0 +_3_0 (+_3_3)) (P_2_0 +_3_1 (+_3_0 +_3_1 +_3_3))
 (P_2_0 -_3_1 (-_3_1)) (P_2_0 P_3_1 (P_3_1)) (P_2_0 -_3_2 (-_3_1))
 (P_2_0 +_3_3 (+_3_3)) (P_2_0 -_3_3 (-_3_1 -_3_2 -_3_3))
 (P_2_0 O_3_3 (O_3_3)) (-_2_1 P_S_0 (-_2_1)) (-_2_1 O_0_0 (+_3_3))
 (-_2_1 +_0_1 (+_3_0 +_3_1 P_3_1 -_3_1 +_3_3))
 (-_2_1 P_0_2 (-_3_1))
 (-_2_1 -_0_3 (-_3_1 -_3_2 +_3_3 O_3_3 -_3_3))
 (-_2_1 +_S_1 (P_2_0 -_2_1 +_2_3))
 (-_2_1 -_1_0 (+_3_3 O_2_2 O_2_2 O_S_2 -_1_1 O_0_0 O_0_0))
 (-_2_1 +_1_1
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_1_2 +_S_1
   +_1_3 +_2_3 +_2_3 +_3_3))
 (-_2_1 -_1_1
  (+_3_0 +_0_1 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_1_2 +_S_1
   +_1_3 +_2_3 +_2_3 +_3_3))
 (-_2_1 O_1_1
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3))
 (-_2_1 +_1_2 (+_1_3 P_0_2 P_0_2 -_3_1 P_2_0 P_2_0 P_S_0))
 (-_2_1 +_1_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (-_2_1 -_1_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (-_2_1 P_1_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 -_3_3))
 (-_2_1 O_S_2 (+_2_3)) (-_2_1 P_2_0 (-_1_1))
 (-_2_1 -_2_1 (+_1_1 O_1_1 -_1_1 +_1_2 +_1_3))
 (-_2_1 O_2_2 (+_1_3))
 (-_2_1 +_2_3 (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3))
 (-_2_1 -_S_3 (-_2_1 O_2_2 +_2_3))
 (-_2_1 +_3_0 (P_2_0 P_2_0 -_1_1 +_3_3))
 (-_2_1 +_3_1
  (+_3_0 -_1_1 -_2_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_3))
 (-_2_1 -_3_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_2_1 -_3_1 +_1_2 +_1_3))
 (-_2_1 P_3_1 (-_1_1 -_2_1 -_2_1 -_3_1))
 (-_2_1 -_3_2 (-_3_1 O_2_2 O_2_2 +_1_3))
 (-_2_1 +_3_3
  (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_2_3 +_2_3 +_3_3))
 (-_2_1 -_3_3
  (-_3_1 -_3_2 +_1_3 +_2_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (-_2_1 O_3_3 (+_1_3 +_2_3 +_2_3 +_3_3)) (O_2_2 P_S_0 (O_2_2))
 (O_2_2 O_0_0 (P_2_0 P_2_0)) (O_2_2 +_0_1 (-_2_1 -_2_1))
 (O_2_2 P_0_2 (O_2_2 O_2_2)) (O_2_2 -_0_3 (+_2_3 +_2_3))
 (O_2_2 +_S_1 (-_2_1)) (O_2_2 -_1_0 (+_3_3)) (O_2_2 +_1_1 (-_3_1))
 (O_2_2 -_1_1 (+_3_0 +_3_1 +_3_3)) (O_2_2 O_1_1 (P_3_1))
 (O_2_2 +_1_2 (-_3_1)) (O_2_2 +_1_3 (-_3_1 -_3_2 -_3_3))
 (O_2_2 -_1_3 (+_3_3)) (O_2_2 P_1_3 (O_3_3)) (O_2_2 O_S_2 (P_2_0))
 (O_2_2 P_2_0 (O_0_0 O_0_0 O_S_2 O_2_2 O_2_2))
 (O_2_2 -_2_1 (+_0_1 +_0_1 +_S_1 +_2_3 +_2_3))
 (O_2_2 O_2_2 (P_S_0 P_2_0 P_2_0 P_0_2 P_0_2))
 (O_2_2 +_2_3 (-_S_3 -_2_1 -_2_1 -_0_3 -_0_3))
 (O_2_2 -_S_3 (+_2_3)) (O_2_2 +_3_0 (-_1_1)) (O_2_2 +_3_1 (-_1_1))
 (O_2_2 -_3_1 (+_1_1 +_1_2 +_1_3)) (O_2_2 P_3_1 (O_1_1))
 (O_2_2 -_3_2 (+_1_3)) (O_2_2 +_3_3 (-_1_0 -_1_1 -_1_3))
 (O_2_2 -_3_3 (+_1_3)) (O_2_2 O_3_3 (P_1_3)) (+_2_3 P_S_0 (+_2_3))
 (+_2_3 O_0_0 (-_1_1))
 (+_2_3 +_0_1 (+_1_1 O_1_1 -_1_1 +_1_2 +_1_3))
 (+_2_3 P_0_2 (+_1_3))
 (+_2_3 -_0_3 (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3))
 (+_2_3 +_S_1 (-_2_1 O_2_2 +_2_3))
 (+_2_3 -_1_0 (P_2_0 P_2_0 -_1_1 +_3_3))
 (+_2_3 +_1_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_2_1 -_3_1 +_1_2 +_1_3))
 (+_2_3 -_1_1
  (+_3_0 -_1_1 -_2_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_3))
 (+_2_3 O_1_1 (-_1_1 -_2_1 -_2_1 -_3_1))
 (+_2_3 +_1_2 (-_3_1 O_2_2 O_2_2 +_1_3))
 (+_2_3 +_1_3
  (-_3_1 -_3_2 +_1_3 +_2_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (+_2_3 -_1_3
  (-_1_0 -_1_1 +_1_3 P_1_3 -_1_3 +_2_3 +_2_3 +_3_3))
 (+_2_3 P_1_3 (+_1_3 +_2_3 +_2_3 +_3_3)) (+_2_3 O_S_2 (-_2_1))
 (+_2_3 P_2_0 (+_3_3))
 (+_2_3 -_2_1 (+_3_0 +_3_1 P_3_1 -_3_1 +_3_3))
 (+_2_3 O_2_2 (-_3_1))
 (+_2_3 +_2_3 (-_3_1 -_3_2 +_3_3 O_3_3 -_3_3))
 (+_2_3 -_S_3 (P_2_0 -_2_1 +_2_3))
 (+_2_3 +_3_0 (+_3_3 O_2_2 O_2_2 O_S_2 -_1_1 O_0_0 O_0_0))
 (+_2_3 +_3_1
  (+_3_0 +_0_1 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_1_2 +_S_1
   +_1_3 +_2_3 +_2_3 +_3_3))
 (+_2_3 -_3_1
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_1_2 +_S_1
   +_1_3 +_2_3 +_2_3 +_3_3))
 (+_2_3 P_3_1
  (+_3_0 +_0_1 +_0_1 +_1_1 +_3_1 +_1_2 +_S_1 +_1_3 +_2_3
   +_2_3 +_3_3))
 (+_2_3 -_3_2 (+_1_3 P_0_2 P_0_2 -_3_1 P_2_0 P_2_0 P_S_0))
 (+_2_3 +_3_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (+_2_3 -_3_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   +_1_3 P_1_3 -_1_3 -_3_3))
 (+_2_3 O_3_3
  (-_1_0 -_S_3 -_1_1 -_2_1 -_2_1 -_3_1 -_3_2 -_0_3 -_0_3
   -_1_3 -_3_3))
 (-_S_3 P_S_0 (-_S_3)) (-_S_3 O_0_0 (+_3_0))
 (-_S_3 +_0_1 (+_3_1 P_3_1 -_3_1)) (-_S_3 P_0_2 (-_3_2))
 (-_S_3 -_0_3 (+_3_3 O_3_3 -_3_3))
 (-_S_3 +_S_1 (P_S_0 -_S_3 +_S_1))
 (-_S_3 -_1_0 (O_0_0 -_1_0 +_3_0))
 (-_S_3 +_1_1 (-_3_1 P_3_1 +_3_1 +_1_1 +_0_1))
 (-_S_3 -_1_1 (+_3_1 -_1_1 O_1_1 +_1_1 +_0_1))
 (-_S_3 O_1_1 (+_0_1 +_1_1 +_3_1))
 (-_S_3 +_1_2 (P_0_2 +_1_2 -_3_2))
 (-_S_3 +_1_3 (-_3_3 -_1_3 P_1_3 +_1_3 -_0_3))
 (-_S_3 -_1_3 (-_3_3 O_3_3 +_3_3 -_1_3 -_0_3))
 (-_S_3 P_1_3 (-_0_3 -_1_3 -_3_3)) (-_S_3 O_S_2 (+_S_1))
 (-_S_3 P_2_0 (-_1_0)) (-_S_3 -_2_1 (+_1_1 O_1_1 -_1_1))
 (-_S_3 O_2_2 (+_1_2)) (-_S_3 +_2_3 (+_1_3 P_1_3 -_1_3))
 (-_S_3 -_S_3 (-_S_3 O_S_2 +_S_1))
 (-_S_3 +_3_0 (-_1_0 P_2_0 +_3_0))
 (-_S_3 +_3_1 (-_3_1 P_3_1 +_3_1 -_2_1 -_1_1))
 (-_S_3 -_3_1 (-_3_1 -_2_1 -_1_1 O_1_1 +_1_1))
 (-_S_3 P_3_1 (-_1_1 -_2_1 -_3_1))
 (-_S_3 -_3_2 (+_1_2 O_2_2 -_3_2))
 (-_S_3 +_3_3 (+_3_3 +_2_3 -_1_3 P_1_3 +_1_3))
 (-_S_3 -_3_3 (-_3_3 O_3_3 +_3_3 +_2_3 +_1_3))
 (-_S_3 O_3_3 (+_1_3 +_2_3 +_3_3)) (+_3_0 P_S_0 (+_3_0))
 (+_3_0 O_0_0 (-_1_0 -_1_0 -_S_3 -_3_2 -_3_2))
 (+_3_0 +_0_1
  (-_S_3 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 O_S_2 +_S_1 +_3_3
   O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 P_0_2 (+_3_0 +_3_0 +_1_2 +_1_2 +_S_1))
 (+_3_0 -_0_3
  (P_S_0 -_S_3 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 +_S_1 +_1_3
   P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (+_3_0 +_S_1 (+_3_3 O_3_3 -_3_3))
 (+_3_0 -_1_0 (-_1_1 -_2_1 +_3_1 P_3_1 -_3_1))
 (+_3_0 +_1_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (+_3_0 -_1_1 (-_1_1 -_2_1 +_3_1 P_3_1 -_3_1))
 (+_3_0 O_1_1 (-_3_1 -_2_1 -_1_1))
 (+_3_0 +_1_2 (+_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 +_1_3 (+_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 -_1_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (+_3_0 P_1_3 (+_3_3 +_2_3 +_1_3)) (+_3_0 O_S_2 (-_3_2))
 (+_3_0 P_2_0 (+_3_0 +_3_0))
 (+_3_0 -_2_1 (+_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1))
 (+_3_0 O_2_2 (-_3_2 -_3_2))
 (+_3_0 +_2_3 (+_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 -_S_3 (+_3_1 P_3_1 -_3_1))
 (+_3_0 +_3_0 (-_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 +_3_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (+_3_0 -_3_1 (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1))
 (+_3_0 P_3_1 (+_3_1 +_1_1 +_0_1))
 (+_3_0 -_3_2 (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1))
 (+_3_0 +_3_3 (-_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (+_3_0 -_3_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (+_3_0 O_3_3 (-_3_3 -_1_3 -_0_3)) (+_3_1 P_S_0 (+_3_1))
 (-_3_1 P_S_0 (-_3_1)) (P_3_1 P_S_0 (P_3_1))
 (+_3_1 O_0_0 (-_0_3 -_1_3 -_3_3)) (-_3_1 O_0_0 (+_3_3))
 (P_3_1 O_0_0 (O_3_3))
 (+_3_1 +_0_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (-_3_1 +_0_1 (+_3_0 +_3_1 P_3_1 -_3_1 +_3_3))
 (P_3_1 +_0_1 (+_3_3 +_3_1 +_3_0))
 (+_3_1 P_0_2 (+_0_1 +_1_1 +_3_1)) (-_3_1 P_0_2 (-_3_1))
 (P_3_1 P_0_2 (P_3_1))
 (+_3_1 -_0_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (-_3_1 -_0_3 (-_3_1 -_3_2 +_3_3 O_3_3 -_3_3))
 (P_3_1 -_0_3 (-_3_3 -_3_2 -_3_1))
 (+_3_1 +_S_1 (-_3_3 O_3_3 +_3_3 +_3_1 +_3_0))
 (-_3_1 +_S_1 (+_3_3 -_3_1 P_3_1 +_3_1 +_3_0))
 (P_3_1 +_S_1 (+_3_0 +_3_1 +_3_3))
 (+_3_1 -_1_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_3_2 -_0_3 -_1_3 -_3_3))
 (-_3_1 -_1_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (P_3_1 -_1_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 -_3_3))
 (+_3_1 +_1_1
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 -_3_1 +_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   +_1_3 -_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_3_1 -_1_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 P_3_1 +_3_1 -_2_1
   -_1_1 -_1_1 -_S_3 -_1_0))
 (+_3_1 O_1_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (-_3_1 +_1_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 -_3_1 P_3_1 +_3_1
   +_1_1 +_1_1 +_0_1 +_3_0))
 (-_3_1 -_1_1
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 -_3_1 +_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   +_1_3 -_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_3_1 O_1_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (P_3_1 +_1_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (P_3_1 -_1_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (P_3_1 O_1_1 (O_3_3 O_3_3 O_2_2 O_S_2 O_1_1 O_1_1 O_0_0))
 (+_3_1 +_1_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (-_3_1 +_1_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_1_2 +_1_2
   +_S_1 +_1_3 +_2_3 +_3_3))
 (P_3_1 +_1_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3))
 (+_3_1 +_1_3
  (-_3_3 O_3_3 +_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1
   +_3_1 +_1_1 +_0_1 +_3_0))
 (+_3_1 -_1_3
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 -_1_1 +_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3 -_3_3))
 (+_3_1 P_1_3
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (-_3_1 +_1_3
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 -_1_1 +_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3 -_3_3))
 (-_3_1 -_1_3
  (-_3_3 O_3_3 +_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1
   -_2_1 -_1_1 -_S_3 -_1_0))
 (-_3_1 P_1_3
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (P_3_1 +_1_3
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (P_3_1 -_1_3
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (P_3_1 P_1_3 (P_1_3 P_1_3 P_0_2 P_3_1 P_3_1 P_2_0 P_S_0))
 (+_3_1 O_S_2 (-_3_3)) (-_3_1 O_S_2 (+_3_3)) (P_3_1 O_S_2 (O_3_3))
 (+_3_1 P_2_0 (+_3_1)) (-_3_1 P_2_0 (-_1_1 -_2_1 -_3_1))
 (P_3_1 P_2_0 (P_3_1))
 (+_3_1 -_2_1 (+_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (-_3_1 -_2_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (P_3_1 -_2_1 (-_3_3 -_3_2 -_3_1)) (+_3_1 O_2_2 (-_3_3))
 (-_3_1 O_2_2 (+_1_3 +_2_3 +_3_3)) (P_3_1 O_2_2 (O_3_3))
 (+_3_1 +_2_3 (+_3_0 +_3_1 +_3_3 O_3_3 -_3_3))
 (-_3_1 +_2_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (P_3_1 +_2_3 (+_3_3 +_3_1 +_3_0))
 (+_3_1 -_S_3 (-_3_3 -_3_2 -_3_1 P_3_1 +_3_1))
 (-_3_1 -_S_3 (-_3_3 O_3_3 +_3_3 -_3_2 -_3_1))
 (P_3_1 -_S_3 (-_3_1 -_3_2 -_3_3))
 (+_3_1 +_3_0
  (+_3_0 +_3_0 +_3_1 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (-_3_1 +_3_0
  (+_3_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_3))
 (P_3_1 +_3_0 (+_3_0 +_3_0 +_3_1 +_3_3))
 (+_3_1 +_3_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_3_1 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (+_3_1 -_3_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_3_3))
 (+_3_1 P_3_1 (+_0_1 +_1_1 +_3_1 +_3_1))
 (-_3_1 +_3_1
  (+_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1
   +_3_3))
 (-_3_1 -_3_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (-_3_1 P_3_1 (-_1_1 -_2_1 -_3_1 -_3_1))
 (P_3_1 +_3_1 (+_3_0 +_3_1 +_3_1 +_3_3))
 (P_3_1 -_3_1 (-_3_1 -_3_1 -_3_2 -_3_3)) (P_3_1 P_3_1 (P_3_1 P_3_1))
 (+_3_1 -_3_2
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 -_3_2 -_3_2 -_3_3))
 (-_3_1 -_3_2
  (-_3_1 -_3_2 -_3_2 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (P_3_1 -_3_2 (-_3_1 -_3_2 -_3_2 -_3_3))
 (+_3_1 +_3_3
  (+_3_0 +_3_1 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3
   -_3_3))
 (+_3_1 -_3_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3 -_3_3))
 (+_3_1 O_3_3 (-_0_3 -_1_3 -_3_3 -_3_3))
 (-_3_1 +_3_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3 +_3_3))
 (-_3_1 -_3_3
  (-_3_1 -_3_2 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3
   -_3_3))
 (-_3_1 O_3_3 (+_1_3 +_2_3 +_3_3 +_3_3))
 (P_3_1 +_3_3 (+_3_0 +_3_1 +_3_3 +_3_3))
 (P_3_1 -_3_3 (-_3_1 -_3_2 -_3_3 -_3_3)) (P_3_1 O_3_3 (O_3_3 O_3_3))
 (-_3_2 P_S_0 (-_3_2)) (-_3_2 O_0_0 (+_3_0 +_3_0))
 (-_3_2 +_0_1 (+_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1))
 (-_3_2 P_0_2 (-_3_2 -_3_2))
 (-_3_2 -_0_3 (+_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 +_S_1 (+_3_1 P_3_1 -_3_1))
 (-_3_2 -_1_0 (-_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 +_1_1 (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1))
 (-_3_2 -_1_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (-_3_2 O_1_1 (+_3_1 +_1_1 +_0_1))
 (-_3_2 +_1_2 (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1))
 (-_3_2 +_1_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (-_3_2 -_1_3 (-_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 P_1_3 (-_3_3 -_1_3 -_0_3)) (-_3_2 O_S_2 (+_3_0))
 (-_3_2 P_2_0 (-_1_0 -_1_0 -_S_3 -_3_2 -_3_2))
 (-_3_2 -_2_1
  (-_S_3 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1 -_1_1 O_S_2 +_S_1 +_3_3
   O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 O_2_2 (+_3_0 +_3_0 +_1_2 +_1_2 +_S_1))
 (-_3_2 +_2_3
  (P_S_0 -_S_3 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 +_S_1 +_1_3
   P_1_3 -_1_3 +_1_3 P_1_3 -_1_3))
 (-_3_2 -_S_3 (+_3_3 O_3_3 -_3_3))
 (-_3_2 +_3_0 (-_1_1 -_2_1 +_3_1 P_3_1 -_3_1))
 (-_3_2 +_3_1 (-_1_1 -_2_1 +_3_1 P_3_1 -_3_1))
 (-_3_2 -_3_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (-_3_2 P_3_1 (-_3_1 -_2_1 -_1_1))
 (-_3_2 -_3_2 (+_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 +_3_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (-_3_2 -_3_3 (+_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (-_3_2 O_3_3 (+_3_3 +_2_3 +_1_3)) (+_3_3 P_S_0 (+_3_3))
 (-_3_3 P_S_0 (-_3_3)) (O_3_3 P_S_0 (O_3_3))
 (+_3_3 O_0_0 (-_1_1 -_2_1 -_3_1)) (-_3_3 O_0_0 (+_3_1))
 (O_3_3 O_0_0 (P_3_1))
 (+_3_3 +_0_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3 +_2_3
   +_3_3 O_3_3 -_3_3))
 (-_3_3 +_0_1 (+_3_1 P_3_1 -_3_1 -_3_2 -_3_3))
 (O_3_3 +_0_1 (-_3_3 -_3_2 -_3_1))
 (+_3_3 P_0_2 (+_1_3 +_2_3 +_3_3)) (-_3_3 P_0_2 (-_3_3))
 (O_3_3 P_0_2 (O_3_3))
 (+_3_3 -_0_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3))
 (-_3_3 -_0_3 (+_3_0 +_3_1 +_3_3 O_3_3 -_3_3))
 (O_3_3 -_0_3 (+_3_3 +_3_1 +_3_0))
 (+_3_3 +_S_1 (-_3_3 O_3_3 +_3_3 -_3_2 -_3_1))
 (-_3_3 +_S_1 (-_3_3 -_3_2 -_3_1 P_3_1 +_3_1))
 (O_3_3 +_S_1 (-_3_1 -_3_2 -_3_3))
 (+_3_3 -_1_0
  (+_3_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_3))
 (-_3_3 -_1_0
  (+_3_0 +_3_0 +_3_1 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3))
 (O_3_3 -_1_0 (+_3_0 +_3_0 +_3_1 +_3_3))
 (+_3_3 +_1_1
  (+_1_1 O_1_1 -_1_1 -_2_1 -_3_1 -_3_1 +_1_2 O_2_2 -_3_2 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (+_3_3 -_1_1
  (+_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1
   +_3_3))
 (+_3_3 O_1_1 (-_1_1 -_2_1 -_3_1 -_3_1))
 (-_3_3 +_1_1
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_3_3))
 (-_3_3 -_1_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 +_3_1 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (-_3_3 O_1_1 (+_0_1 +_1_1 +_3_1 +_3_1))
 (O_3_3 +_1_1 (-_3_1 -_3_1 -_3_2 -_3_3))
 (O_3_3 -_1_1 (+_3_0 +_3_1 +_3_1 +_3_3)) (O_3_3 O_1_1 (P_3_1 P_3_1))
 (+_3_3 +_1_2
  (-_3_1 -_3_2 -_3_2 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3))
 (-_3_3 +_1_2
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 -_3_2 -_3_2 -_3_3))
 (O_3_3 +_1_2 (-_3_1 -_3_2 -_3_2 -_3_3))
 (+_3_3 +_1_3
  (-_3_1 -_3_2 +_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3
   -_3_3))
 (+_3_3 -_1_3
  (-_1_0 P_2_0 +_3_0 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 +_1_3 P_1_3
   -_1_3 +_2_3 +_3_3 +_3_3))
 (+_3_3 P_1_3 (+_1_3 +_2_3 +_3_3 +_3_3))
 (-_3_3 +_1_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3 -_3_3))
 (-_3_3 -_1_3
  (+_3_0 +_3_1 -_0_3 -_1_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3
   -_3_3))
 (-_3_3 P_1_3 (-_0_3 -_1_3 -_3_3 -_3_3))
 (O_3_3 +_1_3 (-_3_1 -_3_2 -_3_3 -_3_3))
 (O_3_3 -_1_3 (+_3_0 +_3_1 +_3_3 +_3_3)) (O_3_3 P_1_3 (O_3_3 O_3_3))
 (+_3_3 O_S_2 (-_3_1)) (-_3_3 O_S_2 (+_3_1)) (O_3_3 O_S_2 (P_3_1))
 (+_3_3 P_2_0 (+_3_3)) (-_3_3 P_2_0 (-_0_3 -_1_3 -_3_3))
 (O_3_3 P_2_0 (O_3_3))
 (+_3_3 -_2_1 (+_3_0 +_3_1 P_3_1 -_3_1 +_3_3))
 (-_3_3 -_2_1
  (O_0_0 -_1_0 +_3_0 +_0_1 +_1_1 O_1_1 -_1_1 +_3_1 -_0_3 -_1_3
   +_3_3 O_3_3 -_3_3))
 (O_3_3 -_2_1 (+_3_3 +_3_1 +_3_0)) (+_3_3 O_2_2 (-_3_1))
 (-_3_3 O_2_2 (+_0_1 +_1_1 +_3_1)) (O_3_3 O_2_2 (P_3_1))
 (+_3_3 +_2_3 (-_3_1 -_3_2 +_3_3 O_3_3 -_3_3))
 (-_3_3 +_2_3
  (+_0_1 +_1_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 -_0_3 +_1_3
   P_1_3 -_1_3 -_3_3))
 (O_3_3 +_2_3 (-_3_3 -_3_2 -_3_1))
 (+_3_3 -_S_3 (+_3_3 -_3_1 P_3_1 +_3_1 +_3_0))
 (-_3_3 -_S_3 (-_3_3 O_3_3 +_3_3 +_3_1 +_3_0))
 (O_3_3 -_S_3 (+_3_0 +_3_1 +_3_3))
 (+_3_3 +_3_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 +_3_3 O_3_3 -_3_3))
 (-_3_3 +_3_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 +_3_1 P_3_1 -_3_1 -_3_2
   -_3_2 -_0_3 -_1_3 -_3_3))
 (O_3_3 +_3_0
  (-_1_0 -_1_0 -_S_3 -_1_1 -_2_1 -_3_1 -_3_2 -_3_2 -_0_3
   -_1_3 -_3_3))
 (+_3_3 +_3_1
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 -_3_1 +_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   +_1_3 -_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (+_3_3 -_3_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 -_3_1 P_3_1 +_3_1
   +_1_1 +_1_1 +_0_1 +_3_0))
 (+_3_3 P_3_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (-_3_3 +_3_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 P_3_1 +_3_1 -_2_1
   -_1_1 -_1_1 -_S_3 -_1_0))
 (-_3_3 -_3_1
  (O_0_0 -_1_0 +_3_0 -_S_3 +_0_1 +_1_1 O_1_1 -_1_1 +_1_1 O_1_1
   -_1_1 -_2_1 -_3_1 +_3_1 O_S_2 +_1_2 O_2_2 -_3_2 +_S_1 -_0_3
   +_1_3 -_1_3 +_2_3 +_3_3 O_3_3 -_3_3 +_3_3 O_3_3 -_3_3))
 (-_3_3 P_3_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (O_3_3 +_3_1
  (-_3_3 -_3_3 -_1_3 -_0_3 -_3_2 -_3_1 -_2_1 -_1_1 -_1_1
   -_S_3 -_1_0))
 (O_3_3 -_3_1
  (+_3_3 +_3_3 +_2_3 +_1_3 +_S_1 +_1_2 +_3_1 +_1_1 +_1_1
   +_0_1 +_3_0))
 (O_3_3 P_3_1 (O_3_3 O_3_3 O_2_2 O_S_2 O_1_1 O_1_1 O_0_0))
 (+_3_3 -_3_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 P_3_1 -_3_1 +_1_2 +_1_2
   +_S_1 +_1_3 +_2_3 +_3_3))
 (-_3_3 -_3_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3 O_3_3 -_3_3))
 (O_3_3 -_3_2
  (+_3_0 +_3_0 +_0_1 +_1_1 +_3_1 +_1_2 +_1_2 +_S_1 +_1_3
   +_2_3 +_3_3))
 (+_3_3 +_3_3
  (-_3_3 O_3_3 +_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1
   -_2_1 -_1_1 -_S_3 -_1_0))
 (+_3_3 -_3_3
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 -_1_1 +_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3 -_3_3))
 (+_3_3 O_3_3
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (-_3_3 +_3_3
  (P_S_0 -_1_0 P_2_0 +_3_0 -_S_3 +_0_1 -_1_1 +_1_1 -_2_1 +_3_1
   P_3_1 -_3_1 +_3_1 P_3_1 -_3_1 P_0_2 +_1_2 -_3_2 +_S_1 -_0_3
   +_1_3 P_1_3 -_1_3 +_1_3 P_1_3 -_1_3 +_2_3 +_3_3 -_3_3))
 (-_3_3 -_3_3
  (-_3_3 O_3_3 +_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1
   +_3_1 +_1_1 +_0_1 +_3_0))
 (-_3_3 O_3_3
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (O_3_3 +_3_3
  (-_3_3 -_1_3 -_1_3 -_0_3 -_3_2 -_3_1 -_3_1 -_2_1 -_1_1
   -_S_3 -_1_0))
 (O_3_3 -_3_3
  (+_3_3 +_2_3 +_1_3 +_1_3 +_S_1 +_1_2 +_3_1 +_3_1 +_1_1
   +_0_1 +_3_0))
 (O_3_3 O_3_3 (P_1_3 P_1_3 P_0_2 P_3_1 P_3_1 P_2_0 P_S_0))))
