#define COINS 12
#define FOUR 4
#define WGHS 3

2lp_main()
{
	if solve_coins(0,0,0,0,COINS);
	then printf("A solution strategy weighing 4 vs 4 each time indeed exists \n");
}

same_as_tip_left(int nl2,u2,nl1,u1,nh1,nh2,p1,p2)
{
	nh1+u1==nh2+u2; nl2+u2==nl1+u1;
}

can_tip_left(int nl1,u1,nh2,u2)
{		 
	not {
		nl1 == 0; u1 == 0; 
		nh2 == 0; u2 == 0;
	}
}

can_tip_right(int nl2,u2,nh1,u1)
{
	not {
		nl2 == 0; u2 == 0; 
		nh1 == 0; u1 == 0;
	}
}

can_balance(int p1,u1,u2,nl1,nl2,nh1,nh2,p)
{
	not {
		p1 == 0;  u1 == 0;  u2 == 0;  nl1 == 0;
		nl2 == 0;  nh1 == 0;  nh2 == 0;  p == 0;
	}
}

solution_found(int p,u)
{
	p>= COINS - 1;		// At least all coins but one perfect
	u == 0;			// No coins unknown
}

four(int nh1,nl1,p1,u1,nh2,nl2,p2,u2) 
{
	FOUR == nh1 + nl1 + p1 + u1;  // 4 coins in each tray
	FOUR == nh2 + nl2 + p2 + u2;
}

solve_coins(int w,nh,nl,p,u)
{
	if solution_found(p,u);
	then return;

	w < WGHS;		// Weighing still possible?

	// Select coins for weighing
	c_or(int nh1=0;nh1<=nh;nh1++)		// NotHeavies on left
	c_or(int nh2=0;nh2<=nh-nh1;nh2++)	// NotHeavies on right
		c_or(int nl1=0;nl1<=nl;nl1++)			// and so on
		c_or(int nl2=0;nl2<=nl-nl1;nl2++) 
			c_or(int p1=0;p1<=p;p1++)  
			c_or(int p2=0;p2<=p-p1;p2++)
				c_or(int u1=u;u1>=0;u1--)  
				c_or(int u2=u-u1;u2>=0;u2--)
	{

		four(nh1,nl1,p1,u1,nh2,nl2,p2,u2);				// 4 to a tray?

		if can_tip_left(nl1,u1,nh2,u2); 
		then
		solve_coins(w+1,nh2+u2,nl1+u1,p+nl-nl1+nh-nh2+u-u1-u2,0); 

		if can_balance(p1,u1,u2,nl1,nl2,nh1,nh2,p); 
		then 
		solve_coins(w+1,nh-nh1-nh2,nl-nl1-nl2,p+nh1+nh2+nl1+nl2+u1+u2,u-u1-u2);
                
		if {
			can_tip_right(nl2,u2,nh1,u1);
			not same_as_tip_left(nl2,u2,nl1,u1,nh1,nh2,p1,p2); 
		} 
		then 
		solve_coins(w+1,nh1+u1,nl2+u2,p+nl-nl2+nh-nh1+u-u2-u1,0); 
	}
}


 