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/submitted/een/normalized-p0282.opb
MD5SUM	dd62132555621025f45a5a6099c90742
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	282
Total number of constraints	221
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	44
Minimum length of a constraint	2
Maximum length of a constraint	57
Trace number 6993

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 20:50:41 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5049 boxname=wulflinc9 idbench=389 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  dd62132555621025f45a5a6099c90742  /oldhome/oroussel/tmp/wulflinc9/normalized-p0282.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc9/normalized-p0282.opb
IDLAUNCH: 5049
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        861464 kB
Buffers:         37088 kB
Cached:         115552 kB
SwapCached:        564 kB
Active:          61744 kB
Inactive:        94340 kB
HighTotal:      131008 kB
HighFree:        11536 kB
LowTotal:       903652 kB
LowFree:        849928 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11536 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:10:43 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 5049 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss
c ---[  46]---> BDD-cost:    4
c ---[  45]---> BDD-cost:    8
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   16
c ---[  42]---> Sorter-cost: 1109     Base: 2 5 3 3
c ---[  41]---> Sorter-cost:  898     Base: 2 5 3 2
c ---[  40]---> Sorter-cost: 1118     Base: 2 5 5
c ---[  38]---> Sorter-cost: 1012     Base: 2 5 5
c ---[  37]---> Sorter-cost:  910     Base: 2 5 5
c ---[  36]---> Sorter-cost:  998     Base: 2 5 3 2
c ---[  35]---> Sorter-cost:  852     Base: 2 5 3 3
c ---[  34]---> Sorter-cost:  843     Base: 5 2 3 3
c ---[  33]---> Sorter-cost:  713     Base: 5 2 3 3
c ---[  32]---> Sorter-cost:  948     Base: 2 5 3 3
c ---[  31]---> Sorter-cost:  841     Base: 2 5 3 3
c ---[  30]---> Sorter-cost:  909     Base: 2 5 5
c ---[  29]---> Sorter-cost:  935     Base: 2 5 3 2
c ---[  28]---> Sorter-cost:  998     Base: 2 5 3
c ---[  27]---> Sorter-cost:  763     Base: 5 2 3 3
c ---[  26]---> Sorter-cost:  910     Base: 2 5 5
c ---[  25]---> Sorter-cost:  909     Base: 2 5 5
c ---[  24]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  23]---> Sorter-cost:  909     Base: 2 5 5
c ---[  22]---> Sorter-cost:  909     Base: 2 5 5
c ---[  21]---> Sorter-cost: 1008     Base: 2 5 3
c ---[  20]---> Sorter-cost:  898     Base: 2 5 3 3
c ---[  19]---> Sorter-cost:  843     Base: 2 5 3 3
c ---[  18]---> Sorter-cost:  760     Base: 2 5 3 3
c ---[  17]---> Sorter-cost:  714     Base: 5 2 3 3
c ---[  16]---> Sorter-cost: 1071     Base: 2 5 3 3
c ---[  15]---> Sorter-cost:  949     Base: 2 5 3 3
c ---[  14]---> BDD-cost:   26
c ---[  13]---> Sorter-cost: 1108     Base: 2 5 3 3
c ---[  11]---> Sorter-cost: 1081     Base: 2 5 3 3
c ---[  10]---> Sorter-cost:  999     Base: 2 5 3 2
c ---[   9]---> Sorter-cost:  995     Base: 2 5 3 3
c ---[   8]---> Sorter-cost:  982     Base: 2 5 3 2
c ---[   7]---> Sorter-cost:  996     Base: 2 5 3 3
c ---[   5]---> BDD-cost:   56
c ---[   4]---> BDD-cost:   56
c ---[   3]---> BDD-cost:   56
c ---[   2]---> BDD-cost:   12
c ---[   1]---> Sorter-cost:  719     Base: 2 5 3
c ---[   0]---> Sorter-cost:  657     Base: 2 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70259   164905 |   23419       0        0     nan |  0.000 % |
c |       100 |   70095   164539 |   25760      95      543     5.7 |  0.350 % |
c ==============================================================================
c [1mFound solution: 724525[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:77310     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       142 |  288791   675552 |   96263     133      783     5.9 |  0.350 % |
c |       243 |  288753   675469 |  105889     232     8890    38.3 |  0.135 % |
c |       394 |  288753   675469 |  116478     383     9895    25.8 |  0.135 % |
c |       619 |  288729   675415 |  128126     606    11903    19.6 |  0.141 % |
c |       958 |  288729   675415 |  140938     945    14339    15.2 |  0.141 % |
c |      1464 |  288729   675415 |  155032    1451    22778    15.7 |  0.141 % |
c |      2223 |  288729   675415 |  170535    2210    29879    13.5 |  0.141 % |
c ==============================================================================
c [1mFound solution: 684888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2898 |  289763   678459 |   96587    2885    40586    14.1 |  0.141 % |
c |      2998 |  289763   678459 |  106245    2985    41152    13.8 |  0.142 % |
c |      3148 |  289763   678459 |  116870    3135    43697    13.9 |  0.142 % |
c |      3373 |  289541   677962 |  128557    3358    44882    13.4 |  0.198 % |
c |      3710 |  289541   677962 |  141413    3695    47359    12.8 |  0.198 % |
c |      4216 |  289339   677507 |  155554    4195    50487    12.0 |  0.253 % |
c |      4978 |  289125   677025 |  171109    4944    76497    15.5 |  0.311 % |
c |      6118 |  289125   677025 |  188220    6084    89395    14.7 |  0.311 % |
c |      7826 |  289085   676937 |  207042    7791   116144    14.9 |  0.322 % |
c |     10388 |  289085   676937 |  227747   10353   151098    14.6 |  0.322 % |
c ==============================================================================
c [1mFound solution: 578178[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10739 |  289932   679099 |   96644   10704   153297    14.3 |  0.322 % |
c |     10839 |  289932   679099 |  106308   10804   154269    14.3 |  0.322 % |
c |     10990 |  289928   679090 |  116939   10954   160300    14.6 |  0.323 % |
c |     11215 |  289928   679090 |  128633   11179   162352    14.5 |  0.323 % |
c |     11552 |  289928   679090 |  141496   11516   167498    14.5 |  0.323 % |
c |     12058 |  289928   679090 |  155646   12022   172787    14.4 |  0.323 % |
c |     12818 |  289858   678932 |  171210   12778   196199    15.4 |  0.341 % |
c |     13957 |  289738   678664 |  188331   13914   232109    16.7 |  0.374 % |
c |     15665 |  289696   678572 |  207164   15620   308337    19.7 |  0.386 % |
c ==============================================================================
c [1mFound solution: 578177[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16131 |  290070   679650 |   96690   16086   349262    21.7 |  0.386 % |
c |     16232 |  290070   679650 |  106359   16187   349838    21.6 |  0.386 % |
c |     16382 |  290070   679650 |  116994   16336   353008    21.6 |  0.390 % |
c |     16607 |  289264   677819 |  128694   16465   356427    21.6 |  0.617 % |
c |     16947 |  289230   677742 |  141563   16804   360762    21.5 |  0.626 % |
c |     17454 |  289107   677464 |  155720   17303   381114    22.0 |  0.660 % |
c |     18213 |  288887   676961 |  171292   18052   397830    22.0 |  0.728 % |
c |     19352 |  288857   676894 |  188421   19189   409056    21.3 |  0.737 % |
c |     21060 |  288746   676646 |  207263   20894   426690    20.4 |  0.765 % |
c |     23622 |  288732   676614 |  227989   23455   466524    19.9 |  0.769 % |
c ==============================================================================
c [1mFound solution: 575263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25123 |  288831   676860 |   96277   24955   513620    20.6 |  0.769 % |
c |     25224 |  288831   676860 |  105904   25056   514371    20.5 |  0.778 % |
c |     25374 |  288831   676860 |  116495   25206   515438    20.4 |  0.778 % |
c |     25600 |  288787   676761 |  128144   25429   518957    20.4 |  0.789 % |
c |     25937 |  288787   676761 |  140959   25766   526390    20.4 |  0.789 % |
c |     26443 |  288787   676761 |  155055   26272   555169    21.1 |  0.789 % |
c |     27203 |  288762   676706 |  170560   27028   566266    21.0 |  0.796 % |
c |     28343 |  288762   676706 |  187616   28168   586098    20.8 |  0.796 % |
c ==============================================================================
c [1mFound solution: 509328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28688 |  288797   676820 |   96265   28513   590359    20.7 |  0.796 % |
c |     28788 |  288797   676820 |  105891   28613   591371    20.7 |  0.797 % |
c |     28938 |  288797   676820 |  116480   28763   594191    20.7 |  0.797 % |
c |     29164 |  288797   676820 |  128128   28989   603627    20.8 |  0.797 % |
c |     29501 |  288797   676820 |  140941   29326   625029    21.3 |  0.797 % |
c |     30007 |  288556   676287 |  155035   29823   636972    21.4 |  0.868 % |
c |     30766 |  288512   676187 |  170539   30578   647058    21.2 |  0.880 % |
c |     31905 |  288402   675935 |  187593   31706   733123    23.1 |  0.913 % |
c ==============================================================================
c [1mFound solution: 463296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32344 |  288083   675214 |   96027   31915   736457    23.1 |  0.913 % |
c |     32444 |  288083   675214 |  105629   32015   737041    23.0 |  1.009 % |
c |     32596 |  288083   675214 |  116192   32167   742942    23.1 |  1.009 % |
c |     32821 |  287968   674955 |  127811   32386   744476    23.0 |  1.042 % |
c |     33158 |  287929   674866 |  140593   32717   746579    22.8 |  1.053 % |
c |     33666 |  287921   674847 |  154652   33224   755861    22.8 |  1.056 % |
c |     34425 |  287871   674735 |  170117   33982   817024    24.0 |  1.069 % |
c |     35565 |  287757   674474 |  187129   35112   858665    24.5 |  1.101 % |
c ==============================================================================
c [1mFound solution: 463295[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36196 |  287774   674592 |   95924   35743   948772    26.5 |  1.101 % |
c |     36296 |  287757   674554 |  105516   35842   949543    26.5 |  1.107 % |
c |     36448 |  287757   674554 |  116068   35994   950740    26.4 |  1.107 % |
c |     36674 |  287757   674554 |  127674   36220   951915    26.3 |  1.107 % |
c |     37011 |  287757   674554 |  140442   36557   959994    26.3 |  1.107 % |
c |     37517 |  287753   674545 |  154486   37062   963704    26.0 |  1.108 % |
c |     38276 |  287753   674545 |  169935   37821   971452    25.7 |  1.108 % |
c |     39415 |  287676   674372 |  186928   38949  1000029    25.7 |  1.132 % |
c |     41123 |  287676   674372 |  205621   40657  1054468    25.9 |  1.132 % |
c |     43685 |  287611   674228 |  226183   43217  1437731    33.3 |  1.151 % |
c |     47529 |  287460   673886 |  248802   47054  1525178    32.4 |  1.194 % |
c |     53297 |  287427   673813 |  273682   52820  1918118    36.3 |  1.205 % |
c |     61946 |  287032   672932 |  301050   61458  2278466    37.1 |  1.312 % |
c ==============================================================================
c [1mFound solution: 441120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66730 |  286585   671910 |   95528   65738  2524196    38.4 |  1.312 % |
c |     66830 |  286585   671910 |  105080   65838  2525363    38.4 |  1.452 % |
c |     66982 |  286585   671910 |  115588   65990  2536009    38.4 |  1.451 % |
c |     67208 |  286568   671872 |  127147   66215  2540611    38.4 |  1.456 % |
c ==============================================================================
c [1mFound solution: 441117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67312 |  286586   671913 |   95528   66319  2549906    38.4 |  1.456 % |
c |     67413 |  286586   671913 |  105080   66420  2551175    38.4 |  1.457 % |
c ==============================================================================
c [1mFound solution: 440937[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67541 |  286492   671814 |   95497   66542  2554718    38.4 |  1.457 % |
c |     67642 |  286465   671754 |  105046   66642  2555460    38.3 |  1.494 % |
c |     67792 |  286465   671754 |  115551   66792  2571498    38.5 |  1.494 % |
c |     68019 |  286465   671754 |  127106   67019  2582435    38.5 |  1.494 % |
c |     68358 |  286430   671676 |  139817   67352  2603548    38.7 |  1.505 % |
c |     68864 |  286430   671676 |  153798   67858  2672535    39.4 |  1.505 % |
c |     69623 |  286430   671676 |  169178   68617  2690831    39.2 |  1.505 % |
c |     70762 |  286430   671676 |  186096   69756  2709565    38.8 |  1.505 % |
c |     72470 |  286338   671470 |  204706   71460  2796432    39.1 |  1.530 % |
c |     75033 |  286338   671470 |  225176   74023  2896818    39.1 |  1.530 % |
c ==============================================================================
c [1mFound solution: 440714[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76507 |  286257   671290 |   95419   75496  2924689    38.7 |  1.530 % |
c |     76607 |  286257   671290 |  104960   75596  2928665    38.7 |  1.555 % |
c |     76760 |  286257   671290 |  115456   75749  2933128    38.7 |  1.555 % |
c |     76986 |  286257   671290 |  127002   75975  2942362    38.7 |  1.555 % |
c |     77323 |  286257   671290 |  139702   76312  2951490    38.7 |  1.555 % |
c |     77829 |  286257   671290 |  153673   76818  2970849    38.7 |  1.555 % |
c |     78588 |  286230   671231 |  169040   77569  2979297    38.4 |  1.563 % |
c |     79727 |  286230   671231 |  185944   78708  3024430    38.4 |  1.563 % |
c |     81435 |  286230   671231 |  204539   80416  3130463    38.9 |  1.563 % |
c |     83997 |  286173   671104 |  224993   82976  3189961    38.4 |  1.577 % |
c |     87842 |  286173   671104 |  247492   86821  3495106    40.3 |  1.577 % |
c ==============================================================================
c [1mFound solution: 436562[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88784 |  286180   671128 |   95393   87763  3571401    40.7 |  1.577 % |
c |     88884 |  286180   671128 |  104932   87863  3574534    40.7 |  1.578 % |
c |     89034 |  286180   671128 |  115425   88013  3575802    40.6 |  1.578 % |
c |     89259 |  286180   671128 |  126968   88238  3581269    40.6 |  1.578 % |
c |     89599 |  286180   671128 |  139664   88578  3589720    40.5 |  1.578 % |
c |     90105 |  286180   671128 |  153631   89084  3612909    40.6 |  1.578 % |
c |     90864 |  286151   671060 |  168994   89842  3641246    40.5 |  1.585 % |
c |     92003 |  286151   671060 |  185893   90981  3697182    40.6 |  1.585 % |
c |     93712 |  286151   671060 |  204483   92690  3792373    40.9 |  1.585 % |
c ==============================================================================
c [1mFound solution: 427815[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     94016 |  286157   671074 |   95385   92994  3818233    41.1 |  1.585 % |
c |     94117 |  286157   671074 |  104923   93095  3819543    41.0 |  1.586 % |
c |     94267 |  286157   671074 |  115415   93245  3825171    41.0 |  1.586 % |
c |     94494 |  286157   671074 |  126957   93472  3827815    41.0 |  1.586 % |
c |     94831 |  286157   671074 |  139653   93809  3831738    40.8 |  1.586 % |
c |     95337 |  286157   671074 |  153618   94315  3837485    40.7 |  1.586 % |
c |     96097 |  286157   671074 |  168980   95075  3871909    40.7 |  1.586 % |
c |     97236 |  286157   671074 |  185878   96214  3892235    40.5 |  1.586 % |
c |     98945 |  286157   671074 |  204466   97923  3931458    40.1 |  1.586 % |
c |    101507 |  286093   670930 |  224912  100484  4098561    40.8 |  1.602 % |
c |    105351 |  286021   670769 |  247404  104327  4254002    40.8 |  1.621 % |
c ==============================================================================
c [1mFound solution: 424422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107116 |  286034   670798 |   95344  106092  4384417    41.3 |  1.621 % |
c |    107217 |  286034   670798 |  104878   31750   635393    20.0 |  1.622 % |
c |    107367 |  286034   670798 |  115366   31900   640752    20.1 |  1.622 % |
c |    107594 |  286034   670798 |  126902   32127   642350    20.0 |  1.622 % |
c |    107936 |  286034   670798 |  139593   32469   651840    20.1 |  1.622 % |
c ==============================================================================
c [1mFound solution: 423440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108099 |  286041   670820 |   95347   32632   658158    20.2 |  1.622 % |
c |    108199 |  286041   670820 |  104881   32732   661867    20.2 |  1.623 % |
c |    108349 |  286041   670820 |  115369   32882   670390    20.4 |  1.623 % |
c |    108574 |  285965   670649 |  126906   33106   676906    20.4 |  1.642 % |
c |    108913 |  285965   670649 |  139597   33445   680004    20.3 |  1.642 % |
c ==============================================================================
c [1mFound solution: 382543[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109317 |  285834   670364 |   95278   33838   707994    20.9 |  1.642 % |
c |    109417 |  285834   670364 |  104805   33938   710354    20.9 |  1.689 % |
c |    109567 |  285834   670364 |  115286   34088   726522    21.3 |  1.689 % |
c |    109792 |  285834   670364 |  126815   34313   732419    21.3 |  1.689 % |
c |    110130 |  285834   670364 |  139496   34651   736312    21.2 |  1.689 % |
c |    110636 |  285811   670314 |  153446   35151   754513    21.5 |  1.695 % |
c |    111395 |  285784   670252 |  168790   35908   764162    21.3 |  1.703 % |
c |    112534 |  285784   670252 |  185669   37047   806769    21.8 |  1.703 % |
c |    114243 |  285731   670133 |  204236   38752   928384    24.0 |  1.717 % |
c ==============================================================================
c [1mFound solution: 381645[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    115623 |  285719   670115 |   95239   40130  1107869    27.6 |  1.717 % |
c |    115723 |  285719   670115 |  104762   40230  1108982    27.6 |  1.725 % |
c |    115875 |  285719   670115 |  115239   40382  1110196    27.5 |  1.725 % |
c |    116101 |  285707   670088 |  126763   40606  1112014    27.4 |  1.728 % |
c |    116438 |  285707   670088 |  139439   40943  1136156    27.7 |  1.728 % |
c |    116944 |  285707   670088 |  153383   41449  1142861    27.6 |  1.728 % |
c |    117703 |  285707   670088 |  168721   42208  1156172    27.4 |  1.728 % |
c |    118843 |  285707   670088 |  185593   43348  1226016    28.3 |  1.728 % |
c |    120553 |  285707   670088 |  204153   45058  1287861    28.6 |  1.728 % |
c |    123115 |  285610   669871 |  224568   47618  1476244    31.0 |  1.756 % |
c ==============================================================================
c [1mFound solution: 341794[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123277 |  285620   669898 |   95206   47780  1498747    31.4 |  1.756 % |
c |    123377 |  285564   669768 |  104726   47878  1499197    31.3 |  1.775 % |
c |    123530 |  285564   669768 |  115199   48031  1499987    31.2 |  1.775 % |
c |    123755 |  285564   669768 |  126719   48256  1513855    31.4 |  1.775 % |
c |    124092 |  285564   669768 |  139391   48593  1546362    31.8 |  1.775 % |
c |    124598 |  285495   669612 |  153330   49098  1632060    33.2 |  1.794 % |
c ==============================================================================
c [1mFound solution: 340199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125084 |  285508   669644 |   95169   49584  1674676    33.8 |  1.794 % |
c |    125184 |  285508   669644 |  104685   49684  1676540    33.7 |  1.794 % |
c |    125334 |  285508   669644 |  115154   49834  1678062    33.7 |  1.794 % |
c |    125559 |  285461   669536 |  126669   50058  1680694    33.6 |  1.807 % |
c |    125896 |  285461   669536 |  139336   50395  1695835    33.7 |  1.807 % |
c |    126402 |  285461   669536 |  153270   50901  1703452    33.5 |  1.807 % |
c |    127163 |  285461   669536 |  168597   51662  1715031    33.2 |  1.807 % |
c |    128302 |  285368   669321 |  185457   52790  1806817    34.2 |  1.838 % |
c |    130010 |  285256   669067 |  204003   54497  1934305    35.5 |  1.865 % |
c |    132573 |  285235   669021 |  224403   57059  2172307    38.1 |  1.871 % |
c |    136417 |  285235   669021 |  246843   60903  2353067    38.6 |  1.871 % |
c ==============================================================================
c [1mFound solution: 340198[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137442 |  285209   668966 |   95069   61925  2410980    38.9 |  1.871 % |
c |    137543 |  285209   668966 |  104575   62026  2412693    38.9 |  1.885 % |
c |    137693 |  285209   668966 |  115033   62176  2414448    38.8 |  1.885 % |
c |    137918 |  285209   668966 |  126536   62401  2428672    38.9 |  1.885 % |
c |    138255 |  285111   668744 |  139190   62725  2431134    38.8 |  1.907 % |
c |    138761 |  285111   668744 |  153109   63231  2443067    38.6 |  1.907 % |
c |    139521 |  285111   668744 |  168420   63991  2459033    38.4 |  1.907 % |
c |    140660 |  284989   668462 |  185262   65118  2524989    38.8 |  1.945 % |
c ==============================================================================
c [1mFound solution: 331503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    142111 |  284997   668485 |   94999   66569  2656790    39.9 |  1.945 % |
c |    142213 |  284862   668180 |  104498   66665  2657300    39.9 |  1.983 % |
c |    142363 |  284862   668180 |  114948   66815  2658278    39.8 |  1.983 % |
c |    142588 |  284862   668180 |  126443   67040  2663187    39.7 |  1.983 % |
c |    142925 |  284856   668166 |  139088   67374  2671148    39.6 |  1.985 % |
c |    143433 |  284832   668111 |  152996   67878  2680184    39.5 |  1.992 % |
c |    144192 |  284717   667847 |  168296   68496  2714972    39.6 |  2.027 % |
c |    145331 |  284666   667731 |  185126   69634  2873119    41.3 |  2.040 % |
c ==============================================================================
c [1mFound solution: 331424[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    145849 |  284674   667754 |   94891   70152  2926480    41.7 |  2.040 % |
c |    145949 |  284674   667754 |  104380   70252  2927403    41.7 |  2.041 % |
c |    146100 |  284674   667754 |  114818   70403  2935391    41.7 |  2.041 % |
c |    146325 |  284674   667754 |  126299   70628  2953818    41.8 |  2.041 % |
c ==============================================================================
c [1mFound solution: 327213[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146659 |  284681   667770 |   94893   70962  2972612    41.9 |  2.041 % |
c |    146760 |  284681   667770 |  104382   71063  2973029    41.8 |  2.042 % |
c |    146910 |  284681   667770 |  114820   71213  2978813    41.8 |  2.042 % |
c |    147135 |  284681   667770 |  126302   71438  2996160    41.9 |  2.042 % |
c |    147476 |  284681   667770 |  138932   71779  3025354    42.1 |  2.042 % |
c |    147983 |  284681   667770 |  152826   72286  3044149    42.1 |  2.042 % |
c |    148742 |  284681   667770 |  168108   73045  3097983    42.4 |  2.042 % |
c |    149883 |  284681   667770 |  184919   74186  3162243    42.6 |  2.042 % |
c ==============================================================================
c [1mFound solution: 327131[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150630 |  284692   667798 |   94897   74933  3185990    42.5 |  2.042 % |
c |    150730 |  284692   667798 |  104386   75033  3186692    42.5 |  2.043 % |
c |    150882 |  284692   667798 |  114825   75185  3187726    42.4 |  2.043 % |
c |    151107 |  284692   667798 |  126307   75410  3208813    42.6 |  2.043 % |
c |    151444 |  284692   667798 |  138938   75747  3228407    42.6 |  2.043 % |
c |    151951 |  284692   667798 |  152832   76254  3257739    42.7 |  2.043 % |
c |    152713 |  284692   667798 |  168115   77016  3302679    42.9 |  2.043 % |
c |    153852 |  284692   667798 |  184927   78155  3354572    42.9 |  2.043 % |
c ==============================================================================
c [1mFound solution: 321381[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    154732 |  284691   667796 |   94897   79032  3377809    42.7 |  2.043 % |
c |    154832 |  284691   667796 |  104386   79132  3384729    42.8 |  2.046 % |
c |    154983 |  284691   667796 |  114825   79283  3389556    42.8 |  2.046 % |
c |    155209 |  284691   667796 |  126307   79509  3416182    43.0 |  2.046 % |
c |    155546 |  284691   667796 |  138938   79846  3420798    42.8 |  2.046 % |
c |    156053 |  284691   667796 |  152832   80353  3426988    42.6 |  2.046 % |
c |    156812 |  284691   667796 |  168115   81112  3436621    42.4 |  2.046 % |
c |    157951 |  284629   667654 |  184927   82250  3519564    42.8 |  2.064 % |
c ==============================================================================
c [1mFound solution: 321358[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    159428 |  284640   667682 |   94880   83727  3658549    43.7 |  2.064 % |
c |    159528 |  284640   667682 |  104368   83827  3660023    43.7 |  2.065 % |
c |    159678 |  284640   667682 |  114804   83977  3685394    43.9 |  2.065 % |
c |    159907 |  284640   667682 |  126285   84206  3700321    43.9 |  2.065 % |
c |    160245 |  284640   667682 |  138913   84544  3721122    44.0 |  2.065 % |
c |    160751 |  284640   667682 |  152805   85050  3770877    44.3 |  2.065 % |
c |    161511 |  284586   667559 |  168085   85805  3803929    44.3 |  2.079 % |
c |    162651 |  284565   667512 |  184894   86944  3923709    45.1 |  2.084 % |
c |    164359 |  284546   667470 |  203383   88651  4062953    45.8 |  2.089 % |
c |    166921 |  284546   667470 |  223722   91213  4211302    46.2 |  2.089 % |
c ==============================================================================
c [1mFound solution: 321219[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    168036 |  284558   667500 |   94852   92328  4304736    46.6 |  2.089 % |
c |    168136 |  284558   667500 |  104337   92428  4307028    46.6 |  2.090 % |
c |    168286 |  284558   667500 |  114770   92578  4314011    46.6 |  2.090 % |
c |    168514 |  284558   667500 |  126248   92806  4322326    46.6 |  2.090 % |
c |    168851 |  284558   667500 |  138872   93143  4357959    46.8 |  2.090 % |
c |    169357 |  284558   667500 |  152760   93649  4396711    46.9 |  2.090 % |
c |    170116 |  284528   667434 |  168036   94407  4454127    47.2 |  2.098 % |
c |    171256 |  284482   667329 |  184839   95543  4493811    47.0 |  2.113 % |
c ==============================================================================
c [1mFound solution: 321217[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    171928 |  284494   667359 |   94831   96215  4605484    47.9 |  2.113 % |
c |    172028 |  284494   667359 |  104314   96315  4606454    47.8 |  2.114 % |
c |    172178 |  284494   667359 |  114745   96465  4607766    47.8 |  2.114 % |
c |    172403 |  284247   666800 |  126220   96606  4612171    47.7 |  2.182 % |
c |    172741 |  284082   666430 |  138842   96745  4614985    47.7 |  2.232 % |
c |    173250 |  284082   666430 |  152726   97254  4670801    48.0 |  2.232 % |
c |    174009 |  284082   666430 |  167998   98013  4683121    47.8 |  2.232 % |
c |    175149 |  284082   666430 |  184798   99153  4749458    47.9 |  2.232 % |
c ==============================================================================
c [1mFound solution: 292158[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175332 |  284097   666471 |   94699   99336  4767362    48.0 |  2.232 % |
c |    175432 |  284097   666471 |  104168   37917   967890    25.5 |  2.234 % |
c |    175582 |  284097   666471 |  114585   38067   971146    25.5 |  2.234 % |
c |    175807 |  284097   666471 |  126044   38292   981015    25.6 |  2.234 % |
c |    176146 |  284097   666471 |  138648   38631  1014671    26.3 |  2.234 % |
c |    176653 |  284097   666471 |  152513   39138  1049495    26.8 |  2.234 % |
#### 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.94 0.69 2/54 11117
Raw data (stat): 11117 (runsolver) R 11116 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429385429 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0002 s]
Raw data (loadavg): 0.87 0.94 0.69 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 8683 0 0 0 976 22 0 0 25 0 1 0 429385429 39149568 8352 4294967295 134512640 134672761 3221224640 3221223792 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9558 8352 603 41 0 9517 0
vsize: 38232
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.69 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 8900 0 0 0 1975 23 0 0 25 0 1 0 429385429 39972864 8569 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9759 8569 603 41 0 9718 0
vsize: 39036
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.94 0.70 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9044 0 0 0 2974 24 0 0 25 0 1 0 429385429 40574976 8713 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9906 8713 603 41 0 9865 0
vsize: 39624
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.94 0.70 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9084 0 0 0 3974 24 0 0 25 0 1 0 429385429 40710144 8753 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9939 8753 603 41 0 9898 0
vsize: 39756
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.94 0.70 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9144 0 0 0 4974 24 0 0 25 0 1 0 429385429 40968192 8813 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10002 8813 603 41 0 9961 0
vsize: 40008
[startup+60.0024 s]
Raw data (loadavg): 0.94 0.95 0.70 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9218 0 0 0 5974 25 0 0 25 0 1 0 429385429 41234432 8887 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10067 8887 603 41 0 10026 0
vsize: 40268
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.95 0.71 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9280 0 0 0 6973 26 0 0 25 0 1 0 429385429 41504768 8949 4294967295 134512640 134672761 3221224640 3221223744 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10133 8949 603 41 0 10092 0
vsize: 40532
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9325 0 0 0 7973 26 0 0 25 0 1 0 429385429 41738240 8994 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10190 8994 603 41 0 10149 0
vsize: 40760
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.95 0.71 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9408 0 0 0 8973 26 0 0 25 0 1 0 429385429 42008576 9077 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10256 9077 603 41 0 10215 0
vsize: 41024
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9495 0 0 0 9972 26 0 0 25 0 1 0 429385429 42414080 9164 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10355 9164 603 41 0 10314 0
vsize: 41420
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.72 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9587 0 0 0 10972 27 0 0 25 0 1 0 429385429 42758144 9256 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10439 9256 603 41 0 10398 0
vsize: 41756
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9638 0 0 0 11972 27 0 0 25 0 1 0 429385429 42885120 9307 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10470 9307 603 41 0 10429 0
vsize: 41880
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.72 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9671 0 0 0 12972 27 0 0 25 0 1 0 429385429 43020288 9340 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9340 603 41 0 10462 0
vsize: 42012
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9767 0 0 0 13972 28 0 0 25 0 1 0 429385429 43421696 9436 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10601 9436 603 41 0 10560 0
vsize: 42404
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.73 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9840 0 0 0 14972 28 0 0 25 0 1 0 429385429 43814912 9509 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10697 9509 603 41 0 10656 0
vsize: 42788
[startup+160.005 s]
Raw data (loadavg): 0.99 0.95 0.73 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 9876 0 0 0 15972 28 0 0 25 0 1 0 429385429 43950080 9545 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10730 9545 603 41 0 10689 0
vsize: 42920
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.73 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10005 0 0 0 16972 28 0 0 25 0 1 0 429385429 44494848 9674 4294967295 134512640 134672761 3221224640 3221223744 134554907 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10863 9674 603 41 0 10822 0
vsize: 43452
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10067 0 0 0 17972 29 0 0 25 0 1 0 429385429 44761088 9736 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10928 9736 603 41 0 10887 0
vsize: 43712
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10169 0 0 0 18971 29 0 0 25 0 1 0 429385429 45162496 9838 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11026 9838 603 41 0 10985 0
vsize: 44104
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10347 0 0 0 19971 29 0 0 25 0 1 0 429385429 45969408 10016 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11223 10016 603 41 0 11182 0
vsize: 44892
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10541 0 0 0 20971 30 0 0 25 0 1 0 429385429 46632960 10210 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11385 10210 603 41 0 11344 0
vsize: 45540
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.74 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10628 0 0 0 21971 30 0 0 25 0 1 0 429385429 47038464 10297 4294967295 134512640 134672761 3221224640 3221223800 134565025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11484 10297 603 41 0 11443 0
vsize: 45936
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 10959 0 0 0 22970 31 0 0 25 0 1 0 429385429 48386048 10628 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11813 10628 603 41 0 11772 0
vsize: 47252
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11087 0 0 0 23970 32 0 0 25 0 1 0 429385429 48926720 10756 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11945 10756 603 41 0 11904 0
vsize: 47780
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11171 0 0 0 24970 32 0 0 25 0 1 0 429385429 49197056 10840 4294967295 134512640 134672761 3221224640 3221223744 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12011 10840 603 41 0 11970 0
vsize: 48044
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.75 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11268 0 0 0 25969 33 0 0 25 0 1 0 429385429 49602560 10937 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12110 10937 603 41 0 12069 0
vsize: 48440
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11371 0 0 0 26969 33 0 0 25 0 1 0 429385429 50008064 11040 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12209 11040 603 41 0 12168 0
vsize: 48836
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11481 0 0 0 27969 33 0 0 25 0 1 0 429385429 50540544 11150 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12339 11150 603 41 0 12298 0
vsize: 49356
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11572 0 0 0 28969 33 0 0 25 0 1 0 429385429 50810880 11241 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12405 11241 603 41 0 12364 0
vsize: 49620
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11662 0 0 0 29969 34 0 0 25 0 1 0 429385429 51208192 11331 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12502 11331 603 41 0 12461 0
vsize: 50008
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11817 0 0 0 30968 34 0 0 25 0 1 0 429385429 52047872 11486 4294967295 134512640 134672761 3221224640 3221223972 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12707 11486 603 41 0 12666 0
vsize: 50828
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11858 0 0 0 31968 34 0 0 25 0 1 0 429385429 52285440 11527 4294967295 134512640 134672761 3221224640 3221223812 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12765 11527 603 41 0 12724 0
vsize: 51060
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 11917 0 0 0 32968 35 0 0 25 0 1 0 429385429 52551680 11586 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12830 11586 603 41 0 12789 0
vsize: 51320
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12028 0 0 0 33968 35 0 0 25 0 1 0 429385429 52957184 11697 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12929 11697 603 41 0 12888 0
vsize: 51716
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12122 0 0 0 34968 36 0 0 25 0 1 0 429385429 53354496 11791 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13026 11791 603 41 0 12985 0
vsize: 52104
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12190 0 0 0 35968 36 0 0 25 0 1 0 429385429 53616640 11859 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13090 11859 603 41 0 13049 0
vsize: 52360
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12256 0 0 0 36968 36 0 0 25 0 1 0 429385429 53882880 11925 4294967295 134512640 134672761 3221224640 3221223812 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13155 11925 603 41 0 13114 0
vsize: 52620
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12296 0 0 0 37968 37 0 0 25 0 1 0 429385429 53972992 11965 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13177 11965 603 41 0 13136 0
vsize: 52708
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12320 0 0 0 38968 37 0 0 25 0 1 0 429385429 54104064 11989 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13209 11989 603 41 0 13168 0
vsize: 52836
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12403 0 0 0 39968 37 0 0 25 0 1 0 429385429 54509568 12072 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13308 12072 603 41 0 13267 0
vsize: 53232
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12503 0 0 0 40967 37 0 0 25 0 1 0 429385429 54910976 12172 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13406 12172 603 41 0 13365 0
vsize: 53624
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12615 0 0 0 41967 38 0 0 25 0 1 0 429385429 55304192 12284 4294967295 134512640 134672761 3221224640 3221223796 134564777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13502 12284 603 41 0 13461 0
vsize: 54008
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12727 0 0 0 42967 38 0 0 25 0 1 0 429385429 55709696 12396 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13601 12396 603 41 0 13560 0
vsize: 54404
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 12925 0 0 0 43966 39 0 0 25 0 1 0 429385429 56516608 12594 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13798 12594 603 41 0 13757 0
vsize: 55192
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13003 0 0 0 44966 39 0 0 25 0 1 0 429385429 56922112 12672 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13897 12672 603 41 0 13856 0
vsize: 55588
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13074 0 0 0 45966 40 0 0 25 0 1 0 429385429 57098240 12743 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13940 12743 603 41 0 13899 0
vsize: 55760
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13126 0 0 0 46966 40 0 0 25 0 1 0 429385429 57360384 12795 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14004 12795 603 41 0 13963 0
vsize: 56016
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13180 0 0 0 47966 40 0 0 25 0 1 0 429385429 57626624 12849 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14069 12849 603 41 0 14028 0
vsize: 56276
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13233 0 0 0 48966 40 0 0 25 0 1 0 429385429 57761792 12902 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 12902 603 41 0 14061 0
vsize: 56408
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13290 0 0 0 49966 40 0 0 25 0 1 0 429385429 58028032 12959 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14167 12959 603 41 0 14126 0
vsize: 56668
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13339 0 0 0 50966 40 0 0 25 0 1 0 429385429 58163200 13008 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14200 13008 603 41 0 14159 0
vsize: 56800
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13468 0 0 0 51966 41 0 0 25 0 1 0 429385429 58699776 13137 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14331 13137 603 41 0 14290 0
vsize: 57324
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.80 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13544 0 0 0 52966 41 0 0 25 0 1 0 429385429 58970112 13213 4294967295 134512640 134672761 3221224640 3221223840 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14397 13213 603 41 0 14356 0
vsize: 57588
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13652 0 0 0 53966 41 0 0 25 0 1 0 429385429 59510784 13321 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14529 13321 603 41 0 14488 0
vsize: 58116
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13748 0 0 0 54966 42 0 0 25 0 1 0 429385429 59781120 13417 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14595 13417 603 41 0 14554 0
vsize: 58380
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.81 2/54 11117
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 13845 0 0 0 55966 42 0 0 25 0 1 0 429385429 60178432 13514 4294967295 134512640 134672761 3221224640 3221223776 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14692 13514 603 41 0 14651 0
vsize: 58768
[startup+570.018 s]
Raw data (loadavg): 1.15 1.00 0.82 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 56965 42 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+580.019 s]
Raw data (loadavg): 1.12 1.00 0.82 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 57965 42 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+590.019 s]
Raw data (loadavg): 1.10 1.00 0.82 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 58965 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223764 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+600.02 s]
Raw data (loadavg): 1.09 1.00 0.83 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 59965 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+610.02 s]
Raw data (loadavg): 1.07 1.00 0.83 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 60965 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223812 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+620.021 s]
Raw data (loadavg): 1.06 1.00 0.83 2/54 11170
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 61965 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223776 134560632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+630.02 s]
Raw data (loadavg): 1.05 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 62966 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+640.02 s]
Raw data (loadavg): 1.04 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 63966 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+650.02 s]
Raw data (loadavg): 1.04 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 64966 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+660.02 s]
Raw data (loadavg): 1.03 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 65966 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223776 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+670.022 s]
Raw data (loadavg): 1.03 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14002 0 0 0 66966 43 0 0 25 0 1 0 429385429 60837888 13671 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13671 603 41 0 14812 0
vsize: 59412
[startup+680.022 s]
Raw data (loadavg): 1.02 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 67966 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223744 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+690.021 s]
Raw data (loadavg): 1.02 1.00 0.83 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 68966 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223904 134562558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+700.022 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 69967 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+710.022 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 70967 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+720.023 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 71967 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+730.023 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 72967 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+740.023 s]
Raw data (loadavg): 1.01 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 73967 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+750.024 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 74968 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+760.024 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 75968 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+770.025 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 76968 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223812 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+780.026 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 77968 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223776 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+790.025 s]
Raw data (loadavg): 1.00 1.00 0.84 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14003 0 0 0 78968 43 0 0 25 0 1 0 429385429 60837888 13672 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13672 603 41 0 14812 0
vsize: 59412
[startup+800.025 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14004 0 0 0 79968 43 0 0 25 0 1 0 429385429 60837888 13673 4294967295 134512640 134672761 3221224640 3221223200 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13673 603 41 0 14812 0
vsize: 59412
[startup+810.026 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14004 0 0 0 80969 43 0 0 25 0 1 0 429385429 60837888 13673 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13673 603 41 0 14812 0
vsize: 59412
[startup+820.026 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14004 0 0 0 81969 43 0 0 25 0 1 0 429385429 60837888 13673 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13673 603 41 0 14812 0
vsize: 59412
[startup+830.033 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14004 0 0 0 82970 43 0 0 25 0 1 0 429385429 60837888 13673 4294967295 134512640 134672761 3221224640 3221223840 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13673 603 41 0 14812 0
vsize: 59412
[startup+840.034 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14007 0 0 0 83970 43 0 0 25 0 1 0 429385429 60837888 13676 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13676 603 41 0 14812 0
vsize: 59412
[startup+850.034 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 84970 43 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+860.034 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 85970 43 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+870.035 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11172
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 86970 43 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223744 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+880.035 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 87970 43 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+890.035 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 88971 43 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+900.036 s]
Raw data (loadavg): 1.00 1.00 0.85 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 89971 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223744 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+910.036 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 90971 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+920.042 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 91972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223744 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+930.042 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 92972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221205200 134523226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+940.042 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 93972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+950.043 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 94972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+960.043 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 95972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+970.044 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 96972 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+980.046 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 97973 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+990.046 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 98973 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.86 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 99973 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14008 0 0 0 100973 44 0 0 25 0 1 0 429385429 60837888 13677 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13677 603 41 0 14812 0
vsize: 59412
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 101974 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 102974 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 103974 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 104974 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 105974 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 106975 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14010 0 0 0 107975 44 0 0 25 0 1 0 429385429 60837888 13679 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 13679 603 41 0 14812 0
vsize: 59412
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14072 0 0 0 108975 44 0 0 25 0 1 0 429385429 61087744 13741 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14914 13741 603 41 0 14873 0
vsize: 59656
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.87 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14109 0 0 0 109975 44 0 0 25 0 1 0 429385429 61214720 13778 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14945 13778 603 41 0 14904 0
vsize: 59780
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14180 0 0 0 110975 44 0 0 25 0 1 0 429385429 61612032 13849 4294967295 134512640 134672761 3221224640 3221223776 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15042 13849 603 41 0 15001 0
vsize: 60168
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14223 0 0 0 111975 45 0 0 25 0 1 0 429385429 61743104 13892 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15074 13892 603 41 0 15033 0
vsize: 60296
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14322 0 0 0 112975 45 0 0 25 0 1 0 429385429 62169088 13991 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15178 13991 603 41 0 15137 0
vsize: 60712
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14407 0 0 0 113975 45 0 0 25 0 1 0 429385429 62574592 14076 4294967295 134512640 134672761 3221224640 3221223812 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15277 14076 603 41 0 15236 0
vsize: 61108
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14421 0 0 0 114975 45 0 0 25 0 1 0 429385429 62574592 14090 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15277 14090 603 41 0 15236 0
vsize: 61108
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14508 0 0 0 115975 45 0 0 25 0 1 0 429385429 62967808 14177 4294967295 134512640 134672761 3221224640 3221223808 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15373 14177 603 41 0 15332 0
vsize: 61492
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14598 0 0 0 116975 45 0 0 25 0 1 0 429385429 63234048 14267 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15438 14267 603 41 0 15397 0
vsize: 61752
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14598 0 0 0 117975 45 0 0 25 0 1 0 429385429 63234048 14267 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15438 14267 603 41 0 15397 0
vsize: 61752
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14598 0 0 0 118975 45 0 0 25 0 1 0 429385429 63234048 14267 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15438 14267 603 41 0 15397 0
vsize: 61752
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 11174
Raw data (stat): 11117 (minisat+) R 11116 30854 30853 0 -1 0 14598 0 0 0 119975 45 0 0 25 0 1 0 429385429 63234048 14267 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15438 14267 603 41 0 15397 0
vsize: 61752
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.88 1/54 11174
Raw data (stat): 11117 (minisat+) Z 11116 30854 30853 0 -1 12 14601 0 0 0 119976 48 0 0 25 0 1 0 429385429 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: 10
Real time (s): 1200.08
CPU time (s): 1200.25
CPU user time (s): 1199.76
CPU system time (s): 0.488925
CPU usage (%): 100.014
Max. virtual memory (Kb): 61752
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####