=====UNSATISFIABLE=====
%%  runtime:       0.035 (35.000 ms)
%%  solvetime:     0.016 (16.000 ms)
%%  solutions:     0
%%  variables:     285
%%  propagators:   375
%%  propagations:  151940
%%  nodes:         1683
%%  failures:      842
%%  restarts:      0
%%  peak depth:    15