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 4919

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 20:50:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1499 boxname=wulflinc21 idbench=167 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc21/normalized-ii8b1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-ii8b1.opb
IDLAUNCH: 1499
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        910980 kB
Buffers:         26152 kB
Cached:          77820 kB
SwapCached:          0 kB
Active:          33728 kB
Inactive:        73176 kB
HighTotal:      131008 kB
HighFree:        49504 kB
LowTotal:       903652 kB
LowFree:        861476 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11120 kB
Committed_AS:    63784 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:10:29 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 1499 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.92 0.95 0.90 2/55 1462
Raw data (stat): 1462 (runsolver) R 1461 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356227406 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 2423 0 0 0 993 5 0 0 25 0 1 0 356227406 11685888 2334 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2853 2334 603 41 0 2812 0
vsize: 11412
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 2726 0 0 0 1992 7 0 0 25 0 1 0 356227406 13455360 2637 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3285 2637 603 41 0 3244 0
vsize: 13140
[startup+30.002 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 3005 0 0 0 2991 8 0 0 25 0 1 0 356227406 14528512 2916 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3547 2916 603 41 0 3506 0
vsize: 14188
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 3250 0 0 0 3990 9 0 0 25 0 1 0 356227406 15704064 3161 4294967295 134512640 134672761 3221224640 3221223744 134560347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3834 3161 603 41 0 3793 0
vsize: 15336
[startup+50.0039 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 3463 0 0 0 4989 10 0 0 25 0 1 0 356227406 16506880 3374 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4030 3374 603 41 0 3989 0
vsize: 16120
[startup+60.0032 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 3667 0 0 0 5988 11 0 0 25 0 1 0 356227406 17297408 3578 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4223 3578 603 41 0 4182 0
vsize: 16892
[startup+70.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 3837 0 0 0 6987 12 0 0 25 0 1 0 356227406 17965056 3748 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4386 3748 603 41 0 4345 0
vsize: 17544
[startup+80.0047 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4016 0 0 0 7987 13 0 0 25 0 1 0 356227406 18763776 3927 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4581 3927 603 41 0 4540 0
vsize: 18324
[startup+90.0054 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4221 0 0 0 8986 13 0 0 25 0 1 0 356227406 19693568 4132 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4808 4132 603 41 0 4767 0
vsize: 19232
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4443 0 0 0 9985 15 0 0 25 0 1 0 356227406 20627456 4354 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5036 4354 603 41 0 4995 0
vsize: 20144
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4674 0 0 0 10984 16 0 0 25 0 1 0 356227406 21565440 4585 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5265 4585 603 41 0 5224 0
vsize: 21060
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4678 0 0 0 11985 16 0 0 25 0 1 0 356227406 21565440 4589 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5265 4589 603 41 0 5224 0
vsize: 21060
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4679 0 0 0 12984 16 0 0 25 0 1 0 356227406 21565440 4590 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5265 4590 603 41 0 5224 0
vsize: 21060
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4684 0 0 0 13984 16 0 0 25 0 1 0 356227406 21565440 4595 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5265 4595 603 41 0 5224 0
vsize: 21060
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4689 0 0 0 14984 16 0 0 25 0 1 0 356227406 21565440 4600 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5265 4600 603 41 0 5224 0
vsize: 21060
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4701 0 0 0 15984 16 0 0 25 0 1 0 356227406 21704704 4612 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5299 4612 603 41 0 5258 0
vsize: 21196
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4702 0 0 0 16984 16 0 0 25 0 1 0 356227406 21704704 4613 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5299 4613 603 41 0 5258 0
vsize: 21196
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4733 0 0 0 17984 17 0 0 25 0 1 0 356227406 21835776 4644 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5331 4644 603 41 0 5290 0
vsize: 21324
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 4877 0 0 0 18984 17 0 0 25 0 1 0 356227406 22364160 4788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5460 4788 603 41 0 5419 0
vsize: 21840
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5008 0 0 0 19984 18 0 0 25 0 1 0 356227406 22900736 4919 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5591 4919 603 41 0 5550 0
vsize: 22364
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5150 0 0 0 20983 18 0 0 25 0 1 0 356227406 23560192 5061 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5752 5061 603 41 0 5711 0
vsize: 23008
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5272 0 0 0 21982 19 0 0 25 0 1 0 356227406 23957504 5183 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5849 5183 603 41 0 5808 0
vsize: 23396
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5280 0 0 0 22982 19 0 0 25 0 1 0 356227406 24100864 5191 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5884 5191 603 41 0 5843 0
vsize: 23536
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5281 0 0 0 23982 19 0 0 25 0 1 0 356227406 24100864 5192 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5884 5192 603 41 0 5843 0
vsize: 23536
[startup+250.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5290 0 0 0 24982 20 0 0 25 0 1 0 356227406 24100864 5201 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5884 5201 603 41 0 5843 0
vsize: 23536
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5295 0 0 0 25982 20 0 0 25 0 1 0 356227406 24100864 5206 4294967295 134512640 134672761 3221224640 3221223824 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5884 5206 603 41 0 5843 0
vsize: 23536
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5308 0 0 0 26982 20 0 0 25 0 1 0 356227406 24264704 5219 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5924 5219 603 41 0 5883 0
vsize: 23696
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5312 0 0 0 27982 20 0 0 25 0 1 0 356227406 24264704 5223 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5924 5223 603 41 0 5883 0
vsize: 23696
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5334 0 0 0 28982 21 0 0 25 0 1 0 356227406 24428544 5245 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5964 5245 603 41 0 5923 0
vsize: 23856
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5337 0 0 0 29982 21 0 0 25 0 1 0 356227406 24428544 5248 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5964 5248 603 41 0 5923 0
vsize: 23856
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5348 0 0 0 30982 21 0 0 25 0 1 0 356227406 24428544 5259 4294967295 134512640 134672761 3221224640 3221223824 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5964 5259 603 41 0 5923 0
vsize: 23856
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5350 0 0 0 31982 21 0 0 25 0 1 0 356227406 24428544 5261 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5964 5261 603 41 0 5923 0
vsize: 23856
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5371 0 0 0 32982 21 0 0 25 0 1 0 356227406 24621056 5282 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6011 5282 603 41 0 5970 0
vsize: 24044
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5375 0 0 0 33982 21 0 0 25 0 1 0 356227406 24621056 5286 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6011 5286 603 41 0 5970 0
vsize: 24044
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5435 0 0 0 34982 22 0 0 25 0 1 0 356227406 24752128 5346 4294967295 134512640 134672761 3221224640 3221223744 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5346 603 41 0 6002 0
vsize: 24172
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5435 0 0 0 35982 22 0 0 25 0 1 0 356227406 24752128 5346 4294967295 134512640 134672761 3221224640 3221223808 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5346 603 41 0 6002 0
vsize: 24172
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5435 0 0 0 36982 22 0 0 25 0 1 0 356227406 24752128 5346 4294967295 134512640 134672761 3221224640 3221223824 134559159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5346 603 41 0 6002 0
vsize: 24172
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5435 0 0 0 37982 22 0 0 25 0 1 0 356227406 24752128 5346 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5346 603 41 0 6002 0
vsize: 24172
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5435 0 0 0 38982 22 0 0 25 0 1 0 356227406 24752128 5346 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6043 5346 603 41 0 6002 0
vsize: 24172
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5440 0 0 0 39982 22 0 0 25 0 1 0 356227406 24891392 5351 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5351 603 41 0 6036 0
vsize: 24308
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5440 0 0 0 40982 22 0 0 25 0 1 0 356227406 24891392 5351 4294967295 134512640 134672761 3221224640 3221223764 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5351 603 41 0 6036 0
vsize: 24308
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5446 0 0 0 41982 22 0 0 25 0 1 0 356227406 24891392 5357 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5357 603 41 0 6036 0
vsize: 24308
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5453 0 0 0 42982 22 0 0 25 0 1 0 356227406 24891392 5364 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5364 603 41 0 6036 0
vsize: 24308
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5462 0 0 0 43982 22 0 0 25 0 1 0 356227406 24891392 5373 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5373 603 41 0 6036 0
vsize: 24308
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5463 0 0 0 44982 23 0 0 25 0 1 0 356227406 24891392 5374 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6077 5374 603 41 0 6036 0
vsize: 24308
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5482 0 0 0 45982 23 0 0 25 0 1 0 356227406 25055232 5393 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6117 5393 603 41 0 6076 0
vsize: 24468
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5559 0 0 0 46982 23 0 0 25 0 1 0 356227406 25321472 5470 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6182 5470 603 41 0 6141 0
vsize: 24728
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5716 0 0 0 47981 24 0 0 25 0 1 0 356227406 25985024 5627 4294967295 134512640 134672761 3221224640 3221223744 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6344 5627 603 41 0 6303 0
vsize: 25376
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5829 0 0 0 48981 25 0 0 25 0 1 0 356227406 26382336 5740 4294967295 134512640 134672761 3221224640 3221223840 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6441 5740 603 41 0 6400 0
vsize: 25764
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5947 0 0 0 49981 25 0 0 25 0 1 0 356227406 26910720 5858 4294967295 134512640 134672761 3221224640 3221223824 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6570 5858 603 41 0 6529 0
vsize: 26280
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5984 0 0 0 50980 25 0 0 25 0 1 0 356227406 27041792 5895 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5895 603 41 0 6561 0
vsize: 26408
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5987 0 0 0 51980 26 0 0 25 0 1 0 356227406 27041792 5898 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5898 603 41 0 6561 0
vsize: 26408
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5993 0 0 0 52980 26 0 0 25 0 1 0 356227406 27041792 5904 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5904 603 41 0 6561 0
vsize: 26408
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5993 0 0 0 53980 26 0 0 25 0 1 0 356227406 27041792 5904 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5904 603 41 0 6561 0
vsize: 26408
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5993 0 0 0 54980 26 0 0 25 0 1 0 356227406 27041792 5904 4294967295 134512640 134672761 3221224640 3221223804 134564518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6602 5904 603 41 0 6561 0
vsize: 26408
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 5998 0 0 0 55980 26 0 0 25 0 1 0 356227406 27181056 5909 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 5909 603 41 0 6595 0
vsize: 26544
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1462
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6032 0 0 0 56980 26 0 0 25 0 1 0 356227406 27377664 5943 4294967295 134512640 134672761 3221224640 3221223744 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6684 5943 603 41 0 6643 0
vsize: 26736
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6032 0 0 0 57977 29 0 0 25 0 1 0 356227406 27377664 5943 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5943 603 41 0 6643 0
vsize: 26736
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6037 0 0 0 58978 29 0 0 25 0 1 0 356227406 27377664 5948 4294967295 134512640 134672761 3221224640 3221223764 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5948 603 41 0 6643 0
vsize: 26736
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6039 0 0 0 59978 29 0 0 25 0 1 0 356227406 27377664 5950 4294967295 134512640 134672761 3221224640 3221223824 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5950 603 41 0 6643 0
vsize: 26736
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6040 0 0 0 60978 29 0 0 25 0 1 0 356227406 27377664 5951 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5951 603 41 0 6643 0
vsize: 26736
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6040 0 0 0 61978 29 0 0 25 0 1 0 356227406 27377664 5951 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5951 603 41 0 6643 0
vsize: 26736
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1516
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6041 0 0 0 62978 29 0 0 25 0 1 0 356227406 27377664 5952 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5952 603 41 0 6643 0
vsize: 26736
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6044 0 0 0 63978 29 0 0 25 0 1 0 356227406 27377664 5955 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5955 603 41 0 6643 0
vsize: 26736
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6045 0 0 0 64979 29 0 0 25 0 1 0 356227406 27377664 5956 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6684 5956 603 41 0 6643 0
vsize: 26736
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6144 0 0 0 65978 29 0 0 25 0 1 0 356227406 27774976 6055 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6781 6055 603 41 0 6740 0
vsize: 27124
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6166 0 0 0 66978 29 0 0 25 0 1 0 356227406 27906048 6077 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6813 6077 603 41 0 6772 0
vsize: 27252
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6166 0 0 0 67978 30 0 0 25 0 1 0 356227406 27906048 6077 4294967295 134512640 134672761 3221224640 3221223824 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6077 603 41 0 6772 0
vsize: 27252
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6166 0 0 0 68978 30 0 0 25 0 1 0 356227406 27906048 6077 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6077 603 41 0 6772 0
vsize: 27252
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 69978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 70978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 71978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 72978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 73978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 74978 30 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223744 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+760.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 75978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 76978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 77978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 78978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 79978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6167 0 0 0 80978 31 0 0 25 0 1 0 356227406 27906048 6078 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6813 6078 603 41 0 6772 0
vsize: 27252
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6331 0 0 0 81977 33 0 0 25 0 1 0 356227406 28565504 6242 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6974 6242 603 41 0 6933 0
vsize: 27896
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6488 0 0 0 82977 33 0 0 25 0 1 0 356227406 29241344 6399 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7139 6399 603 41 0 7098 0
vsize: 28556
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6612 0 0 0 83976 33 0 0 25 0 1 0 356227406 29896704 6523 4294967295 134512640 134672761 3221224640 3221223744 134554677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7299 6523 603 41 0 7258 0
vsize: 29196
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6612 0 0 0 84976 34 0 0 25 0 1 0 356227406 29896704 6523 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7299 6523 603 41 0 7258 0
vsize: 29196
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6612 0 0 0 85976 34 0 0 25 0 1 0 356227406 29896704 6523 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7299 6523 603 41 0 7258 0
vsize: 29196
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6613 0 0 0 86977 34 0 0 25 0 1 0 356227406 29896704 6524 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7299 6524 603 41 0 7258 0
vsize: 29196
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6615 0 0 0 87976 34 0 0 25 0 1 0 356227406 30031872 6526 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6526 603 41 0 7291 0
vsize: 29328
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6615 0 0 0 88976 34 0 0 25 0 1 0 356227406 30031872 6526 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6526 603 41 0 7291 0
vsize: 29328
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1520
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6630 0 0 0 89976 35 0 0 25 0 1 0 356227406 30031872 6541 4294967295 134512640 134672761 3221224640 3221223796 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6541 603 41 0 7291 0
vsize: 29328
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6644 0 0 0 90975 35 0 0 25 0 1 0 356227406 30031872 6555 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7332 6555 603 41 0 7291 0
vsize: 29328
[startup+920.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6656 0 0 0 91975 36 0 0 25 0 1 0 356227406 30195712 6567 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6567 603 41 0 7331 0
vsize: 29488
[startup+930.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6658 0 0 0 92975 36 0 0 25 0 1 0 356227406 30195712 6569 4294967295 134512640 134672761 3221224640 3221223776 134565089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6569 603 41 0 7331 0
vsize: 29488
[startup+940.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6665 0 0 0 93975 36 0 0 25 0 1 0 356227406 30195712 6576 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6576 603 41 0 7331 0
vsize: 29488
[startup+950.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6681 0 0 0 94975 36 0 0 25 0 1 0 356227406 30195712 6592 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7372 6592 603 41 0 7331 0
vsize: 29488
[startup+960.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6696 0 0 0 95975 37 0 0 25 0 1 0 356227406 30392320 6607 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6607 603 41 0 7379 0
vsize: 29680
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6700 0 0 0 96975 37 0 0 25 0 1 0 356227406 30392320 6611 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6611 603 41 0 7379 0
vsize: 29680
[startup+980.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6719 0 0 0 97975 37 0 0 25 0 1 0 356227406 30392320 6630 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6630 603 41 0 7379 0
vsize: 29680
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6724 0 0 0 98975 37 0 0 25 0 1 0 356227406 30392320 6635 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6635 603 41 0 7379 0
vsize: 29680
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6736 0 0 0 99975 37 0 0 25 0 1 0 356227406 30523392 6647 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7452 6647 603 41 0 7411 0
vsize: 29808
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6884 0 0 0 100975 38 0 0 25 0 1 0 356227406 31059968 6795 4294967295 134512640 134672761 3221224640 3221223744 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7583 6795 603 41 0 7542 0
vsize: 30332
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 101974 38 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 102974 39 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223808 134559675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 103973 39 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 104973 39 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 105973 39 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6951 0 0 0 106973 39 0 0 25 0 1 0 356227406 31326208 6862 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6862 603 41 0 7607 0
vsize: 30592
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6954 0 0 0 107973 39 0 0 25 0 1 0 356227406 31326208 6865 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7648 6865 603 41 0 7607 0
vsize: 30592
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6958 0 0 0 108973 39 0 0 25 0 1 0 356227406 31461376 6869 4294967295 134512640 134672761 3221224640 3221223700 1075346542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6869 603 41 0 7640 0
vsize: 30724
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6961 0 0 0 109974 39 0 0 25 0 1 0 356227406 31461376 6872 4294967295 134512640 134672761 3221224640 3221223796 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6872 603 41 0 7640 0
vsize: 30724
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6964 0 0 0 110974 40 0 0 25 0 1 0 356227406 31461376 6875 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6875 603 41 0 7640 0
vsize: 30724
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6971 0 0 0 111973 40 0 0 25 0 1 0 356227406 31461376 6882 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6882 603 41 0 7640 0
vsize: 30724
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6975 0 0 0 112974 40 0 0 25 0 1 0 356227406 31461376 6886 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6886 603 41 0 7640 0
vsize: 30724
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 6975 0 0 0 113973 40 0 0 25 0 1 0 356227406 31461376 6886 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7681 6886 603 41 0 7640 0
vsize: 30724
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7006 0 0 0 114973 40 0 0 25 0 1 0 356227406 31608832 6917 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 6917 603 41 0 7676 0
vsize: 30868
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7010 0 0 0 115973 41 0 0 25 0 1 0 356227406 31608832 6921 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 6921 603 41 0 7676 0
vsize: 30868
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7011 0 0 0 116973 41 0 0 25 0 1 0 356227406 31608832 6922 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 6922 603 41 0 7676 0
vsize: 30868
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7014 0 0 0 117973 41 0 0 25 0 1 0 356227406 31608832 6925 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7717 6925 603 41 0 7676 0
vsize: 30868
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7037 0 0 0 118973 41 0 0 25 0 1 0 356227406 31756288 6948 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7753 6948 603 41 0 7712 0
vsize: 31012
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 1522
Raw data (stat): 1462 (minisat+) R 1461 30927 30926 0 -1 0 7039 0 0 0 119973 41 0 0 25 0 1 0 356227406 31756288 6950 4294967295 134512640 134672761 3221224640 3221223744 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7753 6950 603 41 0 7712 0
vsize: 31012
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 1522
Raw data (stat): 1462 (minisat+) Z 1461 30927 30926 0 -1 12 7042 0 0 0 119973 42 0 0 25 0 1 0 356227406 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.17
CPU user time (s): 1199.74
CPU system time (s): 0.429934
CPU usage (%): 100.011
Max. virtual memory (Kb): 31012
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####