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/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb
MD5SUM	112c693a7a90a8dc93ad23dc136d9b75
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	22
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.026995
Number of variables	840
Total number of constraints	82
Number of constraints which are clauses	42
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	21
Trace number 6086

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        850588 kB
Buffers:         36232 kB
Cached:         124508 kB
SwapCached:       3276 kB
Active:          80704 kB
Inactive:        86140 kB
HighTotal:      131008 kB
HighFree:         8036 kB
LowTotal:       903652 kB
LowFree:        842552 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11364 kB
Committed_AS:    71640 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:41:13 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4520 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 82 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................
c ---[  39]---> BDD-cost:   39
c ---[  38]---> BDD-cost:   39
c ---[  37]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   39
c ---[  35]---> BDD-cost:   39
c ---[  34]---> BDD-cost:   39
c ---[  33]---> BDD-cost:   39
c ---[  32]---> BDD-cost:   39
c ---[  31]---> BDD-cost:   39
c ---[  30]---> BDD-cost:   39
c ---[  29]---> BDD-cost:   39
c ---[  28]---> BDD-cost:   39
c ---[  27]---> BDD-cost:   39
c ---[  26]---> BDD-cost:   39
c ---[  25]---> BDD-cost:   39
c ---[  24]---> BDD-cost:   39
c ---[  23]---> BDD-cost:   39
c ---[  22]---> BDD-cost:   39
c ---[  21]---> BDD-cost:   39
c ---[  20]---> BDD-cost:   39
c ---[  19]---> BDD-cost:   39
c ---[  18]---> BDD-cost:   39
c ---[  17]---> BDD-cost:   39
c ---[  16]---> BDD-cost:   39
c ---[  15]---> BDD-cost:   39
c ---[  14]---> BDD-cost:   39
c ---[  13]---> BDD-cost:   39
c ---[  12]---> BDD-cost:   39
c ---[  11]---> BDD-cost:   39
c ---[  10]---> BDD-cost:   39
c ---[   9]---> BDD-cost:   39
c ---[   8]---> BDD-cost:   39
c ---[   7]---> BDD-cost:   39
c ---[   6]---> BDD-cost:   39
c ---[   5]---> BDD-cost:   39
c ---[   4]---> BDD-cost:   39
c ---[   3]---> BDD-cost:   39
c ---[   2]---> BDD-cost:   39
c ---[   1]---> BDD-cost:   39
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6882    19760 |    2294       0        0     nan |  0.000 % |
c |       101 |    6882    19760 |    2523     101     6935    68.7 |  1.667 % |
c |       252 |    6712    19250 |    2775     166     9493    57.2 |  3.083 % |
c |       477 |    6497    18605 |    3053     290    18134    62.5 |  4.875 % |
c |       816 |    6412    18350 |    3358     596    49041    82.3 |  5.583 % |
c |      1323 |    6347    18155 |    3694    1067   102118    95.7 |  6.125 % |
c |      2083 |    6327    18095 |    4063    1818   251345   138.3 |  6.292 % |
c |      3222 |    6262    17900 |    4470    2937   397201   135.2 |  6.833 % |
c |      4930 |    6203    17725 |    4917    4622   756092   163.6 |  7.333 % |
c |      7492 |    6138    17530 |    5409    4403   905330   205.6 |  7.875 % |
c |     11336 |    6063    17305 |    5950    4961   910789   183.6 |  8.500 % |
c |     17102 |    5696    16210 |    6545    3978   669255   168.2 | 11.583 % |
c |     25755 |    5482    15570 |    7199    4979   968543   194.5 | 13.375 % |
c |     38729 |    5179    14665 |    7919    5579  1026460   184.0 | 15.917 % |
c |     58191 |    4782    13480 |    8711    7413  1079997   145.7 | 19.250 % |
c |     87383 |    4512    12670 |    9582    7321  1293023   176.6 | 21.500 % |
c |    131175 |    4145    11575 |   10540    8886  1678772   188.9 | 24.583 % |
c |    196859 |    3830    10630 |   11594   10679  1954703   183.0 | 27.208 % |
c |    295388 |    3662    10130 |   12754    7300  1383568   189.5 | 28.625 % |
#### 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.92 0.98 0.93 2/54 19124
Raw data (stat): 19124 (runsolver) R 19123 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423083707 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 1969 0 0 0 994 4 0 0 25 0 1 0 423083707 9633792 1947 4294967295 134512640 134672761 3221224544 3221223728 134559166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2352 1947 603 41 0 2311 0
vsize: 9408
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2028 0 0 0 1993 4 0 0 25 0 1 0 423083707 9900032 2006 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2417 2006 603 41 0 2376 0
vsize: 9668
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2175 0 0 0 2992 5 0 0 25 0 1 0 423083707 10436608 2153 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2548 2153 603 41 0 2507 0
vsize: 10192
[startup+40.003 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2487 0 0 0 3991 6 0 0 25 0 1 0 423083707 11776000 2465 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2875 2465 603 41 0 2834 0
vsize: 11500
[startup+50.0038 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2500 0 0 0 4991 6 0 0 25 0 1 0 423083707 11911168 2478 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2908 2478 603 41 0 2867 0
vsize: 11632
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2560 0 0 0 5991 6 0 0 25 0 1 0 423083707 12042240 2538 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2940 2538 603 41 0 2899 0
vsize: 11760
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2891 0 0 0 6990 7 0 0 25 0 1 0 423083707 13381632 2869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3267 2869 603 41 0 3226 0
vsize: 13068
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2931 0 0 0 7990 7 0 0 25 0 1 0 423083707 13676544 2909 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2909 603 41 0 3298 0
vsize: 13356
[startup+90.0058 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2932 0 0 0 8991 7 0 0 25 0 1 0 423083707 13676544 2910 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2910 603 41 0 3298 0
vsize: 13356
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 2932 0 0 0 9991 7 0 0 25 0 1 0 423083707 13676544 2910 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2910 603 41 0 3298 0
vsize: 13356
[startup+110.006 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3001 0 0 0 10990 8 0 0 25 0 1 0 423083707 13938688 2979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3403 2979 603 41 0 3362 0
vsize: 13612
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3115 0 0 0 11990 8 0 0 25 0 1 0 423083707 14344192 3093 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 3093 603 41 0 3461 0
vsize: 14008
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3115 0 0 0 12991 8 0 0 25 0 1 0 423083707 14344192 3093 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3502 3093 603 41 0 3461 0
vsize: 14008
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3196 0 0 0 13991 8 0 0 25 0 1 0 423083707 14749696 3174 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3601 3174 603 41 0 3560 0
vsize: 14404
[startup+150.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3226 0 0 0 14991 8 0 0 25 0 1 0 423083707 14888960 3204 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3635 3204 603 41 0 3594 0
vsize: 14540
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3324 0 0 0 15991 8 0 0 25 0 1 0 423083707 15347712 3302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3747 3302 603 41 0 3706 0
vsize: 14988
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3324 0 0 0 16991 8 0 0 25 0 1 0 423083707 15347712 3302 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3747 3302 603 41 0 3706 0
vsize: 14988
[startup+180.008 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3324 0 0 0 17991 8 0 0 25 0 1 0 423083707 15347712 3302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3747 3302 603 41 0 3706 0
vsize: 14988
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3324 0 0 0 18992 8 0 0 25 0 1 0 423083707 15347712 3302 4294967295 134512640 134672761 3221224544 3221223648 134554907 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3747 3302 603 41 0 3706 0
vsize: 14988
[startup+200.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3621 0 0 0 19991 9 0 0 25 0 1 0 423083707 16556032 3599 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4042 3599 603 41 0 4001 0
vsize: 16168
[startup+210.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3626 0 0 0 20991 9 0 0 25 0 1 0 423083707 16556032 3604 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4042 3604 603 41 0 4001 0
vsize: 16168
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3809 0 0 0 21991 9 0 0 25 0 1 0 423083707 17371136 3787 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4241 3787 603 41 0 4200 0
vsize: 16964
[startup+230.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 3953 0 0 0 22990 10 0 0 25 0 1 0 423083707 17907712 3931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4372 3931 603 41 0 4331 0
vsize: 17488
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4081 0 0 0 23990 10 0 0 25 0 1 0 423083707 18460672 4059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4059 603 41 0 4466 0
vsize: 18028
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4081 0 0 0 24990 10 0 0 25 0 1 0 423083707 18460672 4059 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4059 603 41 0 4466 0
vsize: 18028
[startup+260.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4227 0 0 0 25990 10 0 0 25 0 1 0 423083707 19136512 4205 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4672 4205 603 41 0 4631 0
vsize: 18688
[startup+270.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4227 0 0 0 26990 10 0 0 25 0 1 0 423083707 19136512 4205 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4672 4205 603 41 0 4631 0
vsize: 18688
[startup+280.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4227 0 0 0 27991 10 0 0 25 0 1 0 423083707 19136512 4205 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4672 4205 603 41 0 4631 0
vsize: 18688
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4303 0 0 0 28991 10 0 0 25 0 1 0 423083707 19406848 4281 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4281 603 41 0 4697 0
vsize: 18952
[startup+300.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4304 0 0 0 29991 10 0 0 25 0 1 0 423083707 19406848 4282 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4282 603 41 0 4697 0
vsize: 18952
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4305 0 0 0 30991 10 0 0 25 0 1 0 423083707 19406848 4283 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4283 603 41 0 4697 0
vsize: 18952
[startup+320.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4305 0 0 0 31991 10 0 0 25 0 1 0 423083707 19406848 4283 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4283 603 41 0 4697 0
vsize: 18952
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4306 0 0 0 32992 10 0 0 25 0 1 0 423083707 19406848 4284 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4284 603 41 0 4697 0
vsize: 18952
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4306 0 0 0 33992 10 0 0 25 0 1 0 423083707 19406848 4284 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4738 4284 603 41 0 4697 0
vsize: 18952
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4329 0 0 0 34992 10 0 0 25 0 1 0 423083707 19542016 4307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4307 603 41 0 4730 0
vsize: 19084
[startup+360.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4329 0 0 0 35992 10 0 0 25 0 1 0 423083707 19542016 4307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4307 603 41 0 4730 0
vsize: 19084
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4329 0 0 0 36992 10 0 0 25 0 1 0 423083707 19542016 4307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4307 603 41 0 4730 0
vsize: 19084
[startup+380.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4335 0 0 0 37993 10 0 0 25 0 1 0 423083707 19542016 4313 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4313 603 41 0 4730 0
vsize: 19084
[startup+390.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4335 0 0 0 38993 10 0 0 25 0 1 0 423083707 19542016 4313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4313 603 41 0 4730 0
vsize: 19084
[startup+400.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4335 0 0 0 39993 10 0 0 25 0 1 0 423083707 19542016 4313 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4771 4313 603 41 0 4730 0
vsize: 19084
[startup+410.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4336 0 0 0 40993 10 0 0 25 0 1 0 423083707 19542016 4314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4771 4314 603 41 0 4730 0
vsize: 19084
[startup+420.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4350 0 0 0 41992 11 0 0 25 0 1 0 423083707 19677184 4328 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4804 4328 603 41 0 4763 0
vsize: 19216
[startup+430.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4418 0 0 0 42991 11 0 0 25 0 1 0 423083707 19972096 4396 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4876 4396 603 41 0 4835 0
vsize: 19504
[startup+440.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4529 0 0 0 43991 11 0 0 25 0 1 0 423083707 20377600 4507 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4507 603 41 0 4934 0
vsize: 19900
[startup+450.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4529 0 0 0 44992 11 0 0 25 0 1 0 423083707 20377600 4507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4975 4507 603 41 0 4934 0
vsize: 19900
[startup+460.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4604 0 0 0 45992 11 0 0 25 0 1 0 423083707 20774912 4582 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5072 4582 603 41 0 5031 0
vsize: 20288
[startup+470.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4604 0 0 0 46992 11 0 0 25 0 1 0 423083707 20774912 4582 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5072 4582 603 41 0 5031 0
vsize: 20288
[startup+480.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 47992 12 0 0 25 0 1 0 423083707 21180416 4677 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5171 4677 603 41 0 5130 0
vsize: 20684
[startup+490.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 48992 12 0 0 25 0 1 0 423083707 21180416 4677 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5171 4677 603 41 0 5130 0
vsize: 20684
[startup+500.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 49992 12 0 0 25 0 1 0 423083707 21180416 4677 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5171 4677 603 41 0 5130 0
vsize: 20684
[startup+510.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 50992 12 0 0 25 0 1 0 423083707 21139456 4677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5161 4677 603 41 0 5120 0
vsize: 20644
[startup+520.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 51992 12 0 0 25 0 1 0 423083707 21139456 4677 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5161 4677 603 41 0 5120 0
vsize: 20644
[startup+530.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4699 0 0 0 52993 12 0 0 25 0 1 0 423083707 21135360 4677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4677 603 41 0 5119 0
vsize: 20640
[startup+540.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4701 0 0 0 53993 12 0 0 25 0 1 0 423083707 21135360 4679 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4679 603 41 0 5119 0
vsize: 20640
[startup+550.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4708 0 0 0 54993 12 0 0 25 0 1 0 423083707 21135360 4686 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4686 603 41 0 5119 0
vsize: 20640
[startup+560.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4708 0 0 0 55993 12 0 0 25 0 1 0 423083707 21135360 4686 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4686 603 41 0 5119 0
vsize: 20640
[startup+570.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4708 0 0 0 56993 12 0 0 25 0 1 0 423083707 21135360 4686 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4686 603 41 0 5119 0
vsize: 20640
[startup+580.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4708 0 0 0 57994 12 0 0 25 0 1 0 423083707 21135360 4686 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4686 603 41 0 5119 0
vsize: 20640
[startup+590.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4708 0 0 0 58994 12 0 0 25 0 1 0 423083707 21135360 4686 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4686 603 41 0 5119 0
vsize: 20640
[startup+600.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4709 0 0 0 59994 12 0 0 25 0 1 0 423083707 21135360 4687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5160 4687 603 41 0 5119 0
vsize: 20640
[startup+610.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4822 0 0 0 60994 12 0 0 25 0 1 0 423083707 21671936 4800 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5291 4800 603 41 0 5250 0
vsize: 21164
[startup+620.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4846 0 0 0 61994 12 0 0 25 0 1 0 423083707 21807104 4824 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4824 603 41 0 5283 0
vsize: 21296
[startup+630.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4851 0 0 0 62994 12 0 0 25 0 1 0 423083707 21807104 4829 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4829 603 41 0 5283 0
vsize: 21296
[startup+640.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4864 0 0 0 63994 12 0 0 25 0 1 0 423083707 21807104 4842 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4842 603 41 0 5283 0
vsize: 21296
[startup+650.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4864 0 0 0 64995 12 0 0 25 0 1 0 423083707 21807104 4842 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4842 603 41 0 5283 0
vsize: 21296
[startup+660.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4864 0 0 0 65995 12 0 0 25 0 1 0 423083707 21807104 4842 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4842 603 41 0 5283 0
vsize: 21296
[startup+670.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4873 0 0 0 66995 12 0 0 25 0 1 0 423083707 21807104 4851 4294967295 134512640 134672761 3221224544 3221223648 134555314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4851 603 41 0 5283 0
vsize: 21296
[startup+680.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4873 0 0 0 67995 12 0 0 25 0 1 0 423083707 21807104 4851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4851 603 41 0 5283 0
vsize: 21296
[startup+690.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4873 0 0 0 68995 12 0 0 25 0 1 0 423083707 21807104 4851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4851 603 41 0 5283 0
vsize: 21296
[startup+700.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4873 0 0 0 69995 12 0 0 25 0 1 0 423083707 21807104 4851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5324 4851 603 41 0 5283 0
vsize: 21296
[startup+710.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4914 0 0 0 70995 12 0 0 25 0 1 0 423083707 22110208 4892 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4892 603 41 0 5357 0
vsize: 21592
[startup+720.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 4925 0 0 0 71996 12 0 0 25 0 1 0 423083707 22110208 4903 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5398 4903 603 41 0 5357 0
vsize: 21592
[startup+730.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5097 0 0 0 72996 13 0 0 25 0 1 0 423083707 22786048 5075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5563 5075 603 41 0 5522 0
vsize: 22252
[startup+740.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5253 0 0 0 73995 13 0 0 25 0 1 0 423083707 23465984 5231 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5729 5231 603 41 0 5688 0
vsize: 22916
[startup+750.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5382 0 0 0 74996 13 0 0 25 0 1 0 423083707 24006656 5360 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5861 5360 603 41 0 5820 0
vsize: 23444
[startup+760.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5388 0 0 0 75996 13 0 0 25 0 1 0 423083707 24006656 5366 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5861 5366 603 41 0 5820 0
vsize: 23444
[startup+770.032 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5404 0 0 0 76996 13 0 0 25 0 1 0 423083707 24170496 5382 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5382 603 41 0 5860 0
vsize: 23604
[startup+780.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5422 0 0 0 77996 13 0 0 25 0 1 0 423083707 24170496 5400 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5400 603 41 0 5860 0
vsize: 23604
[startup+790.033 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5422 0 0 0 78996 13 0 0 25 0 1 0 423083707 24170496 5400 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5400 603 41 0 5860 0
vsize: 23604
[startup+800.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5438 0 0 0 79996 13 0 0 25 0 1 0 423083707 24334336 5416 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5941 5416 603 41 0 5900 0
vsize: 23764
[startup+810.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5453 0 0 0 80996 13 0 0 25 0 1 0 423083707 24334336 5431 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5941 5431 603 41 0 5900 0
vsize: 23764
[startup+820.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5472 0 0 0 81997 13 0 0 25 0 1 0 423083707 24494080 5450 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5980 5450 603 41 0 5939 0
vsize: 23920
[startup+830.034 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5481 0 0 0 82997 13 0 0 25 0 1 0 423083707 24494080 5459 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5980 5459 603 41 0 5939 0
vsize: 23920
[startup+840.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5495 0 0 0 83997 13 0 0 25 0 1 0 423083707 24494080 5473 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5980 5473 603 41 0 5939 0
vsize: 23920
[startup+850.035 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5550 0 0 0 84997 13 0 0 25 0 1 0 423083707 24821760 5528 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6060 5528 603 41 0 6019 0
vsize: 24240
[startup+860.036 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5550 0 0 0 85998 13 0 0 25 0 1 0 423083707 24821760 5528 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6060 5528 603 41 0 6019 0
vsize: 24240
[startup+870.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5605 0 0 0 86998 13 0 0 25 0 1 0 423083707 25092096 5583 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5583 603 41 0 6085 0
vsize: 24504
[startup+880.037 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5606 0 0 0 87998 13 0 0 25 0 1 0 423083707 25092096 5584 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5584 603 41 0 6085 0
vsize: 24504
[startup+890.038 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5606 0 0 0 88998 13 0 0 25 0 1 0 423083707 25092096 5584 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5584 603 41 0 6085 0
vsize: 24504
[startup+900.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5612 0 0 0 89998 13 0 0 25 0 1 0 423083707 25092096 5590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5590 603 41 0 6085 0
vsize: 24504
[startup+910.038 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5619 0 0 0 90999 13 0 0 25 0 1 0 423083707 25092096 5597 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5597 603 41 0 6085 0
vsize: 24504
[startup+920.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5624 0 0 0 91999 13 0 0 25 0 1 0 423083707 25092096 5602 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5602 603 41 0 6085 0
vsize: 24504
[startup+930.039 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5625 0 0 0 92999 13 0 0 25 0 1 0 423083707 25092096 5603 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6126 5603 603 41 0 6085 0
vsize: 24504
[startup+940.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5655 0 0 0 93999 13 0 0 25 0 1 0 423083707 25251840 5633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6165 5633 603 41 0 6124 0
vsize: 24660
[startup+950.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5655 0 0 0 94999 13 0 0 25 0 1 0 423083707 25251840 5633 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6165 5633 603 41 0 6124 0
vsize: 24660
[startup+960.041 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5657 0 0 0 96000 13 0 0 25 0 1 0 423083707 25251840 5635 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6165 5635 603 41 0 6124 0
vsize: 24660
[startup+970.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5657 0 0 0 97000 13 0 0 25 0 1 0 423083707 25251840 5635 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6165 5635 603 41 0 6124 0
vsize: 24660
[startup+980.042 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5684 0 0 0 98000 13 0 0 25 0 1 0 423083707 25415680 5662 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6205 5662 603 41 0 6164 0
vsize: 24820
[startup+990.043 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5684 0 0 0 99000 13 0 0 25 0 1 0 423083707 25415680 5662 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6205 5662 603 41 0 6164 0
vsize: 24820
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5723 0 0 0 100000 13 0 0 25 0 1 0 423083707 25579520 5701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5701 603 41 0 6204 0
vsize: 24980
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5723 0 0 0 101000 13 0 0 25 0 1 0 423083707 25579520 5701 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5701 603 41 0 6204 0
vsize: 24980
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5723 0 0 0 102001 13 0 0 25 0 1 0 423083707 25579520 5701 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5701 603 41 0 6204 0
vsize: 24980
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5723 0 0 0 103001 13 0 0 25 0 1 0 423083707 25579520 5701 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5701 603 41 0 6204 0
vsize: 24980
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 5723 0 0 0 104001 13 0 0 25 0 1 0 423083707 25579520 5701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6245 5701 603 41 0 6204 0
vsize: 24980
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6189 0 0 0 105001 14 0 0 25 0 1 0 423083707 27467776 6167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6706 6167 603 41 0 6665 0
vsize: 26824
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6477 0 0 0 106000 15 0 0 25 0 1 0 423083707 28684288 6455 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7003 6455 603 41 0 6962 0
vsize: 28012
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6496 0 0 0 107000 15 0 0 25 0 1 0 423083707 28827648 6474 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6474 603 41 0 6997 0
vsize: 28152
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 108000 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 109000 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 110001 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 111001 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 112001 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 113001 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 114001 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 115002 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6504 0 0 0 116002 15 0 0 25 0 1 0 423083707 28827648 6482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6482 603 41 0 6997 0
vsize: 28152
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6505 0 0 0 117002 15 0 0 25 0 1 0 423083707 28827648 6483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6483 603 41 0 6997 0
vsize: 28152
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6505 0 0 0 118002 15 0 0 25 0 1 0 423083707 28827648 6483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6483 603 41 0 6997 0
vsize: 28152
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6505 0 0 0 119002 15 0 0 25 0 1 0 423083707 28827648 6483 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6483 603 41 0 6997 0
vsize: 28152
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 19124
Raw data (stat): 19124 (minisat+) R 19123 10720 10719 0 -1 0 6505 0 0 0 120003 15 0 0 25 0 1 0 423083707 28827648 6483 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7038 6483 603 41 0 6997 0
vsize: 28152
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 19124
Raw data (stat): 19124 (minisat+) Z 19123 10720 10719 0 -1 12 6507 0 0 0 120003 16 0 0 25 0 1 0 423083707 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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