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/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 32443

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-05-27 09:59:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23835 boxname=wulflinc9 idbench=1479 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 23835
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        902712 kB
Buffers:         13036 kB
Cached:          99708 kB
SwapCached:        612 kB
Active:          18120 kB
Inactive:        96688 kB
HighTotal:      131008 kB
HighFree:        44156 kB
LowTotal:       903652 kB
LowFree:        858556 kB
SwapTotal:     2097136 kB
SwapFree:      2095636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5120 kB
Slab:            11644 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:19:32 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23835 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> BDD-cost:  817
c ---[ 136]---> BDD-cost: 1034
c ---[ 134]---> BDD-cost: 1141
c ---[ 132]---> BDD-cost: 1061
c ---[ 130]---> BDD-cost: 1053
c ---[ 128]---> BDD-cost:  607
c ---[ 126]---> BDD-cost: 1110
c ---[ 124]---> BDD-cost:  977
c ---[ 122]---> BDD-cost: 1061
c ---[ 120]---> BDD-cost: 1143
c ---[ 118]---> BDD-cost:  748
c ---[ 116]---> BDD-cost: 1143
c ---[ 114]---> BDD-cost:  748
c ---[ 112]---> BDD-cost: 1169
c ---[ 110]---> BDD-cost:  954
c ---[ 108]---> BDD-cost:  888
c ---[ 106]---> BDD-cost: 1062
c ---[ 104]---> BDD-cost: 1086
c ---[ 102]---> BDD-cost: 1197
c ---[ 100]---> BDD-cost:  748
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   57457   165221 |   19152       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 12461981[0m
c ---[   0]---> Sorter-cost:143862     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        29 |  465966  1118983 |  155322      29      528    18.2 |  0.000 % |
c |       129 |  465966  1118983 |  170854     129    18497   143.4 |  0.712 % |
c |       279 |  465880  1118789 |  187939     278    20652    74.3 |  0.725 % |
c |       504 |  465778  1118557 |  206733     502    21705    43.2 |  0.744 % |
c |       843 |  465119  1117061 |  227406     820    23464    28.6 |  0.859 % |
c |      1349 |  465119  1117061 |  250147    1326    74627    56.3 |  0.859 % |
c ==============================================================================
c [1mFound solution: 6603958[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1678 |  466587  1121636 |  155529    1655    81661    49.3 |  0.859 % |
c |      1778 |  465774  1119783 |  171081    1743    82414    47.3 |  0.997 % |
c |      1928 |  465774  1119783 |  188190    1893    83321    44.0 |  0.997 % |
c |      2155 |  465526  1119220 |  207009    2111    85063    40.3 |  1.042 % |
c |      2492 |  464364  1116567 |  227710    2417    86942    36.0 |  1.255 % |
c |      3000 |  464364  1116567 |  250481    2925    89895    30.7 |  1.255 % |
c |      3759 |  464356  1116549 |  275529    3683    96343    26.2 |  1.256 % |
c |      4898 |  464356  1116549 |  303082    4822   108010    22.4 |  1.256 % |
c |      6606 |  464356  1116549 |  333390    6530   126203    19.3 |  1.256 % |
c |      9168 |  464356  1116549 |  366729    9092   443910    48.8 |  1.256 % |
c |     13012 |  463965  1115651 |  403402   12927   983621    76.1 |  1.329 % |
c ==============================================================================
c [1mFound solution: 4926880[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15049 |  464439  1116883 |  154813   14809  1140868    77.0 |  1.329 % |
c |     15149 |  464439  1116883 |  170294   14909  1142400    76.6 |  1.363 % |
c |     15299 |  464439  1116883 |  187323   15059  1143754    76.0 |  1.363 % |
c |     15524 |  464439  1116883 |  206056   15284  1145206    74.9 |  1.363 % |
c |     15863 |  464439  1116883 |  226661   15623  1148990    73.5 |  1.363 % |
c |     16369 |  464439  1116883 |  249327   16129  1153401    71.5 |  1.363 % |
c |     17128 |  464439  1116883 |  274260   16888  1162575    68.8 |  1.363 % |
c |     18268 |  464439  1116883 |  301686   18028  1199418    66.5 |  1.363 % |
c |     19976 |  464439  1116883 |  331855   19736  1220790    61.9 |  1.363 % |
c |     22538 |  464439  1116883 |  365040   22298  1457358    65.4 |  1.363 % |
c |     26384 |  464395  1116783 |  401545   26143  1528959    58.5 |  1.370 % |
c ==============================================================================
c [1mFound solution: 4772380[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31232 |  465109  1118631 |  155036   30991  2818819    91.0 |  1.370 % |
c |     31332 |  464838  1118011 |  170539   31082  2822575    90.8 |  1.421 % |
c |     31482 |  464838  1118011 |  187593   31232  2824137    90.4 |  1.421 % |
c |     31707 |  464006  1116105 |  206352   31419  2825963    89.9 |  1.577 % |
c |     32044 |  464006  1116105 |  226988   31756  2865528    90.2 |  1.577 % |
c |     32553 |  464006  1116105 |  249687   32265  2898261    89.8 |  1.577 % |
c |     33313 |  464006  1116105 |  274655   33025  2928269    88.7 |  1.577 % |
c |     34452 |  464006  1116105 |  302121   34164  3033784    88.8 |  1.577 % |
c |     36160 |  463090  1113997 |  332333   35822  3112841    86.9 |  1.750 % |
c |     38722 |  463063  1113938 |  365566   38383  3358856    87.5 |  1.755 % |
c |     42566 |  463063  1113938 |  402123   42227  3634636    86.1 |  1.755 % |
c |     48333 |  462393  1112401 |  442335   47979  3871000    80.7 |  1.882 % |
c ==============================================================================
c [1mFound solution: 4529410[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50046 |  462562  1112967 |  154187   49687  3924581    79.0 |  1.882 % |
c |     50146 |  462562  1112967 |  169605   49787  3925225    78.8 |  1.891 % |
c |     50297 |  462562  1112967 |  186566   49938  3926837    78.6 |  1.891 % |
c |     50524 |  462562  1112967 |  205222   50165  3928189    78.3 |  1.891 % |
c |     50861 |  462562  1112967 |  225745   50502  3937036    78.0 |  1.891 % |
c |     51367 |  462558  1112958 |  248319   51007  3968200    77.8 |  1.892 % |
c |     52127 |  462408  1112616 |  273151   51766  4023243    77.7 |  1.919 % |
c |     53266 |  462296  1112360 |  300466   52903  4109630    77.7 |  1.939 % |
c |     54977 |  461899  1111444 |  330513   54578  4847745    88.8 |  2.017 % |
c |     57539 |  461656  1110882 |  363564   57133  5088634    89.1 |  2.064 % |
c ==============================================================================
c [1mFound solution: 4515501[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61231 |  461517  1110594 |  153839   60819  5477880    90.1 |  2.064 % |
c |     61331 |  461517  1110594 |  169222   60919  5484008    90.0 |  2.093 % |
c |     61482 |  461517  1110594 |  186145   61070  5493732    90.0 |  2.093 % |
c |     61707 |  461517  1110594 |  204759   61295  5519604    90.0 |  2.093 % |
c |     62044 |  461517  1110594 |  225235   61632  5533687    89.8 |  2.093 % |
c |     62550 |  460644  1108586 |  247759   62072  5537675    89.2 |  2.259 % |
c |     63311 |  460644  1108586 |  272535   62833  5547566    88.3 |  2.259 % |
c |     64453 |  460644  1108586 |  299788   63975  5559773    86.9 |  2.259 % |
c |     66161 |  460614  1108518 |  329767   65682  5603143    85.3 |  2.264 % |
c |     68723 |  460614  1108518 |  362744   68244  5989138    87.8 |  2.264 % |
c |     72567 |  460590  1108464 |  399018   72087  6797213    94.3 |  2.268 % |
c |     78333 |  460590  1108464 |  438920   77853  7534987    96.8 |  2.268 % |
c |     86984 |  460590  1108464 |  482812   86504  8760906   101.3 |  2.268 % |
c ==============================================================================
c [1mFound solution: 3847060[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97334 |  460210  1107633 |  153403   96841 11722134   121.0 |  2.268 % |
c |     97434 |  460210  1107633 |  168743   96941 11724996   120.9 |  2.351 % |
c |     97584 |  460210  1107633 |  185617   97091 11727871   120.8 |  2.351 % |
c |     97809 |  460034  1107233 |  204179   97311 11732839   120.6 |  2.382 % |
c |     98146 |  460034  1107233 |  224597   97648 11817981   121.0 |  2.382 % |
c |     98652 |  460034  1107233 |  247057   98154 11830636   120.5 |  2.382 % |
c |     99411 |  460034  1107233 |  271762   98913 11838684   119.7 |  2.382 % |
c ==============================================================================
c [1mFound solution: 3843251[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 3 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99663 |  460054  1107278 |  153351   99165 11859813   119.6 |  2.382 % |
c |     99763 |  460054  1107278 |  168686   99265 11862626   119.5 |  2.382 % |
c |     99914 |  460054  1107278 |  185554   99416 11865724   119.4 |  2.382 % |
c |    100140 |  460054  1107278 |  204110   99642 11896849   119.4 |  2.382 % |
c |    100481 |  460054  1107278 |  224521   99983 11902836   119.0 |  2.382 % |
c |    100988 |  459870  1106854 |  246973  100481 11908214   118.5 |  2.417 % |
c |    101747 |  459852  1106813 |  271670  101239 11966293   118.2 |  2.420 % |
c |    102887 |  458697  1104161 |  298837  102297 12107846   118.4 |  2.636 % |
c |    104596 |  458670  1104100 |  328721  104005 12153140   116.9 |  2.641 % |
c |    107159 |  458670  1104100 |  361593  106568 12319800   115.6 |  2.641 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  1644 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.00 0.97 0.91 2/54 1640
Raw data (stat): 1640 (runsolver) R 1639 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 797043848 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+10.0001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0005 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 1644
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0029 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0026 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.0024 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.002 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 1704
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.005 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1706
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 3/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.04 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.78 s]
Raw data (loadavg): 1.06 1.00 0.92 1/53 1708
Raw data (stat): 1640 (minisat+_script) S 1639 3944 3943 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 797043848 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.78
CPU time (s): 1229.88
CPU user time (s): 1228.96
CPU system time (s): 0.922859
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####