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/synthesis-ptl-cmos-circuits/normalized-cc.opb
MD5SUM	0493ba9e257fafbb54efa7af2eeb7bf2
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1567
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	60
Number of bits for the biggest coefficient in the objective function	6
Sum of the numbers in the objective function	5699
Number of bits of the sum of numbers in the objective function	13
Biggest number in a constraint	60
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	5699
Number of bits of the biggest sum of numbers	13
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.134979
Number of variables	133
Total number of constraints	229
Number of constraints which are clauses	229
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	1
Maximum length of a constraint	31
Trace number 6342

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 04:22:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4763 boxname=wulflinc8 idbench=251 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0493ba9e257fafbb54efa7af2eeb7bf2  /oldhome/oroussel/tmp/wulflinc8/normalized-cc.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-cc.opb /oldhome/oroussel/tmp/wulflinc8/normalized-cc.opb
IDLAUNCH: 4763
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        875532 kB
Buffers:         37740 kB
Cached:         100028 kB
SwapCached:          0 kB
Active:          75728 kB
Inactive:        66672 kB
HighTotal:      131008 kB
HighFree:        25312 kB
LowTotal:       903652 kB
LowFree:        850220 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11148 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:42:38 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 4763 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 199 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 |     197      772 |      65       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 1846[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10637     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27890    65665 |    9296       0        0     nan |  0.000 % |
c |       100 |   27875    65632 |   10225      99     2048    20.7 |  0.173 % |
c |       251 |   27875    65632 |   11248     250     2926    11.7 |  0.173 % |
c |       476 |   27674    65178 |   12372     471     5536    11.8 |  0.705 % |
c |       813 |   27674    65178 |   13610     808     8820    10.9 |  0.704 % |
c |      1319 |   27606    65023 |   14971    1302    29429    22.6 |  0.922 % |
c |      2078 |   27606    65023 |   16468    2061    53508    26.0 |  0.921 % |
c |      3217 |   27606    65023 |   18115    3200   105267    32.9 |  0.921 % |
c ==============================================================================
c [1mFound solution: 1821[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3278 |   28012    66045 |    9337    3261   107887    33.1 |  0.921 % |
c |      3378 |   28012    66045 |   10270    3361   109355    32.5 |  0.944 % |
c |      3528 |   28012    66045 |   11297    3511   111412    31.7 |  0.943 % |
c ==============================================================================
c [1mFound solution: 1814[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3650 |   28081    66231 |    9360    3633   114553    31.5 |  0.943 % |
c |      3750 |   28059    66181 |   10296    3732   115855    31.0 |  1.017 % |
c |      3902 |   28059    66181 |   11325    3884   118354    30.5 |  1.017 % |
c ==============================================================================
c [1mFound solution: 1787[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3951 |   28318    66826 |    9439    3933   119061    30.3 |  1.017 % |
c |      4052 |   28318    66826 |   10382    4034   124034    30.7 |  1.031 % |
c |      4203 |   28318    66826 |   11421    4185   127387    30.4 |  1.031 % |
c |      4429 |   28232    66628 |   12563    4389   129578    29.5 |  1.307 % |
c |      4768 |   28232    66628 |   13819    4728   155082    32.8 |  1.307 % |
c |      5274 |   28232    66628 |   15201    5234   165528    31.6 |  1.308 % |
c |      6033 |   28232    66628 |   16721    5993   188751    31.5 |  1.307 % |
c |      7172 |   28232    66628 |   18393    7132   269887    37.8 |  1.307 % |
c |      8881 |   28232    66628 |   20233    8841   333235    37.7 |  1.307 % |
c |     11443 |   28232    66628 |   22256   11403   473878    41.6 |  1.307 % |
c ==============================================================================
c [1mFound solution: 1722[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11694 |   28289    66776 |    9429   11653   485103    41.6 |  1.307 % |
c |     11794 |   28289    66776 |   10371    5927   232131    39.2 |  1.347 % |
c |     11945 |   28289    66776 |   11409    6078   234574    38.6 |  1.347 % |
c |     12171 |   28289    66776 |   12549    6304   238314    37.8 |  1.347 % |
c |     12508 |   28289    66776 |   13804    6641   245557    37.0 |  1.347 % |
c ==============================================================================
c [1mFound solution: 1711[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12719 |   28313    66838 |    9437    6852   256172    37.4 |  1.347 % |
c |     12819 |   28313    66838 |   10380    6952   258279    37.2 |  1.356 % |
c |     12971 |   28313    66838 |   11418    7104   261152    36.8 |  1.356 % |
c |     13196 |   28313    66838 |   12560    7329   272451    37.2 |  1.356 % |
c |     13533 |   27986    66087 |   13816    7634   288517    37.8 |  2.342 % |
c |     14039 |   27986    66087 |   15198    8140   307617    37.8 |  2.342 % |
c |     14799 |   27986    66087 |   16718    8900   326371    36.7 |  2.342 % |
c |     15938 |   27982    66078 |   18390   10038   354615    35.3 |  2.352 % |
c |     17647 |   27982    66078 |   20229   11747   424724    36.2 |  2.352 % |
c |     20209 |   27982    66078 |   22251   14309   525247    36.7 |  2.352 % |
c |     24054 |   27982    66078 |   24477   18154   709742    39.1 |  2.352 % |
c |     29821 |   27982    66078 |   26924   23921   979047    40.9 |  2.352 % |
c |     38470 |   27982    66078 |   29617   18281   942688    51.6 |  2.352 % |
c |     51446 |   27982    66078 |   32579   14543   532995    36.6 |  2.352 % |
c ==============================================================================
c [1mFound solution: 1707[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54718 |   27990    66098 |    9330   17815   682114    38.3 |  2.352 % |
c |     54818 |   27990    66098 |   10263    9008   273155    30.3 |  2.362 % |
c |     54968 |   27990    66098 |   11289    9158   277050    30.3 |  2.362 % |
c |     55194 |   27990    66098 |   12418    9384   284593    30.3 |  2.362 % |
c |     55531 |   27990    66098 |   13660    9721   298549    30.7 |  2.362 % |
c |     56039 |   27990    66098 |   15026   10229   307407    30.1 |  2.362 % |
c |     56799 |   27990    66098 |   16528   10989   354163    32.2 |  2.362 % |
c ==============================================================================
c [1mFound solution: 1702[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56861 |   27995    66111 |    9331   11051   355510    32.2 |  2.362 % |
c |     56962 |   27995    66111 |   10264    5627   168821    30.0 |  2.372 % |
c |     57115 |   27995    66111 |   11290    5780   175026    30.3 |  2.372 % |
c |     57344 |   27995    66111 |   12419    6009   186681    31.1 |  2.372 % |
c |     57681 |   27995    66111 |   13661    6346   198044    31.2 |  2.372 % |
c |     58187 |   27995    66111 |   15027    6852   208602    30.4 |  2.372 % |
c |     58946 |   27995    66111 |   16530    7611   245388    32.2 |  2.372 % |
c |     60085 |   27995    66111 |   18183    8750   291127    33.3 |  2.372 % |
c |     61793 |   27995    66111 |   20001   10458   369340    35.3 |  2.372 % |
c |     64355 |   27995    66111 |   22002   13020   519347    39.9 |  2.372 % |
c |     68199 |   27995    66111 |   24202   16864   722372    42.8 |  2.373 % |
c |     73965 |   27995    66111 |   26622   22630  1055736    46.7 |  2.372 % |
c |     82614 |   27995    66111 |   29284   16344   697616    42.7 |  2.372 % |
c |     95589 |   27995    66111 |   32213   29319  1176006    40.1 |  2.372 % |
c |    115054 |   27995    66111 |   35434   29628  1170082    39.5 |  2.372 % |
c ==============================================================================
c [1mFound solution: 1700[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125669 |   28008    66146 |    9336   17780   635862    35.8 |  2.372 % |
c |    125771 |   28008    66146 |   10269    8992   307335    34.2 |  2.382 % |
c |    125921 |   27977    66078 |   11296    9115   309490    34.0 |  2.478 % |
c |    126147 |   27965    66052 |   12426    9335   313606    33.6 |  2.520 % |
c |    126484 |   27965    66052 |   13668    9672   317777    32.9 |  2.520 % |
c |    126990 |   27965    66052 |   15035   10178   338420    33.3 |  2.520 % |
c |    127749 |   27965    66052 |   16539   10937   359837    32.9 |  2.520 % |
c |    128888 |   27965    66052 |   18193   12076   389222    32.2 |  2.521 % |
c |    130596 |   27965    66052 |   20012   13784   450950    32.7 |  2.520 % |
c |    133158 |   27965    66052 |   22013   16346   549384    33.6 |  2.520 % |
c |    137002 |   27965    66052 |   24215   20190   717296    35.5 |  2.520 % |
c ==============================================================================
c [1mFound solution: 1699[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137873 |   27974    66075 |    9324   21061   746657    35.5 |  2.520 % |
c |    137973 |   27974    66075 |   10256    5366   138480    25.8 |  2.530 % |
c |    138125 |   27974    66075 |   11282    5518   142991    25.9 |  2.530 % |
c |    138351 |   27974    66075 |   12410    5744   152469    26.5 |  2.530 % |
c |    138689 |   27974    66075 |   13651    6082   171144    28.1 |  2.530 % |
c |    139196 |   27974    66075 |   15016    6589   187220    28.4 |  2.530 % |
c |    139955 |   27974    66075 |   16518    7348   202844    27.6 |  2.530 % |
c |    141095 |   27974    66075 |   18169    8488   248574    29.3 |  2.530 % |
c |    142806 |   27974    66075 |   19986   10199   308176    30.2 |  2.530 % |
c |    145371 |   27974    66075 |   21985   12764   419399    32.9 |  2.530 % |
c |    149216 |   27974    66075 |   24184   16609   660886    39.8 |  2.530 % |
c |    154984 |   27974    66075 |   26602   22377   866805    38.7 |  2.530 % |
c |    163634 |   27974    66075 |   29262   16776   571865    34.1 |  2.530 % |
c ==============================================================================
c [1mFound solution: 1696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173181 |   27982    66095 |    9327   26323   931345    35.4 |  2.530 % |
c ==============================================================================
c [1mFound solution: 1695[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    173261 |   27994    66125 |    9331    6661   149393    22.4 |  2.530 % |
c |    173361 |   27994    66125 |   10264    6761   152869    22.6 |  2.549 % |
c |    173514 |   27994    66125 |   11290    6914   159847    23.1 |  2.549 % |
c |    173739 |   27994    66125 |   12419    7139   163951    23.0 |  2.549 % |
c |    174080 |   27994    66125 |   13661    7480   175171    23.4 |  2.550 % |
c |    174588 |   27994    66125 |   15027    7988   190103    23.8 |  2.549 % |
c |    175347 |   27994    66125 |   16530    8747   222224    25.4 |  2.549 % |
c |    176486 |   27994    66125 |   18183    9886   272470    27.6 |  2.549 % |
c ==============================================================================
c [1mFound solution: 1686[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177041 |   27998    66135 |    9332   10441   294007    28.2 |  2.549 % |
c |    177143 |   27998    66135 |   10265    5323   130934    24.6 |  2.559 % |
c |    177293 |   27998    66135 |   11291    5473   136715    25.0 |  2.559 % |
c |    177519 |   27998    66135 |   12420    5699   140409    24.6 |  2.559 % |
c ==============================================================================
c [1mFound solution: 1665[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    177644 |   28007    66158 |    9335    5824   145715    25.0 |  2.559 % |
c |    177744 |   28007    66158 |   10268    5924   148963    25.1 |  2.569 % |
c |    177894 |   28007    66158 |   11295    6074   152091    25.0 |  2.569 % |
c |    178119 |   28007    66158 |   12424    6299   156406    24.8 |  2.569 % |
c |    178456 |   28007    66158 |   13667    6636   159953    24.1 |  2.569 % |
c |    178962 |   27882    65876 |   15034    7081   165429    23.4 |  2.907 % |
c |    179721 |   27882    65876 |   16537    7840   212069    27.0 |  2.907 % |
c |    180862 |   27882    65876 |   18191    8981   230250    25.6 |  2.907 % |
c |    182571 |   27882    65876 |   20010   10690   260201    24.3 |  2.907 % |
c |    185133 |   27882    65876 |   22011   13252   500257    37.7 |  2.907 % |
c |    188978 |   27882    65876 |   24212   17097   666974    39.0 |  2.907 % |
c |    194744 |   27882    65876 |   26633   22863   901935    39.4 |  2.907 % |
c |    203395 |   27882    65876 |   29297   17280   581331    33.6 |  2.907 % |
c |    216369 |   27882    65876 |   32226   30254  1110767    36.7 |  2.907 % |
c |    235830 |   27882    65876 |   35449   32044  1084277    33.8 |  2.907 % |
c |    265022 |   27882    65876 |   38994   20312   541266    26.6 |  2.907 % |
c |    308812 |   27882    65876 |   42894   39986  1381571    34.6 |  2.907 % |
c ==============================================================================
c [1mFound solution: 1660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    317737 |   27915    65961 |    9305   25068   823854    32.9 |  2.907 % |
c |    317839 |   27915    65961 |   10235    6369   212056    33.3 |  2.925 % |
c |    317990 |   27915    65961 |   11259    6520   216506    33.2 |  2.925 % |
c |    318215 |   27915    65961 |   12384    6745   225856    33.5 |  2.925 % |
c |    318552 |   27915    65961 |   13623    7082   237467    33.5 |  2.925 % |
c |    319058 |   27915    65961 |   14985    7588   261188    34.4 |  2.925 % |
c |    319820 |   27915    65961 |   16484    8350   284580    34.1 |  2.925 % |
c |    320960 |   27915    65961 |   18132    9490   322098    33.9 |  2.925 % |
c |    322668 |   27915    65961 |   19946   11198   389861    34.8 |  2.925 % |
c |    325230 |   27915    65961 |   21940   13760   495701    36.0 |  2.925 % |
c |    329074 |   27829    65767 |   24134   16865   652477    38.7 |  3.178 % |
c |    334840 |   27829    65767 |   26548   22631   928350    41.0 |  3.178 % |
c |    343490 |   27829    65767 |   29203   16099   673163    41.8 |  3.178 % |
c ==============================================================================
c [1mFound solution: 1657[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    343833 |   27842    65800 |    9280   16442   688178    41.9 |  3.178 % |
c |    343933 |   27842    65800 |   10208    8321   288725    34.7 |  3.187 % |
c |    344083 |   27842    65800 |   11228    8471   293592    34.7 |  3.187 % |
c |    344309 |   27842    65800 |   12351    8697   301652    34.7 |  3.187 % |
c |    344647 |   27842    65800 |   13586    9035   313795    34.7 |  3.187 % |
c |    345154 |   27842    65800 |   14945    9542   326479    34.2 |  3.187 % |
c |    345913 |   27842    65800 |   16440   10301   360905    35.0 |  3.187 % |
c |    347052 |   27842    65800 |   18084   11440   412224    36.0 |  3.187 % |
c |    348760 |   27842    65800 |   19892   13148   507732    38.6 |  3.187 % |
c |    351325 |   27842    65800 |   21881   15713   623365    39.7 |  3.187 % |
c |    355169 |   27842    65800 |   24069   19557   784947    40.1 |  3.187 % |
c |    360935 |   27842    65800 |   26476   25323   990123    39.1 |  3.187 % |
c |    369584 |   27842    65800 |   29124   19541   624987    32.0 |  3.187 % |
c |    382559 |   27842    65800 |   32037   16532   491652    29.7 |  3.187 % |
c |    402020 |   27842    65800 |   35240   18173   564065    31.0 |  3.187 % |
c |    431212 |   27759    65606 |   38764   26205   760214    29.0 |  3.398 % |
#### 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/54 1794
Raw data (stat): 1794 (runsolver) D 1793 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 409891520 1052672 99 4294967295 134512640 135381576 3221224480 3221219724 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 1405 0 0 0 995 3 0 0 25 0 1 0 409891520 7577600 1365 4294967295 134512640 134672761 3221224576 3221223744 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1850 1365 603 41 0 1809 0
vsize: 7400
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 1738 0 0 0 1993 4 0 0 25 0 1 0 409891520 8933376 1698 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1698 603 41 0 2140 0
vsize: 8724
[startup+30.0019 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 1738 0 0 0 2992 4 0 0 25 0 1 0 409891520 8933376 1698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2181 1698 603 41 0 2140 0
vsize: 8724
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 1861 0 0 0 3991 5 0 0 25 0 1 0 409891520 9461760 1821 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2310 1821 603 41 0 2269 0
vsize: 9240
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2088 0 0 0 4990 5 0 0 25 0 1 0 409891520 10452992 2048 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2552 2048 603 41 0 2511 0
vsize: 10208
[startup+60.002 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2306 0 0 0 5990 6 0 0 25 0 1 0 409891520 11382784 2266 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2779 2266 603 41 0 2738 0
vsize: 11116
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2506 0 0 0 6989 7 0 0 25 0 1 0 409891520 12177408 2466 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2973 2466 603 41 0 2932 0
vsize: 11892
[startup+80.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2579 0 0 0 7989 7 0 0 25 0 1 0 409891520 12439552 2539 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3037 2539 603 41 0 2996 0
vsize: 12148
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2579 0 0 0 8989 7 0 0 25 0 1 0 409891520 12439552 2539 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3037 2539 603 41 0 2996 0
vsize: 12148
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2656 0 0 0 9989 7 0 0 25 0 1 0 409891520 12709888 2616 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3103 2616 603 41 0 3062 0
vsize: 12412
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 2849 0 0 0 10988 8 0 0 25 0 1 0 409891520 13500416 2809 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3296 2809 603 41 0 3255 0
vsize: 13184
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3039 0 0 0 11988 9 0 0 25 0 1 0 409891520 14299136 2999 4294967295 134512640 134672761 3221224576 3221223712 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3491 2999 603 41 0 3450 0
vsize: 13964
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3054 0 0 0 12988 9 0 0 25 0 1 0 409891520 14385152 3014 4294967295 134512640 134672761 3221224576 3221223712 134560645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3512 3014 603 41 0 3471 0
vsize: 14048
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3054 0 0 0 13988 9 0 0 25 0 1 0 409891520 14381056 3014 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3014 603 41 0 3470 0
vsize: 14044
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3054 0 0 0 14988 9 0 0 25 0 1 0 409891520 14381056 3014 4294967295 134512640 134672761 3221224576 3221223792 134557665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3014 603 41 0 3470 0
vsize: 14044
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 15988 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 16988 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 17988 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 18989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 19989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223680 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+210.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 20989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+220.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 21989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+230.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 22989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3055 0 0 0 23989 9 0 0 25 0 1 0 409891520 14381056 3015 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3015 603 41 0 3470 0
vsize: 14044
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3056 0 0 0 24990 9 0 0 25 0 1 0 409891520 14381056 3016 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3511 3016 603 41 0 3470 0
vsize: 14044
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3124 0 0 0 25989 9 0 0 25 0 1 0 409891520 14774272 3084 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3607 3084 603 41 0 3566 0
vsize: 14428
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3128 0 0 0 26990 9 0 0 25 0 1 0 409891520 14774272 3088 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3607 3088 603 41 0 3566 0
vsize: 14428
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3128 0 0 0 27990 9 0 0 25 0 1 0 409891520 14774272 3088 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3607 3088 603 41 0 3566 0
vsize: 14428
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3133 0 0 0 28990 9 0 0 25 0 1 0 409891520 14909440 3093 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3640 3093 603 41 0 3599 0
vsize: 14560
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3155 0 0 0 29990 9 0 0 25 0 1 0 409891520 14909440 3115 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3640 3115 603 41 0 3599 0
vsize: 14560
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3172 0 0 0 30990 9 0 0 25 0 1 0 409891520 15048704 3132 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3674 3132 603 41 0 3633 0
vsize: 14696
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3269 0 0 0 31990 10 0 0 25 0 1 0 409891520 15441920 3229 4294967295 134512640 134672761 3221224576 3221223680 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3229 603 41 0 3729 0
vsize: 15080
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 32990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 33989 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 34989 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 35990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223680 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 36990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 37990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 38990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223680 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 39990 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223712 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 40991 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 41991 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 42991 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3284 0 0 0 43991 10 0 0 25 0 1 0 409891520 15441920 3244 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3244 603 41 0 3729 0
vsize: 15080
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 44991 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 45991 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 46992 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 47992 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 48992 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223680 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 49992 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 50993 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 51993 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 52993 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 53993 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 54994 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3285 0 0 0 55994 10 0 0 25 0 1 0 409891520 15441920 3245 4294967295 134512640 134672761 3221224576 3221223760 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3770 3245 603 41 0 3729 0
vsize: 15080
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3298 0 0 0 56994 10 0 0 25 0 1 0 409891520 15572992 3258 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3258 603 41 0 3761 0
vsize: 15208
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3300 0 0 0 57994 10 0 0 25 0 1 0 409891520 15572992 3260 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3260 603 41 0 3761 0
vsize: 15208
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3303 0 0 0 58994 10 0 0 25 0 1 0 409891520 15572992 3263 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3263 603 41 0 3761 0
vsize: 15208
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3313 0 0 0 59994 10 0 0 25 0 1 0 409891520 15572992 3273 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3802 3273 603 41 0 3761 0
vsize: 15208
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3322 0 0 0 60995 10 0 0 25 0 1 0 409891520 15720448 3282 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3282 603 41 0 3797 0
vsize: 15352
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3341 0 0 0 61995 10 0 0 25 0 1 0 409891520 15720448 3301 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3838 3301 603 41 0 3797 0
vsize: 15352
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3367 0 0 0 62995 10 0 0 25 0 1 0 409891520 15851520 3327 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3870 3327 603 41 0 3829 0
vsize: 15480
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3402 0 0 0 63995 10 0 0 25 0 1 0 409891520 15982592 3362 4294967295 134512640 134672761 3221224576 3221223680 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3902 3362 603 41 0 3861 0
vsize: 15608
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3410 0 0 0 64995 10 0 0 25 0 1 0 409891520 15982592 3370 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3902 3370 603 41 0 3861 0
vsize: 15608
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3414 0 0 0 65995 10 0 0 25 0 1 0 409891520 15982592 3374 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3902 3374 603 41 0 3861 0
vsize: 15608
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3416 0 0 0 66996 10 0 0 25 0 1 0 409891520 16121856 3376 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3376 603 41 0 3895 0
vsize: 15744
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3422 0 0 0 67996 10 0 0 25 0 1 0 409891520 16121856 3382 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3382 603 41 0 3895 0
vsize: 15744
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3427 0 0 0 68996 10 0 0 25 0 1 0 409891520 16121856 3387 4294967295 134512640 134672761 3221224576 3221223680 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3387 603 41 0 3895 0
vsize: 15744
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3427 0 0 0 69996 10 0 0 25 0 1 0 409891520 16121856 3387 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3387 603 41 0 3895 0
vsize: 15744
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3437 0 0 0 70996 10 0 0 25 0 1 0 409891520 16121856 3397 4294967295 134512640 134672761 3221224576 3221223776 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3397 603 41 0 3895 0
vsize: 15744
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3441 0 0 0 71997 10 0 0 25 0 1 0 409891520 16121856 3401 4294967295 134512640 134672761 3221224576 3221223744 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3936 3401 603 41 0 3895 0
vsize: 15744
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3447 0 0 0 72997 10 0 0 25 0 1 0 409891520 16277504 3407 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3407 603 41 0 3933 0
vsize: 15896
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3447 0 0 0 73997 10 0 0 25 0 1 0 409891520 16277504 3407 4294967295 134512640 134672761 3221224576 3221223744 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3407 603 41 0 3933 0
vsize: 15896
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3447 0 0 0 74997 10 0 0 25 0 1 0 409891520 16277504 3407 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3407 603 41 0 3933 0
vsize: 15896
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3448 0 0 0 75997 10 0 0 25 0 1 0 409891520 16277504 3408 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3408 603 41 0 3933 0
vsize: 15896
[startup+770.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3474 0 0 0 76997 11 0 0 25 0 1 0 409891520 16277504 3434 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3974 3434 603 41 0 3933 0
vsize: 15896
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3512 0 0 0 77998 11 0 0 25 0 1 0 409891520 16408576 3472 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3472 603 41 0 3965 0
vsize: 16024
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3513 0 0 0 78998 11 0 0 25 0 1 0 409891520 16408576 3473 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3473 603 41 0 3965 0
vsize: 16024
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3513 0 0 0 79998 11 0 0 25 0 1 0 409891520 16408576 3473 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3473 603 41 0 3965 0
vsize: 16024
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3513 0 0 0 80998 11 0 0 25 0 1 0 409891520 16408576 3473 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3473 603 41 0 3965 0
vsize: 16024
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3514 0 0 0 81998 11 0 0 25 0 1 0 409891520 16408576 3474 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3474 603 41 0 3965 0
vsize: 16024
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3517 0 0 0 82998 11 0 0 25 0 1 0 409891520 16408576 3477 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4006 3477 603 41 0 3965 0
vsize: 16024
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3522 0 0 0 83999 11 0 0 25 0 1 0 409891520 16547840 3482 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4040 3482 603 41 0 3999 0
vsize: 16160
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3618 0 0 0 84998 12 0 0 25 0 1 0 409891520 16949248 3578 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4138 3578 603 41 0 4097 0
vsize: 16552
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3703 0 0 0 85997 12 0 0 25 0 1 0 409891520 17235968 3663 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4208 3663 603 41 0 4167 0
vsize: 16832
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3722 0 0 0 86997 12 0 0 25 0 1 0 409891520 17367040 3682 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3682 603 41 0 4199 0
vsize: 16960
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 87998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 88998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 89998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 90998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 91998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 92998 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+940.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 93999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 94999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223752 134553585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 95999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 96999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 97999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 98999 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 100000 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 101000 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 102000 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 103000 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 104000 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 105001 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 106001 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 107001 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134555314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 108001 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 109002 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223736 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 110002 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 111002 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 112002 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3737 0 0 0 113002 12 0 0 25 0 1 0 409891520 17367040 3697 4294967295 134512640 134672761 3221224576 3221223712 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3697 603 41 0 4199 0
vsize: 16960
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3738 0 0 0 114002 12 0 0 25 0 1 0 409891520 17367040 3698 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3698 603 41 0 4199 0
vsize: 16960
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3738 0 0 0 115003 12 0 0 25 0 1 0 409891520 17367040 3698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3698 603 41 0 4199 0
vsize: 16960
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3738 0 0 0 116003 12 0 0 25 0 1 0 409891520 17367040 3698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3698 603 41 0 4199 0
vsize: 16960
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3738 0 0 0 117003 12 0 0 25 0 1 0 409891520 17367040 3698 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3698 603 41 0 4199 0
vsize: 16960
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3738 0 0 0 118003 12 0 0 25 0 1 0 409891520 17367040 3698 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3698 603 41 0 4199 0
vsize: 16960
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3739 0 0 0 119003 12 0 0 25 0 1 0 409891520 17367040 3699 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3699 603 41 0 4199 0
vsize: 16960
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1794
Raw data (stat): 1794 (minisat+) R 1793 26667 26666 0 -1 0 3739 0 0 0 120004 12 0 0 25 0 1 0 409891520 17367040 3699 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4240 3699 603 41 0 4199 0
vsize: 16960
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1794
Raw data (stat): 1794 (minisat+) Z 1793 26667 26666 0 -1 12 3742 0 0 0 120004 13 0 0 25 0 1 0 409891520 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.05
CPU time (s): 1200.18
CPU user time (s): 1200.04
CPU system time (s): 0.135979
CPU usage (%): 100.011
Max. virtual memory (Kb): 16960
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####