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_41_pb.cnf.cr.opb
MD5SUM3c9e81ddaaf37dd621fe2bc839a3f27f
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 42
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.098984
Number of variables3280
Total number of constraints162
Number of constraints which are clauses82
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 constraint41

Trace number 6150 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-14 03:31:10 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4529 boxname=wulflinc19 idbench=17 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c9e81ddaaf37dd621fe2bc839a3f27f  /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc19/normalized-chnl40_41_pb.cnf.cr.opb
IDLAUNCH: 4529
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        876000 kB
Buffers:         35452 kB
Cached:          89272 kB
SwapCached:         56 kB
Active:          49860 kB
Inactive:        77884 kB
HighTotal:      131008 kB
HighFree:        37604 kB
LowTotal:       903652 kB
LowFree:        838396 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25300 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:51:12 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 4529 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 162 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................
c ---[  79]---> BDD-cost:   79
c ---[  78]---> BDD-cost:   79
c ---[  77]---> BDD-cost:   79
c ---[  76]---> BDD-cost:   79
c ---[  75]---> BDD-cost:   79
c ---[  74]---> BDD-cost:   79
c ---[  73]---> BDD-cost:   79
c ---[  72]---> BDD-cost:   79
c ---[  71]---> BDD-cost:   79
c ---[  70]---> BDD-cost:   79
c ---[  69]---> BDD-cost:   79
c ---[  68]---> BDD-cost:   79
c ---[  67]---> BDD-cost:   79
c ---[  66]---> BDD-cost:   79
c ---[  65]---> BDD-cost:   79
c ---[  64]---> BDD-cost:   79
c ---[  63]---> BDD-cost:   79
c ---[  62]---> BDD-cost:   79
c ---[  61]---> BDD-cost:   79
c ---[  60]---> BDD-cost:   79
c ---[  59]---> BDD-cost:   79
c ---[  58]---> BDD-cost:   79
c ---[  57]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   79
c ---[  55]---> BDD-cost:   79
c ---[  54]---> BDD-cost:   79
c ---[  53]---> BDD-cost:   79
c ---[  52]---> BDD-cost:   79
c ---[  51]---> BDD-cost:   79
c ---[  50]---> BDD-cost:   79
c ---[  49]---> BDD-cost:   79
c ---[  48]---> BDD-cost:   79
c ---[  47]---> BDD-cost:   79
c ---[  46]---> BDD-cost:   79
c ---[  45]---> BDD-cost:   79
c ---[  44]---> BDD-cost:   79
c ---[  43]---> BDD-cost:   79
c ---[  42]---> BDD-cost:   79
c ---[  41]---> BDD-cost:   79
c ---[  40]---> BDD-cost:   79
c ---[  39]---> BDD-cost:   79
c ---[  38]---> BDD-cost:   79
c ---[  37]---> BDD-cost:   79
c ---[  36]---> BDD-cost:   79
c ---[  35]---> BDD-cost:   79
c ---[  34]---> BDD-cost:   79
c ---[  33]---> BDD-cost:   79
c ---[  32]---> BDD-cost:   79
c ---[  31]---> BDD-cost:   79
c ---[  30]---> BDD-cost:   79
c ---[  29]---> BDD-cost:   79
c ---[  28]---> BDD-cost:   79
c ---[  27]---> BDD-cost:   79
c ---[  26]---> BDD-cost:   79
c ---[  25]---> BDD-cost:   79
c ---[  24]---> BDD-cost:   79
c ---[  23]---> BDD-cost:   79
c ---[  22]---> BDD-cost:   79
c ---[  21]---> BDD-cost:   79
c ---[  20]---> BDD-cost:   79
c ---[  19]---> BDD-cost:   79
c ---[  18]---> BDD-cost:   79
c ---[  17]---> BDD-cost:   79
c ---[  16]---> BDD-cost:   79
c ---[  15]---> BDD-cost:   79
c ---[  14]---> BDD-cost:   79
c ---[  13]---> BDD-cost:   79
c ---[  12]---> BDD-cost:   79
c ---[  11]---> BDD-cost:   79
c ---[  10]---> BDD-cost:   79
c ---[   9]---> BDD-cost:   79
c ---[   8]---> BDD-cost:   79
c ---[   7]---> BDD-cost:   79
c ---[   6]---> BDD-cost:   79
c ---[   5]---> BDD-cost:   79
c ---[   4]---> BDD-cost:   79
c ---[   3]---> BDD-cost:   79
c ---[   2]---> BDD-cost:   79
c ---[   1]---> BDD-cost:   79
c ---[   0]---> BDD-cost:   79
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28162    81120 |    9387       0        0     nan |  0.000 % |
c |       100 |   27997    80625 |   10325      27     2140    79.3 |  1.177 % |
c |       250 |   27657    79605 |   11358      34     2527    74.3 |  1.896 % |
c |       476 |   27218    78290 |   12494      49     2561    52.3 |  2.812 % |
c |       813 |   26318    75590 |   13743      80     2795    34.9 |  4.688 % |
c |      1321 |   26168    75140 |   15117     519    83828   161.5 |  4.990 % |
c |      2083 |   25748    73880 |   16629    1139   202046   177.4 |  5.865 % |
c |      3222 |   25228    72320 |   18292    2104   390297   185.5 |  6.948 % |
c |      4932 |   24193    69215 |   20121    3426   708435   206.8 |  9.104 % |
c |      7498 |   22984    65590 |   22134    5592  1334596   238.7 | 11.625 % |
c |     11343 |   21704    61750 |   24347    8970  2331930   260.0 | 14.292 % |
c |     17109 |   19166    54140 |   26782   13866  3975662   286.7 | 19.583 % |
c |     25758 |   18416    51890 |   29460   22249  6701305   301.2 | 21.146 % |
c |     38735 |   17668    49650 |   32406   14788  4504952   304.6 | 22.708 % |
c |     58199 |   16889    47315 |   35647   34019 10751402   316.0 | 24.333 % |
c |     87391 |   15981    44595 |   39211   36341 14534040   399.9 | 26.229 % |
c |    131181 |   15097    41945 |   43133   16553  5983149   361.5 | 28.073 % |
c |    196869 |   14347    39695 |   47446   47245 19939784   422.1 | 29.635 % |
#### 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.91 0.97 0.92 2/55 29123
Raw data (stat): 29123 (runsolver) R 29122 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481364026 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.0005 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 1576 0 0 0 996 2 0 0 25 0 1 0 481364026 8290304 1551 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2024 1551 603 41 0 1983 0
vsize: 8096
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 1991 0 0 0 1994 4 0 0 25 0 1 0 481364026 10043392 1966 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2452 1966 603 41 0 2411 0
vsize: 9808
[startup+30.0001 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 2625 0 0 0 2993 5 0 0 25 0 1 0 481364026 12599296 2600 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3076 2600 603 41 0 3035 0
vsize: 12304
[startup+39.9999 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3024 0 0 0 3992 6 0 0 25 0 1 0 481364026 14221312 2999 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3472 2999 603 41 0 3431 0
vsize: 13888
[startup+49.9999 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3712 0 0 0 4990 8 0 0 25 0 1 0 481364026 17063936 3687 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4166 3687 603 41 0 4125 0
vsize: 16664
[startup+60.0005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 3930 0 0 0 5990 8 0 0 25 0 1 0 481364026 18006016 3905 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4396 3905 603 41 0 4355 0
vsize: 17584
[startup+70.0003 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4092 0 0 0 6990 9 0 0 25 0 1 0 481364026 18546688 4067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4528 4067 603 41 0 4487 0
vsize: 18112
[startup+80.0004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4537 0 0 0 7989 9 0 0 25 0 1 0 481364026 20434944 4512 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4989 4512 603 41 0 4948 0
vsize: 19956
[startup+90.0009 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 4759 0 0 0 8989 10 0 0 25 0 1 0 481364026 21377024 4734 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5219 4734 603 41 0 5178 0
vsize: 20876
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 5045 0 0 0 9988 11 0 0 25 0 1 0 481364026 22454272 5020 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5482 5020 603 41 0 5441 0
vsize: 21928
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 5509 0 0 0 10987 12 0 0 25 0 1 0 481364026 24342528 5484 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5943 5484 603 41 0 5902 0
vsize: 23772
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 6133 0 0 0 11985 14 0 0 25 0 1 0 481364026 26906624 6108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6569 6108 603 41 0 6528 0
vsize: 26276
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 6851 0 0 0 12984 16 0 0 25 0 1 0 481364026 29925376 6826 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7306 6826 603 41 0 7265 0
vsize: 29224
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 7191 0 0 0 13983 17 0 0 25 0 1 0 481364026 31268864 7166 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7634 7166 603 41 0 7593 0
vsize: 30536
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 7860 0 0 0 14982 18 0 0 25 0 1 0 481364026 34095104 7835 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8324 7835 603 41 0 8283 0
vsize: 33296
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 8565 0 0 0 15979 21 0 0 25 0 1 0 481364026 36929536 8540 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9016 8540 603 41 0 8975 0
vsize: 36064
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 8961 0 0 0 16979 21 0 0 25 0 1 0 481364026 38551552 8936 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9412 8936 603 41 0 9371 0
vsize: 37648
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 9407 0 0 0 17978 22 0 0 25 0 1 0 481364026 40439808 9382 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9873 9382 603 41 0 9832 0
vsize: 39492
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 10492 0 0 0 18976 24 0 0 25 0 1 0 481364026 44761088 10467 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10928 10467 603 41 0 10887 0
vsize: 43712
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 10610 0 0 0 19976 24 0 0 25 0 1 0 481364026 45297664 10585 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11059 10585 603 41 0 11018 0
vsize: 44236
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11305 0 0 0 20975 26 0 0 25 0 1 0 481364026 48132096 11280 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11751 11280 603 41 0 11710 0
vsize: 47004
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11583 0 0 0 21974 27 0 0 25 0 1 0 481364026 49344512 11558 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12047 11558 603 41 0 12006 0
vsize: 48188
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 22974 27 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 23974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 24974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 25974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 26973 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 27974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29123
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 11839 0 0 0 28974 28 0 0 25 0 1 0 481364026 50282496 11814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12276 11814 603 41 0 12235 0
vsize: 49104
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 12097 0 0 0 29973 29 0 0 25 0 1 0 481364026 51359744 12072 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12539 12072 603 41 0 12498 0
vsize: 50156
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 12935 0 0 0 30971 31 0 0 25 0 1 0 481364026 54984704 12910 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13424 12910 603 41 0 13383 0
vsize: 53696
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 13377 0 0 0 31970 32 0 0 25 0 1 0 481364026 56733696 13352 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13851 13352 603 41 0 13810 0
vsize: 55404
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 13563 0 0 0 32970 33 0 0 25 0 1 0 481364026 57544704 13538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14049 13538 603 41 0 14008 0
vsize: 56196
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14414 0 0 0 33968 35 0 0 25 0 1 0 481364026 61059072 14389 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14907 14389 603 41 0 14866 0
vsize: 59628
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 34967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 35967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 36967 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 37968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 38968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 39968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223728 134559121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 40968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 14809 0 0 0 41968 36 0 0 25 0 1 0 481364026 62550016 14784 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15271 14784 603 41 0 15230 0
vsize: 61084
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15072 0 0 0 42968 36 0 0 25 0 1 0 481364026 63631360 15047 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15535 15047 603 41 0 15494 0
vsize: 62140
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15338 0 0 0 43968 37 0 0 25 0 1 0 481364026 64716800 15313 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15800 15313 603 41 0 15759 0
vsize: 63200
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 15575 0 0 0 44967 37 0 0 25 0 1 0 481364026 65802240 15550 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16065 15550 603 41 0 16024 0
vsize: 64260
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 16500 0 0 0 45965 40 0 0 25 0 1 0 481364026 69582848 16475 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16988 16475 603 41 0 16947 0
vsize: 67952
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 17570 0 0 0 46962 43 0 0 25 0 1 0 481364026 73900032 17545 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18042 17545 603 41 0 18001 0
vsize: 72168
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 17846 0 0 0 47960 44 0 0 25 0 1 0 481364026 75116544 17821 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18339 17821 603 41 0 18298 0
vsize: 73356
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 18267 0 0 0 48960 45 0 0 25 0 1 0 481364026 76722176 18242 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18731 18242 603 41 0 18690 0
vsize: 74924
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 18822 0 0 0 49959 46 0 0 25 0 1 0 481364026 79020032 18797 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19292 18797 603 41 0 19251 0
vsize: 77168
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 50957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 51957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 52957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 53957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223648 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 54957 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 55958 48 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 56958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 57958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29125
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 58958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 59958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 60958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19603 0 0 0 61958 49 0 0 25 0 1 0 481364026 82247680 19578 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19578 603 41 0 20039 0
vsize: 80320
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 19604 0 0 0 62958 49 0 0 25 0 1 0 481364026 82247680 19579 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20080 19579 603 41 0 20039 0
vsize: 80320
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 63957 50 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20213 603 41 0 20664 0
vsize: 82820
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 64957 50 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20213 603 41 0 20664 0
vsize: 82820
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 65957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20213 603 41 0 20664 0
vsize: 82820
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 66957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223728 134559489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20213 603 41 0 20664 0
vsize: 82820
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20238 0 0 0 67957 51 0 0 25 0 1 0 481364026 84807680 20213 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20213 603 41 0 20664 0
vsize: 82820
[startup+690.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 68957 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+700.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 69957 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+710.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 70958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+720.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 71958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 72958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 73958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20239 0 0 0 74958 51 0 0 25 0 1 0 481364026 84807680 20214 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20705 20214 603 41 0 20664 0
vsize: 82820
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 20311 0 0 0 75958 51 0 0 25 0 1 0 481364026 85078016 20286 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20771 20286 603 41 0 20730 0
vsize: 83084
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21085 0 0 0 76957 52 0 0 25 0 1 0 481364026 88322048 21060 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21563 21060 603 41 0 21522 0
vsize: 86252
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21326 0 0 0 77957 53 0 0 25 0 1 0 481364026 89268224 21301 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21794 21301 603 41 0 21753 0
vsize: 87176
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 21819 0 0 0 78957 53 0 0 25 0 1 0 481364026 91295744 21794 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22289 21794 603 41 0 22248 0
vsize: 89156
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 22156 0 0 0 79956 54 0 0 25 0 1 0 481364026 92647424 22131 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22619 22131 603 41 0 22578 0
vsize: 90476
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 22971 0 0 0 80955 56 0 0 25 0 1 0 481364026 96022528 22946 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23443 22946 603 41 0 23402 0
vsize: 93772
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 81955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 82955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 83955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 84955 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 85956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 86956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+880.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 87956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29127
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 88956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+900.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 89956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 90956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+920.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 91956 56 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+930.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23038 0 0 0 92956 57 0 0 25 0 1 0 481364026 96296960 23013 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23510 23013 603 41 0 23469 0
vsize: 94040
[startup+940.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23174 0 0 0 93956 57 0 0 25 0 1 0 481364026 96837632 23149 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23642 23149 603 41 0 23601 0
vsize: 94568
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 23846 0 0 0 94955 58 0 0 25 0 1 0 481364026 99680256 23821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24336 23821 603 41 0 24295 0
vsize: 97344
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 24920 0 0 0 95951 61 0 0 25 0 1 0 481364026 103989248 24895 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25388 24895 603 41 0 25347 0
vsize: 101552
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 25929 0 0 0 96949 64 0 0 25 0 1 0 481364026 108167168 25904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26408 25904 603 41 0 26367 0
vsize: 105632
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 97949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 98949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 99949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 100949 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 101950 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 102950 64 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 103950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 104950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223728 134559618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 105950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 106950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 107950 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 108951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 109951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 110951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223704 134560076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 111951 65 0 0 25 0 1 0 481364026 108978176 26110 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26606 26110 603 41 0 26565 0
vsize: 106424
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 112951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26074 603 41 0 26525 0
vsize: 106264
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 113951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26074 603 41 0 26525 0
vsize: 106264
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 114951 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26074 603 41 0 26525 0
vsize: 106264
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 115952 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223728 134559618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26074 603 41 0 26525 0
vsize: 106264
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26135 0 0 0 116952 65 0 0 25 0 1 0 481364026 108814336 26074 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26074 603 41 0 26525 0
vsize: 106264
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 117952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26075 603 41 0 26525 0
vsize: 106264
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29129
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 118952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26075 603 41 0 26525 0
vsize: 106264
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 29131
Raw data (stat): 29123 (minisat+) R 29122 22929 22928 0 -1 0 26136 0 0 0 119952 65 0 0 25 0 1 0 481364026 108814336 26075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26566 26075 603 41 0 26525 0
vsize: 106264
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 29131
Raw data (stat): 29123 (minisat+) Z 29122 22929 22928 0 -1 12 26138 0 0 0 119952 70 0 0 25 0 1 0 481364026 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.08
CPU time (s): 1200.23
CPU user time (s): 1199.53
CPU system time (s): 0.707892
CPU usage (%): 100.013
Max. virtual memory (Kb): 106424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####