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-1.opb
MD5SUM	94f501465233508e2f652cf118ddaf2d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-31
Optimality of the best value was proved	NO
Number of terms in the objective function	760
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	760
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	760
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.06
Number of variables	760
Total number of constraints	41314
Number of constraints which are clauses	41314
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 5240

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        907784 kB
Buffers:         34220 kB
Cached:          72656 kB
SwapCached:        564 kB
Active:          52368 kB
Inactive:        57932 kB
HighTotal:      131008 kB
HighFree:        54432 kB
LowTotal:       903652 kB
LowFree:        853352 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11100 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:12:00 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3708 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41314 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 |   41314    82628 |   13771       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1492   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   51518   119121 |   17172       0        0     nan |  0.000 % |
c |       100 |   51518   119121 |   18889     100      845     8.4 |  0.226 % |
c |       250 |   51509   119090 |   20778     247     2224     9.0 |  0.273 % |
c |       475 |   51500   119059 |   22855     470     4099     8.7 |  0.315 % |
c |       814 |   51491   119028 |   25141     807     8129    10.1 |  0.358 % |
c |      1320 |   51464   118935 |   27655    1306    13493    10.3 |  0.492 % |
c |      2079 |   51410   118749 |   30421    2048    23207    11.3 |  0.805 % |
c |      3219 |   51311   118408 |   33463    3157    82591    26.2 |  1.252 % |
c |      4927 |   50840   116795 |   36809    4740   109311    23.1 |  3.891 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5789 |   50519   115682 |   16839    5491   125439    22.8 |  3.891 % |
c |      5889 |   50508   115643 |   18522    5588   127161    22.8 |  6.130 % |
c |      6039 |   50450   115445 |   20375    5724   131698    23.0 |  6.487 % |
c |      6264 |   50328   115025 |   22412    5911   135174    22.9 |  7.335 % |
c |      6601 |   50132   114351 |   24653    6198   140437    22.7 |  8.632 % |
c |      7107 |   50034   114015 |   27119    6676   154571    23.2 |  9.347 % |
c |      7866 |   49697   112856 |   29831    7314   178767    24.4 | 11.762 % |
c |      9005 |   49594   112501 |   32814    8422   244309    29.0 | 12.570 % |
c |     10715 |   49312   111533 |   36095   10029   297102    29.6 | 14.539 % |
c |     13277 |   49065   110684 |   39705   12503   405130    32.4 | 16.547 % |
c |     17123 |   48899   110106 |   43676   16255   748617    46.1 | 18.023 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 32   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21652 |   48926   110180 |   16308   20606  1044528    50.7 | 18.023 % |
c |     21753 |   48892   110062 |   17938   10390   591682    56.9 | 18.930 % |
c |     21905 |   48871   109987 |   19732   10536   596316    56.6 | 19.154 % |
c |     22130 |   48840   109880 |   21705   10757   601746    55.9 | 19.416 % |
c |     22467 |   48772   109644 |   23876   11079   622017    56.1 | 19.947 % |
c |     22973 |   48763   109613 |   26264   11564   661765    57.2 | 19.991 % |
c |     23732 |   48707   109421 |   28890   12305   693225    56.3 | 20.345 % |
c |     24875 |   48690   109362 |   31779   13445   773713    57.5 | 20.478 % |
c |     26583 |   48495   108685 |   34957   15114   874195    57.8 | 22.070 % |
c |     29145 |   48396   108342 |   38453   17572  1120612    63.8 | 22.645 % |
c |     32989 |   48347   108173 |   42298   21357  1511085    70.8 | 22.999 % |
c |     38755 |   48232   107772 |   46528   27026  2008606    74.3 | 23.927 % |
c |     47404 |   48210   107694 |   51181   35668  2845031    79.8 | 24.104 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53815 |   48192   107634 |   16064   42075  3516949    83.6 | 24.104 % |
c |     53915 |   48192   107634 |   17670   16676  1209106    72.5 | 24.315 % |
c |     54066 |   48192   107634 |   19437   16827  1217350    72.3 | 24.315 % |
c |     54292 |   48192   107634 |   21381   17053  1228025    72.0 | 24.315 % |
c |     54629 |   48181   107595 |   23519   17386  1240237    71.3 | 24.403 % |
c |     55135 |   48181   107595 |   25871   17892  1278613    71.5 | 24.403 % |
c |     55895 |   48139   107449 |   28458   18635  1324524    71.1 | 24.757 % |
c |     57034 |   48139   107449 |   31304   19774  1424380    72.0 | 24.757 % |
c |     58743 |   48041   107111 |   34434   21462  1542503    71.9 | 25.464 % |
c |     61306 |   48026   107056 |   37878   24020  1723527    71.8 | 25.644 % |
c |     65151 |   48020   107036 |   41665   27860  2036934    73.1 | 25.690 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68565 |   47971   106880 |   15990   31207  2355182    75.5 | 25.690 % |
c |     68665 |   47971   106880 |   17589   15704   939293    59.8 | 26.072 % |
c |     68815 |   47971   106880 |   19347   15854   944741    59.6 | 26.072 % |
c |     69040 |   47971   106880 |   21282   16079   958216    59.6 | 26.074 % |
c |     69377 |   47971   106880 |   23410   16416   977143    59.5 | 26.072 % |
c |     69883 |   47960   106841 |   25752   16914   998205    59.0 | 26.160 % |
c |     70645 |   47938   106763 |   28327   17665  1039029    58.8 | 26.337 % |
c |     71785 |   47894   106615 |   31159   18784  1106314    58.9 | 26.734 % |
c |     73495 |   47886   106587 |   34275   20489  1226054    59.8 | 26.826 % |
c |     76057 |   47886   106587 |   37703   23051  1402563    60.8 | 26.823 % |
c |     79901 |   47815   106342 |   41473   26860  1906641    71.0 | 27.397 % |
c |     85667 |   47815   106342 |   45621   32626  2379271    72.9 | 27.400 % |
c |     94318 |   47815   106342 |   50183   41277  3184512    77.1 | 27.400 % |
c |    107294 |   47815   106342 |   55201   18541  1264623    68.2 | 27.400 % |
c |    126756 |   47778   106213 |   60721   37993  3328654    87.6 | 27.662 % |
c |    155948 |   47742   106091 |   66794   21092  1462978    69.4 | 27.932 % |
c |    199737 |   47742   106091 |   73473   64881  7294868   112.4 | 27.931 % |
c |    265421 |   47742   106091 |   80820   71991  8913319   123.8 | 27.931 % |
c |    363948 |   47742   106091 |   88903   39882  4441953   111.4 | 27.931 % |
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 #### 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.85 0.97 0.91 2/54 1052
Raw data (stat): 1052 (runsolver) R 1051 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421472041 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+10.0005 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 2132 0 0 0 992 6 0 0 25 0 1 0 421472041 10383360 2110 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2535 2110 603 41 0 2494 0
vsize: 10140
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 2338 0 0 0 1991 7 0 0 25 0 1 0 421472041 11194368 2316 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2733 2316 603 41 0 2692 0
vsize: 10932
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 2765 0 0 0 2989 8 0 0 25 0 1 0 421472041 12943360 2743 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3160 2743 603 41 0 3119 0
vsize: 12640
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 3531 0 0 0 3987 11 0 0 25 0 1 0 421472041 16039936 3509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3916 3509 603 41 0 3875 0
vsize: 15664
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 4220 0 0 0 4985 13 0 0 25 0 1 0 421472041 18989056 4198 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4636 4198 603 41 0 4595 0
vsize: 18544
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 4860 0 0 0 5983 15 0 0 25 0 1 0 421472041 21663744 4838 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5289 4838 603 41 0 5248 0
vsize: 21156
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5034 0 0 0 6982 16 0 0 25 0 1 0 421472041 22335488 5012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5012 603 41 0 5412 0
vsize: 21812
[startup+80.0028 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5034 0 0 0 7982 16 0 0 25 0 1 0 421472041 22335488 5012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5012 603 41 0 5412 0
vsize: 21812
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5034 0 0 0 8982 16 0 0 25 0 1 0 421472041 22335488 5012 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5012 603 41 0 5412 0
vsize: 21812
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5034 0 0 0 9982 16 0 0 25 0 1 0 421472041 22335488 5012 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5012 603 41 0 5412 0
vsize: 21812
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5034 0 0 0 10983 16 0 0 25 0 1 0 421472041 22335488 5012 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5012 603 41 0 5412 0
vsize: 21812
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5036 0 0 0 11983 16 0 0 25 0 1 0 421472041 22335488 5014 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5453 5014 603 41 0 5412 0
vsize: 21812
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5431 0 0 0 12982 17 0 0 25 0 1 0 421472041 23945216 5409 4294967295 134512640 134672761 3221224560 3221223716 134565164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5846 5409 603 41 0 5805 0
vsize: 23384
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5700 0 0 0 13981 17 0 0 25 0 1 0 421472041 25018368 5678 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5678 603 41 0 6067 0
vsize: 24432
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5700 0 0 0 14982 17 0 0 25 0 1 0 421472041 25018368 5678 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5678 603 41 0 6067 0
vsize: 24432
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5700 0 0 0 15982 17 0 0 25 0 1 0 421472041 25018368 5678 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5678 603 41 0 6067 0
vsize: 24432
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5700 0 0 0 16982 17 0 0 25 0 1 0 421472041 25018368 5678 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5678 603 41 0 6067 0
vsize: 24432
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 5700 0 0 0 17982 17 0 0 25 0 1 0 421472041 25018368 5678 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6108 5678 603 41 0 6067 0
vsize: 24432
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 6095 0 0 0 18981 18 0 0 25 0 1 0 421472041 26636288 6073 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6503 6073 603 41 0 6462 0
vsize: 26012
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 6669 0 0 0 19980 20 0 0 25 0 1 0 421472041 29057024 6647 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7094 6647 603 41 0 7053 0
vsize: 28376
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 6955 0 0 0 20979 21 0 0 25 0 1 0 421472041 30121984 6933 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7354 6933 603 41 0 7313 0
vsize: 29416
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7292 0 0 0 21978 23 0 0 25 0 1 0 421472041 31596544 7270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7714 7270 603 41 0 7673 0
vsize: 30856
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 22978 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 23978 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 24978 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 25978 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 26978 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7330 0 0 0 27979 23 0 0 25 0 1 0 421472041 31727616 7308 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7308 603 41 0 7705 0
vsize: 30984
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7335 0 0 0 28979 23 0 0 25 0 1 0 421472041 31727616 7313 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7746 7313 603 41 0 7705 0
vsize: 30984
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7363 0 0 0 29979 23 0 0 25 0 1 0 421472041 31887360 7341 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7785 7341 603 41 0 7744 0
vsize: 31140
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 7738 0 0 0 30977 25 0 0 25 0 1 0 421472041 33476608 7716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8173 7716 603 41 0 8132 0
vsize: 32692
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 8106 0 0 0 31976 26 0 0 25 0 1 0 421472041 34938880 8084 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8530 8084 603 41 0 8489 0
vsize: 34120
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 8475 0 0 0 32975 27 0 0 25 0 1 0 421472041 36392960 8453 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8885 8453 603 41 0 8844 0
vsize: 35540
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 8868 0 0 0 33974 28 0 0 25 0 1 0 421472041 38133760 8846 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9310 8846 603 41 0 9269 0
vsize: 37240
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 9251 0 0 0 34973 30 0 0 25 0 1 0 421472041 39596032 9229 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9667 9229 603 41 0 9626 0
vsize: 38668
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 9622 0 0 0 35971 31 0 0 25 0 1 0 421472041 41463808 9600 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10123 9600 603 41 0 10082 0
vsize: 40492
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10024 0 0 0 36969 33 0 0 25 0 1 0 421472041 43081728 10002 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10518 10002 603 41 0 10477 0
vsize: 42072
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10354 0 0 0 37968 34 0 0 25 0 1 0 421472041 44425216 10332 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10846 10332 603 41 0 10805 0
vsize: 43384
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10658 0 0 0 38967 35 0 0 25 0 1 0 421472041 45637632 10636 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10636 603 41 0 11101 0
vsize: 44568
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10659 0 0 0 39968 35 0 0 25 0 1 0 421472041 45637632 10637 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10637 603 41 0 11101 0
vsize: 44568
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 40968 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223664 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 41968 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 42968 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 43969 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 44969 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 45969 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 46969 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1052
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10661 0 0 0 47969 35 0 0 25 0 1 0 421472041 45637632 10639 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10639 603 41 0 11101 0
vsize: 44568
[startup+490.015 s]
Raw data (loadavg): 1.07 0.99 0.92 2/56 1092
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10664 0 0 0 48970 35 0 0 25 0 1 0 421472041 45637632 10642 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10642 603 41 0 11101 0
vsize: 44568
[startup+500.016 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10673 0 0 0 49970 35 0 0 25 0 1 0 421472041 45637632 10651 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10651 603 41 0 11101 0
vsize: 44568
[startup+510.017 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10674 0 0 0 50970 35 0 0 25 0 1 0 421472041 45637632 10652 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10652 603 41 0 11101 0
vsize: 44568
[startup+520.017 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10676 0 0 0 51970 35 0 0 25 0 1 0 421472041 45637632 10654 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11142 10654 603 41 0 11101 0
vsize: 44568
[startup+530.017 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10700 0 0 0 52971 35 0 0 25 0 1 0 421472041 45821952 10678 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 10678 603 41 0 11146 0
vsize: 44748
[startup+540.017 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10712 0 0 0 53971 35 0 0 25 0 1 0 421472041 45821952 10690 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 10690 603 41 0 11146 0
vsize: 44748
[startup+550.018 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 1105
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 10715 0 0 0 54971 35 0 0 25 0 1 0 421472041 45821952 10693 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 10693 603 41 0 11146 0
vsize: 44748
[startup+560.017 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 11013 0 0 0 55970 36 0 0 25 0 1 0 421472041 47153152 10991 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11512 10991 603 41 0 11471 0
vsize: 46048
[startup+570.017 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 11282 0 0 0 56969 37 0 0 25 0 1 0 421472041 48291840 11260 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11790 11260 603 41 0 11749 0
vsize: 47160
[startup+580.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 11553 0 0 0 57968 38 0 0 25 0 1 0 421472041 49524736 11531 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12091 11531 603 41 0 12050 0
vsize: 48364
[startup+590.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 11833 0 0 0 58968 39 0 0 25 0 1 0 421472041 50589696 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12351 11811 603 41 0 12310 0
vsize: 49404
[startup+600.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 59967 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223664 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+610.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 60967 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+620.019 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 61967 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 62968 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+640.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 63968 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+650.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 64968 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 65968 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+670.021 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 66968 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+680.022 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 67969 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 68969 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+700.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 69969 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 70969 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 71969 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 72970 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+740.024 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 73970 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+750.041 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12178 0 0 0 74972 40 0 0 25 0 1 0 421472041 52068352 12156 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12712 12156 603 41 0 12671 0
vsize: 50848
[startup+760.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12205 0 0 0 75972 40 0 0 25 0 1 0 421472041 52269056 12183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12761 12183 603 41 0 12720 0
vsize: 51044
[startup+770.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12257 0 0 0 76972 40 0 0 25 0 1 0 421472041 52416512 12235 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12797 12235 603 41 0 12756 0
vsize: 51188
[startup+780.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12631 0 0 0 77971 41 0 0 25 0 1 0 421472041 54022144 12609 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13189 12609 603 41 0 13148 0
vsize: 52756
[startup+790.042 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 12941 0 0 0 78970 42 0 0 25 0 1 0 421472041 55296000 12919 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13500 12919 603 41 0 13459 0
vsize: 54000
[startup+800.043 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1107
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13253 0 0 0 79969 43 0 0 25 0 1 0 421472041 56639488 13231 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13828 13231 603 41 0 13787 0
vsize: 55312
[startup+810.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 80969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+820.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 81969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+830.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 82969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+840.044 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 83969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+850.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 84970 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+860.046 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 85969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+870.045 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 86968 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+880.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 87969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+890.047 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 88969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+900.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 89969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223664 134554753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+910.048 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 90969 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+920.049 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 91970 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+930.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 92970 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+940.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 93970 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+950.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 94970 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+960.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 95971 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+970.052 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13403 0 0 0 96971 44 0 0 25 0 1 0 421472041 57176064 13381 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13381 603 41 0 13918 0
vsize: 55836
[startup+980.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13405 0 0 0 97971 44 0 0 25 0 1 0 421472041 57176064 13383 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13383 603 41 0 13918 0
vsize: 55836
[startup+990.053 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13408 0 0 0 98971 44 0 0 25 0 1 0 421472041 57176064 13386 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13386 603 41 0 13918 0
vsize: 55836
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 99971 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 100972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 101972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 102972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 103972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 104972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 105972 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 106973 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 107973 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 108973 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223744 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 109973 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 110973 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 111974 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 112974 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 113974 44 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 114974 45 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 115974 45 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13411 0 0 0 116974 45 0 0 25 0 1 0 421472041 57176064 13389 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13389 603 41 0 13918 0
vsize: 55836
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13412 0 0 0 117975 45 0 0 25 0 1 0 421472041 57176064 13390 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13390 603 41 0 13918 0
vsize: 55836
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13412 0 0 0 118975 45 0 0 25 0 1 0 421472041 57176064 13390 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13390 603 41 0 13918 0
vsize: 55836
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 1109
Raw data (stat): 1052 (minisat+) R 1051 30854 30853 0 -1 0 13412 0 0 0 119975 45 0 0 25 0 1 0 421472041 57176064 13390 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13959 13390 603 41 0 13918 0
vsize: 55836
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 1109
Raw data (stat): 1052 (minisat+) Z 1051 30854 30853 0 -1 12 13415 0 0 0 119975 47 0 0 25 0 1 0 421472041 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.09
CPU time (s): 1200.23
CPU user time (s): 1199.76
CPU system time (s): 0.475927
CPU usage (%): 100.012
Max. virtual memory (Kb): 55836
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####