PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-mkc.opb
MD5SUM	44934b498b6e9897bcf8e950d9d30136
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	2946
Biggest coefficient in the objective function	20000
Number of bits for the biggest coefficient in the objective function	15
Sum of the numbers in the objective function	31442101
Number of bits of the sum of numbers in the objective function	25
Biggest number in a constraint	65536000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	629010691
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.11
Number of variables	5363
Total number of constraints	8734
Number of constraints which are clauses	2977
Number of constraints which are cardinality constraints (but not clauses)	5731
Number of constraints which are nor clauses,nor cardinality constraints	26
Minimum length of a constraint	1
Maximum length of a constraint	2942
Trace number 18643

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 15:55:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17704 boxname=wulflinc27 idbench=1362 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  44934b498b6e9897bcf8e950d9d30136  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-mkc.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-mkc.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-mkc.opb
IDLAUNCH: 17704
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        672076 kB
Buffers:         20884 kB
Cached:         318060 kB
SwapCached:        512 kB
Active:          35352 kB
Inactive:       305572 kB
HighTotal:      131008 kB
HighFree:         1652 kB
LowTotal:       903652 kB
LowFree:        670424 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            15964 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:15:39 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 17704 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[3223]---> Adder-cost: 26498   maxlim: 479706816   bits: 29/29
c ---[3222]---> BDD-cost: 2265
c ---[3221]---> BDD-cost:   25
c ---[3210]---> BDD-cost:   23
c ---[3199]---> BDD-cost:    9
c ---[3188]---> BDD-cost:   21
c ---[3177]---> BDD-cost:   27
c ---[3138]---> BDD-cost:  461
c ---[3135]---> BDD-cost:    5
c ---[3114]---> Adder-cost: 1804   maxlim: 2264275   bits: 22/22
c ---[3113]---> BDD-cost:   29
c ---[3102]---> BDD-cost:   19
c ---[3091]---> BDD-cost:    7
c ---[3080]---> BDD-cost:    5
c ---[3069]---> BDD-cost:    5
c ---[3058]---> BDD-cost:    5
c ---[3037]---> BDD-cost:   29
c ---[3026]---> BDD-cost:   27
c ---[3015]---> BDD-cost:   27
c ---[3004]---> BDD-cost: 3790
c ---[3003]---> BDD-cost:    5
c ---[2992]---> BDD-cost:    5
c ---[2981]---> BDD-cost:   29
c ---[2970]---> BDD-cost:   27
c ---[2959]---> BDD-cost:   11
c ---[2948]---> BDD-cost:    9
c ---[2930]---> BDD-cost:  485
c ---[2927]---> BDD-cost:   19
c ---[2916]---> BDD-cost:   19
c ---[2905]---> BDD-cost:   27
c ---[2894]---> BDD-cost: 1005
c ---[2893]---> BDD-cost:   19
c ---[2872]---> BDD-cost:   21
c ---[2839]---> BDD-cost:   19
c ---[2828]---> BDD-cost:   19
c ---[2796]---> BDD-cost:   21
c ---[2785]---> Sorter-cost:17311     Base: 5 2 5 2 3 2 2 2 2 2
c ---[2784]---> BDD-cost:    3
c ---[2773]---> BDD-cost:   29
c ---[2752]---> BDD-cost:   29
c ---[2741]---> BDD-cost:   27
c ---[2730]---> BDD-cost:   29
c ---[2711]---> BDD-cost:  461
c ---[2699]---> BDD-cost:    3
c ---[2688]---> BDD-cost:   13
c ---[2677]---> Adder-cost: 1438   maxlim: 1767687   bits: 21/21
c ---[2665]---> BDD-cost:    3
c ---[2654]---> BDD-cost:    3
c ---[2632]---> BDD-cost:    3
c ---[2621]---> BDD-cost:    3
c ---[2610]---> BDD-cost:   21
c ---[2589]---> BDD-cost:   23
c ---[2568]---> Adder-cost: 1090   maxlim: 131883   bits: 18/18
c ---[2567]---> BDD-cost:    3
c ---[2524]---> BDD-cost:    3
c ---[2505]---> BDD-cost:  461
c ---[2503]---> BDD-cost:   23
c ---[2472]---> BDD-cost:   29
c ---[2461]---> Sorter-cost:10972     Base: 2 5 5 3 11 3 2
c ---[2460]---> BDD-cost:   29
c ---[2438]---> BDD-cost:    3
c ---[2367]---> BDD-cost:   27
c ---[2356]---> BDD-cost: 1027
c ---[2355]---> BDD-cost:   29
c ---[2324]---> BDD-cost:    3
c ---[2305]---> BDD-cost:  461
c ---[2283]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2250]---> BDD-cost:  196
c ---[2239]---> BDD-cost:    5
c ---[2218]---> BDD-cost:   11
c ---[2207]---> BDD-cost:    7
c ---[2196]---> BDD-cost:   15
c ---[2166]---> BDD-cost:   19
c ---[2143]---> Adder-cost: 477   maxlim: 2053920   bits: 22/21
c ---[2142]---> BDD-cost:   81
c ---[2141]---> BDD-cost:   19
c ---[2130]---> BDD-cost:   19
c ---[2119]---> BDD-cost:   17
c ---[2108]---> BDD-cost:   17
c ---[2099]---> BDD-cost:  527
c ---[2097]---> BDD-cost:   19
c ---[2086]---> BDD-cost:   19
c ---[2075]---> BDD-cost:   19
c ---[2033]---> BDD-cost:  171
c ---[2011]---> BDD-cost:   19
c ---[2000]---> BDD-cost:   17
c ---[1989]---> BDD-cost:   19
c ---[1978]---> BDD-cost:   19
c ---[1967]---> BDD-cost:   19
c ---[1946]---> BDD-cost:   21
c ---[1935]---> BDD-cost:   19
c ---[1924]---> BDD-cost:  131
c ---[1923]---> BDD-cost:   17
c ---[1912]---> BDD-cost:   19
c ---[1880]---> BDD-cost:    3
c ---[1869]---> BDD-cost:   15
c ---[1865]---> BDD-cost:  551
c ---[1858]---> BDD-cost:   13
c ---[1848]---> BDD-cost:   19
c ---[1827]---> BDD-cost:   19
c ---[1816]---> BDD-cost:   74
c ---[1815]---> BDD-cost:   19
c ---[1794]---> BDD-cost:   19
c ---[1773]---> BDD-cost:   19
c ---[1752]---> BDD-cost:   19
c ---[1741]---> BDD-cost:   19
c ---[1712]---> BDD-cost:   51
c ---[1711]---> BDD-cost:   15
c ---[1693]---> BDD-cost:   19
c ---[1672]---> BDD-cost:    3
c ---[1661]---> BDD-cost:   15
c ---[1650]---> BDD-cost:   19
c ---[1639]---> BDD-cost:   19
c ---[1628]---> BDD-cost:   19
c ---[1627]---> BDD-cost:  488
c ---[1612]---> BDD-cost:   29
c ---[1611]---> BDD-cost:   17
c ---[1602]---> BDD-cost:   19
c ---[1594]---> BDD-cost:   19
c ---[1577]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1547]---> BDD-cost:   15
c ---[1526]---> BDD-cost:   17
c ---[1518]---> BDD-cost:    3
c ---[1513]---> BDD-cost:   17
c ---[1482]---> BDD-cost:    7
c ---[1462]---> BDD-cost:  335
c ---[1451]---> BDD-cost:    3
c ---[1430]---> BDD-cost:   17
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   11
c ---[1327]---> BDD-cost:    7
c ---[1316]---> BDD-cost:  416
c ---[1306]---> BDD-cost:   17
c ---[1295]---> BDD-cost:    5
c ---[1284]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    7
c ---[1251]---> BDD-cost:    7
c ---[1240]---> BDD-cost:   19
c ---[1229]---> BDD-cost:   19
c ---[1218]---> BDD-cost:   19
c ---[1207]---> BDD-cost:    5
c ---[1196]---> BDD-cost:   17
c ---[1185]---> BDD-cost:   19
c ---[1163]---> BDD-cost:   29
c ---[1152]---> BDD-cost:   29
c ---[1141]---> BDD-cost:   29
c ---[1130]---> BDD-cost:   29
c ---[1128]---> BDD-cost:  260
c ---[1119]---> Adder-cost: 2340   maxlim: 3201964   bits: 22/22
c ---[1118]---> BDD-cost:   21
c ---[1117]---> BDD-cost:   29
c ---[1106]---> BDD-cost:   23
c ---[1095]---> BDD-cost:   17
c ---[1084]---> BDD-cost:   17
c ---[1073]---> BDD-cost:   17
c ---[1062]---> BDD-cost:    7
c ---[1051]---> BDD-cost:    7
c ---[1019]---> BDD-cost:   21
c ---[1008]---> BDD-cost:   29
c ---[1007]---> BDD-cost:    7
c ---[ 996]---> BDD-cost:    5
c ---[ 988]---> BDD-cost:  212
c ---[ 985]---> BDD-cost:    5
c ---[ 974]---> BDD-cost:    5
c ---[ 963]---> BDD-cost:    7
c ---[ 952]---> BDD-cost:    9
c ---[ 931]---> BDD-cost:    5
c ---[ 920]---> BDD-cost:   21
c ---[ 909]---> BDD-cost:   17
c ---[ 891]---> BDD-cost:  161
c ---[ 888]---> BDD-cost:   27
c ---[ 877]---> BDD-cost:   17
c ---[ 866]---> BDD-cost:   17
c ---[ 855]---> BDD-cost:   27
c ---[ 844]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   65
c ---[ 813]---> BDD-cost:   27
c ---[ 802]---> BDD-cost:   19
c ---[ 790]---> BDD-cost:   29
c ---[ 780]---> BDD-cost:   32
c ---[ 779]---> BDD-cost:   23
c ---[ 761]---> BDD-cost:   50
c ---[ 739]---> BDD-cost:   38
c ---[ 738]---> BDD-cost:   21
c ---[ 727]---> BDD-cost:   23
c ---[ 719]---> BDD-cost:   26
c ---[ 704]---> BDD-cost:   17
c ---[ 695]---> BDD-cost:   21
c ---[ 689]---> BDD-cost:   17
c ---[ 684]---> BDD-cost:   11
c ---[ 683]---> BDD-cost:   23
c ---[ 678]---> BDD-cost:   14
c ---[ 672]---> BDD-cost:   11
c ---[ 669]---> BDD-cost:   19
c ---[ 666]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   29
c ---[ 663]---> BDD-cost:   29
c ---[ 662]---> BDD-cost:   19
c ---[ 661]---> BDD-cost:   29
c ---[ 660]---> BDD-cost:   29
c ---[ 659]---> BDD-cost:   23
c ---[ 658]---> BDD-cost:   25
c ---[ 657]---> BDD-cost:   29
c ---[ 656]---> BDD-cost:   27
c ---[ 655]---> BDD-cost:   19
c ---[ 654]---> BDD-cost:   19
c ---[ 653]---> BDD-cost:   19
c ---[ 652]---> BDD-cost:   19
c ---[ 651]---> BDD-cost:   19
c ---[ 650]---> BDD-cost:   17
c ---[ 649]---> BDD-cost:   19
c ---[ 648]---> BDD-cost:    9
c ---[ 647]---> BDD-cost:   19
c ---[ 644]---> BDD-cost:   23
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:   19
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:   25
c ---[ 637]---> BDD-cost:   23
c ---[ 636]---> BDD-cost:   27
c ---[ 635]---> BDD-cost:   21
c ---[ 634]---> BDD-cost:   15
c ---[ 633]---> BDD-cost:   15
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost: 1925
c ---[ 626]---> BDD-cost:    5
c ---[ 625]---> BDD-cost:   29
c ---[ 624]---> BDD-cost:   29
c ---[ 623]---> BDD-cost:   29
c ---[ 622]---> BDD-cost:   29
c ---[ 621]---> BDD-cost:   19
c ---[ 620]---> BDD-cost:   21
c ---[ 619]---> BDD-cost:   19
c ---[ 618]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   19
c ---[ 615]---> BDD-cost:   19
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:   19
c ---[ 612]---> BDD-cost:   15
c ---[ 611]---> BDD-cost:   27
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    9
c ---[ 608]---> BDD-cost:    9
c ---[ 607]---> BDD-cost:    7
c ---[ 606]---> BDD-cost:   19
c ---[ 604]---> BDD-cost:   29
c ---[ 603]---> BDD-cost:   23
c ---[ 602]---> BDD-cost:   21
c ---[ 601]---> BDD-cost:   27
c ---[ 600]---> BDD-cost:   23
c ---[ 598]---> BDD-cost:   23
c ---[ 597]---> BDD-cost:   19
c ---[ 596]---> BDD-cost:   29
c ---[ 595]---> BDD-cost:   27
c ---[ 594]---> BDD-cost:   23
c ---[ 593]---> BDD-cost:   25
c ---[ 592]---> BDD-cost:   19
c ---[ 591]---> BDD-cost:   23
c ---[ 590]---> BDD-cost:   27
c ---[ 584]---> BDD-cost:   23
c ---[ 581]---> BDD-cost:   23
c ---[ 580]---> BDD-cost:   19
c ---[ 579]---> BDD-cost:  659
c ---[ 575]---> BDD-cost:   29
c ---[ 554]---> BDD-cost:   19
c ---[ 543]---> Adder-cost: 1584   maxlim: 1898736   bits: 21/21
c ---[ 542]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   29
c ---[ 466]---> BDD-cost:   23
c ---[ 444]---> BDD-cost:   15
c ---[ 433]---> Adder-cost: 1568   maxlim: 1898736   bits: 21/21
c ---[ 422]---> BDD-cost:   23
c ---[ 400]---> BDD-cost:    5
c ---[ 378]---> BDD-cost:   27
c ---[ 367]---> BDD-cost:   11
c ---[ 356]---> BDD-cost:   29
c ---[ 345]---> BDD-cost:   19
c ---[ 324]---> Adder-cost: 1704   maxlim: 2180627   bits: 22/22
c ---[ 312]---> BDD-cost:   21
c ---[ 279]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:   29
c ---[ 260]---> BDD-cost:  305
c ---[ 246]---> BDD-cost:   29
c ---[ 235]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:   29
c ---[ 213]---> Adder-cost: 1576   maxlim: 1898736   bits: 21/21
c ---[ 212]---> BDD-cost:   15
c ---[ 201]---> BDD-cost:   15
c ---[ 190]---> BDD-cost:   23
c ---[ 179]---> BDD-cost:   23
c ---[ 158]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:  461
c ---[ 115]---> BDD-cost:    5
c ---[ 105]---> Adder-cost: 1630   maxlim: 1978736   bits: 21/21
c ---[  83]---> BDD-cost:   29
c ---[  72]---> BDD-cost:   27
c ---[  61]---> BDD-cost:    5
c ---[  40]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  413166  1342340 |  123949       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/88775          
c   -- var.elim.:  2000/88775          
c   -- var.elim.:  3000/88775          
c   -- var.elim.:  4000/88775          
c   -- var.elim.:  5000/88775          
c   -- var.elim.:  6000/88775          
c   -- var.elim.:  7000/88775          
c   -- var.elim.:  8000/88775          
c   -- var.elim.:  9000/88775          
c   -- var.elim.:  10000/88775          
c   -- var.elim.:  11000/88775          
c   -- var.elim.:  12000/88775          
c   -- var.elim.:  13000/88775          
c   -- var.elim.:  14000/88775          
c   -- var.elim.:  15000/88775          
c   -- var.elim.:  16000/88775          
c   -- var.elim.:  17000/88775          
c   -- var.elim.:  18000/88775          
c   -- var.elim.:  19000/88775          
c   -- var.elim.:  20000/88775          
c   -- var.elim.:  21000/88775          
c   -- var.elim.:  22000/88775          
c   -- var.elim.:  23000/88775          
c   -- var.elim.:  24000/88775          
c   -- var.elim.:  25000/88775          
c   -- var.elim.:  26000/88775          
c   -- var.elim.:  27000/88775          
c   -- var.elim.:  28000/88775          
c   -- var.elim.:  29000/88775          
c   -- var.elim.:  30000/88775          
c   -- var.elim.:  31000/88775          
c   -- var.elim.:  32000/88775          
c   -- var.elim.:  33000/88775          
c   -- var.elim.:  34000/88775          
c   -- var.elim.:  35000/88775          
c   -- var.elim.:  36000/88775          
c   -- var.elim.:  37000/88775          
c   -- var.elim.:  38000/88775          
c   -- var.elim.:  39000/88775          
c   -- var.elim.:  40000/88775          
c   -- var.elim.:  41000/88775          
c   -- var.elim.:  42000/88775          
c   -- var.elim.:  43000/88775          
c   -- var.elim.:  44000/88775          
c   -- var.elim.:  45000/88775          
c   -- var.elim.:  46000/88775          
c   -- var.elim.:  47000/88775          
c   -- var.elim.:  48000/88775          
c   -- var.elim.:  49000/88775          
c   -- var.elim.:  50000/88775          
c   -- var.elim.:  51000/88775          
c   -- var.elim.:  52000/88775          
c   -- var.elim.:  53000/88775          
c   -- var.elim.:  54000/88775          
c   -- var.elim.:  55000/88775          
c   -- var.elim.:  56000/88775          
c   -- var.elim.:  57000/88775          
c   -- var.elim.:  58000/88775          
c   -- var.elim.:  59000/88775          
c   -- var.elim.:  60000/88775          
c   -- var.elim.:  61000/88775          
c   -- var.elim.:  62000/88775          
c   -- var.elim.:  63000/88775          
c   -- var.elim.:  64000/88775          
c   -- var.elim.:  65000/88775          
c   -- var.elim.:  66000/88775          
c   -- var.elim.:  67000/88775          
c   -- var.elim.:  68000/88775          
c   -- var.elim.:  69000/88775          
c   -- var.elim.:  70000/88775          
c   -- var.elim.:  71000/88775          
c   -- var.elim.:  72000/88775          
c   -- var.elim.:  73000/88775          
c   -- var.elim.:  74000/88775          
c   -- var.elim.: #### 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.85 0.97 0.93 2/54 21608
Raw data (stat): 21608 (runsolver) R 21607 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546321411 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 3748 0 0 0 989 9 0 0 25 0 1 0 546321411 11464704 2322 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2322 603 41 0 2758 0
vsize: 11196
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 3748 0 0 0 1990 9 0 0 25 0 1 0 546321411 11464704 2322 4294967295 134512640 134672761 3221224544 3221222096 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2322 603 41 0 2758 0
vsize: 11196
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 9318 0 0 0 2975 23 0 0 25 0 1 0 546321411 28180480 6234 4294967295 134512640 134672761 3221224544 3221221856 134544472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6880 6234 603 41 0 6839 0
vsize: 27520
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 24337 0 0 0 3935 63 0 0 25 0 1 0 546321411 93802496 20466 4294967295 134512640 134672761 3221224544 3221223008 1075349665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22901 20466 603 41 0 22860 0
vsize: 91604
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 26365 0 0 0 4929 69 0 0 25 0 1 0 546321411 90959872 19864 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22207 19864 603 41 0 22166 0
vsize: 88828
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 26796 0 0 0 5928 70 0 0 25 0 1 0 546321411 92667904 20295 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22624 20295 603 41 0 22583 0
vsize: 90496
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 27305 0 0 0 6927 71 0 0 25 0 1 0 546321411 94863360 20804 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23160 20804 603 41 0 23119 0
vsize: 92640
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 27666 0 0 0 7927 72 0 0 25 0 1 0 546321411 96317440 21165 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23515 21165 603 41 0 23474 0
vsize: 94060
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 28106 0 0 0 8926 73 0 0 25 0 1 0 546321411 98181120 21605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23970 21605 603 41 0 23929 0
vsize: 95880
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 28441 0 0 0 9925 74 0 0 25 0 1 0 546321411 99504128 21940 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24293 21940 603 41 0 24252 0
vsize: 97172
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 28780 0 0 0 10924 75 0 0 25 0 1 0 546321411 100823040 22279 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24615 22279 603 41 0 24574 0
vsize: 98460
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29087 0 0 0 11924 76 0 0 25 0 1 0 546321411 102141952 22586 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24937 22586 603 41 0 24896 0
vsize: 99748
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29346 0 0 0 12923 76 0 0 25 0 1 0 546321411 103190528 22845 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25193 22845 603 41 0 25152 0
vsize: 100772
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29530 0 0 0 13923 77 0 0 25 0 1 0 546321411 103858176 23029 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25356 23029 603 41 0 25315 0
vsize: 101424
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29659 0 0 0 14923 77 0 0 25 0 1 0 546321411 104390656 23158 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25486 23158 603 41 0 25445 0
vsize: 101944
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29754 0 0 0 15923 77 0 0 25 0 1 0 546321411 104787968 23253 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25583 23253 603 41 0 25542 0
vsize: 102332
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29852 0 0 0 16923 78 0 0 25 0 1 0 546321411 105181184 23351 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25679 23351 603 41 0 25638 0
vsize: 102716
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 29971 0 0 0 17922 78 0 0 25 0 1 0 546321411 105709568 23470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25808 23470 603 41 0 25767 0
vsize: 103232
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 30190 0 0 0 18922 79 0 0 25 0 1 0 546321411 106778624 23689 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26069 23689 603 41 0 26028 0
vsize: 104276
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 30365 0 0 0 19921 80 0 0 25 0 1 0 546321411 107446272 23864 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26232 23864 603 41 0 26191 0
vsize: 104928
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 30554 0 0 0 20921 80 0 0 25 0 1 0 546321411 108249088 24053 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26428 24053 603 41 0 26387 0
vsize: 105712
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 30730 0 0 0 21920 81 0 0 25 0 1 0 546321411 108912640 24229 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26590 24229 603 41 0 26549 0
vsize: 106360
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 30888 0 0 0 22920 81 0 0 25 0 1 0 546321411 109568000 24387 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26750 24387 603 41 0 26709 0
vsize: 107000
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31045 0 0 0 23920 82 0 0 25 0 1 0 546321411 110239744 24544 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26914 24544 603 41 0 26873 0
vsize: 107656
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31169 0 0 0 24919 82 0 0 25 0 1 0 546321411 110764032 24668 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27042 24668 603 41 0 27001 0
vsize: 108168
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 21608
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31309 0 0 0 25919 83 0 0 25 0 1 0 546321411 111337472 24808 4294967295 134512640 134672761 3221224544 3221223744 134610652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27182 24808 603 41 0 27141 0
vsize: 108728
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 21646
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31461 0 0 0 26918 84 0 0 25 0 1 0 546321411 112017408 24960 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27348 24960 603 41 0 27307 0
vsize: 109392
[startup+280.012 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31613 0 0 0 27918 84 0 0 25 0 1 0 546321411 112574464 25112 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27484 25112 603 41 0 27443 0
vsize: 109936
[startup+290.012 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31756 0 0 0 28918 85 0 0 25 0 1 0 546321411 113102848 25255 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27613 25255 603 41 0 27572 0
vsize: 110452
[startup+300.012 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 31887 0 0 0 29918 85 0 0 25 0 1 0 546321411 113766400 25386 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27775 25386 603 41 0 27734 0
vsize: 111100
[startup+310.012 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32014 0 0 0 30917 85 0 0 25 0 1 0 546321411 114159616 25513 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27871 25513 603 41 0 27830 0
vsize: 111484
[startup+320.012 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32146 0 0 0 31917 86 0 0 25 0 1 0 546321411 114814976 25645 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28031 25645 603 41 0 27990 0
vsize: 112124
[startup+330.013 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 21661
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32286 0 0 0 32917 86 0 0 25 0 1 0 546321411 115339264 25785 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28159 25785 603 41 0 28118 0
vsize: 112636
[startup+340.012 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32427 0 0 0 33917 86 0 0 25 0 1 0 546321411 115867648 25926 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28288 25926 603 41 0 28247 0
vsize: 113152
[startup+350.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32585 0 0 0 34917 87 0 0 25 0 1 0 546321411 116527104 26084 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28449 26084 603 41 0 28408 0
vsize: 113796
[startup+360.013 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32739 0 0 0 35917 87 0 0 25 0 1 0 546321411 117198848 26238 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28613 26238 603 41 0 28572 0
vsize: 114452
[startup+370.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32890 0 0 0 36917 88 0 0 25 0 1 0 546321411 117723136 26389 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28741 26389 603 41 0 28700 0
vsize: 114964
[startup+380.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 32999 0 0 0 37916 88 0 0 25 0 1 0 546321411 118263808 26498 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28873 26498 603 41 0 28832 0
vsize: 115492
[startup+390.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33088 0 0 0 38916 88 0 0 25 0 1 0 546321411 118525952 26587 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28937 26587 603 41 0 28896 0
vsize: 115748
[startup+400.014 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33190 0 0 0 39916 88 0 0 25 0 1 0 546321411 119054336 26689 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29066 26689 603 41 0 29025 0
vsize: 116264
[startup+410.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33309 0 0 0 40916 89 0 0 25 0 1 0 546321411 119455744 26808 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29164 26808 603 41 0 29123 0
vsize: 116656
[startup+420.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33451 0 0 0 41916 89 0 0 25 0 1 0 546321411 120119296 26950 4294967295 134512640 134672761 3221224544 3221223680 134614503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29326 26950 603 41 0 29285 0
vsize: 117304
[startup+430.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33573 0 0 0 42916 90 0 0 25 0 1 0 546321411 120524800 27072 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29425 27072 603 41 0 29384 0
vsize: 117700
[startup+440.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33664 0 0 0 43915 90 0 0 25 0 1 0 546321411 121053184 27163 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29554 27163 603 41 0 29513 0
vsize: 118216
[startup+450.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33761 0 0 0 44915 91 0 0 25 0 1 0 546321411 121319424 27260 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29619 27260 603 41 0 29578 0
vsize: 118476
[startup+460.016 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33857 0 0 0 45915 91 0 0 25 0 1 0 546321411 122241024 27356 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29844 27356 603 41 0 29803 0
vsize: 119376
[startup+470.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 33969 0 0 0 46915 91 0 0 25 0 1 0 546321411 122777600 27468 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29975 27468 603 41 0 29934 0
vsize: 119900
[startup+480.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34077 0 0 0 47915 92 0 0 25 0 1 0 546321411 123174912 27576 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30072 27576 603 41 0 30031 0
vsize: 120288
[startup+490.017 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34149 0 0 0 48914 92 0 0 25 0 1 0 546321411 123441152 27648 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30137 27648 603 41 0 30096 0
vsize: 120548
[startup+500.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34244 0 0 0 49914 92 0 0 25 0 1 0 546321411 123838464 27743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30234 27743 603 41 0 30193 0
vsize: 120936
[startup+510.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34356 0 0 0 50914 92 0 0 25 0 1 0 546321411 124231680 27855 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30330 27855 603 41 0 30289 0
vsize: 121320
[startup+520.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34455 0 0 0 51914 93 0 0 25 0 1 0 546321411 124628992 27954 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30427 27954 603 41 0 30386 0
vsize: 121708
[startup+530.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34568 0 0 0 52914 93 0 0 25 0 1 0 546321411 125157376 28067 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30556 28067 603 41 0 30515 0
vsize: 122224
[startup+540.018 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34643 0 0 0 53914 93 0 0 25 0 1 0 546321411 125419520 28142 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30620 28142 603 41 0 30579 0
vsize: 122480
[startup+550.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34710 0 0 0 54914 93 0 0 25 0 1 0 546321411 125702144 28209 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30689 28209 603 41 0 30648 0
vsize: 122756
[startup+560.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34785 0 0 0 55914 94 0 0 25 0 1 0 546321411 125984768 28284 4294967295 134512640 134672761 3221224544 3221223728 134615779 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30758 28284 603 41 0 30717 0
vsize: 123032
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34885 0 0 0 56914 94 0 0 25 0 1 0 546321411 126509056 28384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30886 28384 603 41 0 30845 0
vsize: 123544
[startup+580.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 34983 0 0 0 57914 94 0 0 25 0 1 0 546321411 126906368 28482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30983 28482 603 41 0 30942 0
vsize: 123932
[startup+590.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35084 0 0 0 58914 94 0 0 25 0 1 0 546321411 127299584 28583 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31079 28583 603 41 0 31038 0
vsize: 124316
[startup+600.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21663
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35176 0 0 0 59914 95 0 0 25 0 1 0 546321411 127561728 28675 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31143 28675 603 41 0 31102 0
vsize: 124572
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35256 0 0 0 60914 95 0 0 25 0 1 0 546321411 127963136 28755 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31241 28755 603 41 0 31200 0
vsize: 124964
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35337 0 0 0 61914 95 0 0 25 0 1 0 546321411 128225280 28836 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31305 28836 603 41 0 31264 0
vsize: 125220
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35418 0 0 0 62914 95 0 0 25 0 1 0 546321411 128626688 28917 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31403 28917 603 41 0 31362 0
vsize: 125612
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35509 0 0 0 63914 96 0 0 25 0 1 0 546321411 129028096 29008 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31501 29008 603 41 0 31460 0
vsize: 126004
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35598 0 0 0 64914 96 0 0 25 0 1 0 546321411 129298432 29097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31567 29097 603 41 0 31526 0
vsize: 126268
[startup+660.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35689 0 0 0 65914 96 0 0 25 0 1 0 546321411 129691648 29188 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31663 29188 603 41 0 31622 0
vsize: 126652
[startup+670.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35780 0 0 0 66913 97 0 0 25 0 1 0 546321411 130093056 29279 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31761 29279 603 41 0 31720 0
vsize: 127044
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35879 0 0 0 67913 97 0 0 25 0 1 0 546321411 130486272 29378 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31857 29378 603 41 0 31816 0
vsize: 127428
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 35963 0 0 0 68913 97 0 0 25 0 1 0 546321411 130908160 29462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31960 29462 603 41 0 31919 0
vsize: 127840
[startup+700.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36045 0 0 0 69913 97 0 0 25 0 1 0 546321411 131178496 29544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32026 29544 603 41 0 31985 0
vsize: 128104
[startup+710.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36144 0 0 0 70913 97 0 0 25 0 1 0 546321411 131571712 29643 4294967295 134512640 134672761 3221224544 3221223584 134612808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32122 29643 603 41 0 32081 0
vsize: 128488
[startup+720.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36244 0 0 0 71913 97 0 0 25 0 1 0 546321411 131964928 29743 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32218 29743 603 41 0 32177 0
vsize: 128872
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36350 0 0 0 72913 98 0 0 25 0 1 0 546321411 132362240 29849 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32315 29849 603 41 0 32274 0
vsize: 129260
[startup+740.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36465 0 0 0 73913 98 0 0 25 0 1 0 546321411 132886528 29964 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32443 29964 603 41 0 32402 0
vsize: 129772
[startup+750.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36564 0 0 0 74913 99 0 0 25 0 1 0 546321411 133279744 30063 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32539 30063 603 41 0 32498 0
vsize: 130156
[startup+760.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36656 0 0 0 75913 99 0 0 25 0 1 0 546321411 133701632 30155 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32642 30155 603 41 0 32601 0
vsize: 130568
[startup+770.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36747 0 0 0 76913 99 0 0 25 0 1 0 546321411 134094848 30246 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32738 30246 603 41 0 32697 0
vsize: 130952
[startup+780.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36844 0 0 0 77912 100 0 0 25 0 1 0 546321411 134492160 30343 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32835 30343 603 41 0 32794 0
vsize: 131340
[startup+790.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 36935 0 0 0 78912 100 0 0 25 0 1 0 546321411 134758400 30434 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32900 30434 603 41 0 32859 0
vsize: 131600
[startup+800.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37019 0 0 0 79912 100 0 0 25 0 1 0 546321411 135155712 30518 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32997 30518 603 41 0 32956 0
vsize: 131988
[startup+810.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37101 0 0 0 80912 100 0 0 25 0 1 0 546321411 135417856 30600 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33061 30600 603 41 0 33020 0
vsize: 132244
[startup+820.026 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37196 0 0 0 81912 101 0 0 25 0 1 0 546321411 135831552 30695 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33162 30695 603 41 0 33121 0
vsize: 132648
[startup+830.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37282 0 0 0 82912 101 0 0 25 0 1 0 546321411 136278016 30781 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33271 30781 603 41 0 33230 0
vsize: 133084
[startup+840.027 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37354 0 0 0 83912 101 0 0 25 0 1 0 546321411 136540160 30853 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33335 30853 603 41 0 33294 0
vsize: 133340
[startup+850.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37454 0 0 0 84912 101 0 0 25 0 1 0 546321411 136933376 30953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33431 30953 603 41 0 33390 0
vsize: 133724
[startup+860.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37544 0 0 0 85912 101 0 0 25 0 1 0 546321411 137330688 31043 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33528 31043 603 41 0 33487 0
vsize: 134112
[startup+870.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37645 0 0 0 86912 102 0 0 25 0 1 0 546321411 137728000 31144 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33625 31144 603 41 0 33584 0
vsize: 134500
[startup+880.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37717 0 0 0 87912 102 0 0 25 0 1 0 546321411 137990144 31216 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33689 31216 603 41 0 33648 0
vsize: 134756
[startup+890.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37804 0 0 0 88912 102 0 0 25 0 1 0 546321411 138407936 31303 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33791 31303 603 41 0 33750 0
vsize: 135164
[startup+900.029 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37894 0 0 0 89913 102 0 0 25 0 1 0 546321411 138674176 31393 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33856 31393 603 41 0 33815 0
vsize: 135424
[startup+910.028 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 37957 0 0 0 90912 102 0 0 25 0 1 0 546321411 138940416 31456 4294967295 134512640 134672761 3221224544 3221223688 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33921 31456 603 41 0 33880 0
vsize: 135684
[startup+920.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38052 0 0 0 91912 103 0 0 25 0 1 0 546321411 139374592 31551 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34027 31551 603 41 0 33986 0
vsize: 136108
[startup+930.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38157 0 0 0 92912 103 0 0 25 0 1 0 546321411 139804672 31656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34132 31656 603 41 0 34091 0
vsize: 136528
[startup+940.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38226 0 0 0 93912 103 0 0 25 0 1 0 546321411 140066816 31725 4294967295 134512640 134672761 3221224544 3221223728 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34196 31725 603 41 0 34155 0
vsize: 136784
[startup+950.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38299 0 0 0 94912 104 0 0 25 0 1 0 546321411 140333056 31798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34261 31798 603 41 0 34220 0
vsize: 137044
[startup+960.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38374 0 0 0 95911 104 0 0 25 0 1 0 546321411 140730368 31873 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34358 31873 603 41 0 34317 0
vsize: 137432
[startup+970.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38449 0 0 0 96911 105 0 0 25 0 1 0 546321411 140992512 31948 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34422 31948 603 41 0 34381 0
vsize: 137688
[startup+980.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38521 0 0 0 97911 105 0 0 25 0 1 0 546321411 141291520 32020 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34495 32020 603 41 0 34454 0
vsize: 137980
[startup+990.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38591 0 0 0 98911 105 0 0 25 0 1 0 546321411 141553664 32090 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34559 32090 603 41 0 34518 0
vsize: 138236
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38647 0 0 0 99911 106 0 0 25 0 1 0 546321411 141815808 32146 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34623 32146 603 41 0 34582 0
vsize: 138492
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38705 0 0 0 100911 106 0 0 25 0 1 0 546321411 142077952 32204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34687 32204 603 41 0 34646 0
vsize: 138748
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38762 0 0 0 101911 106 0 0 25 0 1 0 546321411 142213120 32261 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34720 32261 603 41 0 34679 0
vsize: 138880
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38842 0 0 0 102911 106 0 0 25 0 1 0 546321411 142696448 32341 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34838 32341 603 41 0 34797 0
vsize: 139352
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38928 0 0 0 103911 106 0 0 25 0 1 0 546321411 143142912 32427 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34947 32427 603 41 0 34906 0
vsize: 139788
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 38981 0 0 0 104911 106 0 0 25 0 1 0 546321411 143278080 32480 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34980 32480 603 41 0 34939 0
vsize: 139920
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39041 0 0 0 105911 107 0 0 25 0 1 0 546321411 143544320 32540 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35045 32540 603 41 0 35004 0
vsize: 140180
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39143 0 0 0 106911 107 0 0 25 0 1 0 546321411 143949824 32642 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35144 32642 603 41 0 35103 0
vsize: 140576
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39210 0 0 0 107911 107 0 0 25 0 1 0 546321411 144293888 32709 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35228 32709 603 41 0 35187 0
vsize: 140912
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39265 0 0 0 108911 107 0 0 25 0 1 0 546321411 144424960 32764 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35260 32764 603 41 0 35219 0
vsize: 141040
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39349 0 0 0 109911 108 0 0 25 0 1 0 546321411 144916480 32848 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35380 32848 603 41 0 35339 0
vsize: 141520
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39413 0 0 0 110911 108 0 0 25 0 1 0 546321411 145195008 32912 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35448 32912 603 41 0 35407 0
vsize: 141792
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39473 0 0 0 111911 108 0 0 25 0 1 0 546321411 145473536 32972 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35516 32972 603 41 0 35475 0
vsize: 142064
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39614 0 0 0 112910 108 0 0 25 0 1 0 546321411 145997824 33113 4294967295 134512640 134672761 3221224544 3221223728 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35644 33113 603 41 0 35603 0
vsize: 142576
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39835 0 0 0 113909 109 0 0 25 0 1 0 546321411 146919424 33334 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35869 33334 603 41 0 35828 0
vsize: 143476
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39906 0 0 0 114910 109 0 0 25 0 1 0 546321411 147181568 33405 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35933 33405 603 41 0 35892 0
vsize: 143732
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 39965 0 0 0 115910 109 0 0 25 0 1 0 546321411 147447808 33464 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35998 33464 603 41 0 35957 0
vsize: 143992
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 40059 0 0 0 116910 110 0 0 25 0 1 0 546321411 147841024 33558 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36094 33558 603 41 0 36053 0
vsize: 144376
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 40118 0 0 0 117909 110 0 0 25 0 1 0 546321411 147976192 33617 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36127 33617 603 41 0 36086 0
vsize: 144508
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 40174 0 0 0 118910 110 0 0 25 0 1 0 546321411 148238336 33673 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36191 33673 603 41 0 36150 0
vsize: 144764
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 21665
Raw data (stat): 21608 (minisat+) R 21607 18865 18864 0 -1 0 40250 0 0 0 119909 110 0 0 25 0 1 0 546321411 148500480 33749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36255 33749 603 41 0 36214 0
vsize: 145020
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 21665
Raw data (stat): 21608 (minisat+) Z 21607 18865 18864 0 -1 12 40250 0 0 0 119909 117 0 0 25 0 1 0 546321411 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.28
CPU user time (s): 1199.1
CPU system time (s): 1.17882
CPU usage (%): 100.015
Max. virtual memory (Kb): 145020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####