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/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb
MD5SUM	a8596c98551f801a6658f1ce91b33278
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1053
Optimality of the best value was proved	NO
Number of terms in the objective function	304
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	12887
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	12887
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.97785
Number of variables	304
Total number of constraints	671
Number of constraints which are clauses	671
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	1
Maximum length of a constraint	28
Trace number 5967

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 02:31:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4389 boxname=wulflinc32 idbench=253 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a8596c98551f801a6658f1ce91b33278  /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb /oldhome/oroussel/tmp/wulflinc32/normalized-cmb.opb
IDLAUNCH: 4389
/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:        704988 kB
Buffers:         35212 kB
Cached:         182876 kB
SwapCached:       1212 kB
Active:         146536 kB
Inactive:       151964 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        704732 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25296 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:51:38 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 4389 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 667 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 |     667     3359 |     222       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:43621     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  105121   247278 |   35040       0        0     nan |  0.000 % |
c |       103 |  104168   245118 |   38544      97     4313    44.5 |  0.665 % |
c |       253 |  103349   243238 |   42398     229     8034    35.1 |  1.287 % |
c |       479 |  103349   243238 |   46638     455    17849    39.2 |  1.287 % |
c |       816 |  103349   243238 |   51302     792    23717    29.9 |  1.287 % |
c |      1322 |  103349   243238 |   56432    1298    40177    31.0 |  1.287 % |
c |      2083 |  103122   242717 |   62075    2058    75941    36.9 |  1.487 % |
c |      3222 |  102780   241953 |   68283    3169   126886    40.0 |  1.754 % |
c |      4932 |  102722   241821 |   75111    4870   197921    40.6 |  1.797 % |
c |      7495 |  102722   241821 |   82622    7433   294908    39.7 |  1.797 % |
c ==============================================================================
c [1mFound solution: 1514[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36082     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8239 |  189796   445156 |   63265    8177   316528    38.7 |  1.797 % |
c |      8339 |  189796   445156 |   69591    8277   322185    38.9 |  1.049 % |
c |      8490 |  189796   445156 |   76550    8428   326473    38.7 |  1.049 % |
c |      8715 |  189774   445107 |   84205    8650   331229    38.3 |  1.059 % |
c |      9052 |  189647   444838 |   92626    8982   333087    37.1 |  1.125 % |
c |      9558 |  189568   444660 |  101888    9486   337879    35.6 |  1.152 % |
c ==============================================================================
c [1mFound solution: 1498[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9601 |  189573   444797 |   63191    9529   339448    35.6 |  1.152 % |
c ==============================================================================
c [1mFound solution: 1490[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9608 |  189907   445610 |   63302    9536   339814    35.6 |  1.152 % |
c ==============================================================================
c [1mFound solution: 1450[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9611 |  189928   445664 |   63309    9539   340630    35.7 |  1.152 % |
c ==============================================================================
c [1mFound solution: 1416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9623 |  190264   446559 |   63421    9551   341049    35.7 |  1.152 % |
c |      9724 |  190264   446559 |   69763    9652   348331    36.1 |  1.152 % |
c |      9874 |  190264   446559 |   76739    9802   364696    37.2 |  1.152 % |
c |     10099 |  190252   446532 |   84413   10026   380599    38.0 |  1.157 % |
c |     10439 |  190252   446532 |   92854   10366   387470    37.4 |  1.157 % |
c |     10945 |  190252   446532 |  102140   10872   406819    37.4 |  1.157 % |
c ==============================================================================
c [1mFound solution: 1326[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11585 |  190286   446619 |   63428   11512   555064    48.2 |  1.157 % |
c |     11686 |  190286   446619 |   69770   11613   558245    48.1 |  1.158 % |
c |     11839 |  190286   446619 |   76747   11766   566083    48.1 |  1.158 % |
c |     12064 |  190286   446619 |   84422   11991   577304    48.1 |  1.158 % |
c |     12402 |  190286   446619 |   92864   12329   581418    47.2 |  1.158 % |
c |     12908 |  190258   446556 |  102151   12834   604153    47.1 |  1.167 % |
c |     13667 |  190204   446436 |  112366   13589   636533    46.8 |  1.190 % |
c |     14806 |  190153   446322 |  123603   14720   668941    45.4 |  1.212 % |
c |     16514 |  189969   445907 |  135963   16409   754857    46.0 |  1.289 % |
c |     19076 |  189969   445907 |  149559   18971   880480    46.4 |  1.289 % |
c |     22921 |  189969   445907 |  164515   22816  1083581    47.5 |  1.289 % |
c |     28688 |  189969   445907 |  180967   28583  1429962    50.0 |  1.289 % |
c |     37340 |  189969   445907 |  199064   37235  2157656    57.9 |  1.289 % |
c |     50318 |  189969   445907 |  218970   50213  4133473    82.3 |  1.289 % |
c |     69780 |  189969   445907 |  240867   69675  7316398   105.0 |  1.289 % |
c |     98972 |  189969   445907 |  264954   98867  9521248    96.3 |  1.289 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.95 0.93 2/53 14360
Raw data (stat): 14360 (runsolver) R 14359 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481006773 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.87 0.95 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3685 0 0 0 989 9 0 0 25 0 1 0 481006773 17952768 3535 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4383 3535 603 41 0 4342 0
vsize: 17532
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.95 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3815 0 0 0 1989 9 0 0 25 0 1 0 481006773 18513920 3665 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4520 3665 603 41 0 4479 0
vsize: 18080
[startup+30.0031 s]
Raw data (loadavg): 0.90 0.95 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 3967 0 0 0 2989 10 0 0 25 0 1 0 481006773 19050496 3817 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4651 3817 603 41 0 4610 0
vsize: 18604
[startup+40.0036 s]
Raw data (loadavg): 0.92 0.95 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6419 0 0 0 3983 15 0 0 25 0 1 0 481006773 32186368 6269 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7858 6269 603 41 0 7817 0
vsize: 31432
[startup+50.0053 s]
Raw data (loadavg): 0.93 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6549 0 0 0 4982 16 0 0 25 0 1 0 481006773 32739328 6399 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7993 6399 603 41 0 7952 0
vsize: 31972
[startup+60.0064 s]
Raw data (loadavg): 0.94 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6729 0 0 0 5981 17 0 0 25 0 1 0 481006773 33431552 6579 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8162 6579 603 41 0 8121 0
vsize: 32648
[startup+70.0069 s]
Raw data (loadavg): 0.95 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6799 0 0 0 6980 18 0 0 25 0 1 0 481006773 33665024 6649 4294967295 134512640 134672761 3221224560 3221223708 1074723737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8219 6649 603 41 0 8178 0
vsize: 32876
[startup+80.0077 s]
Raw data (loadavg): 0.96 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6867 0 0 0 7980 18 0 0 25 0 1 0 481006773 33935360 6717 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8285 6717 603 41 0 8244 0
vsize: 33140
[startup+90.0084 s]
Raw data (loadavg): 0.96 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 6931 0 0 0 8980 18 0 0 25 0 1 0 481006773 34205696 6781 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8351 6781 603 41 0 8310 0
vsize: 33404
[startup+100.009 s]
Raw data (loadavg): 0.97 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7008 0 0 0 9980 18 0 0 25 0 1 0 481006773 34607104 6858 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8449 6858 603 41 0 8408 0
vsize: 33796
[startup+110.01 s]
Raw data (loadavg): 0.97 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7072 0 0 0 10980 19 0 0 25 0 1 0 481006773 34873344 6922 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8514 6922 603 41 0 8473 0
vsize: 34056
[startup+120.011 s]
Raw data (loadavg): 0.98 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7133 0 0 0 11980 19 0 0 25 0 1 0 481006773 35139584 6983 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 6983 603 41 0 8538 0
vsize: 34316
[startup+130.013 s]
Raw data (loadavg): 0.98 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7185 0 0 0 12979 19 0 0 25 0 1 0 481006773 35274752 7035 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8612 7035 603 41 0 8571 0
vsize: 34448
[startup+140.013 s]
Raw data (loadavg): 0.98 0.96 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7250 0 0 0 13979 19 0 0 25 0 1 0 481006773 35540992 7100 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8677 7100 603 41 0 8636 0
vsize: 34708
[startup+150.014 s]
Raw data (loadavg): 0.98 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7321 0 0 0 14979 20 0 0 25 0 1 0 481006773 35946496 7171 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8776 7171 603 41 0 8735 0
vsize: 35104
[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7406 0 0 0 15978 20 0 0 25 0 1 0 481006773 36208640 7256 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8840 7256 603 41 0 8799 0
vsize: 35360
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7488 0 0 0 16978 20 0 0 25 0 1 0 481006773 36605952 7338 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 7338 603 41 0 8896 0
vsize: 35748
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7564 0 0 0 17978 20 0 0 25 0 1 0 481006773 36872192 7414 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9002 7414 603 41 0 8961 0
vsize: 36008
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7676 0 0 0 18978 21 0 0 25 0 1 0 481006773 37273600 7526 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9100 7526 603 41 0 9059 0
vsize: 36400
[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7778 0 0 0 19978 21 0 0 25 0 1 0 481006773 37675008 7628 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9198 7628 603 41 0 9157 0
vsize: 36792
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7853 0 0 0 20977 22 0 0 25 0 1 0 481006773 38072320 7703 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9295 7703 603 41 0 9254 0
vsize: 37180
[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 7928 0 0 0 21977 22 0 0 25 0 1 0 481006773 38334464 7778 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 7778 603 41 0 9318 0
vsize: 37436
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8013 0 0 0 22977 22 0 0 25 0 1 0 481006773 38735872 7863 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9457 7863 603 41 0 9416 0
vsize: 37828
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8090 0 0 0 23977 22 0 0 25 0 1 0 481006773 39006208 7940 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9523 7940 603 41 0 9482 0
vsize: 38092
[startup+250.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8161 0 0 0 24977 23 0 0 25 0 1 0 481006773 39272448 8011 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9588 8011 603 41 0 9547 0
vsize: 38352
[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8237 0 0 0 25977 23 0 0 25 0 1 0 481006773 39669760 8087 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9685 8087 603 41 0 9644 0
vsize: 38740
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8300 0 0 0 26977 24 0 0 25 0 1 0 481006773 39936000 8150 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9750 8150 603 41 0 9709 0
vsize: 39000
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8375 0 0 0 27977 24 0 0 25 0 1 0 481006773 40333312 8225 4294967295 134512640 134672761 3221224560 3221223744 134559594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9847 8225 603 41 0 9806 0
vsize: 39388
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8443 0 0 0 28977 24 0 0 25 0 1 0 481006773 40603648 8293 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9913 8293 603 41 0 9872 0
vsize: 39652
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8505 0 0 0 29977 24 0 0 25 0 1 0 481006773 40869888 8355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9978 8355 603 41 0 9937 0
vsize: 39912
[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8575 0 0 0 30977 24 0 0 25 0 1 0 481006773 41132032 8425 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10042 8425 603 41 0 10001 0
vsize: 40168
[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8643 0 0 0 31976 25 0 0 25 0 1 0 481006773 41394176 8493 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10106 8493 603 41 0 10065 0
vsize: 40424
[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8711 0 0 0 32976 25 0 0 25 0 1 0 481006773 41664512 8561 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10172 8561 603 41 0 10131 0
vsize: 40688
[startup+340.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8777 0 0 0 33977 25 0 0 25 0 1 0 481006773 41934848 8627 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10238 8627 603 41 0 10197 0
vsize: 40952
[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8874 0 0 0 34977 25 0 0 25 0 1 0 481006773 42332160 8724 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10335 8724 603 41 0 10294 0
vsize: 41340
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 8979 0 0 0 35977 25 0 0 25 0 1 0 481006773 42737664 8829 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10434 8829 603 41 0 10393 0
vsize: 41736
[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9090 0 0 0 36976 26 0 0 25 0 1 0 481006773 43143168 8940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10533 8940 603 41 0 10492 0
vsize: 42132
[startup+380.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9190 0 0 0 37976 26 0 0 25 0 1 0 481006773 43540480 9040 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10630 9040 603 41 0 10589 0
vsize: 42520
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9340 0 0 0 38976 27 0 0 25 0 1 0 481006773 44212224 9190 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10794 9190 603 41 0 10753 0
vsize: 43176
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9486 0 0 0 39975 28 0 0 25 0 1 0 481006773 44740608 9336 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10923 9336 603 41 0 10882 0
vsize: 43692
[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9636 0 0 0 40975 28 0 0 25 0 1 0 481006773 45404160 9486 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11085 9486 603 41 0 11044 0
vsize: 44340
[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9758 0 0 0 41976 28 0 0 25 0 1 0 481006773 45940736 9608 4294967295 134512640 134672761 3221224560 3221223696 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11216 9609 603 41 0 11175 0
vsize: 44864
[startup+430.049 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 9895 0 0 0 42976 29 0 0 25 0 1 0 481006773 46469120 9745 4294967295 134512640 134672761 3221224560 3221223664 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11345 9745 603 41 0 11304 0
vsize: 45380
[startup+440.06 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10032 0 0 0 43976 29 0 0 25 0 1 0 481006773 47009792 9882 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11477 9882 603 41 0 11436 0
vsize: 45908
[startup+450.061 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10194 0 0 0 44976 30 0 0 25 0 1 0 481006773 47673344 10044 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11639 10044 603 41 0 11598 0
vsize: 46556
[startup+460.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10348 0 0 0 45976 30 0 0 25 0 1 0 481006773 48345088 10198 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11803 10198 603 41 0 11762 0
vsize: 47212
[startup+470.062 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10522 0 0 0 46976 31 0 0 25 0 1 0 481006773 49025024 10372 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 10372 603 41 0 11928 0
vsize: 47876
[startup+480.063 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10671 0 0 0 47975 32 0 0 25 0 1 0 481006773 49565696 10521 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12101 10521 603 41 0 12060 0
vsize: 48404
[startup+490.064 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10805 0 0 0 48974 33 0 0 25 0 1 0 481006773 50241536 10655 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12266 10655 603 41 0 12225 0
vsize: 49064
[startup+500.066 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10882 0 0 0 49975 33 0 0 25 0 1 0 481006773 50511872 10732 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12332 10732 603 41 0 12291 0
vsize: 49328
[startup+510.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 10973 0 0 0 50974 33 0 0 25 0 1 0 481006773 50913280 10823 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12430 10823 603 41 0 12389 0
vsize: 49720
[startup+520.067 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11108 0 0 0 51974 34 0 0 25 0 1 0 481006773 51445760 10958 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12560 10958 603 41 0 12519 0
vsize: 50240
[startup+530.068 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11277 0 0 0 52974 34 0 0 25 0 1 0 481006773 52109312 11127 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12722 11127 603 41 0 12681 0
vsize: 50888
[startup+540.069 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11381 0 0 0 53974 34 0 0 25 0 1 0 481006773 52514816 11231 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12821 11231 603 41 0 12780 0
vsize: 51284
[startup+550.082 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11477 0 0 0 54975 34 0 0 25 0 1 0 481006773 52916224 11327 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12919 11327 603 41 0 12878 0
vsize: 51676
[startup+560.083 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11574 0 0 0 55975 35 0 0 25 0 1 0 481006773 53317632 11424 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13017 11424 603 41 0 12976 0
vsize: 52068
[startup+570.084 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11706 0 0 0 56975 35 0 0 25 0 1 0 481006773 53846016 11556 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13146 11556 603 41 0 13105 0
vsize: 52584
[startup+580.085 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11840 0 0 0 57975 36 0 0 25 0 1 0 481006773 54378496 11690 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13276 11690 603 41 0 13235 0
vsize: 53104
[startup+590.086 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 11974 0 0 0 58975 36 0 0 25 0 1 0 481006773 54919168 11824 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13408 11824 603 41 0 13367 0
vsize: 53632
[startup+600.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12124 0 0 0 59975 36 0 0 25 0 1 0 481006773 55578624 11974 4294967295 134512640 134672761 3221224560 3221223728 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13569 11974 603 41 0 13528 0
vsize: 54276
[startup+610.087 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12275 0 0 0 60975 37 0 0 25 0 1 0 481006773 56115200 12125 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13700 12125 603 41 0 13659 0
vsize: 54800
[startup+620.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12405 0 0 0 61975 37 0 0 25 0 1 0 481006773 56651776 12255 4294967295 134512640 134672761 3221224560 3221223664 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13831 12255 603 41 0 13790 0
vsize: 55324
[startup+630.089 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12569 0 0 0 62975 37 0 0 25 0 1 0 481006773 57352192 12419 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14002 12419 603 41 0 13961 0
vsize: 56008
[startup+640.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12716 0 0 0 63974 38 0 0 25 0 1 0 481006773 58019840 12566 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14165 12566 603 41 0 14124 0
vsize: 56660
[startup+650.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12825 0 0 0 64974 39 0 0 25 0 1 0 481006773 58417152 12675 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14262 12675 603 41 0 14221 0
vsize: 57048
[startup+660.091 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 12985 0 0 0 65973 39 0 0 25 0 1 0 481006773 59084800 12835 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14425 12835 603 41 0 14384 0
vsize: 57700
[startup+670.092 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13161 0 0 0 66974 39 0 0 25 0 1 0 481006773 59760640 13011 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14590 13011 603 41 0 14549 0
vsize: 58360
[startup+680.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13324 0 0 0 67973 40 0 0 25 0 1 0 481006773 60690432 13174 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14817 13174 603 41 0 14776 0
vsize: 59268
[startup+690.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13484 0 0 0 68973 40 0 0 25 0 1 0 481006773 61362176 13334 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14981 13334 603 41 0 14940 0
vsize: 59924
[startup+700.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13639 0 0 0 69973 41 0 0 25 0 1 0 481006773 62038016 13489 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 13489 603 41 0 15105 0
vsize: 60584
[startup+710.095 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13763 0 0 0 70973 41 0 0 25 0 1 0 481006773 62562304 13613 4294967295 134512640 134672761 3221224560 3221223664 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15274 13613 603 41 0 15233 0
vsize: 61096
[startup+720.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 13921 0 0 0 71973 41 0 0 25 0 1 0 481006773 63217664 13771 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15434 13771 603 41 0 15393 0
vsize: 61736
[startup+730.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14069 0 0 0 72972 42 0 0 25 0 1 0 481006773 63758336 13919 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15566 13919 603 41 0 15525 0
vsize: 62264
[startup+740.098 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14138 0 0 0 73972 42 0 0 25 0 1 0 481006773 64028672 13988 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15632 13988 603 41 0 15591 0
vsize: 62528
[startup+750.099 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14193 0 0 0 74972 43 0 0 25 0 1 0 481006773 64294912 14043 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15697 14043 603 41 0 15656 0
vsize: 62788
[startup+760.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14243 0 0 0 75972 43 0 0 25 0 1 0 481006773 64430080 14093 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15730 14093 603 41 0 15689 0
vsize: 62920
[startup+770.1 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14294 0 0 0 76972 43 0 0 25 0 1 0 481006773 64696320 14144 4294967295 134512640 134672761 3221224560 3221223696 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15795 14144 603 41 0 15754 0
vsize: 63180
[startup+780.101 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14354 0 0 0 77972 43 0 0 25 0 1 0 481006773 64966656 14204 4294967295 134512640 134672761 3221224560 3221223744 134559159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15861 14204 603 41 0 15820 0
vsize: 63444
[startup+790.102 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14418 0 0 0 78972 43 0 0 25 0 1 0 481006773 65228800 14268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15925 14268 603 41 0 15884 0
vsize: 63700
[startup+800.103 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14461 0 0 0 79972 43 0 0 25 0 1 0 481006773 65359872 14311 4294967295 134512640 134672761 3221224560 3221223760 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15957 14311 603 41 0 15916 0
vsize: 63828
[startup+810.104 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14526 0 0 0 80972 44 0 0 25 0 1 0 481006773 65622016 14376 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16021 14376 603 41 0 15980 0
vsize: 64084
[startup+820.104 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14577 0 0 0 81972 44 0 0 25 0 1 0 481006773 65884160 14427 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16085 14427 603 41 0 16044 0
vsize: 64340
[startup+830.105 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14630 0 0 0 82972 44 0 0 25 0 1 0 481006773 66015232 14480 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16117 14480 603 41 0 16076 0
vsize: 64468
[startup+840.106 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14685 0 0 0 83972 44 0 0 25 0 1 0 481006773 66293760 14535 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16185 14535 603 41 0 16144 0
vsize: 64740
[startup+850.108 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14729 0 0 0 84972 45 0 0 25 0 1 0 481006773 66424832 14579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16217 14579 603 41 0 16176 0
vsize: 64868
[startup+860.108 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14803 0 0 0 85972 45 0 0 25 0 1 0 481006773 66826240 14653 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16315 14653 603 41 0 16274 0
vsize: 65260
[startup+870.109 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14862 0 0 0 86972 45 0 0 25 0 1 0 481006773 66957312 14712 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16347 14712 603 41 0 16306 0
vsize: 65388
[startup+880.11 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14912 0 0 0 87973 45 0 0 25 0 1 0 481006773 67227648 14762 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16413 14762 603 41 0 16372 0
vsize: 65652
[startup+890.111 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 14963 0 0 0 88973 45 0 0 25 0 1 0 481006773 67362816 14813 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16446 14813 603 41 0 16405 0
vsize: 65784
[startup+900.111 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15018 0 0 0 89973 46 0 0 25 0 1 0 481006773 67633152 14868 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16512 14868 603 41 0 16471 0
vsize: 66048
[startup+910.112 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15067 0 0 0 90972 46 0 0 25 0 1 0 481006773 67895296 14917 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16576 14917 603 41 0 16535 0
vsize: 66304
[startup+920.113 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15112 0 0 0 91972 46 0 0 25 0 1 0 481006773 68030464 14962 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16609 14962 603 41 0 16568 0
vsize: 66436
[startup+930.114 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15163 0 0 0 92973 46 0 0 25 0 1 0 481006773 68165632 15013 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16642 15013 603 41 0 16601 0
vsize: 66568
[startup+940.114 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15203 0 0 0 93973 46 0 0 25 0 1 0 481006773 68431872 15053 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16707 15053 603 41 0 16666 0
vsize: 66828
[startup+950.115 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15247 0 0 0 94973 47 0 0 25 0 1 0 481006773 68567040 15097 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 15097 603 41 0 16699 0
vsize: 66960
[startup+960.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15291 0 0 0 95973 47 0 0 25 0 1 0 481006773 68706304 15141 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16774 15141 603 41 0 16733 0
vsize: 67096
[startup+970.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15366 0 0 0 96973 47 0 0 25 0 1 0 481006773 69103616 15216 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16871 15216 603 41 0 16830 0
vsize: 67484
[startup+980.117 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15421 0 0 0 97973 47 0 0 25 0 1 0 481006773 69234688 15271 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16903 15271 603 41 0 16862 0
vsize: 67612
[startup+990.118 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15471 0 0 0 98973 47 0 0 25 0 1 0 481006773 69496832 15321 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16967 15321 603 41 0 16926 0
vsize: 67868
[startup+1000.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15526 0 0 0 99973 48 0 0 25 0 1 0 481006773 69632000 15376 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17000 15376 603 41 0 16959 0
vsize: 68000
[startup+1010.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15582 0 0 0 100973 48 0 0 25 0 1 0 481006773 69894144 15432 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17064 15432 603 41 0 17023 0
vsize: 68256
[startup+1020.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15641 0 0 0 101973 48 0 0 25 0 1 0 481006773 70164480 15491 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17130 15491 603 41 0 17089 0
vsize: 68520
[startup+1030.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15705 0 0 0 102974 48 0 0 25 0 1 0 481006773 70430720 15555 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17195 15555 603 41 0 17154 0
vsize: 68780
[startup+1040.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15769 0 0 0 103974 48 0 0 25 0 1 0 481006773 70701056 15619 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17261 15619 603 41 0 17220 0
vsize: 69044
[startup+1050.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15840 0 0 0 104974 48 0 0 25 0 1 0 481006773 70967296 15690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17326 15690 603 41 0 17285 0
vsize: 69304
[startup+1060.12 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15922 0 0 0 105974 49 0 0 25 0 1 0 481006773 71364608 15772 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17423 15772 603 41 0 17382 0
vsize: 69692
[startup+1070.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 15981 0 0 0 106974 49 0 0 25 0 1 0 481006773 71495680 15831 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17455 15831 603 41 0 17414 0
vsize: 69820
[startup+1080.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16038 0 0 0 107974 49 0 0 25 0 1 0 481006773 71761920 15888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17520 15888 603 41 0 17479 0
vsize: 70080
[startup+1090.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16100 0 0 0 108974 49 0 0 25 0 1 0 481006773 72032256 15950 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17586 15950 603 41 0 17545 0
vsize: 70344
[startup+1100.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16163 0 0 0 109974 49 0 0 25 0 1 0 481006773 72298496 16013 4294967295 134512640 134672761 3221224560 3221223760 134557820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17651 16013 603 41 0 17610 0
vsize: 70604
[startup+1110.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16221 0 0 0 110974 49 0 0 25 0 1 0 481006773 72564736 16071 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17716 16071 603 41 0 17675 0
vsize: 70864
[startup+1120.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16281 0 0 0 111974 50 0 0 25 0 1 0 481006773 72826880 16131 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17780 16131 603 41 0 17739 0
vsize: 71120
[startup+1130.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16336 0 0 0 112974 50 0 0 25 0 1 0 481006773 72962048 16186 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17813 16186 603 41 0 17772 0
vsize: 71252
[startup+1140.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16393 0 0 0 113974 50 0 0 25 0 1 0 481006773 73224192 16243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17877 16243 603 41 0 17836 0
vsize: 71508
[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16450 0 0 0 114974 51 0 0 25 0 1 0 481006773 73490432 16300 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17942 16300 603 41 0 17901 0
vsize: 71768
[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16502 0 0 0 115974 51 0 0 25 0 1 0 481006773 73621504 16352 4294967295 134512640 134672761 3221224560 3221223696 134560637 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17974 16352 603 41 0 17933 0
vsize: 71896
[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16558 0 0 0 116974 51 0 0 25 0 1 0 481006773 73887744 16408 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18039 16408 603 41 0 17998 0
vsize: 72156
[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16620 0 0 0 117974 51 0 0 25 0 1 0 481006773 74182656 16470 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18111 16470 603 41 0 18070 0
vsize: 72444
[startup+1190.14 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16672 0 0 0 118974 51 0 0 25 0 1 0 481006773 74317824 16522 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18144 16522 603 41 0 18103 0
vsize: 72576
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.93 2/53 14360
Raw data (stat): 14360 (minisat+) R 14359 7987 7986 0 -1 0 16722 0 0 0 119974 52 0 0 25 0 1 0 481006773 74579968 16572 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18208 16572 603 41 0 18167 0
vsize: 72832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 14360
Raw data (stat): 14360 (minisat+) Z 14359 7987 7986 0 -1 12 16725 0 0 0 119974 55 0 0 25 0 1 0 481006773 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.18
CPU time (s): 1200.3
CPU user time (s): 1199.74
CPU system time (s): 0.554915
CPU usage (%): 100.01
Max. virtual memory (Kb): 72832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####