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-f2000.opb
MD5SUM4675a5d50c7e04c9a0597ae768da1a88
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 4000
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 4000
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 4000
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 variables4000
Total number of constraints10500
Number of constraints which are clauses10500
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 5818 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 01:59:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4264 boxname=wulflinc18 idbench=128 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4675a5d50c7e04c9a0597ae768da1a88  /oldhome/oroussel/tmp/wulflinc18/normalized-f2000.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-f2000.opb /oldhome/oroussel/tmp/wulflinc18/normalized-f2000.opb
IDLAUNCH: 4264
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        861888 kB
Buffers:         35084 kB
Cached:         101616 kB
SwapCached:        320 kB
Active:          55720 kB
Inactive:        84120 kB
HighTotal:      131008 kB
HighFree:        25424 kB
LowTotal:       903652 kB
LowFree:        836464 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27376 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 02:19:28 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 4264 7 1200.15 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 10500 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 |   10500    29500 |    3500       0        0     nan |  0.000 % |
c |       101 |   10500    29500 |    3850     101     5214    51.6 |  0.000 % |
c |       254 |   10500    29500 |    4235     254    16768    66.0 |  0.000 % |
c |       480 |   10500    29500 |    4658     480    31254    65.1 |  0.000 % |
c |       818 |   10500    29500 |    5124     818    54667    66.8 |  0.000 % |
c |      1325 |   10500    29500 |    5636    1325    91945    69.4 |  0.000 % |
c |      2085 |   10500    29500 |    6200    2085   147368    70.7 |  0.000 % |
c |      3224 |   10500    29500 |    6820    3224   227442    70.5 |  0.000 % |
c |      4933 |   10500    29500 |    7502    4933   356310    72.2 |  0.000 % |
c |      7498 |   10500    29500 |    8252    7498   558986    74.6 |  0.000 % |
c |     11342 |   10500    29500 |    9078    7035   532667    75.7 |  0.000 % |
c |     17110 |   10500    29500 |    9985    8082   628618    77.8 |  0.000 % |
c |     25760 |   10500    29500 |   10984    6399   501007    78.3 |  0.000 % |
c |     38734 |   10500    29500 |   12082    8099   680844    84.1 |  0.000 % |
c |     58195 |   10500    29500 |   13291    8833   695144    78.7 |  0.000 % |
c |     87387 |   10500    29500 |   14620   10633   872256    82.0 |  0.000 % |
c |    131179 |   10500    29500 |   16082    9098   714655    78.6 |  0.000 % |
c |    196863 |   10500    29500 |   17690    8808   654716    74.3 |  0.000 % |
c |    295391 |   10500    29500 |   19459   16874  1288385    76.4 |  0.000 % |
c |    443181 |   10500    29500 |   21405   15399  1144903    74.3 |  0.000 % |
c |    664864 |   10500    29500 |   23546   18740  1450858    77.4 |  0.000 % |
#### 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.54 0.85 0.87 2/55 27316
Raw data (stat): 27316 (runsolver) R 27315 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480810650 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.0006 s]
Raw data (loadavg): 0.61 0.86 0.87 2/55 27316
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 1400 0 0 0 994 3 0 0 25 0 1 0 480810650 7303168 1378 4294967295 134512640 134672761 3221224560 3221223744 134559559 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1783 1378 603 41 0 1742 0
vsize: 7132
[startup+20.002 s]
Raw data (loadavg): 0.67 0.86 0.87 2/55 27316
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 1659 0 0 0 1993 4 0 0 25 0 1 0 480810650 8380416 1637 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2046 1637 603 41 0 2005 0
vsize: 8184
[startup+30.0029 s]
Raw data (loadavg): 0.72 0.86 0.87 2/55 27316
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 1823 0 0 0 2992 5 0 0 25 0 1 0 480810650 9052160 1801 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2210 1801 603 41 0 2169 0
vsize: 8840
[startup+40.0034 s]
Raw data (loadavg): 0.76 0.87 0.87 3/59 27322
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 1910 0 0 0 3991 6 0 0 25 0 1 0 480810650 9457664 1888 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2309 1888 603 41 0 2268 0
vsize: 9236
[startup+50.0044 s]
Raw data (loadavg): 0.87 0.89 0.88 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2000 0 0 0 4990 7 0 0 25 0 1 0 480810650 9723904 1978 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2374 1978 603 41 0 2333 0
vsize: 9496
[startup+60.004 s]
Raw data (loadavg): 0.89 0.89 0.88 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2038 0 0 0 5990 7 0 0 25 0 1 0 480810650 9859072 2016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2407 2016 603 41 0 2366 0
vsize: 9628
[startup+70.005 s]
Raw data (loadavg): 0.91 0.89 0.88 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2149 0 0 0 6989 7 0 0 25 0 1 0 480810650 10387456 2127 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2536 2127 603 41 0 2495 0
vsize: 10144
[startup+80.0052 s]
Raw data (loadavg): 0.92 0.90 0.88 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2217 0 0 0 7989 8 0 0 25 0 1 0 480810650 10657792 2195 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2602 2195 603 41 0 2561 0
vsize: 10408
[startup+90.0058 s]
Raw data (loadavg): 0.93 0.90 0.89 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2297 0 0 0 8989 8 0 0 25 0 1 0 480810650 10924032 2275 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2667 2275 603 41 0 2626 0
vsize: 10668
[startup+100.006 s]
Raw data (loadavg): 0.94 0.90 0.89 2/55 27369
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2309 0 0 0 9989 8 0 0 25 0 1 0 480810650 11059200 2287 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2700 2287 603 41 0 2659 0
vsize: 10800
[startup+110.006 s]
Raw data (loadavg): 0.95 0.91 0.89 2/55 27371
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2418 0 0 0 10988 9 0 0 25 0 1 0 480810650 11460608 2396 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2798 2396 603 41 0 2757 0
vsize: 11192
[startup+120.007 s]
Raw data (loadavg): 0.96 0.91 0.89 2/55 27371
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2445 0 0 0 11988 9 0 0 25 0 1 0 480810650 11595776 2423 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2831 2423 603 41 0 2790 0
vsize: 11324
[startup+130.006 s]
Raw data (loadavg): 0.96 0.91 0.89 2/55 27371
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2482 0 0 0 12988 9 0 0 25 0 1 0 480810650 11730944 2460 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2864 2460 603 41 0 2823 0
vsize: 11456
[startup+140.007 s]
Raw data (loadavg): 0.97 0.91 0.89 2/55 27371
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2486 0 0 0 13988 9 0 0 25 0 1 0 480810650 11730944 2464 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2864 2464 603 41 0 2823 0
vsize: 11456
[startup+150.008 s]
Raw data (loadavg): 0.97 0.92 0.89 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2512 0 0 0 14988 10 0 0 25 0 1 0 480810650 11866112 2490 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2897 2490 603 41 0 2856 0
vsize: 11588
[startup+160.008 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2517 0 0 0 15988 10 0 0 25 0 1 0 480810650 11866112 2495 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2897 2495 603 41 0 2856 0
vsize: 11588
[startup+170.008 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2545 0 0 0 16988 10 0 0 25 0 1 0 480810650 12001280 2523 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2930 2523 603 41 0 2889 0
vsize: 11720
[startup+180.008 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2647 0 0 0 17988 10 0 0 25 0 1 0 480810650 12546048 2625 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+190.009 s]
Raw data (loadavg): 0.98 0.92 0.89 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2647 0 0 0 18988 10 0 0 25 0 1 0 480810650 12546048 2625 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2625 603 41 0 3022 0
vsize: 12252
[startup+200.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2650 0 0 0 19989 10 0 0 25 0 1 0 480810650 12546048 2628 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2628 603 41 0 3022 0
vsize: 12252
[startup+210.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2669 0 0 0 20989 10 0 0 25 0 1 0 480810650 12546048 2647 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3063 2647 603 41 0 3022 0
vsize: 12252
[startup+220.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2688 0 0 0 21989 10 0 0 25 0 1 0 480810650 12677120 2666 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3095 2666 603 41 0 3054 0
vsize: 12380
[startup+230.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2711 0 0 0 22989 10 0 0 25 0 1 0 480810650 12824576 2689 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3131 2689 603 41 0 3090 0
vsize: 12524
[startup+240.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2714 0 0 0 23989 10 0 0 25 0 1 0 480810650 12824576 2692 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+250.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2714 0 0 0 24989 10 0 0 25 0 1 0 480810650 12824576 2692 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3131 2692 603 41 0 3090 0
vsize: 12524
[startup+260.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2750 0 0 0 25989 10 0 0 25 0 1 0 480810650 12959744 2728 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3164 2728 603 41 0 3123 0
vsize: 12656
[startup+270.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2857 0 0 0 26989 11 0 0 25 0 1 0 480810650 13365248 2835 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3263 2835 603 41 0 3222 0
vsize: 13052
[startup+280.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2915 0 0 0 27989 11 0 0 25 0 1 0 480810650 13631488 2893 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3328 2893 603 41 0 3287 0
vsize: 13312
[startup+290.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2920 0 0 0 28989 11 0 0 25 0 1 0 480810650 13631488 2898 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3328 2898 603 41 0 3287 0
vsize: 13312
[startup+300.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2954 0 0 0 29990 11 0 0 25 0 1 0 480810650 13766656 2932 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3361 2932 603 41 0 3320 0
vsize: 13444
[startup+310.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2968 0 0 0 30990 11 0 0 25 0 1 0 480810650 13766656 2946 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3361 2946 603 41 0 3320 0
vsize: 13444
[startup+320.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2971 0 0 0 31990 11 0 0 25 0 1 0 480810650 13905920 2949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+330.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2971 0 0 0 32990 11 0 0 25 0 1 0 480810650 13905920 2949 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+340.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2971 0 0 0 33990 11 0 0 25 0 1 0 480810650 13905920 2949 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3395 2949 603 41 0 3354 0
vsize: 13580
[startup+350.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 2979 0 0 0 34990 11 0 0 25 0 1 0 480810650 13905920 2957 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3395 2957 603 41 0 3354 0
vsize: 13580
[startup+360.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3008 0 0 0 35990 11 0 0 25 0 1 0 480810650 14041088 2986 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+370.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3008 0 0 0 36991 11 0 0 25 0 1 0 480810650 14041088 2986 4294967295 134512640 134672761 3221224560 3221223556 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+380.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27373
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3008 0 0 0 37991 11 0 0 25 0 1 0 480810650 14041088 2986 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3428 2986 603 41 0 3387 0
vsize: 13712
[startup+390.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3054 0 0 0 38991 11 0 0 25 0 1 0 480810650 14172160 3032 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3460 3032 603 41 0 3419 0
vsize: 13840
[startup+400.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3171 0 0 0 39990 11 0 0 25 0 1 0 480810650 14708736 3149 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3149 603 41 0 3550 0
vsize: 14364
[startup+410.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3177 0 0 0 40989 12 0 0 25 0 1 0 480810650 14708736 3155 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3591 3155 603 41 0 3550 0
vsize: 14364
[startup+420.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3179 0 0 0 41989 12 0 0 25 0 1 0 480810650 14708736 3157 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3591 3157 603 41 0 3550 0
vsize: 14364
[startup+430.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3199 0 0 0 42989 12 0 0 25 0 1 0 480810650 14843904 3177 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3177 603 41 0 3583 0
vsize: 14496
[startup+440.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27375
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3206 0 0 0 43989 12 0 0 25 0 1 0 480810650 14843904 3184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3184 603 41 0 3583 0
vsize: 14496
[startup+450.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3221 0 0 0 44989 12 0 0 25 0 1 0 480810650 14843904 3199 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3624 3199 603 41 0 3583 0
vsize: 14496
[startup+460.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3249 0 0 0 45989 12 0 0 25 0 1 0 480810650 14979072 3227 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3657 3227 603 41 0 3616 0
vsize: 14628
[startup+470.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3255 0 0 0 46989 12 0 0 25 0 1 0 480810650 14979072 3233 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3657 3233 603 41 0 3616 0
vsize: 14628
[startup+480.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3261 0 0 0 47989 12 0 0 25 0 1 0 480810650 15126528 3239 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3239 603 41 0 3652 0
vsize: 14772
[startup+490.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3278 0 0 0 48989 12 0 0 25 0 1 0 480810650 15126528 3256 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3256 603 41 0 3652 0
vsize: 14772
[startup+500.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3280 0 0 0 49989 12 0 0 25 0 1 0 480810650 15126528 3258 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+510.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3280 0 0 0 50990 12 0 0 25 0 1 0 480810650 15126528 3258 4294967295 134512640 134672761 3221224560 3221223664 134560201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3258 603 41 0 3652 0
vsize: 14772
[startup+520.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3283 0 0 0 51990 13 0 0 25 0 1 0 480810650 15126528 3261 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3261 603 41 0 3652 0
vsize: 14772
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3287 0 0 0 52990 13 0 0 25 0 1 0 480810650 15126528 3265 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3265 603 41 0 3652 0
vsize: 14772
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3292 0 0 0 53990 13 0 0 25 0 1 0 480810650 15257600 3270 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3270 603 41 0 3684 0
vsize: 14900
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3293 0 0 0 54990 13 0 0 25 0 1 0 480810650 15257600 3271 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3271 603 41 0 3684 0
vsize: 14900
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3321 0 0 0 55990 13 0 0 25 0 1 0 480810650 15257600 3299 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3725 3299 603 41 0 3684 0
vsize: 14900
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3380 0 0 0 56991 13 0 0 25 0 1 0 480810650 15527936 3358 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3358 603 41 0 3750 0
vsize: 15164
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3387 0 0 0 57991 13 0 0 25 0 1 0 480810650 15527936 3365 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3365 603 41 0 3750 0
vsize: 15164
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3429 0 0 0 58991 13 0 0 25 0 1 0 480810650 15806464 3407 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3859 3407 603 41 0 3818 0
vsize: 15436
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3435 0 0 0 59991 13 0 0 25 0 1 0 480810650 15806464 3413 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3435 0 0 0 60990 13 0 0 25 0 1 0 480810650 15806464 3413 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3859 3413 603 41 0 3818 0
vsize: 15436
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3556 0 0 0 61990 14 0 0 25 0 1 0 480810650 16355328 3534 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3993 3534 603 41 0 3952 0
vsize: 15972
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3560 0 0 0 62990 14 0 0 25 0 1 0 480810650 16355328 3538 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3993 3538 603 41 0 3952 0
vsize: 15972
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3656 0 0 0 63990 14 0 0 25 0 1 0 480810650 16777216 3634 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4096 3634 603 41 0 4055 0
vsize: 16384
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3708 0 0 0 64990 14 0 0 25 0 1 0 480810650 16912384 3686 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4129 3686 603 41 0 4088 0
vsize: 16516
[startup+660.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3727 0 0 0 65990 14 0 0 25 0 1 0 480810650 17047552 3705 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3705 603 41 0 4121 0
vsize: 16648
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3737 0 0 0 66991 14 0 0 25 0 1 0 480810650 17047552 3715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3737 0 0 0 67991 14 0 0 25 0 1 0 480810650 17047552 3715 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3737 0 0 0 68991 14 0 0 25 0 1 0 480810650 17047552 3715 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3715 603 41 0 4121 0
vsize: 16648
[startup+700.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3738 0 0 0 69991 14 0 0 25 0 1 0 480810650 17047552 3716 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3716 603 41 0 4121 0
vsize: 16648
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3742 0 0 0 70991 14 0 0 25 0 1 0 480810650 17047552 3720 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3720 603 41 0 4121 0
vsize: 16648
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3745 0 0 0 71992 14 0 0 25 0 1 0 480810650 17047552 3723 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3723 603 41 0 4121 0
vsize: 16648
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3746 0 0 0 72992 14 0 0 25 0 1 0 480810650 17047552 3724 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4162 3724 603 41 0 4121 0
vsize: 16648
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27377
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3751 0 0 0 73992 14 0 0 25 0 1 0 480810650 17190912 3729 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3751 0 0 0 74992 14 0 0 25 0 1 0 480810650 17190912 3729 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4197 3729 603 41 0 4156 0
vsize: 16788
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3785 0 0 0 75992 14 0 0 25 0 1 0 480810650 17326080 3763 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3763 603 41 0 4189 0
vsize: 16920
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3791 0 0 0 76992 14 0 0 25 0 1 0 480810650 17326080 3769 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3769 603 41 0 4189 0
vsize: 16920
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3810 0 0 0 77993 14 0 0 25 0 1 0 480810650 17326080 3788 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3788 603 41 0 4189 0
vsize: 16920
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3813 0 0 0 78993 14 0 0 25 0 1 0 480810650 17326080 3791 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3813 0 0 0 79993 14 0 0 25 0 1 0 480810650 17326080 3791 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3813 0 0 0 80993 14 0 0 25 0 1 0 480810650 17326080 3791 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3813 0 0 0 81993 14 0 0 25 0 1 0 480810650 17326080 3791 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3791 603 41 0 4189 0
vsize: 16920
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3834 0 0 0 82993 14 0 0 25 0 1 0 480810650 17461248 3812 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3812 603 41 0 4222 0
vsize: 17052
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3834 0 0 0 83994 14 0 0 25 0 1 0 480810650 17461248 3812 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3812 603 41 0 4222 0
vsize: 17052
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3838 0 0 0 84994 14 0 0 25 0 1 0 480810650 17461248 3816 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3816 603 41 0 4222 0
vsize: 17052
[startup+860.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3841 0 0 0 85994 14 0 0 25 0 1 0 480810650 17461248 3819 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3841 0 0 0 86994 14 0 0 25 0 1 0 480810650 17461248 3819 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3841 0 0 0 87995 14 0 0 25 0 1 0 480810650 17461248 3819 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3841 0 0 0 88995 14 0 0 25 0 1 0 480810650 17461248 3819 4294967295 134512640 134672761 3221224560 3221223744 134559199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3841 0 0 0 89995 14 0 0 25 0 1 0 480810650 17461248 3819 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4263 3819 603 41 0 4222 0
vsize: 17052
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3887 0 0 0 90995 14 0 0 25 0 1 0 480810650 17727488 3865 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3865 603 41 0 4287 0
vsize: 17312
[startup+920.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3891 0 0 0 91995 14 0 0 25 0 1 0 480810650 17727488 3869 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3869 603 41 0 4287 0
vsize: 17312
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3931 0 0 0 92995 14 0 0 25 0 1 0 480810650 17883136 3909 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3931 0 0 0 93995 14 0 0 25 0 1 0 480810650 17883136 3909 4294967295 134512640 134672761 3221224560 3221222800 134565779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 3931 0 0 0 94995 14 0 0 25 0 1 0 480810650 17883136 3909 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4366 3909 603 41 0 4325 0
vsize: 17464
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4015 0 0 0 95994 15 0 0 25 0 1 0 480810650 18284544 3993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4464 3993 603 41 0 4423 0
vsize: 17856
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4015 0 0 0 96994 15 0 0 25 0 1 0 480810650 18284544 3993 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4464 3993 603 41 0 4423 0
vsize: 17856
[startup+980.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4021 0 0 0 97994 15 0 0 25 0 1 0 480810650 18284544 3999 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4464 3999 603 41 0 4423 0
vsize: 17856
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4033 0 0 0 98994 15 0 0 25 0 1 0 480810650 18284544 4011 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4464 4011 603 41 0 4423 0
vsize: 17856
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4038 0 0 0 99994 15 0 0 25 0 1 0 480810650 18415616 4016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4016 603 41 0 4455 0
vsize: 17984
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4041 0 0 0 100994 15 0 0 25 0 1 0 480810650 18415616 4019 4294967295 134512640 134672761 3221224560 3221223720 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4019 603 41 0 4455 0
vsize: 17984
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4043 0 0 0 101995 15 0 0 25 0 1 0 480810650 18415616 4021 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4021 603 41 0 4455 0
vsize: 17984
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4047 0 0 0 102995 15 0 0 25 0 1 0 480810650 18415616 4025 4294967295 134512640 134672761 3221224560 3221223728 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4025 603 41 0 4455 0
vsize: 17984
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27379
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4051 0 0 0 103995 15 0 0 25 0 1 0 480810650 18415616 4029 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4051 0 0 0 104995 15 0 0 25 0 1 0 480810650 18415616 4029 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4029 603 41 0 4455 0
vsize: 17984
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4056 0 0 0 105995 15 0 0 25 0 1 0 480810650 18415616 4034 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4034 603 41 0 4455 0
vsize: 17984
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4056 0 0 0 106995 15 0 0 25 0 1 0 480810650 18415616 4034 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4496 4034 603 41 0 4455 0
vsize: 17984
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4095 0 0 0 107996 15 0 0 25 0 1 0 480810650 18546688 4073 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4073 603 41 0 4487 0
vsize: 18112
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4099 0 0 0 108996 15 0 0 25 0 1 0 480810650 18546688 4077 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4528 4077 603 41 0 4487 0
vsize: 18112
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4159 0 0 0 109996 16 0 0 25 0 1 0 480810650 18821120 4137 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4137 603 41 0 4554 0
vsize: 18380
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4159 0 0 0 110996 16 0 0 25 0 1 0 480810650 18821120 4137 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4595 4137 603 41 0 4554 0
vsize: 18380
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4179 0 0 0 111996 16 0 0 25 0 1 0 480810650 18980864 4157 4294967295 134512640 134672761 3221224560 3221223644 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4179 0 0 0 112996 16 0 0 25 0 1 0 480810650 18980864 4157 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4157 603 41 0 4593 0
vsize: 18536
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4184 0 0 0 113996 16 0 0 25 0 1 0 480810650 18980864 4162 4294967295 134512640 134672761 3221224560 3221223616 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4184 0 0 0 114997 16 0 0 25 0 1 0 480810650 18980864 4162 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4184 0 0 0 115997 16 0 0 25 0 1 0 480810650 18980864 4162 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4184 0 0 0 116997 16 0 0 25 0 1 0 480810650 18980864 4162 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4634 4162 603 41 0 4593 0
vsize: 18536
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4210 0 0 0 117997 16 0 0 25 0 1 0 480810650 19111936 4188 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4666 4188 603 41 0 4625 0
vsize: 18664
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4210 0 0 0 118997 16 0 0 25 0 1 0 480810650 19111936 4188 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4666 4188 603 41 0 4625 0
vsize: 18664
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27381
Raw data (stat): 27316 (minisat+) R 27315 20024 20023 0 -1 0 4214 0 0 0 119998 16 0 0 25 0 1 0 480810650 19111936 4192 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4666 4192 603 41 0 4625 0
vsize: 18664
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 27381
Raw data (stat): 27316 (minisat+) Z 27315 20024 20023 0 -1 12 4216 0 0 0 119998 17 0 0 25 0 1 0 480810650 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.15
CPU user time (s): 1199.98
CPU system time (s): 0.170974
CPU usage (%): 100.009
Max. virtual memory (Kb): 18664
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####