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 5720 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 01:38:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4155 boxname=wulflinc30 idbench=19 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2cb05b3a6451c60276a625949666f14e  /oldhome/oroussel/tmp/wulflinc30/normalized-chnl40_50_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-chnl40_50_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc30/normalized-chnl40_50_pb.cnf.cr.opb
IDLAUNCH: 4155
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        732744 kB
Buffers:         38032 kB
Cached:         223224 kB
SwapCached:          0 kB
Active:          82192 kB
Inactive:       181912 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        732492 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            31976 kB
Committed_AS:    63520 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:58:22 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4155 7 1200.2 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 |   19380    54160 |    6460       0        0     nan |  0.000 % |
c |       103 |   19380    54160 |    7106     103    15224   147.8 |  0.680 % |
c |       264 |   19380    54160 |    7816     264    48573   184.0 |  0.680 % |
c |       491 |   19380    54160 |    8598     491    85624   174.4 |  0.680 % |
c |       828 |   19380    54160 |    9458     828   154823   187.0 |  0.680 % |
c |      1334 |   19380    54160 |   10403    1334   306589   229.8 |  0.680 % |
c |      2093 |   19380    54160 |   11444    2093   485053   231.8 |  0.680 % |
c |      3234 |   19380    54160 |   12588    3234   825279   255.2 |  0.680 % |
c |      4943 |   19380    54160 |   13847    4943  1417289   286.7 |  0.680 % |
c |      7505 |   19380    54160 |   15232    7505  2438701   324.9 |  0.680 % |
c |     11349 |   19380    54160 |   16755   11349  3669460   323.3 |  0.680 % |
c |     17115 |   19380    54160 |   18431   17115  6183322   361.3 |  0.680 % |
c |     25765 |   19380    54160 |   20274   14106  6524975   462.6 |  0.680 % |
c |     38745 |   19380    54160 |   22301   13797  6591558   477.8 |  0.680 % |
c |     58212 |   19380    54160 |   24531   17990  8193323   455.4 |  0.680 % |
c |     87406 |   19380    54160 |   26985   14543  4843174   333.0 |  0.680 % |
c |    131196 |   19380    54160 |   29683   19996 12157179   608.0 |  0.680 % |
c |    196881 |   19380    54160 |   32651   14613  5410723   370.3 |  0.680 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.92 2/54 16920
Raw data (stat): 16920 (runsolver) R 16919 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480689102 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 3204 0 0 0 990 8 0 0 25 0 1 0 480689102 14917632 3182 4294967295 134512640 134672761 3221224528 3221223632 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3642 3182 603 41 0 3601 0
vsize: 14568
[startup+20.001 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 5032 0 0 0 1984 13 0 0 25 0 1 0 480689102 22487040 5010 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5490 5010 603 41 0 5449 0
vsize: 21960
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 6442 0 0 0 2981 17 0 0 25 0 1 0 480689102 28282880 6420 4294967295 134512640 134672761 3221224528 3221223632 134554912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6905 6420 603 41 0 6864 0
vsize: 27620
[startup+40.0019 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 7431 0 0 0 3978 20 0 0 25 0 1 0 480689102 32276480 7409 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7880 7409 603 41 0 7839 0
vsize: 31520
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 9031 0 0 0 4974 24 0 0 25 0 1 0 480689102 38879232 9009 4294967295 134512640 134672761 3221224528 3221223696 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9492 9009 603 41 0 9451 0
vsize: 37968
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 10278 0 0 0 5971 27 0 0 25 0 1 0 480689102 44011520 10256 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10745 10256 603 41 0 10704 0
vsize: 42980
[startup+70.0013 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 10689 0 0 0 6970 29 0 0 25 0 1 0 480689102 45629440 10667 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11140 10667 603 41 0 11099 0
vsize: 44560
[startup+80.0018 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 10689 0 0 0 7970 29 0 0 25 0 1 0 480689102 45629440 10667 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11140 10667 603 41 0 11099 0
vsize: 44560
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 10689 0 0 0 8970 29 0 0 25 0 1 0 480689102 45629440 10667 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11140 10667 603 41 0 11099 0
vsize: 44560
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12177 0 0 0 9967 32 0 0 25 0 1 0 480689102 51691520 12155 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12620 12155 603 41 0 12579 0
vsize: 50480
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12976 0 0 0 10965 34 0 0 25 0 1 0 480689102 55066624 12954 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13444 12954 603 41 0 13403 0
vsize: 53776
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12976 0 0 0 11965 35 0 0 25 0 1 0 480689102 55066624 12954 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13444 12954 603 41 0 13403 0
vsize: 53776
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12976 0 0 0 12964 35 0 0 25 0 1 0 480689102 55066624 12954 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13444 12954 603 41 0 13403 0
vsize: 53776
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12976 0 0 0 13964 35 0 0 25 0 1 0 480689102 55066624 12954 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13444 12954 603 41 0 13403 0
vsize: 53776
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 12976 0 0 0 14964 36 0 0 25 0 1 0 480689102 55066624 12954 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13444 12954 603 41 0 13403 0
vsize: 53776
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 13344 0 0 0 15963 36 0 0 25 0 1 0 480689102 56557568 13322 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13808 13322 603 41 0 13767 0
vsize: 55232
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14130 0 0 0 16961 39 0 0 25 0 1 0 480689102 59801600 14108 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14600 14108 603 41 0 14559 0
vsize: 58400
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14770 0 0 0 17959 41 0 0 25 0 1 0 480689102 62365696 14748 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14748 603 41 0 15185 0
vsize: 60904
[startup+190.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14771 0 0 0 18959 41 0 0 25 0 1 0 480689102 62365696 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14749 603 41 0 15185 0
vsize: 60904
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14771 0 0 0 19959 42 0 0 25 0 1 0 480689102 62365696 14749 4294967295 134512640 134672761 3221224528 3221223632 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14749 603 41 0 15185 0
vsize: 60904
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14771 0 0 0 20958 42 0 0 25 0 1 0 480689102 62365696 14749 4294967295 134512640 134672761 3221224528 3221223632 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14749 603 41 0 15185 0
vsize: 60904
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14771 0 0 0 21958 42 0 0 25 0 1 0 480689102 62365696 14749 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14749 603 41 0 15185 0
vsize: 60904
[startup+230.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14771 0 0 0 22958 43 0 0 25 0 1 0 480689102 62365696 14749 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14749 603 41 0 15185 0
vsize: 60904
[startup+240.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 23958 43 0 0 25 0 1 0 480689102 62365696 14751 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15226 14751 603 41 0 15185 0
vsize: 60904
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 24958 43 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 25958 43 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+270.007 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 26958 43 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+280.009 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 27958 44 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+290.009 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 28958 44 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+300.009 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 29958 44 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+310.01 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 30957 44 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+320.009 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 31957 44 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+330.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 32957 45 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+340.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 33957 45 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+350.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 34957 45 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+360.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 35957 45 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+370.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 36956 46 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+380.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 37956 46 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+390.011 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 38956 46 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223632 134559958 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+400.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 39956 47 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+410.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 40956 47 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+420.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 41956 47 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+430.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 42956 47 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+440.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 43956 47 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+450.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 44956 48 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+460.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14773 0 0 0 45956 48 0 0 25 0 1 0 480689102 62361600 14751 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14751 603 41 0 15184 0
vsize: 60900
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 14774 0 0 0 46955 48 0 0 25 0 1 0 480689102 62361600 14752 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15225 14752 603 41 0 15184 0
vsize: 60900
[startup+480.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15478 0 0 0 47954 50 0 0 25 0 1 0 480689102 65200128 15456 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15918 15456 603 41 0 15877 0
vsize: 63672
[startup+490.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 48954 51 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+500.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 49953 51 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+510.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 50953 51 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 51953 51 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+530.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 52953 52 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 53953 52 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+550.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 54953 52 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+560.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15602 0 0 0 55953 52 0 0 25 0 1 0 480689102 65740800 15580 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15580 603 41 0 16009 0
vsize: 64200
[startup+570.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 15603 0 0 0 56953 52 0 0 25 0 1 0 480689102 65740800 15581 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16050 15581 603 41 0 16009 0
vsize: 64200
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 16153 0 0 0 57952 54 0 0 25 0 1 0 480689102 68120576 16131 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16631 16131 603 41 0 16590 0
vsize: 66524
[startup+590.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 16835 0 0 0 58950 56 0 0 25 0 1 0 480689102 70823936 16813 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17291 16813 603 41 0 17250 0
vsize: 69164
[startup+600.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 17463 0 0 0 59948 58 0 0 25 0 1 0 480689102 73490432 17441 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17942 17441 603 41 0 17901 0
vsize: 71768
[startup+610.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 18255 0 0 0 60945 61 0 0 25 0 1 0 480689102 76750848 18233 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18738 18233 603 41 0 18697 0
vsize: 74952
[startup+620.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 19129 0 0 0 61942 64 0 0 25 0 1 0 480689102 80400384 19107 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19629 19107 603 41 0 19588 0
vsize: 78516
[startup+630.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 19606 0 0 0 62942 64 0 0 25 0 1 0 480689102 82329600 19584 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20100 19584 603 41 0 20059 0
vsize: 80400
[startup+640.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 20091 0 0 0 63941 66 0 0 25 0 1 0 480689102 84353024 20069 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20594 20069 603 41 0 20553 0
vsize: 82376
[startup+650.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 20563 0 0 0 64940 67 0 0 25 0 1 0 480689102 86323200 20541 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21075 20541 603 41 0 21034 0
vsize: 84300
[startup+660.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21116 0 0 0 65939 68 0 0 25 0 1 0 480689102 88641536 21094 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21641 21094 603 41 0 21600 0
vsize: 86564
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 66938 69 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 67937 70 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 68937 70 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 69937 70 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+710.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 70937 71 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223632 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+720.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 71936 71 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+730.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 72937 71 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+740.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 73937 71 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+750.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 74937 72 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+760.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21247 0 0 0 75936 72 0 0 25 0 1 0 480689102 89178112 21225 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21772 21225 603 41 0 21731 0
vsize: 87088
[startup+770.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21282 0 0 0 76936 72 0 0 25 0 1 0 480689102 89440256 21260 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21836 21260 603 41 0 21795 0
vsize: 87344
[startup+780.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 77935 73 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+790.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 78935 74 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+800.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 79935 74 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+810.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 80935 74 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+820.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 81935 75 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+830.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 82934 75 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+840.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 83934 75 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+850.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 84934 76 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+860.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 85934 76 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+870.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 86934 76 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+880.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 87934 76 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+890.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 88934 76 0 0 25 0 1 0 480689102 90521600 21543 4294967295 134512640 134672761 3221224528 3221223712 134558638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22100 21543 603 41 0 22059 0
vsize: 88400
[startup+900.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 89934 76 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+910.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 90933 77 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+920.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 91934 77 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+930.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 92934 77 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+940.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 93934 77 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+950.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21565 0 0 0 94934 77 0 0 25 0 1 0 480689102 90427392 21524 4294967295 134512640 134672761 3221224528 3221223632 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21524 603 41 0 22036 0
vsize: 88308
[startup+960.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 95934 77 0 0 25 0 1 0 480689102 90427392 21525 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22077 21525 603 41 0 22036 0
vsize: 88308
[startup+970.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 96934 77 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+980.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 97934 77 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+990.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 98934 77 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 99934 77 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 100934 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 101934 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 102934 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 103934 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 104934 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 105935 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 106935 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 107935 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21566 0 0 0 108935 78 0 0 25 0 1 0 480689102 90423296 21524 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21524 603 41 0 22035 0
vsize: 88304
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21567 0 0 0 109935 78 0 0 25 0 1 0 480689102 90423296 21525 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21525 603 41 0 22035 0
vsize: 88304
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 110935 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 111935 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 112936 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 113936 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223728 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 114936 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 115936 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21652 0 0 0 116936 78 0 0 25 0 1 0 480689102 90828800 21610 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21610 603 41 0 22134 0
vsize: 88700
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21654 0 0 0 117936 78 0 0 25 0 1 0 480689102 90828800 21612 4294967295 134512640 134672761 3221224528 3221223632 134555128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21612 603 41 0 22134 0
vsize: 88700
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21654 0 0 0 118937 79 0 0 25 0 1 0 480689102 90828800 21612 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21612 603 41 0 22134 0
vsize: 88700
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16920
Raw data (stat): 16920 (minisat+) R 16919 11931 11930 0 -1 0 21654 0 0 0 119937 79 0 0 25 0 1 0 480689102 90828800 21612 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22175 21612 603 41 0 22134 0
vsize: 88700
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 16920
Raw data (stat): 16920 (minisat+) Z 16919 11931 11930 0 -1 12 21656 0 0 0 119937 83 0 0 25 0 1 0 480689102 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.07
CPU time (s): 1200.2
CPU user time (s): 1199.37
CPU system time (s): 0.830873
CPU usage (%): 100.011
Max. virtual memory (Kb): 88700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####