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-chnl15_20_pb.cnf.cr.opb
MD5SUMce39bf71367df072c91f9b7587480c93
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 21
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.017996
Number of variables600
Total number of constraints70
Number of constraints which are clauses40
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint20

Trace number 5324 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-13 23:27:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3766 boxname=wulflinc17 idbench=6 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ce39bf71367df072c91f9b7587480c93  /oldhome/oroussel/tmp/wulflinc17/normalized-chnl15_20_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-chnl15_20_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc17/normalized-chnl15_20_pb.cnf.cr.opb
IDLAUNCH: 3766
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        829112 kB
Buffers:         34436 kB
Cached:         136384 kB
SwapCached:       2376 kB
Active:          57460 kB
Inactive:       118676 kB
HighTotal:      131008 kB
HighFree:         1820 kB
LowTotal:       903652 kB
LowFree:        827292 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23612 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:47:09 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3766 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 70 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    2770     7710 |     830       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1680          
c   -- var.elim.:  1680/1680          
c   -- var.elim.:  716/716          
c   -- var.elim.:  136/136          
c   -- subsuming                       
c   -- var.elim.:  466/466          
c   -- var.elim.:  280/280          
c   -- var.elim.:  104/104          
c   -- var.elim.:  102/102          
c   -- var.elim.:  58/58          
c   -- var.elim.:  50/50          
c   -- var.elim.:  52/52          
c   -- var.elim.:  54/54          
c   -- var.elim.:  56/56          
c   -- var.elim.:  58/58          
c   -- var.elim.:  60/60          
c   -- var.elim.:  62/62          
c   -- var.elim.:  64/64          
c   -- var.elim.:  66/66          
c   -- var.elim.:  68/68          
c   -- var.elim.:  144/144          
c   -- subsuming                       
c   -- var.elim.:  674/674          
c   -- var.elim.:  594/594          
c   -- var.elim.:  130/130          
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  106/106          
c   -- var.elim.:  20/20          
c |         0 |    2346     9136 |      --       0       --      -- |     --   | -424/1516
c |         0 |    2346     9136 |     938       0        0     nan |  0.000 % |
c |       100 |    2346     9136 |    1032     100     5088    50.9 |  2.168 % |
c |       253 |    2346     9136 |    1135     253    13047    51.6 |  2.168 % |
c |       480 |    2346     9136 |    1249     480    28272    58.9 |  2.169 % |
c |       817 |    2346     9136 |    1373     817    52967    64.8 |  2.170 % |
c |      1323 |    2346     9136 |    1511    1323    95584    72.2 |  2.168 % |
c |      2083 |    2346     9136 |    1662    1449   117004    80.7 |  2.169 % |
c |      3223 |    2346     9136 |    1828    1881   152365    81.0 |  2.168 % |
c |      4933 |    2346     9136 |    2011    2196   138215    62.9 |  2.168 % |
c |      7495 |    2346     9136 |    2212    1662   159608    96.0 |  2.168 % |
c |     11339 |    2346     9136 |    2433    2156   210463    97.6 |  2.168 % |
c |     17106 |    2346     9136 |    2677    2238   138854    62.0 |  2.168 % |
c |     25755 |    2346     9136 |    2945    2784   347379   124.8 |  2.168 % |
c |     38732 |    2346     9136 |    3239    2739   330951   120.8 |  2.168 % |
c |     58196 |    2346     9136 |    3563    3326   330306    99.3 |  2.168 % |
c |     87394 |    2346     9136 |    3919    2833   322373   113.8 |  2.168 % |
c |    131184 |    2346     9136 |    4311#### 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.98 0.91 2/55 26297
Raw data (stat): 26297 (runsolver) R 26296 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479911572 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99945 s]
Raw data (loadavg): 0.94 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1041 0 0 0 996 2 0 0 25 0 1 0 479911572 5722112 1019 4294967295 134512640 134672761 3221224544 3221223640 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1397 1019 603 41 0 1356 0
vsize: 5588
[startup+20.0003 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1184 0 0 0 1996 2 0 0 25 0 1 0 479911572 6381568 1162 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1558 1162 603 41 0 1517 0
vsize: 6232
[startup+29.9999 s]
Raw data (loadavg): 0.95 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1187 0 0 0 2996 2 0 0 25 0 1 0 479911572 6381568 1165 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1558 1165 603 41 0 1517 0
vsize: 6232
[startup+40.0002 s]
Raw data (loadavg): 0.96 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1254 0 0 0 3996 3 0 0 25 0 1 0 479911572 6639616 1232 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1621 1232 603 41 0 1580 0
vsize: 6484
[startup+50.0001 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1312 0 0 0 4996 3 0 0 25 0 1 0 479911572 6909952 1290 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1687 1290 603 41 0 1646 0
vsize: 6748
[startup+59.9997 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1443 0 0 0 5995 3 0 0 25 0 1 0 479911572 7426048 1421 4294967295 134512640 134672761 3221224544 3221223640 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1813 1421 603 41 0 1772 0
vsize: 7252
[startup+70 s]
Raw data (loadavg): 0.97 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1469 0 0 0 6996 3 0 0 25 0 1 0 479911572 7548928 1447 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1843 1447 603 41 0 1802 0
vsize: 7372
[startup+79.9999 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1469 0 0 0 7996 3 0 0 25 0 1 0 479911572 7548928 1447 4294967295 134512640 134672761 3221224544 3221223536 134542705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1843 1447 603 41 0 1802 0
vsize: 7372
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1473 0 0 0 8996 3 0 0 25 0 1 0 479911572 7548928 1451 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1843 1451 603 41 0 1802 0
vsize: 7372
[startup+99.9999 s]
Raw data (loadavg): 0.98 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1496 0 0 0 9996 3 0 0 25 0 1 0 479911572 7667712 1474 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1872 1474 603 41 0 1831 0
vsize: 7488
[startup+110 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1537 0 0 0 10996 3 0 0 25 0 1 0 479911572 7798784 1515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1904 1515 603 41 0 1863 0
vsize: 7616
[startup+120 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1562 0 0 0 11996 3 0 0 25 0 1 0 479911572 7917568 1540 4294967295 134512640 134672761 3221224544 3221223728 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1933 1540 603 41 0 1892 0
vsize: 7732
[startup+130 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1572 0 0 0 12996 3 0 0 25 0 1 0 479911572 7917568 1550 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1933 1550 603 41 0 1892 0
vsize: 7732
[startup+140.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1604 0 0 0 13996 3 0 0 25 0 1 0 479911572 8146944 1582 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1989 1582 603 41 0 1948 0
vsize: 7956
[startup+150.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1741 0 0 0 14997 4 0 0 25 0 1 0 479911572 8675328 1719 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2118 1719 603 41 0 2077 0
vsize: 8472
[startup+160 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1775 0 0 0 15997 4 0 0 25 0 1 0 479911572 8781824 1753 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2144 1753 603 41 0 2103 0
vsize: 8576
[startup+170.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1839 0 0 0 16996 4 0 0 25 0 1 0 479911572 9043968 1817 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2208 1817 603 41 0 2167 0
vsize: 8832
[startup+180.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1853 0 0 0 17997 4 0 0 25 0 1 0 479911572 9175040 1831 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1831 603 41 0 2199 0
vsize: 8960
[startup+190.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1859 0 0 0 18997 4 0 0 25 0 1 0 479911572 9175040 1837 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2240 1837 603 41 0 2199 0
vsize: 8960
[startup+200.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26297
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1928 0 0 0 19997 4 0 0 25 0 1 0 479911572 9433088 1906 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2303 1906 603 41 0 2262 0
vsize: 9212
[startup+210.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1935 0 0 0 20997 4 0 0 25 0 1 0 479911572 9433088 1913 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2303 1913 603 41 0 2262 0
vsize: 9212
[startup+220.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1981 0 0 0 21997 4 0 0 25 0 1 0 479911572 9682944 1959 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1959 603 41 0 2323 0
vsize: 9456
[startup+230.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 1982 0 0 0 22997 4 0 0 25 0 1 0 479911572 9682944 1960 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2364 1960 603 41 0 2323 0
vsize: 9456
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2013 0 0 0 23997 4 0 0 25 0 1 0 479911572 9805824 1991 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1991 603 41 0 2353 0
vsize: 9576
[startup+250.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2017 0 0 0 24998 4 0 0 25 0 1 0 479911572 9805824 1995 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1995 603 41 0 2353 0
vsize: 9576
[startup+260.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2021 0 0 0 25998 4 0 0 25 0 1 0 479911572 9805824 1999 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2394 1999 603 41 0 2353 0
vsize: 9576
[startup+270.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2038 0 0 0 26998 5 0 0 25 0 1 0 479911572 9908224 2016 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2419 2016 603 41 0 2378 0
vsize: 9676
[startup+280.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2114 0 0 0 27998 5 0 0 25 0 1 0 479911572 10170368 2092 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2483 2092 603 41 0 2442 0
vsize: 9932
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2114 0 0 0 28998 5 0 0 25 0 1 0 479911572 10170368 2092 4294967295 134512640 134672761 3221224544 3221222096 134645642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2483 2092 603 41 0 2442 0
vsize: 9932
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2181 0 0 0 29998 5 0 0 25 0 1 0 479911572 10534912 2159 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2159 603 41 0 2531 0
vsize: 10288
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2181 0 0 0 30998 5 0 0 25 0 1 0 479911572 10534912 2159 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2159 603 41 0 2531 0
vsize: 10288
[startup+320.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2184 0 0 0 31999 5 0 0 25 0 1 0 479911572 10534912 2162 4294967295 134512640 134672761 3221224544 3221223536 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2162 603 41 0 2531 0
vsize: 10288
[startup+330.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2184 0 0 0 32999 5 0 0 25 0 1 0 479911572 10534912 2162 4294967295 134512640 134672761 3221224544 3221223584 134603536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2162 603 41 0 2531 0
vsize: 10288
[startup+340.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2193 0 0 0 33999 5 0 0 25 0 1 0 479911572 10534912 2171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2171 603 41 0 2531 0
vsize: 10288
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2193 0 0 0 34999 5 0 0 25 0 1 0 479911572 10534912 2171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2171 603 41 0 2531 0
vsize: 10288
[startup+360.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2193 0 0 0 35999 5 0 0 25 0 1 0 479911572 10534912 2171 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2171 603 41 0 2531 0
vsize: 10288
[startup+370.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2194 0 0 0 37000 5 0 0 25 0 1 0 479911572 10534912 2172 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2172 603 41 0 2531 0
vsize: 10288
[startup+380.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2196 0 0 0 38000 5 0 0 25 0 1 0 479911572 10534912 2174 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2174 603 41 0 2531 0
vsize: 10288
[startup+390.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2197 0 0 0 39000 5 0 0 25 0 1 0 479911572 10534912 2175 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2572 2175 603 41 0 2531 0
vsize: 10288
[startup+400.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2281 0 0 0 40000 5 0 0 25 0 1 0 479911572 10928128 2259 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2668 2259 603 41 0 2627 0
vsize: 10672
[startup+410.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2281 0 0 0 41000 5 0 0 25 0 1 0 479911572 10924032 2259 4294967295 134512640 134672761 3221224544 3221223584 134612682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2667 2259 603 41 0 2626 0
vsize: 10668
[startup+420.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2298 0 0 0 42001 5 0 0 25 0 1 0 479911572 10924032 2276 4294967295 134512640 134672761 3221224544 3221223552 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2667 2276 603 41 0 2626 0
vsize: 10668
[startup+430.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2298 0 0 0 43001 5 0 0 25 0 1 0 479911572 10924032 2276 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2667 2276 603 41 0 2626 0
vsize: 10668
[startup+440.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2307 0 0 0 44001 5 0 0 25 0 1 0 479911572 11038720 2285 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2285 603 41 0 2654 0
vsize: 10780
[startup+450.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2313 0 0 0 45001 5 0 0 25 0 1 0 479911572 11038720 2291 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2291 603 41 0 2654 0
vsize: 10780
[startup+460.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 46001 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+470.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 47001 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+480.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 48002 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+490.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 49002 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+500.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26299
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 50002 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+510.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2320 0 0 0 51002 5 0 0 25 0 1 0 479911572 11038720 2298 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2695 2298 603 41 0 2654 0
vsize: 10780
[startup+520.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2354 0 0 0 52002 5 0 0 25 0 1 0 479911572 11149312 2332 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2722 2332 603 41 0 2681 0
vsize: 10888
[startup+530.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2366 0 0 0 53002 5 0 0 25 0 1 0 479911572 11268096 2344 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2344 603 41 0 2710 0
vsize: 11004
[startup+540.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 54003 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+550.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 55003 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+560.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 56003 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+570.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 57003 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+580.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 58003 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+590.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2373 0 0 0 59004 5 0 0 25 0 1 0 479911572 11268096 2351 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2751 2351 603 41 0 2710 0
vsize: 11004
[startup+600.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 60003 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+610.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 61004 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+620.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 62004 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+630.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 63004 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+640.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 64004 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223600 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+650.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2417 0 0 0 65005 6 0 0 25 0 1 0 479911572 11501568 2395 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2808 2395 603 41 0 2767 0
vsize: 11232
[startup+660.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2540 0 0 0 66004 6 0 0 25 0 1 0 479911572 12005376 2518 4294967295 134512640 134672761 3221224544 3221223584 134613745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2931 2518 603 41 0 2890 0
vsize: 11724
[startup+670.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2563 0 0 0 67005 6 0 0 25 0 1 0 479911572 12005376 2541 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2931 2541 603 41 0 2890 0
vsize: 11724
[startup+680.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2576 0 0 0 68005 6 0 0 25 0 1 0 479911572 12136448 2554 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2963 2554 603 41 0 2922 0
vsize: 11852
[startup+690.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2581 0 0 0 69005 6 0 0 25 0 1 0 479911572 12136448 2559 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2963 2559 603 41 0 2922 0
vsize: 11852
[startup+700.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2582 0 0 0 70005 6 0 0 25 0 1 0 479911572 12136448 2560 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2963 2560 603 41 0 2922 0
vsize: 11852
[startup+710.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2592 0 0 0 71005 6 0 0 25 0 1 0 479911572 12136448 2570 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2963 2570 603 41 0 2922 0
vsize: 11852
[startup+720.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2599 0 0 0 72006 6 0 0 25 0 1 0 479911572 12255232 2577 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2577 603 41 0 2951 0
vsize: 11968
[startup+730.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2599 0 0 0 73006 6 0 0 25 0 1 0 479911572 12255232 2577 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2577 603 41 0 2951 0
vsize: 11968
[startup+740.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2599 0 0 0 74006 6 0 0 25 0 1 0 479911572 12255232 2577 4294967295 134512640 134672761 3221224544 3221223584 134614223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2577 603 41 0 2951 0
vsize: 11968
[startup+750.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2599 0 0 0 75006 6 0 0 25 0 1 0 479911572 12255232 2577 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2577 603 41 0 2951 0
vsize: 11968
[startup+760.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2599 0 0 0 76006 6 0 0 25 0 1 0 479911572 12255232 2577 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2577 603 41 0 2951 0
vsize: 11968
[startup+770.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2600 0 0 0 77006 6 0 0 25 0 1 0 479911572 12255232 2578 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2992 2578 603 41 0 2951 0
vsize: 11968
[startup+780.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2643 0 0 0 78007 6 0 0 25 0 1 0 479911572 12386304 2621 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3024 2621 603 41 0 2983 0
vsize: 12096
[startup+790.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2643 0 0 0 79007 6 0 0 25 0 1 0 479911572 12386304 2621 4294967295 134512640 134672761 3221224544 3221223668 134566073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3024 2621 603 41 0 2983 0
vsize: 12096
[startup+800.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26301
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2643 0 0 0 80007 6 0 0 25 0 1 0 479911572 12386304 2621 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3024 2621 603 41 0 2983 0
vsize: 12096
[startup+810.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2662 0 0 0 81007 6 0 0 25 0 1 0 479911572 12513280 2640 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2640 603 41 0 3014 0
vsize: 12220
[startup+820.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2671 0 0 0 82007 6 0 0 25 0 1 0 479911572 12513280 2649 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2649 603 41 0 3014 0
vsize: 12220
[startup+830.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2692 0 0 0 83007 6 0 0 25 0 1 0 479911572 12627968 2670 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2670 603 41 0 3042 0
vsize: 12332
[startup+840.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2692 0 0 0 84008 6 0 0 25 0 1 0 479911572 12627968 2670 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2670 603 41 0 3042 0
vsize: 12332
[startup+850.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2699 0 0 0 85008 6 0 0 25 0 1 0 479911572 12627968 2677 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2677 603 41 0 3042 0
vsize: 12332
[startup+860.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2699 0 0 0 86008 6 0 0 25 0 1 0 479911572 12627968 2677 4294967295 134512640 134672761 3221224544 3221223584 134603517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2677 603 41 0 3042 0
vsize: 12332
[startup+870.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2700 0 0 0 87008 6 0 0 25 0 1 0 479911572 12627968 2678 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2678 603 41 0 3042 0
vsize: 12332
[startup+880.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2700 0 0 0 88008 6 0 0 25 0 1 0 479911572 12627968 2678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2678 603 41 0 3042 0
vsize: 12332
[startup+890.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2700 0 0 0 89009 6 0 0 25 0 1 0 479911572 12627968 2678 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2678 603 41 0 3042 0
vsize: 12332
[startup+900.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2700 0 0 0 90009 6 0 0 25 0 1 0 479911572 12627968 2678 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2678 603 41 0 3042 0
vsize: 12332
[startup+910.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2700 0 0 0 91009 6 0 0 25 0 1 0 479911572 12627968 2678 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2678 603 41 0 3042 0
vsize: 12332
[startup+920.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 92009 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+930.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 93009 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+940.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 94010 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+950.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 95010 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+960.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 96010 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+970.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 97010 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+980.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 98010 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+990.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 99011 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 100011 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 101011 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 102011 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 103011 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 104012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 105012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 106012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 107012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 108012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223584 134612625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 109012 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26303
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 110013 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2701 0 0 0 111013 6 0 0 25 0 1 0 479911572 12627968 2679 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3083 2679 603 41 0 3042 0
vsize: 12332
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2745 0 0 0 112013 7 0 0 25 0 1 0 479911572 12763136 2723 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2723 603 41 0 3075 0
vsize: 12464
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2750 0 0 0 113013 7 0 0 25 0 1 0 479911572 12763136 2728 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2728 603 41 0 3075 0
vsize: 12464
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2750 0 0 0 114013 7 0 0 25 0 1 0 479911572 12763136 2728 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2728 603 41 0 3075 0
vsize: 12464
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2750 0 0 0 115013 7 0 0 25 0 1 0 479911572 12763136 2728 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2728 603 41 0 3075 0
vsize: 12464
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2750 0 0 0 116013 7 0 0 25 0 1 0 479911572 12763136 2728 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3116 2728 603 41 0 3075 0
vsize: 12464
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2780 0 0 0 117014 7 0 0 25 0 1 0 479911572 12890112 2758 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3147 2758 603 41 0 3106 0
vsize: 12588
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2798 0 0 0 118014 7 0 0 25 0 1 0 479911572 13021184 2776 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2776 603 41 0 3138 0
vsize: 12716
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2799 0 0 0 119014 7 0 0 25 0 1 0 479911572 13021184 2777 4294967295 134512640 134672761 3221224544 3221223640 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2777 603 41 0 3138 0
vsize: 12716
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/55 26305
Raw data (stat): 26297 (minisat+) R 26296 20838 20837 0 -1 0 2803 0 0 0 120014 7 0 0 25 0 1 0 479911572 13021184 2781 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3179 2781 603 41 0 3138 0
vsize: 12716
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.91 1/55 26305
Raw data (stat): 26297 (minisat+) Z 26296 20838 20837 0 -1 12 2803 0 0 0 120014 7 0 0 25 0 1 0 479911572 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.02
CPU time (s): 1200.23
CPU user time (s): 1200.15
CPU system time (s): 0.078987
CPU usage (%): 100.017
Max. virtual memory (Kb): 12716
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####