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 19188

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 18:13:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16905 boxname=wulflinc31 idbench=1301 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 16905
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        868392 kB
Buffers:         30648 kB
Cached:         110364 kB
SwapCached:        632 kB
Active:          11016 kB
Inactive:       131956 kB
HighTotal:      131008 kB
HighFree:       115388 kB
LowTotal:       903652 kB
LowFree:        753004 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            17604 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:33:40 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 16905 7 1200.25 10
#### 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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 CO100081_bit0 -CO100082_bit0 CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 CO100135_bit0 -CO100136_bit0 -CO100137_bit0 CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0#### 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 2/54 29974
Raw data (stat): 29974 (runsolver) R 29973 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547138374 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 2622 0 1 0 989 7 0 0 25 0 1 0 547138374 12840960 2475 4294967295 134512640 134672761 3221224624 3221223808 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2475 603 41 0 3094 0
vsize: 12540
[startup+20.0003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 7152 0 1 0 1976 19 0 0 25 0 1 0 547138374 30240768 6252 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7383 6252 603 41 0 7342 0
vsize: 29532
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 7544 0 1 0 2974 21 0 0 25 0 1 0 547138374 31604736 6560 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7716 6560 603 41 0 7675 0
vsize: 30864
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 7984 0 1 0 3973 22 0 0 25 0 1 0 547138374 33357824 7000 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8144 7000 603 41 0 8103 0
vsize: 32576
[startup+50.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 8477 0 1 0 4972 23 0 0 25 0 1 0 547138374 35459072 7493 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8657 7493 603 41 0 8616 0
vsize: 34628
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 8995 0 1 0 5970 25 0 0 25 0 1 0 547138374 37478400 8011 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 8011 603 41 0 9109 0
vsize: 36600
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 9617 0 1 0 6967 27 0 0 25 0 1 0 547138374 39686144 8549 4294967295 134512640 134672761 3221224624 3221223808 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9689 8549 603 41 0 9648 0
vsize: 38756
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 9905 0 1 0 7966 28 0 0 25 0 1 0 547138374 40902656 8837 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9986 8837 603 41 0 9945 0
vsize: 39944
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 10379 0 1 0 8965 30 0 0 25 0 1 0 547138374 42782720 9311 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10445 9311 603 41 0 10404 0
vsize: 41780
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 10865 0 1 0 9963 31 0 0 25 0 1 0 547138374 44797952 9797 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10937 9797 603 41 0 10896 0
vsize: 43748
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 11339 0 1 0 10962 33 0 0 25 0 1 0 547138374 46813184 10271 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11429 10271 603 41 0 11388 0
vsize: 45716
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 11611 0 1 0 11961 34 0 0 25 0 1 0 547138374 48013312 10543 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11722 10543 603 41 0 11681 0
vsize: 46888
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 11984 0 1 0 12960 35 0 0 25 0 1 0 547138374 49487872 10916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12082 10916 603 41 0 12041 0
vsize: 48328
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 12498 0 1 0 13957 37 0 0 25 0 1 0 547138374 51646464 11430 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12609 11430 603 41 0 12568 0
vsize: 50436
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 13015 0 1 0 14956 39 0 0 25 0 1 0 547138374 53661696 11947 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13101 11947 603 41 0 13060 0
vsize: 52404
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 13381 0 1 0 15955 41 0 0 25 0 1 0 547138374 55148544 12313 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12313 603 41 0 13423 0
vsize: 53856
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 13802 0 1 0 16953 43 0 0 25 0 1 0 547138374 56889344 12734 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13889 12734 603 41 0 13848 0
vsize: 55556
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 14280 0 1 0 17952 44 0 0 25 0 1 0 547138374 58904576 13212 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14381 13212 603 41 0 14340 0
vsize: 57524
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 14755 0 1 0 18950 45 0 0 25 0 1 0 547138374 60776448 13687 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14838 13687 603 41 0 14797 0
vsize: 59352
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 15169 0 1 0 19949 47 0 0 25 0 1 0 547138374 62500864 14101 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15259 14101 603 41 0 15218 0
vsize: 61036
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 15515 0 1 0 20948 48 0 0 25 0 1 0 547138374 63848448 14447 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15588 14447 603 41 0 15547 0
vsize: 62352
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 15999 0 1 0 21947 50 0 0 25 0 1 0 547138374 65851392 14931 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16077 14931 603 41 0 16036 0
vsize: 64308
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 16459 0 1 0 22946 51 0 0 25 0 1 0 547138374 67723264 15391 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16534 15391 603 41 0 16493 0
vsize: 66136
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 16933 0 1 0 23944 52 0 0 25 0 1 0 547138374 69726208 15865 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17023 15865 603 41 0 16982 0
vsize: 68092
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 17314 0 1 0 24944 53 0 0 25 0 1 0 547138374 71307264 16246 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17409 16246 603 41 0 17368 0
vsize: 69636
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 17735 0 1 0 25942 54 0 0 25 0 1 0 547138374 73039872 16667 4294967295 134512640 134672761 3221224624 3221223728 134559958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17832 16667 603 41 0 17791 0
vsize: 71328
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18225 0 1 0 26941 56 0 0 25 0 1 0 547138374 74915840 17157 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18290 17157 603 41 0 18249 0
vsize: 73160
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18498 0 1 0 27940 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18498 0 1 0 28941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18498 0 1 0 29941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 30941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 31941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223808 134559592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 32941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 33941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 34941 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 35942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 36942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 37942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 38942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 39942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18540 0 1 0 40942 57 0 0 25 0 1 0 547138374 75583488 17322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17322 603 41 0 18412 0
vsize: 73812
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18541 0 1 0 41943 57 0 0 25 0 1 0 547138374 75583488 17323 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18541 0 1 0 42943 57 0 0 25 0 1 0 547138374 75583488 17323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18541 0 1 0 43943 57 0 0 25 0 1 0 547138374 75583488 17323 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18541 0 1 0 44943 57 0 0 25 0 1 0 547138374 75583488 17323 4294967295 134512640 134672761 3221224624 3221223728 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18453 17323 603 41 0 18412 0
vsize: 73812
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 18843 0 1 0 45943 58 0 0 25 0 1 0 547138374 76931072 17625 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18782 17625 603 41 0 18741 0
vsize: 75128
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 46942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 47942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 48942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 49942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 50942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 51942 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 52943 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 53943 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 54943 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 55943 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 56943 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 57944 59 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 58944 60 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19227 0 1 0 59944 60 0 0 25 0 1 0 547138374 77123584 17694 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17694 603 41 0 18788 0
vsize: 75316
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19230 0 1 0 60944 60 0 0 25 0 1 0 547138374 77123584 17697 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18829 17697 603 41 0 18788 0
vsize: 75316
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 19739 0 1 0 61942 62 0 0 25 0 1 0 547138374 79269888 18206 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19353 18206 603 41 0 19312 0
vsize: 77412
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 20287 0 1 0 62940 64 0 0 25 0 1 0 547138374 81563648 18754 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19913 18754 603 41 0 19872 0
vsize: 79652
[startup+640.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 20786 0 1 0 63939 65 0 0 25 0 1 0 547138374 83578880 19253 4294967295 134512640 134672761 3221224624 3221223728 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20405 19253 603 41 0 20364 0
vsize: 81620
[startup+650.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 21343 0 1 0 64938 67 0 0 25 0 1 0 547138374 85852160 19810 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20960 19810 603 41 0 20919 0
vsize: 83840
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 22052 0 1 0 65935 69 0 0 25 0 1 0 547138374 88727552 20519 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21662 20519 603 41 0 21621 0
vsize: 86648
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 22423 0 1 0 66934 71 0 0 25 0 1 0 547138374 90214400 20890 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22025 20890 603 41 0 21984 0
vsize: 88100
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 22895 0 1 0 67933 72 0 0 25 0 1 0 547138374 92196864 21362 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22509 21362 603 41 0 22468 0
vsize: 90036
[startup+690.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 23290 0 1 0 68932 73 0 0 25 0 1 0 547138374 93806592 21757 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22902 21757 603 41 0 22861 0
vsize: 91608
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 23705 0 1 0 69931 74 0 0 25 0 1 0 547138374 95559680 22172 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23330 22172 603 41 0 23289 0
vsize: 93320
[startup+710.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 24267 0 1 0 70930 76 0 0 25 0 1 0 547138374 97861632 22734 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23892 22734 603 41 0 23851 0
vsize: 95568
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 24887 0 1 0 71928 77 0 0 25 0 1 0 547138374 100405248 23354 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24513 23354 603 41 0 24472 0
vsize: 98052
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 25435 0 1 0 72927 79 0 0 25 0 1 0 547138374 102522880 23902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25030 23902 603 41 0 24989 0
vsize: 100120
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 25916 0 1 0 73927 80 0 0 25 0 1 0 547138374 104509440 24383 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25515 24383 603 41 0 25474 0
vsize: 102060
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 26309 0 1 0 74925 81 0 0 25 0 1 0 547138374 106115072 24776 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25907 24776 603 41 0 25866 0
vsize: 103628
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 26719 0 1 0 75924 83 0 0 25 0 1 0 547138374 108097536 25186 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26391 25186 603 41 0 26350 0
vsize: 105564
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 27223 0 1 0 76922 85 0 0 25 0 1 0 547138374 110088192 25690 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26877 25690 603 41 0 26836 0
vsize: 107508
[startup+780.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 27669 0 1 0 77921 86 0 0 25 0 1 0 547138374 111955968 26136 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27333 26136 603 41 0 27292 0
vsize: 109332
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 28115 0 1 0 78920 88 0 0 25 0 1 0 547138374 113831936 26582 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27791 26582 603 41 0 27750 0
vsize: 111164
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 28731 0 1 0 79918 89 0 0 25 0 1 0 547138374 116269056 27198 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28386 27198 603 41 0 28345 0
vsize: 113544
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 29489 0 1 0 80916 92 0 0 25 0 1 0 547138374 119377920 27956 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29145 27956 603 41 0 29104 0
vsize: 116580
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 30128 0 1 0 81914 93 0 0 25 0 1 0 547138374 122060800 28595 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29800 28595 603 41 0 29759 0
vsize: 119200
[startup+830.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 30587 0 1 0 82914 94 0 0 25 0 1 0 547138374 123936768 29054 4294967295 134512640 134672761 3221224624 3221223728 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30258 29054 603 41 0 30217 0
vsize: 121032
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 31039 0 1 0 83912 96 0 0 25 0 1 0 547138374 125677568 29506 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30683 29506 603 41 0 30642 0
vsize: 122732
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 31431 0 1 0 84910 98 0 0 25 0 1 0 547138374 127283200 29898 4294967295 134512640 134672761 3221224624 3221223760 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31075 29898 603 41 0 31034 0
vsize: 124300
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 31768 0 1 0 85909 99 0 0 25 0 1 0 547138374 128761856 30235 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31436 30235 603 41 0 31395 0
vsize: 125744
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 32141 0 1 0 86908 100 0 0 25 0 1 0 547138374 130248704 30608 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31799 30608 603 41 0 31758 0
vsize: 127196
[startup+880.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 32523 0 1 0 87908 101 0 0 25 0 1 0 547138374 131735552 30990 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32162 30990 603 41 0 32121 0
vsize: 128648
[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 32957 0 1 0 88907 103 0 0 25 0 1 0 547138374 133599232 31424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32617 31424 603 41 0 32576 0
vsize: 130468
[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 33325 0 1 0 89906 104 0 0 25 0 1 0 547138374 135073792 31792 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32977 31792 603 41 0 32936 0
vsize: 131908
[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 33685 0 1 0 90905 105 0 0 25 0 1 0 547138374 136544256 32152 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33336 32152 603 41 0 33295 0
vsize: 133344
[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 34051 0 1 0 91904 106 0 0 25 0 1 0 547138374 137998336 32518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33691 32518 603 41 0 33650 0
vsize: 134764
[startup+930.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 34443 0 1 0 92904 107 0 0 25 0 1 0 547138374 139579392 32910 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34077 32910 603 41 0 34036 0
vsize: 136308
[startup+940.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 34813 0 1 0 93902 109 0 0 25 0 1 0 547138374 141180928 33280 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34468 33280 603 41 0 34427 0
vsize: 137872
[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 35199 0 1 0 94901 110 0 0 25 0 1 0 547138374 142778368 33666 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34858 33666 603 41 0 34817 0
vsize: 139432
[startup+960.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 35598 0 1 0 95900 112 0 0 25 0 1 0 547138374 144375808 34065 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35248 34065 603 41 0 35207 0
vsize: 140992
[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 35975 0 1 0 96899 112 0 0 25 0 1 0 547138374 145833984 34442 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35604 34442 603 41 0 35563 0
vsize: 142416
[startup+980.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 36219 0 1 0 97899 113 0 0 25 0 1 0 547138374 146911232 34686 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35867 34686 603 41 0 35826 0
vsize: 143468
[startup+990.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 36592 0 1 0 98898 114 0 0 25 0 1 0 547138374 148377600 35059 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36225 35059 603 41 0 36184 0
vsize: 144900
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 37027 0 1 0 99897 115 0 0 25 0 1 0 547138374 150249472 35494 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36682 35494 603 41 0 36641 0
vsize: 146728
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 37423 0 1 0 100896 117 0 0 25 0 1 0 547138374 151859200 35890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37075 35890 603 41 0 37034 0
vsize: 148300
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 37695 0 1 0 101895 118 0 0 25 0 1 0 547138374 152924160 36162 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37335 36162 603 41 0 37294 0
vsize: 149340
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 38113 0 1 0 102894 119 0 0 25 0 1 0 547138374 154685440 36580 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37765 36580 603 41 0 37724 0
vsize: 151060
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 38396 0 1 0 103893 120 0 0 25 0 1 0 547138374 155766784 36863 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38029 36863 603 41 0 37988 0
vsize: 152116
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 38763 0 1 0 104892 121 0 0 25 0 1 0 547138374 157224960 37230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38385 37230 603 41 0 38344 0
vsize: 153540
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 39274 0 1 0 105892 122 0 0 25 0 1 0 547138374 159367168 37741 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38908 37741 603 41 0 38867 0
vsize: 155632
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 39662 0 1 0 106891 123 0 0 25 0 1 0 547138374 160964608 38129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39298 38129 603 41 0 39257 0
vsize: 157192
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 39997 0 1 0 107890 123 0 0 25 0 1 0 547138374 162295808 38464 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39623 38464 603 41 0 39582 0
vsize: 158492
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 40354 0 1 0 108890 124 0 0 25 0 1 0 547138374 163749888 38821 4294967295 134512640 134672761 3221224624 3221223808 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39978 38821 603 41 0 39937 0
vsize: 159912
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 40840 0 1 0 109889 126 0 0 25 0 1 0 547138374 165752832 39307 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40467 39307 603 41 0 40426 0
vsize: 161868
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 41116 0 1 0 110888 127 0 0 25 0 1 0 547138374 166961152 39583 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40762 39583 603 41 0 40721 0
vsize: 163048
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 41381 0 1 0 111886 128 0 0 25 0 1 0 547138374 168038400 39848 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41025 39848 603 41 0 40984 0
vsize: 164100
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 41775 0 1 0 112884 130 0 0 25 0 1 0 547138374 169644032 40242 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41417 40242 603 41 0 41376 0
vsize: 165668
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 42258 0 1 0 113882 132 0 0 25 0 1 0 547138374 171626496 40725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41901 40725 603 41 0 41860 0
vsize: 167604
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 42692 0 1 0 114881 133 0 0 25 0 1 0 547138374 173359104 41159 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42324 41159 603 41 0 42283 0
vsize: 169296
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 43148 0 1 0 115881 134 0 0 25 0 1 0 547138374 175222784 41615 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42779 41615 603 41 0 42738 0
vsize: 171116
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 43595 0 1 0 116880 135 0 0 25 0 1 0 547138374 177094656 42062 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43236 42062 603 41 0 43195 0
vsize: 172944
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 44013 0 1 0 117879 136 0 0 25 0 1 0 547138374 178688000 42480 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43625 42480 603 41 0 43584 0
vsize: 174500
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 44391 0 1 0 118878 137 0 0 25 0 1 0 547138374 180281344 42858 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44014 42858 603 41 0 43973 0
vsize: 176056
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29974
Raw data (stat): 29974 (minisat+) R 29973 23176 23175 0 -1 0 44770 0 1 0 119877 138 0 0 25 0 1 0 547138374 181870592 43237 4294967295 134512640 134672761 3221224624 3221223760 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44402 43237 603 41 0 44361 0
vsize: 177608
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 29974
Raw data (stat): 29974 (minisat+) Z 29973 23176 23175 0 -1 12 44773 0 1 0 119877 146 0 0 25 0 1 0 547138374 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.15
CPU time (s): 1200.25
CPU user time (s): 1198.78
CPU system time (s): 1.46978
CPU usage (%): 100.008
Max. virtual memory (Kb): 177608
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####