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-4.opb
MD5SUM	7731f50c352d2fd7b2fe148b68bfdbab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
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	41605
Number of constraints which are clauses	41605
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 5034

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-13 21:32:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2939 boxname=wulflinc11 idbench=327 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  7731f50c352d2fd7b2fe148b68bfdbab  /oldhome/oroussel/tmp/wulflinc11/normalized-frb40-19-4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-frb40-19-4.opb
IDLAUNCH: 2939
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        916136 kB
Buffers:         34544 kB
Cached:          59532 kB
SwapCached:       4932 kB
Active:          54620 kB
Inactive:        47220 kB
HighTotal:      131008 kB
HighFree:        67760 kB
LowTotal:       903652 kB
LowFree:        848376 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11136 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:52:52 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 2939 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41605 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 |   41605    83210 |   13868       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77753   168122 |   25917       0        0     nan |  0.000 % |
c |       101 |   77380   167357 |   28508      74     1087    14.7 |  0.796 % |
c |       251 |   76935   166400 |   31359     187     2027    10.8 |  1.831 % |
c |       476 |   75593   163504 |   34495     333     4511    13.5 |  4.972 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       781 |   74235   160714 |   24745     565     8133    14.4 |  4.972 % |
c |       881 |   73694   159487 |   27219     640     8842    13.8 | 10.031 % |
c |      1031 |   73182   158344 |   29941     742     9894    13.3 | 11.290 % |
c |      1256 |   71817   155279 |   32935     908    11980    13.2 | 14.690 % |
c |      1593 |   70390   152058 |   36229    1120    14315    12.8 | 18.255 % |
c |      2099 |   68314   147352 |   39852    1473    20259    13.8 | 23.529 % |
c |      2858 |   64983   139810 |   43837    2005    27170    13.6 | 31.922 % |
c |      3997 |   61942   132839 |   48221    2827    38151    13.5 | 39.672 % |
c |      5705 |   57794   123031 |   53043    4147    58590    14.1 | 50.708 % |
c |      8267 |   53937   113879 |   58347    6175   101349    16.4 | 61.198 % |
c |     12111 |   51088   107100 |   64182    9376   209229    22.3 | 68.931 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14510 |   50433   105575 |   16811   11454   342561    29.9 | 68.931 % |
c |     14610 |   50433   105575 |   18492   11554   344419    29.8 | 70.722 % |
c |     14761 |   50433   105575 |   20341   11705   350475    29.9 | 70.722 % |
c |     14986 |   50433   105575 |   22375   11930   361583    30.3 | 70.722 % |
c |     15324 |   50107   104782 |   24612   12183   372190    30.5 | 71.626 % |
c |     15831 |   49933   104364 |   27074   12595   390221    31.0 | 72.104 % |
c |     16590 |   49629   103648 |   29781   13283   428057    32.2 | 72.916 % |
c |     17729 |   48931   101939 |   32759   14235   473128    33.2 | 74.898 % |
c |     19438 |   48867   101783 |   36035   15894   575254    36.2 | 75.083 % |
c |     22000 |   48275   100352 |   39639   18090   716401    39.6 | 76.734 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24883 |   48095    99832 |   16031   20800   934720    44.9 | 76.734 % |
c |     24983 |   47740    98976 |   17634   20624   932425    45.2 | 78.263 % |
c |     25133 |   47740    98976 |   19397   20774   941755    45.3 | 78.263 % |
c |     25358 |   47702    98882 |   21337   20927   950824    45.4 | 78.376 % |
c |     25695 |   47702    98882 |   23470   21264   970411    45.6 | 78.376 % |
c |     26201 |   47700    98878 |   25818   21769  1001975    46.0 | 78.380 % |
c |     26960 |   47487    98334 |   28399   22339  1043094    46.7 | 79.015 % |
c |     28099 |   47449    98246 |   31239   23430  1110397    47.4 | 79.115 % |
c |     29807 |   47449    98246 |   34363   25138  1301421    51.8 | 79.115 % |
c |     32369 |   47408    98151 |   37800   27600  1517138    55.0 | 79.224 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34890 |   47234    97752 |   15744   29984  1760205    58.7 | 79.224 % |
c |     34990 |   47194    97654 |   17318   29906  1761335    58.9 | 79.907 % |
c |     35140 |   47194    97654 |   19050   30056  1774039    59.0 | 79.907 % |
c |     35365 |   47194    97654 |   20955   30281  1792828    59.2 | 79.907 % |
c |     35702 |   47194    97654 |   23050   30618  1825661    59.6 | 79.907 % |
c |     36208 |   47194    97654 |   25355   31124  1860327    59.8 | 79.907 % |
c |     36968 |   47166    97583 |   27891   31860  1920463    60.3 | 79.991 % |
c |     38109 |   47162    97573 |   30680   32897  2012855    61.2 | 80.003 % |
c |     39818 |   47162    97573 |   33748   34606  2163659    62.5 | 80.003 % |
c |     42380 |   47162    97573 |   37123   37168  2449092    65.9 | 80.003 % |
c |     46227 |   47060    97338 |   40835   40876  2850607    69.7 | 80.260 % |
c |     51994 |   46982    97141 |   44919   46508  3471568    74.6 | 80.484 % |
c |     60644 |   46934    97017 |   49411   54952  4522068    82.3 | 80.632 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65436 |   46893    96903 |   15631   59362  5113871    86.1 | 80.632 % |
c |     65536 |   46893    96903 |   17194   18644  1614753    86.6 | 80.749 % |
c |     65686 |   46854    96804 |   18913   18767  1618131    86.2 | 80.869 % |
c |     65911 |   46795    96659 |   20804   18985  1627818    85.7 | 81.042 % |
c |     66248 |   46795    96659 |   22885   19322  1649457    85.4 | 81.042 % |
c |     66756 |   46795    96659 |   25173   19830  1672800    84.4 | 81.042 % |
c |     67518 |   46795    96659 |   27691   20592  1744416    84.7 | 81.042 % |
c |     68657 |   46795    96659 |   30460   21731  1856295    85.4 | 81.042 % |
c |     70366 |   46795    96659 |   33506   23440  1997186    85.2 | 81.042 % |
c |     72928 |   46742    96532 |   36857   25984  2212431    85.1 | 81.190 % |
c |     76774 |   46714    96464 |   40542   29821  2582192    86.6 | 81.266 % |
c |     82540 |   46712    96460 |   44597   35586  3095009    87.0 | 81.270 % |
c |     91190 |   46712    96460 |   49056   44236  3866480    87.4 | 81.270 % |
c |    104165 |   46623    96245 |   53962   57037  4993464    87.5 | 81.522 % |
c |    123626 |   46580    96146 |   59358   20979  1569020    74.8 | 81.634 % |
c |    152819 |   46485    95911 |   65294   50114  4321342    86.2 | 81.914 % |
c |    196609 |   46391    95677 |   71824   26970  1175384    43.6 | 82.190 % |
c |    262293 |   46384    95660 |   79006   92651  5737328    61.9 | 82.211 % |
c |    360821 |   46278    95411 |   86907   25024  2605510   104.1 | 82.491 % |
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.91 0.95 0.90 2/54 4331
Raw data (stat): 4331 (runsolver) R 4330 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420994960 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 2939 0 0 0 990 7 0 0 25 0 1 0 420994960 14618624 2917 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3569 2917 603 41 0 3528 0
vsize: 14276
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 2939 0 0 0 1990 7 0 0 25 0 1 0 420994960 14618624 2917 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3569 2917 603 41 0 3528 0
vsize: 14276
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 2984 0 0 0 2990 7 0 0 25 0 1 0 420994960 14753792 2962 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3602 2962 603 41 0 3561 0
vsize: 14408
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 3315 0 0 0 3987 9 0 0 25 0 1 0 420994960 16306176 3293 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3981 3293 603 41 0 3940 0
vsize: 15924
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 3739 0 0 0 4985 11 0 0 25 0 1 0 420994960 18079744 3717 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4414 3717 603 41 0 4373 0
vsize: 17656
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 4263 0 0 0 5984 12 0 0 25 0 1 0 420994960 20086784 4241 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4904 4241 603 41 0 4863 0
vsize: 19616
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 4823 0 0 0 6982 14 0 0 25 0 1 0 420994960 22376448 4801 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5463 4801 603 41 0 5422 0
vsize: 21852
[startup+80.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 5308 0 0 0 7979 16 0 0 25 0 1 0 420994960 24465408 5286 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5973 5286 603 41 0 5932 0
vsize: 23892
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 5856 0 0 0 8977 18 0 0 25 0 1 0 420994960 26734592 5834 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6527 5834 603 41 0 6486 0
vsize: 26108
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 6294 0 0 0 9975 20 0 0 25 0 1 0 420994960 28479488 6272 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6953 6272 603 41 0 6912 0
vsize: 27812
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 6755 0 0 0 10974 21 0 0 25 0 1 0 420994960 30359552 6733 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7412 6733 603 41 0 7371 0
vsize: 29648
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 7258 0 0 0 11973 23 0 0 25 0 1 0 420994960 32493568 7236 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7933 7236 603 41 0 7892 0
vsize: 31732
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 7735 0 0 0 12971 24 0 0 25 0 1 0 420994960 34373632 7713 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8392 7713 603 41 0 8351 0
vsize: 33568
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8151 0 0 0 13971 25 0 0 25 0 1 0 420994960 36130816 8129 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8821 8129 603 41 0 8780 0
vsize: 35284
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 14970 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 15970 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 16971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 17971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 18971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 19971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 20971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223796 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 21971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 22971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8575 0 0 0 23971 26 0 0 25 0 1 0 420994960 37740544 8553 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9214 8553 603 41 0 9173 0
vsize: 36856
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 8861 0 0 0 24970 27 0 0 25 0 1 0 420994960 38940672 8839 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9507 8839 603 41 0 9466 0
vsize: 38028
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 9229 0 0 0 25970 28 0 0 25 0 1 0 420994960 40398848 9207 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9863 9207 603 41 0 9822 0
vsize: 39452
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 9571 0 0 0 26969 29 0 0 25 0 1 0 420994960 42135552 9549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10287 9549 603 41 0 10246 0
vsize: 41148
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 9964 0 0 0 27968 30 0 0 25 0 1 0 420994960 43732992 9942 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10677 9942 603 41 0 10636 0
vsize: 42708
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10309 0 0 0 28967 31 0 0 25 0 1 0 420994960 45191168 10287 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11033 10287 603 41 0 10992 0
vsize: 44132
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10621 0 0 0 29967 32 0 0 25 0 1 0 420994960 46383104 10599 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11324 10599 603 41 0 11283 0
vsize: 45296
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 30966 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 31967 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 32967 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223760 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 33967 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 34967 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 35967 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 36968 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 37968 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 38968 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 39968 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 40968 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 41969 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 42969 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10704 0 0 0 43969 32 0 0 25 0 1 0 420994960 46784512 10682 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10682 603 41 0 11381 0
vsize: 45688
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10706 0 0 0 44969 32 0 0 25 0 1 0 420994960 46784512 10684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10684 603 41 0 11381 0
vsize: 45688
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10708 0 0 0 45969 32 0 0 25 0 1 0 420994960 46784512 10686 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10686 603 41 0 11381 0
vsize: 45688
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10710 0 0 0 46969 32 0 0 25 0 1 0 420994960 46784512 10688 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10688 603 41 0 11381 0
vsize: 45688
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10713 0 0 0 47970 32 0 0 25 0 1 0 420994960 46784512 10691 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10691 603 41 0 11381 0
vsize: 45688
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 48970 32 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 49970 32 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 50969 32 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 51968 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 52969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 53969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 54969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 55969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 56969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 57969 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 58970 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 59970 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 60970 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 61970 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 62970 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 63971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 64971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 65971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 66971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 67971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 68971 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10716 0 0 0 69972 33 0 0 25 0 1 0 420994960 46784512 10694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10694 603 41 0 11381 0
vsize: 45688
[startup+710.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10718 0 0 0 70972 33 0 0 25 0 1 0 420994960 46784512 10696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10696 603 41 0 11381 0
vsize: 45688
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10721 0 0 0 71972 33 0 0 25 0 1 0 420994960 46784512 10699 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10699 603 41 0 11381 0
vsize: 45688
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10723 0 0 0 72972 33 0 0 25 0 1 0 420994960 46784512 10701 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10701 603 41 0 11381 0
vsize: 45688
[startup+740.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10726 0 0 0 73972 33 0 0 25 0 1 0 420994960 46784512 10704 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10704 603 41 0 11381 0
vsize: 45688
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10728 0 0 0 74972 33 0 0 25 0 1 0 420994960 46784512 10706 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10706 603 41 0 11381 0
vsize: 45688
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 75972 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 76973 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 77973 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 78973 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 79973 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10730 0 0 0 80973 33 0 0 25 0 1 0 420994960 46784512 10708 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10708 603 41 0 11381 0
vsize: 45688
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 81974 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 82974 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 83974 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 84974 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 85974 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 86975 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 87975 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 88975 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 89975 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 90975 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223760 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 91976 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 92976 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10731 0 0 0 93976 33 0 0 25 0 1 0 420994960 46784512 10709 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11422 10709 603 41 0 11381 0
vsize: 45688
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 10761 0 0 0 94976 33 0 0 25 0 1 0 420994960 46919680 10739 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11455 10739 603 41 0 11414 0
vsize: 45820
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 11130 0 0 0 95975 34 0 0 25 0 1 0 420994960 48386048 11108 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11813 11108 603 41 0 11772 0
vsize: 47252
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 11455 0 0 0 96974 35 0 0 25 0 1 0 420994960 49725440 11433 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12140 11433 603 41 0 12099 0
vsize: 48560
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 11782 0 0 0 97974 36 0 0 25 0 1 0 420994960 51056640 11760 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12465 11760 603 41 0 12424 0
vsize: 49860
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12079 0 0 0 98973 36 0 0 25 0 1 0 420994960 52244480 12057 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12755 12057 603 41 0 12714 0
vsize: 51020
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12389 0 0 0 99972 38 0 0 25 0 1 0 420994960 53579776 12367 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13081 12367 603 41 0 13040 0
vsize: 52324
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12668 0 0 0 100971 39 0 0 25 0 1 0 420994960 54652928 12646 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12646 603 41 0 13302 0
vsize: 53372
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 101971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223776 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 102971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 103970 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 104971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 105971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 106971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 107971 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223808 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 108972 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 109972 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12669 0 0 0 110972 39 0 0 25 0 1 0 420994960 54652928 12647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12647 603 41 0 13302 0
vsize: 53372
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12670 0 0 0 111972 39 0 0 25 0 1 0 420994960 54652928 12648 4294967295 134512640 134672761 3221224624 3221223780 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12648 603 41 0 13302 0
vsize: 53372
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12670 0 0 0 112972 40 0 0 25 0 1 0 420994960 54652928 12648 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12648 603 41 0 13302 0
vsize: 53372
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12670 0 0 0 113972 40 0 0 25 0 1 0 420994960 54652928 12648 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12648 603 41 0 13302 0
vsize: 53372
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12670 0 0 0 114973 40 0 0 25 0 1 0 420994960 54652928 12648 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12648 603 41 0 13302 0
vsize: 53372
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12670 0 0 0 115973 40 0 0 25 0 1 0 420994960 54652928 12648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13343 12648 603 41 0 13302 0
vsize: 53372
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 12719 0 0 0 116973 40 0 0 25 0 1 0 420994960 54915072 12697 4294967295 134512640 134672761 3221224624 3221223760 134560645 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13407 12697 603 41 0 13366 0
vsize: 53628
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 13094 0 0 0 117972 41 0 0 25 0 1 0 420994960 56381440 13072 4294967295 134512640 134672761 3221224624 3221223780 134559752 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13765 13072 603 41 0 13724 0
vsize: 55060
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 13455 0 0 0 118971 42 0 0 25 0 1 0 420994960 57856000 13433 4294967295 134512640 134672761 3221224624 3221223760 134560650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14125 13433 603 41 0 14084 0
vsize: 56500
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4331
Raw data (stat): 4331 (minisat+) R 4330 32461 32460 0 -1 0 13769 0 0 0 119970 43 0 0 25 0 1 0 420994960 59187200 13747 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14450 13747 603 41 0 14409 0
vsize: 57800
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4331
Raw data (stat): 4331 (minisat+) Z 4330 32461 32460 0 -1 12 13772 0 0 0 119970 46 0 0 25 0 1 0 420994960 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.05
CPU time (s): 1200.17
CPU user time (s): 1199.71
CPU system time (s): 0.461929
CPU usage (%): 100.01
Max. virtual memory (Kb): 57800
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####