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_16_pb.cnf.cr.opb
MD5SUM3f8902c4e8af50006f671e2bddb3e9aa
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 17
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.013997
Number of variables480
Total number of constraints62
Number of constraints which are clauses32
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 constraint16

Trace number 5322 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 23:26:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3765 boxname=wulflinc13 idbench=5 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3f8902c4e8af50006f671e2bddb3e9aa  /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-chnl15_16_pb.cnf.cr.opb
IDLAUNCH: 3765
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907348 kB
Buffers:         34600 kB
Cached:          73196 kB
SwapCached:        392 kB
Active:          53272 kB
Inactive:        57796 kB
HighTotal:      131008 kB
HighFree:        53928 kB
LowTotal:       903652 kB
LowFree:        853420 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10652 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:46:30 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 3765 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 62 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................
c ---[  29]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  27]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  25]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  19]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  17]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  15]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   29
c ---[  12]---> BDD-cost:   29
c ---[  11]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   8]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   6]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   4]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost:   29
c ---[   1]---> BDD-cost:   29
c ---[   0]---> BDD-cost:   29
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    2162     6030 |     648       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1320          
c   -- var.elim.:  1320/1320          
c   -- var.elim.:  592/592          
c   -- var.elim.:  136/136          
c   -- subsuming                       
c   -- var.elim.:  398/398          
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.:  136/136          
c   -- subsuming                       
c   -- var.elim.:  550/550          
c   -- var.elim.:  474/474          
c   -- var.elim.:  122/122          
c   -- subsuming                       
c   -- var.elim.:  222/222          
c   -- var.elim.:  106/106          
c   -- var.elim.:  20/20          
c |         0 |    1778     7024 |      --       0       --      -- |     --   | -384/1084
c |         0 |    1778     7024 |     711       0        0     nan |  0.000 % |
c |       101 |    1778     7024 |     782     101     5283    52.3 |  2.841 % |
c |       255 |    1778     7024 |     860     255    13775    54.0 |  2.841 % |
c |       481 |    1778     7024 |     946     481    27187    56.5 |  2.841 % |
c |       818 |    1778     7024 |    1041     818    48481    59.3 |  2.841 % |
c |      1327 |    1778     7024 |    1145    1327    81896    61.7 |  2.841 % |
c |      2086 |    1778     7024 |    1259    1126    74705    66.3 |  2.841 % |
c |      3225 |    1778     7024 |    1385    1182    86787    73.4 |  2.841 % |
c |      4933 |    1778     7024 |    1524    1239   107657    86.9 |  2.841 % |
c |      7497 |    1778     7024 |    1676    1408   140052    99.5 |  2.841 % |
c |     11343 |    1778     7024 |    1844    1903   162058    85.2 |  2.841 % |
c |     17110 |    1778     7024 |    2029    2080   203938    98.0 |  2.842 % |
c |     25761 |    1778     7024 |    2232    1716   162311    94.6 |  2.841 % |
c |     38737 |    1778     7024 |    2455    2281   238229   104.4 |  2.841 % |
c |     58198 |    1778     7024 |    2700    2640   263793    99.9 |  2.841 % |
c |     87392 |    1778     7024 |    2970    2217   241731   109.0 |  2.841 % |
c |    131184 |    1778     7024 |    3267    2962   287620    97.1 |  2.841 % |
c |    196870 |    1778     7024 |    3594    2453   248730   101.4 |  2.841 % |
c |    295398 |    1778     #### 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.86 0.93 0.90 2/54 3691
Raw data (stat): 3691 (runsolver) R 3690 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421682725 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 876 0 0 0 997 1 0 0 25 0 1 0 421682725 5062656 854 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1236 854 603 41 0 1195 0
vsize: 4944
[startup+20 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 954 0 0 0 1996 2 0 0 25 0 1 0 421682725 5324800 932 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1300 932 603 41 0 1259 0
vsize: 5200
[startup+30.0003 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1030 0 0 0 2996 2 0 0 25 0 1 0 421682725 5713920 1008 4294967295 134512640 134672761 3221224544 3221223584 134612835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1395 1008 603 41 0 1354 0
vsize: 5580
[startup+39.9999 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1056 0 0 0 3995 2 0 0 25 0 1 0 421682725 5832704 1034 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1424 1034 603 41 0 1383 0
vsize: 5696
[startup+50.001 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1126 0 0 0 4995 3 0 0 25 0 1 0 421682725 6098944 1104 4294967295 134512640 134672761 3221224544 3221223584 134612885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1489 1104 603 41 0 1448 0
vsize: 5956
[startup+60.0012 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1140 0 0 0 5995 3 0 0 25 0 1 0 421682725 6098944 1118 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1489 1118 603 41 0 1448 0
vsize: 5956
[startup+70.0009 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 6994 3 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1555 1180 603 41 0 1514 0
vsize: 6220
[startup+80.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 7994 4 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223584 134603529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1555 1180 603 41 0 1514 0
vsize: 6220
[startup+90.0012 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1202 0 0 0 8993 5 0 0 25 0 1 0 421682725 6369280 1180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1555 1180 603 41 0 1514 0
vsize: 6220
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1262 0 0 0 9993 5 0 0 25 0 1 0 421682725 6635520 1240 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1620 1240 603 41 0 1579 0
vsize: 6480
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1272 0 0 0 10993 5 0 0 25 0 1 0 421682725 6635520 1250 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1620 1250 603 41 0 1579 0
vsize: 6480
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1287 0 0 0 11992 5 0 0 25 0 1 0 421682725 6758400 1265 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1650 1265 603 41 0 1609 0
vsize: 6600
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1298 0 0 0 12992 5 0 0 25 0 1 0 421682725 6758400 1276 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1650 1276 603 41 0 1609 0
vsize: 6600
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1325 0 0 0 13992 6 0 0 25 0 1 0 421682725 6885376 1303 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1681 1303 603 41 0 1640 0
vsize: 6724
[startup+150.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 14991 6 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1406 603 41 0 1735 0
vsize: 7104
[startup+160.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 15991 6 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223408 1075349796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1406 603 41 0 1735 0
vsize: 7104
[startup+170.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 16991 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1406 603 41 0 1735 0
vsize: 7104
[startup+180.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 17990 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1406 603 41 0 1735 0
vsize: 7104
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1428 0 0 0 18990 7 0 0 25 0 1 0 421682725 7274496 1406 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1776 1406 603 41 0 1735 0
vsize: 7104
[startup+200.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1432 0 0 0 19990 7 0 0 25 0 1 0 421682725 7401472 1410 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1410 603 41 0 1766 0
vsize: 7228
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1493 0 0 0 20989 8 0 0 25 0 1 0 421682725 7659520 1471 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1870 1471 603 41 0 1829 0
vsize: 7480
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1535 0 0 0 21989 8 0 0 25 0 1 0 421682725 7790592 1513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1902 1513 603 41 0 1861 0
vsize: 7608
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1564 0 0 0 22990 8 0 0 25 0 1 0 421682725 7921664 1542 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1934 1542 603 41 0 1893 0
vsize: 7736
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1583 0 0 0 23990 8 0 0 25 0 1 0 421682725 8011776 1561 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1956 1561 603 41 0 1915 0
vsize: 7824
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1604 0 0 0 24990 8 0 0 25 0 1 0 421682725 8134656 1582 4294967295 134512640 134672761 3221224544 3221223600 134644275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1582 603 41 0 1945 0
vsize: 7944
[startup+260.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1608 0 0 0 25990 8 0 0 25 0 1 0 421682725 8134656 1586 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1586 603 41 0 1945 0
vsize: 7944
[startup+270.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1608 0 0 0 26990 8 0 0 25 0 1 0 421682725 8134656 1586 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1586 603 41 0 1945 0
vsize: 7944
[startup+280.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1612 0 0 0 27990 8 0 0 25 0 1 0 421682725 8134656 1590 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1590 603 41 0 1945 0
vsize: 7944
[startup+290.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 28990 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1594 603 41 0 1945 0
vsize: 7944
[startup+300.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 29990 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1594 603 41 0 1945 0
vsize: 7944
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1616 0 0 0 30991 8 0 0 25 0 1 0 421682725 8134656 1594 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1986 1594 603 41 0 1945 0
vsize: 7944
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1668 0 0 0 31991 8 0 0 25 0 1 0 421682725 8392704 1646 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1646 603 41 0 2008 0
vsize: 8196
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1676 0 0 0 32991 8 0 0 25 0 1 0 421682725 8392704 1654 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1654 603 41 0 2008 0
vsize: 8196
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1680 0 0 0 33991 8 0 0 25 0 1 0 421682725 8392704 1658 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2049 1658 603 41 0 2008 0
vsize: 8196
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1696 0 0 0 34991 8 0 0 25 0 1 0 421682725 8507392 1674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1674 603 41 0 2036 0
vsize: 8308
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1707 0 0 0 35991 8 0 0 25 0 1 0 421682725 8507392 1685 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1685 603 41 0 2036 0
vsize: 8308
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1711 0 0 0 36992 8 0 0 25 0 1 0 421682725 8507392 1689 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2077 1689 603 41 0 2036 0
vsize: 8308
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 37992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1702 603 41 0 2064 0
vsize: 8420
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 38992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1702 603 41 0 2064 0
vsize: 8420
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 39992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223640 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1702 603 41 0 2064 0
vsize: 8420
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1724 0 0 0 40992 8 0 0 25 0 1 0 421682725 8622080 1702 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1702 603 41 0 2064 0
vsize: 8420
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1727 0 0 0 41992 8 0 0 25 0 1 0 421682725 8622080 1705 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1705 603 41 0 2064 0
vsize: 8420
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 42993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1709 603 41 0 2064 0
vsize: 8420
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 43993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1709 603 41 0 2064 0
vsize: 8420
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 44993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1709 603 41 0 2064 0
vsize: 8420
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 45993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1709 603 41 0 2064 0
vsize: 8420
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1731 0 0 0 46993 8 0 0 25 0 1 0 421682725 8622080 1709 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1709 603 41 0 2064 0
vsize: 8420
[startup+480.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1743 0 0 0 47993 8 0 0 25 0 1 0 421682725 8622080 1721 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1721 603 41 0 2064 0
vsize: 8420
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1744 0 0 0 48993 8 0 0 25 0 1 0 421682725 8622080 1722 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1722 603 41 0 2064 0
vsize: 8420
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1763 0 0 0 49993 8 0 0 25 0 1 0 421682725 8769536 1741 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1741 603 41 0 2100 0
vsize: 8564
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1784 0 0 0 50994 8 0 0 25 0 1 0 421682725 8769536 1762 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1762 603 41 0 2100 0
vsize: 8564
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 51994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2169 1778 603 41 0 2128 0
vsize: 8676
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 52994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2169 1778 603 41 0 2128 0
vsize: 8676
[startup+540.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1800 0 0 0 53994 8 0 0 25 0 1 0 421682725 8884224 1778 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2169 1778 603 41 0 2128 0
vsize: 8676
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1801 0 0 0 54994 8 0 0 25 0 1 0 421682725 8884224 1779 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2169 1779 603 41 0 2128 0
vsize: 8676
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1819 0 0 0 55994 9 0 0 25 0 1 0 421682725 9015296 1797 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1797 603 41 0 2160 0
vsize: 8804
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1824 0 0 0 56994 9 0 0 25 0 1 0 421682725 9015296 1802 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1802 603 41 0 2160 0
vsize: 8804
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1828 0 0 0 57995 9 0 0 25 0 1 0 421682725 9015296 1806 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1806 603 41 0 2160 0
vsize: 8804
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1832 0 0 0 58995 9 0 0 25 0 1 0 421682725 9015296 1810 4294967295 134512640 134672761 3221224544 3221223728 134616006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1810 603 41 0 2160 0
vsize: 8804
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1844 0 0 0 59995 9 0 0 25 0 1 0 421682725 9015296 1822 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1822 603 41 0 2160 0
vsize: 8804
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1844 0 0 0 60995 9 0 0 25 0 1 0 421682725 9015296 1822 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2201 1822 603 41 0 2160 0
vsize: 8804
[startup+620.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1848 0 0 0 61995 9 0 0 25 0 1 0 421682725 9129984 1826 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1826 603 41 0 2188 0
vsize: 8916
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1848 0 0 0 62995 9 0 0 25 0 1 0 421682725 9129984 1826 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1826 603 41 0 2188 0
vsize: 8916
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1852 0 0 0 63996 9 0 0 25 0 1 0 421682725 9129984 1830 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1830 603 41 0 2188 0
vsize: 8916
[startup+650.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1856 0 0 0 64996 9 0 0 25 0 1 0 421682725 9129984 1834 4294967295 134512640 134672761 3221224544 3221223640 134616356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1834 603 41 0 2188 0
vsize: 8916
[startup+660.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1860 0 0 0 65996 9 0 0 25 0 1 0 421682725 9129984 1838 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1838 603 41 0 2188 0
vsize: 8916
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1868 0 0 0 66996 9 0 0 25 0 1 0 421682725 9129984 1846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1846 603 41 0 2188 0
vsize: 8916
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1872 0 0 0 67996 9 0 0 25 0 1 0 421682725 9129984 1850 4294967295 134512640 134672761 3221224544 3221223708 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2229 1850 603 41 0 2188 0
vsize: 8916
[startup+690.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 68996 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1855 603 41 0 2216 0
vsize: 9028
[startup+700.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 69997 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1855 603 41 0 2216 0
vsize: 9028
[startup+710.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1877 0 0 0 70997 9 0 0 25 0 1 0 421682725 9244672 1855 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1855 603 41 0 2216 0
vsize: 9028
[startup+720.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1880 0 0 0 71997 9 0 0 25 0 1 0 421682725 9244672 1858 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1858 603 41 0 2216 0
vsize: 9028
[startup+730.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 1880 0 0 0 72997 9 0 0 25 0 1 0 421682725 9244672 1858 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2257 1858 603 41 0 2216 0
vsize: 9028
[startup+740.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2002 0 0 0 73997 9 0 0 25 0 1 0 421682725 9740288 1980 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2378 1980 603 41 0 2337 0
vsize: 9512
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2090 0 0 0 74997 10 0 0 25 0 1 0 421682725 10121216 2068 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2471 2068 603 41 0 2430 0
vsize: 9884
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2119 0 0 0 75997 10 0 0 25 0 1 0 421682725 10248192 2097 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2502 2097 603 41 0 2461 0
vsize: 10008
[startup+770.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2273 0 0 0 76996 10 0 0 25 0 1 0 421682725 10891264 2251 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2659 2251 603 41 0 2618 0
vsize: 10636
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2275 0 0 0 77997 10 0 0 25 0 1 0 421682725 10883072 2253 4294967295 134512640 134672761 3221224544 3221223584 134612880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2657 2253 603 41 0 2616 0
vsize: 10628
[startup+790.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2286 0 0 0 78997 10 0 0 25 0 1 0 421682725 10883072 2264 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2657 2264 603 41 0 2616 0
vsize: 10628
[startup+800.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2286 0 0 0 79997 10 0 0 25 0 1 0 421682725 10883072 2264 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2657 2264 603 41 0 2616 0
vsize: 10628
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2290 0 0 0 80997 10 0 0 25 0 1 0 421682725 10883072 2268 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2657 2268 603 41 0 2616 0
vsize: 10628
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2299 0 0 0 81997 10 0 0 25 0 1 0 421682725 10997760 2277 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2685 2277 603 41 0 2644 0
vsize: 10740
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2314 0 0 0 82998 10 0 0 25 0 1 0 421682725 10997760 2292 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2685 2292 603 41 0 2644 0
vsize: 10740
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2333 0 0 0 83998 10 0 0 25 0 1 0 421682725 11108352 2311 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2712 2311 603 41 0 2671 0
vsize: 10848
[startup+850.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2337 0 0 0 84998 10 0 0 25 0 1 0 421682725 11108352 2315 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2712 2315 603 41 0 2671 0
vsize: 10848
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2372 0 0 0 85998 10 0 0 25 0 1 0 421682725 11247616 2350 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2746 2350 603 41 0 2705 0
vsize: 10984
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2389 0 0 0 86998 10 0 0 25 0 1 0 421682725 11350016 2367 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2367 603 41 0 2730 0
vsize: 11084
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2402 0 0 0 87998 10 0 0 25 0 1 0 421682725 11350016 2380 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2380 603 41 0 2730 0
vsize: 11084
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2402 0 0 0 88999 10 0 0 25 0 1 0 421682725 11350016 2380 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2380 603 41 0 2730 0
vsize: 11084
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 89999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2384 603 41 0 2730 0
vsize: 11084
[startup+910.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 90999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2384 603 41 0 2730 0
vsize: 11084
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 91999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2384 603 41 0 2730 0
vsize: 11084
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2406 0 0 0 92999 10 0 0 25 0 1 0 421682725 11350016 2384 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2384 603 41 0 2730 0
vsize: 11084
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2411 0 0 0 94000 10 0 0 25 0 1 0 421682725 11350016 2389 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2771 2389 603 41 0 2730 0
vsize: 11084
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2426 0 0 0 95000 10 0 0 25 0 1 0 421682725 11464704 2404 4294967295 134512640 134672761 3221224544 3221223584 134612634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2404 603 41 0 2758 0
vsize: 11196
[startup+960.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2441 0 0 0 96000 10 0 0 25 0 1 0 421682725 11509760 2419 4294967295 134512640 134672761 3221224544 3221223584 134603536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2810 2419 603 41 0 2769 0
vsize: 11240
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2441 0 0 0 97000 10 0 0 25 0 1 0 421682725 11509760 2419 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2810 2419 603 41 0 2769 0
vsize: 11240
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2446 0 0 0 98000 10 0 0 25 0 1 0 421682725 11509760 2424 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2810 2424 603 41 0 2769 0
vsize: 11240
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 99000 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2431 603 41 0 2797 0
vsize: 11352
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 100001 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2431 603 41 0 2797 0
vsize: 11352
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2453 0 0 0 101001 10 0 0 25 0 1 0 421682725 11624448 2431 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2431 603 41 0 2797 0
vsize: 11352
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2459 0 0 0 102001 10 0 0 25 0 1 0 421682725 11624448 2437 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2437 603 41 0 2797 0
vsize: 11352
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2464 0 0 0 103001 10 0 0 25 0 1 0 421682725 11624448 2442 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2442 603 41 0 2797 0
vsize: 11352
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2472 0 0 0 104001 10 0 0 25 0 1 0 421682725 11624448 2450 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2838 2450 603 41 0 2797 0
vsize: 11352
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2486 0 0 0 105002 10 0 0 25 0 1 0 421682725 11730944 2464 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2464 603 41 0 2823 0
vsize: 11456
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2486 0 0 0 106002 10 0 0 25 0 1 0 421682725 11730944 2464 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2464 603 41 0 2823 0
vsize: 11456
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2503 0 0 0 107002 10 0 0 25 0 1 0 421682725 11730944 2481 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2481 603 41 0 2823 0
vsize: 11456
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2510 0 0 0 108002 10 0 0 25 0 1 0 421682725 11845632 2488 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2892 2488 603 41 0 2851 0
vsize: 11568
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2629 0 0 0 109002 10 0 0 25 0 1 0 421682725 12337152 2607 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3012 2607 603 41 0 2971 0
vsize: 12048
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2639 0 0 0 110002 10 0 0 25 0 1 0 421682725 12304384 2617 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3004 2617 603 41 0 2963 0
vsize: 12016
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2662 0 0 0 111002 11 0 0 25 0 1 0 421682725 12443648 2640 4294967295 134512640 134672761 3221224544 3221223584 134612927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3038 2640 603 41 0 2997 0
vsize: 12152
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2691 0 0 0 112002 11 0 0 25 0 1 0 421682725 12562432 2669 4294967295 134512640 134672761 3221224544 3221223584 134612608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3067 2669 603 41 0 3026 0
vsize: 12268
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2722 0 0 0 113003 11 0 0 25 0 1 0 421682725 12677120 2700 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3095 2700 603 41 0 3054 0
vsize: 12380
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2771 0 0 0 114003 11 0 0 25 0 1 0 421682725 12910592 2749 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2749 603 41 0 3111 0
vsize: 12608
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2795 0 0 0 115003 11 0 0 25 0 1 0 421682725 13012992 2773 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2773 603 41 0 3136 0
vsize: 12708
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2804 0 0 0 116003 11 0 0 25 0 1 0 421682725 13012992 2782 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3177 2782 603 41 0 3136 0
vsize: 12708
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2824 0 0 0 117003 11 0 0 25 0 1 0 421682725 13123584 2802 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3204 2802 603 41 0 3163 0
vsize: 12816
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2825 0 0 0 118003 11 0 0 25 0 1 0 421682725 13123584 2803 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3204 2803 603 41 0 3163 0
vsize: 12816
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2834 0 0 0 119003 11 0 0 25 0 1 0 421682725 13123584 2812 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3204 2812 603 41 0 3163 0
vsize: 12816
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3691
Raw data (stat): 3691 (minisat+) R 3690 30701 30700 0 -1 0 2834 0 0 0 120004 11 0 0 25 0 1 0 421682725 13123584 2812 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3204 2812 603 41 0 3163 0
vsize: 12816
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3691
Raw data (stat): 3691 (minisat+) Z 3690 30701 30700 0 -1 12 2834 0 0 0 120004 12 0 0 25 0 1 0 421682725 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.01
CPU time (s): 1200.16
CPU user time (s): 1200.04
CPU system time (s): 0.120981
CPU usage (%): 100.013
Max. virtual memory (Kb): 12816
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####