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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb30-15-opb/normalized-frb30-15-2.opb
MD5SUM	25130921f4384cc034832ca1cd52ec48
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-30
Optimality of the best value was proved	NO
Number of terms in the objective function	450
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	450
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	450
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05584
Number of variables	450
Total number of constraints	17874
Number of constraints which are clauses	17874
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	2
Trace number 5231

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-13 22:44:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3699 boxname=wulflinc21 idbench=315 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  25130921f4384cc034832ca1cd52ec48  /oldhome/oroussel/tmp/wulflinc21/normalized-frb30-15-2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-frb30-15-2.opb /oldhome/oroussel/tmp/wulflinc21/normalized-frb30-15-2.opb
IDLAUNCH: 3699
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906808 kB
Buffers:         26552 kB
Cached:          81568 kB
SwapCached:          0 kB
Active:          34276 kB
Inactive:        76676 kB
HighTotal:      131008 kB
HighFree:        45836 kB
LowTotal:       903652 kB
LowFree:        860972 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11364 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:04:08 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3699 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17874 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 |   17874    35748 |    5958       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -20[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 883   maxlim: 20   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23892    57256 |    7964       0        0     nan |  0.000 % |
c |       100 |   23874    57194 |    8760      96      955     9.9 |  0.384 % |
c |       250 |   23874    57194 |    9636     246     2349     9.5 |  0.378 % |
c |       475 |   23856    57132 |   10600     467     5621    12.0 |  0.529 % |
c |       812 |   23820    57008 |   11660     792     9919    12.5 |  0.839 % |
c |      1320 |   23727    56689 |   12826    1277    25375    19.9 |  1.669 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 21   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1545 |   23582    56195 |    7860    1470    28004    19.1 |  1.669 % |
c |      1645 |   23567    56144 |    8646    1567    29413    18.8 |  3.321 % |
c |      1795 |   23540    56051 |    9510    1700    31975    18.8 |  3.547 % |
c |      2020 |   23456    55763 |   10461    1905    35360    18.6 |  4.302 % |
c |      2358 |   23438    55701 |   11507    2238    42976    19.2 |  4.462 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2668 |   23219    54954 |    7739    2475    47784    19.3 |  4.462 % |
c |      2768 |   23219    54954 |    8512    2574    49300    19.2 |  7.014 % |
c |      2918 |   23092    54519 |    9364    2698    52590    19.5 |  8.447 % |
c |      3143 |   22883    53794 |   10300    2858    55278    19.3 | 11.011 % |
c |      3480 |   22679    53092 |   11330    3132    60782    19.4 | 13.726 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3925 |   22568    52708 |    7522    3538    73695    20.8 | 13.726 % |
c |      4025 |   22521    52545 |    8274    3628    75151    20.7 | 15.750 % |
c |      4175 |   22096    51070 |    9101    3684    78408    21.3 | 21.854 % |
c |      4400 |   22034    50854 |   10011    3868    81762    21.1 | 22.683 % |
c |      4737 |   21990    50700 |   11012    4197    92992    22.2 | 23.361 % |
c |      5243 |   21941    50529 |   12114    4682   107580    23.0 | 24.039 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5830 |   21911    50425 |    7303    5238   131026    25.0 | 24.039 % |
c |      5930 |   21902    50394 |    8033    5313   132694    25.0 | 24.624 % |
c |      6082 |   21902    50394 |    8836    5465   136281    24.9 | 24.624 % |
c |      6307 |   21902    50394 |    9720    5690   147697    26.0 | 24.624 % |
c |      6646 |   21902    50394 |   10692    6029   159744    26.5 | 24.624 % |
c |      7152 |   21885    50335 |   11761    6528   176988    27.1 | 24.849 % |
c |      7911 |   21874    50296 |   12937    7283   212329    29.2 | 25.000 % |
c |      9051 |   21826    50126 |   14231    8406   272583    32.4 | 25.836 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9254 |   21827    50132 |    7275    8609   281098    32.7 | 25.836 % |
c |      9354 |   21818    50101 |    8002    4389   142408    32.4 | 25.967 % |
c |      9504 |   21807    50062 |    8802    4535   147906    32.6 | 26.115 % |
c |      9729 |   21758    49893 |    9683    4732   153730    32.5 | 26.718 % |
c |     10066 |   21758    49893 |   10651    5069   170496    33.6 | 26.712 % |
c |     10572 |   21674    49601 |   11716    5547   191514    34.5 | 27.922 % |
c |     11331 |   21625    49428 |   12888    6283   218649    34.8 | 28.668 % |
c |     12470 |   21532    49105 |   14176    7393   317118    42.9 | 30.179 % |
c |     14178 |   21523    49074 |   15594    9094   445035    48.9 | 30.248 % |
c |     16741 |   21490    48961 |   17154   11591   608979    52.5 | 30.549 % |
c |     20585 |   21490    48961 |   18869   15435   820264    53.1 | 30.549 % |
c |     26351 |   21490    48961 |   20756   11352   483397    42.6 | 30.549 % |
c |     35000 |   21383    48600 |   22832   19934  1001294    50.2 | 31.979 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37009 |   21361    48526 |    7120   21931  1102750    50.3 | 31.979 % |
c |     37109 |   21361    48526 |    7832    5583   198353    35.5 | 32.406 % |
c |     37260 |   21361    48526 |    8615    5734   204902    35.7 | 32.406 % |
c |     37485 |   21352    48495 |    9476    5955   211918    35.6 | 32.481 % |
c |     37822 |   21352    48495 |   10424    6292   224867    35.7 | 32.487 % |
c |     38328 |   21352    48495 |   11466    6798   250919    36.9 | 32.488 % |
c |     39087 |   21343    48464 |   12613    7550   288340    38.2 | 32.556 % |
c |     40227 |   21343    48464 |   13874    8690   353754    40.7 | 32.556 % |
c |     41936 |   21343    48464 |   15262   10399   429122    41.3 | 32.556 % |
c |     44498 |   21343    48464 |   16788   12961   563745    43.5 | 32.556 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46875 |   21344    48469 |    7114   15338   685507    44.7 | 32.556 % |
c |     46976 |   21323    48394 |    7825    3933   121501    30.9 | 32.983 % |
c |     47126 |   21323    48394 |    8607    4083   128634    31.5 | 32.983 % |
c |     47351 |   21323    48394 |    9468    4308   137468    31.9 | 32.983 % |
c |     47689 |   21323    48394 |   10415    4646   153005    32.9 | 32.983 % |
c |     48195 |   21297    48300 |   11457    5143   168028    32.7 | 33.434 % |
c |     48955 |   21286    48261 |   12602    5901   182385    30.9 | 33.584 % |
c |     50095 |   21286    48261 |   13863    7041   247209    35.1 | 33.584 % |
c |     51803 |   21286    48261 |   15249    8749   343319    39.2 | 33.584 % |
c |     54367 |   21286    48261 |   16774   11313   451418    39.9 | 33.591 % |
c |     58212 |   21286    48261 |   18451   15158   656962    43.3 | 33.584 % |
c |     63979 |   21286    48261 |   20297   11320   373124    33.0 | 33.584 % |
c |     72628 |   21286    48261 |   22326   19969   831430    41.6 | 33.584 % |
c |     85603 |   21286    48261 |   24559   21406  1103281    51.5 | 33.584 % |
c |    105064 |   21286    48261 |   27015   15490  1024757    66.2 | 33.591 % |
c |    134256 |   21286    48261 |   29716   15679   947990    60.5 | 33.591 % |
c |    178046 |   21286    48261 |   32688   26645  2302003    86.4 | 33.591 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    190951 |   21279    48239 |    7093   19795  1136168    57.4 | 33.591 % |
c |    191051 |   21279    48239 |    7802    5049   156196    30.9 | 33.684 % |
c |    191203 |   21262    48178 |    8582    5200   160470    30.9 | 33.989 % |
c |    191428 |   21250    48138 |    9440    5421   167330    30.9 | 34.134 % |
c |    191765 |   21250    48138 |   10384    5758   176309    30.6 | 34.134 % |
c |    192271 |   21250    48138 |   11423    6264   197143    31.5 | 34.134 % |
c |    193030 |   21250    48138 |   12565    7023   233340    33.2 | 34.134 % |
c |    194169 |   21250    48138 |   13822    8162   261370    32.0 | 34.134 % |
c |    195877 |   21250    48138 |   15204    9870   308881    31.3 | 34.134 % |
c |    198439 |   21250    48138 |   16724   12432   385416    31.0 | 34.140 % |
c |    202285 |   21250    48138 |   18397   16278   517656    31.8 | 34.134 % |
c |    208051 |   21218    48026 |   20237   12429   312730    25.2 | 34.584 % |
c |    216700 |   21218    48026 |   22260   10591   256456    24.2 | 34.590 % |
c |    229674 |   21218    48026 |   24486   12056   303602    25.2 | 34.591 % |
c |    249136 |   21218    48026 |   26935   18931   406328    21.5 | 34.584 % |
c |    278329 |   21218    48026 |   29629   20457   473361    23.1 | 34.584 % |
c |    322118 |   21218    48026 |   32592   17769   686744    38.6 | 34.591 % |
c |    387803 |   21218    48026 |   35851   27729  1382964    49.9 | 34.584 % |
c |    486329 |   21218    48026 |   39436   26822   592163    22.1 | 34.584 % |
c |    634118 |   21218    48026 |   43380   35297   837529    23.7 | 34.589 % |
c |    855801 |   21218    48026 |   47718   38513   849733    22.1 | 34.584 % |
#### 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.84 0.94 0.90 2/55 2224
Raw data (stat): 2224 (runsolver) R 2223 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 356909433 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 1456 0 0 0 996 3 0 0 25 0 1 0 356909433 7573504 1434 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1849 1434 603 41 0 1808 0
vsize: 7396
[startup+20.0011 s]
Raw data (loadavg): 0.89 0.94 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 1853 0 0 0 1994 4 0 0 25 0 1 0 356909433 9281536 1831 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2266 1831 603 41 0 2225 0
vsize: 9064
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.94 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2008 0 0 0 2994 5 0 0 25 0 1 0 356909433 9818112 1986 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2397 1986 603 41 0 2356 0
vsize: 9588
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2008 0 0 0 3994 5 0 0 25 0 1 0 356909433 9818112 1986 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2397 1986 603 41 0 2356 0
vsize: 9588
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2009 0 0 0 4994 5 0 0 25 0 1 0 356909433 9818112 1987 4294967295 134512640 134672761 3221224560 3221223728 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2397 1987 603 41 0 2356 0
vsize: 9588
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.95 0.90 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2220 0 0 0 5993 6 0 0 25 0 1 0 356909433 10756096 2198 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2626 2198 603 41 0 2585 0
vsize: 10504
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2407 0 0 0 6993 6 0 0 25 0 1 0 356909433 11431936 2385 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2791 2385 603 41 0 2750 0
vsize: 11164
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2657 0 0 0 7992 7 0 0 25 0 1 0 356909433 12533760 2635 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3060 2635 603 41 0 3019 0
vsize: 12240
[startup+90.0019 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2703 0 0 0 8992 8 0 0 25 0 1 0 356909433 12664832 2681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3092 2681 603 41 0 3051 0
vsize: 12368
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2933 0 0 0 9991 8 0 0 25 0 1 0 356909433 13594624 2911 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3319 2911 603 41 0 3278 0
vsize: 13276
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 2940 0 0 0 10991 8 0 0 25 0 1 0 356909433 13733888 2918 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3353 2918 603 41 0 3312 0
vsize: 13412
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 3009 0 0 0 11991 9 0 0 25 0 1 0 356909433 14004224 2987 4294967295 134512640 134672761 3221224560 3221223744 134559332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3419 2987 603 41 0 3378 0
vsize: 13676
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 3460 0 0 0 12989 10 0 0 25 0 1 0 356909433 15888384 3438 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3879 3438 603 41 0 3838 0
vsize: 15516
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 3783 0 0 0 13989 11 0 0 25 0 1 0 356909433 17092608 3761 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4173 3761 603 41 0 4132 0
vsize: 16692
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 3884 0 0 0 14988 11 0 0 25 0 1 0 356909433 17526784 3862 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4279 3862 603 41 0 4238 0
vsize: 17116
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4503 0 0 0 15987 13 0 0 25 0 1 0 356909433 20099072 4481 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4481 603 41 0 4866 0
vsize: 19628
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4602 0 0 0 16986 14 0 0 25 0 1 0 356909433 20504576 4580 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5006 4580 603 41 0 4965 0
vsize: 20024
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4607 0 0 0 17986 14 0 0 25 0 1 0 356909433 20647936 4585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5041 4585 603 41 0 5000 0
vsize: 20164
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4641 0 0 0 18986 15 0 0 25 0 1 0 356909433 20910080 4619 4294967295 134512640 134672761 3221224560 3221223664 134560361 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4619 603 41 0 5064 0
vsize: 20420
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4641 0 0 0 19986 15 0 0 25 0 1 0 356909433 20910080 4619 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4619 603 41 0 5064 0
vsize: 20420
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4641 0 0 0 20985 15 0 0 25 0 1 0 356909433 20910080 4619 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4619 603 41 0 5064 0
vsize: 20420
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 21985 15 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 22986 15 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 23986 15 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 24986 16 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 25986 16 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 26985 16 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4642 0 0 0 27986 16 0 0 25 0 1 0 356909433 20910080 4620 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4620 603 41 0 5064 0
vsize: 20420
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 28986 16 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 29986 16 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 30985 17 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223744 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 31986 17 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 32985 17 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221222416 134565793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 33986 17 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223696 134560714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4643 0 0 0 34985 17 0 0 25 0 1 0 356909433 20910080 4621 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4621 603 41 0 5064 0
vsize: 20420
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4644 0 0 0 35985 17 0 0 25 0 1 0 356909433 20910080 4622 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4622 603 41 0 5064 0
vsize: 20420
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4645 0 0 0 36985 18 0 0 25 0 1 0 356909433 20910080 4623 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4623 603 41 0 5064 0
vsize: 20420
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4646 0 0 0 37985 18 0 0 25 0 1 0 356909433 20910080 4624 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4624 603 41 0 5064 0
vsize: 20420
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4646 0 0 0 38985 18 0 0 25 0 1 0 356909433 20910080 4624 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4624 603 41 0 5064 0
vsize: 20420
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4648 0 0 0 39985 18 0 0 25 0 1 0 356909433 20910080 4626 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4626 603 41 0 5064 0
vsize: 20420
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 40986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 41986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 42986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 43986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 44986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 45986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 46986 18 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 47986 19 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223744 134558697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 48986 19 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4649 0 0 0 49986 19 0 0 25 0 1 0 356909433 20910080 4627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4627 603 41 0 5064 0
vsize: 20420
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4653 0 0 0 50986 19 0 0 25 0 1 0 356909433 20910080 4631 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4631 603 41 0 5064 0
vsize: 20420
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4653 0 0 0 51986 19 0 0 25 0 1 0 356909433 20910080 4631 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4631 603 41 0 5064 0
vsize: 20420
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4653 0 0 0 52986 19 0 0 25 0 1 0 356909433 20910080 4631 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4631 603 41 0 5064 0
vsize: 20420
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4653 0 0 0 53986 19 0 0 25 0 1 0 356909433 20910080 4631 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4631 603 41 0 5064 0
vsize: 20420
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4653 0 0 0 54986 19 0 0 25 0 1 0 356909433 20910080 4631 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4631 603 41 0 5064 0
vsize: 20420
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 55987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 56987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 57987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 58987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 59987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 60987 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 61988 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 62988 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 63988 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4654 0 0 0 64988 19 0 0 25 0 1 0 356909433 20910080 4632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4632 603 41 0 5064 0
vsize: 20420
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4658 0 0 0 65988 19 0 0 25 0 1 0 356909433 20910080 4636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4636 603 41 0 5064 0
vsize: 20420
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4658 0 0 0 66988 19 0 0 25 0 1 0 356909433 20910080 4636 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4636 603 41 0 5064 0
vsize: 20420
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4658 0 0 0 67988 20 0 0 25 0 1 0 356909433 20910080 4636 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4636 603 41 0 5064 0
vsize: 20420
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 68988 20 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134561269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 69988 20 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223664 134554629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 70988 20 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+720.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 71987 21 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 72988 21 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 73988 21 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4660 0 0 0 74988 21 0 0 25 0 1 0 356909433 20910080 4638 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4638 603 41 0 5064 0
vsize: 20420
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4662 0 0 0 75988 21 0 0 25 0 1 0 356909433 20910080 4640 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4640 603 41 0 5064 0
vsize: 20420
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 76988 21 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 77988 21 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+790.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 78988 21 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 79988 21 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 80988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 81988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+830.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 82988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 83988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 84988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 85988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 86988 22 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 87988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 88988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 89988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 90988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+920.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 91988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 92988 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223716 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 93989 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 2224
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4667 0 0 0 94989 23 0 0 25 0 1 0 356909433 20910080 4645 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4645 603 41 0 5064 0
vsize: 20420
[startup+960.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4668 0 0 0 95989 23 0 0 25 0 1 0 356909433 20910080 4646 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4646 603 41 0 5064 0
vsize: 20420
[startup+970.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4668 0 0 0 96989 23 0 0 25 0 1 0 356909433 20910080 4646 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4646 603 41 0 5064 0
vsize: 20420
[startup+980.014 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4671 0 0 0 97989 23 0 0 25 0 1 0 356909433 20910080 4649 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5105 4649 603 41 0 5064 0
vsize: 20420
[startup+990.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4671 0 0 0 98989 24 0 0 25 0 1 0 356909433 20910080 4649 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4649 603 41 0 5064 0
vsize: 20420
[startup+1000.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4675 0 0 0 99989 24 0 0 25 0 1 0 356909433 20910080 4653 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4653 603 41 0 5064 0
vsize: 20420
[startup+1010.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2277
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4675 0 0 0 100989 24 0 0 25 0 1 0 356909433 20910080 4653 4294967295 134512640 134672761 3221224560 3221223664 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4653 603 41 0 5064 0
vsize: 20420
[startup+1020.02 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4675 0 0 0 101989 25 0 0 25 0 1 0 356909433 20910080 4653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4653 603 41 0 5064 0
vsize: 20420
[startup+1030.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4675 0 0 0 102988 25 0 0 25 0 1 0 356909433 20910080 4653 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4653 603 41 0 5064 0
vsize: 20420
[startup+1040.02 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 103989 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1050.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 104988 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1060.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 105988 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1070.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 106989 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1080.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 107989 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1090.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 108989 25 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 109989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 110989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 111989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 112989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 113989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 114989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 115989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223664 134559941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 116989 26 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 117989 27 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 118989 27 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 2281
Raw data (stat): 2224 (minisat+) R 2223 30927 30926 0 -1 0 4677 0 0 0 119989 27 0 0 25 0 1 0 356909433 20910080 4655 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4655 603 41 0 5064 0
vsize: 20420
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 2281
Raw data (stat): 2224 (minisat+) Z 2223 30927 30926 0 -1 12 4680 0 0 0 119989 28 0 0 25 0 1 0 356909433 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.18
CPU user time (s): 1199.9
CPU system time (s): 0.283956
CPU usage (%): 100.012
Max. virtual memory (Kb): 20420
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####