Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-2.opb |
MD5SUM | a931f7e9a55cb6836807387327525e8b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -35 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 945 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 945 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 945 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.08 |
Number of variables | 945 |
Total number of constraints | 58624 |
Number of constraints which are clauses | 58624 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc22 THE 2005-05-27 05:36:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23084 boxname=wulflinc22 idbench=330 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a931f7e9a55cb6836807387327525e8b /oldhome/oroussel/tmp/wulflinc22/normalized-frb45-21-2.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc22/normalized-frb45-21-2.opb IDLAUNCH: 23084 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 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: 627244 kB Buffers: 34396 kB Cached: 350160 kB SwapCached: 392 kB Active: 66456 kB Inactive: 320368 kB HighTotal: 131008 kB HighFree: 2912 kB LowTotal: 903652 kB LowFree: 624332 kB SwapTotal: 2097892 kB SwapFree: 2096804 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5556 kB Slab: 14924 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 05:56:46 (client local time) WITH STATUS 152 IN 1229.87 SECONDS stats: 23084 7 1229.87 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 58624 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 58624 117248 | 19541 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost:44290 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 104213 224311 | 34737 0 0 nan | 0.000 % | c | 100 | 103753 223355 | 38210 63 352 5.6 | 0.799 % | c | 250 | 103075 221899 | 42031 184 1699 9.2 | 2.046 % | c | 475 | 101685 218869 | 46234 359 3428 9.5 | 4.676 % | c | 813 | 99941 215027 | 50858 624 5935 9.5 | 8.041 % | c ============================================================================== c [1mFound solution: -34[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1145 | 98367 211607 | 32789 875 9453 10.8 | 8.041 % | c | 1246 | 97670 210062 | 36067 936 10041 10.7 | 12.509 % | c | 1396 | 97202 209006 | 39674 1031 10925 10.6 | 13.452 % | c | 1621 | 95987 206277 | 43642 1161 12048 10.4 | 15.877 % | c | 1958 | 94801 203593 | 48006 1411 15086 10.7 | 18.255 % | c | 2464 | 92142 197582 | 52807 1692 17509 10.3 | 23.612 % | c | 3223 | 89622 191786 | 58087 2260 23288 10.3 | 28.835 % | c | 4362 | 85515 182365 | 63896 3094 31899 10.3 | 37.082 % | c | 6070 | 81641 173405 | 70286 4400 47324 10.8 | 45.054 % | c | 8632 | 76140 160465 | 77314 6222 77175 12.4 | 56.811 % | c | 12476 | 71881 150330 | 85046 9255 155440 16.8 | 66.013 % | c ============================================================================== c [1mFound solution: -35[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14307 | 70810 147891 | 23603 10753 201061 18.7 | 66.013 % | c | 14407 | 70765 147784 | 25963 10841 202522 18.7 | 68.509 % | c | 14557 | 70765 147784 | 28559 10991 207402 18.9 | 68.509 % | c | 14783 | 70691 147602 | 31415 11185 216078 19.3 | 68.675 % | c | 15120 | 70586 147358 | 34557 11507 227319 19.8 | 68.886 % | c | 15626 | 70348 146787 | 38012 11951 241938 20.2 | 69.400 % | c | 16385 | 70089 146154 | 41814 12648 271863 21.5 | 69.975 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16815 | 69891 145672 | 23297 13020 282802 21.7 | 69.975 % | c | 16915 | 69891 145672 | 25626 13120 284893 21.7 | 70.395 % | c | 17065 | 69891 145672 | 28189 13270 286399 21.6 | 70.395 % | c | 17290 | 69827 145517 | 31008 13475 295467 21.9 | 70.532 % | c | 17627 | 69734 145292 | 34109 13799 310942 22.5 | 70.743 % | c | 18133 | 69371 144409 | 37520 14192 322561 22.7 | 71.538 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18277 | 69362 144430 | 23120 14335 325818 22.7 | 71.538 % | c | 18377 | 69362 144430 | 25432 14435 332585 23.0 | 71.584 % | c | 18527 | 69277 144233 | 27975 14556 347362 23.9 | 71.763 % | c | 18752 | 69277 144233 | 30772 14781 367844 24.9 | 71.763 % | c | 19089 | 69030 143626 | 33849 14950 374080 25.0 | 72.327 % | c | 19596 | 68741 142905 | 37234 15398 392392 25.5 | 73.016 % | c | 20355 | 68660 142718 | 40958 16081 432831 26.9 | 73.185 % | c | 21494 | 68513 142365 | 45054 17165 509426 29.7 | 73.511 % | c | 23202 | 68154 141510 | 49559 18653 641562 34.4 | 74.298 % | c ============================================================================== c [1mFound solution: -38[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23824 | 67852 140729 | 22617 19046 663777 34.9 | 74.298 % | c | 23924 | 67766 140515 | 24878 19123 665280 34.8 | 75.183 % | c | 24074 | 67714 140393 | 27366 19252 669804 34.8 | 75.292 % | c | 24299 | 67714 140393 | 30103 19477 677322 34.8 | 75.292 % | c | 24636 | 67714 140393 | 33113 19814 696585 35.2 | 75.292 % | c | 25142 | 67678 140303 | 36424 20309 716491 35.3 | 75.375 % | c | 25902 | 67425 139703 | 40067 20929 797034 38.1 | 75.917 % | c | 27042 | 67212 139192 | 44074 21947 872312 39.7 | 76.383 % | c | 28750 | 67142 139014 | 48481 23609 1034815 43.8 | 76.548 % | c | 31312 | 67092 138893 | 53329 26102 1245314 47.7 | 76.657 % | c | 35156 | 66477 137377 | 58662 29648 1507713 50.9 | 78.057 % | c | 40922 | 66357 137092 | 64528 35234 2003265 56.9 | 78.315 % | c | 49572 | 66165 136632 | 70981 43618 2849495 65.3 | 78.733 % | c ============================================================================== c [1mFound solution: -39[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53102 | 66131 136585 | 22043 46964 3239093 69.0 | 78.733 % | c | 53203 | 66092 136494 | 24247 19870 1267667 63.8 | 78.977 % | c | 53353 | 66092 136494 | 26672 20020 1277625 63.8 | 78.977 % | c | 53578 | 66092 136494 | 29339 20245 1297647 64.1 | 78.977 % | c | 53917 | 66083 136473 | 32273 20580 1329003 64.6 | 78.996 % | c | 54424 | 66083 136473 | 35500 21087 1371465 65.0 | 78.996 % | c | 55183 | 66081 136469 | 39050 21844 1449488 66.4 | 78.999 % | c | 56322 | 66081 136469 | 42955 22983 1576964 68.6 | 78.999 % | c | 58030 | 66081 136469 | 47251 24691 1727745 70.0 | 78.999 % | c | 60592 | 65903 136032 | 51976 27218 1994366 73.3 | 79.390 % | c | 64436 | 65748 135667 | 57173 31008 2368011 76.4 | 79.714 % | c | 70202 | 65748 135667 | 62891 36774 3054028 83.0 | 79.714 % | c | 78851 | 65630 135370 | 69180 45415 4281369 94.3 | 79.987 % | c | 91825 | 65630 135370 | 76098 58389 6085540 104.2 | 79.987 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97446 | 65617 135317 | 21872 63942 6734885 105.3 | 79.987 % | c | 97546 | 65521 135083 | 24059 19913 1776166 89.2 | 80.240 % | c | 97696 | 65511 135059 | 26465 20062 1785837 89.0 | 80.262 % | c | 97921 | 65485 134999 | 29111 20286 1798820 88.7 | 80.316 % | c | 98258 | 65485 134999 | 32022 20623 1818617 88.2 | 80.316 % | c | 98765 | 65485 134999 | 35225 21130 1863451 88.2 | 80.316 % | c | 99525 | 65485 134999 | 38747 21890 1943719 88.8 | 80.316 % | c | 100667 | 65432 134870 | 42622 23023 2052223 89.1 | 80.433 % | c | 102376 | 65237 134387 | 46884 24634 2215179 89.9 | 80.881 % | c | 104938 | 65233 134377 | 51573 27193 2439838 89.7 | 80.891 % | c | 108784 | 65114 134084 | 56730 31017 2904470 93.6 | 81.164 % | c | 114550 | 64872 133502 | 62403 36617 3619951 98.9 | 81.689 % | c | 123199 | 64872 133502 | 68643 45266 4649642 102.7 | 81.689 % | c | 136175 | 64810 133346 | 75508 58227 6774965 116.4 | 81.838 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 150026 | 64829 133402 | 21609 72073 8627626 119.7 | 81.838 % | c | 150126 | 64829 133402 | 23769 20486 1739332 84.9 | 81.817 % | c | 150276 | 64829 133402 | 26146 20636 1744519 84.5 | 81.817 % | c | 150501 | 64829 133402 | 28761 20861 1763472 84.5 | 81.817 % | c | 150839 | 64720 133135 | 31637 21184 1776192 83.8 | 82.068 % | c | 151345 | 64720 133135 | 34801 21690 1809498 83.4 | 82.068 % | c | 152104 | 64667 133003 | 38281 22431 1868161 83.3 | 82.192 % | c | 153244 | 64576 132788 | 42109 23332 1921393 82.4 | 82.385 % | c | 154952 | 64519 132644 | 46320 25032 2128460 85.0 | 82.515 % | c | 157514 | 64514 132633 | 50952 27592 2413144 87.5 | 82.525 % | c | 161359 | 64514 132633 | 56048 31437 2830357 90.0 | 82.525 % | c | 167125 | 64508 132619 | 61652 37198 3592888 96.6 | 82.538 % | c | 175774 | 64484 132559 | 67818 45837 4744404 103.5 | 82.595 % | c | 188750 | 64443 132458 | 74600 58799 6135883 104.4 | 82.690 % | c | 208211 | 64435 132438 | 82060 78258 8346917 106.7 | 82.709 % | c | 237404 | 64428 132421 | 90266 107448 11304159 105.2 | 82.725 % | c | 281193 | 64313 132144 | 99292 56003 5085663 90.8 | 82.979 % | c | 346877 | 64154 131750 | 109222 121446 12746175 105.0 | 83.347 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 14470 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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 14466 Raw data (stat): 14466 (runsolver) R 14465 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853688552 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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.0003 s] Raw data (loadavg): 0.93 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0006 s] Raw data (loadavg): 0.94 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0014 s] Raw data (loadavg): 0.95 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0015 s] Raw data (loadavg): 0.96 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.002 s] Raw data (loadavg): 0.96 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0016 s] Raw data (loadavg): 0.97 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0019 s] Raw data (loadavg): 0.97 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0021 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0018 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.98 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.003 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.004 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.005 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.006 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.007 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.008 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.009 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.01 s] Raw data (loadavg): 0.99 0.98 0.91 2/55 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.74 s] Raw data (loadavg): 0.99 0.98 0.91 1/53 14470 Raw data (stat): 14466 (minisat+_script) S 14465 23310 23309 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853688552 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.74 CPU time (s): 1229.87 CPU user time (s): 1229.26 CPU system time (s): 0.610907 CPU usage (%): 100.01 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####