unclasp version 0.1
Reading from out0PviVj/gringo_out
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 289729 21 837 133 
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 164601 16 831 82 
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 164601 16 831 82 
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 164601 16 831 82 
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 164601 16 831 82 
Answer: 1
in("x-window-system-core",21913) in("libqthreads-12",12740) in("keduca",28793) in
Optimization: 164601 16 831 82 
SATISFIABLE

Models      : 1+    
  Enumerated: 6
  Optimum   : unknown
Optimization: 164601 16 831 82 
Time        : 4.180s (Solving: 3.10s 1st Model: 0.37s Unsat: 0.00s)
Choices     : 321
Conflicts   : 18
Restarts    : 0

Atoms       : 1065069
Rules       : 1148862 (1: 1138706 2: 1625 3: 8527 6: 4)
Bodies      : 51621 
Equivalences: 2127323 (Atom=Atom: 1036177 Body=Body: 13706 Other: 1077440)
Tight       : Yes

Variables   : 41434  (Eliminated:    0)
Constraints : 971    (Binary:  5.3% Ternary:  1.1% Other: 93.6%)
Lemmas      : 17     (Binary: 47.1% Ternary: 29.4% Other: 23.5%)
  Conflicts : 17     (Average Length: 2.8) 
  Loops     : 0      (Average Length: 0.0) 
  Other     : 0      (Average Length: 0.0) 
  Deleted   : 0     
% warning: recommends/4 is never defined