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-chnl35_45_pb.cnf.cr.opb
MD5SUM	1f5fb3c191c2c77719f10f35e4f5f992
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(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	46
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.094985
Number of variables	3150
Total number of constraints	160
Number of constraints which are clauses	90
Number of constraints which are cardinality constraints (but not clauses)	70
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	35
Maximum length of a constraint	45
Trace number 5336

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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:        915920 kB
Buffers:         34704 kB
Cached:          59780 kB
SwapCached:       4932 kB
Active:          55456 kB
Inactive:        46844 kB
HighTotal:      131008 kB
HighFree:        67480 kB
LowTotal:       903652 kB
LowFree:        848440 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10876 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:54:50 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 3776 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   15210    42490 |    4562       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9170          
c   -- var.elim.:  2000/9170          
c   -- var.elim.:  3000/9170          
c   -- var.elim.:  4000/9170          
c   -- var.elim.:  5000/9170          
c   -- var.elim.:  6000/9170          
c   -- var.elim.:  7000/9170          
c   -- var.elim.:  8000/9170          
c   -- var.elim.:  9000/9170          
c   -- var.elim.:  9170/9170          
c   -- var.elim.:  1000/3450          
c   -- var.elim.:  2000/3450          
c   -- var.elim.:  3000/3450          
c   -- var.elim.:  3450/3450          
c   -- var.elim.:  146/146          
c   -- subsuming                       
c   -- var.elim.:  1000/1958          
c   -- var.elim.:  1958/1958          
c   -- var.elim.:  682/682          
c   -- var.elim.:  224/224          
c   -- var.elim.:  222/222          
c   -- var.elim.:  98/98          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108    #### 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.92 0.95 0.90 2/54 5531
Raw data (stat): 5531 (runsolver) R 5530 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421726920 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.0008 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 3796 0 0 0 989 10 0 0 25 0 1 0 421726920 17367040 3730 4294967295 134512640 134672761 3221224544 3221223584 134613822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3730 603 41 0 4199 0
vsize: 16960
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 5546 0 0 0 1984 14 0 0 25 0 1 0 421726920 24510464 5480 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5984 5480 603 41 0 5943 0
vsize: 23936
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 6281 0 0 0 2983 16 0 0 25 0 1 0 421726920 27648000 6214 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6750 6214 603 41 0 6709 0
vsize: 27000
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 6435 0 0 0 3982 17 0 0 25 0 1 0 421726920 28303360 6368 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6910 6368 603 41 0 6869 0
vsize: 27640
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 7216 0 0 0 4980 19 0 0 25 0 1 0 421726920 31461376 7149 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7681 7149 603 41 0 7640 0
vsize: 30724
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 7796 0 0 0 5978 22 0 0 25 0 1 0 421726920 34000896 7729 4294967295 134512640 134672761 3221224544 3221223640 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8301 7729 603 41 0 8260 0
vsize: 33204
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 7796 0 0 0 6978 22 0 0 25 0 1 0 421726920 33869824 7728 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8269 7728 603 41 0 8228 0
vsize: 33076
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 7909 0 0 0 7978 22 0 0 25 0 1 0 421726920 34394112 7841 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8397 7841 603 41 0 8356 0
vsize: 33588
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 8856 0 0 0 8976 24 0 0 25 0 1 0 421726920 38195200 8788 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9325 8788 603 41 0 9284 0
vsize: 37300
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 8856 0 0 0 9976 24 0 0 25 0 1 0 421726920 38195200 8788 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9325 8788 603 41 0 9284 0
vsize: 37300
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 8856 0 0 0 10977 24 0 0 25 0 1 0 421726920 38195200 8788 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9325 8788 603 41 0 9284 0
vsize: 37300
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 9143 0 0 0 11976 25 0 0 25 0 1 0 421726920 39395328 9075 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9618 9075 603 41 0 9577 0
vsize: 38472
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 9971 0 0 0 12974 27 0 0 25 0 1 0 421726920 42831872 9903 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10457 9903 603 41 0 10416 0
vsize: 41828
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10620 0 0 0 13972 29 0 0 25 0 1 0 421726920 45469696 10552 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11101 10552 603 41 0 11060 0
vsize: 44404
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10955 0 0 0 14972 29 0 0 25 0 1 0 421726920 46813184 10886 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11429 10886 603 41 0 11388 0
vsize: 45716
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10956 0 0 0 15972 29 0 0 25 0 1 0 421726920 46813184 10887 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11429 10887 603 41 0 11388 0
vsize: 45716
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10957 0 0 0 16972 29 0 0 25 0 1 0 421726920 46813184 10888 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11429 10888 603 41 0 11388 0
vsize: 45716
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10957 0 0 0 17973 29 0 0 25 0 1 0 421726920 46813184 10888 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11429 10888 603 41 0 11388 0
vsize: 45716
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 10957 0 0 0 18973 29 0 0 25 0 1 0 421726920 46813184 10888 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11429 10888 603 41 0 11388 0
vsize: 45716
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11131 0 0 0 19973 30 0 0 25 0 1 0 421726920 47607808 11062 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11623 11062 603 41 0 11582 0
vsize: 46492
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11621 0 0 0 20972 31 0 0 25 0 1 0 421726920 49553408 11552 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12098 11552 603 41 0 12057 0
vsize: 48392
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11621 0 0 0 21972 31 0 0 25 0 1 0 421726920 49553408 11552 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12098 11552 603 41 0 12057 0
vsize: 48392
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11621 0 0 0 22972 31 0 0 25 0 1 0 421726920 49553408 11552 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12098 11552 603 41 0 12057 0
vsize: 48392
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11622 0 0 0 23972 31 0 0 25 0 1 0 421726920 49553408 11553 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12098 11553 603 41 0 12057 0
vsize: 48392
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 24973 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 25973 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 26973 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 27973 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 28973 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 29974 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 30974 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 31974 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11625 0 0 0 32974 31 0 0 25 0 1 0 421726920 49541120 11555 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11555 603 41 0 12054 0
vsize: 48380
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 33974 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 34975 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 35975 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 36975 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 37975 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 38975 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223584 134612601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 39976 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11627 0 0 0 40976 31 0 0 25 0 1 0 421726920 49541120 11557 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11557 603 41 0 12054 0
vsize: 48380
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11629 0 0 0 41976 31 0 0 25 0 1 0 421726920 49541120 11559 4294967295 134512640 134672761 3221224544 3221223640 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11559 603 41 0 12054 0
vsize: 48380
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11629 0 0 0 42976 31 0 0 25 0 1 0 421726920 49541120 11559 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11559 603 41 0 12054 0
vsize: 48380
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11629 0 0 0 43977 31 0 0 25 0 1 0 421726920 49541120 11559 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11559 603 41 0 12054 0
vsize: 48380
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11629 0 0 0 44977 31 0 0 25 0 1 0 421726920 49541120 11559 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11559 603 41 0 12054 0
vsize: 48380
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 11629 0 0 0 45977 31 0 0 25 0 1 0 421726920 49541120 11559 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12095 11559 603 41 0 12054 0
vsize: 48380
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 12526 0 0 0 46974 34 0 0 25 0 1 0 421726920 53219328 12456 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12993 12456 603 41 0 12952 0
vsize: 51972
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 13682 0 0 0 47972 36 0 0 25 0 1 0 421726920 57950208 13612 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14148 13612 603 41 0 14107 0
vsize: 56592
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 14643 0 0 0 48970 38 0 0 25 0 1 0 421726920 61898752 14573 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15112 14573 603 41 0 15071 0
vsize: 60448
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15147 0 0 0 49969 40 0 0 25 0 1 0 421726920 63995904 15077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15624 15077 603 41 0 15583 0
vsize: 62496
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15694 0 0 0 50968 41 0 0 25 0 1 0 421726920 66236416 15623 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15623 603 41 0 16130 0
vsize: 64684
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15694 0 0 0 51968 41 0 0 25 0 1 0 421726920 66236416 15623 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15623 603 41 0 16130 0
vsize: 64684
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15694 0 0 0 52968 41 0 0 25 0 1 0 421726920 66236416 15623 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15623 603 41 0 16130 0
vsize: 64684
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15695 0 0 0 53968 41 0 0 25 0 1 0 421726920 66236416 15624 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15624 603 41 0 16130 0
vsize: 64684
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15696 0 0 0 54969 41 0 0 25 0 1 0 421726920 66236416 15625 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15625 603 41 0 16130 0
vsize: 64684
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15696 0 0 0 55969 41 0 0 25 0 1 0 421726920 66236416 15625 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15625 603 41 0 16130 0
vsize: 64684
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 15698 0 0 0 56969 41 0 0 25 0 1 0 421726920 66236416 15627 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15627 603 41 0 16130 0
vsize: 64684
[startup+580.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 16126 0 0 0 57967 43 0 0 25 0 1 0 421726920 68071424 16055 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16619 16055 603 41 0 16578 0
vsize: 66476
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 16561 0 0 0 58967 44 0 0 25 0 1 0 421726920 69795840 16490 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17040 16490 603 41 0 16999 0
vsize: 68160
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 16837 0 0 0 59966 44 0 0 25 0 1 0 421726920 70987776 16766 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17331 16766 603 41 0 17290 0
vsize: 69324
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 17182 0 0 0 60966 45 0 0 25 0 1 0 421726920 72433664 17111 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17684 17111 603 41 0 17643 0
vsize: 70736
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 17686 0 0 0 61965 47 0 0 25 0 1 0 421726920 74461184 17615 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18179 17615 603 41 0 18138 0
vsize: 72716
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 18100 0 0 0 62963 48 0 0 25 0 1 0 421726920 76169216 18029 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18596 18029 603 41 0 18555 0
vsize: 74384
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 18436 0 0 0 63962 49 0 0 25 0 1 0 421726920 77664256 18365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18961 18365 603 41 0 18920 0
vsize: 75844
[startup+650.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 18926 0 0 0 64962 50 0 0 25 0 1 0 421726920 79683584 18855 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19454 18855 603 41 0 19413 0
vsize: 77816
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 19342 0 0 0 65961 51 0 0 25 0 1 0 421726920 81391616 19271 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19871 19271 603 41 0 19830 0
vsize: 79484
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 19828 0 0 0 66959 53 0 0 25 0 1 0 421726920 83394560 19757 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20360 19757 603 41 0 20319 0
vsize: 81440
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20317 0 0 0 67957 55 0 0 25 0 1 0 421726920 85360640 20246 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20840 20246 603 41 0 20799 0
vsize: 83360
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20720 0 0 0 68956 56 0 0 25 0 1 0 421726920 87076864 20649 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21259 20649 603 41 0 21218 0
vsize: 85036
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 69956 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 70956 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 71956 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 72957 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+740.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 73957 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+750.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20987 0 0 0 74957 57 0 0 25 0 1 0 421726920 88129536 20915 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20915 603 41 0 21475 0
vsize: 86064
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20989 0 0 0 75957 57 0 0 25 0 1 0 421726920 88129536 20917 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21516 20917 603 41 0 21475 0
vsize: 86064
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20989 0 0 0 76957 57 0 0 25 0 1 0 421726920 87932928 20874 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20874 603 41 0 21427 0
vsize: 85872
[startup+780.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20989 0 0 0 77957 57 0 0 25 0 1 0 421726920 87932928 20874 4294967295 134512640 134672761 3221224544 3221223584 134613128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20874 603 41 0 21427 0
vsize: 85872
[startup+790.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20989 0 0 0 78958 57 0 0 25 0 1 0 421726920 87932928 20874 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20874 603 41 0 21427 0
vsize: 85872
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20990 0 0 0 79958 57 0 0 25 0 1 0 421726920 87932928 20875 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20875 603 41 0 21427 0
vsize: 85872
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20990 0 0 0 80958 57 0 0 25 0 1 0 421726920 87932928 20875 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20875 603 41 0 21427 0
vsize: 85872
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20990 0 0 0 81958 57 0 0 25 0 1 0 421726920 87932928 20875 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20875 603 41 0 21427 0
vsize: 85872
[startup+830.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 82958 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 83959 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 84959 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 85959 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 86959 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 87959 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 88960 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 89960 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+910.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 90960 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+920.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 91960 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 92960 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 93961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 94961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+960.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 95961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 96961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 97961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+990.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 98961 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 99962 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 100962 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 101962 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 102962 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 103962 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 104963 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 105963 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 106963 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 107963 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223332 1074972064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 108963 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 109964 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 110964 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223584 134612634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 111964 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20991 0 0 0 112964 57 0 0 25 0 1 0 421726920 87932928 20876 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20876 603 41 0 21427 0
vsize: 85872
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20992 0 0 0 113964 57 0 0 25 0 1 0 421726920 87932928 20877 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20877 603 41 0 21427 0
vsize: 85872
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20994 0 0 0 114965 57 0 0 25 0 1 0 421726920 87932928 20879 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20879 603 41 0 21427 0
vsize: 85872
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20994 0 0 0 115965 57 0 0 25 0 1 0 421726920 87932928 20879 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20879 603 41 0 21427 0
vsize: 85872
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20995 0 0 0 116965 57 0 0 25 0 1 0 421726920 87932928 20880 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20880 603 41 0 21427 0
vsize: 85872
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20995 0 0 0 117965 57 0 0 25 0 1 0 421726920 87932928 20880 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20880 603 41 0 21427 0
vsize: 85872
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20995 0 0 0 118965 57 0 0 25 0 1 0 421726920 87932928 20880 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20880 603 41 0 21427 0
vsize: 85872
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5531
Raw data (stat): 5531 (minisat+) R 5530 32461 32460 0 -1 0 20995 0 0 0 119965 57 0 0 25 0 1 0 421726920 87932928 20880 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21468 20880 603 41 0 21427 0
vsize: 85872
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5531
Raw data (stat): 5531 (minisat+) Z 5530 32461 32460 0 -1 12 20995 0 0 0 119966 61 0 0 25 0 1 0 421726920 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.08
CPU time (s): 1200.27
CPU user time (s): 1199.66
CPU system time (s): 0.612906
CPU usage (%): 100.016
Max. virtual memory (Kb): 86064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####