PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb
MD5SUM	dd81121db7c1c4b8597dd9571c707a87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	372
Biggest coefficient in the objective function	220
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	983
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	220
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	983
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.03484
Number of variables	372
Total number of constraints	792
Number of constraints which are clauses	345
Number of constraints which are cardinality constraints (but not clauses)	447
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	18
Trace number 31739

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        759196 kB
Buffers:         33812 kB
Cached:         219716 kB
SwapCached:        452 kB
Active:          50336 kB
Inactive:       205476 kB
HighTotal:      131008 kB
HighFree:        52752 kB
LowTotal:       903652 kB
LowFree:        706444 kB
SwapTotal:     2097892 kB
SwapFree:      2096752 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5616 kB
Slab:            14016 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 06:18:25 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23120 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 420 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   23
c ---[  83]---> BDD-cost:   29
c ---[  82]---> BDD-cost:   35
c ---[  81]---> BDD-cost:   35
c ---[  80]---> BDD-cost:   32
c ---[  79]---> BDD-cost:   32
c ---[  78]---> BDD-cost:   26
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   20
c ---[  74]---> BDD-cost:   26
c ---[  73]---> BDD-cost:   32
c ---[  72]---> BDD-cost:   35
c ---[  71]---> BDD-cost:   35
c ---[  70]---> BDD-cost:   32
c ---[  69]---> BDD-cost:   35
c ---[  68]---> BDD-cost:   26
c ---[  67]---> BDD-cost:   23
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   18
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   32
c ---[  62]---> BDD-cost:   38
c ---[  61]---> BDD-cost:   44
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   38
c ---[  58]---> BDD-cost:   32
c ---[  57]---> BDD-cost:   26
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   23
c ---[  53]---> BDD-cost:   32
c ---[  52]---> BDD-cost:   44
c ---[  51]---> BDD-cost:   47
c ---[  50]---> BDD-cost:   41
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:   29
c ---[  47]---> BDD-cost:   21
c ---[  46]---> BDD-cost:   20
c ---[  45]---> BDD-cost:   11
c ---[  44]---> BDD-cost:   17
c ---[  43]---> BDD-cost:   21
c ---[  42]---> BDD-cost:   38
c ---[  41]---> BDD-cost:   32
c ---[  40]---> BDD-cost:   41
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   23
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:   14
c ---[  32]---> BDD-cost:   20
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   26
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:   11
c ---[  27]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    8
c ---[  23]---> BDD-cost:   11
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   11
c ---[  18]---> BDD-cost:    7
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    8
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4084    11649 |    1361       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 355[0m
c ---[   0]---> Sorter-cost:20800     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   39610    94771 |   13203       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 119[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        52 |   40635    97290 |   13545      47      509    10.8 |  0.000 % |
c |       153 |   40635    97290 |   14899     148     2006    13.6 |  0.807 % |
c |       303 |   40635    97290 |   16389     298     3680    12.3 |  0.807 % |
c ==============================================================================
c [1mFound solution: 93[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       335 |   40816    97778 |   13605     330     3969    12.0 |  0.807 % |
c ==============================================================================
c [1mFound solution: 74[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       381 |   40957    98168 |   13652     376     4254    11.3 |  0.807 % |
c |       482 |   40957    98168 |   15017     477     6680    14.0 |  0.809 % |
c ==============================================================================
c [1mFound solution: 66[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |   41021    98358 |   13673     538     7309    13.6 |  0.809 % |
c |       643 |   41007    98330 |   15040     637     8156    12.8 |  0.847 % |
c ==============================================================================
c [1mFound solution: 39[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       741 |   41137    98688 |   13712     735    12723    17.3 |  0.847 % |
c |       841 |   41137    98688 |   15083     835    14812    17.7 |  0.858 % |
c |       991 |   41137    98688 |   16591     985    15900    16.1 |  0.858 % |
c |      1216 |   41137    98688 |   18250    1210    24830    20.5 |  0.858 % |
c ==============================================================================
c [1mFound solution: 32[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1549 |   40826    98032 |   13608    1526    31796    20.8 |  0.858 % |
c |      1649 |   40807    97993 |   14968    1625    32748    20.2 |  1.610 % |
c |      1799 |   40807    97993 |   16465    1775    35020    19.7 |  1.610 % |
c |      2024 |   40807    97993 |   18112    2000    57066    28.5 |  1.610 % |
c |      2361 |   40157    96519 |   19923    2253    61245    27.2 |  2.962 % |
c |      2870 |   40157    96519 |   21915    2762    71091    25.7 |  2.962 % |
c |      3629 |   40157    96519 |   24107    3521    86728    24.6 |  2.962 % |
c |      4768 |   40069    96331 |   26518    4641   109000    23.5 |  3.209 % |
c |      6476 |   39881    95923 |   29169    6320   241528    38.2 |  3.710 % |
c |      9040 |   39881    95923 |   32086    8884   558335    62.8 |  3.710 % |
c |     12886 |   39881    95923 |   35295   12730   837536    65.8 |  3.710 % |
c |     18654 |   39881    95923 |   38825   18498  1338946    72.4 |  3.710 % |
c |     27303 |   39881    95923 |   42707   27147  2479319    91.3 |  3.710 % |
c ==============================================================================
c [1mFound solution: 31[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30230 |   39885    95933 |   13295   30074  2833854    94.2 |  3.710 % |
c |     30330 |   39885    95933 |   14624   13138  1476713   112.4 |  3.714 % |
c |     30481 |   39885    95933 |   16086   13289  1480028   111.4 |  3.714 % |
c |     30709 |   39885    95933 |   17695   13517  1485023   109.9 |  3.714 % |
c |     31046 |   39885    95933 |   19465   13854  1491450   107.7 |  3.714 % |
c |     31552 |   39885    95933 |   21411   14360  1526895   106.3 |  3.714 % |
c |     32311 |   39885    95933 |   23552   15119  1570893   103.9 |  3.714 % |
c |     33452 |   39885    95933 |   25908   16260  1620404    99.7 |  3.714 % |
c |     35160 |   39871    95901 |   28499   17966  1667556    92.8 |  3.734 % |
c |     37722 |   39871    95901 |   31348   20528  1922784    93.7 |  3.734 % |
c ==============================================================================
c [1mFound solution: 30[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37876 |   39892    95963 |   13297   20682  1934151    93.5 |  3.734 % |
c |     37977 |   39838    95840 |   14626   10433   624856    59.9 |  3.810 % |
c |     38128 |   39838    95840 |   16089   10584   628193    59.4 |  3.810 % |
c |     38354 |   39838    95840 |   17698   10810   630346    58.3 |  3.810 % |
c |     38692 |   39838    95840 |   19468   11148   638017    57.2 |  3.810 % |
c |     39198 |   39838    95840 |   21414   11654   656390    56.3 |  3.810 % |
c |     39957 |   39820    95799 |   23556   12406   664944    53.6 |  3.835 % |
c ==============================================================================
c [1mFound solution: 25[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40470 |   39846    95875 |   13282   12919   696562    53.9 |  3.835 % |
c |     40570 |   39846    95875 |   14610   13019   698367    53.6 |  3.837 % |
c |     40720 |   39846    95875 |   16071   13169   700531    53.2 |  3.837 % |
c |     40945 |   39846    95875 |   17678   13394   705284    52.7 |  3.837 % |
c |     41282 |   39739    95631 |   19446   13723   724893    52.8 |  4.074 % |
c |     41789 |   39739    95631 |   21390   14230   774776    54.4 |  4.074 % |
c |     42549 |   39721    95589 |   23529   14989   793085    52.9 |  4.129 % |
c |     43688 |   39721    95589 |   25882   16128   862249    53.5 |  4.129 % |
c |     45397 |   39721    95589 |   28471   17837   943295    52.9 |  4.129 % |
c |     47959 |   39721    95589 |   31318   20399  1340906    65.7 |  4.129 % |
c |     51803 |   39721    95589 |   34450   24243  1730566    71.4 |  4.129 % |
c ==============================================================================
c [1mFound solution: 18[0m
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53697 |   39759    95694 |   13253   26132  1833701    70.2 |  4.129 % |
c |     53798 |   39759    95694 |   14578   13167   983300    74.7 |  4.137 % |
c |     53948 |   39721    95606 |   16036   13310   984452    74.0 |  4.197 % |
c |     54173 |   39721    95606 |   17639   13535   995185    73.5 |  4.197 % |
c |     54510 |   39721    95606 |   19403   13872  1004647    72.4 |  4.197 % |
c ==============================================================================
c [1mFound solution: 9[0m
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54616 |   39766    95725 |   13255   13978  1006538    72.0 |  4.197 % |
c |     54716 |   39748    95684 |   14580   14071  1007232    71.6 |  4.220 % |
c |     54866 |   39748    95684 |   16038   14221  1012093    71.2 |  4.220 % |
c |     55091 |   39742    95670 |   17642   14443  1014604    70.2 |  4.230 % |
c |     55428 |   39738    95661 |   19406   14779  1023087    69.2 |  4.235 % |
c |     55934 |   39738    95661 |   21347   15285  1037095    67.9 |  4.235 % |
c |     56693 |   39738    95661 |   23482   16044  1092277    68.1 |  4.235 % |
c |     57832 |   39738    95661 |   25830   17183  1134775    66.0 |  4.235 % |
c |     59541 |   39738    95661 |   28413   18892  1247008    66.0 |  4.235 % |
c |     62103 |   39738    95661 |   31254   21454  1403165    65.4 |  4.235 % |
c |     65947 |   39738    95661 |   34380   25298  2020808    79.9 |  4.235 % |
c |     71714 |   39738    95661 |   37818   31065  2590932    83.4 |  4.235 % |
c |     80363 |   39738    95661 |   41599   39714  3547339    89.3 |  4.235 % |
c |     93337 |   39738    95661 |   45759   19456  2317262   119.1 |  4.235 % |
c |    112798 |   39738    95661 |   50335   38917  5379251   138.2 |  4.235 % |
c |    141992 |   39716    95612 |   55369   26150  3557617   136.0 |  4.270 % |
c |    185781 |   39640    95444 |   60906   27874  1990715    71.4 |  4.457 % |
c |    251466 |   39640    95444 |   66997   44447  9458461   212.8 |  4.457 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11758 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.92 0.97 0.91 2/54 11754
Raw data (stat): 11754 (runsolver) R 11753 20001 20000 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853814863 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0036 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0056 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0057 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11758
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 11759
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.063 s]
Raw data (loadavg): 1.14 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.064 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.064 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.065 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.064 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.065 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.066 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 11811
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.066 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.067 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.066 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.067 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.067 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.068 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.069 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.069 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.069 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.07 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.071 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.072 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.073 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.074 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.075 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.076 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.077 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11813
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.078 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.079 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.08 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.081 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.082 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.083 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.084 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.085 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.086 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.087 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.088 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.089 s]
Raw data (loadavg): 1.00 1.00 0.92 3/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.089 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.091 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.092 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.093 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.093 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.094 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.094 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.094 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.1 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.7 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 11815
Raw data (stat): 11754 (minisat+_script) S 11753 20001 20000 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853814863 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 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.86
CPU user time (s): 1229.31
CPU system time (s): 0.547916
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####