Some explanations

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

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_50_pb.cnf.cr.opb
MD5SUM2cb05b3a6451c60276a625949666f14e
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 51
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.12498
Number of variables4000
Total number of constraints180
Number of constraints which are clauses100
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint40
Maximum length of a constraint50

Trace number 6153 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-14 03:32:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4531 boxname=wulflinc28 idbench=19 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2cb05b3a6451c60276a625949666f14e  /oldhome/oroussel/tmp/wulflinc28/normalized-chnl40_50_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc28/normalized-chnl40_50_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc28/normalized-chnl40_50_pb.cnf.cr.opb
IDLAUNCH: 4531
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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	: 3
cpu MHz		: 451.077
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:        884332 kB
Buffers:         35828 kB
Cached:          77660 kB
SwapCached:          4 kB
Active:          53716 kB
Inactive:        63572 kB
HighTotal:      131008 kB
HighFree:        48748 kB
LowTotal:       903652 kB
LowFree:        835584 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27432 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:52:02 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4531 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................
c ---[  79]---> BDD-cost:   97
c ---[  78]---> BDD-cost:   97
c ---[  77]---> BDD-cost:   97
c ---[  76]---> BDD-cost:   97
c ---[  75]---> BDD-cost:   97
c ---[  74]---> BDD-cost:   97
c ---[  73]---> BDD-cost:   97
c ---[  72]---> BDD-cost:   97
c ---[  71]---> BDD-cost:   97
c ---[  70]---> BDD-cost:   97
c ---[  69]---> BDD-cost:   97
c ---[  68]---> BDD-cost:   97
c ---[  67]---> BDD-cost:   97
c ---[  66]---> BDD-cost:   97
c ---[  65]---> BDD-cost:   97
c ---[  64]---> BDD-cost:   97
c ---[  63]---> BDD-cost:   97
c ---[  62]---> BDD-cost:   97
c ---[  61]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   97
c ---[  59]---> BDD-cost:   97
c ---[  58]---> BDD-cost:   97
c ---[  57]---> BDD-cost:   97
c ---[  56]---> BDD-cost:   97
c ---[  55]---> BDD-cost:   97
c ---[  54]---> BDD-cost:   97
c ---[  53]---> BDD-cost:   97
c ---[  52]---> BDD-cost:   97
c ---[  51]---> BDD-cost:   97
c ---[  50]---> BDD-cost:   97
c ---[  49]---> BDD-cost:   97
c ---[  48]---> BDD-cost:   97
c ---[  47]---> BDD-cost:   97
c ---[  46]---> BDD-cost:   97
c ---[  45]---> BDD-cost:   97
c ---[  44]---> BDD-cost:   97
c ---[  43]---> BDD-cost:   97
c ---[  42]---> BDD-cost:   97
c ---[  41]---> BDD-cost:   97
c ---[  40]---> BDD-cost:   97
c ---[  39]---> BDD-cost:   97
c ---[  38]---> BDD-cost:   97
c ---[  37]---> BDD-cost:   97
c ---[  36]---> BDD-cost:   97
c ---[  35]---> BDD-cost:   97
c ---[  34]---> BDD-cost:   97
c ---[  33]---> BDD-cost:   97
c ---[  32]---> BDD-cost:   97
c ---[  31]---> BDD-cost:   97
c ---[  30]---> BDD-cost:   97
c ---[  29]---> BDD-cost:   97
c ---[  28]---> BDD-cost:   97
c ---[  27]---> BDD-cost:   97
c ---[  26]---> BDD-cost:   97
c ---[  25]---> BDD-cost:   97
c ---[  24]---> BDD-cost:   97
c ---[  23]---> BDD-cost:   97
c ---[  22]---> BDD-cost:   97
c ---[  21]---> BDD-cost:   97
c ---[  20]---> BDD-cost:   97
c ---[  19]---> BDD-cost:   97
c ---[  18]---> BDD-cost:   97
c ---[  17]---> BDD-cost:   97
c ---[  16]---> BDD-cost:   97
c ---[  15]---> BDD-cost:   97
c ---[  14]---> BDD-cost:   97
c ---[  13]---> BDD-cost:   97
c ---[  12]---> BDD-cost:   97
c ---[  11]---> BDD-cost:   97
c ---[  10]---> BDD-cost:   97
c ---[   9]---> BDD-cost:   97
c ---[   8]---> BDD-cost:   97
c ---[   7]---> BDD-cost:   97
c ---[   6]---> BDD-cost:   97
c ---[   5]---> BDD-cost:   97
c ---[   4]---> BDD-cost:   97
c ---[   3]---> BDD-cost:   97
c ---[   2]---> BDD-cost:   97
c ---[   1]---> BDD-cost:   97
c ---[   0]---> BDD-cost:   97
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34660    99840 |   11553       0        0     nan |  0.000 % |
c |       100 |   34545    99495 |   12708      51      267     5.2 |  0.876 % |
c |       250 |   34060    98040 |   13979      22       56     2.5 |  1.701 % |
c |       475 |   33376    95990 |   15377      43      199     4.6 |  2.866 % |
c |       812 |   32386    93020 |   16914      54     1136    21.0 |  4.549 % |
c |      1321 |   32271    92675 |   18606     536   106253   198.2 |  4.745 % |
c |      2081 |   31526    90440 |   20466    1072   214962   200.5 |  6.012 % |
c |      3221 |   30986    88820 |   22513    2045   552817   270.3 |  6.930 % |
c |      4929 |   29716    85010 |   24764    3294   818307   248.4 |  9.099 % |
c |      7494 |   28871    82475 |   27241    5511  1332684   241.8 | 10.527 % |
c |     11338 |   27931    79655 |   29965    9044  2826451   312.5 | 12.126 % |
c |     17108 |   26061    74045 |   32962   14130  4357496   308.4 | 15.306 % |
c |     25759 |   24936    70670 |   36258   22395  6891457   307.7 | 17.219 % |
c |     38733 |   22356    62930 |   39884   34504 10805010   313.2 | 21.607 % |
c |     58196 |   20796    58250 |   43872   22700  7431040   327.4 | 24.260 % |
c |     87389 |   19466    54260 |   48259   15300  5197906   339.7 | 26.522 % |
c |    131180 |   18526    51440 |   53085   18731  6422408   342.9 | 28.121 % |
c |    196864 |   17833    49365 |   58394   38953 15584083   400.1 | 29.303 % |
#### 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.84 0.94 0.90 2/54 20712
Raw data (stat): 20712 (runsolver) R 20711 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481378192 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 1535 0 0 0 994 4 0 0 25 0 1 0 481378192 8118272 1513 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1982 1513 603 41 0 1941 0
vsize: 7928
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 2117 0 0 0 1992 6 0 0 25 0 1 0 481378192 10547200 2095 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2575 2095 603 41 0 2534 0
vsize: 10300
[startup+30.0016 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 2544 0 0 0 2990 7 0 0 25 0 1 0 481378192 12304384 2522 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3004 2522 603 41 0 2963 0
vsize: 12016
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 3986 0 0 0 3986 11 0 0 25 0 1 0 481378192 18100224 3964 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4419 3964 603 41 0 4378 0
vsize: 17676
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 4133 0 0 0 4986 11 0 0 25 0 1 0 481378192 18821120 4111 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4111 603 41 0 4554 0
vsize: 18380
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 4364 0 0 0 5986 12 0 0 25 0 1 0 481378192 19763200 4342 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4825 4342 603 41 0 4784 0
vsize: 19300
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 4525 0 0 0 6985 12 0 0 25 0 1 0 481378192 20434944 4503 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4989 4503 603 41 0 4948 0
vsize: 19956
[startup+80.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 4785 0 0 0 7984 13 0 0 25 0 1 0 481378192 21381120 4763 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5220 4763 603 41 0 5179 0
vsize: 20880
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 4806 0 0 0 8984 13 0 0 25 0 1 0 481378192 21516288 4784 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5253 4784 603 41 0 5212 0
vsize: 21012
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 5303 0 0 0 9983 14 0 0 25 0 1 0 481378192 23535616 5281 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5746 5281 603 41 0 5705 0
vsize: 22984
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 5954 0 0 0 10982 16 0 0 25 0 1 0 481378192 26234880 5932 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6405 5932 603 41 0 6364 0
vsize: 25620
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 6639 0 0 0 11980 18 0 0 25 0 1 0 481378192 29061120 6617 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7095 6617 603 41 0 7054 0
vsize: 28380
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 6756 0 0 0 12980 18 0 0 25 0 1 0 481378192 29466624 6734 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6734 603 41 0 7153 0
vsize: 28776
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 7264 0 0 0 13978 20 0 0 25 0 1 0 481378192 31604736 7242 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7716 7242 603 41 0 7675 0
vsize: 30864
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 7761 0 0 0 14978 21 0 0 25 0 1 0 481378192 33632256 7739 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8211 7739 603 41 0 8170 0
vsize: 32844
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 8151 0 0 0 15977 22 0 0 25 0 1 0 481378192 35250176 8129 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8606 8129 603 41 0 8565 0
vsize: 34424
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 8520 0 0 0 16976 22 0 0 25 0 1 0 481378192 36732928 8498 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 8498 603 41 0 8927 0
vsize: 35872
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9229 0 0 0 17974 24 0 0 25 0 1 0 481378192 39694336 9207 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9691 9207 603 41 0 9650 0
vsize: 38764
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9395 0 0 0 18974 25 0 0 25 0 1 0 481378192 40370176 9373 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9856 9373 603 41 0 9815 0
vsize: 39424
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9507 0 0 0 19974 25 0 0 25 0 1 0 481378192 40779776 9485 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9956 9485 603 41 0 9915 0
vsize: 39824
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9780 0 0 0 20974 25 0 0 25 0 1 0 481378192 41861120 9758 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10220 9758 603 41 0 10179 0
vsize: 40880
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9793 0 0 0 21975 25 0 0 25 0 1 0 481378192 41996288 9771 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10253 9771 603 41 0 10212 0
vsize: 41012
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9954 0 0 0 22975 25 0 0 25 0 1 0 481378192 42663936 9932 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10416 9932 603 41 0 10375 0
vsize: 41664
[startup+240.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 9993 0 0 0 23975 25 0 0 25 0 1 0 481378192 42799104 9971 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10449 9971 603 41 0 10408 0
vsize: 41796
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 10605 0 0 0 24973 27 0 0 25 0 1 0 481378192 45232128 10583 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11043 10583 603 41 0 11002 0
vsize: 44172
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 10974 0 0 0 25972 28 0 0 25 0 1 0 481378192 46718976 10952 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11406 10952 603 41 0 11365 0
vsize: 45624
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 11302 0 0 0 26971 29 0 0 25 0 1 0 481378192 48074752 11280 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11737 11280 603 41 0 11696 0
vsize: 46948
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 11480 0 0 0 27971 30 0 0 25 0 1 0 481378192 48885760 11458 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11935 11458 603 41 0 11894 0
vsize: 47740
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 11634 0 0 0 28971 30 0 0 25 0 1 0 481378192 49426432 11612 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12067 11612 603 41 0 12026 0
vsize: 48268
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 12045 0 0 0 29970 31 0 0 25 0 1 0 481378192 51179520 12023 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12495 12023 603 41 0 12454 0
vsize: 49980
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 12219 0 0 0 30970 31 0 0 25 0 1 0 481378192 51855360 12197 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 12197 603 41 0 12619 0
vsize: 50640
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 12390 0 0 0 31970 32 0 0 25 0 1 0 481378192 52523008 12368 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12823 12368 603 41 0 12782 0
vsize: 51292
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 12686 0 0 0 32969 32 0 0 25 0 1 0 481378192 53743616 12664 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13121 12664 603 41 0 13080 0
vsize: 52484
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 12951 0 0 0 33969 33 0 0 25 0 1 0 481378192 54947840 12929 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13415 12929 603 41 0 13374 0
vsize: 53660
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 13289 0 0 0 34968 34 0 0 25 0 1 0 481378192 56426496 13267 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13776 13267 603 41 0 13735 0
vsize: 55104
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 13488 0 0 0 35968 34 0 0 25 0 1 0 481378192 57241600 13466 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13975 13466 603 41 0 13934 0
vsize: 55900
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 13526 0 0 0 36968 34 0 0 25 0 1 0 481378192 57376768 13504 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14008 13504 603 41 0 13967 0
vsize: 56032
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 13715 0 0 0 37967 35 0 0 25 0 1 0 481378192 58052608 13693 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14173 13693 603 41 0 14132 0
vsize: 56692
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 14308 0 0 0 38966 36 0 0 25 0 1 0 481378192 60473344 14286 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14764 14286 603 41 0 14723 0
vsize: 59056
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 14841 0 0 0 39964 38 0 0 25 0 1 0 481378192 62783488 14819 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15328 14819 603 41 0 15287 0
vsize: 61312
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 15966 0 0 0 40961 41 0 0 25 0 1 0 481378192 67379200 15944 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16450 15944 603 41 0 16409 0
vsize: 65800
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 41960 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 42960 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 43960 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 44960 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 45961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 46961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 47961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 48961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 49961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 50961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 51961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 52961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 53961 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 54962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 55962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 56962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 57962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 58962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 59962 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+610.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 60963 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16618 0 0 0 61963 43 0 0 25 0 1 0 481378192 69931008 16596 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17073 16596 603 41 0 17032 0
vsize: 68292
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 16711 0 0 0 62962 43 0 0 25 0 1 0 481378192 70336512 16689 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17172 16689 603 41 0 17131 0
vsize: 68688
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 17461 0 0 0 63961 45 0 0 25 0 1 0 481378192 73437184 17439 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17929 17439 603 41 0 17888 0
vsize: 71716
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 18196 0 0 0 64960 46 0 0 25 0 1 0 481378192 76402688 18174 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18653 18174 603 41 0 18612 0
vsize: 74612
[startup+660.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 18597 0 0 0 65958 48 0 0 25 0 1 0 481378192 78143488 18575 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19078 18575 603 41 0 19037 0
vsize: 76312
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19366 0 0 0 66956 50 0 0 25 0 1 0 481378192 81252352 19344 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19837 19344 603 41 0 19796 0
vsize: 79348
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 67956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 68955 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 69956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 70956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 71955 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 72956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 73956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 74956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+760.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 75956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 76956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+780.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 77956 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 78957 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223604 1075346603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 79957 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 80957 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19614 0 0 0 81957 51 0 0 25 0 1 0 481378192 82194432 19592 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20067 19592 603 41 0 20026 0
vsize: 80268
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 19967 0 0 0 82956 52 0 0 25 0 1 0 481378192 83677184 19945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20429 19945 603 41 0 20388 0
vsize: 81716
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 20607 0 0 0 83954 54 0 0 25 0 1 0 481378192 86380544 20585 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21089 20585 603 41 0 21048 0
vsize: 84356
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 21171 0 0 0 84953 55 0 0 25 0 1 0 481378192 88678400 21149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21650 21149 603 41 0 21609 0
vsize: 86600
[startup+860.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22027 0 0 0 85953 56 0 0 25 0 1 0 481378192 92180480 22005 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22505 22005 603 41 0 22464 0
vsize: 90020
[startup+870.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 86951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 87951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+890.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 88952 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+900.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 89951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 90951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+920.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 91951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22465 0 0 0 92951 58 0 0 25 0 1 0 481378192 93937664 22443 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22443 603 41 0 22893 0
vsize: 91736
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 93951 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+950.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 94952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+960.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 95952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+970.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 96952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 97952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+990.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 98952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 99952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 100952 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223648 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22466 0 0 0 101953 58 0 0 25 0 1 0 481378192 93937664 22444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22934 22444 603 41 0 22893 0
vsize: 91736
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 22604 0 0 0 102953 58 0 0 25 0 1 0 481378192 94474240 22582 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23065 22582 603 41 0 23024 0
vsize: 92260
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 23324 0 0 0 103951 60 0 0 25 0 1 0 481378192 97423360 23302 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23785 23302 603 41 0 23744 0
vsize: 95140
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 24055 0 0 0 104950 62 0 0 25 0 1 0 481378192 100515840 24033 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24540 24033 603 41 0 24499 0
vsize: 98160
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25328 0 0 0 105946 65 0 0 25 0 1 0 481378192 105775104 25306 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25824 25306 603 41 0 25783 0
vsize: 103296
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 106945 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 107945 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 108946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 109946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 110946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223728 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 111946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 112946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 113946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 114947 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 115947 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 116947 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 117947 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 118947 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20712
Raw data (stat): 20712 (minisat+) R 20711 10614 10613 0 -1 0 25737 0 0 0 119946 66 0 0 25 0 1 0 481378192 107405312 25715 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 25715 603 41 0 26181 0
vsize: 104888
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20712
Raw data (stat): 20712 (minisat+) Z 20711 10614 10613 0 -1 12 25739 0 0 0 119946 71 0 0 25 0 1 0 481378192 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.47
CPU system time (s): 0.71889
CPU usage (%): 100.011
Max. virtual memory (Kb): 104888
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####