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 5995

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 02:51:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4463 boxname=wulflinc28 idbench=327 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7731f50c352d2fd7b2fe148b68bfdbab  /oldhome/oroussel/tmp/wulflinc28/normalized-frb40-19-4.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc28/normalized-frb40-19-4.opb /oldhome/oroussel/tmp/wulflinc28/normalized-frb40-19-4.opb
IDLAUNCH: 4463
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        883412 kB
Buffers:         35796 kB
Cached:          78236 kB
SwapCached:          4 kB
Active:          54548 kB
Inactive:        63260 kB
HighTotal:      131008 kB
HighFree:        48188 kB
LowTotal:       903652 kB
LowFree:        835224 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27836 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:11:43 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4463 7 1200.21 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.84 0.94 0.90 2/54 20475
Raw data (stat): 20475 (runsolver) R 20474 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481136300 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99956 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 2899 0 0 0 990 8 0 0 25 0 1 0 481136300 14442496 2877 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3526 2877 603 41 0 3485 0
vsize: 14104
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 2899 0 0 0 1990 8 0 0 25 0 1 0 481136300 14442496 2877 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3526 2877 603 41 0 3485 0
vsize: 14104
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 2956 0 0 0 2990 8 0 0 25 0 1 0 481136300 14712832 2934 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3592 2934 603 41 0 3551 0
vsize: 14368
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 3286 0 0 0 3988 9 0 0 25 0 1 0 481136300 16187392 3264 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3952 3264 603 41 0 3911 0
vsize: 15808
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 3715 0 0 0 4987 10 0 0 25 0 1 0 481136300 17965056 3693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4386 3693 603 41 0 4345 0
vsize: 17544
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 4246 0 0 0 5986 11 0 0 25 0 1 0 481136300 20111360 4224 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4910 4224 603 41 0 4869 0
vsize: 19640
[startup+70.0026 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 4804 0 0 0 6983 14 0 0 25 0 1 0 481136300 22388736 4782 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5466 4782 603 41 0 5425 0
vsize: 21864
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 5298 0 0 0 7982 15 0 0 25 0 1 0 481136300 24481792 5276 4294967295 134512640 134672761 3221224560 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5977 5276 603 41 0 5936 0
vsize: 23908
[startup+90.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 5846 0 0 0 8981 17 0 0 25 0 1 0 481136300 26763264 5824 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6534 5824 603 41 0 6493 0
vsize: 26136
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 6272 0 0 0 9980 18 0 0 25 0 1 0 481136300 28499968 6250 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6958 6250 603 41 0 6917 0
vsize: 27832
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 6738 0 0 0 10979 19 0 0 25 0 1 0 481136300 30375936 6716 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7416 6716 603 41 0 7375 0
vsize: 29664
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 7235 0 0 0 11977 21 0 0 25 0 1 0 481136300 32378880 7213 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7905 7213 603 41 0 7864 0
vsize: 31620
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 7725 0 0 0 12976 23 0 0 25 0 1 0 481136300 34390016 7703 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8396 7703 603 41 0 8355 0
vsize: 33584
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8138 0 0 0 13974 24 0 0 25 0 1 0 481136300 35987456 8116 4294967295 134512640 134672761 3221224560 3221223744 134558764 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8786 8116 603 41 0 8745 0
vsize: 35144
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 14974 25 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 15973 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 16974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 17974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 18974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 19974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223664 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 20974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 21974 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223664 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 22975 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8533 0 0 0 23975 26 0 0 25 0 1 0 481136300 37597184 8511 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9179 8511 603 41 0 9138 0
vsize: 36716
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 8835 0 0 0 24974 27 0 0 25 0 1 0 481136300 38797312 8813 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9472 8813 603 41 0 9431 0
vsize: 37888
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 9203 0 0 0 25972 29 0 0 25 0 1 0 481136300 40398848 9181 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9863 9181 603 41 0 9822 0
vsize: 39452
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 9544 0 0 0 26971 30 0 0 25 0 1 0 481136300 41988096 9522 4294967295 134512640 134672761 3221224560 3221223696 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10251 9522 603 41 0 10210 0
vsize: 41004
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 9935 0 0 0 27970 31 0 0 25 0 1 0 481136300 43581440 9913 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10640 9913 603 41 0 10599 0
vsize: 42560
[startup+290.005 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10280 0 0 0 28969 33 0 0 25 0 1 0 481136300 45043712 10258 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10997 10258 603 41 0 10956 0
vsize: 43988
[startup+300.004 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10589 0 0 0 29968 34 0 0 25 0 1 0 481136300 46252032 10567 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11292 10567 603 41 0 11251 0
vsize: 45168
[startup+310.004 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 30968 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+320.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 31968 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+330.004 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 32969 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+340.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 33969 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+350.005 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 34969 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+360.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 35969 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+370.004 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 36969 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+380.004 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 37970 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+390.004 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 38970 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+400.005 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 39970 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+410.005 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 40970 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+420.005 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 41970 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+430.005 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 42971 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+440.006 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10675 0 0 0 43971 34 0 0 25 0 1 0 481136300 46649344 10653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10653 603 41 0 11348 0
vsize: 45556
[startup+450.005 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10677 0 0 0 44971 34 0 0 25 0 1 0 481136300 46649344 10655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10655 603 41 0 11348 0
vsize: 45556
[startup+460.005 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10679 0 0 0 45971 34 0 0 25 0 1 0 481136300 46649344 10657 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10657 603 41 0 11348 0
vsize: 45556
[startup+470.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10681 0 0 0 46971 34 0 0 25 0 1 0 481136300 46649344 10659 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10659 603 41 0 11348 0
vsize: 45556
[startup+480.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10684 0 0 0 47972 34 0 0 25 0 1 0 481136300 46649344 10662 4294967295 134512640 134672761 3221224560 3221223716 134560075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10662 603 41 0 11348 0
vsize: 45556
[startup+490.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 48972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+500.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 49972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+510.007 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 50971 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+520.008 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 51972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223744 134559489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+530.007 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 52972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223744 134558841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+540.008 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 53972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+550.008 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 54971 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+560.009 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 55971 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+570.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 56972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+580.011 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 20528
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 57972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+590.011 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 58972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+600.012 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 59972 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+610.012 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 60973 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+620.012 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 61973 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+630.012 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 62973 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+640.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 63973 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+650.013 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 64974 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+660.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 65974 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+670.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 66974 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+680.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 67974 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+690.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 68974 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+700.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10687 0 0 0 69975 34 0 0 25 0 1 0 481136300 46649344 10665 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10665 603 41 0 11348 0
vsize: 45556
[startup+710.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10689 0 0 0 70975 34 0 0 25 0 1 0 481136300 46649344 10667 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10667 603 41 0 11348 0
vsize: 45556
[startup+720.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10692 0 0 0 71975 34 0 0 25 0 1 0 481136300 46649344 10670 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10670 603 41 0 11348 0
vsize: 45556
[startup+730.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10694 0 0 0 72975 34 0 0 25 0 1 0 481136300 46649344 10672 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10672 603 41 0 11348 0
vsize: 45556
[startup+740.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10696 0 0 0 73975 34 0 0 25 0 1 0 481136300 46649344 10674 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10674 603 41 0 11348 0
vsize: 45556
[startup+750.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10699 0 0 0 74975 34 0 0 25 0 1 0 481136300 46649344 10677 4294967295 134512640 134672761 3221224560 3221223684 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10677 603 41 0 11348 0
vsize: 45556
[startup+760.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 75975 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+770.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 76975 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+780.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 77975 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+790.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 78976 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223744 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+800.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 79976 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+810.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20530
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10701 0 0 0 80976 34 0 0 25 0 1 0 481136300 46649344 10679 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10679 603 41 0 11348 0
vsize: 45556
[startup+820.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 81976 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+830.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 82976 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223744 134558934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+840.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 83977 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+850.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 84977 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223744 134558947 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+860.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 85977 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+870.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 86977 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+880.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 87977 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 88978 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+900.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 89978 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+910.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 90978 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+920.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 91978 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+930.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 92978 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+940.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 93979 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+950.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 10702 0 0 0 94979 34 0 0 25 0 1 0 481136300 46649344 10680 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11389 10680 603 41 0 11348 0
vsize: 45556
[startup+960.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 11027 0 0 0 95979 34 0 0 25 0 1 0 481136300 47988736 11005 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11716 11005 603 41 0 11675 0
vsize: 46864
[startup+970.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 11356 0 0 0 96978 35 0 0 25 0 1 0 481136300 49319936 11334 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12041 11334 603 41 0 12000 0
vsize: 48164
[startup+980.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 11684 0 0 0 97978 36 0 0 25 0 1 0 481136300 50647040 11662 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12365 11662 603 41 0 12324 0
vsize: 49460
[startup+990.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 11984 0 0 0 98977 37 0 0 25 0 1 0 481136300 51847168 11962 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12658 11962 603 41 0 12617 0
vsize: 50632
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12293 0 0 0 99976 38 0 0 25 0 1 0 481136300 53174272 12271 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12982 12271 603 41 0 12941 0
vsize: 51928
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12578 0 0 0 100975 39 0 0 25 0 1 0 481136300 54247424 12556 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13244 12556 603 41 0 13203 0
vsize: 52976
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 101975 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 102975 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 103975 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 104976 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 105976 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 106976 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 107976 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 108976 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 109977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 110977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 111977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 112977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 113977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 114977 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 115978 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12640 0 0 0 116978 39 0 0 25 0 1 0 481136300 54513664 12618 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13309 12618 603 41 0 13268 0
vsize: 53236
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 12959 0 0 0 117977 40 0 0 25 0 1 0 481136300 55836672 12937 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13632 12937 603 41 0 13591 0
vsize: 54528
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 13326 0 0 0 118977 41 0 0 25 0 1 0 481136300 57307136 13304 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13991 13304 603 41 0 13950 0
vsize: 55964
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 20532
Raw data (stat): 20475 (minisat+) R 20474 10614 10613 0 -1 0 13659 0 0 0 119975 42 0 0 25 0 1 0 481136300 58765312 13637 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14347 13637 603 41 0 14306 0
vsize: 57388
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 20532
Raw data (stat): 20475 (minisat+) Z 20474 10614 10613 0 -1 12 13662 0 0 0 119976 45 0 0 25 0 1 0 481136300 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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