PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	808
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	808
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03884
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 30299

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-25 16:05:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21643 boxname=wulflinc12 idbench=61 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc12/normalized-alu4.b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-alu4.b.opb
IDLAUNCH: 21643
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        347744 kB
Buffers:         34640 kB
Cached:         630720 kB
SwapCached:        564 kB
Active:          54876 kB
Inactive:       612856 kB
HighTotal:      131008 kB
HighFree:         2380 kB
LowTotal:       903652 kB
LowFree:        345364 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13564 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 16:26:01 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 21643 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1694    35961 |     564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68[0m
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   42441   131004 |   14147       0        0     nan |  0.000 % |
c |       103 |   42315   130746 |   15561      97     5670    58.5 |  0.508 % |
c |       254 |   42257   130625 |   17117     246     9210    37.4 |  0.616 % |
c |       482 |   42257   130625 |   18829     474    16778    35.4 |  0.616 % |
c |       820 |   42255   130621 |   20712     810    34182    42.2 |  0.620 % |
c ==============================================================================
c [1mFound solution: 63[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1123 |   42283   130700 |   14094    1110    51005    46.0 |  0.620 % |
c |      1224 |   42283   130700 |   15503    1211    56791    46.9 |  0.656 % |
c ==============================================================================
c [1mFound solution: 58[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1350 |   42293   130731 |   14097    1334    61072    45.8 |  0.656 % |
c |      1450 |   42293   130731 |   15506    1434    64885    45.2 |  0.735 % |
c |      1600 |   42293   130731 |   17057    1584    72364    45.7 |  0.735 % |
c |      1825 |   42293   130731 |   18763    1809    90475    50.0 |  0.735 % |
c |      2165 |   42293   130731 |   20639    2149   100442    46.7 |  0.735 % |
c ==============================================================================
c [1mFound solution: 55[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2333 |   42323   130808 |   14107    2317   105896    45.7 |  0.735 % |
c |      2434 |   42323   130808 |   15517    2418   107674    44.5 |  0.741 % |
c |      2586 |   42323   130808 |   17069    2570   113643    44.2 |  0.741 % |
c |      2812 |   42323   130808 |   18776    2796   122642    43.9 |  0.741 % |
c |      3149 |   42323   130808 |   20654    3133   148371    47.4 |  0.741 % |
c |      3655 |   42323   130808 |   22719    3639   188290    51.7 |  0.741 % |
c |      4416 |   42323   130808 |   24991    4400   229246    52.1 |  0.741 % |
c |      5555 |   42323   130808 |   27490    5539   356505    64.4 |  0.741 % |
c |      7263 |   42323   130808 |   30239    7247   491744    67.9 |  0.741 % |
c |      9825 |   42323   130808 |   33263    9809   797859    81.3 |  0.741 % |
c |     13669 |   42323   130808 |   36589   13653  1440093   105.5 |  0.741 % |
c ==============================================================================
c [1mFound solution: 54[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19430 |   42302   130754 |   14100   19343  2037073   105.3 |  0.741 % |
c |     19531 |   42302   130754 |   15510    9773  1091785   111.7 |  0.814 % |
c |     19682 |   42302   130754 |   17061    9924  1098840   110.7 |  0.814 % |
c |     19907 |   42302   130754 |   18767   10149  1110962   109.5 |  0.814 % |
c |     20244 |   42302   130754 |   20643   10486  1137911   108.5 |  0.814 % |
c |     20750 |   42302   130754 |   22708   10992  1183261   107.6 |  0.814 % |
c |     21509 |   42302   130754 |   24979   11751  1271618   108.2 |  0.814 % |
c |     22648 |   42302   130754 |   27476   12890  1364515   105.9 |  0.814 % |
c |     24356 |   42302   130754 |   30224   14598  1522658   104.3 |  0.814 % |
c |     26918 |   42302   130754 |   33247   17160  1804901   105.2 |  0.814 % |
c |     30765 |   42302   130754 |   36571   21007  2183394   103.9 |  0.814 % |
c |     36531 |   42302   130754 |   40228   26773  2754170   102.9 |  0.814 % |
c ==============================================================================
c [1mFound solution: 53[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41162 |   42320   130803 |   14106   31404  3162248   100.7 |  0.814 % |
c |     41263 |   42320   130803 |   15516   12929  1110801    85.9 |  0.817 % |
c |     41416 |   42320   130803 |   17068   13082  1118557    85.5 |  0.817 % |
c |     41642 |   42320   130803 |   18775   13308  1129179    84.8 |  0.817 % |
c |     41979 |   42320   130803 |   20652   13645  1149623    84.3 |  0.817 % |
c |     42486 |   42320   130803 |   22717   14152  1173763    82.9 |  0.817 % |
c |     43245 |   42320   130803 |   24989   14911  1221475    81.9 |  0.817 % |
c |     44384 |   42320   130803 |   27488   16050  1286940    80.2 |  0.817 % |
c |     46093 |   42320   130803 |   30237   17759  1430670    80.6 |  0.817 % |
c |     48656 |   42320   130803 |   33261   20322  1598315    78.6 |  0.817 % |
c |     52500 |   42320   130803 |   36587   24166  1930446    79.9 |  0.817 % |
c |     58268 |   42320   130803 |   40246   29934  2285715    76.4 |  0.817 % |
c |     66922 |   42320   130803 |   44270   38588  3113757    80.7 |  0.817 % |
c |     79899 |   42320   130803 |   48697   16361  2362967   144.4 |  0.817 % |
c |     99360 |   42320   130803 |   53567   35822  5244635   146.4 |  0.817 % |
c |    128552 |   42320   130803 |   58924   23711  3095697   130.6 |  0.817 % |
c |    172341 |   42320   130803 |   64816   19113  1980374   103.6 |  0.817 % |
c |    238028 |   42320   130803 |   71298   32956  2841949    86.2 |  0.817 % |
c ==============================================================================
c [1mFound solution: 52[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    256317 |   42113   130312 |   14037   43501  3635709    83.6 |  0.817 % |
c |    256418 |   42113   130312 |   15440   14391  1134454    78.8 |  1.341 % |
c |    256570 |   42113   130312 |   16984   14543  1144573    78.7 |  1.341 % |
c |    256795 |   42113   130312 |   18683   14768  1155199    78.2 |  1.341 % |
c |    257132 |   42113   130312 |   20551   15105  1168575    77.4 |  1.341 % |
c |    257638 |   42113   130312 |   22606   15611  1202306    77.0 |  1.341 % |
c |    258397 |   42113   130312 |   24867   16370  1247447    76.2 |  1.341 % |
c |    259538 |   42113   130312 |   27354   17511  1340342    76.5 |  1.341 % |
c |    261246 |   42113   130312 |   30089   19219  1556816    81.0 |  1.341 % |
c |    263809 |   42113   130312 |   33098   21782  1674246    76.9 |  1.341 % |
c |    267654 |   42113   130312 |   36408   25627  2061057    80.4 |  1.341 % |
c |    273420 |   42113   130312 |   40049   31393  2429661    77.4 |  1.341 % |
c |    282070 |   42113   130312 |   44054   40043  3047738    76.1 |  1.341 % |
c |    295044 |   42113   130312 |   48459   20186  1894183    93.8 |  1.341 % |
c |    314506 |   42113   130312 |   53305   39648  4523628   114.1 |  1.341 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14078 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): 0.79 0.94 0.98 2/54 14074
Raw data (stat): 14074 (runsolver) R 14073 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 781954996 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.0004 s]
Raw data (loadavg): 0.82 0.94 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0002 s]
Raw data (loadavg): 0.85 0.94 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0014 s]
Raw data (loadavg): 0.87 0.94 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0019 s]
Raw data (loadavg): 0.89 0.94 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0018 s]
Raw data (loadavg): 0.91 0.94 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0019 s]
Raw data (loadavg): 0.92 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0025 s]
Raw data (loadavg): 0.93 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0033 s]
Raw data (loadavg): 0.94 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.0035 s]
Raw data (loadavg): 0.95 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.003 s]
Raw data (loadavg): 0.96 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.004 s]
Raw data (loadavg): 0.96 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.005 s]
Raw data (loadavg): 0.97 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.97 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.006 s]
Raw data (loadavg): 0.98 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.98 0.95 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.007 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.01 s]
Raw data (loadavg): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.011 s]
Raw data (loadavg): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.012 s]
Raw data (loadavg): 0.99 0.96 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.71 s]
Raw data (loadavg): 0.99 0.97 0.98 1/53 14078
Raw data (stat): 14074 (minisat+_script) S 14073 32284 32283 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 781954996 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 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.7
CPU time (s): 1229.85
CPU user time (s): 1229.48
CPU system time (s): 0.374943
CPU usage (%): 100.012
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####