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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.335948
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 22061

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-22 02:03:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12147 boxname=wulflinc30 idbench=935 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  1d9168a9335e29df835d07b0bdf2adea  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-p0291.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-p0291.opb
IDLAUNCH: 12147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        718048 kB
Buffers:         16660 kB
Cached:         274776 kB
SwapCached:        352 kB
Active:          23000 kB
Inactive:       271132 kB
HighTotal:      131008 kB
HighFree:        16464 kB
LowTotal:       903652 kB
LowFree:        701584 kB
SwapTotal:     2097892 kB
SwapFree:      2097328 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5980 kB
Slab:            16884 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:23:12 (client local time) WITH STATUS 10 IN 1200.28 SECONDS
stats: 12147 7 1200.28 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 % |
c |     39302 | 1086018  2554284 |  398206   21964   665743    30.3 | 32.675 % |
#### 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.92 0.98 0.91 2/54 1511
Raw data (stat): 1511 (runsolver) R 1510 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549967062 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 897 0 0 0 997 2 0 0 25 0 1 0 549967062 4816896 750 4294967295 134512640 134672761 3221224624 3221222608 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.0011 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 897 0 0 0 1997 2 0 0 25 0 1 0 549967062 4816896 750 4294967295 134512640 134672761 3221224624 3221222320 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+30.0022 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 897 0 0 0 2997 2 0 0 25 0 1 0 549967062 4816896 750 4294967295 134512640 134672761 3221224624 3221222032 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+40.002 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 897 0 0 0 3997 2 0 0 25 0 1 0 549967062 4816896 750 4294967295 134512640 134672761 3221224624 3221222464 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.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10160 0 0 0 4975 23 0 0 25 0 1 0 549967062 43065344 9695 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10514 9695 603 41 0 10473 0
vsize: 42056
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10565 0 0 0 5974 24 0 0 25 0 1 0 549967062 44126208 9975 4294967295 134512640 134672761 3221224624 3221222176 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.0034 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10565 0 0 0 6974 24 0 0 25 0 1 0 549967062 44126208 9975 4294967295 134512640 134672761 3221224624 3221222608 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.0039 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10565 0 0 0 7975 24 0 0 25 0 1 0 549967062 44126208 9975 4294967295 134512640 134672761 3221224624 3221223040 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.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10565 0 0 0 8975 24 0 0 25 0 1 0 549967062 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+100.004 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10742 0 0 0 9974 25 0 0 25 0 1 0 549967062 44126208 10020 4294967295 134512640 134672761 3221224624 3221221600 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10742 0 0 0 10974 25 0 0 25 0 1 0 549967062 44126208 10020 4294967295 134512640 134672761 3221224624 3221222320 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10742 0 0 0 11975 25 0 0 25 0 1 0 549967062 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10742 0 0 0 12975 25 0 0 25 0 1 0 549967062 44126208 10020 4294967295 134512640 134672761 3221224624 3221222896 134597197 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10742 0 0 0 13975 25 0 0 25 0 1 0 549967062 44126208 10020 4294967295 134512640 134672761 3221224624 3221221888 134544780 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1511
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10885 0 0 0 14975 25 0 0 25 0 1 0 549967062 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10885 0 0 0 15975 25 0 0 25 0 1 0 549967062 44126208 10023 4294967295 134512640 134672761 3221224624 3221222464 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10885 0 0 0 16975 25 0 0 25 0 1 0 549967062 44126208 10023 4294967295 134512640 134672761 3221224624 3221222464 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.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10885 0 0 0 17975 25 0 0 25 0 1 0 549967062 44126208 10023 4294967295 134512640 134672761 3221224624 3221222432 134522368 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 10886 0 0 0 18975 25 0 0 25 0 1 0 549967062 44126208 10024 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 11137 0 0 0 19975 26 0 0 25 0 1 0 549967062 44408832 10092 4294967295 134512640 134672761 3221224624 3221221568 134522380 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 11137 0 0 0 20975 26 0 0 25 0 1 0 549967062 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 11137 0 0 0 21975 26 0 0 25 0 1 0 549967062 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+230.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 11137 0 0 0 22975 26 0 0 25 0 1 0 549967062 44408832 10092 4294967295 134512640 134672761 3221224624 3221222176 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+240.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 11137 0 0 0 23975 26 0 0 25 0 1 0 549967062 44408832 10092 4294967295 134512640 134672761 3221224624 3221222176 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17487 0 0 0 24961 40 0 0 25 0 1 0 549967062 75223040 16112 4294967295 134512640 134672761 3221224624 3221223796 134556632 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17932 0 0 0 25960 41 0 0 25 0 1 0 549967062 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+270.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17932 0 0 0 26960 41 0 0 25 0 1 0 549967062 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.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17932 0 0 0 27961 41 0 0 25 0 1 0 549967062 76288000 16432 4294967295 134512640 134672761 3221224624 3221221744 134597191 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.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17932 0 0 0 28961 41 0 0 25 0 1 0 549967062 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+300.006 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17947 0 0 0 29961 41 0 0 25 0 1 0 549967062 76402688 16447 4294967295 134512640 134672761 3221224624 3221223768 134560630 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 17953 0 0 0 30961 41 0 0 25 0 1 0 549967062 76402688 16453 4294967295 134512640 134672761 3221224624 3221223796 134556634 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18195 0 0 0 31961 42 0 0 25 0 1 0 549967062 76595200 16516 4294967295 134512640 134672761 3221224624 3221222032 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18195 0 0 0 32961 42 0 0 25 0 1 0 549967062 76595200 16516 4294967295 134512640 134672761 3221224624 3221222032 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18195 0 0 0 33961 42 0 0 25 0 1 0 549967062 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18195 0 0 0 34961 42 0 0 25 0 1 0 549967062 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18198 0 0 0 35961 42 0 0 25 0 1 0 549967062 76595200 16516 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18259 0 0 0 36961 42 0 0 25 0 1 0 549967062 76857344 16577 4294967295 134512640 134672761 3221224624 3221223824 134557842 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.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18477 0 0 0 37961 43 0 0 25 0 1 0 549967062 76972032 16612 4294967295 134512640 134672761 3221224624 3221222608 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18477 0 0 0 38961 43 0 0 25 0 1 0 549967062 76972032 16612 4294967295 134512640 134672761 3221224624 3221222320 134597224 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18477 0 0 0 39961 43 0 0 25 0 1 0 549967062 76972032 16612 4294967295 134512640 134672761 3221224624 3221221888 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18477 0 0 0 40961 43 0 0 25 0 1 0 549967062 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+420.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18484 0 0 0 41961 43 0 0 25 0 1 0 549967062 76972032 16615 4294967295 134512640 134672761 3221224624 3221223760 134560688 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18700 0 0 0 42961 43 0 0 25 0 1 0 549967062 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+440.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18700 0 0 0 43961 43 0 0 25 0 1 0 549967062 77119488 16651 4294967295 134512640 134672761 3221224624 3221222320 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18700 0 0 0 44961 43 0 0 25 0 1 0 549967062 77119488 16651 4294967295 134512640 134672761 3221224624 3221222608 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18700 0 0 0 45961 43 0 0 25 0 1 0 549967062 77119488 16651 4294967295 134512640 134672761 3221224624 3221222032 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+470.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18705 0 0 0 46961 44 0 0 25 0 1 0 549967062 77119488 16652 4294967295 134512640 134672761 3221224624 3221223796 134556688 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.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18721 0 0 0 47961 44 0 0 25 0 1 0 549967062 77250560 16668 4294967295 134512640 134672761 3221224624 3221223728 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18860 16668 603 41 0 18819 0
vsize: 75440
[startup+490.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 18861 0 0 0 48961 44 0 0 25 0 1 0 549967062 77791232 16808 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18992 16808 603 41 0 18951 0
vsize: 75968
[startup+500.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19029 0 0 0 49960 45 0 0 25 0 1 0 549967062 78495744 16976 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19164 16976 603 41 0 19123 0
vsize: 76656
[startup+510.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19097 0 0 0 50960 45 0 0 25 0 1 0 549967062 78766080 17044 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19230 17044 603 41 0 19189 0
vsize: 76920
[startup+520.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19140 0 0 0 51960 45 0 0 25 0 1 0 549967062 79032320 17087 4294967295 134512640 134672761 3221224624 3221223760 134560557 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19183 0 0 0 52960 46 0 0 25 0 1 0 549967062 79167488 17130 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19328 17130 603 41 0 19287 0
vsize: 77312
[startup+540.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19246 0 0 0 53960 46 0 0 25 0 1 0 549967062 79433728 17193 4294967295 134512640 134672761 3221224624 3221223792 134560898 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.009 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19466 0 0 0 54959 47 0 0 25 0 1 0 549967062 79863808 17288 4294967295 134512640 134672761 3221224624 3221221600 134597184 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19466 0 0 0 55959 47 0 0 25 0 1 0 549967062 79863808 17288 4294967295 134512640 134672761 3221224624 3221222148 1075351265 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19466 0 0 0 56960 47 0 0 25 0 1 0 549967062 79863808 17288 4294967295 134512640 134672761 3221224624 3221222752 134597184 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19466 0 0 0 57960 47 0 0 25 0 1 0 549967062 79863808 17288 4294967295 134512640 134672761 3221224624 3221222176 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+590.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19466 0 0 0 58960 47 0 0 25 0 1 0 549967062 79863808 17288 4294967295 134512640 134672761 3221224624 3221223824 134557842 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19607 0 0 0 59959 48 0 0 25 0 1 0 549967062 79863808 17304 4294967295 134512640 134672761 3221224624 3221222000 1075349698 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19607 0 0 0 60960 48 0 0 25 0 1 0 549967062 79863808 17304 4294967295 134512640 134672761 3221224624 3221222032 134597215 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19607 0 0 0 61960 48 0 0 25 0 1 0 549967062 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19607 0 0 0 62960 48 0 0 25 0 1 0 549967062 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+640.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19607 0 0 0 63960 48 0 0 25 0 1 0 549967062 79863808 17304 4294967295 134512640 134672761 3221224624 3221223760 134560588 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19608 0 0 0 64960 48 0 0 25 0 1 0 549967062 79863808 17305 4294967295 134512640 134672761 3221224624 3221223792 134560855 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19851 0 0 0 65960 48 0 0 25 0 1 0 549967062 80068608 17366 4294967295 134512640 134672761 3221224624 3221221744 134597212 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19851 0 0 0 66960 48 0 0 25 0 1 0 549967062 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+680.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19851 0 0 0 67960 48 0 0 25 0 1 0 549967062 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+690.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19851 0 0 0 68960 48 0 0 25 0 1 0 549967062 80068608 17366 4294967295 134512640 134672761 3221224624 3221222464 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.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19851 0 0 0 69960 48 0 0 25 0 1 0 549967062 80068608 17366 4294967295 134512640 134672761 3221224624 3221222608 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19856 0 0 0 70960 48 0 0 25 0 1 0 549967062 80068608 17367 4294967295 134512640 134672761 3221224624 3221223760 134560729 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19904 0 0 0 71961 48 0 0 25 0 1 0 549967062 80343040 17415 4294967295 134512640 134672761 3221224624 3221223792 134561375 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.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 19960 0 0 0 72961 49 0 0 25 0 1 0 549967062 80613376 17471 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19681 17472 603 41 0 19640 0
vsize: 78724
[startup+740.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 20243 0 0 0 73960 49 0 0 25 0 1 0 549967062 80904192 17574 4294967295 134512640 134672761 3221224624 3221221456 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+750.011 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 20243 0 0 0 74961 49 0 0 25 0 1 0 549967062 80904192 17574 4294967295 134512640 134672761 3221224624 3221223328 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+760.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 20243 0 0 0 75961 49 0 0 25 0 1 0 549967062 80904192 17574 4294967295 134512640 134672761 3221224624 3221223040 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+770.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 20243 0 0 0 76961 49 0 0 25 0 1 0 549967062 80904192 17574 4294967295 134512640 134672761 3221224624 3221222608 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19752 17574 603 41 0 19711 0
vsize: 79008
[startup+780.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26091 0 0 0 77948 63 0 0 25 0 1 0 549967062 119406592 23422 4294967295 134512640 134672761 3221224624 3221223768 1074754681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29152 23422 603 41 0 29111 0
vsize: 116608
[startup+790.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26448 0 0 0 78947 63 0 0 25 0 1 0 549967062 120807424 23654 4294967295 134512640 134672761 3221224624 3221222000 134522368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+800.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26448 0 0 0 79947 63 0 0 25 0 1 0 549967062 120807424 23654 4294967295 134512640 134672761 3221224624 3221223040 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+810.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26448 0 0 0 80947 64 0 0 25 0 1 0 549967062 120807424 23654 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+820.012 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26448 0 0 0 81947 64 0 0 25 0 1 0 549967062 120807424 23654 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29494 23654 603 41 0 29453 0
vsize: 117976
[startup+830.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26609 0 0 0 82947 64 0 0 25 0 1 0 549967062 120913920 23686 4294967295 134512640 134672761 3221224624 3221221568 134522369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+840.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26609 0 0 0 83947 64 0 0 25 0 1 0 549967062 120913920 23686 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+850.013 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26609 0 0 0 84947 64 0 0 25 0 1 0 549967062 120913920 23686 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+860.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 26609 0 0 0 85948 64 0 0 25 0 1 0 549967062 120913920 23686 4294967295 134512640 134672761 3221224624 3221221744 134597257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29520 23686 603 41 0 29479 0
vsize: 118080
[startup+870.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 30140 0 0 0 86940 72 0 0 25 0 1 0 549967062 131051520 27217 4294967295 134512640 134672761 3221224624 3221223924 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31995 27217 603 41 0 31954 0
vsize: 127980
[startup+880.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31816 0 0 0 87937 75 0 0 25 0 1 0 549967062 134201344 28109 4294967295 134512640 134672761 3221224624 3221221744 134597256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+890.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31816 0 0 0 88937 75 0 0 25 0 1 0 549967062 134201344 28109 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+900.014 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31816 0 0 0 89937 75 0 0 25 0 1 0 549967062 134201344 28109 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+910.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31816 0 0 0 90938 75 0 0 25 0 1 0 549967062 134201344 28109 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32764 28109 603 41 0 32723 0
vsize: 131056
[startup+920.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31827 0 0 0 91938 75 0 0 25 0 1 0 549967062 134303744 28120 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 28120 603 41 0 32748 0
vsize: 131156
[startup+930.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31827 0 0 0 92938 76 0 0 25 0 1 0 549967062 134303744 28120 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 28120 603 41 0 32748 0
vsize: 131156
[startup+940.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31845 0 0 0 93938 76 0 0 25 0 1 0 549967062 134303744 28138 4294967295 134512640 134672761 3221224624 3221223728 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32789 28138 603 41 0 32748 0
vsize: 131156
[startup+950.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 31911 0 0 0 94938 76 0 0 25 0 1 0 549967062 134692864 28204 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32884 28204 603 41 0 32843 0
vsize: 131536
[startup+960.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 32102 0 0 0 95938 76 0 0 25 0 1 0 549967062 134746112 28230 4294967295 134512640 134672761 3221224624 3221221744 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+970.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 32102 0 0 0 96938 76 0 0 25 0 1 0 549967062 134746112 28230 4294967295 134512640 134672761 3221224624 3221221888 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+980.022 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 32102 0 0 0 97938 76 0 0 25 0 1 0 549967062 134746112 28230 4294967295 134512640 134672761 3221224624 3221222320 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32897 28230 603 41 0 32856 0
vsize: 131588
[startup+990.023 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 37289 0 0 0 98926 88 0 0 25 0 1 0 549967062 153944064 33417 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37584 33417 603 41 0 37543 0
vsize: 150336
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 37289 0 0 0 99926 88 0 0 25 0 1 0 549967062 153944064 33417 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37584 33417 603 41 0 37543 0
vsize: 150336
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 37505 0 0 0 100926 89 0 0 25 0 1 0 549967062 153944064 33591 4294967295 134512640 134672761 3221224624 3221222752 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37584 33591 603 41 0 37543 0
vsize: 150336
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 37557 0 0 0 101926 89 0 0 25 0 1 0 549967062 153944064 33643 4294967295 134512640 134672761 3221224624 3221221488 134522987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37584 33644 603 41 0 37543 0
vsize: 150336
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 41636 0 0 0 102916 99 0 0 25 0 1 0 549967062 164909056 37722 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40261 37722 603 41 0 40220 0
vsize: 161044
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 41685 0 0 0 103916 99 0 0 25 0 1 0 549967062 164909056 37771 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40261 37771 603 41 0 40220 0
vsize: 161044
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 41895 0 0 0 104916 100 0 0 25 0 1 0 549967062 165003264 37935 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44341 0 0 0 105911 105 0 0 25 0 1 0 549967062 183701504 40381 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44849 40381 603 41 0 44808 0
vsize: 179396
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44359 0 0 0 106911 105 0 0 25 0 1 0 549967062 183701504 40399 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44849 40399 603 41 0 44808 0
vsize: 179396
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44382 0 0 0 107911 105 0 0 25 0 1 0 549967062 183836672 40422 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44882 40422 603 41 0 44841 0
vsize: 179528
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44585 0 0 0 108911 105 0 0 25 0 1 0 549967062 186097664 40583 4294967295 134512640 134672761 3221224624 3221222312 134597469 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44603 0 0 0 109911 105 0 0 25 0 1 0 549967062 186167296 40601 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 44603 0 0 0 110911 105 0 0 25 0 1 0 549967062 186167296 40601 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 46335 0 0 0 111908 109 0 0 25 0 1 0 549967062 219615232 42287 4294967295 134512640 134672761 3221224624 3221192160 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53617 42288 603 41 0 53576 0
vsize: 214468
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47106 0 0 0 112907 111 0 0 25 0 1 0 549967062 222318592 43058 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47320 0 0 0 113907 111 0 0 25 0 1 0 549967062 222625792 43230 4294967295 134512640 134672761 3221224624 3221222176 134597218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54352 43230 603 41 0 54311 0
vsize: 217408
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47820 0 0 0 114906 112 0 0 25 0 1 0 549967062 222662656 43250 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54361 43250 603 41 0 54320 0
vsize: 217444
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47879 0 0 0 115905 112 0 0 25 0 1 0 549967062 222679040 43267 4294967295 134512640 134672761 3221224624 3221222752 134597184 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47880 0 0 0 116906 112 0 0 25 0 1 0 549967062 222679040 43268 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54365 43268 603 41 0 54324 0
vsize: 217460
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47924 0 0 0 117906 113 0 0 25 0 1 0 549967062 222736384 43270 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54379 43270 603 41 0 54338 0
vsize: 217516
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47966 0 0 0 118905 113 0 0 25 0 1 0 549967062 222736384 43270 4294967295 134512640 134672761 3221224624 3221222576 134597446 0 0 5 16386 0 0 0 17 1 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.91 2/54 1513
Raw data (stat): 1511 (minisat+) R 1510 11931 11930 0 -1 0 47966 0 0 0 119905 113 0 0 25 0 1 0 549967062 222736384 43270 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 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.91 1/54 1513
Raw data (stat): 1511 (minisat+) Z 1510 11931 11930 0 -1 12 47969 0 0 0 119906 121 0 0 25 0 1 0 549967062 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.11
CPU time (s): 1200.28
CPU user time (s): 1199.06
CPU system time (s): 1.21981
CPU usage (%): 100.014
Max. virtual memory (Kb): 217516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####