2 0 default_concat 1 2 3 SAT NOT_SAT 3 3 G Z B 2 3 SAT NOT_SAT 3 3 G Z B 2 3 SAT NOT_SAT 3 3 G Z B 3 3 G Z B 4 3 SAT NOT_SAT NOT_SAT NOT_SAT 4 3 SAT SAT SAT NOT_SAT 9 3 G Z B Z Z B B B B 9 3 G G G G Z Z G Z B 6 3 G B Z B B B 6 3 G G G Z G B default_compare 0 2 3 SAT NOT_SAT 2 3 SAT NOT_SAT 5 3 PB B Z N NB 3 3 G Z B 2 3 SAT NOT_SAT 2 3 SAT NOT_SAT 2 3 SAT NOT_SAT 2 3 SAT NOT_SAT 5 3 B B Z G G 5 3 G G Z B B 5 3 B Z G Z B 5 3 G Z B Z B