PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        699388 kB
Buffers:         35412 kB
Cached:         188048 kB
SwapCached:       1212 kB
Active:         148528 kB
Inactive:       155272 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        699132 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25752 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:02:41 (client local time) WITH STATUS 10 IN 1200.49 SECONDS
stats: 4839 7 1200.49 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 41605 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41605    83210 |   13868       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  114334   253453 |   38111       0        0     nan |  0.000 % |
c |       100 |  114171   253088 |   41922      97      498     5.1 |  0.174 % |
c |       250 |  113686   251991 |   46114     232     1285     5.5 |  0.724 % |
c |       475 |  111537   247076 |   50725     397     2410     6.1 |  3.315 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       564 |  111119   246138 |   37039     481     2889     6.0 |  3.315 % |
c |       664 |  108736   240697 |   40742     526     3297     6.3 |  6.613 % |
c |       815 |  107054   236848 |   44817     651     4318     6.6 |  8.666 % |
c |      1040 |  104060   229956 |   49298     792     5839     7.4 | 12.425 % |
c |      1378 |  100225   221100 |   54228     979     6743     6.9 | 17.308 % |
c |      1884 |   94253   207286 |   59651    1301     9579     7.4 | 25.080 % |
c |      2643 |   88648   194310 |   65616    1879    14098     7.5 | 32.343 % |
c |      3784 |   75734   164164 |   72178    2532    20845     8.2 | 49.400 % |
c |      5493 |   67410   144634 |   79396    3514    30765     8.8 | 60.968 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6310 |   64049   136834 |   21349    3949    36266     9.2 | 60.968 % |
c |      6410 |   63495   135539 |   23483    3997    36735     9.2 | 66.592 % |
c |      6562 |   63107   134624 |   25832    4071    39131     9.6 | 67.280 % |
c |      6787 |   62258   132618 |   28415    4206    41213     9.8 | 68.358 % |
c |      7124 |   61454   130723 |   31257    4463    43805     9.8 | 69.500 % |
c |      7630 |   59164   125359 |   34382    4522    48842    10.8 | 72.687 % |
c |      8389 |   56640   119402 |   37821    4876    55041    11.3 | 76.231 % |
c |      9528 |   54760   114990 |   41603    5576    67110    12.0 | 78.866 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10453 |   54041   113271 |   18013    6292    87187    13.9 | 78.866 % |
c |     10553 |   53610   112253 |   19814    6248    86886    13.9 | 80.481 % |
c |     10703 |   53414   111794 |   21795    6344    89162    14.1 | 80.755 % |
c |     10929 |   53274   111464 |   23975    6473    93483    14.4 | 80.956 % |
c |     11267 |   53129   111123 |   26372    6751   102323    15.2 | 81.169 % |
c |     11773 |   52827   110415 |   29010    7084   119773    16.9 | 81.595 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11958 |   52627   109956 |   17542    7133   123037    17.2 | 81.595 % |
c |     12059 |   52262   109098 |   19296    7116   122951    17.3 | 82.412 % |
c |     12209 |   52262   109098 |   21225    7266   125577    17.3 | 82.412 % |
c |     12435 |   51949   108358 |   23348    7295   128371    17.6 | 82.870 % |
c |     12772 |   51875   108186 |   25683    7543   137405    18.2 | 82.970 % |
c |     13278 |   51875   108186 |   28251    8049   173476    21.6 | 82.970 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13913 |   51836   108072 |   17278    8640   213528    24.7 | 82.970 % |
c |     14013 |   51836   108072 |   19005    8740   215817    24.7 | 83.004 % |
c |     14163 |   51836   108072 |   20906    8890   218365    24.6 | 83.004 % |
c |     14388 |   51830   108058 |   22997    9111   227646    25.0 | 83.012 % |
c |     14726 |   51830   108058 |   25296    9449   249665    26.4 | 83.012 % |
c |     15232 |   51732   107828 |   27826    9905   263417    26.6 | 83.149 % |
c |     15991 |   51528   107347 |   30609   10380   312581    30.1 | 83.442 % |
c |     17130 |   51477   107226 |   33669   11476   383469    33.4 | 83.522 % |
c |     18838 |   51477   107226 |   37036   13184   511304    38.8 | 83.522 % |
c |     21402 |   51186   106539 |   40740   15310   709140    46.3 | 83.940 % |
c |     25246 |   51102   106342 |   44814   19122  1132551    59.2 | 84.061 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28872 |   51172   106517 |   17057   22748  1491875    65.6 | 84.061 % |
c |     28973 |   51172   106517 |   18762   22849  1496551    65.5 | 84.037 % |
c |     29124 |   51172   106517 |   20638   23000  1499475    65.2 | 84.037 % |
c |     29349 |   51172   106517 |   22702   23225  1509411    65.0 | 84.037 % |
c |     29686 |   51112   106373 |   24973   23482  1518559    64.7 | 84.129 % |
c |     30193 |   51112   106373 |   27470   23989  1548803    64.6 | 84.129 % |
c |     30952 |   51112   106373 |   30217   24748  1605268    64.9 | 84.129 % |
c |     32091 |   50976   106059 |   33239   25757  1657429    64.3 | 84.305 % |
c |     33799 |   50920   105928 |   36563   27405  1796193    65.5 | 84.381 % |
c |     36361 |   50886   105849 |   40219   29880  1963616    65.7 | 84.425 % |
c |     40205 |   50886   105849 |   44241   33724  2284557    67.7 | 84.425 % |
c |     45971 |   50711   105434 |   48665   39098  2762496    70.7 | 84.686 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46411 |   50684   105359 |   16894   39438  2782592    70.6 | 84.686 % |
c |     46511 |   50644   105266 |   18583   16841   949913    56.4 | 84.771 % |
c |     46662 |   50644   105266 |   20441   16992   955434    56.2 | 84.771 % |
c |     46890 |   50644   105266 |   22485   17220   972175    56.5 | 84.771 % |
c |     47228 |   50571   105093 |   24734   17495   993938    56.8 | 84.875 % |
c |     47734 |   50571   105093 |   27207   18001  1023698    56.9 | 84.875 % |
c |     48493 |   50571   105093 |   29928   18760  1071592    57.1 | 84.875 % |
c |     49633 |   50571   105093 |   32921   19900  1169713    58.8 | 84.875 % |
c |     51342 |   50504   104935 |   36213   21578  1291192    59.8 | 84.975 % |
c |     53907 |   50504   104935 |   39835   24143  1497711    62.0 | 84.975 % |
c |     57752 |   50498   104921 |   43818   27985  1782426    63.7 | 84.983 % |
c |     63518 |   50498   104921 |   48200   33751  2293550    68.0 | 84.983 % |
c |     72167 |   50498   104921 |   53020   42400  3082184    72.7 | 84.983 % |
c |     85142 |   50498   104921 |   58322   55375  3894729    70.3 | 84.983 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89343 |   50539   105022 |   16846   59576  4219576    70.8 | 84.983 % |
c |     89445 |   50539   105022 |   18530   18626   917328    49.2 | 84.948 % |
c |     89596 |   50539   105022 |   20383   18777   926071    49.3 | 84.948 % |
c |     89821 |   50539   105022 |   22422   19002   943962    49.7 | 84.948 % |
c |     90158 |   50539   105022 |   24664   19339   958158    49.5 | 84.948 % |
c |     90664 |   50478   104879 |   27130   19840   993861    50.1 | 85.036 % |
c |     91423 |   50478   104879 |   29843   20599  1031854    50.1 | 85.036 % |
c |     92562 |   50478   104879 |   32828   21738  1101012    50.6 | 85.036 % |
c |     94270 |   50478   104879 |   36110   23446  1199972    51.2 | 85.036 % |
c |     96832 |   50478   104879 |   39721   26008  1430267    55.0 | 85.036 % |
c |    100676 |   50478   104879 |   43694   29852  1697025    56.8 | 85.036 % |
c |    106442 |   50380   104649 |   48063   35609  2259596    63.5 | 85.172 % |
c |    115091 |   50380   104649 |   52869   44258  2945031    66.5 | 85.172 % |
c |    128065 |   50358   104597 |   58156   57228  3796363    66.3 | 85.204 % |
c |    147526 |   50273   104393 |   63972   76672  5565172    72.6 | 85.332 % |
c |    176718 |   50102   103989 |   70369   39078  2007290    51.4 | 85.580 % |
c |    220507 |   50096   103975 |   77406   82866  4384527    52.9 | 85.587 % |
c |    286195 |   50090   103961 |   85147   66937  4090683    61.1 | 85.595 % |
c |    384722 |   49955   103644 |   93662   76119  5195504    68.3 | 85.787 % |
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 -C75#### 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.94 0.90 2/53 15651
Raw data (stat): 15651 (runsolver) R 15650 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481793078 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.95 0.90 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 3108 0 0 0 990 7 0 0 25 0 1 0 481793078 15040512 3086 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3672 3086 603 41 0 3631 0
vsize: 14688
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 3108 0 0 0 1990 7 0 0 25 0 1 0 481793078 15040512 3086 4294967295 134512640 134672761 3221224560 3221223756 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3672 3086 603 41 0 3631 0
vsize: 14688
[startup+30.003 s]
Raw data (loadavg): 0.91 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 3109 0 0 0 2989 8 0 0 25 0 1 0 481793078 15040512 3087 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3672 3087 603 41 0 3631 0
vsize: 14688
[startup+40.0039 s]
Raw data (loadavg): 0.92 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 3350 0 0 0 3989 8 0 0 25 0 1 0 481793078 16166912 3328 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3947 3328 603 41 0 3906 0
vsize: 15788
[startup+50.0056 s]
Raw data (loadavg): 0.93 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 4079 0 0 0 4987 11 0 0 25 0 1 0 481793078 19087360 4057 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4660 4057 603 41 0 4619 0
vsize: 18640
[startup+60.0062 s]
Raw data (loadavg): 0.94 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 4765 0 0 0 5984 13 0 0 25 0 1 0 481793078 21946368 4743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5358 4743 603 41 0 5317 0
vsize: 21432
[startup+70.0062 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 5214 0 0 0 6984 14 0 0 25 0 1 0 481793078 23691264 5192 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5784 5192 603 41 0 5743 0
vsize: 23136
[startup+80.0069 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 5660 0 0 0 7982 16 0 0 25 0 1 0 481793078 25694208 5638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6273 5638 603 41 0 6232 0
vsize: 25092
[startup+90.0075 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6103 0 0 0 8982 17 0 0 25 0 1 0 481793078 27435008 6081 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6698 6081 603 41 0 6657 0
vsize: 26792
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6103 0 0 0 9982 17 0 0 25 0 1 0 481793078 27435008 6081 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6698 6081 603 41 0 6657 0
vsize: 26792
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6103 0 0 0 10982 17 0 0 25 0 1 0 481793078 27435008 6081 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6698 6081 603 41 0 6657 0
vsize: 26792
[startup+120.01 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6103 0 0 0 11982 17 0 0 25 0 1 0 481793078 27435008 6081 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6698 6081 603 41 0 6657 0
vsize: 26792
[startup+130.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6227 0 0 0 12982 17 0 0 25 0 1 0 481793078 27963392 6205 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6827 6205 603 41 0 6786 0
vsize: 27308
[startup+140.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6583 0 0 0 13981 18 0 0 25 0 1 0 481793078 29425664 6561 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7184 6561 603 41 0 7143 0
vsize: 28736
[startup+150.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 6841 0 0 0 14981 19 0 0 25 0 1 0 481793078 30474240 6819 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7440 6819 603 41 0 7399 0
vsize: 29760
[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7061 0 0 0 15980 20 0 0 25 0 1 0 481793078 31399936 7039 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7666 7039 603 41 0 7625 0
vsize: 30664
[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7292 0 0 0 16980 20 0 0 25 0 1 0 481793078 32329728 7270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7893 7270 603 41 0 7852 0
vsize: 31572
[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7618 0 0 0 17979 21 0 0 25 0 1 0 481793078 33656832 7596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8217 7596 603 41 0 8176 0
vsize: 32868
[startup+190.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 18979 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 19979 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 20979 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 21979 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 22979 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 23980 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 24980 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 25980 21 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+270.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7789 0 0 0 26980 22 0 0 25 0 1 0 481793078 34263040 7767 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8365 7767 603 41 0 8324 0
vsize: 33460
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 7886 0 0 0 27980 22 0 0 25 0 1 0 481793078 34660352 7864 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8462 7864 603 41 0 8421 0
vsize: 33848
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 8248 0 0 0 28979 23 0 0 25 0 1 0 481793078 36384768 8226 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8883 8226 603 41 0 8842 0
vsize: 35532
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 8621 0 0 0 29979 23 0 0 25 0 1 0 481793078 37982208 8599 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9273 8599 603 41 0 9232 0
vsize: 37092
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 8954 0 0 0 30978 25 0 0 25 0 1 0 481793078 39309312 8932 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9597 8932 603 41 0 9556 0
vsize: 38388
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 9253 0 0 0 31977 25 0 0 25 0 1 0 481793078 40513536 9231 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9891 9231 603 41 0 9850 0
vsize: 39564
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 9553 0 0 0 32976 27 0 0 25 0 1 0 481793078 41734144 9531 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10189 9531 603 41 0 10148 0
vsize: 40756
[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 9807 0 0 0 33976 27 0 0 25 0 1 0 481793078 42807296 9785 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10451 9785 603 41 0 10410 0
vsize: 41804
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10027 0 0 0 34976 28 0 0 25 0 1 0 481793078 43618304 10005 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10649 10005 603 41 0 10608 0
vsize: 42596
[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 35975 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 36975 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+380.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 37975 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 38976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 39976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+410.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 40975 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 41976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 42976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 43976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 44976 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+460.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 45977 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10173 0 0 0 46977 29 0 0 25 0 1 0 481793078 44290048 10151 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10151 603 41 0 10772 0
vsize: 43252
[startup+480.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 47977 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+490.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 48977 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 49978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 50978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+520.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 51978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 52978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 53978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 54979 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10174 0 0 0 55978 29 0 0 25 0 1 0 481793078 44290048 10152 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10152 603 41 0 10772 0
vsize: 43252
[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10195 0 0 0 56978 29 0 0 25 0 1 0 481793078 44449792 10173 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10173 603 41 0 10811 0
vsize: 43408
[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10199 0 0 0 57978 29 0 0 25 0 1 0 481793078 44449792 10177 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10177 603 41 0 10811 0
vsize: 43408
[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10202 0 0 0 58979 29 0 0 25 0 1 0 481793078 44449792 10180 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10180 603 41 0 10811 0
vsize: 43408
[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10205 0 0 0 59979 29 0 0 25 0 1 0 481793078 44449792 10183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10183 603 41 0 10811 0
vsize: 43408
[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10208 0 0 0 60979 29 0 0 25 0 1 0 481793078 44449792 10186 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10186 603 41 0 10811 0
vsize: 43408
[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 61979 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+630.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 62980 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 63980 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 64980 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 65980 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 66981 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 67981 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 68981 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 69981 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 70982 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 71982 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 72982 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+740.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 73982 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+750.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 74983 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+760.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10209 0 0 0 75983 29 0 0 25 0 1 0 481793078 44449792 10187 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10852 10187 603 41 0 10811 0
vsize: 43408
[startup+770.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10211 0 0 0 76982 29 0 0 25 0 1 0 481793078 44449792 10189 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10189 603 41 0 10811 0
vsize: 43408
[startup+780.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10211 0 0 0 77983 29 0 0 25 0 1 0 481793078 44449792 10189 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10189 603 41 0 10811 0
vsize: 43408
[startup+790.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10228 0 0 0 78983 29 0 0 25 0 1 0 481793078 44449792 10206 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10206 603 41 0 10811 0
vsize: 43408
[startup+800.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10229 0 0 0 79983 29 0 0 25 0 1 0 481793078 44449792 10207 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10207 603 41 0 10811 0
vsize: 43408
[startup+810.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10229 0 0 0 80983 29 0 0 25 0 1 0 481793078 44449792 10207 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10207 603 41 0 10811 0
vsize: 43408
[startup+820.061 s]
Raw data (loadavg): 1.07 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10229 0 0 0 81984 29 0 0 25 0 1 0 481793078 44449792 10207 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10852 10207 603 41 0 10811 0
vsize: 43408
[startup+830.062 s]
Raw data (loadavg): 1.06 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10391 0 0 0 82983 30 0 0 25 0 1 0 481793078 45121536 10369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11016 10369 603 41 0 10975 0
vsize: 44064
[startup+840.063 s]
Raw data (loadavg): 1.05 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10690 0 0 0 83983 31 0 0 25 0 1 0 481793078 46452736 10668 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11341 10668 603 41 0 11300 0
vsize: 45364
[startup+850.064 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 10986 0 0 0 84982 31 0 0 25 0 1 0 481793078 47648768 10964 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11633 10964 603 41 0 11592 0
vsize: 46532
[startup+860.064 s]
Raw data (loadavg): 1.04 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11228 0 0 0 85982 32 0 0 25 0 1 0 481793078 48574464 11206 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11859 11206 603 41 0 11818 0
vsize: 47436
[startup+870.065 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11429 0 0 0 86981 33 0 0 25 0 1 0 481793078 49364992 11407 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11407 603 41 0 12011 0
vsize: 48208
[startup+880.066 s]
Raw data (loadavg): 1.03 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11429 0 0 0 87981 33 0 0 25 0 1 0 481793078 49364992 11407 4294967295 134512640 134672761 3221224560 3221223632 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11407 603 41 0 12011 0
vsize: 48208
[startup+890.067 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11430 0 0 0 88981 33 0 0 25 0 1 0 481793078 49364992 11408 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11408 603 41 0 12011 0
vsize: 48208
[startup+900.067 s]
Raw data (loadavg): 1.02 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11430 0 0 0 89982 33 0 0 25 0 1 0 481793078 49364992 11408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11408 603 41 0 12011 0
vsize: 48208
[startup+910.068 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11430 0 0 0 90982 33 0 0 25 0 1 0 481793078 49364992 11408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11408 603 41 0 12011 0
vsize: 48208
[startup+920.069 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11430 0 0 0 91982 33 0 0 25 0 1 0 481793078 49364992 11408 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11408 603 41 0 12011 0
vsize: 48208
[startup+930.069 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11435 0 0 0 92982 33 0 0 25 0 1 0 481793078 49364992 11413 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 11413 603 41 0 12011 0
vsize: 48208
[startup+940.071 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11440 0 0 0 93982 33 0 0 25 0 1 0 481793078 49520640 11418 4294967295 134512640 134672761 3221224560 3221223744 134559403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11418 603 41 0 12049 0
vsize: 48360
[startup+950.071 s]
Raw data (loadavg): 1.01 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 94983 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+960.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 95983 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+970.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 96983 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+980.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 97983 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+990.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 98984 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223744 134558914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11441 0 0 0 99984 33 0 0 25 0 1 0 481793078 49520640 11419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11419 603 41 0 12049 0
vsize: 48360
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11448 0 0 0 100984 33 0 0 25 0 1 0 481793078 49520640 11426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11426 603 41 0 12049 0
vsize: 48360
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11449 0 0 0 101984 33 0 0 25 0 1 0 481793078 49520640 11427 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11427 603 41 0 12049 0
vsize: 48360
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11450 0 0 0 102985 33 0 0 25 0 1 0 481793078 49520640 11428 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11428 603 41 0 12049 0
vsize: 48360
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/53 15651
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11464 0 0 0 103984 34 0 0 25 0 1 0 481793078 49520640 11442 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11442 603 41 0 12049 0
vsize: 48360
[startup+1050.26 s]
Raw data (loadavg): 1.00 0.99 0.91 3/56 15687
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11464 0 0 0 105000 35 0 0 25 0 1 0 481793078 49520640 11442 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11442 603 41 0 12049 0
vsize: 48360
[startup+1060.32 s]
Raw data (loadavg): 1.15 1.02 0.93 4/57 15703
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11464 0 0 0 106007 35 0 0 25 0 1 0 481793078 49520640 11442 4294967295 134512640 134672761 3221224560 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12090 11442 603 41 0 12049 0
vsize: 48360
[startup+1070.32 s]
Raw data (loadavg): 1.13 1.02 0.93 2/53 15704
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11469 0 0 0 107007 35 0 0 25 0 1 0 481793078 49684480 11447 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12130 11447 603 41 0 12089 0
vsize: 48520
[startup+1080.32 s]
Raw data (loadavg): 1.19 1.03 0.93 2/53 15704
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11469 0 0 0 108007 35 0 0 25 0 1 0 481793078 49684480 11447 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12130 11447 603 41 0 12089 0
vsize: 48520
[startup+1090.32 s]
Raw data (loadavg): 1.16 1.03 0.93 2/53 15704
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11469 0 0 0 109007 35 0 0 25 0 1 0 481793078 49684480 11447 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12130 11447 603 41 0 12089 0
vsize: 48520
[startup+1100.33 s]
Raw data (loadavg): 1.13 1.03 0.93 2/53 15704
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11469 0 0 0 110008 35 0 0 25 0 1 0 481793078 49684480 11447 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12130 11447 603 41 0 12089 0
vsize: 48520
[startup+1110.33 s]
Raw data (loadavg): 1.11 1.03 0.93 2/53 15704
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11474 0 0 0 111008 35 0 0 25 0 1 0 481793078 49684480 11452 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12130 11452 603 41 0 12089 0
vsize: 48520
[startup+1120.33 s]
Raw data (loadavg): 1.10 1.03 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11526 0 0 0 112008 35 0 0 25 0 1 0 481793078 49815552 11504 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12162 11504 603 41 0 12121 0
vsize: 48648
[startup+1130.33 s]
Raw data (loadavg): 1.08 1.03 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11667 0 0 0 113008 36 0 0 25 0 1 0 481793078 50479104 11645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12324 11645 603 41 0 12283 0
vsize: 49296
[startup+1140.33 s]
Raw data (loadavg): 1.07 1.03 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11815 0 0 0 114007 36 0 0 25 0 1 0 481793078 51007488 11793 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12453 11793 603 41 0 12412 0
vsize: 49812
[startup+1150.33 s]
Raw data (loadavg): 1.06 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 11953 0 0 0 115007 37 0 0 25 0 1 0 481793078 51679232 11931 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12617 11931 603 41 0 12576 0
vsize: 50468
[startup+1160.34 s]
Raw data (loadavg): 1.05 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 12105 0 0 0 116007 37 0 0 25 0 1 0 481793078 52203520 12083 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12745 12083 603 41 0 12704 0
vsize: 50980
[startup+1170.34 s]
Raw data (loadavg): 1.04 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 12274 0 0 0 117007 38 0 0 25 0 1 0 481793078 53010432 12252 4294967295 134512640 134672761 3221224560 3221223644 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12942 12252 603 41 0 12901 0
vsize: 51768
[startup+1180.34 s]
Raw data (loadavg): 1.03 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 12334 0 0 0 118007 39 0 0 25 0 1 0 481793078 53141504 12312 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12974 12312 603 41 0 12933 0
vsize: 51896
[startup+1190.34 s]
Raw data (loadavg): 1.03 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 12334 0 0 0 119007 39 0 0 25 0 1 0 481793078 53141504 12312 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12974 12312 603 41 0 12933 0
vsize: 51896
[startup+1200.34 s]
Raw data (loadavg): 1.02 1.02 0.93 2/53 15706
Raw data (stat): 15651 (minisat+) R 15650 7987 7986 0 -1 0 12334 0 0 0 120007 39 0 0 25 0 1 0 481793078 53141504 12312 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12974 12312 603 41 0 12933 0
vsize: 51896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.38 s]
Raw data (loadavg): 1.02 1.02 0.93 1/53 15706
Raw data (stat): 15651 (minisat+) Z 15650 7987 7986 0 -1 12 12337 0 0 0 120007 41 0 0 25 0 1 0 481793078 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.38
CPU time (s): 1200.49
CPU user time (s): 1200.08
CPU system time (s): 0.414936
CPU usage (%): 100.01
Max. virtual memory (Kb): 51896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####