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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0291.opb
MD5SUM	1d9168a9335e29df835d07b0bdf2adea
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10447498
Optimality of the best value was proved	NO
Number of terms in the objective function	289
Biggest coefficient in the objective function	80000000
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	686518451
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	80000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	686518451
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.333948
Number of variables	291
Total number of constraints	543
Number of constraints which are clauses	189
Number of constraints which are cardinality constraints (but not clauses)	295
Number of constraints which are nor clauses,nor cardinality constraints	59
Minimum length of a constraint	1
Maximum length of a constraint	53
Trace number 15603

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 05:10:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17139 boxname=wulflinc27 idbench=1319 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  1d9168a9335e29df835d07b0bdf2adea  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-p0291.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-p0291.opb
IDLAUNCH: 17139
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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	: 3
cpu MHz		: 451.169
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:        813192 kB
Buffers:         24660 kB
Cached:         168332 kB
SwapCached:        604 kB
Active:          31004 kB
Inactive:       164056 kB
HighTotal:      131008 kB
HighFree:        15932 kB
LowTotal:       903652 kB
LowFree:        797260 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5236 kB
Slab:            20752 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:31:01 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 17139 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[  14]---> Sorter-cost: 1503     Base: 2 2 5 2 3
c ---[  13]---> Sorter-cost: 1241     Base: 2 2 5 2 3
c ---[  11]---> BDD-cost:   52
c ---[  10]---> BDD-cost:   52
c ---[   9]---> BDD-cost:   52
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:    8
c ---[   6]---> BDD-cost:   16
c ---[   5]---> BDD-cost:   28
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   86
c ---[   2]---> Sorter-cost:  749     Base: 2 5 2 2
c ---[   1]---> Sorter-cost:  880     Base: 2 2 5 3
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10113    23793 |    3371       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 372252078[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:118480     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        34 |  349617   816479 |  116539      30      135     4.5 |  0.000 % |
c |       136 |  349617   816479 |  128192     132     7265    55.0 |  0.057 % |
c |       286 |  349498   816213 |  141012     277     9530    34.4 |  0.083 % |
c |       511 |  349437   816074 |  155113     501    15435    30.8 |  0.097 % |
c ==============================================================================
c [1mFound solution: 343257499[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   22     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       751 |  350888   820068 |  116962     740    17165    23.2 |  0.097 % |
c ==============================================================================
c [1mFound solution: 129653021[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       797 |  351215   821187 |  117071     786    18015    22.9 |  0.097 % |
c ==============================================================================
c [1mFound solution: 96610461[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       816 |  351238   821329 |  117079     805    18273    22.7 |  0.097 % |
c |       916 |  351238   821329 |  128786     905    18809    20.8 |  0.100 % |
c |      1066 |  351071   820956 |  141665    1053    21633    20.5 |  0.136 % |
c |      1291 |  351071   820956 |  155832    1278    29913    23.4 |  0.136 % |
c |      1628 |  351051   820911 |  171415    1614    40393    25.0 |  0.140 % |
c |      2136 |  350472   819603 |  188556    2071    47282    22.8 |  0.273 % |
c ==============================================================================
c [1mFound solution: 89231177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:80217     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2521 |  575673  1345522 |  191891    2451    84434    34.4 |  0.273 % |
c |      2621 |  575673  1345522 |  211080    2551    85722    33.6 |  0.272 % |
c |      2776 |  575673  1345522 |  232188    2706    90445    33.4 |  0.272 % |
c |      3001 |  575549  1345244 |  255406    2927    93583    32.0 |  0.290 % |
c |      3338 |  575473  1345071 |  280947    3261    95116    29.2 |  0.300 % |
c |      3845 |  575473  1345071 |  309042    3768   101931    27.1 |  0.300 % |
c |      4604 |  575375  1344846 |  339946    4523   107038    23.7 |  0.316 % |
c ==============================================================================
c [1mFound solution: 88982784[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4884 |  576502  1348290 |  192167    4802   115045    24.0 |  0.316 % |
c |      4986 |  576502  1348290 |  211383    4904   115953    23.6 |  0.319 % |
c |      5136 |  576502  1348290 |  232522    5054   116718    23.1 |  0.319 % |
c |      5361 |  576502  1348290 |  255774    5279   118823    22.5 |  0.319 % |
c |      5698 |  576502  1348290 |  281351    5616   122115    21.7 |  0.319 % |
c |      6204 |  576460  1348196 |  309486    6119   161620    26.4 |  0.326 % |
c |      6964 |  576282  1347795 |  340435    6865   171325    25.0 |  0.350 % |
c |      8103 |  575376  1345748 |  374479    7995   184812    23.1 |  0.479 % |
c ==============================================================================
c [1mFound solution: 88982623[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8416 |  575333  1345903 |  191777    8306   194111    23.4 |  0.479 % |
c |      8517 |  575311  1345856 |  210954    8406   194613    23.2 |  0.491 % |
c |      8670 |  575311  1345856 |  232050    8559   195622    22.9 |  0.491 % |
c |      8895 |  575140  1345466 |  255255    8781   197098    22.4 |  0.516 % |
c |      9232 |  575140  1345466 |  280780    9118   199574    21.9 |  0.516 % |
c |      9738 |  575140  1345466 |  308858    9624   232895    24.2 |  0.516 % |
c |     10498 |  575021  1345200 |  339744   10383   245465    23.6 |  0.532 % |
c |     11637 |  575013  1345182 |  373719   11521   253331    22.0 |  0.533 % |
c ==============================================================================
c [1mFound solution: 87532076[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12421 |  575477  1346314 |  191825   12305   263672    21.4 |  0.533 % |
c |     12522 |  575477  1346314 |  211007   12406   264059    21.3 |  0.534 % |
c |     12672 |  575477  1346314 |  232108   12556   267133    21.3 |  0.534 % |
c |     12897 |  575204  1345699 |  255319   12774   269710    21.1 |  0.570 % |
c |     13234 |  575083  1345425 |  280850   13094   276905    21.1 |  0.588 % |
c ==============================================================================
c [1mFound solution: 87531855[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   24     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13670 |  575101  1345470 |  191700   13529   283766    21.0 |  0.588 % |
c |     13770 |  575101  1345470 |  210870   13629   287057    21.1 |  0.590 % |
c |     13920 |  574872  1344953 |  231957   13774   288404    20.9 |  0.623 % |
c |     14146 |  574706  1344575 |  255152   13999   290366    20.7 |  0.647 % |
c |     14483 |  574449  1343991 |  280667   14331   292857    20.4 |  0.685 % |
c |     14990 |  574449  1343991 |  308734   14838   361561    24.4 |  0.685 % |
c |     15749 |  574396  1343873 |  339608   15594   429877    27.6 |  0.692 % |
c |     16888 |  574392  1343865 |  373569   16732   508600    30.4 |  0.693 % |
c |     18598 |  574362  1343797 |  410925   18441   617992    33.5 |  0.697 % |
c |     21160 |  573765  1342438 |  452018   20985   768496    36.6 |  0.786 % |
c ==============================================================================
c [1mFound solution: 85113488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21465 |  573778  1342481 |  191259   21290   813012    38.2 |  0.786 % |
c |     21566 |  573732  1342378 |  210384   21390   816940    38.2 |  0.793 % |
c |     21719 |  573732  1342378 |  231423   21543   821851    38.1 |  0.793 % |
c |     21944 |  573322  1341449 |  254565   21633   822080    38.0 |  0.850 % |
c ==============================================================================
c [1mFound solution: 84006258[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22119 |  573378  1341602 |  191126   21808   825248    37.8 |  0.850 % |
c |     22219 |  573378  1341602 |  210238   21908   836031    38.2 |  0.851 % |
c |     22371 |  573378  1341602 |  231262   22060   837755    38.0 |  0.851 % |
c |     22596 |  573328  1341488 |  254388   22284   838858    37.6 |  0.859 % |
c |     22933 |  573018  1340778 |  279827   22598   845717    37.4 |  0.906 % |
c |     23440 |  573018  1340778 |  307810   23105   849125    36.8 |  0.906 % |
c |     24199 |  573018  1340778 |  338591   23864   881359    36.9 |  0.906 % |
c |     25338 |  573018  1340778 |  372450   25003   905358    36.2 |  0.906 % |
c ==============================================================================
c [1mFound solution: 84002262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 2 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25976 |  572915  1340559 |  190971   25640   924715    36.1 |  0.906 % |
c |     26076 |  572915  1340559 |  210068   25740   928300    36.1 |  0.924 % |
c |     26226 |  572915  1340559 |  231074   25890   937919    36.2 |  0.924 % |
c |     26451 |  572915  1340559 |  254182   26115   946203    36.2 |  0.924 % |
c |     26788 |  572822  1340349 |  279600   26451   966819    36.6 |  0.937 % |
c |     27294 |  572822  1340349 |  307560   26957   994879    36.9 |  0.937 % |
c |     28054 |  572528  1339674 |  338316   27687  1018467    36.8 |  0.982 % |
c |     29195 |  572368  1339307 |  372148   28826  1030099    35.7 |  1.007 % |
c ==============================================================================
c [1mFound solution: 84001972[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:81240     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29900 |  799446  1869514 |  266482   29483  1108026    37.6 |  1.007 % |
c |     30000 |  799446  1869514 |  293130   29583  1114692    37.7 |  1.062 % |
c |     30150 |  799446  1869514 |  322443   29733  1115605    37.5 |  1.062 % |
c ==============================================================================
c [1mFound solution: 81508936[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30269 |  799348  1870290 |  266449   29839  1117910    37.5 |  1.062 % |
c ==============================================================================
c [1mFound solution: 67489773[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:51565     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30355 |  939340  2197364 |  313113   29881  1118957    37.4 |  1.062 % |
c ==============================================================================
c [1mFound solution: 67149523[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   23     Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30371 |  940245  2199831 |  313415   29897  1120138    37.5 |  1.062 % |
c |     30472 |  940245  2199831 |  344756   29998  1138786    38.0 |  1.319 % |
c |     30623 |  939332  2197757 |  379232   30126  1142694    37.9 |  1.403 % |
c |     30848 |  939240  2197552 |  417155   30349  1148829    37.9 |  1.410 % |
c |     31185 |  939240  2197552 |  458870   30686  1157226    37.7 |  1.410 % |
c |     31691 |  937130  2192769 |  504757   31156  1202270    38.6 |  1.595 % |
c ==============================================================================
c [1mFound solution: 37041654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:73486     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32144 |  877918  2061850 |  292639   22184   747496    33.7 |  1.595 % |
c |     32244 |  877274  2060361 |  321902   22256   748049    33.6 | 22.593 % |
c |     32394 |  877274  2060361 |  354093   22406   748904    33.4 | 22.593 % |
c |     32619 |  875160  2055459 |  389502   22605   751911    33.3 | 22.769 % |
c |     32957 |  875160  2055459 |  428452   22943   754947    32.9 | 22.769 % |
c |     33463 |  875160  2055459 |  471298   23449   759486    32.4 | 22.769 % |
c ==============================================================================
c [1mFound solution: 25632297[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:84242     Base: 2 5 2 2 2 2 2 2 3 3 3 3 2 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33536 | 1113500  2612117 |  371166   23522   761056    32.4 | 22.769 % |
c |     33640 | 1113500  2612117 |  408282   23626   771132    32.6 | 18.901 % |
c |     33790 | 1113500  2612117 |  449110   23776   780605    32.8 | 18.901 % |
c |     34015 | 1113500  2612117 |  494021   24001   788833    32.9 | 18.901 % |
c |     34352 | 1113319  2611712 |  543424   24336   791250    32.5 | 18.911 % |
c ==============================================================================
c [1mFound solution: 25626371[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:54299     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34525 |  984405  2315139 |  328135   17933   604626    33.7 | 18.911 % |
c |     34625 |  983858  2313874 |  360948   18032   608726    33.8 | 34.503 % |
c |     34775 |  983747  2313626 |  397043   18181   609784    33.5 | 34.509 % |
c |     35003 |  982856  2311564 |  436747   18356   616573    33.6 | 34.564 % |
c |     35340 |  982597  2310985 |  480422   18689   629132    33.7 | 34.577 % |
c |     35846 |  982597  2310985 |  528464   19195   638194    33.2 | 34.577 % |
c |     36605 |  982494  2310755 |  581311   19951   644925    32.3 | 34.583 % |
c ==============================================================================
c [1mFound solution: 22759117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37372 |  982661  2311606 |  327553   20715   661870    32.0 | 34.583 % |
c |     37472 |  982661  2311606 |  360308   20815   662447    31.8 | 34.578 % |
c |     37622 |  982530  2311300 |  396339   20963   663212    31.6 | 34.587 % |
c |     37847 |  982530  2311300 |  435973   21188   675196    31.9 | 34.587 % |
c ==============================================================================
c [1mFound solution: 14796233[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:39919     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38141 | 1085930  2553439 |  361976   20901   652137    31.2 | 34.587 % |
c |     38241 | 1085930  2553439 |  398173   21001   654482    31.2 | 32.663 % |
c |     38392 | 1085891  2553352 |  437990   21150   655308    31.0 | 32.666 % |
c |     38617 | 1085827  2553209 |  481790   21370   659881    30.9 | 32.668 % |
c ==============================================================================
c [1mFound solution: 14059303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38852 | 1086322  2554851 |  362107   21605   669705    31.0 | 32.668 % |
c |     38953 | 1086322  2554851 |  398317   21706   670709    30.9 | 32.652 % |
c ==============================================================================
c [1mFound solution: 13892366[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38996 | 1086632  2555667 |  362210   21749   673318    31.0 | 32.652 % |
c |     39096 | 1086529  2555436 |  398431   21847   675169    30.9 | 32.647 % |
c ==============================================================================
c [1mFound solution: 13556961[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39171 | 1086002  2554239 |  362000   21833   662053    30.3 | 32.647 % |
c ==============================================================================
c [1mFound solution: 13542933[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 3 3 2 2 3 2 3 3 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39202 | 1086018  2554284 |  362006   21864   662702    30.3 | 32.647 % |
#### 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.93 0.98 0.93 2/54 12459
Raw data (stat): 12459 (runsolver) R 12458 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542453144 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99999 s]
Raw data (loadavg): 0.94 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 897 0 0 0 997 2 0 0 25 0 1 0 542453144 4816896 750 4294967295 134512640 134672761 3221224624 3221221744 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1176 750 603 41 0 1135 0
vsize: 4704
[startup+20 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 897 0 0 0 1996 2 0 0 25 0 1 0 542453144 4816896 750 4294967295 134512640 134672761 3221224624 3221222320 134597225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1176 750 603 41 0 1135 0
vsize: 4704
[startup+30.0056 s]
Raw data (loadavg): 0.95 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 897 0 0 0 2996 3 0 0 25 0 1 0 542453144 4816896 750 4294967295 134512640 134672761 3221224624 3221222464 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1176 750 603 41 0 1135 0
vsize: 4704
[startup+40.0053 s]
Raw data (loadavg): 0.96 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 897 0 0 0 3996 3 0 0 25 0 1 0 542453144 4816896 750 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1176 750 603 41 0 1135 0
vsize: 4704
[startup+50.0068 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10160 0 0 0 4974 25 0 0 25 0 1 0 542453144 43065344 9695 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10514 9695 603 41 0 10473 0
vsize: 42056
[startup+60.0071 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10565 0 0 0 5973 26 0 0 25 0 1 0 542453144 44126208 9975 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9975 603 41 0 10732 0
vsize: 43092
[startup+70.0068 s]
Raw data (loadavg): 0.97 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10565 0 0 0 6974 26 0 0 25 0 1 0 542453144 44126208 9975 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9975 603 41 0 10732 0
vsize: 43092
[startup+80.0079 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10565 0 0 0 7973 26 0 0 25 0 1 0 542453144 44126208 9975 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9975 603 41 0 10732 0
vsize: 43092
[startup+90.0077 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10565 0 0 0 8973 26 0 0 25 0 1 0 542453144 44126208 9975 4294967295 134512640 134672761 3221224624 3221222032 134597221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9975 603 41 0 10732 0
vsize: 43092
[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10742 0 0 0 9972 27 0 0 25 0 1 0 542453144 44126208 10020 4294967295 134512640 134672761 3221224624 3221221888 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10020 603 41 0 10732 0
vsize: 43092
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10742 0 0 0 10972 28 0 0 25 0 1 0 542453144 44126208 10020 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10020 603 41 0 10732 0
vsize: 43092
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10742 0 0 0 11972 28 0 0 25 0 1 0 542453144 44126208 10020 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10020 603 41 0 10732 0
vsize: 43092
[startup+130.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10742 0 0 0 12972 28 0 0 25 0 1 0 542453144 44126208 10020 4294967295 134512640 134672761 3221224624 3221221744 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10020 603 41 0 10732 0
vsize: 43092
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10742 0 0 0 13972 29 0 0 25 0 1 0 542453144 44126208 10020 4294967295 134512640 134672761 3221224624 3221221248 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10020 603 41 0 10732 0
vsize: 43092
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10885 0 0 0 14971 29 0 0 25 0 1 0 542453144 44126208 10023 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10023 603 41 0 10732 0
vsize: 43092
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10885 0 0 0 15971 29 0 0 25 0 1 0 542453144 44126208 10023 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10023 603 41 0 10732 0
vsize: 43092
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10885 0 0 0 16971 30 0 0 25 0 1 0 542453144 44126208 10023 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10023 603 41 0 10732 0
vsize: 43092
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10885 0 0 0 17970 30 0 0 25 0 1 0 542453144 44126208 10023 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10023 603 41 0 10732 0
vsize: 43092
[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 10886 0 0 0 18970 30 0 0 25 0 1 0 542453144 44126208 10024 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 10024 603 41 0 10732 0
vsize: 43092
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 11137 0 0 0 19970 31 0 0 25 0 1 0 542453144 44408832 10092 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10842 10092 603 41 0 10801 0
vsize: 43368
[startup+210.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 11137 0 0 0 20969 32 0 0 25 0 1 0 542453144 44408832 10092 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10842 10092 603 41 0 10801 0
vsize: 43368
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 11137 0 0 0 21969 32 0 0 25 0 1 0 542453144 44408832 10092 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10842 10092 603 41 0 10801 0
vsize: 43368
[startup+230.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 11137 0 0 0 22969 32 0 0 25 0 1 0 542453144 44408832 10092 4294967295 134512640 134672761 3221224624 3221222896 134597203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10842 10092 603 41 0 10801 0
vsize: 43368
[startup+240.012 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 11137 0 0 0 23968 33 0 0 25 0 1 0 542453144 44408832 10092 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10842 10092 603 41 0 10801 0
vsize: 43368
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17487 0 0 0 24953 48 0 0 25 0 1 0 542453144 75223040 16112 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18365 16112 603 41 0 18324 0
vsize: 73460
[startup+260.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17932 0 0 0 25952 49 0 0 25 0 1 0 542453144 76288000 16432 4294967295 134512640 134672761 3221224624 3221222176 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18625 16432 603 41 0 18584 0
vsize: 74500
[startup+270.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17932 0 0 0 26952 49 0 0 25 0 1 0 542453144 76288000 16432 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18625 16432 603 41 0 18584 0
vsize: 74500
[startup+280.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17932 0 0 0 27952 50 0 0 25 0 1 0 542453144 76288000 16432 4294967295 134512640 134672761 3221224624 3221221744 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18625 16432 603 41 0 18584 0
vsize: 74500
[startup+290.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17932 0 0 0 28952 50 0 0 25 0 1 0 542453144 76288000 16432 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18625 16432 603 41 0 18584 0
vsize: 74500
[startup+300.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17947 0 0 0 29951 50 0 0 25 0 1 0 542453144 76402688 16447 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18653 16447 603 41 0 18612 0
vsize: 74612
[startup+310.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 17953 0 0 0 30951 51 0 0 25 0 1 0 542453144 76402688 16453 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18653 16453 603 41 0 18612 0
vsize: 74612
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18195 0 0 0 31950 52 0 0 25 0 1 0 542453144 76595200 16516 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18700 16516 603 41 0 18659 0
vsize: 74800
[startup+330.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18195 0 0 0 32950 52 0 0 25 0 1 0 542453144 76595200 16516 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18700 16516 603 41 0 18659 0
vsize: 74800
[startup+340.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18195 0 0 0 33950 52 0 0 25 0 1 0 542453144 76595200 16516 4294967295 134512640 134672761 3221224624 3221222176 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18700 16516 603 41 0 18659 0
vsize: 74800
[startup+350.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18195 0 0 0 34950 53 0 0 25 0 1 0 542453144 76595200 16516 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18700 16516 603 41 0 18659 0
vsize: 74800
[startup+360.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18198 0 0 0 35950 53 0 0 25 0 1 0 542453144 76595200 16516 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18700 16516 603 41 0 18659 0
vsize: 74800
[startup+370.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18259 0 0 0 36949 53 0 0 25 0 1 0 542453144 76857344 16577 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18764 16577 603 41 0 18723 0
vsize: 75056
[startup+380.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18477 0 0 0 37949 54 0 0 25 0 1 0 542453144 76972032 16612 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 16612 603 41 0 18751 0
vsize: 75168
[startup+390.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18477 0 0 0 38949 54 0 0 25 0 1 0 542453144 76972032 16612 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 16612 603 41 0 18751 0
vsize: 75168
[startup+400.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18477 0 0 0 39949 54 0 0 25 0 1 0 542453144 76972032 16612 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 16612 603 41 0 18751 0
vsize: 75168
[startup+410.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18477 0 0 0 40949 55 0 0 25 0 1 0 542453144 76972032 16612 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 16612 603 41 0 18751 0
vsize: 75168
[startup+420.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18484 0 0 0 41948 55 0 0 25 0 1 0 542453144 76972032 16615 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 16615 603 41 0 18751 0
vsize: 75168
[startup+430.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18700 0 0 0 42948 56 0 0 25 0 1 0 542453144 77119488 16651 4294967295 134512640 134672761 3221224624 3221222320 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 16651 603 41 0 18787 0
vsize: 75312
[startup+440.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18700 0 0 0 43948 56 0 0 25 0 1 0 542453144 77119488 16651 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 16651 603 41 0 18787 0
vsize: 75312
[startup+450.017 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18700 0 0 0 44947 56 0 0 25 0 1 0 542453144 77119488 16651 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 16651 603 41 0 18787 0
vsize: 75312
[startup+460.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18700 0 0 0 45948 56 0 0 25 0 1 0 542453144 77119488 16651 4294967295 134512640 134672761 3221224624 3221221888 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 16651 603 41 0 18787 0
vsize: 75312
[startup+470.018 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18705 0 0 0 46947 56 0 0 25 0 1 0 542453144 77119488 16652 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18828 16652 603 41 0 18787 0
vsize: 75312
[startup+480.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18720 0 0 0 47947 57 0 0 25 0 1 0 542453144 77250560 16667 4294967295 134512640 134672761 3221224624 3221223728 134559896 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18860 16667 603 41 0 18819 0
vsize: 75440
[startup+490.019 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 18855 0 0 0 48946 58 0 0 25 0 1 0 542453144 77791232 16802 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18992 16802 603 41 0 18951 0
vsize: 75968
[startup+500.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19023 0 0 0 49946 58 0 0 25 0 1 0 542453144 78495744 16970 4294967295 134512640 134672761 3221224624 3221223808 134558504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19164 16970 603 41 0 19123 0
vsize: 76656
[startup+510.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19096 0 0 0 50945 59 0 0 25 0 1 0 542453144 78766080 17043 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19230 17043 603 41 0 19189 0
vsize: 76920
[startup+520.02 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19140 0 0 0 51945 59 0 0 25 0 1 0 542453144 79032320 17087 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19295 17087 603 41 0 19254 0
vsize: 77180
[startup+530.021 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19180 0 0 0 52945 60 0 0 25 0 1 0 542453144 79167488 17127 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19328 17127 603 41 0 19287 0
vsize: 77312
[startup+540.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19246 0 0 0 53944 60 0 0 25 0 1 0 542453144 79433728 17193 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19393 17193 603 41 0 19352 0
vsize: 77572
[startup+550.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19466 0 0 0 54943 61 0 0 25 0 1 0 542453144 79863808 17288 4294967295 134512640 134672761 3221224624 3221222464 134597224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17288 603 41 0 19457 0
vsize: 77992
[startup+560.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19466 0 0 0 55943 61 0 0 25 0 1 0 542453144 79863808 17288 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17288 603 41 0 19457 0
vsize: 77992
[startup+570.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19466 0 0 0 56943 62 0 0 25 0 1 0 542453144 79863808 17288 4294967295 134512640 134672761 3221224624 3221222896 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17288 603 41 0 19457 0
vsize: 77992
[startup+580.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19466 0 0 0 57943 62 0 0 25 0 1 0 542453144 79863808 17288 4294967295 134512640 134672761 3221224624 3221222296 1075353074 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17288 603 41 0 19457 0
vsize: 77992
[startup+590.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19466 0 0 0 58943 62 0 0 25 0 1 0 542453144 79863808 17288 4294967295 134512640 134672761 3221224624 3221223796 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17288 603 41 0 19457 0
vsize: 77992
[startup+600.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19607 0 0 0 59942 62 0 0 25 0 1 0 542453144 79863808 17304 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17304 603 41 0 19457 0
vsize: 77992
[startup+610.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19607 0 0 0 60943 62 0 0 25 0 1 0 542453144 79863808 17304 4294967295 134512640 134672761 3221224624 3221222320 134597218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17304 603 41 0 19457 0
vsize: 77992
[startup+620.022 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19607 0 0 0 61942 63 0 0 25 0 1 0 542453144 79863808 17304 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17304 603 41 0 19457 0
vsize: 77992
[startup+630.023 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19607 0 0 0 62942 63 0 0 25 0 1 0 542453144 79863808 17304 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17304 603 41 0 19457 0
vsize: 77992
[startup+640.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19607 0 0 0 63942 63 0 0 25 0 1 0 542453144 79863808 17304 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17304 603 41 0 19457 0
vsize: 77992
[startup+650.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19608 0 0 0 64942 64 0 0 25 0 1 0 542453144 79863808 17305 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19498 17305 603 41 0 19457 0
vsize: 77992
[startup+660.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19851 0 0 0 65941 64 0 0 25 0 1 0 542453144 80068608 17366 4294967295 134512640 134672761 3221224624 3221221312 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17366 603 41 0 19507 0
vsize: 78192
[startup+670.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19851 0 0 0 66941 64 0 0 25 0 1 0 542453144 80068608 17366 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17366 603 41 0 19507 0
vsize: 78192
[startup+680.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19851 0 0 0 67941 65 0 0 25 0 1 0 542453144 80068608 17366 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17366 603 41 0 19507 0
vsize: 78192
[startup+690.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19851 0 0 0 68940 65 0 0 25 0 1 0 542453144 80068608 17366 4294967295 134512640 134672761 3221224624 3221222896 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17366 603 41 0 19507 0
vsize: 78192
[startup+700.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19851 0 0 0 69940 65 0 0 25 0 1 0 542453144 80068608 17366 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17366 603 41 0 19507 0
vsize: 78192
[startup+710.025 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19856 0 0 0 70940 66 0 0 25 0 1 0 542453144 80068608 17367 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17367 603 41 0 19507 0
vsize: 78192
[startup+720.024 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19904 0 0 0 71940 66 0 0 25 0 1 0 542453144 80343040 17415 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19615 17415 603 41 0 19574 0
vsize: 78460
[startup+730.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 19957 0 0 0 72939 67 0 0 25 0 1 0 542453144 80478208 17468 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19648 17468 603 41 0 19607 0
vsize: 78592
[startup+740.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 20243 0 0 0 73938 68 0 0 25 0 1 0 542453144 80904192 17574 4294967295 134512640 134672761 3221224624 3221222320 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+750.026 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 20243 0 0 0 74938 68 0 0 25 0 1 0 542453144 80904192 17574 4294967295 134512640 134672761 3221224624 3221222464 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+760.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 20243 0 0 0 75939 68 0 0 25 0 1 0 542453144 80904192 17574 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+770.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 20243 0 0 0 76939 68 0 0 25 0 1 0 542453144 80904192 17574 4294967295 134512640 134672761 3221224624 3221221744 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+780.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26086 0 0 0 77926 81 0 0 25 0 1 0 542453144 119406592 23417 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29152 23417 603 41 0 29111 0
vsize: 116608
[startup+790.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26448 0 0 0 78925 82 0 0 25 0 1 0 542453144 120807424 23654 4294967295 134512640 134672761 3221224624 3221221856 134522368 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+800.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26448 0 0 0 79925 82 0 0 25 0 1 0 542453144 120807424 23654 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+810.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26448 0 0 0 80925 82 0 0 25 0 1 0 542453144 120807424 23654 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+820.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26448 0 0 0 81925 82 0 0 25 0 1 0 542453144 120807424 23654 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+830.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26452 0 0 0 82925 82 0 0 25 0 1 0 542453144 120807424 23658 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29494 23658 603 41 0 29453 0
vsize: 117976
[startup+840.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26609 0 0 0 83925 83 0 0 25 0 1 0 542453144 120913920 23686 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+850.027 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26609 0 0 0 84925 83 0 0 25 0 1 0 542453144 120913920 23686 4294967295 134512640 134672761 3221224624 3221221600 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+860.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26609 0 0 0 85925 83 0 0 25 0 1 0 542453144 120913920 23686 4294967295 134512640 134672761 3221224624 3221222896 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+870.028 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 26609 0 0 0 86925 83 0 0 25 0 1 0 542453144 120913920 23686 4294967295 134512640 134672761 3221224624 3221223040 134597176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+880.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31816 0 0 0 87914 94 0 0 25 0 1 0 542453144 134201344 28109 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+890.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31816 0 0 0 88915 94 0 0 25 0 1 0 542453144 134201344 28109 4294967295 134512640 134672761 3221224624 3221222464 134597257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+900.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31816 0 0 0 89915 94 0 0 25 0 1 0 542453144 134201344 28109 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+910.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31816 0 0 0 90915 94 0 0 25 0 1 0 542453144 134201344 28109 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+920.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31827 0 0 0 91915 94 0 0 25 0 1 0 542453144 134303744 28120 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32789 28120 603 41 0 32748 0
vsize: 131156
[startup+930.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31827 0 0 0 92915 94 0 0 25 0 1 0 542453144 134303744 28120 4294967295 134512640 134672761 3221224624 3221223776 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32789 28120 603 41 0 32748 0
vsize: 131156
[startup+940.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31828 0 0 0 93915 95 0 0 25 0 1 0 542453144 134303744 28121 4294967295 134512640 134672761 3221224624 3221223760 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32789 28121 603 41 0 32748 0
vsize: 131156
[startup+950.029 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 31911 0 0 0 94915 95 0 0 25 0 1 0 542453144 134692864 28204 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32884 28204 603 41 0 32843 0
vsize: 131536
[startup+960.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 32102 0 0 0 95915 95 0 0 25 0 1 0 542453144 134746112 28230 4294967295 134512640 134672761 3221224624 3221221888 134597008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+970.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 32102 0 0 0 96915 95 0 0 25 0 1 0 542453144 134746112 28230 4294967295 134512640 134672761 3221224624 3221222464 134597225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+980.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 32102 0 0 0 97915 96 0 0 25 0 1 0 542453144 134746112 28230 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+990.031 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 32102 0 0 0 98915 96 0 0 25 0 1 0 542453144 134746112 28230 4294967295 134512640 134672761 3221224624 3221222468 1075351081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 37289 0 0 0 99903 108 0 0 25 0 1 0 542453144 153944064 33417 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37584 33417 603 41 0 37543 0
vsize: 150336
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 37505 0 0 0 100902 109 0 0 25 0 1 0 542453144 153944064 33591 4294967295 134512640 134672761 3221224624 3221222032 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37584 33591 603 41 0 37543 0
vsize: 150336
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 37505 0 0 0 101902 109 0 0 25 0 1 0 542453144 153944064 33591 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37584 33591 603 41 0 37543 0
vsize: 150336
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 41625 0 0 0 102893 118 0 0 25 0 1 0 542453144 164777984 37711 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40229 37711 603 41 0 40188 0
vsize: 160916
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 41648 0 0 0 103893 118 0 0 25 0 1 0 542453144 164909056 37734 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40261 37734 603 41 0 40220 0
vsize: 161044
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 41895 0 0 0 104893 119 0 0 25 0 1 0 542453144 165003264 37935 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 37935 603 41 0 40243 0
vsize: 161136
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44337 0 0 0 105887 125 0 0 25 0 1 0 542453144 183701504 40377 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44849 40377 603 41 0 44808 0
vsize: 179396
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44348 0 0 0 106887 125 0 0 25 0 1 0 542453144 183701504 40388 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44849 40388 603 41 0 44808 0
vsize: 179396
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44373 0 0 0 107887 125 0 0 25 0 1 0 542453144 183701504 40413 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44849 40413 603 41 0 44808 0
vsize: 179396
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44585 0 0 0 108887 125 0 0 25 0 1 0 542453144 186097664 40583 4294967295 134512640 134672761 3221224624 3221222176 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45434 40583 603 41 0 45393 0
vsize: 181736
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44603 0 0 0 109887 126 0 0 25 0 1 0 542453144 186167296 40601 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45451 40601 603 41 0 45410 0
vsize: 181804
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44603 0 0 0 110887 126 0 0 25 0 1 0 542453144 186167296 40601 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45451 40601 603 41 0 45410 0
vsize: 181804
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 44663 0 0 0 111887 126 0 0 25 0 1 0 542453144 186167296 40615 4294967295 134512640 134672761 3221224624 3221222176 134597212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45451 40615 603 41 0 45410 0
vsize: 181804
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47106 0 0 0 112881 132 0 0 25 0 1 0 542453144 222318592 43058 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54277 43058 603 41 0 54236 0
vsize: 217108
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47111 0 0 0 113882 132 0 0 25 0 1 0 542453144 222318592 43063 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54277 43063 603 41 0 54236 0
vsize: 217108
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47320 0 0 0 114881 132 0 0 25 0 1 0 542453144 222625792 43230 4294967295 134512640 134672761 3221224624 3221222668 1075349820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54352 43230 603 41 0 54311 0
vsize: 217408
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47879 0 0 0 115881 133 0 0 25 0 1 0 542453144 222679040 43267 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54365 43267 603 41 0 54324 0
vsize: 217460
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47880 0 0 0 116881 133 0 0 25 0 1 0 542453144 222679040 43268 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54365 43268 603 41 0 54324 0
vsize: 217460
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47924 0 0 0 117881 133 0 0 25 0 1 0 542453144 222736384 43270 4294967295 134512640 134672761 3221224624 3221222176 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54379 43270 603 41 0 54338 0
vsize: 217516
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47966 0 0 0 118881 133 0 0 25 0 1 0 542453144 222736384 43270 4294967295 134512640 134672761 3221224624 3221222320 134597195 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54379 43270 603 41 0 54338 0
vsize: 217516
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.93 2/54 12459
Raw data (stat): 12459 (minisat+) R 12458 18865 18864 0 -1 0 47966 0 0 0 119881 134 0 0 25 0 1 0 542453144 222736384 43270 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54379 43270 603 41 0 54338 0
vsize: 217516
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.98 0.93 1/54 12459
Raw data (stat): 12459 (minisat+) Z 12458 18865 18864 0 -1 12 47969 0 0 0 119881 142 0 0 25 0 1 0 542453144 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.12
CPU time (s): 1200.24
CPU user time (s): 1198.81
CPU system time (s): 1.42678
CPU usage (%): 100.01
Max. virtual memory (Kb): 217516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####