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-cmb.opb
MD5SUM	a8596c98551f801a6658f1ce91b33278
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1053
Optimality of the best value was proved	NO
Number of terms in the objective function	304
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	12887
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	12887
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.97785
Number of variables	304
Total number of constraints	671
Number of constraints which are clauses	671
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	28
Trace number 5209

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 22:30:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3637 boxname=wulflinc12 idbench=253 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a8596c98551f801a6658f1ce91b33278  /oldhome/oroussel/tmp/wulflinc12/normalized-cmb.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-cmb.opb /oldhome/oroussel/tmp/wulflinc12/normalized-cmb.opb
IDLAUNCH: 3637
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        919400 kB
Buffers:         34780 kB
Cached:          61288 kB
SwapCached:         16 kB
Active:          59532 kB
Inactive:        39464 kB
HighTotal:      131008 kB
HighFree:        65744 kB
LowTotal:       903652 kB
LowFree:        853656 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10664 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:50:33 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 3637 7 1200.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 667 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 |     667     3359 |     222       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1524[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1466   maxlim: 11363   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10848    39698 |    3616       0        0     nan |  0.000 % |
c |       101 |   10841    39675 |    3977     100      410     4.1 |  0.452 % |
c |       252 |   10807    39566 |    4375     249     1188     4.8 |  0.564 % |
c |       478 |   10741    39370 |    4812     470     2640     5.6 |  0.790 % |
c |       815 |   10726    39319 |    5294     803     5129     6.4 |  0.902 % |
c |      1323 |   10726    39319 |    5823    1311     8820     6.7 |  0.902 % |
c |      2083 |   10693    39218 |    6405    2065    18491     9.0 |  1.184 % |
c |      3222 |   10693    39218 |    7046    3204    59026    18.4 |  1.184 % |
c |      4930 |   10693    39218 |    7751    4912   159135    32.4 |  1.184 % |
c |      7492 |   10693    39218 |    8526    7474   340811    45.6 |  1.184 % |
c |     11338 |   10693    39218 |    9378    6961   311886    44.8 |  1.184 % |
c |     17104 |   10693    39218 |   10316    7817   500088    64.0 |  1.184 % |
c |     25754 |   10693    39218 |   11348    5719   420428    73.5 |  1.184 % |
c |     38728 |   10693    39218 |   12483    6951   504197    72.5 |  1.184 % |
c |     58190 |   10693    39218 |   13731    6923   633610    91.5 |  1.184 % |
c |     87383 |   10693    39218 |   15104    7790   700528    89.9 |  1.184 % |
c |    131175 |   10693    39218 |   16615   12791  1301608   101.8 |  1.184 % |
c |    196859 |   10693    39218 |   18276   10288   928499    90.3 |  1.184 % |
c |    295385 |   10693    39218 |   20104   15878  1236031    77.8 |  1.184 % |
c |    443174 |   10693    39218 |   22115   19453  2365896   121.6 |  1.184 % |
c |    664861 |   10693    39218 |   24326   15607  1466374    94.0 |  1.184 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 28946
Raw data (stat): 28946 (runsolver) R 28945 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421340220 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+9.99972 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 1376 0 0 0 994 4 0 0 25 0 1 0 421340220 7131136 1354 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1741 1354 603 41 0 1700 0
vsize: 6964
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 1661 0 0 0 1992 5 0 0 25 0 1 0 421340220 8335360 1639 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2035 1639 603 41 0 1994 0
vsize: 8140
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 1797 0 0 0 2992 5 0 0 25 0 1 0 421340220 8876032 1775 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2167 1775 603 41 0 2126 0
vsize: 8668
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2167 0 0 0 3991 6 0 0 25 0 1 0 421340220 10342400 2145 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2525 2145 603 41 0 2484 0
vsize: 10100
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2223 0 0 0 4991 6 0 0 25 0 1 0 421340220 10612736 2201 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2591 2201 603 41 0 2550 0
vsize: 10364
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2315 0 0 0 5991 7 0 0 25 0 1 0 421340220 11010048 2293 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2688 2293 603 41 0 2647 0
vsize: 10752
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2400 0 0 0 6991 7 0 0 25 0 1 0 421340220 11415552 2378 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2787 2378 603 41 0 2746 0
vsize: 11148
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2468 0 0 0 7991 7 0 0 25 0 1 0 421340220 11685888 2446 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2853 2446 603 41 0 2812 0
vsize: 11412
[startup+90.0056 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2468 0 0 0 8992 7 0 0 25 0 1 0 421340220 11685888 2446 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2853 2446 603 41 0 2812 0
vsize: 11412
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2590 0 0 0 9991 7 0 0 25 0 1 0 421340220 12087296 2568 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2951 2568 603 41 0 2910 0
vsize: 11804
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2732 0 0 0 10991 8 0 0 25 0 1 0 421340220 12754944 2710 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3114 2710 603 41 0 3073 0
vsize: 12456
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2750 0 0 0 11991 8 0 0 25 0 1 0 421340220 12926976 2728 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3156 2728 603 41 0 3115 0
vsize: 12624
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2750 0 0 0 12991 8 0 0 25 0 1 0 421340220 12926976 2728 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3156 2728 603 41 0 3115 0
vsize: 12624
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2781 0 0 0 13991 8 0 0 25 0 1 0 421340220 12926976 2759 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3156 2759 603 41 0 3115 0
vsize: 12624
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 2997 0 0 0 14991 9 0 0 25 0 1 0 421340220 13864960 2975 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3385 2975 603 41 0 3344 0
vsize: 13540
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3112 0 0 0 15990 9 0 0 25 0 1 0 421340220 14405632 3090 4294967295 134512640 134672761 3221224576 3221223760 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3090 603 41 0 3476 0
vsize: 14068
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3112 0 0 0 16990 9 0 0 25 0 1 0 421340220 14405632 3090 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3517 3090 603 41 0 3476 0
vsize: 14068
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3112 0 0 0 17989 10 0 0 25 0 1 0 421340220 14405632 3090 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3517 3090 603 41 0 3476 0
vsize: 14068
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3112 0 0 0 18989 10 0 0 25 0 1 0 421340220 14405632 3090 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3517 3090 603 41 0 3476 0
vsize: 14068
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3114 0 0 0 19988 10 0 0 25 0 1 0 421340220 14405632 3092 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3092 603 41 0 3476 0
vsize: 14068
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3114 0 0 0 20988 10 0 0 25 0 1 0 421340220 14405632 3092 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3092 603 41 0 3476 0
vsize: 14068
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3114 0 0 0 21989 10 0 0 25 0 1 0 421340220 14405632 3092 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3092 603 41 0 3476 0
vsize: 14068
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3119 0 0 0 22989 10 0 0 25 0 1 0 421340220 14405632 3097 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3097 603 41 0 3476 0
vsize: 14068
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3124 0 0 0 23989 10 0 0 25 0 1 0 421340220 14405632 3102 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3102 603 41 0 3476 0
vsize: 14068
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3124 0 0 0 24989 10 0 0 25 0 1 0 421340220 14405632 3102 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3102 603 41 0 3476 0
vsize: 14068
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3124 0 0 0 25989 10 0 0 25 0 1 0 421340220 14405632 3102 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3102 603 41 0 3476 0
vsize: 14068
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3124 0 0 0 26989 10 0 0 25 0 1 0 421340220 14405632 3102 4294967295 134512640 134672761 3221224576 3221223760 134559503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3102 603 41 0 3476 0
vsize: 14068
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3319 0 0 0 27989 11 0 0 25 0 1 0 421340220 15204352 3297 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3297 603 41 0 3671 0
vsize: 14848
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3319 0 0 0 28989 11 0 0 25 0 1 0 421340220 15204352 3297 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3297 603 41 0 3671 0
vsize: 14848
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3319 0 0 0 29989 11 0 0 25 0 1 0 421340220 15204352 3297 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3297 603 41 0 3671 0
vsize: 14848
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3320 0 0 0 30989 11 0 0 25 0 1 0 421340220 15204352 3298 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3298 603 41 0 3671 0
vsize: 14848
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3334 0 0 0 31990 11 0 0 25 0 1 0 421340220 15204352 3312 4294967295 134512640 134672761 3221224576 3221223648 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3712 3312 603 41 0 3671 0
vsize: 14848
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3616 0 0 0 32988 12 0 0 25 0 1 0 421340220 16400384 3594 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4004 3594 603 41 0 3963 0
vsize: 16016
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3771 0 0 0 33988 13 0 0 25 0 1 0 421340220 17059840 3749 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4165 3749 603 41 0 4124 0
vsize: 16660
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 3835 0 0 0 34988 13 0 0 25 0 1 0 421340220 17326080 3813 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4230 3813 603 41 0 4189 0
vsize: 16920
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4037 0 0 0 35987 14 0 0 25 0 1 0 421340220 18124800 4015 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 4015 603 41 0 4384 0
vsize: 17700
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4038 0 0 0 36988 14 0 0 25 0 1 0 421340220 18124800 4016 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4425 4016 603 41 0 4384 0
vsize: 17700
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4312 0 0 0 37987 15 0 0 25 0 1 0 421340220 19320832 4290 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4290 603 41 0 4676 0
vsize: 18868
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4312 0 0 0 38987 15 0 0 25 0 1 0 421340220 19320832 4290 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4290 603 41 0 4676 0
vsize: 18868
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4333 0 0 0 39987 15 0 0 25 0 1 0 421340220 19320832 4311 4294967295 134512640 134672761 3221224576 3221223680 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4717 4311 603 41 0 4676 0
vsize: 18868
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4350 0 0 0 40987 15 0 0 25 0 1 0 421340220 19464192 4328 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4752 4328 603 41 0 4711 0
vsize: 19008
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4432 0 0 0 41987 15 0 0 25 0 1 0 421340220 19730432 4410 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4817 4410 603 41 0 4776 0
vsize: 19268
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4433 0 0 0 42987 15 0 0 25 0 1 0 421340220 19730432 4411 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4817 4411 603 41 0 4776 0
vsize: 19268
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4437 0 0 0 43988 15 0 0 25 0 1 0 421340220 19865600 4415 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4415 603 41 0 4809 0
vsize: 19400
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4458 0 0 0 44988 15 0 0 25 0 1 0 421340220 19865600 4436 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4436 603 41 0 4809 0
vsize: 19400
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 45988 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223760 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 46988 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 47988 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 48989 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 49989 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 50989 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4459 0 0 0 51989 15 0 0 25 0 1 0 421340220 19865600 4437 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4437 603 41 0 4809 0
vsize: 19400
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4460 0 0 0 52989 15 0 0 25 0 1 0 421340220 19865600 4438 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4438 603 41 0 4809 0
vsize: 19400
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4461 0 0 0 53990 15 0 0 25 0 1 0 421340220 19865600 4439 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4850 4439 603 41 0 4809 0
vsize: 19400
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 54989 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+560.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 55989 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 56989 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223680 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 57990 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 58990 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 59990 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 60991 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 61991 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 62991 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 63991 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+650.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 64992 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+660.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 65992 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223760 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4462 0 0 0 66992 16 0 0 25 0 1 0 421340220 19865600 4440 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4440 603 41 0 4809 0
vsize: 19400
[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4525 0 0 0 67992 16 0 0 25 0 1 0 421340220 20127744 4503 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4914 4503 603 41 0 4873 0
vsize: 19656
[startup+690.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 68992 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+700.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 69992 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+710.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 70993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 71993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 72993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 73993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223712 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 74993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223712 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 75993 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+770.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 76994 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+780.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4540 0 0 0 77994 16 0 0 25 0 1 0 421340220 20271104 4518 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4518 603 41 0 4908 0
vsize: 19796
[startup+790.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4542 0 0 0 78994 16 0 0 25 0 1 0 421340220 20271104 4520 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4520 603 41 0 4908 0
vsize: 19796
[startup+800.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4543 0 0 0 79994 16 0 0 25 0 1 0 421340220 20271104 4521 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4521 603 41 0 4908 0
vsize: 19796
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4543 0 0 0 80994 16 0 0 25 0 1 0 421340220 20271104 4521 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4521 603 41 0 4908 0
vsize: 19796
[startup+820.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4543 0 0 0 81994 16 0 0 25 0 1 0 421340220 20271104 4521 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4949 4521 603 41 0 4908 0
vsize: 19796
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4543 0 0 0 82994 16 0 0 25 0 1 0 421340220 20271104 4521 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4521 603 41 0 4908 0
vsize: 19796
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 83994 16 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 84993 16 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223764 1075346980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 85993 17 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+870.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 86993 17 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+880.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 87992 17 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+890.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 88992 17 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+900.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 89991 18 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+910.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 90991 18 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+920.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 91991 18 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 92990 19 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+940.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 93990 19 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+950.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 94989 20 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+960.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 95989 20 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+970.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4545 0 0 0 96988 20 0 0 25 0 1 0 421340220 20271104 4523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4949 4523 603 41 0 4908 0
vsize: 19796
[startup+980.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4664 0 0 0 97988 21 0 0 25 0 1 0 421340220 20836352 4642 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5087 4642 603 41 0 5046 0
vsize: 20348
[startup+990.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4669 0 0 0 98987 21 0 0 25 0 1 0 421340220 20836352 4647 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5087 4647 603 41 0 5046 0
vsize: 20348
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4704 0 0 0 99987 22 0 0 25 0 1 0 421340220 20971520 4682 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4682 603 41 0 5079 0
vsize: 20480
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4704 0 0 0 100986 22 0 0 25 0 1 0 421340220 20971520 4682 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4682 603 41 0 5079 0
vsize: 20480
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4704 0 0 0 101986 23 0 0 25 0 1 0 421340220 20971520 4682 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5120 4682 603 41 0 5079 0
vsize: 20480
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4732 0 0 0 102985 23 0 0 25 0 1 0 421340220 21106688 4710 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5153 4710 603 41 0 5112 0
vsize: 20612
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4742 0 0 0 103985 23 0 0 25 0 1 0 421340220 21106688 4720 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5153 4720 603 41 0 5112 0
vsize: 20612
[startup+1050.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4841 0 0 0 104984 24 0 0 25 0 1 0 421340220 21520384 4819 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5254 4819 603 41 0 5213 0
vsize: 21016
[startup+1060.05 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4849 0 0 0 105984 24 0 0 25 0 1 0 421340220 21520384 4827 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5254 4827 603 41 0 5213 0
vsize: 21016
[startup+1070.05 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4889 0 0 0 106983 25 0 0 25 0 1 0 421340220 21790720 4867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5320 4867 603 41 0 5279 0
vsize: 21280
[startup+1080.05 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4889 0 0 0 107983 25 0 0 25 0 1 0 421340220 21790720 4867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5320 4867 603 41 0 5279 0
vsize: 21280
[startup+1090.05 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4923 0 0 0 108982 26 0 0 25 0 1 0 421340220 21921792 4901 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5352 4901 603 41 0 5311 0
vsize: 21408
[startup+1100.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4929 0 0 0 109982 26 0 0 25 0 1 0 421340220 21921792 4907 4294967295 134512640 134672761 3221224576 3221223760 134558909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5352 4907 603 41 0 5311 0
vsize: 21408
[startup+1110.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4979 0 0 0 110982 26 0 0 25 0 1 0 421340220 22052864 4957 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5384 4957 603 41 0 5343 0
vsize: 21536
[startup+1120.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 4983 0 0 0 111982 26 0 0 25 0 1 0 421340220 22192128 4961 4294967295 134512640 134672761 3221224576 3221223760 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5418 4961 603 41 0 5377 0
vsize: 21672
[startup+1130.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5036 0 0 0 112981 26 0 0 25 0 1 0 421340220 22339584 5014 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5454 5014 603 41 0 5413 0
vsize: 21816
[startup+1140.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5138 0 0 0 113981 27 0 0 25 0 1 0 421340220 22876160 5116 4294967295 134512640 134672761 3221224576 3221223636 1075349617 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5116 603 41 0 5544 0
vsize: 22340
[startup+1150.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5147 0 0 0 114981 27 0 0 25 0 1 0 421340220 22876160 5125 4294967295 134512640 134672761 3221224576 3221223776 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5125 603 41 0 5544 0
vsize: 22340
[startup+1160.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5147 0 0 0 115980 27 0 0 25 0 1 0 421340220 22876160 5125 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5125 603 41 0 5544 0
vsize: 22340
[startup+1170.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5149 0 0 0 116980 28 0 0 25 0 1 0 421340220 22876160 5127 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5127 603 41 0 5544 0
vsize: 22340
[startup+1180.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5149 0 0 0 117979 28 0 0 25 0 1 0 421340220 22876160 5127 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5127 603 41 0 5544 0
vsize: 22340
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5149 0 0 0 118979 28 0 0 25 0 1 0 421340220 22876160 5127 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5127 603 41 0 5544 0
vsize: 22340
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28946
Raw data (stat): 28946 (minisat+) R 28945 25285 25284 0 -1 0 5149 0 0 0 119979 28 0 0 25 0 1 0 421340220 22876160 5127 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5127 603 41 0 5544 0
vsize: 22340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28946
Raw data (stat): 28946 (minisat+) Z 28945 25285 25284 0 -1 12 5152 0 0 0 119979 29 0 0 25 0 1 0 421340220 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.09
CPU user time (s): 1199.8
CPU system time (s): 0.298954
CPU usage (%): 100.002
Max. virtual memory (Kb): 22340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####