PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb
MD5SUM	9b291040ec2b77d0bffb739c0db80d53
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1194
Optimality of the best value was proved	NO
Number of terms in the objective function	239
Biggest coefficient in the objective function	61
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	10012
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	61
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	10012
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.941856
Number of variables	239
Total number of constraints	524
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	4
Minimum length of a constraint	1
Maximum length of a constraint	36
Trace number 5206

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 22:27:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3634 boxname=wulflinc6 idbench=250 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc6/normalized-c8.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-c8.opb /oldhome/oroussel/tmp/wulflinc6/normalized-c8.opb
IDLAUNCH: 3634
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        913784 kB
Buffers:         34864 kB
Cached:          64220 kB
SwapCached:       2644 kB
Active:          51128 kB
Inactive:        53480 kB
HighTotal:      131008 kB
HighFree:        62888 kB
LowTotal:       903652 kB
LowFree:        850896 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10712 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:47:46 (client local time) WITH STATUS 10 IN 1200.42 SECONDS
stats: 3634 7 1200.42 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 519 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 |     519     2283 |     173       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1761[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1280   maxlim: 8251   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |    9369    33879 |    3123       1       14    14.0 |  0.000 % |
c |       101 |    9369    33879 |    3435     101      444     4.4 |  0.789 % |
c |       251 |    9355    33840 |    3778     249     1311     5.3 |  0.855 % |
c |       477 |    9338    33795 |    4156     473     9817    20.8 |  0.920 % |
c |       814 |    9266    33587 |    4572     801    11582    14.5 |  1.315 % |
c |      1320 |    9266    33587 |    5029    1307    19391    14.8 |  1.315 % |
c |      2079 |    9266    33587 |    5532    2066    39232    19.0 |  1.315 % |
c |      3219 |    9266    33587 |    6085    3206    80009    25.0 |  1.315 % |
c |      4927 |    9266    33587 |    6694    4914   187737    38.2 |  1.315 % |
c |      7489 |    9266    33587 |    7363    3967   180247    45.4 |  1.315 % |
c |     11333 |    9266    33587 |    8100    3921   187887    47.9 |  1.315 % |
c |     17101 |    9266    33587 |    8910    5366   396134    73.8 |  1.315 % |
c |     25753 |    9266    33587 |    9801    4843   299553    61.9 |  1.315 % |
c |     38727 |    9266    33587 |   10781    7701   565591    73.4 |  1.315 % |
c |     58189 |    9266    33587 |   11859   10263  1108351   108.0 |  1.315 % |
c |     87383 |    9266    33587 |   13045    8743   829241    94.8 |  1.315 % |
c |    131172 |    9266    33587 |   14350   12537   996233    79.5 |  1.315 % |
c |    196856 |    9266    33587 |   15785   11454   840873    73.4 |  1.315 % |
c |    295382 |    9266    33587 |   17363   12800  1223472    95.6 |  1.315 % |
c |    443174 |    9266    33587 |   19099   10420   828156    79.5 |  1.315 % |
c |    664860 |    9266    33587 |   21009   17981  1701249    94.6 |  1.315 % |
#### 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.85 0.94 0.90 1/54 32601
Raw data (stat): 32601 (runsolver) R 32600 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421326088 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 1227 0 0 0 995 3 0 0 25 0 1 0 421326088 6533120 1205 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1595 1205 603 41 0 1554 0
vsize: 6380
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 1414 0 0 0 1994 4 0 0 25 0 1 0 421326088 7340032 1392 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1792 1392 603 41 0 1751 0
vsize: 7168
[startup+30.002 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 1806 0 0 0 2994 5 0 0 25 0 1 0 421326088 8962048 1784 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2188 1784 603 41 0 2147 0
vsize: 8752
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2042 0 0 0 3993 6 0 0 25 0 1 0 421326088 9900032 2020 4294967295 134512640 134672761 3221224576 3221223744 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2417 2020 603 41 0 2376 0
vsize: 9668
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2069 0 0 0 4993 6 0 0 25 0 1 0 421326088 10035200 2047 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2450 2047 603 41 0 2409 0
vsize: 9800
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2069 0 0 0 5994 6 0 0 25 0 1 0 421326088 10035200 2047 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2450 2047 603 41 0 2409 0
vsize: 9800
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2109 0 0 0 6994 6 0 0 25 0 1 0 421326088 10170368 2087 4294967295 134512640 134672761 3221224576 3221223760 134558856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2483 2087 603 41 0 2442 0
vsize: 9932
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2124 0 0 0 7994 6 0 0 25 0 1 0 421326088 10301440 2102 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2515 2102 603 41 0 2474 0
vsize: 10060
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2124 0 0 0 8994 6 0 0 25 0 1 0 421326088 10301440 2102 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2515 2102 603 41 0 2474 0
vsize: 10060
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2124 0 0 0 9995 6 0 0 25 0 1 0 421326088 10301440 2102 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2515 2102 603 41 0 2474 0
vsize: 10060
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2124 0 0 0 10995 6 0 0 25 0 1 0 421326088 10297344 2102 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2514 2102 603 41 0 2473 0
vsize: 10056
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2256 0 0 0 11995 7 0 0 25 0 1 0 421326088 10833920 2234 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2645 2234 603 41 0 2604 0
vsize: 10580
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2471 0 0 0 12995 7 0 0 25 0 1 0 421326088 11632640 2449 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2449 603 41 0 2799 0
vsize: 11360
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2471 0 0 0 13995 7 0 0 25 0 1 0 421326088 11632640 2449 4294967295 134512640 134672761 3221224576 3221223760 134559334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2449 603 41 0 2799 0
vsize: 11360
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2471 0 0 0 14995 7 0 0 25 0 1 0 421326088 11632640 2449 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2449 603 41 0 2799 0
vsize: 11360
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2473 0 0 0 15996 7 0 0 25 0 1 0 421326088 11632640 2451 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2840 2451 603 41 0 2799 0
vsize: 11360
[startup+170.007 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2537 0 0 0 16996 7 0 0 25 0 1 0 421326088 11894784 2515 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2904 2515 603 41 0 2863 0
vsize: 11616
[startup+180.007 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2559 0 0 0 17996 8 0 0 25 0 1 0 421326088 12038144 2537 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2939 2537 603 41 0 2898 0
vsize: 11756
[startup+190.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2559 0 0 0 18996 8 0 0 25 0 1 0 421326088 12038144 2537 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2939 2537 603 41 0 2898 0
vsize: 11756
[startup+200.009 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2567 0 0 0 19996 8 0 0 25 0 1 0 421326088 12222464 2545 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2984 2545 603 41 0 2943 0
vsize: 11936
[startup+210.01 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2705 0 0 0 20996 8 0 0 25 0 1 0 421326088 12759040 2683 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3115 2683 603 41 0 3074 0
vsize: 12460
[startup+220.011 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2777 0 0 0 21996 9 0 0 25 0 1 0 421326088 13025280 2755 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3180 2755 603 41 0 3139 0
vsize: 12720
[startup+230.011 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2777 0 0 0 22996 9 0 0 25 0 1 0 421326088 13025280 2755 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3180 2755 603 41 0 3139 0
vsize: 12720
[startup+240.011 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2780 0 0 0 23996 9 0 0 25 0 1 0 421326088 13025280 2758 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3180 2758 603 41 0 3139 0
vsize: 12720
[startup+250.011 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2858 0 0 0 24996 9 0 0 25 0 1 0 421326088 13426688 2836 4294967295 134512640 134672761 3221224576 3221223744 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3278 2836 603 41 0 3237 0
vsize: 13112
[startup+260.012 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 2867 0 0 0 25997 9 0 0 25 0 1 0 421326088 13426688 2845 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3278 2845 603 41 0 3237 0
vsize: 13112
[startup+270.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3111 0 0 0 26996 10 0 0 25 0 1 0 421326088 14356480 3089 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3505 3089 603 41 0 3464 0
vsize: 14020
[startup+280.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3341 0 0 0 27996 11 0 0 25 0 1 0 421326088 15409152 3319 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3319 603 41 0 3721 0
vsize: 15048
[startup+290.015 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3345 0 0 0 28996 11 0 0 25 0 1 0 421326088 15409152 3323 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3323 603 41 0 3721 0
vsize: 15048
[startup+300.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3345 0 0 0 29997 11 0 0 25 0 1 0 421326088 15409152 3323 4294967295 134512640 134672761 3221224576 3221223700 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3323 603 41 0 3721 0
vsize: 15048
[startup+310.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 30996 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+320.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 31997 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+330.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 32997 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+340.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 33998 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223680 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+350.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 34998 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+360.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 35998 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+370.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 36999 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+380.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 37999 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+390.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 38999 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+400.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 40000 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+410.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 41000 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+420.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 42001 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+430.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 43001 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+440.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 44001 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+450.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 45002 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+460.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 46002 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+470.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 47003 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+480.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 48003 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+490.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 49003 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+500.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3346 0 0 0 50003 11 0 0 25 0 1 0 421326088 15409152 3324 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3324 603 41 0 3721 0
vsize: 15048
[startup+510.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3348 0 0 0 51004 11 0 0 25 0 1 0 421326088 15409152 3326 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3326 603 41 0 3721 0
vsize: 15048
[startup+520.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3348 0 0 0 52004 11 0 0 25 0 1 0 421326088 15409152 3326 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3762 3326 603 41 0 3721 0
vsize: 15048
[startup+530.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3447 0 0 0 53004 11 0 0 25 0 1 0 421326088 15826944 3425 4294967295 134512640 134672761 3221224576 3221223760 134559422 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3864 3425 603 41 0 3823 0
vsize: 15456
[startup+540.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3454 0 0 0 54005 11 0 0 25 0 1 0 421326088 15826944 3432 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3864 3432 603 41 0 3823 0
vsize: 15456
[startup+550.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3457 0 0 0 55006 11 0 0 25 0 1 0 421326088 15826944 3435 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3864 3435 603 41 0 3823 0
vsize: 15456
[startup+560.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 56006 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+570.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 57006 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+580.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 58007 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+590.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 59007 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223680 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+600.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 60008 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+610.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3524 0 0 0 61008 11 0 0 25 0 1 0 421326088 16093184 3502 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3502 603 41 0 3888 0
vsize: 15716
[startup+620.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3526 0 0 0 62008 11 0 0 25 0 1 0 421326088 16093184 3504 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3929 3504 603 41 0 3888 0
vsize: 15716
[startup+630.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3546 0 0 0 63009 11 0 0 25 0 1 0 421326088 16228352 3524 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3962 3524 603 41 0 3921 0
vsize: 15848
[startup+640.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3559 0 0 0 64009 11 0 0 25 0 1 0 421326088 16228352 3537 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3962 3537 603 41 0 3921 0
vsize: 15848
[startup+650.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3569 0 0 0 65009 11 0 0 25 0 1 0 421326088 16359424 3547 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3547 603 41 0 3953 0
vsize: 15976
[startup+660.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3590 0 0 0 66010 11 0 0 25 0 1 0 421326088 16359424 3568 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3568 603 41 0 3953 0
vsize: 15976
[startup+670.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3590 0 0 0 67010 11 0 0 25 0 1 0 421326088 16359424 3568 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3568 603 41 0 3953 0
vsize: 15976
[startup+680.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3590 0 0 0 68010 11 0 0 25 0 1 0 421326088 16359424 3568 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3994 3568 603 41 0 3953 0
vsize: 15976
[startup+690.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3596 0 0 0 69011 11 0 0 25 0 1 0 421326088 16494592 3574 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4027 3574 603 41 0 3986 0
vsize: 16108
[startup+700.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3599 0 0 0 70011 11 0 0 25 0 1 0 421326088 16494592 3577 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4027 3577 603 41 0 3986 0
vsize: 16108
[startup+710.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3606 0 0 0 71012 11 0 0 25 0 1 0 421326088 16494592 3584 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4027 3584 603 41 0 3986 0
vsize: 16108
[startup+720.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3630 0 0 0 72012 11 0 0 25 0 1 0 421326088 16629760 3608 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3608 603 41 0 4019 0
vsize: 16240
[startup+730.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3635 0 0 0 73012 11 0 0 25 0 1 0 421326088 16629760 3613 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3613 603 41 0 4019 0
vsize: 16240
[startup+740.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3635 0 0 0 74013 11 0 0 25 0 1 0 421326088 16629760 3613 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4060 3613 603 41 0 4019 0
vsize: 16240
[startup+750.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3674 0 0 0 75013 12 0 0 25 0 1 0 421326088 16764928 3652 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4093 3652 603 41 0 4052 0
vsize: 16372
[startup+760.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3678 0 0 0 76013 12 0 0 25 0 1 0 421326088 16764928 3656 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4093 3656 603 41 0 4052 0
vsize: 16372
[startup+770.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3678 0 0 0 77014 12 0 0 25 0 1 0 421326088 16764928 3656 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4093 3656 603 41 0 4052 0
vsize: 16372
[startup+780.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3678 0 0 0 78014 12 0 0 25 0 1 0 421326088 16764928 3656 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4093 3656 603 41 0 4052 0
vsize: 16372
[startup+790.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3678 0 0 0 79014 12 0 0 25 0 1 0 421326088 16764928 3656 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4093 3656 603 41 0 4052 0
vsize: 16372
[startup+800.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 3934 0 0 0 80013 13 0 0 25 0 1 0 421326088 17833984 3912 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4354 3912 603 41 0 4313 0
vsize: 17416
[startup+810.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4029 0 0 0 81013 13 0 0 25 0 1 0 421326088 18235392 4007 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4452 4007 603 41 0 4411 0
vsize: 17808
[startup+820.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4038 0 0 0 82013 14 0 0 25 0 1 0 421326088 18235392 4016 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4452 4016 603 41 0 4411 0
vsize: 17808
[startup+830.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4205 0 0 0 83013 14 0 0 25 0 1 0 421326088 19034112 4183 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4183 603 41 0 4606 0
vsize: 18588
[startup+840.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4206 0 0 0 84013 14 0 0 25 0 1 0 421326088 19034112 4184 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4184 603 41 0 4606 0
vsize: 18588
[startup+850.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4318 0 0 0 85013 14 0 0 25 0 1 0 421326088 19431424 4296 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4744 4296 603 41 0 4703 0
vsize: 18976
[startup+860.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4318 0 0 0 86014 14 0 0 25 0 1 0 421326088 19431424 4296 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4744 4296 603 41 0 4703 0
vsize: 18976
[startup+870.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4320 0 0 0 87013 15 0 0 25 0 1 0 421326088 19431424 4298 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4744 4298 603 41 0 4703 0
vsize: 18976
[startup+880.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4335 0 0 0 88014 15 0 0 25 0 1 0 421326088 19582976 4313 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4313 603 41 0 4740 0
vsize: 19124
[startup+890.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4336 0 0 0 89014 15 0 0 25 0 1 0 421326088 19582976 4314 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4314 603 41 0 4740 0
vsize: 19124
[startup+900.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4336 0 0 0 90014 15 0 0 25 0 1 0 421326088 19582976 4314 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4314 603 41 0 4740 0
vsize: 19124
[startup+910.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4342 0 0 0 91015 15 0 0 25 0 1 0 421326088 19582976 4320 4294967295 134512640 134672761 3221224576 3221223644 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4320 603 41 0 4740 0
vsize: 19124
[startup+920.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4342 0 0 0 92015 15 0 0 25 0 1 0 421326088 19582976 4320 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4320 603 41 0 4740 0
vsize: 19124
[startup+930.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4342 0 0 0 93015 15 0 0 25 0 1 0 421326088 19582976 4320 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4320 603 41 0 4740 0
vsize: 19124
[startup+940.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4342 0 0 0 94016 15 0 0 25 0 1 0 421326088 19582976 4320 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4320 603 41 0 4740 0
vsize: 19124
[startup+950.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4342 0 0 0 95016 15 0 0 25 0 1 0 421326088 19582976 4320 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4320 603 41 0 4740 0
vsize: 19124
[startup+960.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4418 0 0 0 96016 15 0 0 25 0 1 0 421326088 19849216 4396 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4846 4396 603 41 0 4805 0
vsize: 19384
[startup+970.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4455 0 0 0 97017 15 0 0 25 0 1 0 421326088 19992576 4433 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4881 4433 603 41 0 4840 0
vsize: 19524
[startup+980.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 98017 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+990.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 99017 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 100018 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 101018 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 102019 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4469 0 0 0 103019 15 0 0 25 0 1 0 421326088 20123648 4447 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4447 603 41 0 4872 0
vsize: 19652
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 104019 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 105020 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 106020 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223680 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 107021 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 108021 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1090.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 109021 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1100.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 110022 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1110.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 111022 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1120.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 112022 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223680 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1130.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 113023 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223712 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1140.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 114023 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 115023 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 116023 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 117024 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 118024 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 119025 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32601
Raw data (stat): 32601 (minisat+) R 32600 29653 29652 0 -1 0 4474 0 0 0 120025 15 0 0 25 0 1 0 421326088 20123648 4452 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4913 4452 603 41 0 4872 0
vsize: 19652
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 32601
Raw data (stat): 32601 (minisat+) Z 32600 29653 29652 0 -1 12 4477 0 0 0 120025 16 0 0 25 0 1 0 421326088 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: 10
Real time (s): 1200.07
CPU time (s): 1200.42
CPU user time (s): 1200.25
CPU system time (s): 0.168974
CPU usage (%): 100.029
Max. virtual memory (Kb): 19652
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####