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-jnh201.opb
MD5SUM	ba509931ad93c2223be235a06a9b3100
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	84
Optimality of the best value was proved	NO
Number of terms in the objective function	200
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	200
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	200
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	200
Total number of constraints	900
Number of constraints which are clauses	900
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	14
Trace number 5141

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 22:12:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3564 boxname=wulflinc19 idbench=180 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ba509931ad93c2223be235a06a9b3100  /oldhome/oroussel/tmp/wulflinc19/normalized-jnh201.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-jnh201.opb /oldhome/oroussel/tmp/wulflinc19/normalized-jnh201.opb
IDLAUNCH: 3564
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        891712 kB
Buffers:         33524 kB
Cached:          75764 kB
SwapCached:         56 kB
Active:          45968 kB
Inactive:        66312 kB
HighTotal:      131008 kB
HighFree:        51212 kB
LowTotal:       903652 kB
LowFree:        840500 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            24988 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:32:30 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3564 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 900 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 |     900     4354 |     300       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 91[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 394   maxlim: 109   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |    3617    14044 |    1205       7       55     7.9 |  0.000 % |
c |       107 |    3617    14044 |    1325     107     2664    24.9 |  0.836 % |
c |       257 |    3617    14044 |    1458     257     3997    15.6 |  0.836 % |
c |       483 |    3617    14044 |    1603     483     9834    20.4 |  0.837 % |
c |       820 |    3542    13679 |    1764     817    14442    17.7 |  1.673 % |
c |      1327 |    3542    13679 |    1940    1324    28397    21.4 |  1.673 % |
c |      2090 |    3533    13648 |    2134    2086    47632    22.8 |  1.840 % |
c |      3229 |    3533    13648 |    2348    2086    52362    25.1 |  1.840 % |
c |      4937 |    3533    13648 |    2583    2493    79786    32.0 |  1.840 % |
c |      7500 |    3533    13648 |    2841    2286    68853    30.1 |  1.840 % |
c |     11344 |    3533    13648 |    3125    3029   108773    35.9 |  1.840 % |
c ==============================================================================
c [1mFound solution: 90[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 342   maxlim: 108   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12799 |    5888    22045 |    1962    2877    74420    25.9 |  1.840 % |
c |     12901 |    5888    22045 |    2158    1541    31355    20.3 |  1.693 % |
c |     13051 |    5888    22045 |    2374    1691    33337    19.7 |  1.693 % |
c |     13276 |    5888    22045 |    2611    1916    42283    22.1 |  1.693 % |
c |     13613 |    5888    22045 |    2872    2253    52603    23.3 |  1.693 % |
c |     14121 |    5888    22045 |    3159    2761    70455    25.5 |  1.693 % |
c |     14881 |    5888    22045 |    3475    1912    40162    21.0 |  1.693 % |
c |     16020 |    5888    22045 |    3823    3051    85649    28.1 |  1.693 % |
c |     17730 |    5888    22045 |    4205    2747    70474    25.7 |  1.693 % |
c |     20292 |    5888    22045 |    4626    3046    89232    29.3 |  1.695 % |
c |     24137 |    5888    22045 |    5088    4488   175648    39.1 |  1.693 % |
c |     29903 |    5888    22045 |    5597    4991   191858    38.4 |  1.693 % |
c |     38552 |    5888    22045 |    6157    4886   171074    35.0 |  1.693 % |
c ==============================================================================
c [1mFound solution: 89[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 109   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46036 |    5889    22053 |    1963    6029   141261    23.4 |  1.693 % |
c |     46138 |    5889    22053 |    2159    1610    26301    16.3 |  1.797 % |
c |     46289 |    5889    22053 |    2375    1761    33267    18.9 |  1.797 % |
c |     46515 |    5889    22053 |    2612    1987    36365    18.3 |  1.797 % |
c |     46852 |    5889    22053 |    2874    2324    52714    22.7 |  1.797 % |
c |     47358 |    5889    22053 |    3161    2830    60167    21.3 |  1.797 % |
c |     48117 |    5889    22053 |    3477    3589    95853    26.7 |  1.797 % |
c |     49257 |    5889    22053 |    3825    2935    59986    20.4 |  1.797 % |
c |     50967 |    5889    22053 |    4207    2571    78949    30.7 |  1.797 % |
c |     53529 |    5889    22053 |    4628    2970    66264    22.3 |  1.797 % |
c |     57373 |    5889    22053 |    5091    4308   131941    30.6 |  1.797 % |
c |     63139 |    5889    22053 |    5600    4637   146362    31.6 |  1.797 % |
c ==============================================================================
c [1mFound solution: 88[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 110   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65826 |    5892    22068 |    1964    4345   126995    29.2 |  1.797 % |
c |     65929 |    5892    22068 |    2160    1190    16354    13.7 |  1.901 % |
c |     66080 |    5892    22068 |    2376    1341    21874    16.3 |  1.901 % |
c |     66305 |    5892    22068 |    2614    1566    24625    15.7 |  1.901 % |
c |     66642 |    5892    22068 |    2875    1903    31408    16.5 |  1.901 % |
c |     67149 |    5892    22068 |    3163    2410    37811    15.7 |  1.901 % |
c |     67908 |    5892    22068 |    3479    3169    76491    24.1 |  1.901 % |
c |     69048 |    5892    22068 |    3827    2528    62154    24.6 |  1.901 % |
c |     70756 |    5892    22068 |    4210    4236   140890    33.3 |  1.901 % |
c |     73320 |    5892    22068 |    4631    2485    37806    15.2 |  1.901 % |
c |     77165 |    5892    22068 |    5094    3869   124695    32.2 |  1.901 % |
c |     82932 |    5892    22068 |    5603    4241   136402    32.2 |  1.901 % |
c |     91581 |    5892    22068 |    6163    4292   105424    24.6 |  1.901 % |
c |    104557 |    5892    22068 |    6780    4712   117381    24.9 |  1.901 % |
c |    124018 |    5892    22068 |    7458    6522   214914    33.0 |  1.901 % |
c |    153210 |    5892    22068 |    8204    4840   147569    30.5 |  1.901 % |
c |    197000 |    5892    22068 |    9024    6138   184160    30.0 |  1.901 % |
c |    262684 |    5892    22068 |    9926    6826   209413    30.7 |  1.901 % |
c |    361210 |    5892    22068 |   10919    8405   276350    32.9 |  1.901 % |
c |    508999 |    5892    22068 |   12011   10861   356884    32.9 |  1.901 % |
c |    730682 |    5892    22068 |   13212   10587   400658    37.8 |  1.901 % |
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 111   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    868472 |    5893    22073 |    1964    6849   185255    27.0 |  1.901 % |
c |    868574 |    5893    22073 |    2160    1815    25868    14.3 |  2.004 % |
c |    868726 |    5893    22073 |    2376    1967    28182    14.3 |  2.004 % |
c |    868952 |    5893    22073 |    2614    2193    36851    16.8 |  2.005 % |
c |    869290 |    5893    22073 |    2875    2531    44588    17.6 |  2.004 % |
c |    869797 |    5893    22073 |    3163    3038    56433    18.6 |  2.004 % |
c |    870557 |    5893    22073 |    3479    2182    34189    15.7 |  2.004 % |
c |    871696 |    5893    22073 |    3827    3321    70559    21.2 |  2.004 % |
c |    873405 |    5893    22073 |    4210    3085    66134    21.4 |  2.004 % |
c |    875969 |    5893    22073 |    4631    3501    56589    16.2 |  2.004 % |
c |    879814 |    5893    22073 |    5094    4799   182218    38.0 |  2.005 % |
c |    885580 |    5893    22073 |    5603    2709    53960    19.9 |  2.004 % |
c |    894230 |    5893    22073 |    6163    5466   181971    33.3 |  2.004 % |
c |    907204 |    5893    22073 |    6780    5597   151580    27.1 |  2.004 % |
c ==============================================================================
c [1mFound solution: 86[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 112   bits: 8/7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    919122 |    5896    22088 |    1965    6909   210646    30.5 |  2.004 % |
c |    919222 |    5896    22088 |    2161    1828    30264    16.6 |  2.108 % |
c |    919373 |    5896    22088 |    2377    1979    34550    17.5 |  2.108 % |
c |    919598 |    5896    22088 |    2615    2204    38006    17.2 |  2.108 % |
c |    919936 |    5896    22088 |    2876    2542    50082    19.7 |  2.111 % |
c |    920442 |    5896    22088 |    3164    1547    16007    10.3 |  2.108 % |
c |    921201 |    5896    22088 |    3481    2306    50678    22.0 |  2.108 % |
c |    922340 |    5896    22088 |    3829    3445    80842    23.5 |  2.108 % |
c |    924048 |    5896    22088 |    4212    3131    77384    24.7 |  2.108 % |
c |    926612 |    5896    22088 |    4633    3516    60702    17.3 |  2.108 % |
c |    930456 |    5896    22088 |    5096    2549    59210    23.2 |  2.109 % |
c |    936222 |    5896    22088 |    5606    3055    68333    22.4 |  2.108 % |
c |    944871 |    5896    22088 |    6167    3036    62967    20.7 |  2.108 % |
c |    957846 |    5896    22088 |    6783    6383   200808    31.5 |  2.108 % |
c |    977308 |    5896    22088 |    7462    4663   116048    24.9 |  2.108 % |
c |   1006501 |    5896    22088 |    8208    6859   209625    30.6 |  2.108 % |
c |   1050290 |    5896    22088 |    9029    8246   234960    28.5 |  2.108 % |
c |   1115976 |    5896    22088 |    9932    8745   265586    30.4 |  2.108 % |
c |   1214502 |    5896    22088 |   10925    5171   141470    27.4 |  2.108 % |
c |   1362292 |    5896    22088 |   12017    7664   291474    38.0 |  2.108 % |
c |   1583975 |    5896    22088 |   13219    8445   296148    35.1 |  2.108 % |
#### 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.77 0.92 0.89 2/55 26541
Raw data (stat): 26541 (runsolver) R 26540 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479451552 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.0003 s]
Raw data (loadavg): 0.81 0.92 0.89 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 686 0 0 0 996 2 0 0 25 0 1 0 479451552 4321280 664 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1055 664 603 41 0 1014 0
vsize: 4220
[startup+20.0017 s]
Raw data (loadavg): 0.84 0.93 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 748 0 0 0 1995 3 0 0 25 0 1 0 479451552 4583424 726 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1119 726 603 41 0 1078 0
vsize: 4476
[startup+30.0022 s]
Raw data (loadavg): 0.86 0.93 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 753 0 0 0 2994 3 0 0 25 0 1 0 479451552 4583424 731 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1119 731 603 41 0 1078 0
vsize: 4476
[startup+40.0024 s]
Raw data (loadavg): 0.88 0.93 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 795 0 0 0 3994 3 0 0 25 0 1 0 479451552 4714496 773 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1151 773 603 41 0 1110 0
vsize: 4604
[startup+50.0031 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 891 0 0 0 4995 3 0 0 25 0 1 0 479451552 5115904 869 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1249 869 603 41 0 1208 0
vsize: 4996
[startup+60.0026 s]
Raw data (loadavg): 0.91 0.93 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 952 0 0 0 5994 4 0 0 25 0 1 0 479451552 5386240 930 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1315 930 603 41 0 1274 0
vsize: 5260
[startup+70.0038 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 974 0 0 0 6994 4 0 0 25 0 1 0 479451552 5521408 952 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1348 952 603 41 0 1307 0
vsize: 5392
[startup+80.0046 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1060 0 0 0 7994 4 0 0 25 0 1 0 479451552 5931008 1038 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1448 1038 603 41 0 1407 0
vsize: 5792
[startup+90.0041 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1068 0 0 0 8994 4 0 0 25 0 1 0 479451552 5931008 1046 4294967295 134512640 134672761 3221224576 3221223760 134559385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1448 1046 603 41 0 1407 0
vsize: 5792
[startup+100.004 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1080 0 0 0 9994 5 0 0 25 0 1 0 479451552 5931008 1058 4294967295 134512640 134672761 3221224576 3221223760 134558974 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1448 1058 603 41 0 1407 0
vsize: 5792
[startup+110.005 s]
Raw data (loadavg): 0.96 0.94 0.90 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1124 0 0 0 10994 5 0 0 25 0 1 0 479451552 6201344 1102 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1514 1102 603 41 0 1473 0
vsize: 6056
[startup+120.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1140 0 0 0 11994 5 0 0 25 0 1 0 479451552 6201344 1118 4294967295 134512640 134672761 3221224576 3221223744 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1514 1118 603 41 0 1473 0
vsize: 6056
[startup+130.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1151 0 0 0 12994 5 0 0 25 0 1 0 479451552 6340608 1129 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1548 1129 603 41 0 1507 0
vsize: 6192
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1161 0 0 0 13994 5 0 0 25 0 1 0 479451552 6340608 1139 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1548 1139 603 41 0 1507 0
vsize: 6192
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1209 0 0 0 14994 5 0 0 25 0 1 0 479451552 6471680 1187 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1580 1187 603 41 0 1539 0
vsize: 6320
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1219 0 0 0 15994 5 0 0 25 0 1 0 479451552 6606848 1197 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1613 1197 603 41 0 1572 0
vsize: 6452
[startup+170.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1284 0 0 0 16994 6 0 0 25 0 1 0 479451552 6877184 1262 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1679 1262 603 41 0 1638 0
vsize: 6716
[startup+180.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1284 0 0 0 17994 6 0 0 25 0 1 0 479451552 6877184 1262 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1679 1262 603 41 0 1638 0
vsize: 6716
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1284 0 0 0 18994 6 0 0 25 0 1 0 479451552 6877184 1262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1679 1262 603 41 0 1638 0
vsize: 6716
[startup+200.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1292 0 0 0 19995 6 0 0 25 0 1 0 479451552 6877184 1270 4294967295 134512640 134672761 3221224576 3221223572 1075351112 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1679 1270 603 41 0 1638 0
vsize: 6716
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1295 0 0 0 20995 6 0 0 25 0 1 0 479451552 6877184 1273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1679 1273 603 41 0 1638 0
vsize: 6716
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26541
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1327 0 0 0 21995 6 0 0 25 0 1 0 479451552 7008256 1305 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1711 1305 603 41 0 1670 0
vsize: 6844
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1341 0 0 0 22995 6 0 0 25 0 1 0 479451552 7147520 1319 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1745 1319 603 41 0 1704 0
vsize: 6980
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1368 0 0 0 23995 6 0 0 25 0 1 0 479451552 7147520 1346 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1745 1346 603 41 0 1704 0
vsize: 6980
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1376 0 0 0 24995 6 0 0 25 0 1 0 479451552 7282688 1354 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1778 1354 603 41 0 1737 0
vsize: 7112
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1376 0 0 0 25995 6 0 0 25 0 1 0 479451552 7282688 1354 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1778 1354 603 41 0 1737 0
vsize: 7112
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1445 0 0 0 26995 6 0 0 25 0 1 0 479451552 7557120 1423 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1423 603 41 0 1804 0
vsize: 7380
[startup+280.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1447 0 0 0 27996 6 0 0 25 0 1 0 479451552 7557120 1425 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1425 603 41 0 1804 0
vsize: 7380
[startup+290.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1453 0 0 0 28996 6 0 0 25 0 1 0 479451552 7557120 1431 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1431 603 41 0 1804 0
vsize: 7380
[startup+300.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1456 0 0 0 29996 6 0 0 25 0 1 0 479451552 7557120 1434 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1434 603 41 0 1804 0
vsize: 7380
[startup+310.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1456 0 0 0 30996 6 0 0 25 0 1 0 479451552 7557120 1434 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1434 603 41 0 1804 0
vsize: 7380
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1456 0 0 0 31996 6 0 0 25 0 1 0 479451552 7557120 1434 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1845 1434 603 41 0 1804 0
vsize: 7380
[startup+330.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1468 0 0 0 32996 6 0 0 25 0 1 0 479451552 7692288 1446 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1878 1446 603 41 0 1837 0
vsize: 7512
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1545 0 0 0 33996 7 0 0 25 0 1 0 479451552 7958528 1523 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1943 1523 603 41 0 1902 0
vsize: 7772
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1545 0 0 0 34996 7 0 0 25 0 1 0 479451552 7958528 1523 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1943 1523 603 41 0 1902 0
vsize: 7772
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1587 0 0 0 35996 7 0 0 25 0 1 0 479451552 8089600 1565 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1565 603 41 0 1934 0
vsize: 7900
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1591 0 0 0 36996 7 0 0 25 0 1 0 479451552 8089600 1569 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1569 603 41 0 1934 0
vsize: 7900
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1591 0 0 0 37997 7 0 0 25 0 1 0 479451552 8089600 1569 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1569 603 41 0 1934 0
vsize: 7900
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1591 0 0 0 38997 7 0 0 25 0 1 0 479451552 8089600 1569 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1569 603 41 0 1934 0
vsize: 7900
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1592 0 0 0 39997 7 0 0 25 0 1 0 479451552 8089600 1570 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1570 603 41 0 1934 0
vsize: 7900
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1592 0 0 0 40997 7 0 0 25 0 1 0 479451552 8089600 1570 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1570 603 41 0 1934 0
vsize: 7900
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1595 0 0 0 41997 7 0 0 25 0 1 0 479451552 8089600 1573 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1975 1573 603 41 0 1934 0
vsize: 7900
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1605 0 0 0 42997 7 0 0 25 0 1 0 479451552 8228864 1583 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2009 1583 603 41 0 1968 0
vsize: 8036
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1613 0 0 0 43998 7 0 0 25 0 1 0 479451552 8228864 1591 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2009 1591 603 41 0 1968 0
vsize: 8036
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1626 0 0 0 44998 7 0 0 25 0 1 0 479451552 8228864 1604 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2009 1604 603 41 0 1968 0
vsize: 8036
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1702 0 0 0 45998 8 0 0 25 0 1 0 479451552 8626176 1680 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1680 603 41 0 2065 0
vsize: 8424
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1702 0 0 0 46998 8 0 0 25 0 1 0 479451552 8626176 1680 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1680 603 41 0 2065 0
vsize: 8424
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1702 0 0 0 47998 8 0 0 25 0 1 0 479451552 8626176 1680 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1680 603 41 0 2065 0
vsize: 8424
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1702 0 0 0 48998 8 0 0 25 0 1 0 479451552 8626176 1680 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1680 603 41 0 2065 0
vsize: 8424
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1703 0 0 0 49998 8 0 0 25 0 1 0 479451552 8626176 1681 4294967295 134512640 134672761 3221224576 3221223760 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1681 603 41 0 2065 0
vsize: 8424
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1703 0 0 0 50998 8 0 0 25 0 1 0 479451552 8626176 1681 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1681 603 41 0 2065 0
vsize: 8424
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26543
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1713 0 0 0 51998 8 0 0 25 0 1 0 479451552 8626176 1691 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1691 603 41 0 2065 0
vsize: 8424
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1714 0 0 0 52998 8 0 0 25 0 1 0 479451552 8626176 1692 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1692 603 41 0 2065 0
vsize: 8424
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1718 0 0 0 53998 8 0 0 25 0 1 0 479451552 8626176 1696 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2106 1696 603 41 0 2065 0
vsize: 8424
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1723 0 0 0 54998 8 0 0 25 0 1 0 479451552 8769536 1701 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1701 603 41 0 2100 0
vsize: 8564
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1723 0 0 0 55999 8 0 0 25 0 1 0 479451552 8769536 1701 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1701 603 41 0 2100 0
vsize: 8564
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1734 0 0 0 56999 8 0 0 25 0 1 0 479451552 8769536 1712 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1712 603 41 0 2100 0
vsize: 8564
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1738 0 0 0 57999 8 0 0 25 0 1 0 479451552 8769536 1716 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1716 603 41 0 2100 0
vsize: 8564
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1747 0 0 0 58999 8 0 0 25 0 1 0 479451552 8769536 1725 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1725 603 41 0 2100 0
vsize: 8564
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1747 0 0 0 59999 9 0 0 25 0 1 0 479451552 8769536 1725 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2141 1725 603 41 0 2100 0
vsize: 8564
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 60999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 61999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 62999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 63999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223532 1075350803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 64998 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 65998 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 66998 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223732 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 67999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 68999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 69999 9 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 70999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+720.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 71999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 72999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 73999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 74999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 76000 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+770.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 76999 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1751 0 0 0 78000 10 0 0 25 0 1 0 479451552 8916992 1729 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1729 603 41 0 2136 0
vsize: 8708
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1754 0 0 0 79000 10 0 0 25 0 1 0 479451552 8916992 1732 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1732 603 41 0 2136 0
vsize: 8708
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1757 0 0 0 80000 10 0 0 25 0 1 0 479451552 8916992 1735 4294967295 134512640 134672761 3221224576 3221223672 1075347325 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1735 603 41 0 2136 0
vsize: 8708
[startup+810.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1757 0 0 0 81000 10 0 0 25 0 1 0 479451552 8916992 1735 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1735 603 41 0 2136 0
vsize: 8708
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26545
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1760 0 0 0 82000 10 0 0 25 0 1 0 479451552 8916992 1738 4294967295 134512640 134672761 3221224576 3221223680 134554625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1738 603 41 0 2136 0
vsize: 8708
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1760 0 0 0 83000 10 0 0 25 0 1 0 479451552 8916992 1738 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1738 603 41 0 2136 0
vsize: 8708
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1760 0 0 0 84001 10 0 0 25 0 1 0 479451552 8916992 1738 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1738 603 41 0 2136 0
vsize: 8708
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1771 0 0 0 85001 10 0 0 25 0 1 0 479451552 8916992 1749 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2177 1749 603 41 0 2136 0
vsize: 8708
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1817 0 0 0 86001 10 0 0 25 0 1 0 479451552 9191424 1795 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1795 603 41 0 2203 0
vsize: 8976
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1823 0 0 0 87001 10 0 0 25 0 1 0 479451552 9191424 1801 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1801 603 41 0 2203 0
vsize: 8976
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1823 0 0 0 88001 10 0 0 25 0 1 0 479451552 9191424 1801 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1801 603 41 0 2203 0
vsize: 8976
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1823 0 0 0 89001 10 0 0 25 0 1 0 479451552 9191424 1801 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1801 603 41 0 2203 0
vsize: 8976
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1824 0 0 0 90001 10 0 0 25 0 1 0 479451552 9191424 1802 4294967295 134512640 134672761 3221224576 3221223760 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1802 603 41 0 2203 0
vsize: 8976
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1824 0 0 0 91001 10 0 0 25 0 1 0 479451552 9191424 1802 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1802 603 41 0 2203 0
vsize: 8976
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1824 0 0 0 92002 10 0 0 25 0 1 0 479451552 9191424 1802 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1802 603 41 0 2203 0
vsize: 8976
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1824 0 0 0 93002 10 0 0 25 0 1 0 479451552 9191424 1802 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1802 603 41 0 2203 0
vsize: 8976
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1830 0 0 0 94002 10 0 0 25 0 1 0 479451552 9191424 1808 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2244 1808 603 41 0 2203 0
vsize: 8976
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1869 0 0 0 95002 11 0 0 25 0 1 0 479451552 9322496 1847 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2276 1847 603 41 0 2235 0
vsize: 9104
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1869 0 0 0 96002 11 0 0 25 0 1 0 479451552 9322496 1847 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2276 1847 603 41 0 2235 0
vsize: 9104
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1872 0 0 0 97002 11 0 0 25 0 1 0 479451552 9322496 1850 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2276 1850 603 41 0 2235 0
vsize: 9104
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1889 0 0 0 98002 11 0 0 25 0 1 0 479451552 9453568 1867 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1867 603 41 0 2267 0
vsize: 9232
[startup+990.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1889 0 0 0 99002 11 0 0 25 0 1 0 479451552 9453568 1867 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1867 603 41 0 2267 0
vsize: 9232
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1893 0 0 0 100002 11 0 0 25 0 1 0 479451552 9453568 1871 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1871 603 41 0 2267 0
vsize: 9232
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 101002 11 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 102002 11 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223728 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 103002 11 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 104002 11 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 105003 11 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 106003 12 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223736 134559749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 107003 12 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 108003 12 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 109003 12 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1896 0 0 0 110003 12 0 0 25 0 1 0 479451552 9453568 1874 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2308 1874 603 41 0 2267 0
vsize: 9232
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1909 0 0 0 111003 12 0 0 25 0 1 0 479451552 9588736 1887 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2341 1887 603 41 0 2300 0
vsize: 9364
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26547
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1914 0 0 0 112003 12 0 0 25 0 1 0 479451552 9588736 1892 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2341 1892 603 41 0 2300 0
vsize: 9364
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1918 0 0 0 113003 12 0 0 25 0 1 0 479451552 9588736 1896 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2341 1896 603 41 0 2300 0
vsize: 9364
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1938 0 0 0 114003 12 0 0 25 0 1 0 479451552 9732096 1916 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1916 603 41 0 2335 0
vsize: 9504
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1944 0 0 0 115003 12 0 0 25 0 1 0 479451552 9732096 1922 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1922 603 41 0 2335 0
vsize: 9504
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1944 0 0 0 116003 12 0 0 25 0 1 0 479451552 9732096 1922 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1922 603 41 0 2335 0
vsize: 9504
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1948 0 0 0 117003 12 0 0 25 0 1 0 479451552 9732096 1926 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1926 603 41 0 2335 0
vsize: 9504
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1952 0 0 0 118004 12 0 0 25 0 1 0 479451552 9732096 1930 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1930 603 41 0 2335 0
vsize: 9504
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1952 0 0 0 119004 12 0 0 25 0 1 0 479451552 9732096 1930 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1930 603 41 0 2335 0
vsize: 9504
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26549
Raw data (stat): 26541 (minisat+) R 26540 22929 22928 0 -1 0 1953 0 0 0 120004 12 0 0 25 0 1 0 479451552 9732096 1931 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2376 1931 603 41 0 2335 0
vsize: 9504
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26549
Raw data (stat): 26541 (minisat+) Z 26540 22929 22928 0 -1 12 1956 0 0 0 120004 13 0 0 25 0 1 0 479451552 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.03
CPU time (s): 1200.18
CPU user time (s): 1200.04
CPU system time (s): 0.132979
CPU usage (%): 100.012
Max. virtual memory (Kb): 9504
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####