Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-momentum3.opb |
MD5SUM | fd20bcfe4a71405dc1e0ef3cb894b630 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 87370 |
Biggest coefficient in the objective function | 1310720000 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 13573186735 |
Number of bits of the sum of numbers in the objective function | 34 |
Biggest number in a constraint | 10240000000000000927712935936 |
Number of bits of the biggest number in a constraint | 94 |
Biggest sum of numbers in a constraint | 29801266744107043904416645120 |
Number of bits of the biggest sum of numbers | 95 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.893863 |
Number of variables | 93400 |
Total number of constraints | 70153 |
Number of constraints which are clauses | 6081 |
Number of constraints which are cardinality constraints (but not clauses) | 7185 |
Number of constraints which are nor clauses,nor cardinality constraints | 56887 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1018 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc23 THE 2005-05-27 07:07:32 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23339 boxname=wulflinc23 idbench=983 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fd20bcfe4a71405dc1e0ef3cb894b630 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-momentum3.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-momentum3.opb IDLAUNCH: 23339 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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.037 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: 314108 kB Buffers: 3204 kB Cached: 695148 kB SwapCached: 552 kB Active: 317828 kB Inactive: 382808 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 313856 kB SwapTotal: 2097136 kB SwapFree: 2095880 kB Dirty: 20 kB Writeback: 0 kB Mapped: 5620 kB Slab: 14100 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 07:28:09 (client local time) WITH STATUS 139 IN 1227.88 SECONDS stats: 23339 7 1227.88 139 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 35810] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 30306 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################=====================================================================================================================================================================================================================================================================================================================################################################################################################################################################################################################################################################################################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.s...........s...ss....................s......s......s..s.s.s....s.s...s..........s.....ss.s.......s.s...........s.s.......s.....s.s.sssssssssssssss..........s......ss.sss....................ss...........s...........s.s.........s............s...............s......s.ss....................s.....s.s...s..s...s......s.......s..s...sssss..s.ss..ss..s......s....ss........s..ss.s.s......s..s.....ss.s.ssss.......s.....ss........s.s.......ss......s...........s..ss......s......s......s.s.....s..s..s....s........s........s.sss..................s....s......ss..ssssss.....ss..s.....ssss..s...ss..s.s.sss....s.ss.sssssss.sss..s.ss.....s..ss..s.s...s..s..ss.s.ss.s.....ssss....ssss..s....s..sss..ssss.s..ss.sss......s.ssss..ss...s.....s.sssss.s...s.s........s..ssss.ss...s..sssssssssss.sssssssssssssssssss.s.s.s....s....ss......ss................s.......ss.ss...s....s...s.s.s..s..s..ss......sss.s..ss......s...s...s.s........ss...s.....s.s....s...ss........ss..ssss........ss.sss...s.ss.sss.sss..s..s..s.s..s.s..ssss.ssssss..sssssss.sss.sss..ss..ss..s.....sssssss...ss.ssssssss..ss..sssssss..ss....ssss.ss....ss.s....s.s..s.s.sss.s.s.ssssss.ss.s..s..s.ss.....s.sssssssssssssssss.sssssssss.s.s..s...ssssssss.s.sssss.s.s.sssssssssssssssssssssss.ssss..sss..sssssssss.ssss.sssssssss..ssssss.sssssssssssssssssssssssssssss.s.ssssssssssssssssssssssssssssssss..sss.s.ss.ssss.ss.ssssssssssssssssss.ssssssssssssssssssssssssssssssssssss..ss.s.sssssss.ssssssssssssssssssssssssssssssssssssssssssssssssss..ssssssss.ssssssssssssssssssssssssss..s..ss.sssss...s.s.s.ss.sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssss.s.ss..ssssssssssssssssssssssssssssssssssssssss.sssssssssssss..s..sss.sssss.ssssssssssssssssssss.sssss..sssssss.sssssssssssssssssssssss.sssssssssss..sssssss.ssssss.ssssssssssssssssssssssssssssssssssssssss.ssssssssssssssssss..sss.sssssssssssss.sss.ssss.ssssssssssssssssssssssssssssssssssssssssssssss.sssssssssssssssssssssssssss.ss.sssssssssssssssssssssss.sss.sssssss.sssssssssssssssssssssssss..ss.s...s....sssssssssssssssssssss.s.s.ssssss.sssssssssssssssssssss.sssssssssssssssss.ssssss.ssssssssssssssssssssssss.ssssssssssssssssssssssssss.ss.sssssssssssssssssssss...s.ssss.ssssssssss............................................................................................s...........s.............................s................................s............s...........................s.......................................................................s......s.........ss.sssssss...........................................s.............s....s.........................................s.....................s...........s........................................s.............................s...s.........s.......s...............................................s......s..........s......s....s....s..................ss....s.......s.......s...s...s...s...s...s.....s..sss.................s....s.............s...............s....................s.......................................................................s...........................................................s......s...........s...............................................................................................................................................s........................s...................................................................................................................................................s.............................................................................................................s..........s..............................................................................................................................................................................................................................................................................................................................................ss..s.s...s.s.....s.....s..s..............s.....s...........................s...s............s...ss.ss..s......................................s...................ss...............s.......s................s...s....................s..................s.......s.s....s..........s....s..............s...................s....s.....s....ssss.........s..s...........s.....s.......s..s...s...........s.........s........s..s.........................s....s.s.s................s.................s..s..s.....s.s....ss.........s...s............s.ss....s.ss..sss...........s........s.s.ss.......s.......s.s.s...s.......ss.s.ss..s..... c ---[32998]---> BDD-cost: 7 c ---[32997]---> BDD-cost: 10 c ---[32996]---> BDD-cost: 10 c ---[32995]---> BDD-cost: 10 c ---[32994]---> BDD-cost: 10 c ---[32993]---> BDD-cost: 10 c ---[32992]---> BDD-cost: 10 c ---[32991]---> BDD-cost: 10 c ---[32990]---> BDD-cost: 10 c ---[32989]---> BDD-cost: 10 c ---[32988]---> BDD-cost: 10 c ---[32987]---> BDD-cost: 10 c ---[32986]---> BDD-cost: 10 c ---[32985]---> BDD-cost: 10 c ---[32984]---> BDD-cost: 10 c ---[32983]---> BDD-cost: 10 c ---[32982]---> BDD-cost: 10 c ---[32981]---> BDD-cost: 10 c ---[32980]---> BDD-cost: 10 c ---[32979]---> BDD-cost: 10 c ---[32978]---> BDD-cost: 10 c ---[32977]---> BDD-cost: 10 c ---[32976]---> BDD-cost: 10 c ---[32975]---> BDD-cost: 10 c ---[32974]---> BDD-cost: 10 c ---[32973]---> BDD-cost: 10 c ---[32972]---> BDD-cost: 10 c ---[32971]---> BDD-cost: 10 c ---[32970]---> BDD-cost: 10 c ---[32969]---> BDD-cost: 10 c ---[32968]---> BDD-cost: 10 c ---[32967]---> BDD-cost: 10 c ---[32966]---> BDD-cost: 10 c ---[32965]---> BDD-cost: 10 c ---[32964]---> BDD-cost: 10 c ---[32963]---> BDD-cost: 10 c ---[32962]---> BDD-cost: 10 c ---[32961]---> BDD-cost: 10 c ---[32960]---> BDD-cost: 10 c ---[32959]---> BDD-cost: 10 c ---[32958]---> BDD-cost: 10 c ---[32957]---> BDD-cost: 10 c ---[32956]---> BDD-cost: 10 c ---[32954]---> BDD-cost: 10 c ---[32953]---> BDD-cost: 10 c ---[32952]---> BDD-cost: 10 c ---[32951]---> BDD-cost: 10 c ---[32949]---> BDD-cost: 10 c ---[32948]---> BDD-cost: 10 c ---[32947]---> BDD-cost: 10 c ---[32944]---> BDD-cost: 10 c ---[32941]---> BDD-cost: 10 c ---[32940]---> BDD-cost: 10 c ---[32939]---> BDD-cost: 10 c ---[32938]---> BDD-cost: 10 c ---[32937]---> BDD-cost: 10 c ---[32936]---> BDD-cost: 10 c ---[32935]---> BDD-cost: 10 c ---[32933]---> BDD-cost: 10 c ---[32932]---> BDD-cost: 10 c ---[32931]---> BDD-cost: 10 c ---[32930]---> BDD-cost: 10 c ---[32929]---> BDD-cost: 10 c ---[32927]---> BDD-cost: 10 c ---[32924]---> BDD-cost: 10 c ---[32921]---> BDD-cost: 10 c ---[32918]---> BDD-cost: 10 c ---[32916]---> BDD-cost: 10 c ---[32915]---> BDD-cost: 10 c ---[32914]---> BDD-cost: 10 c ---[32913]---> BDD-cost: 10 c ---[32911]---> BDD-cost: 10 c ---[32909]---> BDD-cost: 10 c ---[32908]---> BDD-cost: 10 c ---[32906]---> BDD-cost: 10 c ---[32904]---> BDD-cost: 10 c ---[32903]---> BDD-cost: 10 c ---[32902]---> BDD-cost: 10 c ---[32901]---> BDD-cost: 10 c ---[32900]---> BDD-cost: 10 c ---[32899]---> BDD-cost: 10 c ---[32896]---> BDD-cost: 10 c ---[32895]---> BDD-cost: 10 c ---[32894]---> BDD-cost: 10 c ---[32890]---> BDD-cost: 10 c ---[32889]---> BDD-cost: 10 c ---[32888]---> BDD-cost: 10 c ---[32885]---> BDD-cost: 10 c ---[32884]---> BDD-cost: 10 c ---[32883]---> BDD-cost: 10 c ---[32882]---> BDD-cost: 10 c ---[32881]---> BDD-cost: 10 c ---[32879]---> BDD-cost: 10 c ---[32878]---> BDD-cost: 10 c ---[32877]---> BDD-cost: 10 c ---[32876]---> BDD-cost: 10 c ---[32875]---> BDD-cost: 10 c ---[32874]---> BDD-cost: 10 c ---[32873]---> BDD-cost: 10 c ---[32872]---> BDD-cost: 10 c ---[32871]---> BDD-cost: 10 c ---[32870]---> BDD-cost: 10 c ---[32869]---> BDD-cost: 10 c ---[32868]---> BDD-cost: 10 c ---[32867]---> BDD-cost: 10 c ---[32866]---> BDD-cost: 10 c ---[32865]---> BDD-cost: 10 c ---[32864]---> BDD-cost: 10 c ---[32863]---> BDD-cost: 10 c ---[32861]---> BDD-cost: 10 c ---[32860]---> BDD-cost: 10 c ---[32857]---> BDD-cost: 10 c ---[32855]---> BDD-cost: 10 c ---[32854]---> BDD-cost: 10 c ---[32852]---> BDD-cost: 10 c ---[32848]---> BDD-cost: 10 c ---[32847]---> BDD-cost: 10 c ---[32846]---> BDD-cost: 10 c ---[32845]---> BDD-cost: 10 c ---[32841]---> BDD-cost: 10 c ---[32840]---> BDD-cost: 10 c ---[32839]---> BDD-cost: 10 c ---[32838]---> BDD-cost: 10 c ---[32837]---> BDD-cost: 10 c ---[32836]---> BDD-cost: 10 c ---[32835]---> BDD-cost: 10 c ---[32834]---> BDD-cost: 10 c ---[32833]---> BDD-cost: 10 c ---[32832]---> BDD-cost: 10 c ---[32831]---> BDD-cost: 10 c ---[32830]---> BDD-cost: 10 c ---[32827]---> BDD-cost: 10 c ---[32826]---> BDD-cost: 10 c ---[32825]---> BDD-cost: 10 c ---[32824]---> BDD-cost: 10 c ---[32822]---> BDD-cost: 10 c ---[32821]---> BDD-cost: 10 c ---[32819]---> BDD-cost: 10 c ---[32817]---> BDD-cost: 10 c ---[32816]---> BDD-cost: 10 c ---[32815]---> BDD-cost: 10 c ---[32812]---> BDD-cost: 10 c ---[32811]---> BDD-cost: 10 c ---[32810]---> BDD-cost: 10 c ---[32809]---> BDD-cost: 10 c ---[32807]---> BDD-cost: 10 c ---[32806]---> BDD-cost: 10 c ---[32804]---> BDD-cost: 10 c ---[32803]---> BDD-cost: 10 c ---[32802]---> BDD-cost: 10 c ---[32801]---> BDD-cost: 10 c ---[32798]---> BDD-cost: 10 c ---[26713]---> BDD-cost: 7 c ---[26712]---> BDD-cost: 10 c ---[26711]---> BDD-cost: 10 c ---[26709]---> BDD-cost: 7 c ---[26706]---> BDD-cost: 10 c ---[26704]---> BDD-cost: 7 c ---[26701]---> BDD-cost: 7 c ---[26700]---> BDD-cost: 10 c ---[26699]---> BDD-cost: 10 c ---[26697]---> BDD-cost: 7 c ---[26696]---> BDD-cost: 7 c ---[26695]---> BDD-cost: 10 c ---[26694]---> BDD-cost: 10 c ---[26693]---> BDD-cost: 10 c ---[26692]---> BDD-cost: 10 c ---[26689]---> BDD-cost: 10 c ---[26683]---> BDD-cost: 7 c ---[26682]---> BDD-cost: 10 c ---[26681]---> BDD-cost: 10 c ---[26680]---> BDD-cost: 10 c ---[26678]---> BDD-cost: 10 c ---[26676]---> BDD-cost: 10 c ---[26675]---> BDD-cost: 10 c ---[26673]---> BDD-cost: 10 c ---[26670]---> BDD-cost: 10 c ---[26669]---> BDD-cost: 7 c ---[26668]---> BDD-cost: 10 c ---[26666]---> BDD-cost: 10 c ---[26664]---> BDD-cost: 7 c ---[26660]---> BDD-cost: 10 c ---[26659]---> BDD-cost: 10 c ---[26655]---> BDD-cost: 10 c ---[26654]---> BDD-cost: 10 c ---[26648]---> BDD-cost: 10 c ---[26646]---> BDD-cost: 10 c ---[26645]---> BDD-cost: 10 c ---[26638]---> BDD-cost: 10 c ---[26636]---> BDD-cost: 10 c ---[26635]---> BDD-cost: 7 c ---[26629]---> BDD-cost: 10 c ---[26628]---> BDD-cost: 7 c ---[26627]---> BDD-cost: 7 c ---[26626]---> BDD-cost: 7 c ---[26620]---> BDD-cost: 10 c ---[26618]---> BDD-cost: 10 c ---[26617]---> BDD-cost: 7 c ---[26614]---> BDD-cost: 7 c ---[26609]---> BDD-cost: 10 c ---[26608]---> BDD-cost: 7 c ---[26607]---> BDD-cost: 10 c ---[26601]---> BDD-cost: 7 c ---[26600]---> BDD-cost: 7 c ---[26599]---> BDD-cost: 7 c ---[26598]---> BDD-cost: 7 c ---[26594]---> BDD-cost: 7 c ---[26591]---> BDD-cost: 10 c ---[26588]---> BDD-cost: 10 c ---[26586]---> BDD-cost: 10 c ---[26585]---> BDD-cost: 7 c ---[26581]---> BDD-cost: 10 c ---[26580]---> BDD-cost: 10 c ---[26577]---> BDD-cost: 10 c ---[26574]---> BDD-cost: 10 c ---[26573]---> BDD-cost: 10 c ---[26571]---> BDD-cost: 10 c ---[26570]---> BDD-cost: 7 c ---[26568]---> BDD-cost: 10 c ---[26565]---> BDD-cost: 10 c ---[26563]---> BDD-cost: 10 c ---[26560]---> BDD-cost: 7 c ---[26559]---> BDD-cost: 10 c ---[26558]---> BDD-cost: 7 c ---[26550]---> BDD-cost: 10 c ---[26549]---> BDD-cost: 10 c ---[26546]---> BDD-cost: 7 c ---[26542]---> BDD-cost: 10 c ---[26541]---> BDD-cost: 7 c ---[26539]---> BDD-cost: 10 c ---[26535]---> BDD-cost: 7 c ---[26528]---> BDD-cost: 7 c ---[26527]---> BDD-cost: 10 c ---[26526]---> BDD-cost: 7 c ---[26525]---> BDD-cost: 7 c ---[26524]---> BDD-cost: 7 c ---[26521]---> BDD-cost: 10 c ---[26515]---> BDD-cost: 10 c ---[26514]---> BDD-cost: 10 c ---[26512]---> BDD-cost: 10 c ---[26510]---> BDD-cost: 7 c ---[26509]---> BDD-cost: 10 c ---[26508]---> BDD-cost: 7 c ---[26507]---> BDD-cost: 10 c ---[26506]---> BDD-cost: 7 c ---[26503]---> BDD-cost: 10 c ---[26502]---> BDD-cost: 10 c ---[26501]---> BDD-cost: 10 c ---[26500]---> BDD-cost: 7 c ---[26499]---> BDD-cost: 10 c ---[26497]---> BDD-cost: 10 c ---[26495]---> BDD-cost: 7 c ---[26494]---> BDD-cost: 10 c ---[26493]---> BDD-cost: 7 c ---[26492]---> BDD-cost: 10 c ---[26490]---> BDD-cost: 10 c ---[26488]---> BDD-cost: 10 c ---[26484]---> BDD-cost: 10 c ---[26482]---> BDD-cost: 7 c ---[26480]---> BDD-cost: 7 c ---[26479]---> BDD-cost: 7 c ---[26478]---> BDD-cost: 7 c ---[26475]---> BDD-cost: 10 c ---[26473]---> BDD-cost: 10 c ---[26472]---> BDD-cost: 7 c ---[26471]---> BDD-cost: 10 c ---[26470]---> BDD-cost: 7 c ---[26469]---> BDD-cost: 10 c ---[26465]---> BDD-cost: 7 c ---[26464]---> BDD-cost: 10 c ---[26458]---> BDD-cost: 10 c ---[26456]---> BDD-cost: 10 c ---[26455]---> BDD-cost: 10 c ---[26453]---> BDD-cost: 10 c ---[26450]---> BDD-cost: 10 c ---[26449]---> BDD-cost: 7 c ---[26448]---> BDD-cost: 10 c ---[26445]---> BDD-cost: 7 c ---[26444]---> BDD-cost: 7 c ---[26443]---> BDD-cost: 10 c ---[26438]---> BDD-cost: 7 c ---[26436]---> BDD-cost: 10 c ---[26435]---> BDD-cost: 7 c ---[26431]---> BDD-cost: 10 c ---[26430]---> BDD-cost: 10 c ---[26428]---> BDD-cost: 10 c ---[26425]---> BDD-cost: 10 c ---[26424]---> BDD-cost: 10 c ---[26420]---> BDD-cost: 7 c ---[26418]---> BDD-cost: 7 c ---[26417]---> BDD-cost: 10 c ---[26412]---> BDD-cost: 7 c ---[26409]---> BDD-cost: 10 c ---[26408]---> BDD-cost: 7 c ---[26407]---> BDD-cost: 10 c ---[26404]---> BDD-cost: 10 c ---[26400]---> BDD-cost: 7 c ---[26399]---> BDD-cost: 7 c ---[26394]---> BDD-cost: 10 c ---[26392]---> BDD-cost: 10 c ---[26390]---> BDD-cost: 7 c ---[26389]---> BDD-cost: 10 c ---[26388]---> BDD-cost: 10 c ---[26387]---> BDD-cost: 10 c ---[26386]---> BDD-cost: 7 c ---[26384]---> BDD-cost: 10 c ---[26379]---> BDD-cost: 7 c ---[26378]---> BDD-cost: 7 c ---[26373]---> BDD-cost: 7 c ---[26369]---> BDD-cost: 10 c ---[26368]---> BDD-cost: 10 c ---[26367]---> BDD-cost: 7 c ---[26361]---> BDD-cost: 7 c ---[26360]---> BDD-cost: 10 c ---[26359]---> BDD-cost: 10 c ---[26358]---> BDD-cost: 10 c ---[26357]---> BDD-cost: 7 c ---[26356]---> BDD-cost: 10 c ---[26355]---> BDD-cost: 7 c ---[26354]---> BDD-cost: 7 c ---[26353]---> BDD-cost: 7 c ---[26352]---> BDD-cost: 7 c ---[26349]---> BDD-cost: 7 c ---[26348]---> BDD-cost: 7 c ---[26343]---> BDD-cost: 7 c ---[26342]---> BDD-cost: 7 c ---[26340]---> BDD-cost: 7 c ---[26336]---> BDD-cost: 10 c ---[26335]---> BDD-cost: 10 c ---[26332]---> BDD-cost: 7 c ---[26331]---> BDD-cost: 10 c ---[26330]---> BDD-cost: 10 c ---[26329]---> BDD-cost: 7 c ---[26321]---> BDD-cost: 10 c ---[26320]---> BDD-cost: 7 c ---[26319]---> BDD-cost: 7 c ---[26317]---> BDD-cost: 7 c ---[26315]---> BDD-cost: 10 c ---[26311]---> BDD-cost: 10 c ---[26310]---> BDD-cost: 7 c ---[26309]---> BDD-cost: 10 c ---[26308]---> BDD-cost: 10 c ---[26304]---> BDD-cost: 10 c ---[26302]---> BDD-cost: 7 c ---[26301]---> BDD-cost: 10 c ---[26299]---> BDD-cost: 7 c ---[26297]---> BDD-cost: 10 c ---[26289]---> BDD-cost: 7 c ---[26283]---> BDD-cost: 10 c ---[26279]---> BDD-cost: 7 c ---[26276]---> BDD-cost: 7 c ---[26275]---> BDD-cost: 7 c ---[26274]---> BDD-cost: 10 c ---[26273]---> BDD-cost: 7 c ---[26271]---> BDD-cost: 7 c ---[26269]---> BDD-cost: 10 c ---[26267]---> BDD-cost: 7 c ---[26172]---> BDD-cost: 10 c ---[25957]---> BDD-cost: 11 c ---[25441]---> BDD-cost: 10 c ---[25288]---> BDD-cost: 11 c ---[25084]---> BDD-cost: 10 c ---[25066]---> BDD-cost: 1 c ---[25030]---> BDD-cost: 11 c ---[25023]---> BDD-cost: 5 c ---[25012]---> BDD-cost: 1 c ---[24983]---> BDD-cost: 11 c ---[24954]---> BDD-cost: 11 c ---[24919]---> BDD-cost: 10 c ---[24905]---> BDD-cost: 11 c ---[24898]---> BDD-cost: 9 c ---[24892]---> BDD-cost: 10 c ---[24871]---> BDD-cost: 11 c ---[24855]---> BDD-cost: 8 c ---[24773]---> BDD-cost: 11 c ---[24726]---> BDD-cost: 11 c ---[24716]---> BDD-cost: 1 c ---[24646]---> BDD-cost: 1 c ---[24596]---> BDD-cost: 11 c ---[24587]---> BDD-cost: 11 c ---[24585]---> BDD-cost: 1 c ---[24555]---> BDD-cost: 10 c ---[24456]---> BDD-cost: 11 c ---[24454]---> BDD-cost: 5 c ---[24430]---> BDD-cost: 10 c ---[24429]---> BDD-cost: 1 c ---[24410]---> BDD-cost: 8 c ---[24368]---> BDD-cost: 11 c ---[24355]---> BDD-cost: 10 c ---[24345]---> BDD-cost: 1 c ---[24324]---> BDD-cost: 9 c ---[24319]---> BDD-cost: 8 c ---[24317]---> BDD-cost: 1 c ---[24311]---> BDD-cost: 10 c ---[24300]---> BDD-cost: 2 c ---[24291]---> BDD-cost: 11 c ---[24290]---> BDD-cost: 9 c ---[24269]---> BDD-cost: 1 c ---[24268]---> BDD-cost: 1 c ---[24257]---> BDD-cost: 10 c ---[24237]---> BDD-cost: 2 c ---[24208]---> BDD-cost: 10 c ---[24162]---> BDD-cost: 10 c ---[24161]---> BDD-cost: 2 c ---[24146]---> BDD-cost: 11 c ---[24134]---> BDD-cost: 1 c ---[24124]---> BDD-cost: 1 c ---[24111]---> BDD-cost: 10 c ---[24090]---> BDD-cost: 11 c ---[24068]---> BDD-cost: 10 c ---[24056]---> BDD-cost: 2 c ---[24054]---> BDD-cost: 2 c ---[24053]---> BDD-cost: 10 c ---[23989]---> BDD-cost: 10 c ---[23933]---> BDD-cost: 11 c ---[23932]---> BDD-cost: 10 c ---[23919]---> BDD-cost: 10 c ---[23914]---> BDD-cost: 1 c ---[23894]---> BDD-cost: 2 c ---[23890]---> BDD-cost: 10 c ---[23875]---> BDD-cost: 9 c ---[23828]---> BDD-cost: 10 c ---[23816]---> BDD-cost: 10 c ---[23796]---> BDD-cost: 2 c ---[23789]---> BDD-cost: 2 c ---[23779]---> BDD-cost: 11 c ---[23748]---> BDD-cost: 1 c ---[23716]---> BDD-cost: 11 c ---[23678]---> BDD-cost: 10 c ---[23667]---> BDD-cost: 1 c ---[23648]---> BDD-cost: 1 c ---[23610]---> BDD-cost: 1 c ---[23600]---> BDD-cost: 11 c ---[23593]---> BDD-cost: 10 c ---[23589]---> BDD-cost: 2 c ---[23588]---> BDD-cost: 10 c ---[23569]---> BDD-cost: 9 c ---[23539]---> BDD-cost: 10 c ---[23452]---> BDD-cost: 1 c ---[23444]---> BDD-cost: 1 c ---[23417]---> BDD-cost: 11 c ---[23354]---> BDD-cost: 10 c ---[23327]---> BDD-cost: 10 c ---[23245]---> BDD-cost: 10 c ---[23243]---> BDD-cost: 10 c ---[23220]---> BDD-cost: 9 c ---[23209]---> BDD-cost: 1 c ---[23206]---> BDD-cost: 1 c ---[23201]---> BDD-cost: 2 c ---[23179]---> BDD-cost: 11 c ---[23172]---> BDD-cost: 2 c ---[23168]---> BDD-cost: 2 c ---[23149]---> BDD-cost: 11 c ---[23132]---> BDD-cost: 10 c ---[23131]---> BDD-cost: 9 c ---[23112]---> BDD-cost: 2 c ---[23075]---> BDD-cost: 1 c ---[23070]---> BDD-cost: 10 c ---[23065]---> BDD-cost: 11 c ---[23028]---> BDD-cost: 11 c ---[23008]---> BDD-cost: 11 c ---[22988]---> BDD-cost: 1 c ---[22963]---> BDD-cost: 1 c ---[22962]---> BDD-cost: 1 c ---[22947]---> BDD-cost: 1 c ---[22937]---> BDD-cost: 11 c ---[22935]---> BDD-cost: 12 c ---[22925]---> BDD-cost: 10 c ---[22911]---> BDD-cost: 2 c ---[22909]---> BDD-cost: 10 c ---[22878]---> BDD-cost: 2 c ---[22815]---> BDD-cost: 10 c ---[22800]---> BDD-cost: 10 c ---[22788]---> BDD-cost: 11 c ---[22708]---> BDD-cost: 1 c ---[22692]---> BDD-cost: 11 c ---[22664]---> BDD-cost: 1 c ---[22663]---> BDD-cost: 1 c ---[22616]---> BDD-cost: 11 c ---[22592]---> BDD-cost: 8 c ---[22555]---> BDD-cost: 11 c ---[22532]---> BDD-cost: 1 c ---[22530]---> BDD-cost: 1 c ---[22500]---> BDD-cost: 1 c ---[22472]---> BDD-cost: 1 c ---[22450]---> BDD-cost: 10 c ---[22448]---> BDD-cost: 11 c ---[22355]---> BDD-cost: 11 c ---[22341]---> BDD-cost: 8 c ---[22313]---> BDD-cost: 1 c ---[22312]---> BDD-cost: 1 c ---[22292]---> BDD-cost: 12 c ---[22243]---> BDD-cost: 11 c ---[22224]---> BDD-cost: 10 c ---[22190]---> BDD-cost: 10 c ---[22178]---> BDD-cost: 2 c ---[22160]---> BDD-cost: 10 c ---[22137]---> BDD-cost: 2 c ---[22105]---> BDD-cost: 11 c ---[22073]---> BDD-cost: 8 c ---[22072]---> BDD-cost: 2 c ---[21958]---> BDD-cost: 11 c ---[21928]---> BDD-cost: 1 c ---[21925]---> BDD-cost: 10 c ---[21923]---> BDD-cost: 11 c ---[21874]---> BDD-cost: 10 c ---[21845]---> BDD-cost: 11 c ---[21841]---> BDD-cost: 10 c ---[21737]---> BDD-cost: 11 c ---[21729]---> BDD-cost: 2 c ---[21701]---> BDD-cost: 10 c ---[21691]---> BDD-cost: 10 c ---[21685]---> BDD-cost: 11 c ---[21636]---> BDD-cost: 10 c ---[21606]---> BDD-cost: 11 c ---[21600]---> BDD-cost: 1 c ---[21598]---> BDD-cost: 10 c ---[21593]---> BDD-cost: 1 c ---[21575]---> BDD-co/oldhome/oroussel/solvers/minisat+_script: line 16: 28555 Segmentation fault $XDIR/minisat+_bignum_static* "$@" #### 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): 1.13 1.02 0.93 2/54 28550 Raw data (stat): 28550 (runsolver) R 28549 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854240181 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0006 s] Raw data (loadavg): 1.11 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+20.0039 s] Raw data (loadavg): 1.10 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0032 s] Raw data (loadavg): 1.08 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0042 s] Raw data (loadavg): 1.07 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.005 s] Raw data (loadavg): 1.06 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0041 s] Raw data (loadavg): 1.05 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+70.0052 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+80.0057 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.005 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100.005 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110.005 s] Raw data (loadavg): 1.02 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120.006 s] Raw data (loadavg): 1.02 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130.006 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140.005 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150.006 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160.006 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170.006 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260.007 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290.008 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+300.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+310.009 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+320.01 s] Raw data (loadavg): 1.00 1.00 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+330.009 s] Raw data (loadavg): 1.08 1.02 0.93 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340.009 s] Raw data (loadavg): 1.14 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+350.011 s] Raw data (loadavg): 1.12 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360.011 s] Raw data (loadavg): 1.10 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370.011 s] Raw data (loadavg): 1.08 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380.011 s] Raw data (loadavg): 1.07 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+390.011 s] Raw data (loadavg): 1.06 1.03 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400.012 s] Raw data (loadavg): 1.05 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+410.011 s] Raw data (loadavg): 1.04 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+420.013 s] Raw data (loadavg): 1.04 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+430.013 s] Raw data (loadavg): 1.03 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+440.012 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+450.013 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+460.012 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+470.013 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+480.013 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+490.013 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+500.013 s] Raw data (loadavg): 1.01 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+510.015 s] Raw data (loadavg): 1.01 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+520.015 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+530.015 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+540.153 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+550.153 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+560.165 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+570.166 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+580.166 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+590.166 s] Raw data (loadavg): 1.00 1.01 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+600.167 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610.168 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+620.168 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+630.169 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+640.168 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+650.169 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+660.17 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+670.17 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+680.171 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+690.178 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+700.185 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+710.184 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+720.186 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+730.186 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+740.185 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+750.186 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+760.187 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+770.187 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+780.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+790.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+800.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+810.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+820.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+830.188 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+840.189 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+850.189 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+860.189 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+870.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+880.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+890.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+900.191 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+910.191 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+920.192 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+930.192 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+940.191 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+950.191 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+960.191 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+970.192 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+980.192 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+990.193 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1000.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1010.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1020.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1030.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1040.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1050.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1060.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1070.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1080.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1090.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1100.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1110.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1120.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1130.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1140.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1150.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1160.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1170.19 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1180.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1190.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1200.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 234 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1210.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 213 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 213 485 147 0 385 0 vsize: 2128 [startup+1220.2 s] Raw data (loadavg): 1.00 1.00 0.94 2/55 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 213 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 213 485 147 0 385 0 vsize: 2128 [startup+1229.24 s] Raw data (loadavg): 1.00 1.00 0.94 1/53 28555 Raw data (stat): 28550 (minisat+_script) S 28549 5562 5561 0 -1 0 300 5598 0 0 0 0 157 19 19 0 1 0 854240181 2179072 213 4294967295 134512640 135087896 3221224528 3221223416 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 213 485 147 0 385 0 vsize: 0 Child status: 139 Real time (s): 1229.2 CPU time (s): 1227.88 CPU user time (s): 1218.14 CPU system time (s): 9.74252 CPU usage (%): 99.8931 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####