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-chnl50_60_pb.cnf.cr.opb
MD5SUM	6968a43b42bba7df68b13fdfd3b616a1
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	61
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.187971
Number of variables	6000
Total number of constraints	220
Number of constraints which are clauses	120
Number of constraints which are cardinality constraints (but not clauses)	100
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	50
Maximum length of a constraint	60
Trace number 4629

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 19:26:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3406 boxname=wulflinc21 idbench=22 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6968a43b42bba7df68b13fdfd3b616a1  /oldhome/oroussel/tmp/wulflinc21/normalized-chnl50_60_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-chnl50_60_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc21/normalized-chnl50_60_pb.cnf.cr.opb
IDLAUNCH: 3406
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        913640 kB
Buffers:         25728 kB
Cached:          75796 kB
SwapCached:          0 kB
Active:          33304 kB
Inactive:        71116 kB
HighTotal:      131008 kB
HighFree:        51492 kB
LowTotal:       903652 kB
LowFree:        862148 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11056 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:46:48 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3406 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 220 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................
c ---[  99]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  98]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  97]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  96]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  95]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  94]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  93]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  92]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  91]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  90]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  89]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  88]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  87]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  86]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  85]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  84]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  83]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  82]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  81]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  80]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  79]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  78]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  77]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  76]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  75]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  74]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  73]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  72]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  71]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  70]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  69]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  68]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  67]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  66]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  65]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  64]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  63]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  62]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  61]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  60]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  59]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  58]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  57]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  56]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  55]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  54]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  53]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  52]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  51]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  50]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  49]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  48]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  47]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  46]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  45]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  44]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  43]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  42]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  41]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  40]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  39]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  38]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  37]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  36]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  35]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  34]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  33]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  32]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  31]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  30]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  29]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  28]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  27]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  26]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  25]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  24]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  23]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  22]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  21]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  20]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  19]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  18]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  17]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  16]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  15]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  14]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  13]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  12]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  11]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[  10]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   9]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   8]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   7]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   6]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   5]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   4]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   3]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   2]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   1]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ---[   0]---> Adder-cost: 112   maxlim: 58   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   75620   274800 |   25206       0        0     nan |  0.000 % |
c |       100 |   75122   273086 |   27726      25       74     3.0 |  4.443 % |
c |       250 |   74383   270545 |   30499      62      183     3.0 |  5.153 % |
c |       475 |   73209   266507 |   33549     112      334     3.0 |  6.239 % |
c |       812 |   71498   260626 |   36904     198      592     3.0 |  7.864 % |
c |      1318 |   69566   254000 |   40594     422     1342     3.2 |  9.795 % |
c |      2077 |   69158   252624 |   44653    1119     4859     4.3 | 10.148 % |
c |      3216 |   68326   249823 |   49119    2126     8715     4.1 | 10.926 % |
c |      4924 |   65176   238945 |   54031    3327    14407     4.3 | 13.955 % |
c |      7486 |   56740   209696 |   59434    4490    24095     5.4 | 22.028 % |
c |     11331 |   44666   167951 |   65377    6345    44257     7.0 | 33.574 % |
c |     17097 |   39162   149380 |   71915   11238  1393486   124.0 | 39.199 % |
c |     25746 |   39016   148885 |   79107   19850  4999667   251.9 | 39.347 % |
c |     38721 |   39004   148845 |   87017   32823 10740250   327.2 | 39.358 % |
c |     58183 |   38888   148450 |   95719   52262 20965373   401.2 | 39.466 % |
c |     87377 |   38888   148450 |  105291   81456 44781250   549.8 | 39.466 % |
c |    131166 |   38888   148450 |  115820   25555 15553697   608.6 | 39.466 % |
#### 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.05 0.02 0.00 1/55 490
Raw data (stat): 490 (runsolver) R 489 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 355725249 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+9.99986 s]
Raw data (loadavg): 0.19 0.06 0.01 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2020 0 1 0 982 5 0 0 25 0 1 0 355725249 10481664 1940 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2559 1940 603 41 0 2518 0
vsize: 10236
[startup+19.9995 s]
Raw data (loadavg): 0.32 0.09 0.02 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2037 0 1 0 1982 5 0 0 25 0 1 0 355725249 10616832 1957 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1957 603 41 0 2551 0
vsize: 10368
[startup+30.0002 s]
Raw data (loadavg): 0.42 0.12 0.03 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2040 0 1 0 2982 5 0 0 25 0 1 0 355725249 10616832 1960 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1960 603 41 0 2551 0
vsize: 10368
[startup+39.9999 s]
Raw data (loadavg): 0.51 0.14 0.04 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2043 0 1 0 3982 5 0 0 25 0 1 0 355725249 10616832 1963 4294967295 134512640 134672761 3221224544 3221223696 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1963 603 41 0 2551 0
vsize: 10368
[startup+49.9996 s]
Raw data (loadavg): 0.66 0.19 0.06 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2044 0 1 0 4982 5 0 0 25 0 1 0 355725249 10616832 1964 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1964 603 41 0 2551 0
vsize: 10368
[startup+59.9996 s]
Raw data (loadavg): 0.72 0.22 0.07 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2051 0 1 0 5982 5 0 0 25 0 1 0 355725249 10616832 1971 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1971 603 41 0 2551 0
vsize: 10368
[startup+69.9999 s]
Raw data (loadavg): 0.76 0.24 0.08 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2051 0 1 0 6982 6 0 0 25 0 1 0 355725249 10616832 1971 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1971 603 41 0 2551 0
vsize: 10368
[startup+80.0006 s]
Raw data (loadavg): 0.80 0.27 0.09 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2054 0 1 0 7982 6 0 0 25 0 1 0 355725249 10616832 1974 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2592 1974 603 41 0 2551 0
vsize: 10368
[startup+90.0007 s]
Raw data (loadavg): 0.83 0.29 0.10 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2061 0 1 0 8982 6 0 0 25 0 1 0 355725249 10752000 1981 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2625 1981 603 41 0 2584 0
vsize: 10500
[startup+100 s]
Raw data (loadavg): 0.85 0.31 0.10 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2065 0 1 0 9982 6 0 0 25 0 1 0 355725249 10752000 1985 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2625 1985 603 41 0 2584 0
vsize: 10500
[startup+110.001 s]
Raw data (loadavg): 0.87 0.33 0.11 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2080 0 1 0 10982 6 0 0 25 0 1 0 355725249 10752000 2000 4294967295 134512640 134672761 3221224544 3221223668 134566075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2625 2000 603 41 0 2584 0
vsize: 10500
[startup+120.001 s]
Raw data (loadavg): 0.89 0.36 0.12 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 2180 0 1 0 11981 7 0 0 25 0 1 0 355725249 11157504 2100 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2724 2100 603 41 0 2683 0
vsize: 10896
[startup+130.001 s]
Raw data (loadavg): 0.91 0.38 0.13 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 3447 0 1 0 12979 9 0 0 25 0 1 0 355725249 16322560 3367 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3985 3367 603 41 0 3944 0
vsize: 15940
[startup+140.002 s]
Raw data (loadavg): 0.92 0.40 0.14 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 5135 0 1 0 13976 13 0 0 25 0 1 0 355725249 23330816 5055 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5696 5055 603 41 0 5655 0
vsize: 22784
[startup+150.002 s]
Raw data (loadavg): 0.93 0.42 0.15 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 6486 0 1 0 14973 16 0 0 25 0 1 0 355725249 28921856 6406 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7061 6406 603 41 0 7020 0
vsize: 28244
[startup+160.002 s]
Raw data (loadavg): 0.94 0.43 0.16 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 7594 0 1 0 15971 18 0 0 25 0 1 0 355725249 33378304 7514 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8149 7514 603 41 0 8108 0
vsize: 32596
[startup+170.002 s]
Raw data (loadavg): 0.95 0.45 0.17 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 9337 0 1 0 16966 23 0 0 25 0 1 0 355725249 40509440 9257 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9890 9257 603 41 0 9849 0
vsize: 39560
[startup+180.002 s]
Raw data (loadavg): 0.96 0.47 0.18 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 10525 0 1 0 17964 25 0 0 25 0 1 0 355725249 45367296 10445 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11076 10445 603 41 0 11035 0
vsize: 44304
[startup+190.002 s]
Raw data (loadavg): 0.96 0.49 0.18 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 11412 0 1 0 18962 27 0 0 25 0 1 0 355725249 49004544 11332 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11964 11332 603 41 0 11923 0
vsize: 47856
[startup+200.002 s]
Raw data (loadavg): 0.97 0.50 0.19 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 12494 0 1 0 19959 30 0 0 25 0 1 0 355725249 53448704 12414 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13049 12414 603 41 0 13008 0
vsize: 52196
[startup+210.001 s]
Raw data (loadavg): 0.97 0.52 0.20 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 13770 0 1 0 20957 32 0 0 25 0 1 0 355725249 58830848 13690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14363 13690 603 41 0 14322 0
vsize: 57452
[startup+220.001 s]
Raw data (loadavg): 0.98 0.54 0.21 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 15704 0 1 0 21953 37 0 0 25 0 1 0 355725249 66789376 15624 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16306 15624 603 41 0 16265 0
vsize: 65224
[startup+230.001 s]
Raw data (loadavg): 0.98 0.55 0.22 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 16959 0 1 0 22950 40 0 0 25 0 1 0 355725249 71929856 16879 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17561 16879 603 41 0 17520 0
vsize: 70244
[startup+240.001 s]
Raw data (loadavg): 0.98 0.56 0.22 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 18386 0 1 0 23948 42 0 0 25 0 1 0 355725249 77729792 18306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18977 18306 603 41 0 18936 0
vsize: 75908
[startup+250 s]
Raw data (loadavg): 0.98 0.58 0.23 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 19339 0 1 0 24945 45 0 0 25 0 1 0 355725249 81649664 19259 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19934 19259 603 41 0 19893 0
vsize: 79736
[startup+260 s]
Raw data (loadavg): 0.99 0.59 0.24 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 20057 0 1 0 25943 47 0 0 25 0 1 0 355725249 84627456 19977 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20661 19977 603 41 0 20620 0
vsize: 82644
[startup+270 s]
Raw data (loadavg): 0.99 0.60 0.25 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 20588 0 1 0 26942 49 0 0 25 0 1 0 355725249 86781952 20508 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21187 20508 603 41 0 21146 0
vsize: 84748
[startup+280 s]
Raw data (loadavg): 0.99 0.62 0.25 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 21248 0 1 0 27940 51 0 0 25 0 1 0 355725249 89481216 21168 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21846 21168 603 41 0 21805 0
vsize: 87384
[startup+290 s]
Raw data (loadavg): 0.99 0.63 0.26 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 21971 0 1 0 28938 53 0 0 25 0 1 0 355725249 92446720 21891 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22570 21891 603 41 0 22529 0
vsize: 90280
[startup+300 s]
Raw data (loadavg): 0.99 0.64 0.27 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 23198 0 1 0 29936 55 0 0 25 0 1 0 355725249 97452032 23118 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23792 23118 603 41 0 23751 0
vsize: 95168
[startup+309.999 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 24596 0 1 0 30932 58 0 0 25 0 1 0 355725249 103251968 24516 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25208 24516 603 41 0 25167 0
vsize: 100832
[startup+319.999 s]
Raw data (loadavg): 0.99 0.66 0.28 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 25595 0 1 0 31930 61 0 0 25 0 1 0 355725249 107302912 25515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26197 25515 603 41 0 26156 0
vsize: 104788
[startup+329.999 s]
Raw data (loadavg): 0.99 0.67 0.29 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 26469 0 1 0 32928 63 0 0 25 0 1 0 355725249 110944256 26389 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27086 26389 603 41 0 27045 0
vsize: 108344
[startup+339.998 s]
Raw data (loadavg): 0.99 0.68 0.30 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 27332 0 1 0 33926 65 0 0 25 0 1 0 355725249 114475008 27252 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27948 27252 603 41 0 27907 0
vsize: 111792
[startup+349.998 s]
Raw data (loadavg): 0.99 0.69 0.30 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 28285 0 1 0 34924 68 0 0 25 0 1 0 355725249 118259712 28205 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28872 28205 603 41 0 28831 0
vsize: 115488
[startup+359.999 s]
Raw data (loadavg): 0.99 0.70 0.31 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 29159 0 1 0 35922 70 0 0 25 0 1 0 355725249 121937920 29079 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 29079 603 41 0 29729 0
vsize: 119080
[startup+369.998 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 30000 0 1 0 36920 72 0 0 25 0 1 0 355725249 125444096 29920 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30626 29920 603 41 0 30585 0
vsize: 122504
[startup+379.998 s]
Raw data (loadavg): 0.99 0.72 0.33 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 30863 0 1 0 37919 73 0 0 25 0 1 0 355725249 128892928 30783 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31468 30784 603 41 0 31427 0
vsize: 125872
[startup+389.998 s]
Raw data (loadavg): 0.99 0.73 0.33 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 31601 0 1 0 38917 75 0 0 25 0 1 0 355725249 132026368 31521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32233 31521 603 41 0 32192 0
vsize: 128932
[startup+399.997 s]
Raw data (loadavg): 0.99 0.74 0.34 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 32270 0 1 0 39916 76 0 0 25 0 1 0 355725249 134733824 32190 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32894 32190 603 41 0 32853 0
vsize: 131576
[startup+409.997 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 33125 0 1 0 40915 78 0 0 25 0 1 0 355725249 138285056 33045 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33761 33045 603 41 0 33720 0
vsize: 135044
[startup+419.997 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 33791 0 1 0 41913 80 0 0 25 0 1 0 355725249 140972032 33711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34417 33711 603 41 0 34376 0
vsize: 137668
[startup+429.997 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 34576 0 1 0 42911 82 0 0 25 0 1 0 355725249 144498688 34496 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35278 34496 603 41 0 35237 0
vsize: 141112
[startup+439.997 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 35169 0 1 0 43910 83 0 0 25 0 1 0 355725249 146952192 35089 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35877 35089 603 41 0 35836 0
vsize: 143508
[startup+449.997 s]
Raw data (loadavg): 0.99 0.78 0.37 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 35842 0 1 0 44909 84 0 0 25 0 1 0 355725249 149790720 35762 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36570 35762 603 41 0 36529 0
vsize: 146280
[startup+459.997 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 36379 0 1 0 45908 85 0 0 25 0 1 0 355725249 151969792 36299 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37102 36299 603 41 0 37061 0
vsize: 148408
[startup+469.997 s]
Raw data (loadavg): 0.99 0.79 0.38 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 36847 0 1 0 46906 87 0 0 25 0 1 0 355725249 153845760 36767 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37560 36767 603 41 0 37519 0
vsize: 150240
[startup+479.997 s]
Raw data (loadavg): 0.99 0.80 0.39 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 37488 0 1 0 47905 89 0 0 25 0 1 0 355725249 156549120 37408 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38220 37408 603 41 0 38179 0
vsize: 152880
[startup+489.996 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 38124 0 1 0 48904 90 0 0 25 0 1 0 355725249 159158272 38044 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38857 38044 603 41 0 38816 0
vsize: 155428
[startup+499.996 s]
Raw data (loadavg): 0.99 0.81 0.40 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 38597 0 1 0 49903 91 0 0 25 0 1 0 355725249 161042432 38517 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39317 38517 603 41 0 39276 0
vsize: 157268
[startup+509.996 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 39124 0 1 0 50901 93 0 0 25 0 1 0 355725249 163213312 39044 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39847 39044 603 41 0 39806 0
vsize: 159388
[startup+519.995 s]
Raw data (loadavg): 0.99 0.82 0.41 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 39681 0 1 0 51900 95 0 0 25 0 1 0 355725249 165543936 39601 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40416 39601 603 41 0 40375 0
vsize: 161664
[startup+529.996 s]
Raw data (loadavg): 1.07 0.84 0.42 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 40278 0 1 0 52899 96 0 0 25 0 1 0 355725249 168083456 40198 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41036 40198 603 41 0 40995 0
vsize: 164144
[startup+539.996 s]
Raw data (loadavg): 1.06 0.85 0.43 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 40900 0 1 0 53898 97 0 0 25 0 1 0 355725249 170532864 40820 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41634 40820 603 41 0 41593 0
vsize: 166536
[startup+549.995 s]
Raw data (loadavg): 1.05 0.85 0.44 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 41356 0 1 0 54897 98 0 0 25 0 1 0 355725249 172408832 41276 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42092 41276 603 41 0 42051 0
vsize: 168368
[startup+559.996 s]
Raw data (loadavg): 1.04 0.86 0.44 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 41862 0 1 0 55896 100 0 0 25 0 1 0 355725249 174559232 41782 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42617 41782 603 41 0 42576 0
vsize: 170468
[startup+569.996 s]
Raw data (loadavg): 1.04 0.86 0.45 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 42507 0 1 0 56894 101 0 0 25 0 1 0 355725249 177168384 42427 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43254 42427 603 41 0 43213 0
vsize: 173016
[startup+579.996 s]
Raw data (loadavg): 1.03 0.86 0.45 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 43126 0 1 0 57893 103 0 0 25 0 1 0 355725249 179765248 43046 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43888 43046 603 41 0 43847 0
vsize: 175552
[startup+589.996 s]
Raw data (loadavg): 1.03 0.87 0.46 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 43621 0 1 0 58892 103 0 0 25 0 1 0 355725249 181772288 43541 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44378 43541 603 41 0 44337 0
vsize: 177512
[startup+599.996 s]
Raw data (loadavg): 1.02 0.87 0.46 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 43975 0 1 0 59892 104 0 0 25 0 1 0 355725249 183107584 43895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44704 43895 603 41 0 44663 0
vsize: 178816
[startup+609.996 s]
Raw data (loadavg): 1.02 0.88 0.47 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 44440 0 1 0 60891 105 0 0 25 0 1 0 355725249 185110528 44360 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45193 44360 603 41 0 45152 0
vsize: 180772
[startup+619.996 s]
Raw data (loadavg): 1.01 0.88 0.47 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 44898 0 1 0 61890 106 0 0 25 0 1 0 355725249 187043840 44818 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45665 44818 603 41 0 45624 0
vsize: 182660
[startup+629.996 s]
Raw data (loadavg): 1.01 0.88 0.48 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 45452 0 1 0 62889 108 0 0 25 0 1 0 355725249 189202432 45372 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46192 45372 603 41 0 46151 0
vsize: 184768
[startup+639.995 s]
Raw data (loadavg): 1.08 0.90 0.49 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 46089 0 1 0 63887 109 0 0 25 0 1 0 355725249 191893504 46009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46849 46009 603 41 0 46808 0
vsize: 187396
[startup+649.995 s]
Raw data (loadavg): 1.15 0.92 0.50 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 46637 0 1 0 64886 111 0 0 25 0 1 0 355725249 194035712 46557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47372 46557 603 41 0 47331 0
vsize: 189488
[startup+659.995 s]
Raw data (loadavg): 1.13 0.93 0.50 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 47269 0 1 0 65884 112 0 0 25 0 1 0 355725249 196657152 47189 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48012 47189 603 41 0 47971 0
vsize: 192048
[startup+669.994 s]
Raw data (loadavg): 1.11 0.93 0.51 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 47792 0 1 0 66883 114 0 0 25 0 1 0 355725249 198807552 47712 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48537 47712 603 41 0 48496 0
vsize: 194148
[startup+679.995 s]
Raw data (loadavg): 1.09 0.93 0.51 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 48334 0 1 0 67881 116 0 0 25 0 1 0 355725249 201117696 48254 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49101 48254 603 41 0 49060 0
vsize: 196404
[startup+689.995 s]
Raw data (loadavg): 1.08 0.93 0.52 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 49686 0 1 0 68878 119 0 0 25 0 1 0 355725249 206540800 49606 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50425 49606 603 41 0 50384 0
vsize: 201700
[startup+699.994 s]
Raw data (loadavg): 1.06 0.93 0.52 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 51132 0 1 0 69875 122 0 0 25 0 1 0 355725249 212467712 51052 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51872 51052 603 41 0 51831 0
vsize: 207488
[startup+709.995 s]
Raw data (loadavg): 1.05 0.93 0.53 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 52730 0 1 0 70872 125 0 0 25 0 1 0 355725249 219099136 52650 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53491 52650 603 41 0 53450 0
vsize: 213964
[startup+719.995 s]
Raw data (loadavg): 1.04 0.94 0.53 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 53957 0 1 0 71869 128 0 0 25 0 1 0 355725249 224112640 53877 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54715 53877 603 41 0 54674 0
vsize: 218860
[startup+729.995 s]
Raw data (loadavg): 1.04 0.94 0.54 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 55142 0 1 0 72866 131 0 0 25 0 1 0 355725249 228974592 55062 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55902 55062 603 41 0 55861 0
vsize: 223608
[startup+739.996 s]
Raw data (loadavg): 1.03 0.94 0.54 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 56101 0 1 0 73864 134 0 0 25 0 1 0 355725249 232865792 56021 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56852 56021 603 41 0 56811 0
vsize: 227408
[startup+749.996 s]
Raw data (loadavg): 1.03 0.94 0.55 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 57046 0 1 0 74862 136 0 0 25 0 1 0 355725249 236810240 56966 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57815 56966 603 41 0 57774 0
vsize: 231260
[startup+759.996 s]
Raw data (loadavg): 1.02 0.94 0.55 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 58071 0 1 0 75860 138 0 0 25 0 1 0 355725249 240971776 57991 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58831 57991 603 41 0 58790 0
vsize: 235324
[startup+769.996 s]
Raw data (loadavg): 1.10 0.96 0.56 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 59162 0 1 0 76857 140 0 0 25 0 1 0 355725249 245436416 59082 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59921 59082 603 41 0 59880 0
vsize: 239684
[startup+779.997 s]
Raw data (loadavg): 1.08 0.96 0.56 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 60094 0 1 0 77856 142 0 0 25 0 1 0 355725249 249221120 60014 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60845 60014 603 41 0 60804 0
vsize: 243380
[startup+789.997 s]
Raw data (loadavg): 1.07 0.96 0.57 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 61081 0 1 0 78854 145 0 0 25 0 1 0 355725249 253317120 61001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61845 61001 603 41 0 61804 0
vsize: 247380
[startup+799.997 s]
Raw data (loadavg): 1.06 0.96 0.57 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 62080 0 1 0 79851 148 0 0 25 0 1 0 355725249 257392640 62000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62840 62000 603 41 0 62799 0
vsize: 251360
[startup+809.997 s]
Raw data (loadavg): 1.05 0.96 0.58 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 62981 0 1 0 80849 149 0 0 25 0 1 0 355725249 261201920 62901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63770 62901 603 41 0 63729 0
vsize: 255080
[startup+819.996 s]
Raw data (loadavg): 1.04 0.97 0.58 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 63716 0 1 0 81848 151 0 0 25 0 1 0 355725249 264155136 63636 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64491 63636 603 41 0 64450 0
vsize: 257964
[startup+829.997 s]
Raw data (loadavg): 1.03 0.97 0.58 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 64281 0 1 0 82847 152 0 0 25 0 1 0 355725249 266477568 64201 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65058 64201 603 41 0 65017 0
vsize: 260232
[startup+839.997 s]
Raw data (loadavg): 1.03 0.97 0.59 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 65183 0 1 0 83845 154 0 0 25 0 1 0 355725249 270254080 65103 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65980 65103 603 41 0 65939 0
vsize: 263920
[startup+849.996 s]
Raw data (loadavg): 1.02 0.97 0.59 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 66427 0 1 0 84843 156 0 0 25 0 1 0 355725249 275357696 66347 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67226 66347 603 41 0 67185 0
vsize: 268904
[startup+859.996 s]
Raw data (loadavg): 1.02 0.97 0.60 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 67463 0 1 0 85841 158 0 0 25 0 1 0 355725249 279527424 67383 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68244 67383 603 41 0 68203 0
vsize: 272976
[startup+869.997 s]
Raw data (loadavg): 1.02 0.97 0.60 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 68521 0 1 0 86837 161 0 0 25 0 1 0 355725249 283889664 68441 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69309 68441 603 41 0 69268 0
vsize: 277236
[startup+879.997 s]
Raw data (loadavg): 1.01 0.97 0.60 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 69362 0 1 0 87836 163 0 0 25 0 1 0 355725249 287268864 69282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70134 69282 603 41 0 70093 0
vsize: 280536
[startup+889.997 s]
Raw data (loadavg): 1.01 0.97 0.61 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 70218 0 1 0 88834 165 0 0 25 0 1 0 355725249 290889728 70138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71018 70138 603 41 0 70977 0
vsize: 284072
[startup+899.997 s]
Raw data (loadavg): 1.01 0.97 0.61 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 70957 0 1 0 89832 167 0 0 25 0 1 0 355725249 293842944 70877 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71739 70877 603 41 0 71698 0
vsize: 286956
[startup+909.997 s]
Raw data (loadavg): 1.01 0.97 0.62 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 71780 0 1 0 90831 168 0 0 25 0 1 0 355725249 297291776 71700 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 72581 71700 603 41 0 72540 0
vsize: 290324
[startup+919.997 s]
Raw data (loadavg): 1.00 0.97 0.62 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 72624 0 1 0 91830 169 0 0 25 0 1 0 355725249 300785664 72544 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73434 72544 603 41 0 73393 0
vsize: 293736
[startup+929.998 s]
Raw data (loadavg): 1.00 0.97 0.62 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73515 0 1 0 92828 171 0 0 25 0 1 0 355725249 304394240 73435 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74315 73435 603 41 0 74274 0
vsize: 297260
[startup+939.999 s]
Raw data (loadavg): 1.00 0.97 0.63 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 93828 172 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+949.998 s]
Raw data (loadavg): 1.00 0.97 0.63 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 94828 172 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+959.998 s]
Raw data (loadavg): 1.00 0.97 0.64 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 95828 172 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+969.999 s]
Raw data (loadavg): 1.00 0.97 0.64 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 96828 172 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+979.999 s]
Raw data (loadavg): 1.00 0.97 0.64 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 97828 172 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+989.999 s]
Raw data (loadavg): 1.00 0.97 0.64 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 98828 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1000 s]
Raw data (loadavg): 1.00 0.97 0.65 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 99828 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.65 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 100828 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.65 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 101828 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.66 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 102827 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.66 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 103827 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1050 s]
Raw data (loadavg): 1.00 0.97 0.66 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 104827 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1060 s]
Raw data (loadavg): 1.00 0.97 0.66 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 105827 173 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.67 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 106827 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.67 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 107828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.67 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 108828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 109828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 110828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 111828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 112827 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 113827 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1150 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 114827 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1160 s]
Raw data (loadavg): 1.00 0.97 0.69 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 115828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1170 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 116828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1180 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 117828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1190 s]
Raw data (loadavg): 1.00 0.97 0.70 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 118828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
[startup+1200 s]
Raw data (loadavg): 1.00 0.97 0.71 2/55 490
Raw data (stat): 490 (minisat+) R 489 30927 30926 0 -1 0 73745 0 1 0 119828 174 0 0 25 0 1 0 355725249 305336320 73665 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74545 73665 603 41 0 74504 0
vsize: 298180
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.97 0.71 1/55 490
Raw data (stat): 490 (minisat+) Z 489 30927 30926 0 -1 12 73747 0 1 0 119828 188 0 0 25 0 1 0 355725249 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.14
CPU time (s): 1200.17
CPU user time (s): 1198.29
CPU system time (s): 1.88471
CPU usage (%): 100.003
Max. virtual memory (Kb): 298180
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####