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.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.5:100.opb
MD5SUM	feaa96df552ef9989407735877840272
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	13
Optimality of the best value was proved	NO
Number of terms in the objective function	776
Biggest coefficient in the objective function	474
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	2127
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	474
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	2127
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04084
Number of variables	776
Total number of constraints	1642
Number of constraints which are clauses	701
Number of constraints which are cardinality constraints (but not clauses)	941
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	20
Trace number 31745

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-27 05:58:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23123 boxname=wulflinc15 idbench=369 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  feaa96df552ef9989407735877840272  /oldhome/oroussel/tmp/wulflinc15/normalized-10:20:4.5:0.5:100.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-10:20:4.5:0.5:100.opb
IDLAUNCH: 23123
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        875944 kB
Buffers:         34792 kB
Cached:         102300 kB
SwapCached:        608 kB
Active:          51064 kB
Inactive:        88104 kB
HighTotal:      131008 kB
HighFree:        43092 kB
LowTotal:       903652 kB
LowFree:        832852 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            13952 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 06:18:59 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23123 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 866 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   20
c ---[ 169]---> BDD-cost:   20
c ---[ 168]---> BDD-cost:   23
c ---[ 167]---> BDD-cost:   23
c ---[ 166]---> BDD-cost:   29
c ---[ 165]---> BDD-cost:   29
c ---[ 164]---> BDD-cost:   32
c ---[ 163]---> BDD-cost:   38
c ---[ 162]---> BDD-cost:   44
c ---[ 161]---> BDD-cost:   44
c ---[ 160]---> BDD-cost:   50
c ---[ 159]---> BDD-cost:   44
c ---[ 158]---> BDD-cost:   47
c ---[ 157]---> BDD-cost:   44
c ---[ 156]---> BDD-cost:   41
c ---[ 155]---> BDD-cost:   29
c ---[ 154]---> BDD-cost:   20
c ---[ 153]---> BDD-cost:   11
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   20
c ---[ 149]---> BDD-cost:   20
c ---[ 148]---> BDD-cost:   26
c ---[ 147]---> BDD-cost:   29
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   29
c ---[ 144]---> BDD-cost:   32
c ---[ 143]---> BDD-cost:   41
c ---[ 142]---> BDD-cost:   47
c ---[ 141]---> BDD-cost:   47
c ---[ 140]---> BDD-cost:   50
c ---[ 139]---> BDD-cost:   50
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   47
c ---[ 136]---> BDD-cost:   41
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   11
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   23
c ---[ 129]---> BDD-cost:   23
c ---[ 128]---> BDD-cost:   26
c ---[ 127]---> BDD-cost:   29
c ---[ 126]---> BDD-cost:   35
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   35
c ---[ 123]---> BDD-cost:   41
c ---[ 122]---> BDD-cost:   45
c ---[ 121]---> BDD-cost:   47
c ---[ 120]---> BDD-cost:   50
c ---[ 119]---> BDD-cost:   53
c ---[ 118]---> BDD-cost:   53
c ---[ 117]---> BDD-cost:   47
c ---[ 116]---> BDD-cost:   41
c ---[ 115]---> BDD-cost:   35
c ---[ 114]---> BDD-cost:   21
c ---[ 113]---> BDD-cost:   14
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   20
c ---[ 110]---> BDD-cost:   23
c ---[ 109]---> BDD-cost:   23
c ---[ 108]---> BDD-cost:   20
c ---[ 107]---> BDD-cost:   26
c ---[ 106]---> BDD-cost:   23
c ---[ 105]---> BDD-cost:   29
c ---[ 104]---> BDD-cost:   29
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:   41
c ---[ 101]---> BDD-cost:   47
c ---[ 100]---> BDD-cost:   45
c ---[  99]---> BDD-cost:   53
c ---[  98]---> BDD-cost:   44
c ---[  97]---> BDD-cost:   47
c ---[  96]---> BDD-cost:   41
c ---[  95]---> BDD-cost:   35
c ---[  94]---> BDD-cost:   26
c ---[  93]---> BDD-cost:   17
c ---[  92]---> BDD-cost:    5
c ---[  91]---> BDD-cost:   20
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   20
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   20
c ---[  84]---> BDD-cost:   17
c ---[  83]---> BDD-cost:   32
c ---[  82]---> BDD-cost:   29
c ---[  81]---> BDD-cost:   38
c ---[  80]---> BDD-cost:   29
c ---[  79]---> BDD-cost:   44
c ---[  78]---> BDD-cost:   38
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:   32
c ---[  75]---> BDD-cost:   23
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   20
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    5
c ---[  65]---> BDD-cost:    5
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   20
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   32
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   29
c ---[  57]---> BDD-cost:   23
c ---[  56]---> BDD-cost:   26
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:    7
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   11
c ---[  48]---> BDD-cost:    8
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    8
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    7
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:    7
c ---[  38]---> BDD-cost:   14
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:   11
c ---[  33]---> BDD-cost:   11
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    7
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    8
c ---[  27]---> BDD-cost:   11
c ---[  25]---> BDD-cost:    7
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    8
c ---[  20]---> BDD-cost:   11
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:    8
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    8
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    0
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    9120    26089 |    3040       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 762[0m
c ---[   0]---> Sorter-cost:55537     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78358   188367 |   26119       0        0     nan |  0.000 % |
c |       101 |   78117   187877 |   28730      93     1716    18.5 |  0.575 % |
c ==============================================================================
c [1mFound solution: 59[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       152 |  107305   256100 |   35768     143     2524    17.7 |  0.575 % |
c |       252 |  107197   255852 |   39344     242     3434    14.2 |  0.685 % |
c |       403 |  107146   255749 |   43279     391     5026    12.9 |  0.734 % |
c |       628 |  106679   254725 |   47607     591    15618    26.4 |  1.106 % |
c |       965 |  106679   254725 |   52367     928    19299    20.8 |  1.106 % |
c |      1473 |  106284   253852 |   57604    1423    32871    23.1 |  1.513 % |
c |      2232 |  106079   253390 |   63365    2178    71254    32.7 |  1.661 % |
c |      3371 |  105849   252864 |   69701    3305    82651    25.0 |  1.822 % |
c |      5079 |  105536   252160 |   76671    5001   102675    20.5 |  2.042 % |
c |      7642 |  104895   250715 |   84339    7523   149395    19.9 |  2.539 % |
c |     11487 |  104887   250697 |   92772   11366   263825    23.2 |  2.543 % |
c |     17253 |  104215   249156 |  102050   17080   375171    22.0 |  3.071 % |
c |     25902 |  103982   248623 |  112255   25693   678106    26.4 |  3.266 % |
c |     38878 |  103935   248522 |  123480   38658  1202967    31.1 |  3.317 % |
c |     58340 |  103533   247609 |  135828   58088  5020404    86.4 |  3.663 % |
c ==============================================================================
c [1mFound solution: 54[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     79313 |  103589   247774 |   34529   79061  8055656   101.9 |  3.663 % |
c |     79414 |  103589   247774 |   37981   18273  2365870   129.5 |  3.662 % |
c |     79565 |  103589   247774 |   41780   18424  2369792   128.6 |  3.662 % |
c |     79790 |  103589   247774 |   45958   18649  2371476   127.2 |  3.662 % |
c |     80127 |  103581   247756 |   50553   18979  2374128   125.1 |  3.666 % |
c |     80633 |  103581   247756 |   55609   19485  2385425   122.4 |  3.666 % |
c |     81392 |  103581   247756 |   61170   20244  2396965   118.4 |  3.666 % |
c |     82533 |  103581   247756 |   67287   21385  2443100   114.2 |  3.666 % |
c |     84241 |  103581   247756 |   74015   23093  2486928   107.7 |  3.666 % |
c |     86803 |  103569   247728 |   81417   25653  2555338    99.6 |  3.673 % |
c |     90647 |  103509   247594 |   89559   29474  2657142    90.2 |  3.744 % |
c |     96413 |  103433   247424 |   98515   35233  2893777    82.1 |  3.833 % |
c |    105064 |  103433   247424 |  108366   43884  3859552    87.9 |  3.833 % |
c ==============================================================================
c [1mFound solution: 51[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115370 |  103369   247283 |   34456   54184  5009811    92.5 |  3.833 % |
c |    115472 |  103369   247283 |   37901   19025  1552846    81.6 |  3.880 % |
c |    115626 |  103369   247283 |   41691   19179  1555460    81.1 |  3.880 % |
c |    115851 |  103369   247283 |   45860   19404  1558001    80.3 |  3.880 % |
c |    116188 |  103339   247217 |   50447   19553  1559070    79.7 |  3.914 % |
c |    116694 |  103339   247217 |   55491   20059  1567634    78.2 |  3.914 % |
c |    117454 |  103339   247217 |   61040   20819  1584364    76.1 |  3.914 % |
c |    118593 |  103339   247217 |   67144   21958  1607737    73.2 |  3.914 % |
c |    120301 |  103339   247217 |   73859   23666  1690288    71.4 |  3.914 % |
c |    122864 |  103268   247064 |   81245   26224  1762345    67.2 |  3.992 % |
c |    126708 |  103235   246993 |   89369   30066  1885060    62.7 |  4.028 % |
c ==============================================================================
c [1mFound solution: 46[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    130268 |  103265   247098 |   34421   33620  2093071    62.3 |  4.028 % |
c |    130369 |  103265   247098 |   37863   33721  2094104    62.1 |  4.042 % |
c |    130519 |  103265   247098 |   41649   33871  2098978    62.0 |  4.042 % |
c |    130744 |  103265   247098 |   45814   34096  2101462    61.6 |  4.042 % |
c |    131081 |  103265   247098 |   50395   34433  2108066    61.2 |  4.042 % |
c |    131587 |  103265   247098 |   55435   34939  2120201    60.7 |  4.042 % |
c |    132347 |  103265   247098 |   60978   35699  2132256    59.7 |  4.042 % |
c |    133486 |  103257   247080 |   67076   36831  2171985    59.0 |  4.046 % |
c |    135194 |  103247   247058 |   73784   38534  2230934    57.9 |  4.057 % |
c |    137756 |  103245   247054 |   81162   41093  2339305    56.9 |  4.059 % |
c |    141600 |  103245   247054 |   89279   44937  2493251    55.5 |  4.059 % |
c |    147366 |  103201   246956 |   98207   50695  2727322    53.8 |  4.093 % |
c |    156015 |  103127   246792 |  108027   59328  3406223    57.4 |  4.178 % |
c |    168989 |  103127   246792 |  118830   72302  6008985    83.1 |  4.178 % |
c ==============================================================================
c [1mFound solution: 36[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184940 |  102664   245770 |   34221   88175  7010762    79.5 |  4.178 % |
c |    185040 |  102635   245705 |   37643   23523   930122    39.5 |  4.622 % |
c |    185190 |  102635   245705 |   41407   23673   931813    39.4 |  4.622 % |
c |    185415 |  102635   245705 |   45548   23898   936406    39.2 |  4.622 % |
c |    185753 |  102635   245705 |   50102   24236   943152    38.9 |  4.622 % |
c |    186261 |  102635   245705 |   55113   24744   959954    38.8 |  4.622 % |
c |    187020 |  102597   245618 |   60624   25500   972573    38.1 |  4.647 % |
c |    188160 |  102597   245618 |   66687   26640  1011974    38.0 |  4.647 % |
c |    189868 |  102597   245618 |   73355   28348  1073849    37.9 |  4.647 % |
c |    192430 |  102597   245618 |   80691   30910  1196120    38.7 |  4.647 % |
c |    196274 |  102591   245606 |   88760   34752  1333916    38.4 |  4.653 % |
c |    202040 |  102591   245606 |   97636   40518  1586792    39.2 |  4.653 % |
c |    210691 |  102591   245606 |  107400   49169  1800019    36.6 |  4.653 % |
c |    223667 |  102591   245606 |  118140   62145  2837805    45.7 |  4.653 % |
c |    243128 |  102591   245606 |  129954   81606  5607252    68.7 |  4.653 % |
c ==============================================================================
c [1mFound solution: 27[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    252867 |  102647   245768 |   34215   91345  6466967    70.8 |  4.653 % |
c |    252969 |  102647   245768 |   37636   24176  1473265    60.9 |  4.651 % |
c |    253119 |  102647   245768 |   41400   24326  1476562    60.7 |  4.651 % |
c |    253345 |  102647   245768 |   45540   24552  1483153    60.4 |  4.651 % |
c |    253682 |  102647   245768 |   50094   24889  1496566    60.1 |  4.651 % |
c |    254188 |  102647   245768 |   55103   25395  1536884    60.5 |  4.651 % |
c |    254947 |  102647   245768 |   60613   26154  1554276    59.4 |  4.651 % |
c |    256087 |  102647   245768 |   66675   27294  1588653    58.2 |  4.651 % |
c |    257796 |  102647   245768 |   73342   29003  1630466    56.2 |  4.651 % |
c |    260358 |  102525   245486 |   80677   31558  1753312    55.6 |  4.780 % |
c |    264203 |  102446   245313 |   88744   35398  1915675    54.1 |  4.869 % |
c |    269969 |  102446   245313 |   97619   41164  2915278    70.8 |  4.869 % |
c |    278620 |  102446   245313 |  107381   49815  5075380   101.9 |  4.869 % |
c |    291594 |  102446   245313 |  118119   62789  6711273   106.9 |  4.869 % |
c |    311057 |  102446   245313 |  129931   82252  8879602   108.0 |  4.869 % |
c ==============================================================================
c [1mFound solution: 26[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    325078 |  102364   245152 |   34121   96259 11264784   117.0 |  4.869 % |
c |    325178 |  102364   245152 |   37533   23136  2286606    98.8 |  4.968 % |
c |    325328 |  102364   245152 |   41286   23286  2288054    98.3 |  4.968 % |
c |    325553 |  102364   245152 |   45415   23511  2298866    97.8 |  4.968 % |
c |    325891 |  102364   245152 |   49956   23849  2302986    96.6 |  4.968 % |
c |    326398 |  102364   245152 |   54952   24356  2323339    95.4 |  4.968 % |
c |    327157 |  102364   245152 |   60447   25115  2343960    93.3 |  4.968 % |
c |    328297 |  102364   245152 |   66492   26255  2376548    90.5 |  4.968 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 19219 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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): 1.14 1.00 0.92 2/54 19215
Raw data (stat): 19215 (runsolver) R 19214 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795595205 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99949 s]
Raw data (loadavg): 1.11 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0006 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.001 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0021 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0029 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0024 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0035 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0043 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0047 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 19219
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.134 s]
Raw data (loadavg): 1.10 1.02 0.93 3/58 19264
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.134 s]
Raw data (loadavg): 1.16 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.135 s]
Raw data (loadavg): 1.13 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.135 s]
Raw data (loadavg): 1.11 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.136 s]
Raw data (loadavg): 1.10 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.137 s]
Raw data (loadavg): 1.08 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.136 s]
Raw data (loadavg): 1.07 1.03 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.136 s]
Raw data (loadavg): 1.06 1.02 0.93 2/55 19276
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.136 s]
Raw data (loadavg): 1.05 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.136 s]
Raw data (loadavg): 1.04 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.136 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.136 s]
Raw data (loadavg): 1.03 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.137 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.137 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.137 s]
Raw data (loadavg): 1.02 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.138 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.138 s]
Raw data (loadavg): 1.01 1.02 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.138 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.137 s]
Raw data (loadavg): 1.01 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.138 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.138 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.137 s]
Raw data (loadavg): 1.00 1.01 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19278
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.139 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.138 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.137 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.138 s]
Raw data (loadavg): 1.08 1.02 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.137 s]
Raw data (loadavg): 1.07 1.02 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.137 s]
Raw data (loadavg): 1.06 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.137 s]
Raw data (loadavg): 1.05 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.137 s]
Raw data (loadavg): 1.04 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.138 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.137 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.137 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.138 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.138 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.14 s]
Raw data (loadavg): 1.01 1.01 0.94 3/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.14 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.14 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.14 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 19280
Raw data (stat): 19215 (minisat+_script) S 19214 23514 23513 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795595205 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.86
CPU user time (s): 1229.31
CPU system time (s): 0.558915
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####