PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga25_23_sat_pb.cnf.cr.opb
MD5SUM	002d92124dd96ccf471b7e05fe08f2d6
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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 numbers	5
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.252961
Number of variables	863
Total number of constraints	646
Number of constraints which are clauses	598
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	12
Maximum length of a constraint	25
Trace number 5395

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-13 23:38:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3803 boxname=wulflinc3 idbench=43 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  002d92124dd96ccf471b7e05fe08f2d6  /oldhome/oroussel/tmp/wulflinc3/normalized-fpga25_23_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc3/normalized-fpga25_23_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc3/normalized-fpga25_23_sat_pb.cnf.cr.opb
IDLAUNCH: 3803
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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.190
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:        886176 kB
Buffers:         35408 kB
Cached:          90176 kB
SwapCached:       3276 kB
Active:          68252 kB
Inactive:        63452 kB
HighTotal:      131008 kB
HighFree:        36904 kB
LowTotal:       903652 kB
LowFree:        849272 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11136 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:58:55 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3803 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  47]---> BDD-cost:   43
c ---[  46]---> BDD-cost:   43
c ---[  45]---> BDD-cost:   43
c ---[  44]---> BDD-cost:   43
c ---[  43]---> BDD-cost:   43
c ---[  42]---> BDD-cost:   43
c ---[  41]---> BDD-cost:   43
c ---[  40]---> BDD-cost:   43
c ---[  39]---> BDD-cost:   43
c ---[  38]---> BDD-cost:   43
c ---[  37]---> BDD-cost:   43
c ---[  36]---> BDD-cost:   43
c ---[  35]---> BDD-cost:   43
c ---[  34]---> BDD-cost:   43
c ---[  33]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   43
c ---[  31]---> BDD-cost:   43
c ---[  30]---> BDD-cost:   43
c ---[  29]---> BDD-cost:   43
c ---[  28]---> BDD-cost:   43
c ---[  27]---> BDD-cost:   43
c ---[  26]---> BDD-cost:   43
c ---[  25]---> BDD-cost:   43
c ---[  24]---> BDD-cost:   43
c ---[  23]---> BDD-cost:   43
c ---[  22]---> BDD-cost:   21
c ---[  21]---> BDD-cost:   21
c ---[  20]---> BDD-cost:   21
c ---[  19]---> BDD-cost:   21
c ---[  18]---> BDD-cost:   21
c ---[  17]---> BDD-cost:   21
c ---[  16]---> BDD-cost:   21
c ---[  15]---> BDD-cost:   21
c ---[  14]---> BDD-cost:   21
c ---[  13]---> BDD-cost:   21
c ---[  12]---> BDD-cost:   21
c ---[  11]---> BDD-cost:   23
c ---[  10]---> BDD-cost:   23
c ---[   9]---> BDD-cost:   23
c ---[   8]---> BDD-cost:   23
c ---[   7]---> BDD-cost:   23
c ---[   6]---> BDD-cost:   23
c ---[   5]---> BDD-cost:   23
c ---[   4]---> BDD-cost:   23
c ---[   3]---> BDD-cost:   23
c ---[   2]---> BDD-cost:   23
c ---[   1]---> BDD-cost:   23
c ---[   0]---> BDD-cost:   23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4481    17889 |    1344       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2397          
c   -- var.elim.:  2000/2397          
c   -- var.elim.:  2397/2397          
c   -- var.elim.:  836/836          
c   -- subsuming                       
c   -- var.elim.:  728/728          
c   -- var.elim.:  866/866          
c   -- subsuming                       
c   -- var.elim.:  452/452          
c   -- var.elim.:  635/635          
c   -- subsuming                       
c   -- var.elim.:  556/556          
c   -- var.elim.:  77/77          
c |         0 |    4122    18288 |      --       0       --      -- |     --   | -359/543
c |         0 |    4122    18288 |    1648       0        0     nan |  0.000 % |
c |       102 |    4122    18288 |    1813     102    11994   117.6 |  2.200 % |
c |       253 |    4122    18288 |    1995     253    34803   137.6 |  2.201 % |
c |       479 |    4122    18288 |    2194     479    56338   117.6 |  2.200 % |
c |       819 |    4122    18288 |    2414     819   109951   134.3 |  2.200 % |
c |      1328 |    4122    18288 |    2655    1328   162588   122.4 |  2.201 % |
c |      2089 |    4122    18288 |    2920    2089   267639   128.1 |  2.200 % |
c |      3228 |    4122    18288 |    3213    3228   458588   142.1 |  2.200 % |
c |      4937 |    4122    18288 |    3534    3451   509017   147.5 |  2.201 % |
c |      7500 |    4122    18288 |    3887    4411   763850  #### 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.55 0.83 0.87 2/54 17906
Raw data (stat): 17906 (runsolver) R 17905 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421749728 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0006 s]
Raw data (loadavg): 0.62 0.84 0.87 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 1570 0 0 0 995 3 0 0 25 0 1 0 421749728 7979008 1548 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1948 1548 603 41 0 1907 0
vsize: 7792
[startup+20.0007 s]
Raw data (loadavg): 0.68 0.84 0.87 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2454 0 0 0 1993 5 0 0 25 0 1 0 421749728 11640832 2432 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2842 2432 603 41 0 2801 0
vsize: 11368
[startup+30.0015 s]
Raw data (loadavg): 0.72 0.85 0.87 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2783 0 0 0 2992 6 0 0 25 0 1 0 421749728 12922880 2761 4294967295 134512640 134672761 3221224544 3221223648 134603947 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2761 603 41 0 3114 0
vsize: 12620
[startup+40.001 s]
Raw data (loadavg): 0.77 0.85 0.87 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2783 0 0 0 3992 6 0 0 25 0 1 0 421749728 12922880 2761 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2761 603 41 0 3114 0
vsize: 12620
[startup+50.0012 s]
Raw data (loadavg): 0.80 0.86 0.87 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2784 0 0 0 4992 6 0 0 25 0 1 0 421749728 12922880 2762 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2762 603 41 0 3114 0
vsize: 12620
[startup+60.002 s]
Raw data (loadavg): 0.91 0.88 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2784 0 0 0 5992 6 0 0 25 0 1 0 421749728 12922880 2762 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3155 2762 603 41 0 3114 0
vsize: 12620
[startup+70.0025 s]
Raw data (loadavg): 0.92 0.88 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2826 0 0 0 6993 6 0 0 25 0 1 0 421749728 13164544 2804 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2804 603 41 0 3173 0
vsize: 12856
[startup+80.0037 s]
Raw data (loadavg): 0.93 0.88 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2829 0 0 0 7993 6 0 0 25 0 1 0 421749728 13164544 2807 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3214 2807 603 41 0 3173 0
vsize: 12856
[startup+90.0036 s]
Raw data (loadavg): 0.94 0.89 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2841 0 0 0 8993 6 0 0 25 0 1 0 421749728 13246464 2819 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3234 2819 603 41 0 3193 0
vsize: 12936
[startup+100.003 s]
Raw data (loadavg): 0.95 0.89 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2841 0 0 0 9993 6 0 0 25 0 1 0 421749728 13246464 2819 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3234 2819 603 41 0 3193 0
vsize: 12936
[startup+110.004 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2841 0 0 0 10993 6 0 0 25 0 1 0 421749728 13246464 2819 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3234 2819 603 41 0 3193 0
vsize: 12936
[startup+120.005 s]
Raw data (loadavg): 0.96 0.90 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2841 0 0 0 11994 6 0 0 25 0 1 0 421749728 13246464 2819 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3234 2819 603 41 0 3193 0
vsize: 12936
[startup+130.006 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 2841 0 0 0 12994 6 0 0 25 0 1 0 421749728 13246464 2819 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3234 2819 603 41 0 3193 0
vsize: 12936
[startup+140.006 s]
Raw data (loadavg): 0.97 0.90 0.88 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3256 0 0 0 13993 7 0 0 25 0 1 0 421749728 14934016 3234 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3646 3234 603 41 0 3605 0
vsize: 14584
[startup+150.005 s]
Raw data (loadavg): 0.98 0.90 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3305 0 0 0 14993 7 0 0 25 0 1 0 421749728 15159296 3283 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3283 603 41 0 3660 0
vsize: 14804
[startup+160.005 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3312 0 0 0 15993 7 0 0 25 0 1 0 421749728 15159296 3290 4294967295 134512640 134672761 3221224544 3221223584 134614346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3701 3290 603 41 0 3660 0
vsize: 14804
[startup+170.005 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3330 0 0 0 16993 7 0 0 25 0 1 0 421749728 15257600 3308 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3308 603 41 0 3684 0
vsize: 14900
[startup+180.006 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3344 0 0 0 17993 7 0 0 25 0 1 0 421749728 15257600 3322 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3322 603 41 0 3684 0
vsize: 14900
[startup+190.006 s]
Raw data (loadavg): 0.99 0.91 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 3613 0 0 0 18993 8 0 0 25 0 1 0 421749728 16441344 3591 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4014 3591 603 41 0 3973 0
vsize: 16056
[startup+200.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4032 0 0 0 19991 10 0 0 25 0 1 0 421749728 18120704 4010 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4424 4010 603 41 0 4383 0
vsize: 17696
[startup+210.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4124 0 0 0 20991 10 0 0 25 0 1 0 421749728 18513920 4102 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4520 4102 603 41 0 4479 0
vsize: 18080
[startup+220.006 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4124 0 0 0 21991 10 0 0 25 0 1 0 421749728 18501632 4102 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4517 4102 603 41 0 4476 0
vsize: 18068
[startup+230.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4124 0 0 0 22992 10 0 0 25 0 1 0 421749728 18501632 4102 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4517 4102 603 41 0 4476 0
vsize: 18068
[startup+240.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4358 0 0 0 23991 11 0 0 25 0 1 0 421749728 19423232 4336 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4742 4336 603 41 0 4701 0
vsize: 18968
[startup+250.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4420 0 0 0 24991 11 0 0 25 0 1 0 421749728 19685376 4398 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4806 4398 603 41 0 4765 0
vsize: 19224
[startup+260.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4537 0 0 0 25991 11 0 0 25 0 1 0 421749728 20197376 4515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4515 603 41 0 4890 0
vsize: 19724
[startup+270.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4538 0 0 0 26991 11 0 0 25 0 1 0 421749728 20197376 4516 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4516 603 41 0 4890 0
vsize: 19724
[startup+280.007 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4538 0 0 0 27992 11 0 0 25 0 1 0 421749728 20197376 4516 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4516 603 41 0 4890 0
vsize: 19724
[startup+290.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4538 0 0 0 28992 11 0 0 25 0 1 0 421749728 20197376 4516 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4516 603 41 0 4890 0
vsize: 19724
[startup+300.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4538 0 0 0 29992 11 0 0 25 0 1 0 421749728 20197376 4516 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4516 603 41 0 4890 0
vsize: 19724
[startup+310.008 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4539 0 0 0 30992 11 0 0 25 0 1 0 421749728 20197376 4517 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4931 4517 603 41 0 4890 0
vsize: 19724
[startup+320.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4554 0 0 0 31992 11 0 0 25 0 1 0 421749728 20275200 4532 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4950 4532 603 41 0 4909 0
vsize: 19800
[startup+330.009 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4792 0 0 0 32992 12 0 0 25 0 1 0 421749728 21192704 4770 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4770 603 41 0 5133 0
vsize: 20696
[startup+340.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4792 0 0 0 33992 12 0 0 25 0 1 0 421749728 21192704 4770 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4770 603 41 0 5133 0
vsize: 20696
[startup+350.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4792 0 0 0 34992 12 0 0 25 0 1 0 421749728 21192704 4770 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4770 603 41 0 5133 0
vsize: 20696
[startup+360.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4792 0 0 0 35993 12 0 0 25 0 1 0 421749728 21192704 4770 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4770 603 41 0 5133 0
vsize: 20696
[startup+370.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4792 0 0 0 36993 12 0 0 25 0 1 0 421749728 21008384 4732 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4732 603 41 0 5088 0
vsize: 20516
[startup+380.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 37993 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+390.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 38993 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+400.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 39994 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+410.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 40994 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+420.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 41994 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+430.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 42994 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+440.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 43994 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+450.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 44995 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+460.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 45995 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+470.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 46995 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+480.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 47995 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+490.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 48995 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+500.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 49996 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+510.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 50996 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+520.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 4794 0 0 0 51996 12 0 0 25 0 1 0 421749728 21008384 4734 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5129 4734 603 41 0 5088 0
vsize: 20516
[startup+530.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5075 0 0 0 52995 12 0 0 25 0 1 0 421749728 22192128 5015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5418 5015 603 41 0 5377 0
vsize: 21672
[startup+540.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 53995 13 0 0 25 0 1 0 421749728 22847488 5161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5578 5161 603 41 0 5537 0
vsize: 22312
[startup+550.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 54995 13 0 0 25 0 1 0 421749728 22847488 5161 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5578 5161 603 41 0 5537 0
vsize: 22312
[startup+560.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 55995 13 0 0 25 0 1 0 421749728 22835200 5161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5575 5161 603 41 0 5534 0
vsize: 22300
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 56995 13 0 0 25 0 1 0 421749728 22835200 5161 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5575 5161 603 41 0 5534 0
vsize: 22300
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 57996 13 0 0 25 0 1 0 421749728 22818816 5161 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5571 5161 603 41 0 5530 0
vsize: 22284
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 58996 13 0 0 25 0 1 0 421749728 22818816 5161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5571 5161 603 41 0 5530 0
vsize: 22284
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 59996 13 0 0 25 0 1 0 421749728 22818816 5161 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5571 5161 603 41 0 5530 0
vsize: 22284
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 60996 13 0 0 25 0 1 0 421749728 22818816 5161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5571 5161 603 41 0 5530 0
vsize: 22284
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 61996 13 0 0 25 0 1 0 421749728 22818816 5161 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5571 5161 603 41 0 5530 0
vsize: 22284
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 62997 13 0 0 25 0 1 0 421749728 22814720 5161 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5161 603 41 0 5529 0
vsize: 22280
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 63997 13 0 0 25 0 1 0 421749728 22814720 5161 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5161 603 41 0 5529 0
vsize: 22280
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 64997 13 0 0 25 0 1 0 421749728 22814720 5161 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5570 5161 603 41 0 5529 0
vsize: 22280
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 65997 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 66997 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 67998 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 68998 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 69998 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 70998 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 71998 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5221 0 0 0 72999 13 0 0 25 0 1 0 421749728 22810624 5161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5161 603 41 0 5528 0
vsize: 22276
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5223 0 0 0 73999 13 0 0 25 0 1 0 421749728 22810624 5163 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5569 5163 603 41 0 5528 0
vsize: 22276
[startup+750.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5250 0 0 0 74999 13 0 0 25 0 1 0 421749728 22974464 5190 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5609 5190 603 41 0 5568 0
vsize: 22436
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5324 0 0 0 75999 13 0 0 25 0 1 0 421749728 23379968 5264 4294967295 134512640 134672761 3221224544 3221223640 134616368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5708 5264 603 41 0 5667 0
vsize: 22832
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5329 0 0 0 76999 13 0 0 25 0 1 0 421749728 23314432 5269 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5692 5269 603 41 0 5651 0
vsize: 22768
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5336 0 0 0 77999 14 0 0 25 0 1 0 421749728 23314432 5276 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5692 5276 603 41 0 5651 0
vsize: 22768
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5512 0 0 0 78998 15 0 0 25 0 1 0 421749728 24100864 5452 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5884 5452 603 41 0 5843 0
vsize: 23536
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5588 0 0 0 79998 15 0 0 25 0 1 0 421749728 24379392 5528 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5952 5528 603 41 0 5911 0
vsize: 23808
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5692 0 0 0 80998 15 0 0 25 0 1 0 421749728 24772608 5632 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6048 5632 603 41 0 6007 0
vsize: 24192
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 81998 15 0 0 25 0 1 0 421749728 25407488 5767 4294967295 134512640 134672761 3221224544 3221223584 134612668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5767 603 41 0 6162 0
vsize: 24812
[startup+830.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 82998 15 0 0 25 0 1 0 421749728 25407488 5767 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6203 5767 603 41 0 6162 0
vsize: 24812
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 83998 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 84999 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 85999 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+870.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 86999 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 87999 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223728 134616006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 88999 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5827 0 0 0 90000 15 0 0 25 0 1 0 421749728 25403392 5767 4294967295 134512640 134672761 3221224544 3221223584 134614271 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5767 603 41 0 6161 0
vsize: 24808
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5828 0 0 0 91000 15 0 0 25 0 1 0 421749728 25395200 5768 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5768 603 41 0 6159 0
vsize: 24800
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5828 0 0 0 92000 15 0 0 25 0 1 0 421749728 25395200 5768 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6200 5768 603 41 0 6159 0
vsize: 24800
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5828 0 0 0 93000 15 0 0 25 0 1 0 421749728 25391104 5768 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5768 603 41 0 6158 0
vsize: 24796
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5828 0 0 0 94000 15 0 0 25 0 1 0 421749728 25391104 5768 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5768 603 41 0 6158 0
vsize: 24796
[startup+950.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 95000 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+960.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 96001 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 97001 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 98001 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 99001 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 100001 15 0 0 25 0 1 0 421749728 25391104 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6199 5769 603 41 0 6158 0
vsize: 24796
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 101002 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 102002 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 103002 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 104002 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223548 134619842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 105002 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 106003 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 107003 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 108003 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 109003 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 110003 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 111004 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 112004 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 113004 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 114004 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 115004 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 116005 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 117005 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 118005 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 119005 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 17906
Raw data (stat): 17906 (minisat+) R 17905 10720 10719 0 -1 0 5829 0 0 0 120005 15 0 0 25 0 1 0 421749728 25387008 5769 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6198 5769 603 41 0 6157 0
vsize: 24792
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 17906
Raw data (stat): 17906 (minisat+) Z 17905 10720 10719 0 -1 12 5829 0 0 0 120005 17 0 0 25 0 1 0 421749728 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.05
CPU time (s): 1200.23
CPU user time (s): 1200.06
CPU system time (s): 0.171973
CPU usage (%): 100.015
Max. virtual memory (Kb): 24812
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####