dwolter_SparQ/Calculi/tpcc.lisp
;;; 
;;; Ternary Point Configuration Calculus
;;;

(def-calculus "Ternary Point Configuration Calculus (TPCC)"
  :arity :ternary
  :basis-entity :2d-point
  :consistency :unknown
  :qualifier (external-lib "libtpcc.dylib" "tpcc_qualify")
  :identity-relation sam
  :inverse-operation ( ( dou dou )
		       ( tri tri )
		       ( sam dsf )
		       ( csb dsf )
		       ( dsb dsf )
		       ( clb drf )
		       ( dlb drf )
		       ( cbl drf )
		       ( dbl dfr drf )
		       ( csl drf )
		       ( dsl dfr drf )
		       ( cfl cfr crf dfr drf )
		       ( dfl cfr dbr dfr dsr )
		       ( clf cfr crf )
		       ( dlf cbr cfr crb csr dbr drb )
		       ( csf csf )
		       ( dsf csb dsb sam )
		       ( crf cfl clf )
		       ( drf cbl cfl clb csl dbl dlb )
		       ( cfr cfl clf dfl dlf )
		       ( dfr cfl dbl dfl dsl )
		       ( csr dlf )
		       ( dsr dfl dlf )
		       ( cbr dlf )
		       ( dbr dfl dlf )
		       ( crb dlf )
		       ( drb dlf ))

  
  :shortcut-operation ( (dou dsf )
			(tri tri )
			(sam sam )
			(csb csf )
			(dsb csf )
			(clb cfr crf )
			(dlb crf )
			(cbl cfr crf csr )
			(dbl crf )
			(csl cfr csr )
			(dsl crf )
			(cfl cbr cfr csr dfr )
			(dfl cfr crf dfr drf )
			(clf cbr crb dbr dfr drb dsr )
			(dlf dfr drf )
			(csf csb dsb )
			(dsf dou drf )
			(crf cbl clb dbl dfl dlb dsl )
			(drf dfl dlf drf dsf )
			(cfr cbl cfl csl dfl )
			(dfr cfl clf dfl dlf )
			(csr cfl csl )
			(dsr clf )
			(cbr cfl clf csl )
			(dbr clf )
			(crb cfl clf )
			(drb clf))

  
  :homing-operation ( (dou dou )
		      (tri tri )
		      (sam dou )
		      (csb dsf )
		      (dsb dsf )
		      (clb dlf )
		      (dlb dlf )
		      (cbl dfl dlf )
		      (dbl dlf )
		      (csl dfl )
		      (dsl dlf )
		      (cfl cfl dbl dfl dsl )
		      (dfl cfl clf dfl dlf )
		      (clf cbl cfl clb csl dbl dlb )
		      (dlf cfl clf )
		      (csf clb dlb )
		      (dsf clf csl )
		      (crf cbr cfr clb crb csb csr dbr dlb drb dsb )
		      (drf cfr clf crf csf )
		      (cfr cfr dbr dfr dsr )
		      (dfr cfr crf dfr drf )
		      (csr dfr )
		      (dsr dfr drf )
		      (cbr dfr drf )
		      (dbr drf )
		      (crb drf )
		      (drb drf ))
  
  :base-relations ( tri dou sam csb dsb clb dlb cbl dbl csl dsl cfl dfl clf dlf csf dsf crf drf cfr dfr csr dsr cbr dbr crb drb )

  
  :composition-operation ( (tri tri ( tri ))
			   (tri dou ( dou ))
			   (dou sam ( dou ))
			   (dou csb ( dou ))
			   (dou dsb ( dou ))
			   (dou clb ( dou ))
			   (dou dlb ( dou ))
			   (dou cbl ( dou ))
			   (dou dbl ( dou ))
			   (dou csl ( dou ))
			   (dou dsl ( dou ))
			   (dou cfl ( dou ))
			   (dou dfl ( dou ))
			   (dou clf ( dou ))
			   (dou dlf ( dou ))
			   (dou csf ( dou ))
			   (dou dsf ( dou ))
			   (dou crf ( dou ))
			   (dou drf ( dou ))
			   (dou cfr ( dou ))
			   (dou dfr ( dou ))
			   (dou csr ( dou ))
			   (dou dsr ( dou ))
			   (dou cbr ( dou ))
			   (dou dbr ( dou ))
			   (dou crb ( dou ))
			   (dou drb ( dou ))
			   (sam tri ( sam ))
			   (sam dou ( sam csb dsb clb dlb cbl dbl csl dsl cfl dfl clf dlf csf dsf crf drf cfr dfr csr dsr cbr dbr crb drb ))
			   (csb sam ( csb ))
			   (csb csb ( csb dsb ))
			   (csb dsb ( csb dsb ))
			   (csb clb ( clb dlb ))
			   (csb dlb ( clb dlb ))
			   (csb cbl ( clb dlb ))
			   (csb dbl ( cbl clb dbl dlb ))
			   (csb csl ( clb dlb ))
			   (csb dsl ( cbl clb dbl dlb ))
			   (csb cfl ( cbl clb dbl dlb ))
			   (csb dfl ( cbl cfl csl dbl dfl dsl ))
			   (csb clf ( cbl clb ))
			   (csb dlf ( cbl cfl clf csl dfl dlf ))
			   (csb csf ( csb ))
			   (csb dsf ( csf dsf sam ))
			   (csb crf ( cbr crb ))
			   (csb drf ( cbr cfr crf csr dfr drf ))
			   (csb cfr ( cbr crb dbr drb ))
			   (csb dfr ( cbr cfr csr dbr dfr dsr ))
			   (csb csr ( crb drb ))
			   (csb dsr ( cbr crb dbr drb ))
			   (csb cbr ( crb drb ))
			   (csb dbr ( cbr crb dbr drb ))
			   (csb crb ( crb drb ))
			   (csb drb ( crb drb ))
			   (dsb sam ( dsb ))
			   (dsb csb ( dsb ))
			   (dsb dsb ( dsb ))
			   (dsb clb ( dlb ))
			   (dsb dlb ( dlb ))
			   (dsb cbl ( dlb ))
			   (dsb dbl ( dbl dlb ))
			   (dsb csl ( dlb ))
			   (dsb dsl ( dbl dlb ))
			   (dsb cfl ( cbl clb dbl dlb ))
			   (dsb dfl ( cbl dbl dfl dsl ))
			   (dsb clf ( cbl clb dbl dlb ))
			   (dsb dlf ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (dsb csf ( csb dsb ))
			   (dsb dsf ( csf dsf sam ))
			   (dsb crf ( cbr crb dbr drb ))
			   (dsb drf ( cbr cfr crf csr dbr dfr drf dsr ))
			   (dsb cfr ( cbr crb dbr drb ))
			   (dsb dfr ( cbr dbr dfr dsr ))
			   (dsb csr ( drb ))
			   (dsb dsr ( dbr drb ))
			   (dsb cbr ( drb ))
			   (dsb dbr ( dbr drb ))
			   (dsb crb ( drb ))
			   (dsb drb ( drb ))
			   (clb sam ( clb ))
			   (clb csb ( clb dlb ))
			   (clb dsb ( clb dlb ))
			   (clb clb ( cbl clb dbl dlb ))
			   (clb dlb ( cbl clb dbl dlb ))
			   (clb cbl ( cbl clb dbl dlb ))
			   (clb dbl ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (clb csl ( cbl clb dbl dlb ))
			   (clb dsl ( cbl cfl csl dbl dfl dsl ))
			   (clb cfl ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (clb dfl ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (clb clf ( cbl cfl clb csl ))
			   (clb dlf ( cbl cfl clf crf csf csl dfl dlf drf dsf ))
			   (clb csf ( clb ))
			   (clb dsf ( crf drf sam ))
			   (clb crf ( cbr clb crb csb ))
			   (clb drf ( cbr cfr crb crf csr dbr dfr drf dsr ))
			   (clb cfr ( cbr clb crb csb dbr dlb drb dsb ))
			   (clb dfr ( cbr cfr crb csr dbr dfr drb dsr ))
			   (clb csr ( clb crb csb dlb drb dsb ))
			   (clb dsr ( cbr crb csb dbr drb dsb ))
			   (clb cbr ( clb crb csb dlb drb dsb ))
			   (clb dbr ( cbr clb crb csb dbr dlb drb dsb ))
			   (clb crb ( clb crb csb dlb drb dsb ))
			   (clb drb ( clb crb csb dlb drb dsb ))
			   (dlb sam ( dlb ))
			   (dlb csb ( dlb ))
			   (dlb dsb ( dlb ))
			   (dlb clb ( dbl dlb ))
			   (dlb dlb ( dbl dlb ))
			   (dlb cbl ( dbl dlb ))
			   (dlb dbl ( dbl dfl dlb dsl ))
			   (dlb csl ( dbl dlb ))
			   (dlb dsl ( dbl dfl dsl ))
			   (dlb cfl ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (dlb dfl ( cbl cfl csl dbl dfl dlf dsl ))
			   (dlb clf ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (dlb dlf ( cbl cfl clf crf csf csl dbl dfl dlf drf dsf dsl ))
			   (dlb csf ( clb dlb ))
			   (dlb dsf ( crf drf sam ))
			   (dlb crf ( cbr clb crb csb dbr dlb drb dsb ))
			   (dlb drf ( cbr cfr crb crf csr dbr dfr drb drf dsr ))
			   (dlb cfr ( cbr clb crb csb dbr dlb drb dsb ))
			   (dlb dfr ( cbr crb dbr dfr drb dsr ))
			   (dlb csr ( clb dlb drb dsb ))
			   (dlb dsr ( dbr drb dsb ))
			   (dlb cbr ( dlb drb dsb ))
			   (dlb dbr ( dbr dlb drb dsb ))
			   (dlb crb ( dlb drb dsb ))
			   (dlb drb ( dlb drb dsb ))
			   (cbl sam ( cbl ))
			   (cbl csb ( cbl dbl ))
			   (cbl dsb ( cbl dbl ))
			   (cbl clb ( cbl cfl csl dbl dfl dsl ))
			   (cbl dlb ( cbl cfl csl dbl dfl dsl ))
			   (cbl cbl ( cbl cfl csl dbl dfl dsl ))
			   (cbl dbl ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (cbl csl ( cbl cfl csl dbl dfl dsl ))
			   (cbl dsl ( cfl clf dfl dlf ))
			   (cbl cfl ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (cbl dfl ( cfl clf crf csf dfl dlf drf dsf ))
			   (cbl clf ( cbl cfl clf csl ))
			   (cbl dlf ( cfl cfr clf crf csf dfr dlf drf dsf ))
			   (cbl csf ( cbl ))
			   (cbl dsf ( cfr dfr sam ))
			   (cbl crf ( cbl clb crb csb ))
			   (cbl drf ( cbr cfr clb crb csb csr dbr dfr drb dsr ))
			   (cbl cfr ( cbl clb crb csb dbl dlb drb dsb ))
			   (cbl dfr ( cbr clb crb csb dbr dlb drb dsb ))
			   (cbl csr ( cbl clb dbl dlb ))
			   (cbl dsr ( clb crb csb dlb drb dsb ))
			   (cbl cbr ( cbl clb dbl dlb ))
			   (cbl dbr ( cbl clb crb csb dbl dlb drb dsb ))
			   (cbl crb ( cbl clb dbl dlb ))
			   (cbl drb ( cbl clb dbl dlb ))
			   (dbl sam ( dbl ))
			   (dbl csb ( dbl ))
			   (dbl dsb ( dbl ))
			   (dbl clb ( dbl dfl dsl ))
			   (dbl dlb ( dbl dfl dsl ))
			   (dbl cbl ( dbl dfl dsl ))
			   (dbl dbl ( dbl dfl dlf dsl ))
			   (dbl csl ( dbl dfl dsl ))
			   (dbl dsl ( dfl dlf ))
			   (dbl cfl ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (dbl dfl ( cfl clf dfl dlf drf dsf ))
			   (dbl clf ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (dbl dlf ( cfl cfr clf crf csf dfl dfr dlf drf dsf ))
			   (dbl csf ( cbl dbl ))
			   (dbl dsf ( cfr dfr sam ))
			   (dbl crf ( cbl clb crb csb dbl dlb drb dsb ))
			   (dbl drf ( cbr cfr clb crb csb csr dbr dfr dlb drb dsb dsr ))
			   (dbl cfr ( cbl clb crb csb dbl dlb drb dsb ))
			   (dbl dfr ( clb crb csb dbr dlb drb dsb ))
			   (dbl csr ( dbl dlb ))
			   (dbl dsr ( dlb drb dsb ))
			   (dbl cbr ( dbl dlb ))
			   (dbl dbr ( dbl dlb drb dsb ))
			   (dbl crb ( dbl dlb ))
			   (dbl drb ( dbl dlb ))
			   (csl sam ( csl ))
			   (csl csb ( csl dsl ))
			   (csl dsb ( csl dsl ))
			   (csl clb ( cfl dfl ))
			   (csl dlb ( cfl dfl ))
			   (csl cbl ( cfl dfl ))
			   (csl dbl ( cfl clf dfl dlf ))
			   (csl csl ( cfl dfl ))
			   (csl dsl ( clf dlf ))
			   (csl cfl ( cfl clf dfl dlf ))
			   (csl dfl ( clf crf csf dlf drf dsf ))
			   (csl clf ( cfl clf ))
			   (csl dlf ( cfr clf crf csf dfr drf ))
			   (csl csf ( csl ))
			   (csl dsf ( csr dsr sam ))
			   (csl crf ( cbl clb ))
			   (csl drf ( cbr clb crb csb dbr drb ))
			   (csl cfr ( cbl clb dbl dlb ))
			   (csl dfr ( clb crb csb dlb drb dsb ))
			   (csl csr ( cbl dbl ))
			   (csl dsr ( clb dlb ))
			   (csl cbr ( cbl dbl ))
			   (csl dbr ( cbl clb dbl dlb ))
			   (csl crb ( cbl dbl ))
			   (csl drb ( cbl dbl ))
			   (dsl sam ( dsl ))
			   (dsl csb ( dsl ))
			   (dsl dsb ( dsl ))
			   (dsl clb ( dfl ))
			   (dsl dlb ( dfl ))
			   (dsl cbl ( dfl ))
			   (dsl dbl ( dfl dlf ))
			   (dsl csl ( dfl ))
			   (dsl dsl ( dlf ))
			   (dsl cfl ( cfl clf dfl dlf ))
			   (dsl dfl ( clf dlf drf dsf ))
			   (dsl clf ( cfl clf dfl dlf ))
			   (dsl dlf ( cfr clf crf csf dfr dlf drf dsf ))
			   (dsl csf ( csl dsl ))
			   (dsl dsf ( csr dsr sam ))
			   (dsl crf ( cbl clb dbl dlb ))
			   (dsl drf ( cbr clb crb csb dbr dlb drb dsb ))
			   (dsl cfr ( cbl clb dbl dlb ))
			   (dsl dfr ( clb dlb drb dsb ))
			   (dsl csr ( dbl ))
			   (dsl dsr ( dlb ))
			   (dsl cbr ( dbl ))
			   (dsl dbr ( dbl dlb ))
			   (dsl crb ( dbl ))
			   (dsl drb ( dbl ))
			   (cfl sam ( cfl ))
			   (cfl csb ( cfl dfl ))
			   (cfl dsb ( cfl dfl ))
			   (cfl clb ( cfl clf dfl dlf ))
			   (cfl dlb ( cfl clf dfl dlf ))
			   (cfl cbl ( cfl clf dfl dlf ))
			   (cfl dbl ( cfl clf crf csf dfl dlf drf dsf ))
			   (cfl csl ( cfl clf dfl dlf ))
			   (cfl dsl ( clf crf csf dlf drf dsf ))
			   (cfl cfl ( cfl clf crf csf dfl dlf drf dsf ))
			   (cfl dfl ( cfr clf crf csf dfr dlf drf dsf ))
			   (cfl clf ( cfl clf crf csf ))
			   (cfl dlf ( cbr cfr clf crf csf csr dbr dfr drf dsr ))
			   (cfl csf ( cfl ))
			   (cfl dsf ( cbr dbr sam ))
			   (cfl crf ( cbl cfl clb csl ))
			   (cfl drf ( cbl cbr clb crb csb dbr dlb drb dsb ))
			   (cfl cfr ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (cfl dfr ( cbl clb crb csb dbl dlb drb dsb ))
			   (cfl csr ( cbl cfl csl dbl dfl dsl ))
			   (cfl dsr ( cbl clb dbl dlb ))
			   (cfl cbr ( cbl cfl csl dbl dfl dsl ))
			   (cfl dbr ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (cfl crb ( cbl cfl csl dbl dfl dsl ))
			   (cfl drb ( cbl cfl csl dbl dfl dsl ))
			   (dfl sam ( dfl ))
			   (dfl csb ( dfl ))
			   (dfl dsb ( dfl ))
			   (dfl clb ( dfl dlf ))
			   (dfl dlb ( dfl dlf ))
			   (dfl cbl ( dfl dlf ))
			   (dfl dbl ( dfl dlf drf dsf ))
			   (dfl csl ( dfl dlf ))
			   (dfl dsl ( dlf drf dsf ))
			   (dfl cfl ( cfl clf crf csf dfl dlf drf dsf ))
			   (dfl dfl ( clf crf csf dfr dlf drf dsf ))
			   (dfl clf ( cfl clf crf csf dfl dlf drf dsf ))
			   (dfl dlf ( cbr cfr clf crf csf csr dbr dfr dlf drf dsf dsr ))
			   (dfl csf ( cfl dfl ))
			   (dfl dsf ( cbr dbr sam ))
			   (dfl crf ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (dfl drf ( cbl cbr clb crb csb dbl dbr dlb drb dsb ))
			   (dfl cfr ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (dfl dfr ( cbl clb dbl dlb drb dsb ))
			   (dfl csr ( cfl dbl dfl dsl ))
			   (dfl dsr ( dbl dlb ))
			   (dfl cbr ( dbl dfl dsl ))
			   (dfl dbr ( dbl dfl dlb dsl ))
			   (dfl crb ( dbl dfl dsl ))
			   (dfl drb ( dbl dfl dsl ))
			   (clf sam ( clf ))
			   (clf csb ( clf dlf ))
			   (clf dsb ( clf dlf ))
			   (clf clb ( clf crf csf dlf drf dsf ))
			   (clf dlb ( clf crf csf dlf drf dsf ))
			   (clf cbl ( clf crf csf dlf drf dsf ))
			   (clf dbl ( cfr clf crf csf dfr dlf drf dsf ))
			   (clf csl ( clf crf csf dlf drf dsf ))
			   (clf dsl ( cfr crf csf dfr drf dsf ))
			   (clf cfl ( cfr clf crf csf dfr dlf drf dsf ))
			   (clf dfl ( cbr cfr crf csr dbr dfr drf dsr ))
			   (clf clf ( cfr clf crf csf ))
			   (clf dlf ( cbr cfr crb crf csr dbr dfr drb dsr ))
			   (clf csf ( clf ))
			   (clf dsf ( crb drb sam ))
			   (clf crf ( cbl cfl clf csl ))
			   (clf drf ( cbl cfl clb crb csb csl dbl dlb drb dsb ))
			   (clf cfr ( cbl cfl clf csl dbl dfl dlf dsl )) 
			   (clf dfr ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (clf csr ( cfl clf dfl dlf ))
			   (clf dsr ( cbl cfl csl dbl dfl dsl ))
			   (clf cbr ( cfl clf dfl dlf ))
			   (clf dbr ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (clf crb ( cfl clf dfl dlf ))
			   (clf drb ( cfl clf dfl dlf ))
			   (dlf sam ( dlf ))
			   (dlf csb ( dlf ))
			   (dlf dsb ( dlf ))
			   (dlf clb ( dlf drf dsf ))
			   (dlf dlb ( dlf drf dsf ))
			   (dlf cbl ( dlf drf dsf ))
			   (dlf dbl ( dfr dlf drf dsf ))
			   (dlf csl ( dlf drf dsf ))
			   (dlf dsl ( dfr drf dsf ))
			   (dlf cfl ( cfr clf crf csf dfr dlf drf dsf ))
			   (dlf dfl ( cfr crf dbr dfr drf dsr ))
			   (dlf clf ( cfr clf crf csf dfr dlf drf dsf ))
			   (dlf dlf ( cbr cfr crb crf csr dbr dfr drb drf dsr ))
			   (dlf csf ( clf dlf ))
			   (dlf dsf ( crb drb sam ))
			   (dlf crf ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (dlf drf ( cbl cfl clb crb csb csl dbl dfl dlb drb dsb dsl ))
			   (dlf cfr ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (dlf dfr ( cbl cfl csl dbl dfl dlb dsl ))
			   (dlf csr ( dfl dlf ))
			   (dlf dsr ( dbl dfl dsl ))
			   (dlf cbr ( dfl dlf ))
			   (dlf dbr ( dbl dfl dlf dsl ))
			   (dlf crb ( dfl dlf ))
			   (dlf drb ( dfl dlf ))
			   (csf sam ( csf ))
			   (csf csb ( csf dsf ))
			   (csf dsb ( csf dsf ))
			   (csf clb ( crf drf ))
			   (csf dlb ( crf drf ))
			   (csf cbl ( crf drf ))
			   (csf dbl ( cfr crf dfr drf ))
			   (csf csl ( crf drf ))
			   (csf dsl ( cfr crf dfr drf ))
			   (csf cfl ( cfr crf dfr drf ))
			   (csf dfl ( cbr cfr csr dbr dfr dsr ))
			   (csf clf ( cfr crf ))
			   (csf dlf ( cbr cfr crb csr dbr drb ))
			   (csf csf ( csf ))
			   (csf dsf ( csb dsb sam ))
			   (csf crf ( cfl clf ))
			   (csf drf ( cbl cfl clb csl dbl dlb ))
			   (csf cfr ( cfl clf dfl dlf ))
			   (csf dfr ( cbl cfl csl dbl dfl dsl ))
			   (csf csr ( clf dlf ))
			   (csf dsr ( cfl clf dfl dlf ))
			   (csf cbr ( clf dlf ))
			   (csf dbr ( cfl clf dfl dlf ))
			   (csf crb ( clf dlf ))
			   (csf drb ( clf dlf ))
			   (dsf sam ( dsf ))
			   (dsf csb ( dsf ))
			   (dsf dsb ( dsf ))
			   (dsf clb ( drf ))
			   (dsf dlb ( drf ))
			   (dsf cbl ( drf ))
			   (dsf dbl ( dfr drf ))
			   (dsf csl ( drf ))
			   (dsf dsl ( dfr drf ))
			   (dsf cfl ( cfr crf dfr drf ))
			   (dsf dfl ( cfr dbr dfr dsr ))
			   (dsf clf ( cfr crf dfr drf ))
			   (dsf dlf ( cbr cfr crb csr dbr dfr drb dsr ))
			   (dsf csf ( csf dsf ))
			   (dsf dsf ( csb dsb sam ))
			   (dsf crf ( cfl clf dfl dlf ))
			   (dsf drf ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (dsf cfr ( cfl clf dfl dlf ))
			   (dsf dfr ( cfl dbl dfl dsl ))
			   (dsf csr ( dlf ))
			   (dsf dsr ( dfl dlf ))
			   (dsf cbr ( dlf ))
			   (dsf dbr ( dfl dlf ))
			   (dsf crb ( dlf ))
			   (dsf drb ( dlf ))
			   (crf sam ( crf ))
			   (crf csb ( crf drf ))
			   (crf dsb ( crf drf ))
			   (crf clb ( cfr crf dfr drf ))
			   (crf dlb ( cfr crf dfr drf ))
			   (crf cbl ( cfr crf dfr drf ))
			   (crf dbl ( cbr cfr crf csr dbr dfr drf dsr ))
			   (crf csl ( cfr crf dfr drf ))
			   (crf dsl ( cbr cfr csr dbr dfr dsr ))
			   (crf cfl ( cbr cfr crf csr dbr dfr drf dsr ))
			   (crf dfl ( cbr cfr crb csr dbr dfr drb dsr ))
			   (crf clf ( cbr cfr crf csr ))
			   (crf dlf ( cbr cfr clb crb csb csr dbr dlb drb dsb ))
			   (crf csf ( crf ))
			   (crf dsf ( clb dlb sam ))
			   (crf crf ( cfl clf crf csf ))
			   (crf drf ( cbl cfl clb clf csl dbl dfl dlb dsl )) 
			   (crf cfr ( cfl clf crf csf dfl dlf drf dsf ))
			   (crf dfr ( cbl cfl clf csl dbl dfl dlf dsl ))
			   (crf csr ( clf crf csf dlf drf dsf ))
			   (crf dsr ( cfl clf csf dfl dlf dsf ))
			   (crf cbr ( clf crf csf dlf drf dsf ))
			   (crf dbr ( cfl clf crf csf dfl dlf drf dsf ))
			   (crf crb ( clf crf csf dlf drf dsf ))
			   (crf drb ( clf crf csf dlf drf dsf ))
			   (drf sam ( drf ))
			   (drf csb ( drf ))
			   (drf dsb ( drf ))
			   (drf clb ( dfr drf ))
			   (drf dlb ( dfr drf ))
			   (drf cbl ( dfr drf ))
			   (drf dbl ( dbr dfr drf dsr ))
			   (drf csl ( dfr drf ))
			   (drf dsl ( dbr dfr dsr ))
			   (drf cfl ( cbr cfr crf csr dbr dfr drf dsr ))
			   (drf dfl ( cbr cfr csr dbr dfr drb dsr ))
			   (drf clf ( cbr cfr crf csr dbr dfr drf dsr ))
			   (drf dlf ( cbr cfr clb crb csb csr dbr dfr dlb drb dsb dsr ))
			   (drf csf ( crf drf ))
			   (drf dsf ( clb dlb sam ))
			   (drf crf ( cfl clf crf csf dfl dlf drf dsf ))
			   (drf drf ( cbl cfl clb clf csl dbl dfl dlb dlf dsl ))
			   (drf cfr ( cfl clf crf csf dfl dlf drf dsf ))
			   (drf dfr ( cfl clf dbl dfl dlf dsl ))
			   (drf csr ( crf dlf drf dsf ))
			   (drf dsr ( dfl dlf dsf ))
			   (drf cbr ( dlf drf dsf ))
			   (drf dbr ( dfl dlf drf dsf ))
			   (drf crb ( dlf drf dsf ))
			   (drf drb ( dlf drf dsf ))
			   (cfr sam ( cfr ))
			   (cfr csb ( cfr dfr ))
			   (cfr dsb ( cfr dfr ))
			   (cfr clb ( cbr cfr csr dbr dfr dsr ))
			   (cfr dlb ( cbr cfr csr dbr dfr dsr ))
			   (cfr cbl ( cbr cfr csr dbr dfr dsr ))
			   (cfr dbl ( cbr cfr crb csr dbr dfr drb dsr ))
			   (cfr csl ( cbr cfr csr dbr dfr dsr ))
			   (cfr dsl ( cbr crb dbr drb ))
			   (cfr cfl ( cbr cfr crb csr dbr dfr drb dsr ))
			   (cfr dfl ( cbr clb crb csb dbr dlb drb dsb ))
			   (cfr clf ( cbr cfr crb csr ))
			   (cfr dlf ( cbl cbr clb crb csb dbl dlb drb dsb ))
			   (cfr csf ( cfr ))
			   (cfr dsf ( cbl dbl sam ))
			   (cfr crf ( cfr clf crf csf ))
			   (cfr drf ( cbl cfl clf crf csf csl dbl dfl dlf dsl ))
			   (cfr cfr ( cfr clf crf csf dfr dlf drf dsf ))
			   (cfr dfr ( cfl clf crf csf dfl dlf drf dsf ))
			   (cfr csr ( cfr crf dfr drf ))
			   (cfr dsr ( clf crf csf dlf drf dsf ))
			   (cfr cbr ( cfr crf dfr drf ))
			   (cfr dbr ( cfr clf crf csf dfr dlf drf dsf ))
			   (cfr crb ( cfr crf dfr drf ))
			   (cfr drb ( cfr crf dfr drf ))
			   (dfr sam ( dfr ))
			   (dfr csb ( dfr ))
			   (dfr dsb ( dfr ))
			   (dfr clb ( dbr dfr dsr ))
			   (dfr dlb ( dbr dfr dsr ))
			   (dfr cbl ( dbr dfr dsr ))
			   (dfr dbl ( dbr dfr drb dsr ))
			   (dfr csl ( dbr dfr dsr ))
			   (dfr dsl ( dbr drb ))
			   (dfr cfl ( cbr cfr crb csr dbr dfr drb dsr ))
			   (dfr dfl ( cbr crb dbr dlb drb dsb ))
			   (dfr clf ( cbr cfr crb csr dbr dfr drb dsr ))
			   (dfr dlf ( cbl cbr clb crb csb dbl dbr dlb drb dsb ))
			   (dfr csf ( cfr dfr ))
			   (dfr dsf ( cbl dbl sam ))
			   (dfr crf ( cfr clf crf csf dfr dlf drf dsf ))
			   (dfr drf ( cbl cfl clf crf csf csl dbl dfl dlf drf dsf dsl ))
			   (dfr cfr ( cfr clf crf csf dfr dlf drf dsf ))
			   (dfr dfr ( clf crf csf dfl dlf drf dsf ))
			   (dfr csr ( dfr drf ))
			   (dfr dsr ( dlf drf dsf ))
			   (dfr cbr ( dfr drf ))
			   (dfr dbr ( dfr dlf drf dsf ))
			   (dfr crb ( dfr drf ))
			   (dfr drb ( dfr drf ))
			   (csr sam ( csr ))
			   (csr csb ( csr dsr ))
			   (csr dsb ( csr dsr ))
			   (csr clb ( cbr dbr ))
			   (csr dlb ( cbr dbr ))
			   (csr cbl ( cbr dbr ))
			   (csr dbl ( cbr crb dbr drb ))
			   (csr csl ( cbr dbr ))
			   (csr dsl ( crb drb ))
			   (csr cfl ( cbr crb dbr drb ))
			   (csr dfl ( clb crb csb dlb drb dsb ))
			   (csr clf ( cbr crb ))
			   (csr dlf ( cbl clb crb csb dbl dlb ))
			   (csr csf ( csr ))
			   (csr dsf ( csl dsl sam ))
			   (csr crf ( cfr crf ))
			   (csr drf ( cfl clf crf csf dfl dlf ))
			   (csr cfr ( cfr crf dfr drf ))
			   (csr dfr ( clf crf csf dlf drf dsf ))
			   (csr csr ( cfr dfr ))
			   (csr dsr ( crf drf ))
			   (csr cbr ( cfr dfr ))
			   (csr dbr ( cfr crf dfr drf ))
			   (csr crb ( cfr dfr ))
			   (csr drb ( cfr dfr ))
			   (dsr sam ( dsr ))
			   (dsr csb ( dsr ))
			   (dsr dsb ( dsr ))
			   (dsr clb ( dbr ))
			   (dsr dlb ( dbr ))
			   (dsr cbl ( dbr ))
			   (dsr dbl ( dbr drb ))
			   (dsr csl ( dbr ))
			   (dsr dsl ( drb ))
			   (dsr cfl ( cbr crb dbr drb ))
			   (dsr dfl ( crb dlb drb dsb ))
			   (dsr clf ( cbr crb dbr drb ))
			   (dsr dlf ( cbl clb crb csb dbl dlb drb dsb ))
			   (dsr csf ( csr dsr ))
			   (dsr dsf ( csl dsl sam ))
			   (dsr crf ( cfr crf dfr drf ))
			   (dsr drf ( cfl clf crf csf dfl dlf drf dsf ))
			   (dsr cfr ( cfr crf dfr drf ))
			   (dsr dfr ( crf dlf drf dsf ))
			   (dsr csr ( dfr ))
			   (dsr dsr ( drf ))
			   (dsr cbr ( dfr ))
			   (dsr dbr ( dfr drf ))
			   (dsr crb ( dfr ))
			   (dsr drb ( dfr ))
			   (cbr sam ( cbr ))
			   (cbr csb ( cbr dbr ))
			   (cbr dsb ( cbr dbr ))
			   (cbr clb ( cbr crb dbr drb ))
			   (cbr dlb ( cbr crb dbr drb ))
			   (cbr cbl ( cbr crb dbr drb ))
			   (cbr dbl ( cbr clb crb csb dbr dlb drb dsb ))
			   (cbr csl ( cbr crb dbr drb ))
			   (cbr dsl ( clb crb csb dlb drb dsb ))
			   (cbr cfl ( cbr clb crb csb dbr dlb drb dsb ))
			   (cbr dfl ( cbl clb crb csb dbl dlb drb dsb ))
			   (cbr clf ( cbr clb crb csb ))
			   (cbr dlf ( cbl cfl clb crb csb csl dbl dfl dlb dsl ))
			   (cbr csf ( cbr ))
			   (cbr dsf ( cfl dfl sam ))
			   (cbr crf ( cbr cfr crf csr ))
			   (cbr drf ( cfl cfr clf crf csf dfl dlf drf dsf ))
			   (cbr cfr ( cbr cfr crf csr dbr dfr drf dsr ))
			   (cbr dfr ( cfr clf crf csf dfr dlf drf dsf ))
			   (cbr csr ( cbr cfr csr dbr dfr dsr ))
			   (cbr dsr ( cfr crf dfr drf ))
			   (cbr cbr ( cbr cfr csr dbr dfr dsr ))
			   (cbr dbr ( cbr cfr crf csr dbr dfr drf dsr ))
			   (cbr crb ( cbr cfr csr dbr dfr dsr ))
			   (cbr drb ( cbr cfr csr dbr dfr dsr ))
			   (dbr sam ( dbr ))
			   (dbr csb ( dbr ))
			   (dbr dsb ( dbr ))
			   (dbr clb ( dbr drb ))
			   (dbr dlb ( dbr drb ))
			   (dbr cbl ( dbr drb ))
			   (dbr dbl ( dbr dlb drb dsb ))
			   (dbr csl ( dbr drb ))
			   (dbr dsl ( dlb drb dsb ))
			   (dbr cfl ( cbr clb crb csb dbr dlb drb dsb ))
			   (dbr dfl ( clb crb csb dbl dlb drb dsb ))
			   (dbr clf ( cbr clb crb csb dbr dlb drb dsb ))
			   (dbr dlf ( cbl cfl clb crb csb csl dbl dfl dlb drb dsb dsl ))
			   (dbr csf ( cbr dbr ))
			   (dbr dsf ( cfl dfl sam ))
			   (dbr crf ( cbr cfr crf csr dbr dfr drf dsr ))
			   (dbr drf ( cfl cfr clf crf csf dfl dfr dlf drf dsf ))
			   (dbr cfr ( cbr cfr crf csr dbr dfr drf dsr ))
			   (dbr dfr ( cfr crf dfr dlf drf dsf ))
			   (dbr csr ( cbr dbr dfr dsr ))
			   (dbr dsr ( dfr drf ))
			   (dbr cbr ( dbr dfr dsr ))
			   (dbr dbr ( dbr dfr drf dsr ))
			   (dbr crb ( dbr dfr dsr ))
			   (dbr drb ( dbr dfr dsr ))
			   (crb sam ( crb ))
			   (crb csb ( crb drb ))
			   (crb dsb ( crb drb ))
			   (crb clb ( clb crb csb dlb drb dsb ))
			   (crb dlb ( clb crb csb dlb drb dsb ))
			   (crb cbl ( clb crb csb dlb drb dsb ))
			   (crb dbl ( cbl clb crb csb dbl dlb drb dsb ))
			   (crb csl ( clb crb csb dlb drb dsb ))
			   (crb dsl ( cbl clb csb dbl dlb dsb ))
			   (crb cfl ( cbl clb crb csb dbl dlb drb dsb ))
			   (crb dfl ( cbl cfl clb csl dbl dfl dlb dsl ))
			   (crb clf ( cbl clb crb csb ))
			   (crb dlf ( cbl cfl clb clf csl dbl dfl dlf dsl ))
			   (crb csf ( crb ))
			   (crb dsf ( clf dlf sam ))
			   (crb crf ( cbr cfr crb csr ))
			   (crb drf ( cbr cfr clf crf csf csr dfr dlf drf dsf ))
			   (crb cfr ( cbr cfr crb csr dbr dfr drb dsr ))
			   (crb dfr ( cbr cfr crf csr dbr dfr drf dsr ))
			   (crb csr ( cbr crb dbr drb ))
			   (crb dsr ( cbr cfr csr dbr dfr dsr ))
			   (crb cbr ( cbr crb dbr drb ))
			   (crb dbr ( cbr cfr crb csr dbr dfr drb dsr ))
			   (crb crb ( cbr crb dbr drb ))
			   (crb drb ( cbr crb dbr drb ))
			   (drb sam ( drb ))
			   (drb csb ( drb ))
			   (drb dsb ( drb ))
			   (drb clb ( dlb drb dsb ))
			   (drb dlb ( dlb drb dsb ))
			   (drb cbl ( dlb drb dsb ))
			   (drb dbl ( dbl dlb drb dsb ))
			   (drb csl ( dlb drb dsb ))
			   (drb dsl ( dbl dlb dsb ))
			   (drb cfl ( cbl clb crb csb dbl dlb drb dsb ))
			   (drb dfl ( cbl clb dbl dfl dlb dsl ))
			   (drb clf ( cbl clb crb csb dbl dlb drb dsb ))
			   (drb dlf ( cbl cfl clb clf csl dbl dfl dlb dlf dsl ))
			   (drb csf ( crb drb ))
			   (drb dsf ( clf dlf sam ))
			   (drb crf ( cbr cfr crb csr dbr dfr drb dsr ))
			   (drb drf ( cbr cfr clf crf csf csr dbr dfr dlf drf dsf dsr ))
			   (drb cfr ( cbr cfr crb csr dbr dfr drb dsr ))
			   (drb dfr ( cbr cfr csr dbr dfr drf dsr ))
			   (drb csr ( dbr drb ))
			   (drb dsr ( dbr dfr dsr ))
			   (drb cbr ( dbr drb ))
			   (drb dbr ( dbr dfr drb dsr ))
			   (drb crb ( dbr drb ))
			   (drb drb ( dbr drb )))
)
