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/miplib3/normalized-mps-v2-13-7-mkc.opb
MD5SUM	b9e9aa470fdb3341d7e10860fcc70cec
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 15082

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 02:51:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18614 boxname=wulflinc21 idbench=1432 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b9e9aa470fdb3341d7e10860fcc70cec  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-mkc.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-mkc.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-mkc.opb
IDLAUNCH: 18614
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        790240 kB
Buffers:          6364 kB
Cached:         214840 kB
SwapCached:          0 kB
Active:          60932 kB
Inactive:       163156 kB
HighTotal:      131008 kB
HighFree:        68068 kB
LowTotal:       903652 kB
LowFree:        722172 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14780 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:11:10 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18614 7 1200.24 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.92 0.95 0.90 2/55 347
Raw data (stat): 347 (runsolver) R 346 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 418880332 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 3748 0 0 0 988 11 0 0 25 0 1 0 418880332 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.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 3748 0 0 0 1988 11 0 0 25 0 1 0 418880332 11464704 2322 4294967295 134512640 134672761 3221224544 3221222096 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+30.0015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 9905 0 0 0 2973 26 0 0 25 0 1 0 418880332 30777344 6821 4294967295 134512640 134672761 3221224544 3221214368 134605503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7514 6821 603 41 0 7473 0
vsize: 30056
[startup+40.0011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 24337 0 0 0 3935 64 0 0 25 0 1 0 418880332 93802496 20466 4294967295 134512640 134672761 3221224544 3221223088 134621062 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.0018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 26366 0 0 0 4930 69 0 0 25 0 1 0 418880332 90959872 19865 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22207 19865 603 41 0 22166 0
vsize: 88828
[startup+60.0015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 26802 0 0 0 5929 71 0 0 25 0 1 0 418880332 92667904 20301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22624 20301 603 41 0 22583 0
vsize: 90496
[startup+70.0022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 27316 0 0 0 6927 72 0 0 25 0 1 0 418880332 94863360 20815 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23160 20815 603 41 0 23119 0
vsize: 92640
[startup+80.0034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 27676 0 0 0 7926 73 0 0 25 0 1 0 418880332 96317440 21175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23515 21175 603 41 0 23474 0
vsize: 94060
[startup+90.0026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 28122 0 0 0 8925 74 0 0 25 0 1 0 418880332 98181120 21621 4294967295 134512640 134672761 3221224544 3221223744 134610667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23970 21621 603 41 0 23929 0
vsize: 95880
[startup+100.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 28467 0 0 0 9924 76 0 0 25 0 1 0 418880332 99635200 21966 4294967295 134512640 134672761 3221224544 3221223552 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24325 21966 603 41 0 24284 0
vsize: 97300
[startup+110.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 28804 0 0 0 10923 77 0 0 25 0 1 0 418880332 100954112 22303 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24647 22303 603 41 0 24606 0
vsize: 98588
[startup+120.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29096 0 0 0 11922 78 0 0 25 0 1 0 418880332 102141952 22595 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24937 22595 603 41 0 24896 0
vsize: 99748
[startup+130.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29371 0 0 0 12922 79 0 0 25 0 1 0 418880332 103190528 22870 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25193 22870 603 41 0 25152 0
vsize: 100772
[startup+140.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29561 0 0 0 13921 80 0 0 25 0 1 0 418880332 103989248 23060 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25388 23060 603 41 0 25347 0
vsize: 101552
[startup+150.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29667 0 0 0 14920 80 0 0 25 0 1 0 418880332 104390656 23166 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25486 23166 603 41 0 25445 0
vsize: 101944
[startup+160.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29764 0 0 0 15920 81 0 0 25 0 1 0 418880332 104787968 23263 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25583 23263 603 41 0 25542 0
vsize: 102332
[startup+170.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 29861 0 0 0 16920 81 0 0 25 0 1 0 418880332 105181184 23360 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25679 23360 603 41 0 25638 0
vsize: 102716
[startup+180.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30008 0 0 0 17919 82 0 0 25 0 1 0 418880332 106110976 23507 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25906 23507 603 41 0 25865 0
vsize: 103624
[startup+190.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30213 0 0 0 18919 82 0 0 25 0 1 0 418880332 106909696 23712 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26101 23712 603 41 0 26060 0
vsize: 104404
[startup+200.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30401 0 0 0 19918 83 0 0 25 0 1 0 418880332 107585536 23900 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26266 23900 603 41 0 26225 0
vsize: 105064
[startup+210.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30584 0 0 0 20918 84 0 0 25 0 1 0 418880332 108384256 24083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26461 24083 603 41 0 26420 0
vsize: 105844
[startup+220.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30750 0 0 0 21917 84 0 0 25 0 1 0 418880332 109043712 24249 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26622 24249 603 41 0 26581 0
vsize: 106488
[startup+230.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 30918 0 0 0 22917 85 0 0 25 0 1 0 418880332 109699072 24417 4294967295 134512640 134672761 3221224544 3221223584 134612981 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26782 24417 603 41 0 26741 0
vsize: 107128
[startup+240.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31073 0 0 0 23917 85 0 0 25 0 1 0 418880332 110370816 24572 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26946 24572 603 41 0 26905 0
vsize: 107784
[startup+250.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31184 0 0 0 24916 86 0 0 25 0 1 0 418880332 110764032 24683 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27042 24683 603 41 0 27001 0
vsize: 108168
[startup+260.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31340 0 0 0 25916 87 0 0 25 0 1 0 418880332 111468544 24839 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27214 24839 603 41 0 27173 0
vsize: 108856
[startup+270.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31486 0 0 0 26915 87 0 0 25 0 1 0 418880332 112017408 24985 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27348 24985 603 41 0 27307 0
vsize: 109392
[startup+280.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31640 0 0 0 27915 87 0 0 25 0 1 0 418880332 112709632 25139 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27517 25139 603 41 0 27476 0
vsize: 110068
[startup+290.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31784 0 0 0 28915 88 0 0 25 0 1 0 418880332 113233920 25283 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27645 25283 603 41 0 27604 0
vsize: 110580
[startup+300.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 31911 0 0 0 29915 88 0 0 25 0 1 0 418880332 113766400 25410 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 25410 603 41 0 27734 0
vsize: 111100
[startup+310.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32037 0 0 0 30915 88 0 0 25 0 1 0 418880332 114290688 25536 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27903 25536 603 41 0 27862 0
vsize: 111612
[startup+320.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32170 0 0 0 31915 88 0 0 25 0 1 0 418880332 114814976 25669 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28031 25669 603 41 0 27990 0
vsize: 112124
[startup+330.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32307 0 0 0 32915 89 0 0 25 0 1 0 418880332 115339264 25806 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28159 25806 603 41 0 28118 0
vsize: 112636
[startup+340.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32454 0 0 0 33914 89 0 0 25 0 1 0 418880332 115998720 25953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28320 25953 603 41 0 28279 0
vsize: 113280
[startup+350.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32611 0 0 0 34914 89 0 0 25 0 1 0 418880332 116658176 26110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28481 26110 603 41 0 28440 0
vsize: 113924
[startup+360 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32756 0 0 0 35914 90 0 0 25 0 1 0 418880332 117198848 26255 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28613 26255 603 41 0 28572 0
vsize: 114452
[startup+370 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 32906 0 0 0 36913 91 0 0 25 0 1 0 418880332 117854208 26405 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28773 26405 603 41 0 28732 0
vsize: 115092
[startup+380 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33014 0 0 0 37913 91 0 0 25 0 1 0 418880332 118263808 26513 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28873 26513 603 41 0 28832 0
vsize: 115492
[startup+389.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33101 0 0 0 38913 92 0 0 25 0 1 0 418880332 118657024 26600 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28969 26600 603 41 0 28928 0
vsize: 115876
[startup+400 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33201 0 0 0 39913 92 0 0 25 0 1 0 418880332 119054336 26700 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29066 26700 603 41 0 29025 0
vsize: 116264
[startup+410 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33326 0 0 0 40912 92 0 0 25 0 1 0 418880332 119586816 26825 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29196 26825 603 41 0 29155 0
vsize: 116784
[startup+420 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33475 0 0 0 41912 93 0 0 25 0 1 0 418880332 120119296 26974 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29326 26974 603 41 0 29285 0
vsize: 117304
[startup+430 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33586 0 0 0 42912 93 0 0 25 0 1 0 418880332 120659968 27085 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29458 27085 603 41 0 29417 0
vsize: 117832
[startup+440 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33682 0 0 0 43912 94 0 0 25 0 1 0 418880332 121053184 27181 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29554 27181 603 41 0 29513 0
vsize: 118216
[startup+450.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33774 0 0 0 44912 94 0 0 25 0 1 0 418880332 121450496 27273 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29651 27273 603 41 0 29610 0
vsize: 118604
[startup+460 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33874 0 0 0 45911 94 0 0 25 0 1 0 418880332 122372096 27373 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29876 27373 603 41 0 29835 0
vsize: 119504
[startup+470.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 33994 0 0 0 46911 94 0 0 25 0 1 0 418880332 122777600 27493 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29975 27493 603 41 0 29934 0
vsize: 119900
[startup+480.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34091 0 0 0 47911 95 0 0 25 0 1 0 418880332 123174912 27590 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30072 27590 603 41 0 30031 0
vsize: 120288
[startup+490 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34169 0 0 0 48911 95 0 0 25 0 1 0 418880332 123576320 27668 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30170 27668 603 41 0 30129 0
vsize: 120680
[startup+500.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34275 0 0 0 49911 95 0 0 25 0 1 0 418880332 123969536 27774 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30266 27774 603 41 0 30225 0
vsize: 121064
[startup+510.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34382 0 0 0 50911 95 0 0 25 0 1 0 418880332 124366848 27881 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30363 27881 603 41 0 30322 0
vsize: 121452
[startup+520.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34484 0 0 0 51910 96 0 0 25 0 1 0 418880332 124764160 27983 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30460 27983 603 41 0 30419 0
vsize: 121840
[startup+530.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 347
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34589 0 0 0 52910 96 0 0 25 0 1 0 418880332 125288448 28088 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30588 28088 603 41 0 30547 0
vsize: 122352
[startup+540.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34661 0 0 0 53910 97 0 0 25 0 1 0 418880332 125550592 28160 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30652 28160 603 41 0 30611 0
vsize: 122608
[startup+550 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34725 0 0 0 54909 97 0 0 25 0 1 0 418880332 125833216 28224 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30721 28224 603 41 0 30680 0
vsize: 122884
[startup+560.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34813 0 0 0 55909 98 0 0 25 0 1 0 418880332 126115840 28312 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30790 28312 603 41 0 30749 0
vsize: 123160
[startup+570.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 34907 0 0 0 56909 98 0 0 25 0 1 0 418880332 126509056 28406 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30886 28406 603 41 0 30845 0
vsize: 123544
[startup+580.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35010 0 0 0 57909 98 0 0 25 0 1 0 418880332 126906368 28509 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30983 28509 603 41 0 30942 0
vsize: 123932
[startup+590 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 400
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35104 0 0 0 58908 99 0 0 25 0 1 0 418880332 127299584 28603 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31079 28603 603 41 0 31038 0
vsize: 124316
[startup+600 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 402
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35195 0 0 0 59907 100 0 0 25 0 1 0 418880332 127696896 28694 4294967295 134512640 134672761 3221224544 3221223728 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31176 28694 603 41 0 31135 0
vsize: 124704
[startup+610 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35274 0 0 0 60907 100 0 0 25 0 1 0 418880332 127963136 28773 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31241 28773 603 41 0 31200 0
vsize: 124964
[startup+620.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35357 0 0 0 61907 100 0 0 25 0 1 0 418880332 128356352 28856 4294967295 134512640 134672761 3221224544 3221223688 134616167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31337 28856 603 41 0 31296 0
vsize: 125348
[startup+630.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35443 0 0 0 62907 101 0 0 25 0 1 0 418880332 128761856 28942 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31436 28942 603 41 0 31395 0
vsize: 125744
[startup+640.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35538 0 0 0 63906 102 0 0 25 0 1 0 418880332 129167360 29037 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31535 29037 603 41 0 31494 0
vsize: 126140
[startup+650.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35627 0 0 0 64906 102 0 0 25 0 1 0 418880332 129429504 29126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31599 29126 603 41 0 31558 0
vsize: 126396
[startup+660 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35721 0 0 0 65905 103 0 0 25 0 1 0 418880332 129826816 29220 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31696 29220 603 41 0 31655 0
vsize: 126784
[startup+670.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35808 0 0 0 66905 103 0 0 25 0 1 0 418880332 130224128 29307 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31793 29307 603 41 0 31752 0
vsize: 127172
[startup+680.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35906 0 0 0 67904 104 0 0 25 0 1 0 418880332 130617344 29405 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31889 29405 603 41 0 31848 0
vsize: 127556
[startup+690.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 35986 0 0 0 68904 104 0 0 25 0 1 0 418880332 130908160 29485 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31960 29485 603 41 0 31919 0
vsize: 127840
[startup+700.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36083 0 0 0 69904 105 0 0 25 0 1 0 418880332 131309568 29582 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32058 29582 603 41 0 32017 0
vsize: 128232
[startup+710.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36176 0 0 0 70904 105 0 0 25 0 1 0 418880332 131702784 29675 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32154 29675 603 41 0 32113 0
vsize: 128616
[startup+720 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36280 0 0 0 71904 105 0 0 25 0 1 0 418880332 132096000 29779 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32250 29779 603 41 0 32209 0
vsize: 129000
[startup+730 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36392 0 0 0 72904 105 0 0 25 0 1 0 418880332 132624384 29891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32379 29891 603 41 0 32338 0
vsize: 129516
[startup+740 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36504 0 0 0 73903 106 0 0 25 0 1 0 418880332 133017600 30003 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32475 30003 603 41 0 32434 0
vsize: 129900
[startup+750.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36600 0 0 0 74903 106 0 0 25 0 1 0 418880332 133439488 30099 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32578 30099 603 41 0 32537 0
vsize: 130312
[startup+760 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36687 0 0 0 75903 106 0 0 25 0 1 0 418880332 133832704 30186 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32674 30186 603 41 0 32633 0
vsize: 130696
[startup+770 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36786 0 0 0 76903 107 0 0 25 0 1 0 418880332 134225920 30285 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32770 30285 603 41 0 32729 0
vsize: 131080
[startup+780 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36877 0 0 0 77903 107 0 0 25 0 1 0 418880332 134627328 30376 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32868 30376 603 41 0 32827 0
vsize: 131472
[startup+789.999 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 36968 0 0 0 78903 107 0 0 25 0 1 0 418880332 134889472 30467 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32932 30467 603 41 0 32891 0
vsize: 131728
[startup+800 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37051 0 0 0 79902 108 0 0 25 0 1 0 418880332 135286784 30550 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33029 30550 603 41 0 32988 0
vsize: 132116
[startup+810 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37137 0 0 0 80902 108 0 0 25 0 1 0 418880332 135548928 30636 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33093 30636 603 41 0 33052 0
vsize: 132372
[startup+820.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37226 0 0 0 81902 108 0 0 25 0 1 0 418880332 135962624 30725 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33194 30725 603 41 0 33153 0
vsize: 132776
[startup+830 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37309 0 0 0 82902 109 0 0 25 0 1 0 418880332 136278016 30808 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33271 30808 603 41 0 33230 0
vsize: 133084
[startup+840 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37395 0 0 0 83902 109 0 0 25 0 1 0 418880332 136671232 30894 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33367 30894 603 41 0 33326 0
vsize: 133468
[startup+850 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 404
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37495 0 0 0 84901 109 0 0 25 0 1 0 418880332 137064448 30994 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33463 30994 603 41 0 33422 0
vsize: 133852
[startup+860 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37590 0 0 0 85900 111 0 0 25 0 1 0 418880332 137465856 31089 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33561 31089 603 41 0 33520 0
vsize: 134244
[startup+870 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37676 0 0 0 86900 111 0 0 25 0 1 0 418880332 137859072 31175 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33657 31175 603 41 0 33616 0
vsize: 134628
[startup+880.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37757 0 0 0 87900 112 0 0 25 0 1 0 418880332 138121216 31256 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33721 31256 603 41 0 33680 0
vsize: 134884
[startup+890 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37849 0 0 0 88899 112 0 0 25 0 1 0 418880332 138539008 31348 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33823 31348 603 41 0 33782 0
vsize: 135292
[startup+900 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 37934 0 0 0 89899 112 0 0 25 0 1 0 418880332 138809344 31433 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33889 31433 603 41 0 33848 0
vsize: 135556
[startup+910.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38007 0 0 0 90899 112 0 0 25 0 1 0 418880332 139243520 31506 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33995 31506 603 41 0 33954 0
vsize: 135980
[startup+920.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38106 0 0 0 91899 112 0 0 25 0 1 0 418880332 139538432 31605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34067 31605 603 41 0 34026 0
vsize: 136268
[startup+930.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38193 0 0 0 92899 113 0 0 25 0 1 0 418880332 139935744 31692 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34164 31692 603 41 0 34123 0
vsize: 136656
[startup+940.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38267 0 0 0 93899 113 0 0 25 0 1 0 418880332 140197888 31766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34228 31766 603 41 0 34187 0
vsize: 136912
[startup+950.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38344 0 0 0 94898 114 0 0 25 0 1 0 418880332 140599296 31843 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34326 31843 603 41 0 34285 0
vsize: 137304
[startup+960.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38411 0 0 0 95898 114 0 0 25 0 1 0 418880332 140861440 31910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34390 31910 603 41 0 34349 0
vsize: 137560
[startup+970.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38492 0 0 0 96898 115 0 0 25 0 1 0 418880332 141148160 31991 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34460 31991 603 41 0 34419 0
vsize: 137840
[startup+980.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38564 0 0 0 97898 115 0 0 25 0 1 0 418880332 141422592 32063 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34527 32063 603 41 0 34486 0
vsize: 138108
[startup+990.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38624 0 0 0 98898 115 0 0 25 0 1 0 418880332 141684736 32123 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34591 32123 603 41 0 34550 0
vsize: 138364
[startup+1000 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38681 0 0 0 99898 115 0 0 25 0 1 0 418880332 141946880 32180 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34655 32180 603 41 0 34614 0
vsize: 138620
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38743 0 0 0 100897 116 0 0 25 0 1 0 418880332 142213120 32242 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34720 32242 603 41 0 34679 0
vsize: 138880
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38797 0 0 0 101897 116 0 0 25 0 1 0 418880332 142344192 32296 4294967295 134512640 134672761 3221224544 3221223688 134616126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34752 32296 603 41 0 34711 0
vsize: 139008
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38900 0 0 0 102897 117 0 0 25 0 1 0 418880332 142979072 32399 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34907 32399 603 41 0 34866 0
vsize: 139628
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 38953 0 0 0 103897 117 0 0 25 0 1 0 418880332 143142912 32452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34947 32452 603 41 0 34906 0
vsize: 139788
[startup+1050 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39019 0 0 0 104897 117 0 0 25 0 1 0 418880332 143409152 32518 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35012 32518 603 41 0 34971 0
vsize: 140048
[startup+1060 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39079 0 0 0 105897 117 0 0 25 0 1 0 418880332 143675392 32578 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35077 32578 603 41 0 35036 0
vsize: 140308
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39205 0 0 0 106896 118 0 0 25 0 1 0 418880332 144293888 32704 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35228 32704 603 41 0 35187 0
vsize: 140912
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39241 0 0 0 107896 118 0 0 25 0 1 0 418880332 144424960 32740 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35260 32740 603 41 0 35219 0
vsize: 141040
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39314 0 0 0 108897 118 0 0 25 0 1 0 418880332 144687104 32813 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35324 32813 603 41 0 35283 0
vsize: 141296
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39391 0 0 0 109897 118 0 0 25 0 1 0 418880332 145047552 32890 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35412 32890 603 41 0 35371 0
vsize: 141648
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39454 0 0 0 110897 118 0 0 25 0 1 0 418880332 145342464 32953 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35484 32953 603 41 0 35443 0
vsize: 141936
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39522 0 0 0 111896 119 0 0 25 0 1 0 418880332 145604608 33021 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35548 33021 603 41 0 35507 0
vsize: 142192
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39810 0 0 0 112896 119 0 0 25 0 1 0 418880332 146788352 33309 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35837 33309 603 41 0 35796 0
vsize: 143348
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39885 0 0 0 113896 120 0 0 25 0 1 0 418880332 147050496 33384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35901 33384 603 41 0 35860 0
vsize: 143604
[startup+1150 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 39953 0 0 0 114896 120 0 0 25 0 1 0 418880332 147316736 33452 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35966 33452 603 41 0 35925 0
vsize: 143864
[startup+1160 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 40048 0 0 0 115895 120 0 0 25 0 1 0 418880332 147709952 33547 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36062 33547 603 41 0 36021 0
vsize: 144248
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 40104 0 0 0 116895 121 0 0 25 0 1 0 418880332 147976192 33603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36127 33603 603 41 0 36086 0
vsize: 144508
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 40157 0 0 0 117895 121 0 0 25 0 1 0 418880332 148238336 33656 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36191 33656 603 41 0 36150 0
vsize: 144764
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 40231 0 0 0 118895 121 0 0 25 0 1 0 418880332 148500480 33730 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36255 33730 603 41 0 36214 0
vsize: 145020
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 406
Raw data (stat): 347 (minisat+) R 346 30927 30926 0 -1 0 40298 0 0 0 119895 121 0 0 25 0 1 0 418880332 148766720 33797 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36320 33797 603 41 0 36279 0
vsize: 145280
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.97 0.91 1/55 406
Raw data (stat): 347 (minisat+) Z 346 30927 30926 0 -1 12 40298 0 0 0 119895 128 0 0 25 0 1 0 418880332 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.24
CPU user time (s): 1198.95
CPU system time (s): 1.2878
CPU usage (%): 100.014
Max. virtual memory (Kb): 145280
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####