number_of_models

('uf75-087.cnf', 375441, [31.487606048583984])
('uf75-025.cnf', 280262, [16.950977087020874])
('uf75-033.cnf', 176098, [31.1582989692688])
('uf75-093.cnf', 41503, [8.910184144973755])
('uf75-073.cnf', 37146, [8.198410987854004])
('uf75-068.cnf', 35202, [6.82702898979187])
('uf75-010.cnf', 30868, [6.246903896331787])
('uf75-077.cnf', 18135, [10.877649068832397])
('uf75-018.cnf', 15117, [3.866144895553589])
('uf75-089.cnf', 11038, [8.57466983795166])
('uf75-050.cnf', 10176, [6.29564905166626])
('uf75-09.cnf', 10077, [7.414304971694946])
('uf75-085.cnf', 9680, [8.864595890045166])
('uf75-098.cnf', 7456, [10.329029083251953])
('uf75-080.cnf', 5978, [14.61707592010498])
('uf75-022.cnf', 4654, [5.633204936981201])
('uf75-02.cnf', 4622, [8.591343879699707])
('uf75-066.cnf', 4522, [9.102866888046265])
('uf75-042.cnf', 4296, [3.0243899822235107])
('uf75-047.cnf', 3401, [4.367305040359497])
('uf75-094.cnf', 3304, [4.352187156677246])
('uf75-021.cnf', 3128, [3.7939629554748535])
('uf75-029.cnf', 2992, [7.590157985687256])
('uf75-070.cnf', 2688, [5.066082000732422])
('uf75-01.cnf', 2258, [4.620126962661743])
('uf75-092.cnf', 2256, [2.436767816543579])
('uf75-074.cnf', 2240, [6.948894023895264])
('uf75-013.cnf', 2219, [10.85535717010498])
('uf75-065.cnf', 2004, [5.864200115203857])
('uf75-017.cnf', 1861, [4.797636985778809])
('uf75-059.cnf', 1692, [3.1884429454803467])
('uf75-014.cnf', 1586, [5.299872875213623])
('uf75-075.cnf', 1514, [5.315432071685791])
('uf75-060.cnf', 1472, [3.8879270553588867])
('uf75-076.cnf', 968, [7.10009503364563])
('uf75-035.cnf', 916, [11.518132209777832])
('uf75-063.cnf', 880, [5.468733072280884])
('uf75-056.cnf', 828, [8.290796995162964])
('uf75-048.cnf', 798, [20.652014017105103])
('uf75-088.cnf', 776, [6.073352098464966])
('uf75-049.cnf', 728, [10.853317975997925])
('uf75-031.cnf', 664, [6.552318096160889])
('uf75-0100.cnf', 652, [11.162454843521118])
('uf75-053.cnf', 644, [6.2494800090789795])
('uf75-097.cnf', 640, [10.353069067001343])
('uf75-034.cnf', 562, [6.230988025665283])
('uf75-058.cnf', 524, [6.470828056335449])
('uf75-027.cnf', 520, [11.50084900856018])
('uf75-099.cnf', 478, [2.1776161193847656])
('uf75-072.cnf', 450, [4.2811119556427])
('uf75-039.cnf', 448, [7.381513833999634])
('uf75-082.cnf', 375, [6.031208038330078])
('uf75-054.cnf', 366, [6.3168699741363525])
('uf75-071.cnf', 365, [3.409031867980957])
('uf75-024.cnf', 304, [2.157097101211548])
('uf75-045.cnf', 295, [4.731722831726074])
('uf75-020.cnf', 288, [5.051242828369141])
('uf75-064.cnf', 283, [3.542635917663574])
('uf75-028.cnf', 272, [7.726073980331421])
('uf75-078.cnf', 248, [6.82859992980957])
('uf75-032.cnf', 230, [1.9444060325622559])
('uf75-086.cnf', 220, [4.2675628662109375])
('uf75-067.cnf', 216, [4.164247035980225])
('uf75-043.cnf', 210, [4.752334117889404])
('uf75-015.cnf', 200, [4.510005950927734])
('uf75-023.cnf', 199, [3.0608320236206055])
('uf75-095.cnf', 198, [2.9615349769592285])
('uf75-06.cnf', 176, [8.630571126937866])
('uf75-069.cnf', 158, [3.970021963119507])
('uf75-079.cnf', 157, [6.060765027999878])
('uf75-083.cnf', 155, [3.2878189086914062])
('uf75-08.cnf', 152, [17.865803956985474])
('uf75-081.cnf', 144, [2.50850510597229])
('uf75-026.cnf', 142, [15.550548076629639])
('uf75-096.cnf', 124, [8.87229299545288])
('uf75-037.cnf', 108, [3.5065770149230957])
('uf75-084.cnf', 108, [9.857846021652222])
('uf75-061.cnf', 100, [3.2033348083496094])
('uf75-036.cnf', 96, [2.8273251056671143])
('uf75-016.cnf', 80, [4.377415895462036])
('uf75-052.cnf', 74, [6.60699987411499])
('uf75-05.cnf', 72, [9.600340127944946])
('uf75-011.cnf', 62, [8.115244150161743])
('uf75-038.cnf', 48, [4.4993321895599365])
('uf75-057.cnf', 48, [2.6601080894470215])
('uf75-090.cnf', 36, [9.892068147659302])
('uf75-044.cnf', 32, [10.626938819885254])
('uf75-040.cnf', 30, [4.601324081420898])
('uf75-07.cnf', 27, [3.126336097717285])
('uf75-012.cnf', 24, [2.597991943359375])
('uf75-04.cnf', 24, [2.708256959915161])
('uf75-051.cnf', 24, [5.204690217971802])
('uf75-062.cnf', 20, [3.5536420345306396])
('uf75-019.cnf', 12, [6.915081977844238])
('uf75-041.cnf', 12, [5.953485012054443])
('uf75-055.cnf', 12, [1.7597410678863525])
('uf75-030.cnf', 10, [5.069978952407837])
('uf75-046.cnf', 8, [6.086397886276245])
('uf75-091.cnf', 8, [33.203953981399536])
('uf75-03.cnf', 3, [5.590798854827881])