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_25_pb.cnf.cr.opb
MD5SUM808390b13d2d87ec4e78f628ed3af9ba
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 26
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.021995
Number of variables750
Total number of constraints80
Number of constraints which are clauses50
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 constraint25

Trace number 5325 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-13 23:27:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3767 boxname=wulflinc7 idbench=7 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  808390b13d2d87ec4e78f628ed3af9ba  /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb
IDLAUNCH: 3767
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        902728 kB
Buffers:         36788 kB
Cached:          75888 kB
SwapCached:          0 kB
Active:          72132 kB
Inactive:        43400 kB
HighTotal:      131008 kB
HighFree:        51212 kB
LowTotal:       903652 kB
LowFree:        851516 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10784 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:47:43 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 3767 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3530     9810 |    1058       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2130          
c   -- var.elim.:  2000/2130          
c   -- var.elim.:  2130/2130          
c   -- var.elim.:  870/870          
c   -- var.elim.:  138/138          
c   -- subsuming                       
c   -- var.elim.:  536/536          
c   -- var.elim.:  282/282          
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.:  70/70          
c   -- var.elim.:  72/72          
c   -- var.elim.:  74/74          
c   -- var.elim.:  76/76          
c   -- var.elim.:  78/78          
c   -- var.elim.:  152/152          
c   -- subsuming                       
c   -- var.elim.:  828/828          
c   -- var.elim.:  750/750          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  172/172          
c   -- var.elim.:  106/106          
c   -- var.elim.:  20/20          
c |         0 |    3056    11870 |      --       0       --      -- |     --   | -474/2150
c |         0 |    3056    11870 |    1222       0        0     nan |  0.000 % |
c |       100 |    3056    11870 |    1344     100     5550    55.5 |  1.672 % |
c |       252 |    3056    11870 |    1479     252    15203    60.3 |  1.672 % |
c |       477 |    3056    11870 |    1627     477    28482    59.7 |  1.672 % |
c |       814 |    3056    11870 |    1789     814    53822    66.1 |  1.672 % |
c |      1323 |    3056    11870 |    1968    1323   101449    76.7 |  1.672 % |
c |      2087 |    3056    11870 |    2165    2087   169352    81.1 |  1.672 % |
c |      3226 |    3056    11870 |    2382    2422   199980    82.6 |  1.673 % |
c |      4937 |    3056    11870 |    2620    2360   186287    78.9 |  1.672 % |
c |      7499 |    3056    11870 |    2882    2843   220073    77.4 |  1.673 % |
c |     11343 |    3056    11870 |    3170    3265   337027   103.2 |  1.672 % |
c |     17110 |    3056    11870 |    3487    3285   387759   118.0 |  1.672 % |
c |     25762 |    3056    11870 |    3836    2992   334469   111.8 |  1.672 % |
c |     38747 |    3056    11870 |    4220    3476   320541    #### 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.89 0.93 0.90 2/54 26337
Raw data (stat): 26337 (runsolver) R 26336 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421690685 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1228 0 0 0 995 2 0 0 25 0 1 0 421690685 6582272 1206 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1607 1206 603 41 0 1566 0
vsize: 6428
[startup+20.0005 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1297 0 0 0 1995 3 0 0 25 0 1 0 421690685 6844416 1275 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1671 1275 603 41 0 1630 0
vsize: 6684
[startup+30.0001 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1395 0 0 0 2994 3 0 0 25 0 1 0 421690685 7331840 1373 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1790 1373 603 41 0 1749 0
vsize: 7160
[startup+40 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1454 0 0 0 3994 3 0 0 25 0 1 0 421690685 7532544 1432 4294967295 134512640 134672761 3221224544 3221223584 134613771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1839 1432 603 41 0 1798 0
vsize: 7356
[startup+50.0004 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1581 0 0 0 4994 4 0 0 25 0 1 0 421690685 8060928 1559 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1968 1559 603 41 0 1927 0
vsize: 7872
[startup+60.0003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1603 0 0 0 5994 4 0 0 25 0 1 0 421690685 8183808 1581 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1998 1581 603 41 0 1957 0
vsize: 7992
[startup+70.0009 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1614 0 0 0 6994 4 0 0 25 0 1 0 421690685 8183808 1592 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1998 1592 603 41 0 1957 0
vsize: 7992
[startup+80.0012 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1690 0 0 0 7994 4 0 0 25 0 1 0 421690685 8556544 1668 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2089 1668 603 41 0 2048 0
vsize: 8356
[startup+90.0009 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1693 0 0 0 8994 4 0 0 25 0 1 0 421690685 8552448 1671 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2088 1671 603 41 0 2047 0
vsize: 8352
[startup+100.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1775 0 0 0 9995 4 0 0 25 0 1 0 421690685 8818688 1753 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2153 1753 603 41 0 2112 0
vsize: 8612
[startup+110 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1783 0 0 0 10995 4 0 0 25 0 1 0 421690685 8921088 1761 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1761 603 41 0 2137 0
vsize: 8712
[startup+120.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1783 0 0 0 11995 4 0 0 25 0 1 0 421690685 8921088 1761 4294967295 134512640 134672761 3221224544 3221223584 134614325 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2178 1761 603 41 0 2137 0
vsize: 8712
[startup+130.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 1954 0 0 0 12995 4 0 0 25 0 1 0 421690685 9584640 1932 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2340 1932 603 41 0 2299 0
vsize: 9360
[startup+140 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2009 0 0 0 13995 5 0 0 25 0 1 0 421690685 9830400 1987 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1987 603 41 0 2359 0
vsize: 9600
[startup+150.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2009 0 0 0 14995 5 0 0 25 0 1 0 421690685 9830400 1987 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1987 603 41 0 2359 0
vsize: 9600
[startup+160.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2014 0 0 0 15995 5 0 0 25 0 1 0 421690685 9830400 1992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1992 603 41 0 2359 0
vsize: 9600
[startup+170.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2014 0 0 0 16995 5 0 0 25 0 1 0 421690685 9830400 1992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1992 603 41 0 2359 0
vsize: 9600
[startup+180.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2014 0 0 0 17995 5 0 0 25 0 1 0 421690685 9830400 1992 4294967295 134512640 134672761 3221224544 3221223680 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2400 1992 603 41 0 2359 0
vsize: 9600
[startup+190.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2028 0 0 0 18996 5 0 0 25 0 1 0 421690685 9945088 2006 4294967295 134512640 134672761 3221224544 3221223584 134603522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2428 2006 603 41 0 2387 0
vsize: 9712
[startup+200.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2035 0 0 0 19996 5 0 0 25 0 1 0 421690685 9945088 2013 4294967295 134512640 134672761 3221224544 3221223640 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2428 2013 603 41 0 2387 0
vsize: 9712
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2066 0 0 0 20996 5 0 0 25 0 1 0 421690685 10092544 2044 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2464 2044 603 41 0 2423 0
vsize: 9856
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2078 0 0 0 21996 5 0 0 25 0 1 0 421690685 10092544 2056 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2464 2056 603 41 0 2423 0
vsize: 9856
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2082 0 0 0 22996 5 0 0 25 0 1 0 421690685 10092544 2060 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2464 2060 603 41 0 2423 0
vsize: 9856
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2125 0 0 0 23996 5 0 0 25 0 1 0 421690685 10416128 2103 4294967295 134512640 134672761 3221224544 3221223600 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2543 2103 603 41 0 2502 0
vsize: 10172
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2125 0 0 0 24996 5 0 0 25 0 1 0 421690685 10416128 2103 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2543 2103 603 41 0 2502 0
vsize: 10172
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2199 0 0 0 25996 5 0 0 25 0 1 0 421690685 10678272 2177 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2607 2177 603 41 0 2566 0
vsize: 10428
[startup+270.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2257 0 0 0 26996 6 0 0 25 0 1 0 421690685 10940416 2235 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2671 2235 603 41 0 2630 0
vsize: 10684
[startup+280 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2273 0 0 0 27996 6 0 0 25 0 1 0 421690685 10940416 2251 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2671 2251 603 41 0 2630 0
vsize: 10684
[startup+290 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2320 0 0 0 28996 6 0 0 25 0 1 0 421690685 11173888 2298 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2728 2298 603 41 0 2687 0
vsize: 10912
[startup+300 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2399 0 0 0 29996 6 0 0 25 0 1 0 421690685 11563008 2377 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2377 603 41 0 2782 0
vsize: 11292
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2421 0 0 0 30996 6 0 0 25 0 1 0 421690685 11563008 2399 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2399 603 41 0 2782 0
vsize: 11292
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2472 0 0 0 31996 7 0 0 25 0 1 0 421690685 11784192 2450 4294967295 134512640 134672761 3221224544 3221223728 134615649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2450 603 41 0 2836 0
vsize: 11508
[startup+329.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2476 0 0 0 32996 7 0 0 25 0 1 0 421690685 11784192 2454 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2454 603 41 0 2836 0
vsize: 11508
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2476 0 0 0 33996 7 0 0 25 0 1 0 421690685 11784192 2454 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2454 603 41 0 2836 0
vsize: 11508
[startup+349.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2476 0 0 0 34996 7 0 0 25 0 1 0 421690685 11784192 2454 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2454 603 41 0 2836 0
vsize: 11508
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2477 0 0 0 35996 7 0 0 25 0 1 0 421690685 11784192 2455 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2455 603 41 0 2836 0
vsize: 11508
[startup+369.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2477 0 0 0 36997 7 0 0 25 0 1 0 421690685 11784192 2455 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2877 2455 603 41 0 2836 0
vsize: 11508
[startup+379.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2500 0 0 0 37997 7 0 0 25 0 1 0 421690685 11915264 2478 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2909 2478 603 41 0 2868 0
vsize: 11636
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2549 0 0 0 38997 7 0 0 25 0 1 0 421690685 12197888 2527 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2978 2527 603 41 0 2937 0
vsize: 11912
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2549 0 0 0 39997 7 0 0 25 0 1 0 421690685 12197888 2527 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2978 2527 603 41 0 2937 0
vsize: 11912
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2570 0 0 0 40997 7 0 0 25 0 1 0 421690685 12197888 2548 4294967295 134512640 134672761 3221224544 3221223376 1075349984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2978 2548 603 41 0 2937 0
vsize: 11912
[startup+419.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 41997 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+429.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 42998 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223584 134603527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+439.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 43998 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 44998 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 45998 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2578 0 0 0 46998 7 0 0 25 0 1 0 421690685 12328960 2556 4294967295 134512640 134672761 3221224544 3221223744 134610697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2556 603 41 0 2969 0
vsize: 12040
[startup+479.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2592 0 0 0 47998 7 0 0 25 0 1 0 421690685 12328960 2570 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3010 2570 603 41 0 2969 0
vsize: 12040
[startup+489.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2607 0 0 0 48999 7 0 0 25 0 1 0 421690685 12439552 2585 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3037 2585 603 41 0 2996 0
vsize: 12148
[startup+499.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2619 0 0 0 49999 7 0 0 25 0 1 0 421690685 12439552 2597 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3037 2597 603 41 0 2996 0
vsize: 12148
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2635 0 0 0 50999 7 0 0 25 0 1 0 421690685 12558336 2613 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3066 2613 603 41 0 3025 0
vsize: 12264
[startup+519.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2684 0 0 0 51999 7 0 0 25 0 1 0 421690685 12689408 2662 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3098 2662 603 41 0 3057 0
vsize: 12392
[startup+529.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2702 0 0 0 52999 7 0 0 25 0 1 0 421690685 12849152 2680 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3137 2680 603 41 0 3096 0
vsize: 12548
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2710 0 0 0 53999 7 0 0 25 0 1 0 421690685 12849152 2688 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3137 2688 603 41 0 3096 0
vsize: 12548
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2718 0 0 0 54999 7 0 0 25 0 1 0 421690685 12849152 2696 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3137 2696 603 41 0 3096 0
vsize: 12548
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2718 0 0 0 56000 7 0 0 25 0 1 0 421690685 12849152 2696 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3137 2696 603 41 0 3096 0
vsize: 12548
[startup+569.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2734 0 0 0 57000 7 0 0 25 0 1 0 421690685 12980224 2712 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3169 2712 603 41 0 3128 0
vsize: 12676
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2734 0 0 0 58000 7 0 0 25 0 1 0 421690685 12980224 2712 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3169 2712 603 41 0 3128 0
vsize: 12676
[startup+589.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2742 0 0 0 59000 7 0 0 25 0 1 0 421690685 12980224 2720 4294967295 134512640 134672761 3221224544 3221223584 134603536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3169 2720 603 41 0 3128 0
vsize: 12676
[startup+599.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2772 0 0 0 60000 7 0 0 25 0 1 0 421690685 13111296 2750 4294967295 134512640 134672761 3221224544 3221223584 134613818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2750 603 41 0 3160 0
vsize: 12804
[startup+609.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2772 0 0 0 61000 7 0 0 25 0 1 0 421690685 13111296 2750 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2750 603 41 0 3160 0
vsize: 12804
[startup+619.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2772 0 0 0 62001 7 0 0 25 0 1 0 421690685 13111296 2750 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2750 603 41 0 3160 0
vsize: 12804
[startup+629.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2773 0 0 0 63001 7 0 0 25 0 1 0 421690685 13111296 2751 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2751 603 41 0 3160 0
vsize: 12804
[startup+639.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2773 0 0 0 64001 7 0 0 25 0 1 0 421690685 13111296 2751 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2751 603 41 0 3160 0
vsize: 12804
[startup+649.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2773 0 0 0 65001 7 0 0 25 0 1 0 421690685 13111296 2751 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2751 603 41 0 3160 0
vsize: 12804
[startup+659.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2782 0 0 0 66001 7 0 0 25 0 1 0 421690685 13111296 2760 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2760 603 41 0 3160 0
vsize: 12804
[startup+669.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2782 0 0 0 67001 7 0 0 25 0 1 0 421690685 13111296 2760 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2760 603 41 0 3160 0
vsize: 12804
[startup+679.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2782 0 0 0 68002 7 0 0 25 0 1 0 421690685 13111296 2760 4294967295 134512640 134672761 3221224544 3221223584 134612572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2760 603 41 0 3160 0
vsize: 12804
[startup+689.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2782 0 0 0 69002 7 0 0 25 0 1 0 421690685 13111296 2760 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2760 603 41 0 3160 0
vsize: 12804
[startup+699.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2782 0 0 0 70002 7 0 0 25 0 1 0 421690685 13111296 2760 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2760 603 41 0 3160 0
vsize: 12804
[startup+709.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2795 0 0 0 71002 7 0 0 25 0 1 0 421690685 13230080 2773 4294967295 134512640 134672761 3221224544 3221223524 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3230 2773 603 41 0 3189 0
vsize: 12920
[startup+719.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2808 0 0 0 72002 7 0 0 25 0 1 0 421690685 13225984 2786 4294967295 134512640 134672761 3221224544 3221223584 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3229 2786 603 41 0 3188 0
vsize: 12916
[startup+729.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2808 0 0 0 73003 7 0 0 25 0 1 0 421690685 13225984 2786 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3229 2786 603 41 0 3188 0
vsize: 12916
[startup+739.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2808 0 0 0 74003 7 0 0 25 0 1 0 421690685 13225984 2786 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3229 2786 603 41 0 3188 0
vsize: 12916
[startup+749.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2808 0 0 0 75003 7 0 0 25 0 1 0 421690685 13225984 2786 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3229 2786 603 41 0 3188 0
vsize: 12916
[startup+759.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2808 0 0 0 76003 7 0 0 25 0 1 0 421690685 13225984 2786 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3229 2786 603 41 0 3188 0
vsize: 12916
[startup+769.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2851 0 0 0 77003 7 0 0 25 0 1 0 421690685 13484032 2829 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3292 2829 603 41 0 3251 0
vsize: 13168
[startup+779.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2911 0 0 0 78003 7 0 0 25 0 1 0 421690685 13737984 2889 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3354 2889 603 41 0 3313 0
vsize: 13416
[startup+789.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2957 0 0 0 79003 7 0 0 25 0 1 0 421690685 13942784 2935 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3404 2935 603 41 0 3363 0
vsize: 13616
[startup+799.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2976 0 0 0 80003 8 0 0 25 0 1 0 421690685 14024704 2954 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3424 2954 603 41 0 3383 0
vsize: 13696
[startup+809.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 2982 0 0 0 81003 8 0 0 25 0 1 0 421690685 14024704 2960 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3424 2960 603 41 0 3383 0
vsize: 13696
[startup+819.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3004 0 0 0 82004 8 0 0 25 0 1 0 421690685 14151680 2982 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3455 2982 603 41 0 3414 0
vsize: 13820
[startup+829.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3024 0 0 0 83004 8 0 0 25 0 1 0 421690685 14151680 3002 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3455 3002 603 41 0 3414 0
vsize: 13820
[startup+839.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3051 0 0 0 84004 8 0 0 25 0 1 0 421690685 14282752 3029 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3487 3029 603 41 0 3446 0
vsize: 13948
[startup+849.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3067 0 0 0 85004 8 0 0 25 0 1 0 421690685 14376960 3045 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3510 3045 603 41 0 3469 0
vsize: 14040
[startup+859.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3067 0 0 0 86004 8 0 0 25 0 1 0 421690685 14376960 3045 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3510 3045 603 41 0 3469 0
vsize: 14040
[startup+869.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3081 0 0 0 87004 8 0 0 25 0 1 0 421690685 14475264 3059 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3534 3059 603 41 0 3493 0
vsize: 14136
[startup+879.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3120 0 0 0 88004 8 0 0 25 0 1 0 421690685 14630912 3098 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3572 3098 603 41 0 3531 0
vsize: 14288
[startup+889.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3157 0 0 0 89004 8 0 0 25 0 1 0 421690685 14761984 3135 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3604 3135 603 41 0 3563 0
vsize: 14416
[startup+899.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3171 0 0 0 90005 8 0 0 25 0 1 0 421690685 14843904 3149 4294967295 134512640 134672761 3221224544 3221223584 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3149 603 41 0 3583 0
vsize: 14496
[startup+909.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3177 0 0 0 91005 8 0 0 25 0 1 0 421690685 14843904 3155 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3155 603 41 0 3583 0
vsize: 14496
[startup+919.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3177 0 0 0 92005 8 0 0 25 0 1 0 421690685 14843904 3155 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3155 603 41 0 3583 0
vsize: 14496
[startup+929.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3194 0 0 0 93005 8 0 0 25 0 1 0 421690685 14942208 3172 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3172 603 41 0 3607 0
vsize: 14592
[startup+939.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3209 0 0 0 94005 8 0 0 25 0 1 0 421690685 14942208 3187 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3187 603 41 0 3607 0
vsize: 14592
[startup+949.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3209 0 0 0 95006 8 0 0 25 0 1 0 421690685 14942208 3187 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3187 603 41 0 3607 0
vsize: 14592
[startup+959.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3209 0 0 0 96006 8 0 0 25 0 1 0 421690685 14942208 3187 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3648 3187 603 41 0 3607 0
vsize: 14592
[startup+969.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3262 0 0 0 97006 8 0 0 25 0 1 0 421690685 15220736 3240 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3716 3240 603 41 0 3675 0
vsize: 14864
[startup+979.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3287 0 0 0 98006 8 0 0 25 0 1 0 421690685 15351808 3265 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3265 603 41 0 3707 0
vsize: 14992
[startup+989.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 99006 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+999.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 100006 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223680 134614664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 101006 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 102007 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 103007 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 104007 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 105007 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 106007 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 107008 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 108008 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 109008 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 110008 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 111008 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 112009 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 113009 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 114009 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 115009 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223744 134610602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3295 0 0 0 116009 8 0 0 25 0 1 0 421690685 15351808 3273 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3273 603 41 0 3707 0
vsize: 14992
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3296 0 0 0 117010 8 0 0 25 0 1 0 421690685 15351808 3274 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3274 603 41 0 3707 0
vsize: 14992
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3296 0 0 0 118010 8 0 0 25 0 1 0 421690685 15351808 3274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3274 603 41 0 3707 0
vsize: 14992
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3296 0 0 0 119010 8 0 0 25 0 1 0 421690685 15351808 3274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3274 603 41 0 3707 0
vsize: 14992
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26337
Raw data (stat): 26337 (minisat+) R 26336 22932 22931 0 -1 0 3406 0 0 0 120010 8 0 0 25 0 1 0 421690685 15814656 3384 4294967295 134512640 134672761 3221224544 3221223584 134612878 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3861 3384 603 41 0 3820 0
vsize: 15444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 26337
Raw data (stat): 26337 (minisat+) Z 26336 22932 22931 0 -1 12 3406 0 0 0 120010 9 0 0 25 0 1 0 421690685 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
CPU time (s): 1200.2
CPU user time (s): 1200.1
CPU system time (s): 0.097985
CPU usage (%): 100.016
Max. virtual memory (Kb): 15444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####