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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare1_1.opb
MD5SUM	452acf9ed3adc2d2cfe293dad01c0934
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	167110
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.02
Number of variables	280
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	45
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	130
Trace number 13653

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-20 21:14:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14481 boxname=wulflinc26 idbench=1114 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  452acf9ed3adc2d2cfe293dad01c0934  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-markshare1_1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-markshare1_1.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-markshare1_1.opb
IDLAUNCH: 14481
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        538456 kB
Buffers:         37680 kB
Cached:         418056 kB
SwapCached:          0 kB
Active:         211652 kB
Inactive:       246996 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        538204 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            31976 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 21:34:10 (client local time) WITH STATUS 10 IN 1201.08 SECONDS
stats: 14481 7 1201.08 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> BDD-cost:87035
c ---[   8]---> BDD-cost:82838
c ---[   6]---> BDD-cost:89015
c ---[   4]---> BDD-cost:39244
c ---[   2]---> BDD-cost:62663
c ---[   0]---> BDD-cost:60806
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1194561  3457768 |  398187       0        0     nan |  0.000 % |
c |       100 | 1194469  3457584 |  438005      98     4658    47.5 |  0.026 % |
c ==============================================================================
c [1mFound solution: 6879072[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       106 | 1198871  3467866 |  399623     104    13063   125.6 |  0.026 % |
c ==============================================================================
c [1mFound solution: 6534298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       107 | 1198906  3468005 |  399635     105    13109   124.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 6443290[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       107 | 1198926  3468050 |  399642     105    13109   124.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 6425568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       117 | 1198942  3468088 |  399647     115    22668   197.1 |  0.026 % |
c ==============================================================================
c [1mFound solution: 3709466[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       118 | 1198972  3468158 |  399657     116    22718   195.8 |  0.026 % |
c ==============================================================================
c [1mFound solution: 3000667[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       121 | 1198994  3468212 |  399664     119    22816   191.7 |  0.026 % |
c |       221 | 1198994  3468212 |  439630     219    29613   135.2 |  0.027 % |
c |       372 | 1198994  3468212 |  483593     370    36880    99.7 |  0.027 % |
c |       597 | 1198994  3468212 |  531952     595    45162    75.9 |  0.027 % |
c |       934 | 1198994  3468212 |  585148     932   568779   610.3 |  0.027 % |
c |      1440 | 1198994  3468212 |  643662    1438   829660   577.0 |  0.027 % |
c |      2201 | 1198994  3468212 |  708029    2199   869139   395.2 |  0.027 % |
c |      3340 | 1198994  3468212 |  778832    3338   948281   284.1 |  0.027 % |
c ==============================================================================
c [1mFound solution: 2998212[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3710 | 1199011  3468261 |  399670    3708   956775   258.0 |  0.027 % |
c |      3814 | 1199011  3468261 |  439637    3812  1182763   310.3 |  0.028 % |
c ==============================================================================
c [1mFound solution: 2485433[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3888 | 1199029  3468310 |  399676    3886  1205452   310.2 |  0.028 % |
c |      3988 | 1199029  3468310 |  439643    3986  1221539   306.5 |  0.028 % |
c |      4139 | 1199029  3468310 |  483607    4137  1227535   296.7 |  0.028 % |
c |      4364 | 1199029  3468310 |  531968    4362  1238676   284.0 |  0.028 % |
c ==============================================================================
c [1mFound solution: 2479423[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4438 | 1199053  3468367 |  399684    4436  1241960   280.0 |  0.028 % |
c |      4538 | 1199053  3468367 |  439652    4536  1261631   278.1 |  0.028 % |
c |      4689 | 1199053  3468367 |  483617    4687  1270123   271.0 |  0.028 % |
c |      4914 | 1199053  3468367 |  531979    4912  1282886   261.2 |  0.028 % |
c |      5253 | 1199053  3468367 |  585177    5251  1298710   247.3 |  0.028 % |
c |      5759 | 1199053  3468367 |  643695    5757  1322349   229.7 |  0.028 % |
c ==============================================================================
c [1mFound solution: 2424683[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6105 | 1199065  3468403 |  399688    6103  1331830   218.2 |  0.028 % |
c |      6206 | 1199065  3468403 |  439656    6204  1420161   228.9 |  0.028 % |
c ==============================================================================
c [1mFound solution: 2424593[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6303 | 1199082  3468449 |  399694    6301  1423998   226.0 |  0.028 % |
c |      6405 | 1199082  3468449 |  439663    6403  1622195   253.3 |  0.029 % |
c |      6560 | 1199082  3468449 |  483629    6558  1818046   277.2 |  0.029 % |
c |      6789 | 1199082  3468449 |  531992    6787  1971496   290.5 |  0.029 % |
c |      7127 | 1199082  3468449 |  585191    7125  1993412   279.8 |  0.029 % |
c |      7634 | 1199082  3468449 |  643711    7632  2023817   265.2 |  0.029 % |
c |      8393 | 1199082  3468449 |  708082    8391  2067658   246.4 |  0.029 % |
c ==============================================================================
c [1mFound solution: 2424372[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8765 | 1199096  3468488 |  399698    8763  2083215   237.7 |  0.029 % |
c |      8868 | 1199096  3468488 |  439667    8866  2360292   266.2 |  0.029 % |
c |      9018 | 1199096  3468488 |  483634    9016  2605265   289.0 |  0.029 % |
c |      9245 | 1199096  3468488 |  531998    9243  2732022   295.6 |  0.029 % |
c |      9584 | 1199096  3468488 |  585197    9582  2907460   303.4 |  0.029 % |
c |     10091 | 1199096  3468488 |  643717   10089  2932346   290.6 |  0.029 % |
c ==============================================================================
c [1mFound solution: 2376660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10272 | 1199115  3468534 |  399705   10270  2952657   287.5 |  0.029 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.90 2/54 18620
Raw data (stat): 18620 (runsolver) R 18619 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539599361 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 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.0005 s]
Raw data (loadavg): 0.87 0.97 0.90 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 38559 0 0 0 912 86 0 0 25 0 1 0 539599361 159444992 35017 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38927 35017 603 41 0 38886 0
vsize: 155708
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.97 0.90 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 39792 0 0 0 1909 89 0 0 25 0 1 0 539599361 165011456 36250 4294967295 134512640 134672761 3221224528 3221223652 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40286 36250 603 41 0 40245 0
vsize: 161144
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.97 0.90 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 39817 0 0 0 2908 90 0 0 25 0 1 0 539599361 165154816 36275 4294967295 134512640 134672761 3221224528 3221223668 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40321 36275 603 41 0 40280 0
vsize: 161284
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.97 0.90 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 39865 0 0 0 3908 90 0 0 25 0 1 0 539599361 165371904 36323 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40374 36323 603 41 0 40333 0
vsize: 161496
[startup+50.0026 s]
Raw data (loadavg): 0.93 0.97 0.90 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 39968 0 0 0 4907 91 0 0 25 0 1 0 539599361 165765120 36394 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40470 36394 603 41 0 40429 0
vsize: 161880
[startup+60.0034 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 39994 0 0 0 5907 91 0 0 25 0 1 0 539599361 165900288 36420 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40503 36420 603 41 0 40462 0
vsize: 162012
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40075 0 0 0 6907 92 0 0 25 0 1 0 539599361 166313984 36501 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40604 36501 603 41 0 40563 0
vsize: 162416
[startup+80.0046 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40123 0 0 0 7907 92 0 0 25 0 1 0 539599361 166453248 36549 4294967295 134512640 134672761 3221224528 3221223632 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40638 36549 603 41 0 40597 0
vsize: 162552
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40190 0 0 0 8906 92 0 0 25 0 1 0 539599361 166723584 36616 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40704 36616 603 41 0 40663 0
vsize: 162816
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40239 0 0 0 9906 93 0 0 25 0 1 0 539599361 166981632 36665 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40767 36665 603 41 0 40726 0
vsize: 163068
[startup+110.013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40303 0 0 0 10907 93 0 0 25 0 1 0 539599361 167276544 36729 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40839 36729 603 41 0 40798 0
vsize: 163356
[startup+120.121 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40345 0 0 0 11917 93 0 0 25 0 1 0 539599361 167387136 36771 4294967295 134512640 134672761 3221224528 3221223632 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40866 36771 603 41 0 40825 0
vsize: 163464
[startup+130.121 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40392 0 0 0 12917 94 0 0 25 0 1 0 539599361 167526400 36818 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40900 36818 603 41 0 40859 0
vsize: 163600
[startup+140.128 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40438 0 0 0 13918 94 0 0 25 0 1 0 539599361 167800832 36864 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40967 36864 603 41 0 40926 0
vsize: 163868
[startup+150.335 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40476 0 0 0 14937 95 0 0 25 0 1 0 539599361 167948288 36902 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41003 36902 603 41 0 40962 0
vsize: 164012
[startup+160.335 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40519 0 0 0 15937 95 0 0 25 0 1 0 539599361 168083456 36945 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41036 36945 603 41 0 40995 0
vsize: 164144
[startup+170.334 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40547 0 0 0 16937 95 0 0 25 0 1 0 539599361 168218624 36973 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41069 36973 603 41 0 41028 0
vsize: 164276
[startup+180.338 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40576 0 0 0 17937 95 0 0 25 0 1 0 539599361 168353792 37002 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41102 37002 603 41 0 41061 0
vsize: 164408
[startup+190.338 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40603 0 0 0 18937 96 0 0 25 0 1 0 539599361 168488960 37029 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41135 37029 603 41 0 41094 0
vsize: 164540
[startup+200.338 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40625 0 0 0 19937 96 0 0 25 0 1 0 539599361 168488960 37051 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41135 37051 603 41 0 41094 0
vsize: 164540
[startup+210.44 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40647 0 0 0 20947 96 0 0 25 0 1 0 539599361 168624128 37073 4294967295 134512640 134672761 3221224528 3221223632 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41168 37073 603 41 0 41127 0
vsize: 164672
[startup+220.441 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40661 0 0 0 21946 97 0 0 25 0 1 0 539599361 168624128 37087 4294967295 134512640 134672761 3221224528 3221223632 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41168 37087 603 41 0 41127 0
vsize: 164672
[startup+230.44 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40682 0 0 0 22945 98 0 0 25 0 1 0 539599361 168759296 37108 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41201 37108 603 41 0 41160 0
vsize: 164804
[startup+240.542 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40714 0 0 0 23956 98 0 0 25 0 1 0 539599361 168910848 37140 4294967295 134512640 134672761 3221224528 3221223632 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41238 37140 603 41 0 41197 0
vsize: 164952
[startup+250.543 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40731 0 0 0 24955 98 0 0 25 0 1 0 539599361 168910848 37157 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41238 37157 603 41 0 41197 0
vsize: 164952
[startup+260.558 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40734 0 0 0 25956 99 0 0 25 0 1 0 539599361 168910848 37160 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41238 37160 603 41 0 41197 0
vsize: 164952
[startup+270.558 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40741 0 0 0 26956 99 0 0 25 0 1 0 539599361 169041920 37167 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37167 603 41 0 41229 0
vsize: 165080
[startup+280.558 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40746 0 0 0 27955 100 0 0 25 0 1 0 539599361 169041920 37172 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37172 603 41 0 41229 0
vsize: 165080
[startup+290.559 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40749 0 0 0 28955 100 0 0 25 0 1 0 539599361 169041920 37175 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37175 603 41 0 41229 0
vsize: 165080
[startup+300.559 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40755 0 0 0 29955 100 0 0 25 0 1 0 539599361 169041920 37181 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37181 603 41 0 41229 0
vsize: 165080
[startup+310.56 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40760 0 0 0 30954 101 0 0 25 0 1 0 539599361 169041920 37186 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37186 603 41 0 41229 0
vsize: 165080
[startup+320.559 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40766 0 0 0 31954 101 0 0 25 0 1 0 539599361 169041920 37192 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41270 37192 603 41 0 41229 0
vsize: 165080
[startup+330.56 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40769 0 0 0 32953 102 0 0 25 0 1 0 539599361 169168896 37195 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41301 37195 603 41 0 41260 0
vsize: 165204
[startup+340.56 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40776 0 0 0 33953 102 0 0 25 0 1 0 539599361 169168896 37202 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41301 37202 603 41 0 41260 0
vsize: 165204
[startup+350.568 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40792 0 0 0 34953 103 0 0 25 0 1 0 539599361 169168896 37218 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41301 37218 603 41 0 41260 0
vsize: 165204
[startup+360.593 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40801 0 0 0 35955 103 0 0 25 0 1 0 539599361 169299968 37227 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41333 37227 603 41 0 41292 0
vsize: 165332
[startup+370.593 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40813 0 0 0 36955 103 0 0 25 0 1 0 539599361 169299968 37239 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41333 37239 603 41 0 41292 0
vsize: 165332
[startup+380.636 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40823 0 0 0 37959 104 0 0 25 0 1 0 539599361 169299968 37249 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41333 37249 603 41 0 41292 0
vsize: 165332
[startup+390.692 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40836 0 0 0 38964 104 0 0 25 0 1 0 539599361 169426944 37262 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41364 37262 603 41 0 41323 0
vsize: 165456
[startup+400.692 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40840 0 0 0 39963 104 0 0 25 0 1 0 539599361 169426944 37266 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41364 37266 603 41 0 41323 0
vsize: 165456
[startup+410.697 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40846 0 0 0 40964 105 0 0 25 0 1 0 539599361 169426944 37272 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41364 37272 603 41 0 41323 0
vsize: 165456
[startup+420.698 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40852 0 0 0 41964 105 0 0 25 0 1 0 539599361 169426944 37278 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41364 37278 603 41 0 41323 0
vsize: 165456
[startup+430.704 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40855 0 0 0 42965 105 0 0 25 0 1 0 539599361 169426944 37281 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41364 37281 603 41 0 41323 0
vsize: 165456
[startup+440.705 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40861 0 0 0 43965 105 0 0 25 0 1 0 539599361 169426944 37287 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41364 37287 603 41 0 41323 0
vsize: 165456
[startup+450.707 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40867 0 0 0 44966 105 0 0 25 0 1 0 539599361 169558016 37293 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41396 37293 603 41 0 41355 0
vsize: 165584
[startup+460.821 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 40944 0 0 0 45977 105 0 0 25 0 1 0 539599361 169783296 37370 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41451 37370 603 41 0 41410 0
vsize: 165804
[startup+470.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41127 0 0 0 46975 106 0 0 25 0 1 0 539599361 170557440 37553 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41640 37553 603 41 0 41599 0
vsize: 166560
[startup+480.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41133 0 0 0 47975 106 0 0 25 0 1 0 539599361 170557440 37559 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41640 37559 603 41 0 41599 0
vsize: 166560
[startup+490.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41146 0 0 0 48975 106 0 0 25 0 1 0 539599361 170692608 37572 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41673 37572 603 41 0 41632 0
vsize: 166692
[startup+500.835 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41150 0 0 0 49975 107 0 0 25 0 1 0 539599361 170692608 37576 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41673 37576 603 41 0 41632 0
vsize: 166692
[startup+510.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41158 0 0 0 50975 107 0 0 25 0 1 0 539599361 170692608 37584 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41673 37584 603 41 0 41632 0
vsize: 166692
[startup+520.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41189 0 0 0 51975 107 0 0 25 0 1 0 539599361 170827776 37615 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41706 37615 603 41 0 41665 0
vsize: 166824
[startup+530.835 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41194 0 0 0 52975 107 0 0 25 0 1 0 539599361 170827776 37620 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41706 37620 603 41 0 41665 0
vsize: 166824
[startup+540.834 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41200 0 0 0 53975 107 0 0 25 0 1 0 539599361 170827776 37626 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41706 37626 603 41 0 41665 0
vsize: 166824
[startup+550.835 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41208 0 0 0 54975 107 0 0 25 0 1 0 539599361 170958848 37634 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41738 37634 603 41 0 41697 0
vsize: 166952
[startup+560.836 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41214 0 0 0 55975 107 0 0 25 0 1 0 539599361 170958848 37640 4294967295 134512640 134672761 3221224528 3221223680 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41738 37640 603 41 0 41697 0
vsize: 166952
[startup+570.835 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41221 0 0 0 56975 107 0 0 25 0 1 0 539599361 170958848 37647 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41738 37647 603 41 0 41697 0
vsize: 166952
[startup+580.836 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41227 0 0 0 57975 108 0 0 25 0 1 0 539599361 170958848 37653 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41738 37653 603 41 0 41697 0
vsize: 166952
[startup+590.836 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41236 0 0 0 58975 108 0 0 25 0 1 0 539599361 170958848 37662 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41738 37662 603 41 0 41697 0
vsize: 166952
[startup+600.841 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41244 0 0 0 59976 108 0 0 25 0 1 0 539599361 171089920 37670 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41770 37670 603 41 0 41729 0
vsize: 167080
[startup+610.843 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41253 0 0 0 60976 108 0 0 25 0 1 0 539599361 171089920 37679 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41770 37679 603 41 0 41729 0
vsize: 167080
[startup+620.843 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41259 0 0 0 61976 108 0 0 25 0 1 0 539599361 171089920 37685 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41770 37685 603 41 0 41729 0
vsize: 167080
[startup+630.849 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41271 0 0 0 62977 108 0 0 25 0 1 0 539599361 171089920 37697 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41770 37697 603 41 0 41729 0
vsize: 167080
[startup+640.848 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41364 0 0 0 63977 108 0 0 25 0 1 0 539599361 171626496 37790 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41901 37790 603 41 0 41860 0
vsize: 167604
[startup+650.849 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41414 0 0 0 64977 108 0 0 25 0 1 0 539599361 171732992 37840 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41927 37840 603 41 0 41886 0
vsize: 167708
[startup+660.854 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41563 0 0 0 65977 109 0 0 25 0 1 0 539599361 172371968 37989 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42083 37989 603 41 0 42042 0
vsize: 168332
[startup+670.858 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41624 0 0 0 66977 109 0 0 25 0 1 0 539599361 172638208 38050 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42148 38050 603 41 0 42107 0
vsize: 168592
[startup+680.859 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41659 0 0 0 67977 109 0 0 25 0 1 0 539599361 172781568 38085 4294967295 134512640 134672761 3221224528 3221223632 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42183 38085 603 41 0 42142 0
vsize: 168732
[startup+690.865 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41670 0 0 0 68978 109 0 0 25 0 1 0 539599361 172781568 38096 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42183 38096 603 41 0 42142 0
vsize: 168732
[startup+700.869 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41702 0 0 0 69979 109 0 0 25 0 1 0 539599361 172929024 38128 4294967295 134512640 134672761 3221224528 3221223632 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42219 38128 603 41 0 42178 0
vsize: 168876
[startup+710.869 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41710 0 0 0 70979 109 0 0 25 0 1 0 539599361 172929024 38136 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42219 38136 603 41 0 42178 0
vsize: 168876
[startup+720.869 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41720 0 0 0 71979 109 0 0 25 0 1 0 539599361 173035520 38146 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42245 38146 603 41 0 42204 0
vsize: 168980
[startup+730.869 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41729 0 0 0 72979 110 0 0 25 0 1 0 539599361 173035520 38155 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42245 38155 603 41 0 42204 0
vsize: 168980
[startup+740.87 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41741 0 0 0 73979 110 0 0 25 0 1 0 539599361 173035520 38167 4294967295 134512640 134672761 3221224528 3221223632 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42245 38167 603 41 0 42204 0
vsize: 168980
[startup+750.87 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41748 0 0 0 74980 110 0 0 25 0 1 0 539599361 173150208 38174 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42273 38174 603 41 0 42232 0
vsize: 169092
[startup+760.87 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41755 0 0 0 75980 110 0 0 25 0 1 0 539599361 173150208 38181 4294967295 134512640 134672761 3221224528 3221223632 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42273 38181 603 41 0 42232 0
vsize: 169092
[startup+770.87 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41766 0 0 0 76980 110 0 0 25 0 1 0 539599361 173150208 38192 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42273 38192 603 41 0 42232 0
vsize: 169092
[startup+780.87 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41790 0 0 0 77980 110 0 0 25 0 1 0 539599361 173293568 38216 4294967295 134512640 134672761 3221224528 3221223632 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42308 38216 603 41 0 42267 0
vsize: 169232
[startup+790.869 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41806 0 0 0 78980 110 0 0 25 0 1 0 539599361 173293568 38232 4294967295 134512640 134672761 3221224528 3221223632 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42308 38232 603 41 0 42267 0
vsize: 169232
[startup+800.87 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41831 0 0 0 79980 110 0 0 25 0 1 0 539599361 173424640 38257 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42340 38257 603 41 0 42299 0
vsize: 169360
[startup+810.871 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41837 0 0 0 80980 110 0 0 25 0 1 0 539599361 173424640 38263 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42340 38263 603 41 0 42299 0
vsize: 169360
[startup+820.87 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41857 0 0 0 81980 110 0 0 25 0 1 0 539599361 173559808 38283 4294967295 134512640 134672761 3221224528 3221223632 134560160 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42373 38283 603 41 0 42332 0
vsize: 169492
[startup+830.871 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41875 0 0 0 82980 110 0 0 25 0 1 0 539599361 173699072 38301 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42407 38301 603 41 0 42366 0
vsize: 169628
[startup+840.872 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41879 0 0 0 83981 110 0 0 25 0 1 0 539599361 173699072 38305 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42407 38305 603 41 0 42366 0
vsize: 169628
[startup+850.872 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41897 0 0 0 84981 110 0 0 25 0 1 0 539599361 173699072 38323 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42407 38323 603 41 0 42366 0
vsize: 169628
[startup+860.872 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41907 0 0 0 85981 110 0 0 25 0 1 0 539599361 173699072 38333 4294967295 134512640 134672761 3221224528 3221223632 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42407 38333 603 41 0 42366 0
vsize: 169628
[startup+870.872 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41920 0 0 0 86981 110 0 0 25 0 1 0 539599361 173830144 38346 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42439 38346 603 41 0 42398 0
vsize: 169756
[startup+880.873 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41933 0 0 0 87981 110 0 0 25 0 1 0 539599361 173830144 38359 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42439 38359 603 41 0 42398 0
vsize: 169756
[startup+890.872 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41940 0 0 0 88981 110 0 0 25 0 1 0 539599361 173830144 38366 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42439 38366 603 41 0 42398 0
vsize: 169756
[startup+900.873 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41950 0 0 0 89982 111 0 0 25 0 1 0 539599361 173965312 38376 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42472 38376 603 41 0 42431 0
vsize: 169888
[startup+910.874 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41957 0 0 0 90982 111 0 0 25 0 1 0 539599361 173965312 38383 4294967295 134512640 134672761 3221224528 3221223664 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42472 38383 603 41 0 42431 0
vsize: 169888
[startup+920.873 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41964 0 0 0 91982 111 0 0 25 0 1 0 539599361 173965312 38390 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42472 38390 603 41 0 42431 0
vsize: 169888
[startup+930.873 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41974 0 0 0 92982 111 0 0 25 0 1 0 539599361 173965312 38400 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42472 38400 603 41 0 42431 0
vsize: 169888
[startup+940.873 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41978 0 0 0 93982 111 0 0 25 0 1 0 539599361 174096384 38404 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42504 38404 603 41 0 42463 0
vsize: 170016
[startup+950.873 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41987 0 0 0 94982 111 0 0 25 0 1 0 539599361 174096384 38413 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42504 38413 603 41 0 42463 0
vsize: 170016
[startup+960.873 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 41998 0 0 0 95982 111 0 0 25 0 1 0 539599361 174096384 38424 4294967295 134512640 134672761 3221224528 3221223728 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42504 38424 603 41 0 42463 0
vsize: 170016
[startup+970.873 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42003 0 0 0 96983 111 0 0 25 0 1 0 539599361 174223360 38429 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42535 38429 603 41 0 42494 0
vsize: 170140
[startup+980.874 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42009 0 0 0 97983 111 0 0 25 0 1 0 539599361 174223360 38435 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42535 38435 603 41 0 42494 0
vsize: 170140
[startup+990.883 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42017 0 0 0 98984 111 0 0 25 0 1 0 539599361 174223360 38443 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42535 38443 603 41 0 42494 0
vsize: 170140
[startup+1000.88 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42028 0 0 0 99984 111 0 0 25 0 1 0 539599361 174223360 38454 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42535 38454 603 41 0 42494 0
vsize: 170140
[startup+1010.88 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42257 0 0 0 100983 112 0 0 25 0 1 0 539599361 175202304 38683 4294967295 134512640 134672761 3221224528 3221223632 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42774 38683 603 41 0 42733 0
vsize: 171096
[startup+1020.88 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42437 0 0 0 101983 112 0 0 25 0 1 0 539599361 175923200 38863 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42950 38863 603 41 0 42909 0
vsize: 171800
[startup+1030.88 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42566 0 0 0 102983 113 0 0 25 0 1 0 539599361 176455680 38992 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43080 38992 603 41 0 43039 0
vsize: 172320
[startup+1040.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42604 0 0 0 103983 113 0 0 25 0 1 0 539599361 176586752 39030 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43112 39030 603 41 0 43071 0
vsize: 172448
[startup+1050.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42636 0 0 0 104983 113 0 0 25 0 1 0 539599361 176721920 39062 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43145 39064 603 41 0 43104 0
vsize: 172580
[startup+1060.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42670 0 0 0 105983 113 0 0 25 0 1 0 539599361 176861184 39096 4294967295 134512640 134672761 3221224528 3221223632 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43179 39096 603 41 0 43138 0
vsize: 172716
[startup+1070.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42711 0 0 0 106983 113 0 0 25 0 1 0 539599361 176996352 39137 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43212 39137 603 41 0 43171 0
vsize: 172848
[startup+1080.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42724 0 0 0 107984 113 0 0 25 0 1 0 539599361 176996352 39150 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43212 39150 603 41 0 43171 0
vsize: 172848
[startup+1090.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42739 0 0 0 108984 113 0 0 25 0 1 0 539599361 177131520 39165 4294967295 134512640 134672761 3221224528 3221223632 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43245 39165 603 41 0 43204 0
vsize: 172980
[startup+1100.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42749 0 0 0 109983 114 0 0 25 0 1 0 539599361 177131520 39175 4294967295 134512640 134672761 3221224528 3221223632 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43245 39175 603 41 0 43204 0
vsize: 172980
[startup+1110.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42769 0 0 0 110983 114 0 0 25 0 1 0 539599361 177266688 39195 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43278 39195 603 41 0 43237 0
vsize: 173112
[startup+1120.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42800 0 0 0 111983 114 0 0 25 0 1 0 539599361 177385472 39226 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43307 39226 603 41 0 43266 0
vsize: 173228
[startup+1130.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42838 0 0 0 112984 114 0 0 25 0 1 0 539599361 177524736 39264 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43341 39264 603 41 0 43300 0
vsize: 173364
[startup+1140.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42847 0 0 0 113984 114 0 0 25 0 1 0 539599361 177524736 39273 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43341 39273 603 41 0 43300 0
vsize: 173364
[startup+1150.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42861 0 0 0 114984 114 0 0 25 0 1 0 539599361 177524736 39287 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43341 39287 603 41 0 43300 0
vsize: 173364
[startup+1160.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42868 0 0 0 115984 114 0 0 25 0 1 0 539599361 177655808 39294 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43373 39294 603 41 0 43332 0
vsize: 173492
[startup+1170.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42876 0 0 0 116984 114 0 0 25 0 1 0 539599361 177655808 39302 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43373 39302 603 41 0 43332 0
vsize: 173492
[startup+1180.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42884 0 0 0 117984 114 0 0 25 0 1 0 539599361 177655808 39310 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43373 39310 603 41 0 43332 0
vsize: 173492
[startup+1190.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42939 0 0 0 118985 114 0 0 25 0 1 0 539599361 178311168 39365 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43533 39365 603 41 0 43492 0
vsize: 174132
[startup+1200.89 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 18620
Raw data (stat): 18620 (minisat+) R 18619 22612 22611 0 -1 0 42955 0 0 0 119985 114 0 0 25 0 1 0 539599361 178311168 39381 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43533 39381 603 41 0 43492 0
vsize: 174132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1201.03 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 18620
Raw data (stat): 18620 (minisat+) Z 18619 22612 22611 0 -1 12 42958 0 0 0 119985 122 0 0 21 0 1 0 539599361 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: 10
Real time (s): 1201.03
CPU time (s): 1201.08
CPU user time (s): 1199.85
CPU system time (s): 1.22681
CPU usage (%): 100.004
Max. virtual memory (Kb): 174132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####