PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb40-19-opb/normalized-frb40-19-3.opb
MD5SUM	3acd642471b3f4559739eef7eb2e9b58
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41095
Number of constraints which are clauses	41095
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5242

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 22:53:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3710 boxname=wulflinc20 idbench=326 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3acd642471b3f4559739eef7eb2e9b58  /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-3.opb /oldhome/oroussel/tmp/wulflinc20/normalized-frb40-19-3.opb
IDLAUNCH: 3710
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        889580 kB
Buffers:         33764 kB
Cached:          75528 kB
SwapCached:       2636 kB
Active:          48256 kB
Inactive:        66512 kB
HighTotal:      131008 kB
HighFree:        51800 kB
LowTotal:       903652 kB
LowFree:        837780 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24680 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:13:31 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 3710 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41095 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41095    82190 |   13698       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1492   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51256   118516 |   17085       0        0     nan |  0.000 % |
c |       100 |   51247   118485 |   18793      96     1236    12.9 |  0.094 % |
c |       250 |   51238   118454 |   20672     244     2622    10.7 |  0.137 % |
c |       475 |   51229   118423 |   22740     467     5364    11.5 |  0.180 % |
c |       812 |   51193   118299 |   25014     796     9438    11.9 |  0.362 % |
c |      1318 |   51148   118144 |   27515    1291    15855    12.3 |  0.584 % |
c |      2077 |   51113   118023 |   30267    2041    25404    12.4 |  0.809 % |
c |      3216 |   50828   117046 |   33293    3071    40907    13.3 |  2.381 % |
c |      4926 |   50341   115369 |   36623    4649    85210    18.3 |  5.126 % |
c |      7489 |   49657   113023 |   40285    6983   173312    24.8 |  9.659 % |
c |     11333 |   48829   110165 |   44314   10504   340905    32.5 | 15.768 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13531 |   48840   110219 |   16280   12665   475336    37.5 | 15.768 % |
c |     13631 |   48834   110199 |   17908   12762   477797    37.4 | 17.110 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13779 |   48835   110206 |   16278   12910   484604    37.5 | 17.110 % |
c |     13879 |   48835   110206 |   17905   13010   488105    37.5 | 17.147 % |
c |     14029 |   48818   110147 |   19696   13156   497776    37.8 | 17.280 % |
c |     14254 |   48803   110096 |   21666   13378   511459    38.2 | 17.368 % |
c |     14591 |   48677   109660 |   23832   13636   522416    38.3 | 18.387 % |
c |     15098 |   48646   109553 |   26215   14138   547823    38.7 | 18.653 % |
c |     15857 |   48637   109522 |   28837   14867   622720    41.9 | 18.701 % |
c |     16996 |   48591   109362 |   31721   15999   683901    42.7 | 19.101 % |
c |     18705 |   48542   109189 |   34893   17694   801749    45.3 | 19.543 % |
c |     21268 |   48483   108984 |   38382   20237   966548    47.8 | 20.027 % |
c |     25112 |   48080   107583 |   42220   23763  1171859    49.3 | 23.221 % |
c |     30879 |   47880   106887 |   46443   29293  1699026    58.0 | 24.812 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39508 |   47883   106901 |   15961   37922  2586539    68.2 | 24.812 % |
c |     39609 |   47883   106901 |   17557   15611  1154481    74.0 | 24.845 % |
c |     39760 |   47865   106839 |   19312   15755  1158489    73.5 | 24.934 % |
c |     39985 |   47846   106772 |   21244   15976  1168232    73.1 | 25.111 % |
c |     40322 |   47827   106705 |   23368   16309  1191327    73.0 | 25.290 % |
c |     40831 |   47796   106598 |   25705   16814  1214356    72.2 | 25.554 % |
c |     41590 |   47796   106598 |   28275   17573  1255015    71.4 | 25.557 % |
c |     42730 |   47787   106567 |   31103   18696  1304667    69.8 | 25.598 % |
c |     44438 |   47699   106265 |   34213   20330  1399730    68.9 | 26.177 % |
c |     47001 |   47648   106090 |   37635   22864  1587591    69.4 | 26.572 % |
c |     50845 |   47633   106039 |   41398   26640  2058693    77.3 | 26.663 % |
c |     56611 |   47612   105964 |   45538   32402  2479610    76.5 | 26.882 % |
c |     65261 |   47603   105933 |   50092   41038  3176079    77.4 | 26.927 % |
c |     78235 |   47589   105883 |   55101   18319  2027403   110.7 | 27.018 % |
c |     97697 |   47490   105538 |   60611   37717  3189180    84.6 | 27.768 % |
c |    126890 |   47451   105405 |   66673   21455   822251    38.3 | 28.080 % |
c |    170680 |   47382   105168 |   73340   65231  5238764    80.3 | 28.742 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200410 |   47383   105174 |   15794   36117  2638708    73.1 | 28.742 % |
c |    200512 |   47383   105174 |   17373   14936   801574    53.7 | 28.776 % |
c |    200668 |   47383   105174 |   19110   15092   810065    53.7 | 28.774 % |
c |    200893 |   47383   105174 |   21021   15317   819117    53.5 | 28.777 % |
c |    201230 |   47355   105084 |   23123   15649   830981    53.1 | 29.039 % |
c |    201736 |   47355   105084 |   25436   16155   852868    52.8 | 29.039 % |
c |    202495 |   47347   105056 |   27980   16911   901275    53.3 | 29.128 % |
c |    203634 |   47347   105056 |   30778   18050   975716    54.1 | 29.128 % |
c |    205342 |   47347   105056 |   33855   19758  1077906    54.6 | 29.131 % |
c |    207904 |   47313   104938 |   37241   22296  1185040    53.2 | 29.397 % |
c |    211748 |   47313   104938 |   40965   26140  1496284    57.2 | 29.394 % |
c |    217515 |   47313   104938 |   45062   31907  1866203    58.5 | 29.397 % |
c |    226164 |   47285   104840 |   49568   40538  2475957    61.1 | 29.615 % |
c |    239139 |   47285   104840 |   54525   18112  1649660    91.1 | 29.617 % |
c |    258602 |   47285   104840 |   59977   37575  4785072   127.3 | 29.615 % |
c |    287795 |   47285   104840 |   65975   20072  2540982   126.6 | 29.618 % |
c |    331584 |   47254   104731 |   72573   63849  6951194   108.9 | 29.972 % |
c |    397268 |   47254   104731 |   79830   70755  9519656   134.5 | 29.972 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    463325 |   47257   104745 |   15752   72412  6934192    95.8 | 29.972 % |
c |    463426 |   47257   104745 |   17327    9365   504546    53.9 | 30.003 % |
c |    463576 |   47257   104745 |   19059    9515   510499    53.7 | 30.003 % |
c |    463801 |   47257   104745 |   20965    9740   515464    52.9 | 30.000 % |
c |    464138 |   47257   104745 |   23062   10077   530216    52.6 | 30.000 % |
c |    464648 |   47257   104745 |   25368   10587   552983    52.2 | 30.000 % |
c |    465407 |   47257   104745 |   27905   11346   586602    51.7 | 30.000 % |
c |    466546 |   47257   104745 |   30696   12485   632882    50.7 | 30.000 % |
c |    468254 |   47257   104745 |   33765   14193   681097    48.0 | 30.000 % |
c |    470816 |   47257   104745 |   37142   16755   775483    46.3 | 30.003 % |
c |    474660 |   47257   104745 |   40856   20599  1055693    51.2 | 30.000 % |
c |    480426 |   47257   104745 |   44942   26365  1612154    61.1 | 30.002 % |
c |    489076 |   47257   104745 |   49436   35015  2171965    62.0 | 30.000 % |
c |    502050 |   47257   104745 |   54380   47989  3193695    66.6 | 30.000 % |
c |    521511 |   47257   104745 |   59818   28293  1743718    61.6 | 30.000 % |
c |    550703 |   47230   104652 |   65800   57466  4611001    80.2 | 30.133 % |
c |    594492 |   47230   104652 |   72380   50552  3810492    75.4 | 30.133 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 C478 -C477 -C476 -C475 -C474 -C473 -C472 C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 C438 -C437 -C436 -C435 -C434 -C433 C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 C347 -C346 -C345 -C344 -C343 -C342 -C341 C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 C118 -C117 -C116 -C115 -C114 -C113 -C112 C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 C89 -C88 -C87 -C86 -C85 -C84 -C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.77 0.92 0.89 2/54 31475
Raw data (stat): 31475 (runsolver) R 31474 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479701645 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.81 0.92 0.89 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 2126 0 0 0 991 6 0 0 25 0 1 0 479701645 10338304 2104 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2524 2104 603 41 0 2483 0
vsize: 10096
[startup+20.0002 s]
Raw data (loadavg): 0.84 0.93 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 2343 0 0 0 1991 6 0 0 25 0 1 0 479701645 11280384 2321 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2321 603 41 0 2713 0
vsize: 11016
[startup+30.0006 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 2989 0 0 0 2989 9 0 0 25 0 1 0 479701645 13832192 2967 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3377 2967 603 41 0 3336 0
vsize: 13508
[startup+40.0005 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 3638 0 0 0 3986 11 0 0 25 0 1 0 479701645 16642048 3616 4294967295 134512640 134672761 3221224560 3221223744 134559358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4063 3616 603 41 0 4022 0
vsize: 16252
[startup+50.0017 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 4022 0 0 0 4985 13 0 0 25 0 1 0 479701645 18235392 4000 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4452 4000 603 41 0 4411 0
vsize: 17808
[startup+60.002 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 4022 0 0 0 5985 13 0 0 25 0 1 0 479701645 18235392 4000 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4452 4000 603 41 0 4411 0
vsize: 17808
[startup+70.0018 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 4148 0 0 0 6983 14 0 0 25 0 1 0 479701645 18771968 4126 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4583 4126 603 41 0 4542 0
vsize: 18332
[startup+80.0029 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 4721 0 0 0 7981 16 0 0 25 0 1 0 479701645 21069824 4699 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5144 4699 603 41 0 5103 0
vsize: 20576
[startup+90.0022 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 5268 0 0 0 8979 19 0 0 25 0 1 0 479701645 23339008 5246 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5698 5246 603 41 0 5657 0
vsize: 22792
[startup+100.003 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6148 0 0 0 9977 21 0 0 25 0 1 0 479701645 26836992 6126 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6552 6126 603 41 0 6511 0
vsize: 26208
[startup+110.004 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6228 0 0 0 10977 21 0 0 25 0 1 0 479701645 27242496 6206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6206 603 41 0 6610 0
vsize: 26604
[startup+120.004 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6228 0 0 0 11976 22 0 0 25 0 1 0 479701645 27242496 6206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6206 603 41 0 6610 0
vsize: 26604
[startup+130.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6228 0 0 0 12976 22 0 0 25 0 1 0 479701645 27242496 6206 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6206 603 41 0 6610 0
vsize: 26604
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6228 0 0 0 13976 23 0 0 25 0 1 0 479701645 27242496 6206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6206 603 41 0 6610 0
vsize: 26604
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6229 0 0 0 14976 23 0 0 25 0 1 0 479701645 27242496 6207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6207 603 41 0 6610 0
vsize: 26604
[startup+160.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6229 0 0 0 15975 23 0 0 25 0 1 0 479701645 27242496 6207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6207 603 41 0 6610 0
vsize: 26604
[startup+170.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6231 0 0 0 16975 24 0 0 25 0 1 0 479701645 27242496 6209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6209 603 41 0 6610 0
vsize: 26604
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6235 0 0 0 17975 24 0 0 25 0 1 0 479701645 27242496 6213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6213 603 41 0 6610 0
vsize: 26604
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6239 0 0 0 18974 25 0 0 25 0 1 0 479701645 27242496 6217 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6217 603 41 0 6610 0
vsize: 26604
[startup+200.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6239 0 0 0 19975 25 0 0 25 0 1 0 479701645 27242496 6217 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6217 603 41 0 6610 0
vsize: 26604
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6240 0 0 0 20974 25 0 0 25 0 1 0 479701645 27242496 6218 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6218 603 41 0 6610 0
vsize: 26604
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6240 0 0 0 21974 26 0 0 25 0 1 0 479701645 27242496 6218 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6218 603 41 0 6610 0
vsize: 26604
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6240 0 0 0 22974 26 0 0 25 0 1 0 479701645 27242496 6218 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6218 603 41 0 6610 0
vsize: 26604
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6247 0 0 0 23973 27 0 0 25 0 1 0 479701645 27242496 6225 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6651 6225 603 41 0 6610 0
vsize: 26604
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6566 0 0 0 24972 28 0 0 25 0 1 0 479701645 28577792 6544 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6977 6544 603 41 0 6936 0
vsize: 27908
[startup+260.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 6716 0 0 0 25971 29 0 0 25 0 1 0 479701645 29253632 6694 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7142 6694 603 41 0 7101 0
vsize: 28568
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 7034 0 0 0 26970 30 0 0 25 0 1 0 479701645 30457856 7012 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7436 7012 603 41 0 7395 0
vsize: 29744
[startup+280.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 7357 0 0 0 27969 32 0 0 25 0 1 0 479701645 32047104 7335 4294967295 134512640 134672761 3221224560 3221223744 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7824 7335 603 41 0 7783 0
vsize: 31296
[startup+290.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 7734 0 0 0 28968 33 0 0 25 0 1 0 479701645 33644544 7712 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8214 7712 603 41 0 8173 0
vsize: 32856
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8105 0 0 0 29967 34 0 0 25 0 1 0 479701645 35110912 8083 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8572 8083 603 41 0 8531 0
vsize: 34288
[startup+310.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 30966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 31966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223664 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+330.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 32966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 33966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 34966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 35966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 36966 35 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 37966 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31475
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 38966 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 39966 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 40966 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 41966 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 42967 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8194 0 0 0 43967 36 0 0 25 0 1 0 479701645 35516416 8172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8172 603 41 0 8630 0
vsize: 34684
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8367 0 0 0 44966 37 0 0 25 0 1 0 479701645 36175872 8345 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8832 8345 603 41 0 8791 0
vsize: 35328
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31528
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 8810 0 0 0 45965 38 0 0 25 0 1 0 479701645 38047744 8788 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9289 8788 603 41 0 9248 0
vsize: 37156
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9282 0 0 0 46964 39 0 0 25 0 1 0 479701645 39923712 9260 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9747 9260 603 41 0 9706 0
vsize: 38988
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9752 0 0 0 47962 41 0 0 25 0 1 0 479701645 41799680 9730 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10205 9730 603 41 0 10164 0
vsize: 40820
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 48962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223744 134559381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 49962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 50962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 51962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 52962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 53962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 54962 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 55963 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 56963 42 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 57963 43 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 58963 43 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 59963 43 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 9906 0 0 0 60963 43 0 0 25 0 1 0 479701645 42471424 9884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10369 9884 603 41 0 10328 0
vsize: 41476
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10222 0 0 0 61962 44 0 0 25 0 1 0 479701645 43814912 10200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10697 10200 603 41 0 10656 0
vsize: 42788
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10677 0 0 0 62961 45 0 0 25 0 1 0 479701645 45694976 10655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11156 10655 603 41 0 11115 0
vsize: 44624
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10731 0 0 0 63960 46 0 0 25 0 1 0 479701645 45830144 10709 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10709 603 41 0 11148 0
vsize: 44756
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10731 0 0 0 64961 46 0 0 25 0 1 0 479701645 45830144 10709 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10709 603 41 0 11148 0
vsize: 44756
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10731 0 0 0 65961 46 0 0 25 0 1 0 479701645 45830144 10709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10709 603 41 0 11148 0
vsize: 44756
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 66961 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 67961 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 68961 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 69962 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 70962 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 31530
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10732 0 0 0 71962 46 0 0 25 0 1 0 479701645 45830144 10710 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10710 603 41 0 11148 0
vsize: 44756
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 31531
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10733 0 0 0 72962 47 0 0 25 0 1 0 479701645 45830144 10711 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10711 603 41 0 11148 0
vsize: 44756
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10734 0 0 0 73962 47 0 0 25 0 1 0 479701645 45830144 10712 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10712 603 41 0 11148 0
vsize: 44756
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 10734 0 0 0 74962 47 0 0 25 0 1 0 479701645 45830144 10712 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11189 10712 603 41 0 11148 0
vsize: 44756
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 11003 0 0 0 75961 48 0 0 25 0 1 0 479701645 46936064 10981 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11459 10981 603 41 0 11418 0
vsize: 45836
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 11409 0 0 0 76960 49 0 0 25 0 1 0 479701645 48680960 11387 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11885 11387 603 41 0 11844 0
vsize: 47540
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 11824 0 0 0 77959 50 0 0 25 0 1 0 479701645 50311168 11802 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12283 11802 603 41 0 12242 0
vsize: 49132
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12210 0 0 0 78958 52 0 0 25 0 1 0 479701645 51920896 12188 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12676 12188 603 41 0 12635 0
vsize: 50704
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12415 0 0 0 79957 52 0 0 25 0 1 0 479701645 52723712 12393 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12872 12393 603 41 0 12831 0
vsize: 51488
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12678 0 0 0 80956 53 0 0 25 0 1 0 479701645 53788672 12656 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13132 12656 603 41 0 13091 0
vsize: 52528
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12888 0 0 0 81956 54 0 0 25 0 1 0 479701645 54710272 12866 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12866 603 41 0 13316 0
vsize: 53428
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12888 0 0 0 82956 54 0 0 25 0 1 0 479701645 54710272 12866 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12866 603 41 0 13316 0
vsize: 53428
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12888 0 0 0 83956 54 0 0 25 0 1 0 479701645 54710272 12866 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12866 603 41 0 13316 0
vsize: 53428
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12888 0 0 0 84956 54 0 0 25 0 1 0 479701645 54710272 12866 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12866 603 41 0 13316 0
vsize: 53428
[startup+860.023 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12888 0 0 0 85956 54 0 0 25 0 1 0 479701645 54710272 12866 4294967295 134512640 134672761 3221224560 3221223480 1075351245 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12866 603 41 0 13316 0
vsize: 53428
[startup+870.023 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 86956 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+880.023 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 87957 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+890.024 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 88957 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+900.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 89957 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+910.024 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 90957 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+920.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 91957 54 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+930.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 92957 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+940.024 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 93957 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+950.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 94958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+960.025 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 95957 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223744 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+970.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 96957 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+980.026 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 97958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+990.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 98958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 99958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 100958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 101958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 102958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 103958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 104958 55 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 105958 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 106959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 107959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 108959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 109959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 110959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 111959 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 112960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 113960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 114960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 115960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 116960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 117960 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 118961 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31532
Raw data (stat): 31475 (minisat+) R 31474 27565 27564 0 -1 0 12889 0 0 0 119961 56 0 0 25 0 1 0 479701645 54710272 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13357 12867 603 41 0 13316 0
vsize: 53428
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31532
Raw data (stat): 31475 (minisat+) Z 31474 27565 27564 0 -1 12 12892 0 0 0 119961 59 0 0 25 0 1 0 479701645 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.61
CPU system time (s): 0.59191
CPU usage (%): 100.012
Max. virtual memory (Kb): 53428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####