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-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
Optimality of the best value was proved	NO
Number of terms in the objective function	210
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	7516192761
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	7516192761
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	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 13651

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-20 21:13:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14494 boxname=wulflinc20 idbench=1115 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 14494
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        725496 kB
Buffers:         33768 kB
Cached:         249808 kB
SwapCached:        528 kB
Active:         163676 kB
Inactive:       121880 kB
HighTotal:      131008 kB
HighFree:          980 kB
LowTotal:       903652 kB
LowFree:        724516 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            17876 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 21:33:53 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 14494 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  12]---> BDD-cost:75277
c ---[  10]---> BDD-cost:110257
c ---[   8]---> BDD-cost:99901
c ---[   6]---> BDD-cost:112483
c ---[   4]---> BDD-cost:82177
c ---[   2]---> BDD-cost:116705
c ---[   0]---> BDD-cost:69441
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1906914  5553068 |  635638       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 10303321[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2159     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 |        61 | 1912357  5565815 |  637452      59     2568    43.5 |  0.000 % |
c ==============================================================================
c [1mFound solution: 8257359[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 |        66 | 1912404  5566011 |  637468      64     2644    41.3 |  0.000 % |
c |       170 | 1912404  5566011 |  701214     168    30730   182.9 |  0.018 % |
c |       321 | 1912404  5566011 |  771336     319    40443   126.8 |  0.018 % |
c |       546 | 1912404  5566011 |  848469     544    51337    94.4 |  0.018 % |
c |       883 | 1912404  5566011 |  933316     881   124886   141.8 |  0.018 % |
c |      1390 | 1912404  5566011 | 1026648    1388   159195   114.7 |  0.018 % |
c ==============================================================================
c [1mFound solution: 8170590[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 |      1499 | 1912426  5566064 |  637475    1497   164057   109.6 |  0.018 % |
c ==============================================================================
c [1mFound solution: 6944472[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 |      1501 | 1912455  5566143 |  637485    1499   164093   109.5 |  0.018 % |
c |      1603 | 1912455  5566143 |  701233    1601   189894   118.6 |  0.019 % |
c |      1753 | 1912455  5566143 |  771356    1751   196656   112.3 |  0.019 % |
c |      1978 | 1912455  5566143 |  848492    1976   213529   108.1 |  0.019 % |
c |      2317 | 1912455  5566143 |  933341    2315   227568    98.3 |  0.019 % |
c |      2825 | 1912455  5566143 | 1026675    2823   263097    93.2 |  0.019 % |
c |      3585 | 1912455  5566143 | 1129343    3583   302077    84.3 |  0.019 % |
c ==============================================================================
c [1mFound solution: 6819989[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 |      3604 | 1912481  5566205 |  637493    3602   303059    84.1 |  0.019 % |
c |      3705 | 1912481  5566205 |  701242    3703   308842    83.4 |  0.019 % |
c |      3857 | 1912481  5566205 |  771366    3855   339437    88.1 |  0.019 % |
c |      4082 | 1912481  5566205 |  848503    4080   351848    86.2 |  0.019 % |
c ==============================================================================
c [1mFound solution: 6788725[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 |      4168 | 1912497  5566247 |  637499    4166   355871    85.4 |  0.019 % |
c |      4269 | 1912497  5566247 |  701248    4267   380365    89.1 |  0.019 % |
c |      4420 | 1912497  5566247 |  771373    4418   390683    88.4 |  0.019 % |
c |      4647 | 1912497  5566247 |  848511    4645   403739    86.9 |  0.019 % |
c |      4984 | 1912497  5566247 |  933362    4982   429461    86.2 |  0.019 % |
c |      5490 | 1912497  5566247 | 1026698    5488   470098    85.7 |  0.019 % |
c |      6249 | 1912497  5566247 | 1129368    6247   519979    83.2 |  0.019 % |
c |      7389 | 1912497  5566247 | 1242305    7387   597583    80.9 |  0.019 % |
c |      9098 | 1912497  5566247 | 1366535    9096   690914    76.0 |  0.019 % |
#### 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.74 0.86 0.87 2/54 23283
Raw data (stat): 23283 (runsolver) R 23282 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539592019 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+9.99993 s]
Raw data (loadavg): 0.78 0.86 0.87 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 54458 0 0 0 875 124 0 0 25 0 1 0 539592019 244772864 49803 4294967295 134512640 134672761 3221224528 3221205744 134566692 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59759 49803 603 41 0 59718 0
vsize: 239036
[startup+19.9995 s]
Raw data (loadavg): 0.81 0.87 0.87 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61120 0 0 0 1858 141 0 0 25 0 1 0 539592019 266805248 56465 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65138 56465 603 41 0 65097 0
vsize: 260552
[startup+30.0007 s]
Raw data (loadavg): 0.84 0.87 0.87 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61206 0 0 0 2857 142 0 0 25 0 1 0 539592019 269873152 56551 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65887 56551 603 41 0 65846 0
vsize: 263548
[startup+40 s]
Raw data (loadavg): 0.86 0.87 0.87 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61376 0 0 0 3856 142 0 0 25 0 1 0 539592019 270790656 56716 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66111 56716 603 41 0 66070 0
vsize: 264444
[startup+50.0007 s]
Raw data (loadavg): 0.96 0.89 0.88 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61382 0 0 0 4856 143 0 0 25 0 1 0 539592019 270921728 56722 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66143 56722 603 41 0 66102 0
vsize: 264572
[startup+60.0008 s]
Raw data (loadavg): 1.04 0.91 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61392 0 0 0 5856 143 0 0 25 0 1 0 539592019 270921728 56732 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66143 56732 603 41 0 66102 0
vsize: 264572
[startup+70.0011 s]
Raw data (loadavg): 1.04 0.91 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61443 0 0 0 6856 143 0 0 25 0 1 0 539592019 271056896 56783 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66176 56783 603 41 0 66135 0
vsize: 264704
[startup+80.0018 s]
Raw data (loadavg): 1.03 0.92 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61488 0 0 0 7856 143 0 0 25 0 1 0 539592019 271331328 56828 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66243 56828 603 41 0 66202 0
vsize: 264972
[startup+90.002 s]
Raw data (loadavg): 1.02 0.92 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61500 0 0 0 8856 144 0 0 25 0 1 0 539592019 271331328 56840 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66243 56840 603 41 0 66202 0
vsize: 264972
[startup+100.002 s]
Raw data (loadavg): 1.02 0.92 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61510 0 0 0 9855 144 0 0 25 0 1 0 539592019 271331328 56850 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66243 56850 603 41 0 66202 0
vsize: 264972
[startup+110.002 s]
Raw data (loadavg): 1.02 0.92 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61518 0 0 0 10855 144 0 0 25 0 1 0 539592019 271462400 56858 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66275 56858 603 41 0 66234 0
vsize: 265100
[startup+120.002 s]
Raw data (loadavg): 1.01 0.92 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61525 0 0 0 11855 144 0 0 25 0 1 0 539592019 271462400 56865 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66275 56865 603 41 0 66234 0
vsize: 265100
[startup+130.002 s]
Raw data (loadavg): 1.01 0.93 0.89 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61554 0 0 0 12856 144 0 0 25 0 1 0 539592019 271462400 56894 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66275 56894 603 41 0 66234 0
vsize: 265100
[startup+140.002 s]
Raw data (loadavg): 1.01 0.93 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61575 0 0 0 13855 145 0 0 25 0 1 0 539592019 271597568 56915 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66308 56915 603 41 0 66267 0
vsize: 265232
[startup+150.019 s]
Raw data (loadavg): 1.01 0.93 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61581 0 0 0 14857 145 0 0 25 0 1 0 539592019 271597568 56921 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66308 56921 603 41 0 66267 0
vsize: 265232
[startup+160.019 s]
Raw data (loadavg): 1.01 0.93 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61587 0 0 0 15857 145 0 0 25 0 1 0 539592019 271597568 56927 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66308 56927 603 41 0 66267 0
vsize: 265232
[startup+170.02 s]
Raw data (loadavg): 1.00 0.93 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61594 0 0 0 16857 145 0 0 25 0 1 0 539592019 271597568 56934 4294967295 134512640 134672761 3221224528 3221223632 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66308 56934 603 41 0 66267 0
vsize: 265232
[startup+180.02 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61602 0 0 0 17857 145 0 0 25 0 1 0 539592019 271732736 56942 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66341 56942 603 41 0 66300 0
vsize: 265364
[startup+190.024 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61612 0 0 0 18858 145 0 0 25 0 1 0 539592019 271732736 56952 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66341 56952 603 41 0 66300 0
vsize: 265364
[startup+200.024 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61622 0 0 0 19858 145 0 0 25 0 1 0 539592019 271732736 56962 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66341 56962 603 41 0 66300 0
vsize: 265364
[startup+210.024 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61630 0 0 0 20858 145 0 0 25 0 1 0 539592019 271867904 56970 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66374 56970 603 41 0 66333 0
vsize: 265496
[startup+220.033 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61642 0 0 0 21859 145 0 0 25 0 1 0 539592019 271867904 56982 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66374 56982 603 41 0 66333 0
vsize: 265496
[startup+230.032 s]
Raw data (loadavg): 1.00 0.94 0.90 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61647 0 0 0 22859 145 0 0 25 0 1 0 539592019 271867904 56987 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66374 56987 603 41 0 66333 0
vsize: 265496
[startup+240.032 s]
Raw data (loadavg): 1.00 0.94 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61654 0 0 0 23859 145 0 0 25 0 1 0 539592019 271867904 56994 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66374 56994 603 41 0 66333 0
vsize: 265496
[startup+250.033 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61662 0 0 0 24859 145 0 0 25 0 1 0 539592019 271867904 57002 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66374 57002 603 41 0 66333 0
vsize: 265496
[startup+260.038 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61669 0 0 0 25860 145 0 0 25 0 1 0 539592019 271998976 57009 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66406 57009 603 41 0 66365 0
vsize: 265624
[startup+270.075 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61676 0 0 0 26864 145 0 0 25 0 1 0 539592019 271998976 57016 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66406 57016 603 41 0 66365 0
vsize: 265624
[startup+280.075 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61685 0 0 0 27864 145 0 0 25 0 1 0 539592019 271998976 57025 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66406 57025 603 41 0 66365 0
vsize: 265624
[startup+290.076 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61693 0 0 0 28864 145 0 0 25 0 1 0 539592019 271998976 57033 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66406 57033 603 41 0 66365 0
vsize: 265624
[startup+300.076 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61697 0 0 0 29864 145 0 0 25 0 1 0 539592019 272130048 57037 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66438 57037 603 41 0 66397 0
vsize: 265752
[startup+310.075 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61703 0 0 0 30864 145 0 0 25 0 1 0 539592019 272130048 57043 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66438 57043 603 41 0 66397 0
vsize: 265752
[startup+320.075 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61710 0 0 0 31865 145 0 0 25 0 1 0 539592019 272130048 57050 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66438 57050 603 41 0 66397 0
vsize: 265752
[startup+330.076 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61717 0 0 0 32865 145 0 0 25 0 1 0 539592019 272130048 57057 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66438 57057 603 41 0 66397 0
vsize: 265752
[startup+340.075 s]
Raw data (loadavg): 1.00 0.95 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61731 0 0 0 33864 145 0 0 25 0 1 0 539592019 272130048 57071 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66438 57071 603 41 0 66397 0
vsize: 265752
[startup+350.076 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61765 0 0 0 34864 145 0 0 25 0 1 0 539592019 272265216 57105 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66471 57105 603 41 0 66430 0
vsize: 265884
[startup+360.091 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61769 0 0 0 35866 145 0 0 25 0 1 0 539592019 272400384 57109 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66504 57109 603 41 0 66463 0
vsize: 266016
[startup+370.092 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61781 0 0 0 36866 145 0 0 25 0 1 0 539592019 272400384 57121 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66504 57121 603 41 0 66463 0
vsize: 266016
[startup+380.095 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61810 0 0 0 37867 145 0 0 25 0 1 0 539592019 272535552 57150 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66537 57150 603 41 0 66496 0
vsize: 266148
[startup+390.095 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61817 0 0 0 38867 146 0 0 25 0 1 0 539592019 272535552 57157 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66537 57157 603 41 0 66496 0
vsize: 266148
[startup+400.096 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61824 0 0 0 39867 146 0 0 25 0 1 0 539592019 272535552 57164 4294967295 134512640 134672761 3221224528 3221223712 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66537 57164 603 41 0 66496 0
vsize: 266148
[startup+410.106 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61832 0 0 0 40868 146 0 0 25 0 1 0 539592019 272666624 57172 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66569 57172 603 41 0 66528 0
vsize: 266276
[startup+420.107 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61838 0 0 0 41868 146 0 0 25 0 1 0 539592019 272666624 57178 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66569 57178 603 41 0 66528 0
vsize: 266276
[startup+430.111 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61849 0 0 0 42868 146 0 0 25 0 1 0 539592019 272666624 57189 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66569 57189 603 41 0 66528 0
vsize: 266276
[startup+440.11 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61859 0 0 0 43868 146 0 0 25 0 1 0 539592019 272666624 57199 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66569 57199 603 41 0 66528 0
vsize: 266276
[startup+450.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61867 0 0 0 44858 146 0 0 25 0 1 0 539592019 272801792 57207 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66602 57207 603 41 0 66561 0
vsize: 266408
[startup+460.11 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61876 0 0 0 45858 146 0 0 25 0 1 0 539592019 272801792 57216 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66602 57216 603 41 0 66561 0
vsize: 266408
[startup+470.111 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61886 0 0 0 46858 146 0 0 25 0 1 0 539592019 272801792 57226 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66602 57226 603 41 0 66561 0
vsize: 266408
[startup+480.131 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61897 0 0 0 47860 146 0 0 25 0 1 0 539592019 272928768 57237 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66633 57237 603 41 0 66592 0
vsize: 266532
[startup+490.136 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61904 0 0 0 48861 146 0 0 25 0 1 0 539592019 272928768 57244 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66633 57244 603 41 0 66592 0
vsize: 266532
[startup+500.137 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61911 0 0 0 49861 146 0 0 25 0 1 0 539592019 272928768 57251 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66633 57251 603 41 0 66592 0
vsize: 266532
[startup+510.136 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61922 0 0 0 50861 146 0 0 25 0 1 0 539592019 272928768 57262 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66633 57262 603 41 0 66592 0
vsize: 266532
[startup+520.137 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61930 0 0 0 51861 146 0 0 25 0 1 0 539592019 273059840 57270 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57270 603 41 0 66624 0
vsize: 266660
[startup+530.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61940 0 0 0 52861 146 0 0 25 0 1 0 539592019 273059840 57280 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57280 603 41 0 66624 0
vsize: 266660
[startup+540.138 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61947 0 0 0 53862 146 0 0 25 0 1 0 539592019 273059840 57287 4294967295 134512640 134672761 3221224528 3221223728 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57287 603 41 0 66624 0
vsize: 266660
[startup+550.14 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61955 0 0 0 54862 146 0 0 25 0 1 0 539592019 273059840 57295 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57295 603 41 0 66624 0
vsize: 266660
[startup+560.14 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61963 0 0 0 55862 146 0 0 25 0 1 0 539592019 273195008 57303 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57303 603 41 0 66657 0
vsize: 266792
[startup+570.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61969 0 0 0 56862 146 0 0 25 0 1 0 539592019 273195008 57309 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57309 603 41 0 66657 0
vsize: 266792
[startup+580.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61974 0 0 0 57862 146 0 0 25 0 1 0 539592019 273195008 57314 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57314 603 41 0 66657 0
vsize: 266792
[startup+590.139 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61980 0 0 0 58862 146 0 0 25 0 1 0 539592019 273195008 57320 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57320 603 41 0 66657 0
vsize: 266792
[startup+600.14 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61985 0 0 0 59863 146 0 0 25 0 1 0 539592019 273195008 57325 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57325 603 41 0 66657 0
vsize: 266792
[startup+610.141 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61989 0 0 0 60863 147 0 0 25 0 1 0 539592019 273195008 57329 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66698 57329 603 41 0 66657 0
vsize: 266792
[startup+620.141 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61995 0 0 0 61863 147 0 0 25 0 1 0 539592019 273330176 57335 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66731 57335 603 41 0 66690 0
vsize: 266924
[startup+630.157 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62002 0 0 0 62865 147 0 0 25 0 1 0 539592019 273330176 57342 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66731 57342 603 41 0 66690 0
vsize: 266924
[startup+640.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62010 0 0 0 63867 147 0 0 25 0 1 0 539592019 273330176 57350 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66731 57350 603 41 0 66690 0
vsize: 266924
[startup+650.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62020 0 0 0 64867 147 0 0 25 0 1 0 539592019 273330176 57360 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66731 57360 603 41 0 66690 0
vsize: 266924
[startup+660.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62023 0 0 0 65867 147 0 0 25 0 1 0 539592019 273330176 57363 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66731 57363 603 41 0 66690 0
vsize: 266924
[startup+670.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62030 0 0 0 66867 147 0 0 25 0 1 0 539592019 273461248 57370 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 57370 603 41 0 66722 0
vsize: 267052
[startup+680.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62034 0 0 0 67868 147 0 0 25 0 1 0 539592019 273461248 57374 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 57374 603 41 0 66722 0
vsize: 267052
[startup+690.178 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62039 0 0 0 68868 147 0 0 25 0 1 0 539592019 273461248 57379 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 57379 603 41 0 66722 0
vsize: 267052
[startup+700.179 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62044 0 0 0 69868 147 0 0 25 0 1 0 539592019 273461248 57384 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 57384 603 41 0 66722 0
vsize: 267052
[startup+710.179 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62056 0 0 0 70867 147 0 0 25 0 1 0 539592019 273461248 57396 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 57396 603 41 0 66722 0
vsize: 267052
[startup+720.179 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62065 0 0 0 71867 147 0 0 25 0 1 0 539592019 273592320 57405 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66795 57405 603 41 0 66754 0
vsize: 267180
[startup+730.181 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62075 0 0 0 72867 147 0 0 25 0 1 0 539592019 273592320 57415 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66795 57415 603 41 0 66754 0
vsize: 267180
[startup+740.18 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62085 0 0 0 73867 148 0 0 25 0 1 0 539592019 273592320 57425 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66795 57425 603 41 0 66754 0
vsize: 267180
[startup+750.183 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62101 0 0 0 74868 148 0 0 25 0 1 0 539592019 273727488 57441 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66828 57441 603 41 0 66787 0
vsize: 267312
[startup+760.183 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62106 0 0 0 75868 148 0 0 25 0 1 0 539592019 273727488 57446 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66828 57446 603 41 0 66787 0
vsize: 267312
[startup+770.183 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62117 0 0 0 76868 148 0 0 25 0 1 0 539592019 273727488 57457 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66828 57457 603 41 0 66787 0
vsize: 267312
[startup+780.184 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62127 0 0 0 77868 148 0 0 25 0 1 0 539592019 273862656 57467 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66861 57467 603 41 0 66820 0
vsize: 267444
[startup+790.183 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62139 0 0 0 78868 148 0 0 25 0 1 0 539592019 273862656 57479 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66861 57479 603 41 0 66820 0
vsize: 267444
[startup+800.184 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62154 0 0 0 79868 148 0 0 25 0 1 0 539592019 274001920 57494 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66895 57494 603 41 0 66854 0
vsize: 267580
[startup+810.185 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62280 0 0 0 80868 148 0 0 25 0 1 0 539592019 274444288 57620 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67003 57620 603 41 0 66962 0
vsize: 268012
[startup+820.184 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62439 0 0 0 81868 148 0 0 25 0 1 0 539592019 275140608 57779 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67173 57779 603 41 0 67132 0
vsize: 268692
[startup+830.185 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62584 0 0 0 82868 149 0 0 25 0 1 0 539592019 275705856 57924 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67311 57924 603 41 0 67270 0
vsize: 269244
[startup+840.185 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62748 0 0 0 83867 150 0 0 25 0 1 0 539592019 276393984 58088 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67479 58088 603 41 0 67438 0
vsize: 269916
[startup+850.186 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62891 0 0 0 84867 150 0 0 25 0 1 0 539592019 276938752 58231 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67612 58231 603 41 0 67571 0
vsize: 270448
[startup+860.186 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63005 0 0 0 85867 151 0 0 25 0 1 0 539592019 277368832 58345 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67717 58345 603 41 0 67676 0
vsize: 270868
[startup+870.186 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63093 0 0 0 86867 151 0 0 25 0 1 0 539592019 277774336 58433 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67816 58433 603 41 0 67775 0
vsize: 271264
[startup+880.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63255 0 0 0 87867 151 0 0 25 0 1 0 539592019 278495232 58595 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67992 58595 603 41 0 67951 0
vsize: 271968
[startup+890.186 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63366 0 0 0 88867 151 0 0 25 0 1 0 539592019 278913024 58706 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68094 58706 603 41 0 68053 0
vsize: 272376
[startup+900.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63423 0 0 0 89867 151 0 0 25 0 1 0 539592019 279207936 58763 4294967295 134512640 134672761 3221224528 3221223632 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68166 58763 603 41 0 68125 0
vsize: 272664
[startup+910.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63438 0 0 0 90867 151 0 0 25 0 1 0 539592019 279207936 58778 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68166 58778 603 41 0 68125 0
vsize: 272664
[startup+920.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63453 0 0 0 91867 151 0 0 25 0 1 0 539592019 279207936 58793 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68166 58793 603 41 0 68125 0
vsize: 272664
[startup+930.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63473 0 0 0 92867 151 0 0 25 0 1 0 539592019 279351296 58813 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68201 58813 603 41 0 68160 0
vsize: 272804
[startup+940.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63508 0 0 0 93867 152 0 0 25 0 1 0 539592019 279490560 58848 4294967295 134512640 134672761 3221224528 3221223632 134560267 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68235 58848 603 41 0 68194 0
vsize: 272940
[startup+950.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63557 0 0 0 94867 152 0 0 25 0 1 0 539592019 279642112 58897 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68272 58897 603 41 0 68231 0
vsize: 273088
[startup+960.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63572 0 0 0 95868 152 0 0 25 0 1 0 539592019 279781376 58912 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68306 58912 603 41 0 68265 0
vsize: 273224
[startup+970.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63601 0 0 0 96867 152 0 0 25 0 1 0 539592019 279920640 58941 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68340 58941 603 41 0 68299 0
vsize: 273360
[startup+980.187 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63627 0 0 0 97868 152 0 0 25 0 1 0 539592019 280055808 58967 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68373 58967 603 41 0 68332 0
vsize: 273492
[startup+990.188 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63647 0 0 0 98867 152 0 0 25 0 1 0 539592019 280055808 58987 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68373 58987 603 41 0 68332 0
vsize: 273492
[startup+1000.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63667 0 0 0 99868 152 0 0 25 0 1 0 539592019 280199168 59007 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68408 59007 603 41 0 68367 0
vsize: 273632
[startup+1010.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63686 0 0 0 100868 152 0 0 25 0 1 0 539592019 280199168 59026 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68408 59026 603 41 0 68367 0
vsize: 273632
[startup+1020.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63715 0 0 0 101868 152 0 0 25 0 1 0 539592019 280322048 59055 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68438 59055 603 41 0 68397 0
vsize: 273752
[startup+1030.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63736 0 0 0 102868 152 0 0 25 0 1 0 539592019 280469504 59076 4294967295 134512640 134672761 3221224528 3221223632 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68474 59076 603 41 0 68433 0
vsize: 273896
[startup+1040.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63756 0 0 0 103868 153 0 0 25 0 1 0 539592019 280469504 59096 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68474 59096 603 41 0 68433 0
vsize: 273896
[startup+1050.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63771 0 0 0 104868 153 0 0 25 0 1 0 539592019 280612864 59111 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68509 59111 603 41 0 68468 0
vsize: 274036
[startup+1060.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63791 0 0 0 105868 153 0 0 25 0 1 0 539592019 280612864 59131 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68509 59131 603 41 0 68468 0
vsize: 274036
[startup+1070.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63806 0 0 0 106868 153 0 0 25 0 1 0 539592019 280756224 59146 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68544 59146 603 41 0 68503 0
vsize: 274176
[startup+1080.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63826 0 0 0 107868 153 0 0 25 0 1 0 539592019 280756224 59166 4294967295 134512640 134672761 3221224528 3221223632 134560201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68544 59166 603 41 0 68503 0
vsize: 274176
[startup+1090.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63842 0 0 0 108869 153 0 0 25 0 1 0 539592019 280903680 59182 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68580 59182 603 41 0 68539 0
vsize: 274320
[startup+1100.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63874 0 0 0 109869 153 0 0 25 0 1 0 539592019 281055232 59214 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68617 59214 603 41 0 68576 0
vsize: 274468
[startup+1110.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63894 0 0 0 110869 153 0 0 25 0 1 0 539592019 281055232 59234 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68617 59234 603 41 0 68576 0
vsize: 274468
[startup+1120.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63910 0 0 0 111869 153 0 0 25 0 1 0 539592019 281198592 59250 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68652 59250 603 41 0 68611 0
vsize: 274608
[startup+1130.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63930 0 0 0 112869 154 0 0 25 0 1 0 539592019 281198592 59270 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68652 59270 603 41 0 68611 0
vsize: 274608
[startup+1140.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63951 0 0 0 113869 154 0 0 25 0 1 0 539592019 281341952 59291 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68687 59291 603 41 0 68646 0
vsize: 274748
[startup+1150.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63968 0 0 0 114869 154 0 0 25 0 1 0 539592019 281341952 59308 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68687 59308 603 41 0 68646 0
vsize: 274748
[startup+1160.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63983 0 0 0 115869 154 0 0 25 0 1 0 539592019 281477120 59323 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68720 59323 603 41 0 68679 0
vsize: 274880
[startup+1170.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64005 0 0 0 116869 154 0 0 25 0 1 0 539592019 281477120 59345 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68720 59345 603 41 0 68679 0
vsize: 274880
[startup+1180.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64026 0 0 0 117869 154 0 0 25 0 1 0 539592019 281612288 59366 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68753 59366 603 41 0 68712 0
vsize: 275012
[startup+1190.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64041 0 0 0 118870 154 0 0 25 0 1 0 539592019 281612288 59381 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68753 59381 603 41 0 68712 0
vsize: 275012
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 23283
Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64061 0 0 0 119870 154 0 0 25 0 1 0 539592019 281755648 59401 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68788 59401 603 41 0 68747 0
vsize: 275152
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.31 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 23283
Raw data (stat): 23283 (minisat+) Z 23282 27565 27564 0 -1 12 64064 0 0 0 119870 166 0 0 25 0 1 0 539592019 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.31
CPU time (s): 1200.37
CPU user time (s): 1198.7
CPU system time (s): 1.66575
CPU usage (%): 100.005
Max. virtual memory (Kb): 275152
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####