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/primes-dimacs-cnf/normalized-ii8b1.opb
MD5SUM	812314147c77e28d5e428080c7a2412d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	672
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	672
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	672
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03684
Number of variables	672
Total number of constraints	2404
Number of constraints which are clauses	2404
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	2
Maximum length of a constraint	8
Trace number 5892

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 02:12:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4303 boxname=wulflinc15 idbench=167 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb
IDLAUNCH: 4303
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        899052 kB
Buffers:         36520 kB
Cached:          77480 kB
SwapCached:       2144 kB
Active:          64060 kB
Inactive:        54976 kB
HighTotal:      131008 kB
HighFree:        49616 kB
LowTotal:       903652 kB
LowFree:        849436 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11084 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:32:30 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 4303 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2404 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 |    2404     5328 |     801       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   39371    91691 |   13123       2       14     7.0 |  0.000 % |
c |       102 |   39094    91112 |   14435      93     3903    42.0 |  0.670 % |
c |       252 |   39002    90914 |   15878     240     6701    27.9 |  0.882 % |
c |       477 |   38987    90884 |   17466     464    15942    34.4 |  0.910 % |
c |       815 |   37805    88284 |   19213     776    24356    31.4 |  3.726 % |
c |      1322 |   37260    87073 |   21134    1269    45788    36.1 |  5.055 % |
c |      2082 |   37129    86792 |   23248    2027    71701    35.4 |  5.354 % |
c |      3223 |   37060    86641 |   25573    3166   105927    33.5 |  5.514 % |
c |      4933 |   36659    85752 |   28130    4825   171835    35.6 |  6.479 % |
c ==============================================================================
c [1mFound solution: 213[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5130 |   36761    86021 |   12253    5022   174707    34.8 |  6.479 % |
c |      5230 |   36692    85868 |   13478    5120   176718    34.5 |  6.749 % |
c |      5381 |   36692    85868 |   14826    5271   182366    34.6 |  6.749 % |
c |      5606 |   36692    85868 |   16308    5496   187885    34.2 |  6.749 % |
c |      5944 |   36590    85644 |   17939    5831   206859    35.5 |  6.987 % |
c |      6450 |   36554    85568 |   19733    6324   229508    36.3 |  7.063 % |
c |      7209 |   36479    85399 |   21706    7081   256581    36.2 |  7.249 % |
c |      8348 |   36479    85399 |   23877    8220   321429    39.1 |  7.249 % |
c ==============================================================================
c [1mFound solution: 212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8492 |   36455    85340 |   12151    8328   322244    38.7 |  7.249 % |
c |      8592 |   36412    85243 |   13366    8427   325487    38.6 |  7.439 % |
c |      8742 |   36412    85243 |   14702    8577   331063    38.6 |  7.440 % |
c ==============================================================================
c [1mFound solution: 191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8825 |   36570    85630 |   12190    8660   333479    38.5 |  7.440 % |
c |      8925 |   36570    85630 |   13409    8760   336090    38.4 |  7.604 % |
c |      9075 |   36570    85630 |   14749    8910   343099    38.5 |  7.604 % |
c |      9301 |   36570    85630 |   16224    9136   351679    38.5 |  7.605 % |
c |      9638 |   36570    85630 |   17847    9473   362266    38.2 |  7.604 % |
c |     10144 |   36472    85414 |   19632    9977   379563    38.0 |  7.834 % |
c |     10905 |   36472    85414 |   21595   10738   407634    38.0 |  7.834 % |
c |     12044 |   36472    85414 |   23754   11877   468101    39.4 |  7.834 % |
c |     13754 |   36472    85414 |   26130   13587   522596    38.5 |  7.834 % |
c |     16317 |   36470    85410 |   28743   16149   629422    39.0 |  7.838 % |
c |     20161 |   36426    85316 |   31617   19992   838045    41.9 |  7.936 % |
c |     25927 |   36382    85218 |   34779   25757  1118768    43.4 |  8.043 % |
c |     34576 |   36305    85037 |   38257   34348  1535481    44.7 |  8.244 % |
c |     47550 |   36181    84771 |   42083   21274   996051    46.8 |  8.517 % |
c |     67011 |   36135    84671 |   46291   40732  1888951    46.4 |  8.624 % |
c |     96203 |   36135    84671 |   50920   35083  1330080    37.9 |  8.624 % |
c |    139993 |   36085    84561 |   56012   42013  1861233    44.3 |  8.742 % |
c |    205677 |   36085    84561 |   61613   20830   839310    40.3 |  8.742 % |
c |    304203 |   36085    84561 |   67775   23016   997862    43.4 |  8.742 % |
#### 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.89 0.95 0.92 2/54 3755
Raw data (stat): 3755 (runsolver) R 3754 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422672202 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.91 0.95 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2398 0 0 0 992 6 0 0 25 0 1 0 422672202 11636736 2321 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2841 2321 603 41 0 2800 0
vsize: 11364
[startup+20.0015 s]
Raw data (loadavg): 0.92 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2682 0 0 0 1990 7 0 0 25 0 1 0 422672202 12972032 2605 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3167 2605 603 41 0 3126 0
vsize: 12668
[startup+30.0016 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 2960 0 0 0 2988 8 0 0 25 0 1 0 422672202 14045184 2883 4294967295 134512640 134672761 3221224560 3221223632 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2883 603 41 0 3388 0
vsize: 13716
[startup+40.0017 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3202 0 0 0 3987 9 0 0 25 0 1 0 422672202 15085568 3125 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3125 603 41 0 3642 0
vsize: 14732
[startup+50.0026 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3412 0 0 0 4986 10 0 0 25 0 1 0 422672202 16023552 3335 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3912 3335 603 41 0 3871 0
vsize: 15648
[startup+60.0021 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3618 0 0 0 5986 11 0 0 25 0 1 0 422672202 16818176 3541 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4106 3541 603 41 0 4065 0
vsize: 16424
[startup+70.0032 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3785 0 0 0 6986 11 0 0 25 0 1 0 422672202 17473536 3708 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4266 3708 603 41 0 4225 0
vsize: 17064
[startup+80.0041 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 3956 0 0 0 7985 12 0 0 25 0 1 0 422672202 18137088 3879 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4428 3879 603 41 0 4387 0
vsize: 17712
[startup+90.0036 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4157 0 0 0 8985 12 0 0 25 0 1 0 422672202 19070976 4080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4656 4080 603 41 0 4615 0
vsize: 18624
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4371 0 0 0 9984 13 0 0 25 0 1 0 422672202 20000768 4294 4294967295 134512640 134672761 3221224560 3221223744 134559274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4883 4294 603 41 0 4842 0
vsize: 19532
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4629 0 0 0 10983 14 0 0 25 0 1 0 422672202 21069824 4552 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4552 603 41 0 5103 0
vsize: 20576
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4634 0 0 0 11984 14 0 0 25 0 1 0 422672202 21069824 4557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4557 603 41 0 5103 0
vsize: 20576
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4636 0 0 0 12984 14 0 0 25 0 1 0 422672202 21069824 4559 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4559 603 41 0 5103 0
vsize: 20576
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4640 0 0 0 13984 14 0 0 25 0 1 0 422672202 21069824 4563 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4563 603 41 0 5103 0
vsize: 20576
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4646 0 0 0 14984 14 0 0 25 0 1 0 422672202 21069824 4569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5144 4569 603 41 0 5103 0
vsize: 20576
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4659 0 0 0 15984 14 0 0 25 0 1 0 422672202 21209088 4582 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5178 4582 603 41 0 5137 0
vsize: 20712
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4661 0 0 0 16984 14 0 0 25 0 1 0 422672202 21209088 4584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5178 4584 603 41 0 5137 0
vsize: 20712
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4661 0 0 0 17984 14 0 0 25 0 1 0 422672202 21209088 4584 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5178 4584 603 41 0 5137 0
vsize: 20712
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4803 0 0 0 18984 15 0 0 25 0 1 0 422672202 21741568 4726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5308 4726 603 41 0 5267 0
vsize: 21232
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 4938 0 0 0 19983 16 0 0 25 0 1 0 422672202 22274048 4861 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5438 4861 603 41 0 5397 0
vsize: 21752
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5073 0 0 0 20983 17 0 0 25 0 1 0 422672202 22941696 4996 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5601 4996 603 41 0 5560 0
vsize: 22404
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5218 0 0 0 21982 17 0 0 25 0 1 0 422672202 23470080 5141 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5730 5141 603 41 0 5689 0
vsize: 22920
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5241 0 0 0 22983 17 0 0 25 0 1 0 422672202 23605248 5164 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5763 5164 603 41 0 5722 0
vsize: 23052
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5243 0 0 0 23983 17 0 0 25 0 1 0 422672202 23605248 5166 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5763 5166 603 41 0 5722 0
vsize: 23052
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5250 0 0 0 24983 17 0 0 25 0 1 0 422672202 23605248 5173 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5763 5173 603 41 0 5722 0
vsize: 23052
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5256 0 0 0 25983 17 0 0 25 0 1 0 422672202 23605248 5179 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5763 5179 603 41 0 5722 0
vsize: 23052
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5269 0 0 0 26983 17 0 0 25 0 1 0 422672202 23769088 5192 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5803 5192 603 41 0 5762 0
vsize: 23212
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5270 0 0 0 27983 17 0 0 25 0 1 0 422672202 23769088 5193 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5803 5193 603 41 0 5762 0
vsize: 23212
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5282 0 0 0 28983 18 0 0 25 0 1 0 422672202 23769088 5205 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5803 5205 603 41 0 5762 0
vsize: 23212
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5297 0 0 0 29983 18 0 0 25 0 1 0 422672202 23932928 5220 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5843 5220 603 41 0 5802 0
vsize: 23372
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5309 0 0 0 30983 18 0 0 25 0 1 0 422672202 23932928 5232 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5843 5232 603 41 0 5802 0
vsize: 23372
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5311 0 0 0 31983 18 0 0 25 0 1 0 422672202 23932928 5234 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5843 5234 603 41 0 5802 0
vsize: 23372
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5313 0 0 0 32983 18 0 0 25 0 1 0 422672202 23932928 5236 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5843 5236 603 41 0 5802 0
vsize: 23372
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5333 0 0 0 33983 18 0 0 25 0 1 0 422672202 24129536 5256 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5891 5256 603 41 0 5850 0
vsize: 23564
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5338 0 0 0 34984 18 0 0 25 0 1 0 422672202 24129536 5261 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5891 5261 603 41 0 5850 0
vsize: 23564
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 35984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5317 603 41 0 5882 0
vsize: 23692
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 36984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5317 603 41 0 5882 0
vsize: 23692
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5394 0 0 0 37984 18 0 0 25 0 1 0 422672202 24260608 5317 4294967295 134512640 134672761 3221224560 3221223664 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5317 603 41 0 5882 0
vsize: 23692
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5398 0 0 0 38984 18 0 0 25 0 1 0 422672202 24260608 5321 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5321 603 41 0 5882 0
vsize: 23692
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 39985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5326 603 41 0 5919 0
vsize: 23840
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 40985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5326 603 41 0 5919 0
vsize: 23840
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5403 0 0 0 41985 18 0 0 25 0 1 0 422672202 24412160 5326 4294967295 134512640 134672761 3221224560 3221223760 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5326 603 41 0 5919 0
vsize: 23840
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5416 0 0 0 42985 18 0 0 25 0 1 0 422672202 24412160 5339 4294967295 134512640 134672761 3221224560 3221223704 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5339 603 41 0 5919 0
vsize: 23840
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5425 0 0 0 43985 18 0 0 25 0 1 0 422672202 24412160 5348 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5348 603 41 0 5919 0
vsize: 23840
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5426 0 0 0 44985 18 0 0 25 0 1 0 422672202 24412160 5349 4294967295 134512640 134672761 3221224560 3221223656 1075347274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5960 5349 603 41 0 5919 0
vsize: 23840
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5441 0 0 0 45985 18 0 0 25 0 1 0 422672202 24576000 5364 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6000 5364 603 41 0 5959 0
vsize: 24000
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5449 0 0 0 46985 18 0 0 25 0 1 0 422672202 24576000 5372 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6000 5372 603 41 0 5959 0
vsize: 24000
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5587 0 0 0 47984 19 0 0 25 0 1 0 422672202 25108480 5510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6130 5510 603 41 0 6089 0
vsize: 24520
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5726 0 0 0 48984 20 0 0 25 0 1 0 422672202 25636864 5649 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6259 5649 603 41 0 6218 0
vsize: 25036
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5831 0 0 0 49984 20 0 0 25 0 1 0 422672202 26161152 5754 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6387 5754 603 41 0 6346 0
vsize: 25548
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5945 0 0 0 50984 20 0 0 25 0 1 0 422672202 26558464 5868 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5868 603 41 0 6443 0
vsize: 25936
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5945 0 0 0 51984 20 0 0 25 0 1 0 422672202 26558464 5868 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5868 603 41 0 6443 0
vsize: 25936
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 52985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5871 603 41 0 6443 0
vsize: 25936
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 53985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5871 603 41 0 6443 0
vsize: 25936
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 54985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5871 603 41 0 6443 0
vsize: 25936
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5948 0 0 0 55985 20 0 0 25 0 1 0 422672202 26558464 5871 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6484 5871 603 41 0 6443 0
vsize: 25936
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5968 0 0 0 56985 20 0 0 25 0 1 0 422672202 26730496 5891 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6526 5891 603 41 0 6485 0
vsize: 26104
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5987 0 0 0 57985 20 0 0 25 0 1 0 422672202 26730496 5910 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6526 5910 603 41 0 6485 0
vsize: 26104
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5987 0 0 0 58985 20 0 0 25 0 1 0 422672202 26730496 5910 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6526 5910 603 41 0 6485 0
vsize: 26104
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5993 0 0 0 59986 20 0 0 25 0 1 0 422672202 26927104 5916 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5916 603 41 0 6533 0
vsize: 26296
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5995 0 0 0 60986 20 0 0 25 0 1 0 422672202 26927104 5918 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5918 603 41 0 6533 0
vsize: 26296
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5996 0 0 0 61986 20 0 0 25 0 1 0 422672202 26927104 5919 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5919 603 41 0 6533 0
vsize: 26296
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5996 0 0 0 62986 20 0 0 25 0 1 0 422672202 26927104 5919 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5919 603 41 0 6533 0
vsize: 26296
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 5997 0 0 0 63986 20 0 0 25 0 1 0 422672202 26927104 5920 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5920 603 41 0 6533 0
vsize: 26296
[startup+650.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6000 0 0 0 64986 20 0 0 25 0 1 0 422672202 26927104 5923 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5923 603 41 0 6533 0
vsize: 26296
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6013 0 0 0 65986 20 0 0 25 0 1 0 422672202 26927104 5936 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6574 5936 603 41 0 6533 0
vsize: 26296
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 66986 20 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6050 603 41 0 6630 0
vsize: 26684
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 67987 20 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6050 603 41 0 6630 0
vsize: 26684
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6127 0 0 0 68986 21 0 0 25 0 1 0 422672202 27324416 6050 4294967295 134512640 134672761 3221224560 3221223664 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6050 603 41 0 6630 0
vsize: 26684
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 69986 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 70987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223744 134558831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 71987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 72987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 73987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 74987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 75987 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223744 134558376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 76988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 77988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 78988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 79988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6128 0 0 0 80988 21 0 0 25 0 1 0 422672202 27324416 6051 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6051 603 41 0 6630 0
vsize: 26684
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6150 0 0 0 81989 21 0 0 25 0 1 0 422672202 27459584 6073 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6704 6073 603 41 0 6663 0
vsize: 26816
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6313 0 0 0 82988 21 0 0 25 0 1 0 422672202 28114944 6236 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6864 6236 603 41 0 6823 0
vsize: 27456
[startup+840.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6471 0 0 0 83988 21 0 0 25 0 1 0 422672202 28774400 6394 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7025 6394 603 41 0 6984 0
vsize: 28100
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 84988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6496 603 41 0 7147 0
vsize: 28752
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 85988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6496 603 41 0 7147 0
vsize: 28752
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6573 0 0 0 86988 22 0 0 25 0 1 0 422672202 29442048 6496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6496 603 41 0 7147 0
vsize: 28752
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6576 0 0 0 87988 22 0 0 25 0 1 0 422672202 29442048 6499 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6499 603 41 0 7147 0
vsize: 28752
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6579 0 0 0 88989 22 0 0 25 0 1 0 422672202 29442048 6502 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6502 603 41 0 7147 0
vsize: 28752
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6579 0 0 0 89989 22 0 0 25 0 1 0 422672202 29442048 6502 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7188 6502 603 41 0 7147 0
vsize: 28752
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6593 0 0 0 90989 22 0 0 25 0 1 0 422672202 29585408 6516 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7223 6516 603 41 0 7182 0
vsize: 28892
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6606 0 0 0 91989 22 0 0 25 0 1 0 422672202 29585408 6529 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7223 6529 603 41 0 7182 0
vsize: 28892
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6618 0 0 0 92989 22 0 0 25 0 1 0 422672202 29585408 6541 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7223 6541 603 41 0 7182 0
vsize: 28892
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6621 0 0 0 93990 22 0 0 25 0 1 0 422672202 29745152 6544 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7262 6544 603 41 0 7221 0
vsize: 29048
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6627 0 0 0 94990 22 0 0 25 0 1 0 422672202 29745152 6550 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7262 6550 603 41 0 7221 0
vsize: 29048
[startup+960.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6638 0 0 0 95990 22 0 0 25 0 1 0 422672202 29745152 6561 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7262 6561 603 41 0 7221 0
vsize: 29048
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6658 0 0 0 96990 22 0 0 25 0 1 0 422672202 29908992 6581 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7302 6581 603 41 0 7261 0
vsize: 29208
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6663 0 0 0 97990 22 0 0 25 0 1 0 422672202 29908992 6586 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7302 6586 603 41 0 7261 0
vsize: 29208
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6682 0 0 0 98990 22 0 0 25 0 1 0 422672202 29908992 6605 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7302 6605 603 41 0 7261 0
vsize: 29208
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6687 0 0 0 99991 22 0 0 25 0 1 0 422672202 29908992 6610 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7302 6610 603 41 0 7261 0
vsize: 29208
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6689 0 0 0 100991 22 0 0 25 0 1 0 422672202 29908992 6612 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7302 6612 603 41 0 7261 0
vsize: 29208
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6832 0 0 0 101990 22 0 0 25 0 1 0 422672202 30576640 6755 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7465 6755 603 41 0 7424 0
vsize: 29860
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 102990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 103990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 104990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 105989 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 106990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 107990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 108990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 109990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6912 0 0 0 110990 23 0 0 25 0 1 0 422672202 30838784 6835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6835 603 41 0 7488 0
vsize: 30116
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6918 0 0 0 111990 23 0 0 25 0 1 0 422672202 30838784 6841 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7529 6841 603 41 0 7488 0
vsize: 30116
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6922 0 0 0 112991 23 0 0 25 0 1 0 422672202 30978048 6845 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7563 6845 603 41 0 7522 0
vsize: 30252
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6929 0 0 0 113991 23 0 0 25 0 1 0 422672202 30978048 6852 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7563 6852 603 41 0 7522 0
vsize: 30252
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6929 0 0 0 114991 23 0 0 25 0 1 0 422672202 30978048 6852 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7563 6852 603 41 0 7522 0
vsize: 30252
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6934 0 0 0 115991 23 0 0 25 0 1 0 422672202 30978048 6857 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7563 6857 603 41 0 7522 0
vsize: 30252
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6963 0 0 0 116991 23 0 0 25 0 1 0 422672202 31174656 6886 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7611 6886 603 41 0 7570 0
vsize: 30444
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6966 0 0 0 117991 23 0 0 25 0 1 0 422672202 31174656 6889 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7611 6889 603 41 0 7570 0
vsize: 30444
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6966 0 0 0 118991 23 0 0 25 0 1 0 422672202 31174656 6889 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7611 6889 603 41 0 7570 0
vsize: 30444
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 3755
Raw data (stat): 3755 (minisat+) R 3754 29151 29150 0 -1 0 6992 0 0 0 119992 23 0 0 25 0 1 0 422672202 31354880 6915 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7655 6915 603 41 0 7614 0
vsize: 30620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 3755
Raw data (stat): 3755 (minisat+) Z 3754 29151 29150 0 -1 12 6995 0 0 0 119992 25 0 0 25 0 1 0 422672202 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.05
CPU time (s): 1200.17
CPU user time (s): 1199.92
CPU system time (s): 0.250961
CPU usage (%): 100.01
Max. virtual memory (Kb): 30620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####