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-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3684
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.3
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 31098

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 21:58:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22485 boxname=wulflinc28 idbench=1301 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 22485
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        816708 kB
Buffers:         29972 kB
Cached:         167092 kB
SwapCached:        748 kB
Active:          18248 kB
Inactive:       181064 kB
HighTotal:      131008 kB
HighFree:         5348 kB
LowTotal:       903652 kB
LowFree:        811360 kB
SwapTotal:     2097640 kB
SwapFree:      2096192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5444 kB
Slab:            13096 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 22:18:54 (client local time) WITH STATUS 152 IN 1229.92 SECONDS
stats: 22485 7 1229.92 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> Adder-cost: 2160   maxlim: 1059   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35697   111365 |   11899       0        0     nan |  0.000 % |
c |       100 |   35673   111283 |   13088      98     3550    36.2 |  1.208 % |
c |       250 |   35673   111283 |   14397     248     6872    27.7 |  1.208 % |
c |       475 |   35673   111283 |   15837     473    22930    48.5 |  1.208 % |
c |       812 |   35582   110964 |   17421     797    32292    40.5 |  1.350 % |
c |      1318 |   35228   109731 |   19163    1236    39075    31.6 |  1.930 % |
c |      2077 |   35115   109352 |   21079    1978    55328    28.0 |  2.083 % |
c |      3216 |   35106   109323 |   23187    3116   134443    43.1 |  2.102 % |
c |      4924 |   35091   109270 |   25506    4817   501813   104.2 |  2.111 % |
c ==============================================================================
c [1mFound solution: 4678[0m
c ---[   0]---> Adder-cost: 8142   maxlim: 192513   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5808 |   91968   312356 |   30656    5701   636022   111.6 |  2.111 % |
c |      5908 |   91968   312356 |   33721    5801   638088   110.0 |  1.222 % |
c ==============================================================================
c [1mFound solution: 4381[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192810   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6012 |   91987   312479 |   30662    5905   642881   108.9 |  1.222 % |
c |      6113 |   91987   312479 |   33728    6006   643901   107.2 |  1.248 % |
c |      6263 |   91987   312479 |   37101    6156   648018   105.3 |  1.248 % |
c |      6490 |   91987   312479 |   40811    6383   655375   102.7 |  1.248 % |
c |      6828 |   91987   312479 |   44892    6721   678577   101.0 |  1.248 % |
c |      7334 |   91987   312479 |   49381    7227   710491    98.3 |  1.248 % |
c |      8093 |   91987   312479 |   54319    7986   772776    96.8 |  1.248 % |
c ==============================================================================
c [1mFound solution: 4329[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192862   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8535 |   92003   312609 |   30667    8428   796805    94.5 |  1.248 % |
c |      8635 |   91996   312585 |   33733    8527   798553    93.6 |  1.285 % |
c |      8786 |   91996   312585 |   37107    8678   799323    92.1 |  1.285 % |
c |      9015 |   91996   312585 |   40817    8907   810541    91.0 |  1.285 % |
c ==============================================================================
c [1mFound solution: 4303[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192888   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9343 |   92000   312645 |   30666    9235   872957    94.5 |  1.285 % |
c |      9447 |   92000   312645 |   33732    9339   877086    93.9 |  1.306 % |
c |      9599 |   92000   312645 |   37105    9491   896729    94.5 |  1.306 % |
c |      9825 |   91979   312575 |   40816    9711   900061    92.7 |  1.322 % |
c |     10164 |   91979   312575 |   44898   10050   962481    95.8 |  1.322 % |
c |     10673 |   91967   312533 |   49387   10550  1020834    96.8 |  1.328 % |
c |     11432 |   91967   312533 |   54326   11309  1107842    98.0 |  1.328 % |
c |     12574 |   91967   312533 |   59759   12451  1288451   103.5 |  1.328 % |
c |     14282 |   91951   312481 |   65735   14156  1567998   110.8 |  1.344 % |
c |     16846 |   91944   312457 |   72308   16718  2021257   120.9 |  1.349 % |
c |     20697 |   91944   312457 |   79539   20569  2889530   140.5 |  1.349 % |
c ==============================================================================
c [1mFound solution: 4269[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192922   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21234 |   91954   312544 |   30651   21106  2966775   140.6 |  1.349 % |
c |     21335 |   91898   312350 |   33716   21192  2969519   140.1 |  1.413 % |
c |     21485 |   91898   312350 |   37087   21342  3004545   140.8 |  1.413 % |
c |     21711 |   91785   311959 |   40796   21531  3013007   139.9 |  1.504 % |
c |     22051 |   91785   311959 |   44876   21871  3070258   140.4 |  1.504 % |
c |     22559 |   91785   311959 |   49363   22379  3176774   142.0 |  1.504 % |
c |     23320 |   91756   311856 |   54300   23120  3255681   140.8 |  1.520 % |
c |     24459 |   91756   311856 |   59730   24259  3473974   143.2 |  1.520 % |
c |     26169 |   91756   311856 |   65703   25969  3776044   145.4 |  1.520 % |
c |     28733 |   91756   311856 |   72273   28533  4179806   146.5 |  1.520 % |
c |     32579 |   91676   311577 |   79500   32345  4833206   149.4 |  1.589 % |
c |     38348 |   91676   311577 |   87450   38114  6308737   165.5 |  1.589 % |
c |     46997 |   91601   311320 |   96195   46740  8459122   181.0 |  1.643 % |
c ==============================================================================
c [1mFound solution: 4262[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192929   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59475 |   91556   311180 |   30518   59211 11444311   193.3 |  1.643 % |
c |     59575 |   91556   311180 |   33569   16951  2967034   175.0 |  1.685 % |
c |     59727 |   91556   311180 |   36926   17103  2987056   174.7 |  1.685 % |
c |     59955 |   91556   311180 |   40619   17331  3023499   174.5 |  1.685 % |
c |     60296 |   91556   311180 |   44681   17672  3059606   173.1 |  1.685 % |
c |     60802 |   91556   311180 |   49149   18178  3146794   173.1 |  1.685 % |
c |     61561 |   91556   311180 |   54064   18937  3286300   173.5 |  1.685 % |
c |     62700 |   91556   311180 |   59470   20076  3636099   181.1 |  1.685 % |
c |     64412 |   91556   311180 |   65418   21788  3877981   178.0 |  1.685 % |
c ==============================================================================
c [1mFound solution: 4219[0m
c ---[   0]---> Adder-cost: 0   maxlim: 192972   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66546 |   91560   311241 |   30520   23922  4366619   182.5 |  1.685 % |
c |     66646 |   91560   311241 |   33572   24022  4371054   182.0 |  1.707 % |
c |     66797 |   91560   311241 |   36929   24173  4384424   181.4 |  1.707 % |
c |     67026 |   91560   311241 |   40622   24402  4398296   180.2 |  1.707 % |
c |     67363 |   91560   311241 |   44684   24739  4461698   180.4 |  1.707 % |
c |     67871 |   91560   311241 |   49152   25247  4557821   180.5 |  1.707 % |
c |     68634 |   91560   311241 |   54068   26010  4671976   179.6 |  1.707 % |
c |     69773 |   91560   311241 |   59474   27149  5037188   185.5 |  1.707 % |
c |     71481 |   91560   311241 |   65422   28857  5394646   186.9 |  1.707 % |
c |     74043 |   91535   311160 |   71964   31415  6062380   193.0 |  1.733 % |
c |     77887 |   91535   311160 |   79161   35259  6921757   196.3 |  1.733 % |
c |     83653 |   91535   311160 |   87077   41025  8057816   196.4 |  1.733 % |
c |     92304 |   91535   311160 |   95784   49676 10781790   217.0 |  1.733 % |
c ==============================================================================
c [1mFound solution: 4172[0m
c ---[   0]---> Adder-cost: 0   maxlim: 193019   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95559 |   91542   311224 |   30514   52931 11644687   220.0 |  1.733 % |
c |     95659 |   91542   311224 |   33565   18941  3654438   192.9 |  1.754 % |
c |     95809 |   91542   311224 |   36921   19091  3658733   191.6 |  1.754 % |
c ==============================================================================
c [1mFound solution: 3944[0m
c ---[   0]---> Adder-cost: 0   maxlim: 193247   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95994 |   91551   311287 |   30517   19276  3681560   191.0 |  1.754 % |
c |     96096 |   91551   311287 |   33568   19378  3703843   191.1 |  1.775 % |
c |     96246 |   91551   311287 |   36925   19528  3722802   190.6 |  1.775 % |
c |     96471 |   91551   311287 |   40618   19753  3810541   192.9 |  1.775 % |
c |     96811 |   91551   311287 |   44679   20093  3856602   191.9 |  1.775 % |
c |     97319 |   91551   311287 |   49147   20601  3980720   193.2 |  1.775 % |
c |     98078 |   91551   311287 |   54062   21360  4197445   196.5 |  1.775 % |
c |     99219 |   91551   311287 |   59468   22501  4443126   197.5 |  1.775 % |
c |    100927 |   91551   311287 |   65415   24209  5125900   211.7 |  1.775 % |
c |    103490 |   91551   311287 |   71957   26772  5785251   216.1 |  1.775 % |
c |    107334 |   91551   311287 |   79153   30616  7230782   236.2 |  1.775 % |
c |    113103 |   91551   311287 |   87068   36385  8775221   241.2 |  1.775 % |
c |    121753 |   91551   311287 |   95775   45035 11913321   264.5 |  1.775 % |
c |    134728 |   91506   311130 |  105352   58002 16013485   276.1 |  1.796 % |
c |    154190 |   91497   311099 |  115888   77462 23776761   306.9 |  1.802 % |
c |    183385 |   91480   311042 |  127477  106650 33287203   312.1 |  1.812 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10757 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.95 0.90 2/54 10753
Raw data (stat): 10753 (runsolver) R 10752 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842307077 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0023 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0024 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0034 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 10757
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 10760
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 1.06 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 1.05 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 1.04 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 1.03 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 10810
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.01 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.015 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.018 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.019 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.02 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.021 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10812
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.022 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.023 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.024 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.025 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.033 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.038 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 0.98 0.91 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.08 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.78 s]
Raw data (loadavg): 1.02 1.00 0.92 1/53 10814
Raw data (stat): 10753 (minisat+_script) S 10752 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842307077 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.78
CPU time (s): 1229.92
CPU user time (s): 1228.43
CPU system time (s): 1.48677
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####