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 5126

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-13 22:01:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3551 boxname=wulflinc15 idbench=167 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ii8b1.opb
IDLAUNCH: 3551
/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:        910408 kB
Buffers:         34872 kB
Cached:          67840 kB
SwapCached:       2144 kB
Active:          60436 kB
Inactive:        47256 kB
HighTotal:      131008 kB
HighFree:        59332 kB
LowTotal:       903652 kB
LowFree:        851076 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10928 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 22:21:35 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3551 7 1200.18 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]---> Adder-cost: 1338   maxlim: 448   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   11710    38535 |    3903       2       14     7.0 |  0.000 % |
c |       102 |   11710    38535 |    4293     102      731     7.2 |  0.199 % |
c |       253 |   11710    38535 |    4722     253     1786     7.1 |  0.199 % |
c |       478 |   11710    38535 |    5194     478     4095     8.6 |  0.199 % |
c |       815 |   11710    38535 |    5714     815     8073     9.9 |  0.199 % |
c |      1321 |   11710    38535 |    6285    1321    12890     9.8 |  0.199 % |
c |      2080 |   11710    38535 |    6914    2080    42831    20.6 |  0.199 % |
c |      3220 |   11710    38535 |    7605    3220    82288    25.6 |  0.199 % |
c |      4930 |   11710    38535 |    8366    4930   121712    24.7 |  0.199 % |
c |      7492 |   11710    38535 |    9203    7492   214797    28.7 |  0.199 % |
c |     11336 |   11710    38535 |   10123    6507   240756    37.0 |  0.199 % |
c |     17102 |   11710    38535 |   11135    6725   467384    69.5 |  0.199 % |
c |     25752 |   11710    38535 |   12249    9271   603199    65.1 |  0.199 % |
c |     38726 |   11710    38535 |   13474    8983   920329   102.5 |  0.199 % |
c |     58187 |   11710    38535 |   14821   13721  1280298    93.3 |  0.199 % |
c |     87381 |   11710    38535 |   16303   11354  1224437   107.8 |  0.199 % |
c |    131172 |   11710    38535 |   17934   11960  1233727   103.2 |  0.199 % |
c |    196857 |   11710    38535 |   19727   11626  1493072   128.4 |  0.199 % |
c |    295384 |   11710    38535 |   21700   16581  2270134   136.9 |  0.199 % |
c |    443175 |   11710    38535 |   23870   19284  2044589   106.0 |  0.199 % |
c |    664858 |   11710    38535 |   26257   18442  1876398   101.7 |  0.199 % |
#### 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.96 0.98 0.91 2/54 1897
Raw data (stat): 1897 (runsolver) R 1896 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421166471 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.0012 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 1466 0 0 0 995 3 0 0 25 0 1 0 421166471 7495680 1444 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1830 1444 603 41 0 1789 0
vsize: 7320
[startup+20.0015 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 1692 0 0 0 1994 4 0 0 25 0 1 0 421166471 8433664 1670 4294967295 134512640 134672761 3221224576 3221223744 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2059 1670 603 41 0 2018 0
vsize: 8236
[startup+30.0029 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2081 0 0 0 2992 6 0 0 25 0 1 0 421166471 10039296 2059 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2451 2059 603 41 0 2410 0
vsize: 9804
[startup+40.0037 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2081 0 0 0 3992 6 0 0 25 0 1 0 421166471 10039296 2059 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2451 2059 603 41 0 2410 0
vsize: 9804
[startup+50.0051 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2188 0 0 0 4991 7 0 0 25 0 1 0 421166471 10440704 2166 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2549 2166 603 41 0 2508 0
vsize: 10196
[startup+60.0054 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2296 0 0 0 5991 8 0 0 25 0 1 0 421166471 10981376 2274 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2681 2274 603 41 0 2640 0
vsize: 10724
[startup+70.0063 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2633 0 0 0 6989 9 0 0 25 0 1 0 421166471 12333056 2611 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3011 2611 603 41 0 2970 0
vsize: 12044
[startup+80.0067 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2652 0 0 0 7989 9 0 0 25 0 1 0 421166471 12513280 2630 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2630 603 41 0 3014 0
vsize: 12220
[startup+90.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2653 0 0 0 8989 9 0 0 25 0 1 0 421166471 12513280 2631 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3055 2631 603 41 0 3014 0
vsize: 12220
[startup+100.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2806 0 0 0 9988 10 0 0 25 0 1 0 421166471 13049856 2784 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3186 2784 603 41 0 3145 0
vsize: 12744
[startup+110.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 2905 0 0 0 10987 11 0 0 25 0 1 0 421166471 13455360 2883 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3285 2883 603 41 0 3244 0
vsize: 13140
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3019 0 0 0 11987 11 0 0 25 0 1 0 421166471 13996032 2997 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 2997 603 41 0 3376 0
vsize: 13668
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3020 0 0 0 12986 12 0 0 25 0 1 0 421166471 13996032 2998 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 2998 603 41 0 3376 0
vsize: 13668
[startup+140.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3223 0 0 0 13985 13 0 0 25 0 1 0 421166471 14807040 3201 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3201 603 41 0 3574 0
vsize: 14460
[startup+150.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3398 0 0 0 14984 14 0 0 25 0 1 0 421166471 15478784 3376 4294967295 134512640 134672761 3221224576 3221223680 134560313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3376 603 41 0 3738 0
vsize: 15116
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3398 0 0 0 15984 14 0 0 25 0 1 0 421166471 15478784 3376 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3779 3376 603 41 0 3738 0
vsize: 15116
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3398 0 0 0 16984 14 0 0 25 0 1 0 421166471 15478784 3376 4294967295 134512640 134672761 3221224576 3221223760 134558754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3779 3376 603 41 0 3738 0
vsize: 15116
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3733 0 0 0 17982 16 0 0 25 0 1 0 421166471 16826368 3711 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4108 3711 603 41 0 4067 0
vsize: 16432
[startup+190.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3739 0 0 0 18983 16 0 0 25 0 1 0 421166471 16965632 3717 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4142 3717 603 41 0 4101 0
vsize: 16568
[startup+200.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3992 0 0 0 19982 17 0 0 25 0 1 0 421166471 17907712 3970 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3970 603 41 0 4331 0
vsize: 17488
[startup+210.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3992 0 0 0 20982 17 0 0 25 0 1 0 421166471 17907712 3970 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3970 603 41 0 4331 0
vsize: 17488
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3993 0 0 0 21982 17 0 0 25 0 1 0 421166471 17907712 3971 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3971 603 41 0 4331 0
vsize: 17488
[startup+230.016 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3994 0 0 0 22982 17 0 0 25 0 1 0 421166471 17907712 3972 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3972 603 41 0 4331 0
vsize: 17488
[startup+240.016 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3994 0 0 0 23982 17 0 0 25 0 1 0 421166471 17907712 3972 4294967295 134512640 134672761 3221224576 3221223680 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3972 603 41 0 4331 0
vsize: 17488
[startup+250.017 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3994 0 0 0 24983 17 0 0 25 0 1 0 421166471 17907712 3972 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3972 603 41 0 4331 0
vsize: 17488
[startup+260.016 s]
Raw data (loadavg): 1.10 1.01 0.93 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 3994 0 0 0 25983 17 0 0 25 0 1 0 421166471 17907712 3972 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3972 603 41 0 4331 0
vsize: 17488
[startup+270.017 s]
Raw data (loadavg): 1.09 1.01 0.93 2/54 1897
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4100 0 0 0 26982 17 0 0 25 0 1 0 421166471 18313216 4078 4294967295 134512640 134672761 3221224576 3221223760 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4471 4078 603 41 0 4430 0
vsize: 17884
[startup+280.017 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4100 0 0 0 27983 17 0 0 25 0 1 0 421166471 18313216 4078 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4471 4078 603 41 0 4430 0
vsize: 17884
[startup+290.017 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4258 0 0 0 28982 18 0 0 25 0 1 0 421166471 18984960 4236 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4635 4236 603 41 0 4594 0
vsize: 18540
[startup+300.018 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4258 0 0 0 29982 18 0 0 25 0 1 0 421166471 18984960 4236 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4635 4236 603 41 0 4594 0
vsize: 18540
[startup+310.019 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4392 0 0 0 30982 18 0 0 25 0 1 0 421166471 19546112 4370 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4772 4370 603 41 0 4731 0
vsize: 19088
[startup+320.019 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4399 0 0 0 31982 18 0 0 25 0 1 0 421166471 19709952 4377 4294967295 134512640 134672761 3221224576 3221223680 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4377 603 41 0 4771 0
vsize: 19248
[startup+330.019 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4400 0 0 0 32982 18 0 0 25 0 1 0 421166471 19709952 4378 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4378 603 41 0 4771 0
vsize: 19248
[startup+340.02 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4409 0 0 0 33983 18 0 0 25 0 1 0 421166471 19709952 4387 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4387 603 41 0 4771 0
vsize: 19248
[startup+350.02 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4409 0 0 0 34983 18 0 0 25 0 1 0 421166471 19709952 4387 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4387 603 41 0 4771 0
vsize: 19248
[startup+360.021 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4409 0 0 0 35983 18 0 0 25 0 1 0 421166471 19709952 4387 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4387 603 41 0 4771 0
vsize: 19248
[startup+370.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4409 0 0 0 36983 18 0 0 25 0 1 0 421166471 19709952 4387 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4812 4387 603 41 0 4771 0
vsize: 19248
[startup+380.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4410 0 0 0 37983 18 0 0 25 0 1 0 421166471 19709952 4388 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4388 603 41 0 4771 0
vsize: 19248
[startup+390.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4410 0 0 0 38983 18 0 0 25 0 1 0 421166471 19709952 4388 4294967295 134512640 134672761 3221224576 3221223744 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4388 603 41 0 4771 0
vsize: 19248
[startup+400.022 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4410 0 0 0 39983 18 0 0 25 0 1 0 421166471 19709952 4388 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4388 603 41 0 4771 0
vsize: 19248
[startup+410.023 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4410 0 0 0 40984 18 0 0 25 0 1 0 421166471 19709952 4388 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4388 603 41 0 4771 0
vsize: 19248
[startup+420.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4410 0 0 0 41984 18 0 0 25 0 1 0 421166471 19709952 4388 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4388 603 41 0 4771 0
vsize: 19248
[startup+430.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 42984 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+440.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 43984 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+450.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 44984 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+460.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 45985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+470.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 46985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+480.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 47985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+490.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 48985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+500.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 49985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+510.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 50985 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+520.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 51986 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+530.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 52986 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+540.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 53986 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+550.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 54986 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+560.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4411 0 0 0 55987 18 0 0 25 0 1 0 421166471 19709952 4389 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4389 603 41 0 4771 0
vsize: 19248
[startup+570.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4413 0 0 0 56986 18 0 0 25 0 1 0 421166471 19709952 4391 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4391 603 41 0 4771 0
vsize: 19248
[startup+580.029 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4413 0 0 0 57986 18 0 0 25 0 1 0 421166471 19709952 4391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4391 603 41 0 4771 0
vsize: 19248
[startup+590.029 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4413 0 0 0 58986 18 0 0 25 0 1 0 421166471 19709952 4391 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4391 603 41 0 4771 0
vsize: 19248
[startup+600.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4413 0 0 0 59987 18 0 0 25 0 1 0 421166471 19709952 4391 4294967295 134512640 134672761 3221224576 3221223760 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4391 603 41 0 4771 0
vsize: 19248
[startup+610.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4413 0 0 0 60987 18 0 0 25 0 1 0 421166471 19709952 4391 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4812 4391 603 41 0 4771 0
vsize: 19248
[startup+620.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4519 0 0 0 61986 19 0 0 25 0 1 0 421166471 20103168 4497 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4908 4497 603 41 0 4867 0
vsize: 19632
[startup+630.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4810 0 0 0 62986 20 0 0 25 0 1 0 421166471 21295104 4788 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5199 4788 603 41 0 5158 0
vsize: 20796
[startup+640.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4814 0 0 0 63986 20 0 0 25 0 1 0 421166471 21295104 4792 4294967295 134512640 134672761 3221224576 3221223712 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5199 4792 603 41 0 5158 0
vsize: 20796
[startup+650.03 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4814 0 0 0 64986 20 0 0 25 0 1 0 421166471 21295104 4792 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5199 4792 603 41 0 5158 0
vsize: 20796
[startup+660.031 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4814 0 0 0 65986 20 0 0 25 0 1 0 421166471 21295104 4792 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5199 4792 603 41 0 5158 0
vsize: 20796
[startup+670.031 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4974 0 0 0 66986 20 0 0 25 0 1 0 421166471 21958656 4952 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5361 4952 603 41 0 5320 0
vsize: 21444
[startup+680.032 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4987 0 0 0 67986 20 0 0 25 0 1 0 421166471 22097920 4965 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5395 4965 603 41 0 5354 0
vsize: 21580
[startup+690.032 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4987 0 0 0 68986 20 0 0 25 0 1 0 421166471 22097920 4965 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5395 4965 603 41 0 5354 0
vsize: 21580
[startup+700.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 4997 0 0 0 69986 20 0 0 25 0 1 0 421166471 22097920 4975 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5395 4975 603 41 0 5354 0
vsize: 21580
[startup+710.033 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 70987 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+720.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 71987 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+730.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 72987 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223680 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+740.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 73987 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+750.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 74987 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+760.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5005 0 0 0 75988 20 0 0 25 0 1 0 421166471 22245376 4983 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4983 603 41 0 5390 0
vsize: 21724
[startup+770.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 76988 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+780.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 77988 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223680 134560352 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+790.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 78988 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221222784 134565789 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+800.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 79988 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+810.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 80988 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223760 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+820.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 81989 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+830.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 82989 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+840.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 83989 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+850.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 84989 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+860.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5020 0 0 0 85989 20 0 0 25 0 1 0 421166471 22245376 4998 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5431 4998 603 41 0 5390 0
vsize: 21724
[startup+870.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5060 0 0 0 86989 21 0 0 25 0 1 0 421166471 22376448 5038 4294967295 134512640 134672761 3221224576 3221223712 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5463 5038 603 41 0 5422 0
vsize: 21852
[startup+880.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5060 0 0 0 87989 21 0 0 25 0 1 0 421166471 22376448 5038 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5463 5038 603 41 0 5422 0
vsize: 21852
[startup+890.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5063 0 0 0 88989 21 0 0 25 0 1 0 421166471 22376448 5041 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5463 5041 603 41 0 5422 0
vsize: 21852
[startup+900.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5063 0 0 0 89990 21 0 0 25 0 1 0 421166471 22376448 5041 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5463 5041 603 41 0 5422 0
vsize: 21852
[startup+910.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5069 0 0 0 90990 21 0 0 25 0 1 0 421166471 22519808 5047 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5047 603 41 0 5457 0
vsize: 21992
[startup+920.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5098 0 0 0 91990 21 0 0 25 0 1 0 421166471 22519808 5076 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5076 603 41 0 5457 0
vsize: 21992
[startup+930.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5098 0 0 0 92989 21 0 0 25 0 1 0 421166471 22519808 5076 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5076 603 41 0 5457 0
vsize: 21992
[startup+940.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5100 0 0 0 93990 21 0 0 25 0 1 0 421166471 22519808 5078 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5078 603 41 0 5457 0
vsize: 21992
[startup+950.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5100 0 0 0 94990 21 0 0 25 0 1 0 421166471 22519808 5078 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5078 603 41 0 5457 0
vsize: 21992
[startup+960.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5100 0 0 0 95990 21 0 0 25 0 1 0 421166471 22519808 5078 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5498 5078 603 41 0 5457 0
vsize: 21992
[startup+970.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5109 0 0 0 96990 21 0 0 25 0 1 0 421166471 22650880 5087 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5530 5087 603 41 0 5489 0
vsize: 22120
[startup+980.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5112 0 0 0 97990 21 0 0 25 0 1 0 421166471 22650880 5090 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5530 5090 603 41 0 5489 0
vsize: 22120
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5295 0 0 0 98990 22 0 0 25 0 1 0 421166471 23322624 5273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5273 603 41 0 5653 0
vsize: 22776
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5463 0 0 0 99989 23 0 0 25 0 1 0 421166471 24125440 5441 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5441 603 41 0 5849 0
vsize: 23560
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5463 0 0 0 100990 23 0 0 25 0 1 0 421166471 24125440 5441 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5441 603 41 0 5849 0
vsize: 23560
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5463 0 0 0 101990 23 0 0 25 0 1 0 421166471 24125440 5441 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5441 603 41 0 5849 0
vsize: 23560
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5463 0 0 0 102990 23 0 0 25 0 1 0 421166471 24125440 5441 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5441 603 41 0 5849 0
vsize: 23560
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5476 0 0 0 103990 23 0 0 25 0 1 0 421166471 24125440 5454 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5454 603 41 0 5849 0
vsize: 23560
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5480 0 0 0 104990 23 0 0 25 0 1 0 421166471 24125440 5458 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5890 5458 603 41 0 5849 0
vsize: 23560
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5503 0 0 0 105990 23 0 0 25 0 1 0 421166471 24260608 5481 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5923 5481 603 41 0 5882 0
vsize: 23692
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5651 0 0 0 106990 23 0 0 25 0 1 0 421166471 24793088 5629 4294967295 134512640 134672761 3221224576 3221223680 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6053 5629 603 41 0 6012 0
vsize: 24212
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5651 0 0 0 107991 23 0 0 25 0 1 0 421166471 24793088 5629 4294967295 134512640 134672761 3221224576 3221223760 134559424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6053 5629 603 41 0 6012 0
vsize: 24212
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5651 0 0 0 108991 23 0 0 25 0 1 0 421166471 24793088 5629 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6053 5629 603 41 0 6012 0
vsize: 24212
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 109991 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 110991 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 111991 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 112992 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 113992 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 114992 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5657 0 0 0 115992 23 0 0 25 0 1 0 421166471 24928256 5635 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6086 5635 603 41 0 6045 0
vsize: 24344
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5804 0 0 0 116992 24 0 0 25 0 1 0 421166471 25468928 5782 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6218 5782 603 41 0 6177 0
vsize: 24872
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5880 0 0 0 117992 24 0 0 25 0 1 0 421166471 25735168 5858 4294967295 134512640 134672761 3221224576 3221223680 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6283 5858 603 41 0 6242 0
vsize: 25132
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 5893 0 0 0 118992 24 0 0 25 0 1 0 421166471 25870336 5871 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6316 5871 603 41 0 6275 0
vsize: 25264
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 1899
Raw data (stat): 1897 (minisat+) R 1896 29151 29150 0 -1 0 6160 0 0 0 119991 25 0 0 25 0 1 0 421166471 26951680 6138 4294967295 134512640 134672761 3221224576 3221223680 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6580 6138 603 41 0 6539 0
vsize: 26320
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 1899
Raw data (stat): 1897 (minisat+) Z 1896 29151 29150 0 -1 12 6164 0 0 0 119991 26 0 0 25 0 1 0 421166471 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.06
CPU time (s): 1200.18
CPU user time (s): 1199.91
CPU system time (s): 0.267959
CPU usage (%): 100.01
Max. virtual memory (Kb): 26320
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####