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/manquinho/primes-dimacs-cnf/normalized-par32-1-c.opb
MD5SUM8c1b8634a2f99e9f8e579ef031d10353
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 2630
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 2630
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2630
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2630
Total number of constraints6569
Number of constraints which are clauses6569
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint3

Trace number 5143 

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        858480 kB
Buffers:         40136 kB
Cached:         111844 kB
SwapCached:          0 kB
Active:         106896 kB
Inactive:        48244 kB
HighTotal:      131008 kB
HighFree:        26404 kB
LowTotal:       903652 kB
LowFree:        832076 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15344 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:34:13 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3587 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6569 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6569    18020 |    2189       0        0     nan |  0.000 % |
c |       100 |    6569    18020 |    2407     100     3667    36.7 |  0.004 % |
c |       251 |    6569    18020 |    2648     251     9998    39.8 |  0.000 % |
c |       477 |    6569    18020 |    2913     477    19389    40.6 |  0.000 % |
c |       814 |    6569    18020 |    3204     814    28997    35.6 |  0.000 % |
c |      1320 |    6569    18020 |    3525    1320    43427    32.9 |  0.000 % |
c |      2079 |    6562    18004 |    3877    2077    64872    31.2 |  0.076 % |
c |      3218 |    6562    18004 |    4265    3216    92939    28.9 |  0.076 % |
c |      4927 |    6562    18004 |    4692    2772    64097    23.1 |  0.076 % |
c |      7489 |    6562    18004 |    5161    2951    64576    21.9 |  0.076 % |
c |     11333 |    6562    18004 |    5677    4187    97402    23.3 |  0.076 % |
c |     17099 |    6562    18004 |    6245    4190    93186    22.2 |  0.076 % |
c |     25748 |    6562    18004 |    6870    3311    68434    20.7 |  0.076 % |
c |     38722 |    6562    18004 |    7557    5903   133047    22.5 |  0.076 % |
c |     58183 |    6562    18004 |    8312    6287   144714    23.0 |  0.076 % |
c |     87376 |    6562    18004 |    9143    6021   133526    22.2 |  0.076 % |
c |    131166 |    6562    18004 |   10058    8376   183814    21.9 |  0.076 % |
c |    196850 |    6562    18004 |   11064    8127   172744    21.3 |  0.076 % |
c |    295376 |    6562    18004 |   12170    6300   144154    22.9 |  0.076 % |
c |    443166 |    6562    18004 |   13387    6996   179583    25.7 |  0.076 % |
c |    664849 |    6562    18004 |   14726   13043   279106    21.4 |  0.076 % |
#### 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.66 0.86 0.88 2/56 16447
Raw data (stat): 16447 (runsolver) R 16446 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364390517 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.71 0.87 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 774 0 0 0 997 1 0 0 25 0 1 0 364390517 4775936 752 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1166 752 603 41 0 1125 0
vsize: 4664
[startup+20.001 s]
Raw data (loadavg): 0.76 0.87 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 801 0 0 0 1997 2 0 0 25 0 1 0 364390517 4775936 779 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1166 779 603 41 0 1125 0
vsize: 4664
[startup+30.0018 s]
Raw data (loadavg): 0.79 0.87 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 815 0 0 0 2997 2 0 0 25 0 1 0 364390517 4915200 793 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1200 793 603 41 0 1159 0
vsize: 4800
[startup+40.0021 s]
Raw data (loadavg): 0.83 0.88 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 835 0 0 0 3996 2 0 0 25 0 1 0 364390517 5054464 813 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1234 813 603 41 0 1193 0
vsize: 4936
[startup+50.0024 s]
Raw data (loadavg): 0.85 0.88 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 871 0 0 0 4996 2 0 0 25 0 1 0 364390517 5185536 849 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 849 603 41 0 1225 0
vsize: 5064
[startup+60.0022 s]
Raw data (loadavg): 0.87 0.88 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 877 0 0 0 5997 2 0 0 25 0 1 0 364390517 5185536 855 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1266 855 603 41 0 1225 0
vsize: 5064
[startup+70.0031 s]
Raw data (loadavg): 0.89 0.89 0.88 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 916 0 0 0 6997 2 0 0 25 0 1 0 364390517 5320704 894 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1299 894 603 41 0 1258 0
vsize: 5196
[startup+80.0039 s]
Raw data (loadavg): 0.91 0.89 0.89 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 920 0 0 0 7997 3 0 0 25 0 1 0 364390517 5459968 898 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+90.0037 s]
Raw data (loadavg): 0.92 0.89 0.89 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 920 0 0 0 8997 3 0 0 25 0 1 0 364390517 5459968 898 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 898 603 41 0 1292 0
vsize: 5332
[startup+100.004 s]
Raw data (loadavg): 0.93 0.90 0.89 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 924 0 0 0 9997 3 0 0 25 0 1 0 364390517 5459968 902 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 902 603 41 0 1292 0
vsize: 5332
[startup+110.004 s]
Raw data (loadavg): 0.94 0.90 0.89 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 948 0 0 0 10997 3 0 0 25 0 1 0 364390517 5459968 926 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 926 603 41 0 1292 0
vsize: 5332
[startup+120.005 s]
Raw data (loadavg): 0.95 0.90 0.89 2/56 16447
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 950 0 0 0 11997 3 0 0 25 0 1 0 364390517 5459968 928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+130.005 s]
Raw data (loadavg): 0.96 0.91 0.89 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 950 0 0 0 12996 3 0 0 25 0 1 0 364390517 5459968 928 4294967295 134512640 134672761 3221224560 3221223728 134560849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1333 928 603 41 0 1292 0
vsize: 5332
[startup+140.005 s]
Raw data (loadavg): 0.96 0.91 0.89 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 959 0 0 0 13996 3 0 0 25 0 1 0 364390517 5595136 937 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 937 603 41 0 1325 0
vsize: 5464
[startup+150.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 960 0 0 0 14996 4 0 0 25 0 1 0 364390517 5595136 938 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1366 938 603 41 0 1325 0
vsize: 5464
[startup+160.006 s]
Raw data (loadavg): 0.97 0.91 0.89 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 989 0 0 0 15996 4 0 0 25 0 1 0 364390517 5730304 967 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 967 603 41 0 1358 0
vsize: 5596
[startup+170.006 s]
Raw data (loadavg): 0.98 0.92 0.89 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1006 0 0 0 16996 4 0 0 25 0 1 0 364390517 5730304 984 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 984 603 41 0 1358 0
vsize: 5596
[startup+180.007 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1010 0 0 0 17996 4 0 0 25 0 1 0 364390517 5730304 988 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 988 603 41 0 1358 0
vsize: 5596
[startup+190.007 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1016 0 0 0 18996 4 0 0 25 0 1 0 364390517 5730304 994 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+200.007 s]
Raw data (loadavg): 0.98 0.92 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1016 0 0 0 19996 4 0 0 25 0 1 0 364390517 5730304 994 4294967295 134512640 134672761 3221224560 3221223744 134558497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+210.007 s]
Raw data (loadavg): 0.99 0.92 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1016 0 0 0 20996 4 0 0 25 0 1 0 364390517 5730304 994 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+220.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1016 0 0 0 21996 5 0 0 25 0 1 0 364390517 5730304 994 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+230.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1016 0 0 0 22996 5 0 0 25 0 1 0 364390517 5730304 994 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1399 994 603 41 0 1358 0
vsize: 5596
[startup+240.008 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1040 0 0 0 23996 5 0 0 25 0 1 0 364390517 5865472 1018 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1432 1018 603 41 0 1391 0
vsize: 5728
[startup+250.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1058 0 0 0 24996 5 0 0 25 0 1 0 364390517 6012928 1036 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1468 1036 603 41 0 1427 0
vsize: 5872
[startup+260.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1058 0 0 0 25997 5 0 0 25 0 1 0 364390517 6012928 1036 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1468 1036 603 41 0 1427 0
vsize: 5872
[startup+270.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1070 0 0 0 26997 5 0 0 25 0 1 0 364390517 6012928 1048 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1468 1048 603 41 0 1427 0
vsize: 5872
[startup+280.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1076 0 0 0 27997 5 0 0 25 0 1 0 364390517 6012928 1054 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1468 1054 603 41 0 1427 0
vsize: 5872
[startup+290.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1094 0 0 0 28997 5 0 0 25 0 1 0 364390517 6148096 1072 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1072 603 41 0 1460 0
vsize: 6004
[startup+300.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1094 0 0 0 29997 5 0 0 25 0 1 0 364390517 6148096 1072 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1072 603 41 0 1460 0
vsize: 6004
[startup+310.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1101 0 0 0 30997 5 0 0 25 0 1 0 364390517 6148096 1079 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1079 603 41 0 1460 0
vsize: 6004
[startup+320.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1108 0 0 0 31997 5 0 0 25 0 1 0 364390517 6148096 1086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1501 1086 603 41 0 1460 0
vsize: 6004
[startup+330.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1114 0 0 0 32998 5 0 0 25 0 1 0 364390517 6291456 1092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+340.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1114 0 0 0 33998 5 0 0 25 0 1 0 364390517 6291456 1092 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+350.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1114 0 0 0 34998 5 0 0 25 0 1 0 364390517 6291456 1092 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1092 603 41 0 1495 0
vsize: 6144
[startup+360.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1123 0 0 0 35998 5 0 0 25 0 1 0 364390517 6291456 1101 4294967295 134512640 134672761 3221224560 3221223696 134565113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1536 1101 603 41 0 1495 0
vsize: 6144
[startup+370.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1124 0 0 0 36998 5 0 0 25 0 1 0 364390517 6291456 1102 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1536 1102 603 41 0 1495 0
vsize: 6144
[startup+380.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1161 0 0 0 37998 5 0 0 25 0 1 0 364390517 6426624 1139 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1569 1139 603 41 0 1528 0
vsize: 6276
[startup+390.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1173 0 0 0 38998 5 0 0 25 0 1 0 364390517 6426624 1151 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+400.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1173 0 0 0 39998 5 0 0 25 0 1 0 364390517 6426624 1151 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1569 1151 603 41 0 1528 0
vsize: 6276
[startup+410.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1175 0 0 0 40998 6 0 0 25 0 1 0 364390517 6561792 1153 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+420.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16449
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1175 0 0 0 41998 6 0 0 25 0 1 0 364390517 6561792 1153 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1153 603 41 0 1561 0
vsize: 6408
[startup+430.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1177 0 0 0 42998 6 0 0 25 0 1 0 364390517 6561792 1155 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1155 603 41 0 1561 0
vsize: 6408
[startup+440.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1180 0 0 0 43998 6 0 0 25 0 1 0 364390517 6561792 1158 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1158 603 41 0 1561 0
vsize: 6408
[startup+450.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1184 0 0 0 44998 6 0 0 25 0 1 0 364390517 6561792 1162 4294967295 134512640 134672761 3221224560 3221223728 134560836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1162 603 41 0 1561 0
vsize: 6408
[startup+460.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1186 0 0 0 45998 6 0 0 25 0 1 0 364390517 6561792 1164 4294967295 134512640 134672761 3221224560 3221223664 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1164 603 41 0 1561 0
vsize: 6408
[startup+470.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1196 0 0 0 46998 7 0 0 25 0 1 0 364390517 6561792 1174 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1602 1174 603 41 0 1561 0
vsize: 6408
[startup+480.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1208 0 0 0 47998 7 0 0 25 0 1 0 364390517 6717440 1186 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1186 603 41 0 1599 0
vsize: 6560
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 48998 7 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+500.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 49998 7 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+510.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 50998 7 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+520.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 51998 7 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+530.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 52998 7 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+540.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1209 0 0 0 53998 8 0 0 25 0 1 0 364390517 6717440 1187 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1187 603 41 0 1599 0
vsize: 6560
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1212 0 0 0 54998 8 0 0 25 0 1 0 364390517 6717440 1190 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1190 603 41 0 1599 0
vsize: 6560
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1228 0 0 0 55998 8 0 0 25 0 1 0 364390517 6717440 1206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1206 603 41 0 1599 0
vsize: 6560
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1238 0 0 0 56998 8 0 0 25 0 1 0 364390517 6717440 1216 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1640 1216 603 41 0 1599 0
vsize: 6560
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1240 0 0 0 57998 8 0 0 25 0 1 0 364390517 6717440 1218 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1640 1218 603 41 0 1599 0
vsize: 6560
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1247 0 0 0 58998 8 0 0 25 0 1 0 364390517 6868992 1225 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1225 603 41 0 1636 0
vsize: 6708
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1253 0 0 0 59998 8 0 0 25 0 1 0 364390517 6868992 1231 4294967295 134512640 134672761 3221224560 3221223744 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1231 603 41 0 1636 0
vsize: 6708
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1260 0 0 0 60998 8 0 0 25 0 1 0 364390517 6868992 1238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1238 603 41 0 1636 0
vsize: 6708
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1261 0 0 0 61998 8 0 0 25 0 1 0 364390517 6868992 1239 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1261 0 0 0 62998 8 0 0 25 0 1 0 364390517 6868992 1239 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1239 603 41 0 1636 0
vsize: 6708
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1267 0 0 0 63999 8 0 0 25 0 1 0 364390517 6868992 1245 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1245 603 41 0 1636 0
vsize: 6708
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1267 0 0 0 64999 8 0 0 25 0 1 0 364390517 6868992 1245 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1245 603 41 0 1636 0
vsize: 6708
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1273 0 0 0 65999 8 0 0 25 0 1 0 364390517 6868992 1251 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1273 0 0 0 66999 8 0 0 25 0 1 0 364390517 6868992 1251 4294967295 134512640 134672761 3221224560 3221223744 134558697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1273 0 0 0 67999 8 0 0 25 0 1 0 364390517 6868992 1251 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1273 0 0 0 69000 8 0 0 25 0 1 0 364390517 6868992 1251 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1273 0 0 0 70000 8 0 0 25 0 1 0 364390517 6868992 1251 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1677 1251 603 41 0 1636 0
vsize: 6708
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1291 0 0 0 71000 8 0 0 25 0 1 0 364390517 7004160 1269 4294967295 134512640 134672761 3221224560 3221223664 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1269 603 41 0 1669 0
vsize: 6840
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16451
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1293 0 0 0 72000 8 0 0 25 0 1 0 364390517 7004160 1271 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1271 603 41 0 1669 0
vsize: 6840
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1299 0 0 0 73000 8 0 0 25 0 1 0 364390517 7004160 1277 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1277 603 41 0 1669 0
vsize: 6840
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 74000 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 75000 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 76001 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+770.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 77001 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 78001 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1305 0 0 0 79001 8 0 0 25 0 1 0 364390517 7139328 1283 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1283 603 41 0 1702 0
vsize: 6972
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1325 0 0 0 80001 8 0 0 25 0 1 0 364390517 7139328 1303 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1743 1303 603 41 0 1702 0
vsize: 6972
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1347 0 0 0 81001 8 0 0 25 0 1 0 364390517 7270400 1325 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1325 603 41 0 1734 0
vsize: 7100
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1355 0 0 0 82001 8 0 0 25 0 1 0 364390517 7270400 1333 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1333 603 41 0 1734 0
vsize: 7100
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1361 0 0 0 83001 9 0 0 25 0 1 0 364390517 7270400 1339 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1339 603 41 0 1734 0
vsize: 7100
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1366 0 0 0 84001 9 0 0 25 0 1 0 364390517 7270400 1344 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1344 603 41 0 1734 0
vsize: 7100
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1367 0 0 0 85001 9 0 0 25 0 1 0 364390517 7270400 1345 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1775 1345 603 41 0 1734 0
vsize: 7100
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1387 0 0 0 86001 9 0 0 25 0 1 0 364390517 7401472 1365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1387 0 0 0 87001 9 0 0 25 0 1 0 364390517 7401472 1365 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1387 0 0 0 88001 9 0 0 25 0 1 0 364390517 7401472 1365 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1365 603 41 0 1766 0
vsize: 7228
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1392 0 0 0 89001 10 0 0 25 0 1 0 364390517 7401472 1370 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1370 603 41 0 1766 0
vsize: 7228
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1393 0 0 0 90001 10 0 0 25 0 1 0 364390517 7401472 1371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1393 0 0 0 91001 10 0 0 25 0 1 0 364390517 7401472 1371 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1807 1371 603 41 0 1766 0
vsize: 7228
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1413 0 0 0 92001 10 0 0 25 0 1 0 364390517 7532544 1391 4294967295 134512640 134672761 3221224560 3221223620 1075346657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1391 603 41 0 1798 0
vsize: 7356
[startup+930.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1428 0 0 0 93001 10 0 0 25 0 1 0 364390517 7532544 1406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1839 1406 603 41 0 1798 0
vsize: 7356
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1432 0 0 0 94001 10 0 0 25 0 1 0 364390517 7667712 1410 4294967295 134512640 134672761 3221224560 3221223616 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1872 1410 603 41 0 1831 0
vsize: 7488
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1432 0 0 0 95001 10 0 0 25 0 1 0 364390517 7663616 1410 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1871 1410 603 41 0 1830 0
vsize: 7484
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1432 0 0 0 96001 10 0 0 25 0 1 0 364390517 7663616 1410 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1410 603 41 0 1830 0
vsize: 7484
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1436 0 0 0 97002 10 0 0 25 0 1 0 364390517 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+980.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1436 0 0 0 98002 10 0 0 25 0 1 0 364390517 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1436 0 0 0 99002 10 0 0 25 0 1 0 364390517 7663616 1414 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1436 0 0 0 100002 10 0 0 25 0 1 0 364390517 7663616 1414 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1414 603 41 0 1830 0
vsize: 7484
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 101002 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16453
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 102002 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 103002 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 104003 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 105003 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 106003 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223760 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 107003 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 108003 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223744 134558365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 109004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 110004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 111004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 112004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 113004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1437 0 0 0 114004 10 0 0 25 0 1 0 364390517 7663616 1415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1415 603 41 0 1830 0
vsize: 7484
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1442 0 0 0 115005 10 0 0 25 0 1 0 364390517 7663616 1420 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1442 0 0 0 116005 10 0 0 25 0 1 0 364390517 7663616 1420 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1442 0 0 0 117005 10 0 0 25 0 1 0 364390517 7663616 1420 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1420 603 41 0 1830 0
vsize: 7484
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1448 0 0 0 118005 10 0 0 25 0 1 0 364390517 7663616 1426 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1448 0 0 0 119005 10 0 0 25 0 1 0 364390517 7663616 1426 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16455
Raw data (stat): 16447 (minisat+) R 16446 12452 12451 0 -1 0 1448 0 0 0 120005 10 0 0 25 0 1 0 364390517 7663616 1426 4294967295 134512640 134672761 3221224560 3221223744 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1871 1426 603 41 0 1830 0
vsize: 7484
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 16455
Raw data (stat): 16447 (minisat+) Z 16446 12452 12451 0 -1 12 1450 0 0 0 120005 11 0 0 25 0 1 0 364390517 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.17
CPU user time (s): 1200.06
CPU system time (s): 0.112982
CPU usage (%): 100.012
Max. virtual memory (Kb): 7488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####