PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-rgn.opb
MD5SUM	1400a638b0a1a6fa8602672cb986ba1d
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	67200
Optimality of the best value was proved	NO
Number of terms in the objective function	920
Biggest coefficient in the objective function	24576
Number of bits for the biggest coefficient in the objective function	15
Sum of the numbers in the objective function	1986400
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3200000000
Number of bits of the biggest number in a constraint	32
Biggest sum of numbers in a constraint	29101875011
Number of bits of the biggest sum of numbers	35
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1227.77
Number of variables	1020
Total number of constraints	204
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	104
Number of constraints which are nor clauses,nor cardinality constraints	100
Minimum length of a constraint	1
Maximum length of a constraint	103
Trace number 31114

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-25 22:08:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22510 boxname=wulflinc10 idbench=1326 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  1400a638b0a1a6fa8602672cb986ba1d  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-rgn.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-rgn.opb
IDLAUNCH: 22510
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        567512 kB
Buffers:         35644 kB
Cached:         409664 kB
SwapCached:         92 kB
Active:          67312 kB
Inactive:       380680 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        567260 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6392 kB
Slab:            13368 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:29:15 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 22510 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 124 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:    8
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    8
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    8
c ---[  98]---> BDD-cost:    8
c ---[  97]---> BDD-cost:    8
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    8
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:    8
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:    8
c ---[  84]---> BDD-cost:    8
c ---[  83]---> BDD-cost:    8
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    8
c ---[  79]---> BDD-cost:    8
c ---[  78]---> BDD-cost:    8
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    8
c ---[  73]---> BDD-cost:    8
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    8
c ---[  70]---> BDD-cost:    8
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    8
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:    8
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:  228
c ---[  40]---> BDD-cost:  906
c ---[  38]---> BDD-cost:  906
c ---[  36]---> BDD-cost:  906
c ---[  34]---> BDD-cost:  906
c ---[  32]---> BDD-cost:  906
c ---[  30]---> BDD-cost:  906
c ---[  28]---> BDD-cost:  906
c ---[  26]---> BDD-cost:  906
c ---[  24]---> BDD-cost:  906
c ---[  23]---> BDD-cost:   47
c ---[  21]---> BDD-cost:  906
c ---[  19]---> BDD-cost:  906
c ---[  17]---> BDD-cost:  906
c ---[  15]---> BDD-cost:  906
c ---[  13]---> BDD-cost:  906
c ---[  11]---> BDD-cost:  906
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   6]---> BDD-cost:  228
c ---[   4]---> BDD-cost:  228
c ---[   2]---> BDD-cost:  228
c ---[   0]---> BDD-cost:  228
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   40259   113278 |   13419       0        0     nan |  0.000 % |
c |       100 |   40118   112996 |   14760      92      564     6.1 |  0.951 % |
c |       250 |   40103   112966 |   16236     240     1981     8.3 |  0.998 % |
c |       477 |   40092   112944 |   17860     466     5702    12.2 |  1.031 % |
c |       814 |   40092   112944 |   19646     803    17649    22.0 |  1.031 % |
c |      1322 |   40092   112944 |   21611    1311    27839    21.2 |  1.031 % |
c |      2083 |   40092   112944 |   23772    2072    38233    18.5 |  1.031 % |
c |      3223 |   39997   112751 |   26149    3200    52692    16.5 |  1.247 % |
c |      4932 |   39983   112722 |   28764    4908    86494    17.6 |  1.254 % |
c |      7498 |   39909   112571 |   31641    7459   133322    17.9 |  1.483 % |
c |     11343 |   39891   112535 |   34805   11301   187175    16.6 |  1.537 % |
c |     17110 |   39766   112261 |   38285   17004   338276    19.9 |  1.874 % |
c |     25759 |   39746   112220 |   42114   25652   792984    30.9 |  1.881 % |
c |     38734 |   39746   112220 |   46326   38627  1026727    26.6 |  1.881 % |
c |     58198 |   39619   111941 |   50958   22540   676426    30.0 |  2.002 % |
c |     87390 |   39602   111907 |   56054   51730  1239064    24.0 |  2.056 % |
c |    131179 |   39292   111258 |   61659   50028  1324784    26.5 |  2.596 % |
c |    196863 |   39125   110902 |   67825   63381  1605437    25.3 |  3.034 % |
c |    295389 |   38687   109943 |   74608   50436  1436146    28.5 |  3.978 % |
c |    443178 |   38500   109542 |   82069   64703  1786871    27.6 |  4.402 % |
c ==============================================================================
c [1mFound solution: 814378[0m
c ---[   0]---> Sorter-cost:66120     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    658244 |  220981   535504 |   73660   52875  3351582    63.4 |  4.402 % |
c |    658344 |  220973   535488 |   81026   52973  3352621    63.3 |  1.005 % |
c |    658495 |  220952   535443 |   89128   53122  3353583    63.1 |  1.005 % |
c |    658720 |  220952   535443 |   98041   53347  3357206    62.9 |  1.005 % |
c |    659058 |  220952   535443 |  107845   53685  3362862    62.6 |  1.005 % |
c |    659564 |  220952   535443 |  118630   54191  3371925    62.2 |  1.005 % |
c |    660323 |  220952   535443 |  130493   54950  3394228    61.8 |  1.005 % |
c |    661462 |  220952   535443 |  143542   56089  3432961    61.2 |  1.005 % |
c |    663171 |  220952   535443 |  157896   57798  3459088    59.8 |  1.005 % |
c |    665733 |  220952   535443 |  173686   60360  3528174    58.5 |  1.005 % |
c |    669577 |  220952   535443 |  191055   64204  3606827    56.2 |  1.005 % |
c |    675343 |  220952   535443 |  210160   69970  3682771    52.6 |  1.005 % |
c |    683992 |  220952   535443 |  231176   78619  3957858    50.3 |  1.005 % |
c |    696967 |  220952   535443 |  254294   91594  4746587    51.8 |  1.005 % |
c |    716429 |  220935   535406 |  279723  111045  5477152    49.3 |  1.016 % |
c |    745621 |  220935   535406 |  307696  140237  6912181    49.3 |  1.016 % |
c |    789411 |  220903   535339 |  338465  184022  9087383    49.4 |  1.035 % |
c ==============================================================================
c [1mFound solution: 448098[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    805474 |  221600   537386 |   73866  200085  9691724    48.4 |  1.035 % |
c |    805576 |  221600   537386 |   81252   22706   518069    22.8 |  1.031 % |
c |    805727 |  221600   537386 |   89377   22857   519321    22.7 |  1.031 % |
c |    805952 |  221600   537386 |   98315   23082   522059    22.6 |  1.031 % |
c |    806290 |  221600   537386 |  108147   23420   525041    22.4 |  1.031 % |
c |    806797 |  221600   537386 |  118961   23927   529488    22.1 |  1.031 % |
c |    807556 |  221518   537202 |  130858   24683   541108    21.9 |  1.058 % |
c |    808695 |  221477   537108 |  143943   25821   552112    21.4 |  1.071 % |
c |    810404 |  221477   537108 |  158338   27530   582434    21.2 |  1.071 % |
c |    812969 |  221477   537108 |  174172   30095   668074    22.2 |  1.071 % |
c |    816814 |  221477   537108 |  191589   33940   772663    22.8 |  1.071 % |
c |    822580 |  221477   537108 |  210748   39706  1057784    26.6 |  1.071 % |
c |    831229 |  221477   537108 |  231823   48355  1421889    29.4 |  1.071 % |
c |    844203 |  221477   537108 |  255005   61329  1917977    31.3 |  1.071 % |
c |    863664 |  221477   537108 |  280506   80790  2407543    29.8 |  1.071 % |
c |    892856 |  221381   536907 |  308556  109946  3371240    30.7 |  1.129 % |
c ==============================================================================
c [1mFound solution: 233250[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    897055 |  221462   537101 |   73820  114145  3524606    30.9 |  1.129 % |
c |    897155 |  221462   537101 |   81202   27724   519075    18.7 |  1.129 % |
c |    897305 |  221462   537101 |   89322   27874   520470    18.7 |  1.129 % |
c |    897530 |  221462   537101 |   98254   28099   522245    18.6 |  1.129 % |
c |    897868 |  221171   536443 |  108079   28404   524583    18.5 |  1.232 % |
c |    898374 |  221171   536443 |  118887   28910   538384    18.6 |  1.232 % |
c |    899133 |  221171   536443 |  130776   29669   549995    18.5 |  1.232 % |
c |    900273 |  221171   536443 |  143854   30809   561146    18.2 |  1.232 % |
c |    901981 |  221171   536443 |  158239   32517   592744    18.2 |  1.232 % |
c |    904543 |  221171   536443 |  174063   35079   710858    20.3 |  1.232 % |
c |    908389 |  221171   536443 |  191470   38925   853279    21.9 |  1.232 % |
c |    914155 |  221171   536443 |  210617   44691  1111469    24.9 |  1.232 % |
c |    922804 |  221171   536443 |  231678   53340  1322266    24.8 |  1.232 % |
c |    935778 |  221134   536360 |  254846   66304  1882902    28.4 |  1.254 % |
c |    955240 |  221134   536360 |  280331   85766  2967169    34.6 |  1.254 % |
c |    984432 |  221107   536306 |  308364  114945  4194533    36.5 |  1.270 % |
c ==============================================================================
c [1mFound solution: 233162[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    988122 |  221125   536453 |   73708  118635  4301809    36.3 |  1.270 % |
c |    988222 |  221123   536449 |   81078   30375   683144    22.5 |  1.273 % |
c |    988372 |  221123   536449 |   89186   30525   684026    22.4 |  1.273 % |
c |    988597 |  221123   536449 |   98105   30750   686137    22.3 |  1.273 % |
c |    988934 |  220944   536046 |  107915   31076   688900    22.2 |  1.334 % |
c |    989440 |  220944   536046 |  118707   31582   693327    22.0 |  1.334 % |
c |    990201 |  220944   536046 |  130578   32343   703900    21.8 |  1.334 % |
c |    991340 |  220944   536046 |  143636   33482   716103    21.4 |  1.334 % |
c |    993048 |  220944   536046 |  157999   35190   774995    22.0 |  1.334 % |
c |    995610 |  220932   536019 |  173799   37751   921702    24.4 |  1.338 % |
c |    999454 |  220932   536019 |  191179   41595  1028393    24.7 |  1.338 % |
c |   1005222 |  220932   536019 |  210297   47363  2188043    46.2 |  1.338 % |
c |   1013873 |  220932   536019 |  231327   56014  2367858    42.3 |  1.338 % |
c |   1026847 |  220932   536019 |  254460   68988  3142624    45.6 |  1.338 % |
c |   1046310 |  220932   536019 |  279906   88451  4144431    46.9 |  1.338 % |
c ==============================================================================
c [1mFound solution: 216484[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1047505 |  220617   535311 |   73539   89627  4182324    46.7 |  1.338 % |
c |   1047606 |  220617   535311 |   80892   32998   660591    20.0 |  1.471 % |
c |   1047757 |  220617   535311 |   88982   33149   662245    20.0 |  1.471 % |
c |   1047982 |  220617   535311 |   97880   33374   664248    19.9 |  1.471 % |
c |   1048319 |  220617   535311 |  107668   33711   668588    19.8 |  1.471 % |
c |   1048825 |  220617   535311 |  118435   34217   674919    19.7 |  1.471 % |
c |   1049584 |  220280   534537 |  130278   34959   688719    19.7 |  1.609 % |
c |   1050724 |  220280   534537 |  143306   36099   723586    20.0 |  1.609 % |
c |   1052432 |  220280   534537 |  157637   37807   783850    20.7 |  1.609 % |
c |   1054994 |  220280   534537 |  173401   40369   858493    21.3 |  1.609 % |
c |   1058838 |  220280   534537 |  190741   44213  1043337    23.6 |  1.609 % |
c |   1064606 |  220280   534537 |  209815   49981  1280146    25.6 |  1.609 % |
c |   1073256 |  220268   534508 |  230796   58630  2348457    40.1 |  1.612 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  2820 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.93 0.97 0.91 1/54 2816
Raw data (stat): 2816 (runsolver) D 2815 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 784154804 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0012 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.0003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+139.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+159.999 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+169.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+179.999 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+949.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+969.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+999.999 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 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.77 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 2820
Raw data (stat): 2816 (minisat+_script) S 2815 15547 15546 0 -1 0 274 239 0 0 0 0 0 0 18 0 1 0 784154804 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.77
CPU time (s): 1229.87
CPU user time (s): 1229.27
CPU system time (s): 0.598908
CPU usage (%): 100.008
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####