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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl35_36_pb.cnf.cr.opb
MD5SUMc779424bd1795a1e1adf6f4e7f38e307
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 37
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.075987
Number of variables2520
Total number of constraints142
Number of constraints which are clauses72
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint36

Trace number 6146 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-14 03:30:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4526 boxname=wulflinc1 idbench=14 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c779424bd1795a1e1adf6f4e7f38e307  /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_36_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_36_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc1/normalized-chnl35_36_pb.cnf.cr.opb
IDLAUNCH: 4526
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        843708 kB
Buffers:         41168 kB
Cached:         125636 kB
SwapCached:          0 kB
Active:         110812 kB
Inactive:        59064 kB
HighTotal:      131008 kB
HighFree:        12768 kB
LowTotal:       903652 kB
LowFree:        830940 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15308 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:50:20 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4526 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 142 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................
c ---[  69]---> BDD-cost:   69
c ---[  68]---> BDD-cost:   69
c ---[  67]---> BDD-cost:   69
c ---[  66]---> BDD-cost:   69
c ---[  65]---> BDD-cost:   69
c ---[  64]---> BDD-cost:   69
c ---[  63]---> BDD-cost:   69
c ---[  62]---> BDD-cost:   69
c ---[  61]---> BDD-cost:   69
c ---[  60]---> BDD-cost:   69
c ---[  59]---> BDD-cost:   69
c ---[  58]---> BDD-cost:   69
c ---[  57]---> BDD-cost:   69
c ---[  56]---> BDD-cost:   69
c ---[  55]---> BDD-cost:   69
c ---[  54]---> BDD-cost:   69
c ---[  53]---> BDD-cost:   69
c ---[  52]---> BDD-cost:   69
c ---[  51]---> BDD-cost:   69
c ---[  50]---> BDD-cost:   69
c ---[  49]---> BDD-cost:   69
c ---[  48]---> BDD-cost:   69
c ---[  47]---> BDD-cost:   69
c ---[  46]---> BDD-cost:   69
c ---[  45]---> BDD-cost:   69
c ---[  44]---> BDD-cost:   69
c ---[  43]---> BDD-cost:   69
c ---[  42]---> BDD-cost:   69
c ---[  41]---> BDD-cost:   69
c ---[  40]---> BDD-cost:   69
c ---[  39]---> BDD-cost:   69
c ---[  38]---> BDD-cost:   69
c ---[  37]---> BDD-cost:   69
c ---[  36]---> BDD-cost:   69
c ---[  35]---> BDD-cost:   69
c ---[  34]---> BDD-cost:   69
c ---[  33]---> BDD-cost:   69
c ---[  32]---> BDD-cost:   69
c ---[  31]---> BDD-cost:   69
c ---[  30]---> BDD-cost:   69
c ---[  29]---> BDD-cost:   69
c ---[  28]---> BDD-cost:   69
c ---[  27]---> BDD-cost:   69
c ---[  26]---> BDD-cost:   69
c ---[  25]---> BDD-cost:   69
c ---[  24]---> BDD-cost:   69
c ---[  23]---> BDD-cost:   69
c ---[  22]---> BDD-cost:   69
c ---[  21]---> BDD-cost:   69
c ---[  20]---> BDD-cost:   69
c ---[  19]---> BDD-cost:   69
c ---[  18]---> BDD-cost:   69
c ---[  17]---> BDD-cost:   69
c ---[  16]---> BDD-cost:   69
c ---[  15]---> BDD-cost:   69
c ---[  14]---> BDD-cost:   69
c ---[  13]---> BDD-cost:   69
c ---[  12]---> BDD-cost:   69
c ---[  11]---> BDD-cost:   69
c ---[  10]---> BDD-cost:   69
c ---[   9]---> BDD-cost:   69
c ---[   8]---> BDD-cost:   69
c ---[   7]---> BDD-cost:   69
c ---[   6]---> BDD-cost:   69
c ---[   5]---> BDD-cost:   69
c ---[   4]---> BDD-cost:   69
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:   69
c ---[   1]---> BDD-cost:   69
c ---[   0]---> BDD-cost:   69
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21492    61880 |    7164       0        0     nan |  0.000 % |
c |       100 |   21232    61100 |    7880       7       14     2.0 |  1.673 % |
c |       250 |   20862    59990 |    8668      23       60     2.6 |  2.667 % |
c |       476 |   20532    59000 |    9535     106     8444    79.7 |  3.565 % |
c |       813 |   20367    58505 |   10488     374    43930   117.5 |  4.014 % |
c |      1325 |   20062    57590 |   11537     764   106520   139.4 |  4.844 % |
c |      2085 |   20022    57470 |   12691    1505   279260   185.6 |  4.952 % |
c |      3224 |   19327    55385 |   13960    2421   520946   215.2 |  6.857 % |
c |      4936 |   19027    54485 |   15356    3994   946569   237.0 |  7.660 % |
c |      7498 |   18240    52130 |   16892    6263  1549791   247.5 |  9.810 % |
c |     11343 |   16980    48350 |   18581    9651  2311400   239.5 | 13.238 % |
c |     17112 |   15247    43155 |   20439   14845  3572511   240.7 | 17.973 % |
c |     25762 |   13988    39380 |   22483   11792  2910674   246.8 | 21.388 % |
c |     38738 |   13329    37405 |   24732   24554  7169929   292.0 | 23.184 % |
c |     58199 |   12539    35035 |   27205   28145  9268835   329.3 | 25.333 % |
c |     87392 |   11843    32955 |   29925   22666  6830758   301.4 | 27.238 % |
c |    131181 |   11237    31145 |   32918   24105  7973909   330.8 | 28.898 % |
c |    196865 |   10858    30010 |   36210   16393  4924963   300.4 | 29.932 % |
c |    295391 |   10569    29145 |   39831   27643  7493269   271.1 | 30.721 % |
#### 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.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (runsolver) D 21302 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 366287461 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 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.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 1757 0 0 0 995 3 0 0 25 0 1 0 366287461 8769536 1734 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1734 603 41 0 2100 0
vsize: 8564
[startup+20.0012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 2292 0 0 0 1994 4 0 0 25 0 1 0 366287461 11059200 2269 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2700 2269 603 41 0 2659 0
vsize: 10800
[startup+30.0009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 2889 0 0 0 2993 6 0 0 25 0 1 0 366287461 13488128 2866 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3293 2866 603 41 0 3252 0
vsize: 13172
[startup+40.0007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 3157 0 0 0 3992 7 0 0 25 0 1 0 366287461 14614528 3134 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 3134 603 41 0 3527 0
vsize: 14272
[startup+50.0019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21303
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 3970 0 0 0 4990 9 0 0 25 0 1 0 366287461 17850368 3947 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4358 3947 603 41 0 4317 0
vsize: 17432
[startup+60.0022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 4383 0 0 0 5989 10 0 0 25 0 1 0 366287461 19603456 4360 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4786 4360 603 41 0 4745 0
vsize: 19144
[startup+70.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 4577 0 0 0 6989 11 0 0 25 0 1 0 366287461 20414464 4554 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4984 4554 603 41 0 4943 0
vsize: 19936
[startup+80.0028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 4777 0 0 0 7988 12 0 0 25 0 1 0 366287461 21229568 4754 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5183 4754 603 41 0 5142 0
vsize: 20732
[startup+90.0026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 4896 0 0 0 8988 12 0 0 25 0 1 0 366287461 21626880 4873 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5280 4873 603 41 0 5239 0
vsize: 21120
[startup+100.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 5160 0 0 0 9987 13 0 0 25 0 1 0 366287461 22708224 5137 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5544 5137 603 41 0 5503 0
vsize: 22176
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 5498 0 0 0 10986 14 0 0 25 0 1 0 366287461 24223744 5475 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5475 603 41 0 5873 0
vsize: 23656
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 5811 0 0 0 11985 15 0 0 25 0 1 0 366287461 25440256 5788 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6211 5788 603 41 0 6170 0
vsize: 24844
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 6376 0 0 0 12984 16 0 0 25 0 1 0 366287461 27725824 6353 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6769 6353 603 41 0 6728 0
vsize: 27076
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 7188 0 0 0 13982 18 0 0 25 0 1 0 366287461 31100928 7165 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 7165 603 41 0 7552 0
vsize: 30372
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 7230 0 0 0 14982 19 0 0 25 0 1 0 366287461 31236096 7207 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7207 603 41 0 7585 0
vsize: 30504
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 7230 0 0 0 15982 19 0 0 25 0 1 0 366287461 31236096 7207 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7626 7207 603 41 0 7585 0
vsize: 30504
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 7230 0 0 0 16982 19 0 0 25 0 1 0 366287461 31236096 7207 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7626 7207 603 41 0 7585 0
vsize: 30504
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 7960 0 0 0 17981 20 0 0 25 0 1 0 366287461 34213888 7937 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8353 7937 603 41 0 8312 0
vsize: 33412
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 8575 0 0 0 18980 22 0 0 25 0 1 0 366287461 36782080 8552 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8980 8552 603 41 0 8939 0
vsize: 35920
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 9913 0 0 0 19977 25 0 0 25 0 1 0 366287461 42172416 9890 4294967295 134512640 134672761 3221224544 3221223648 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10296 9890 603 41 0 10255 0
vsize: 41184
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 20977 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 21977 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 22977 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 23977 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 24977 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 10068 0 0 0 25978 25 0 0 25 0 1 0 366287461 42848256 10045 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10461 10045 603 41 0 10420 0
vsize: 41844
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11297 0 0 0 26974 28 0 0 25 0 1 0 366287461 47837184 11274 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11679 11274 603 41 0 11638 0
vsize: 46716
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 27974 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 28975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 29975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 30975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 31975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 32975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 33975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21305
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 34975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 35975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 36975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 11662 0 0 0 37975 29 0 0 25 0 1 0 366287461 49328128 11639 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12043 11639 603 41 0 12002 0
vsize: 48172
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 12068 0 0 0 38974 30 0 0 25 0 1 0 366287461 51085312 12045 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12472 12045 603 41 0 12431 0
vsize: 49888
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 12910 0 0 0 39973 32 0 0 25 0 1 0 366287461 54460416 12887 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13296 12887 603 41 0 13255 0
vsize: 53184
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 40972 33 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 41972 33 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 42972 33 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 43972 33 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 44972 34 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 13400 0 0 0 45972 34 0 0 25 0 1 0 366287461 56610816 13377 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13821 13377 603 41 0 13780 0
vsize: 55284
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 46970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223104 134565829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 47970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 48970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 49970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 50970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 51970 36 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 52970 37 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14006 0 0 0 53970 37 0 0 25 0 1 0 366287461 59174912 13983 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14447 13983 603 41 0 14406 0
vsize: 57788
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 14615 0 0 0 54969 38 0 0 25 0 1 0 366287461 61607936 14592 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15041 14592 603 41 0 15000 0
vsize: 60164
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15056 0 0 0 55968 39 0 0 25 0 1 0 366287461 63377408 15033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15473 15033 603 41 0 15432 0
vsize: 61892
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 56968 39 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 57968 39 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 58968 39 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 59968 39 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 60968 40 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 61968 40 0 0 25 0 1 0 366287461 63377408 15034 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15473 15034 603 41 0 15432 0
vsize: 61892
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 62969 40 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 63969 40 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21307
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 64969 40 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 65969 40 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 66969 40 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 67969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223648 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 68969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 69969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 70969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 71969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 72969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 73969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 74969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 75969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15057 0 0 0 76969 41 0 0 25 0 1 0 366287461 63152128 14983 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15418 14983 603 41 0 15377 0
vsize: 61672
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15284 0 0 0 77969 42 0 0 25 0 1 0 366287461 64090112 15210 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15647 15210 603 41 0 15606 0
vsize: 62588
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 15952 0 0 0 78967 44 0 0 25 0 1 0 366287461 66924544 15878 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16339 15878 603 41 0 16298 0
vsize: 65356
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 16951 0 0 0 79965 46 0 0 25 0 1 0 366287461 70975488 16877 4294967295 134512640 134672761 3221224544 3221223648 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17328 16877 603 41 0 17287 0
vsize: 69312
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 80965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 81965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223648 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 82965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223648 134559958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 83965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 84965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 85965 47 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 86965 48 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17088 0 0 0 87965 48 0 0 25 0 1 0 366287461 71512064 17014 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17459 17014 603 41 0 17418 0
vsize: 69836
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17416 0 0 0 88965 48 0 0 25 0 1 0 366287461 72859648 17342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17788 17342 603 41 0 17747 0
vsize: 71152
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17865 0 0 0 89963 49 0 0 25 0 1 0 366287461 74747904 17791 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17791 603 41 0 18208 0
vsize: 72996
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 90963 50 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223648 134559943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 91963 50 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 92963 50 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 93963 50 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+950.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21309
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 94963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 95963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 96963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 97963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 98963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 99963 51 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 100963 52 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17867 0 0 0 101963 52 0 0 25 0 1 0 366287461 74747904 17793 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17793 603 41 0 18208 0
vsize: 72996
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17869 0 0 0 102963 52 0 0 25 0 1 0 366287461 74747904 17795 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18249 17795 603 41 0 18208 0
vsize: 72996
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 103963 52 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 104963 52 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 105963 52 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 106964 52 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 107963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 108963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 109963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 110963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 111963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 112963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 113963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 114963 53 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 115963 54 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 116964 54 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 117964 54 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 118963 54 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 21311
Raw data (stat): 21303 (minisat+) R 21302 12452 12451 0 -1 0 17870 0 0 0 119963 54 0 0 25 0 1 0 366287461 74698752 17796 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18237 17796 603 41 0 18196 0
vsize: 72948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 21311
Raw data (stat): 21303 (minisat+) Z 21302 12452 12451 0 -1 12 17872 0 0 0 119963 57 0 0 25 0 1 0 366287461 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.64
CPU system time (s): 0.579911
CPU usage (%): 100.013
Max. virtual memory (Kb): 72996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####